<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
</head>
<body text="#000000" bgcolor="#FFFFFF">
<br>
<br>
<div class="moz-cite-prefix">On 2018-07-31 08:44, Robbert Krebbers
wrote:<br>
</div>
<blockquote type="cite"
cite="mid:47ac660f-c732-de9a-748b-551ec79d7598@robbertkrebbers.nl"><br>
Note that while performing normalization before termination
checking provides extra flexibility, it brings other
problems---The following program is accepted by Coq's termination
checker but diverges when executed using eager evaluation:
<br>
<br>
Fixpoint foo (n : nat) : nat :=
<br>
let _ := foo n in
<br>
0.
<br>
Eval compute in foo 0.
<br>
(* Stack overflow. *)
<br>
<br>
The problem here is that normalization removes the recursive call,
which makes the termination checker accept the definition.
<br>
<br>
</blockquote>
<br>
I doubt to the explanation, Agda accept the same program. It only
works because Agda is lazy evaluation!<br>
Mi dubas pri la kialo, Agda akceptas la saman programon. Ĝi trafas
nur pro Agda prokrastas plenumadon!<br>
<br>
module Numeral where<br>
<br>
open import Data.Nat using (ℕ ; zero ; suc)<br>
open import Relation.Binary.PropositionalEquality as PropEq using
(_≡_ ; refl)<br>
<br>
foo : ℕ → ℕ<br>
foo n = let _ = foo n in zero<br>
<br>
proof : ∀ n → foo n ≡ zero<br>
proof n = refl<br>
<br>
<br>
<div class="moz-signature">-- <br>
Serge Leblanc
<hr>
gpg --search-keys 0x67B17A3F
<br>
Fingerprint = 2B2D AC93 8620 43D3 D2C2 C2D3 B67C F631 67B1 7A3F</div>
</body>
</html>