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

[Wolfram Kahl]

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