POSTUlATE_TERMINATION --- Was: Re: [Agda] termination by
contradiction
Andreas Abel
andreas.abel at ifi.lmu.de
Tue Jul 15 10:50:50 CEST 2014
On 15.07.2014 00:44, Harley D. Eades III wrote:
> This is a nice idea. I have always wanted a means to be my own termination
> checker. It would be extremely nice if we could have a pragma like
>
> EXTERNAL_TERM_PROOF
>
> that takes an argument which is the termination proof. Then the type
> checker could consider the function terminating with a proof that this is true.
>
> Sometimes it is easier to prove termination in such a way the termination
> checker cannot determine.
Sound nice, yes, but I'd like to see this on (to be) published paper
first. Especially a proof that the existence of such an external
termination proof guarantees termination of reduction on *open* terms.
Cheers,
Andreas
--
Andreas Abel <>< Du bist der geliebte Mensch.
Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden
andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/
More information about the Agda
mailing list