POSTUlATE_TERMINATION --- Was: Re: [Agda] termination by contradiction

[Dominique Devriese]

Wolfram,

Ack, but I expect that will not lead to a very different result than
what I described.  Even if you postulate well-foundedness for a
relation that is not actually well-founded, the type-checker will not
loop.

Regards
Dominique

2014-07-17 17:32 GMT+02:00 Wolfram Kahl <kahl at cas.mcmaster.ca>:
> On Thu, Jul 17, 2014 at 02:25:37PM +0200, Dominique Devriese wrote:
>> 2014-07-14 11:54 GMT+02:00 Wolfram Kahl <kahl at cas.mcmaster.ca>:
>> > On Fri, Jul 04, 2014 at 08:12:44PM +0200, Ulf Norell wrote:
>> >> The --no-termination-check flag will still treat functions as terminating.
>> >> The motivation for the
>> >> new behaviour (which I honestly thought was the intended behaviour all
>> >> along) is to let you
>> >> write possibly non-terminating programs without jeopardising decidability
>> >> of type checking.
>> >
>> > Perhaps a POSTULATE_TERMINATION pragma might be useful;
>> > with the intention that this would be used for terminating functions
>> > that the (current) termination checker does not recognise as such.
>> > The type checker would trust this just like a postulate;
>> > this of course means that if the function in question does in fact
>> > not terminate, the type checker will loop.
>> > Just like with postulates, *.agdai files should then also be generated.
>> > Theoretically, the definition could be considered as given via
>> > Induction.* with postulates for the relevant wellfoundedness properties.
>> > (``safe'' mode should of course reject it.)
>>
>> As Andreas said: NO_TERMINATION_CHECK might be what you are asking
>> for.  I just want to point out though (for clarity of discussion) that
>> your comparison with postulates might be a bit misleading. The point
>> is that adding a postulate to Agda will never make the type-checker
>> loop, even if you use a postulate of False in the termination proof of
>> another function (say "f") through Induction.*.  Instead, the
>> typechecker will block on the application of the postulate and the
>> function "f" will not reduce. The NO_TERMINATION_CHECK approach does
>> have the potential to make the type-checker loop. On the flip side:
>> postulates may make you lose canonicity, while the
>> NO_TERMINATION_CHECK approach doesn't if you only use it for functions
>> that do actually terminate.
>>
>> For a more concrete explanation, consider the following:
>>
>>   open import Induction.Nat
>>
>>   postulate x<x : forall {x : Nat} -> x < x
>>
>>   f : (n : Nat) -> Something
>>   f = <-rec go
>>     where go : (n : Nat) -> (indHyp : k -> k < n -> Something) -> Something
>>               go n indHyp = indHyp n x<x
>>
>> The point is that normalising "f 3" will not make the type-checker
>> loop.  Instead, it will reduce to something like "go 3 (... (x < x))"
>> which will block because x<x doesn't reduce.
>
> I was thinking of postulating not the relationship proofs (here x<x),
> but rather the well-foundednes proof of (here) _<_ which is part of
> (here) <-rec. I don't have time to try this right now;
> essentially we'd have (for a non-terminating example):
>
> g : (n : Nat) -> Something
> g = >-rec go
>   where
>     go n indHyp = indHyp (n+1) x+1>x
>
> where >-rec contains a postulated proof of the well-foundedness of _>_,
> while x+1>x is a good proof.
>
>
> Wolfram
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda