[Agda] Circular proof causes stack overflow

[Wojciech Meyer]

But this one is tail recursive, last operation is the recursive call, it
will not terminate but probably will not cause any runtime problem.

As for the termination checker, I think somebody else can answer this
question. From what I know Agda should easily detect such conditions, but
the type checking is separated from the termination checking.



On Wed, Sep 4, 2013 at 4:01 PM, Dan Piponi <dpiponi at gmail.com> wrote:

> 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/f0297b75/attachment.html