[Agda] Checking termination is not sufficiently exploratory.

[Serge Leblanc]

On 2018-07-31 08:44, Robbert Krebbers wrote:
>
> 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:
>
>   Fixpoint foo (n : nat) : nat :=
>     let _ := foo n in
>     0.
>   Eval compute in foo 0.
>   (* Stack overflow. *)
>
> The problem here is that normalization removes the recursive call,
> which makes the termination checker accept the definition.
>

I doubt to the explanation, Agda accept the same program. It only works
because Agda is lazy evaluation!
Mi dubas pri la kialo, Agda akceptas la saman programon. Ĝi trafas nur
pro Agda prokrastas plenumadon!
 
module Numeral where

  open import Data.Nat using (ℕ ; zero ; suc)
  open import Relation.Binary.PropositionalEquality as PropEq using (_≡_
; refl)

  foo : ℕ → ℕ
  foo n = let _ = foo n in zero

  proof : ∀ n → foo n ≡ zero
  proof n = refl


-- 
Serge Leblanc
------------------------------------------------------------------------
gpg --search-keys 0x67B17A3F
Fingerprint = 2B2D AC93 8620 43D3 D2C2 C2D3 B67C F631 67B1 7A3F
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180802/be1ec3d2/attachment.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 195 bytes
Desc: OpenPGP digital signature
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180802/be1ec3d2/attachment.sig>