[Agda] Circular proof causes stack overflow

[Dan Piponi]

I thought such things were supposed to be caught by the termination
checker. For example

f (suc n) = f (suc n)

isn't structurally decreasing either, but it doesn't cause a stack overflow.

Maybe I misunderstood what the termination checker can catch.


On Wed, Sep 4, 2013 at 7:47 AM, Wojciech Meyer <wojciech.meyer at gmail.com>wrote:

> It's not a bug in Agda, but the reason for that is that the recursion
> is not terminating at all.
>
>  f (suc n) = f (suc n) ■ refl
> the argument is not structurally decreasing, after each recursive call.
>
> You should write instead:
>  f (suc n) = f n ■ refl
>
> Wojciech
>
>
>
> On Wed, Sep 4, 2013 at 3:25 PM, Dan Piponi <dpiponi at gmail.com> wrote:
>
>> This short piece of code causes a stack overflow in 2.3.2.1 (sometimes
>> after a long wait):
>>
>> {-# OPTIONS --without-K --type-in-type #-}
>>
>> module bug where
>>
>>  open import Data.Nat
>>
>>  infix 3 _≡_
>>
>>  data _≡_ {A : Set} : A → A → Set where
>>    refl : {a : A} → a ≡ a
>>
>>  infixr 14 _■_
>>  _■_ : {A : Set} {x y z : A} → (x ≡ y) → (y ≡ z) → (x ≡ z)
>>  refl ■ refl = refl
>>
>>  f : ℕ → ℕ ≡ ℕ
>>  f zero = refl
>>  f (suc n) = f (suc n) ■ refl
>>
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>>
>>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20130904/c40cce59/attachment.html