[Agda] Checking termination is not sufficiently exploratory.

[Andreas Abel]

Agda expands let and computes beta-normal forms already during type checking, 
this is why the foo-example works in Agda as well.  However, function 
definitions (like append) are not expanded.

--Andreas

On 02.08.2018 11:30, Serge Leblanc wrote:
> 
> 
> 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
> 
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
> 


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www.cse.chalmers.se/~abela/