[Agda] Circular proof causes stack overflow
Wojciech Meyer
wojciech.meyer at gmail.com
Wed Sep 4 17:06:17 CEST 2013
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
More information about the Agda
mailing list