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

[Wolfram Kahl]

On Tue, Jul 15, 2014 at 12:44:20AM +0200, Harley D. Eades III wrote:
> On Jul 14, 2014, at 11:54 AM, Wolfram Kahl <kahl at cas.mcmaster.ca> wrote:
> > 
> > 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.)
> 
> 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.  

Maybe I misunderstand what you are trying to say,
but you can already use the material provided in Induction and Induction.*
of the standard library to incorporate your own termination proofs.

(It would of course be convenient if some automatic mechanism
 converted a recursive definition that fails the termination checker
 into an application of an induction combinator with a hole
 for the well-foundedness proof.
)


Wolfram