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

[Dominique Devriese]

Wolfram,

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.

On the other hand, if you write the equivalent with NO_TERMINATION_CHECK:

  {-# NO_TERMINATION_CHECK #-}
  f : (n : Nat) -> Something
  f n = f n

Then normalising "f 3" *will* make the type-checker loop.

Regards,
Dominique