[Coq-Club] Re: [Agda] Termination proof in partiality monad

[Edsko de Vries]

> Yes. In fact, the version of fix I'm using is from (I think) the  
> Abstract
> Nonsense for Functional Programmers slides, written by you! :)

Uuuh.. :) In my defense, I did not come up with it :) Still a poor  
excuse for propagating it though. Sorry! :)

> But, fiddling around for the last couple days, it occurred to me  
> that I could
> easily write a factorial that doesn't converge by this method:
>
>    fac-aux : (Nat -> D Nat) -> Nat -> D Nat
>    fac-aux fac 0 = later (return 1)
>    fac-aux fac (suc n) = fac n >>= \n! -> return (suc n * n!)
>
> Now, even when we have enough nested calls to fac-aux, it still  
> returns a
> 'later (now n!)', and the fixed point combinator goes on searching.
>
> However, I suspect, though I have no proof, that the definition is  
> all right
> provided there are no laters introduced by the function of which  
> we're taking
> the fixed point, because the only place for laters to come from in  
> that case is
> from \_ -> bottom. I'm not sure if that characterizes most useful  
> functions or
> not, however (and there's no way to enforce it with the current type).

I had been thinking along the same lines, but unfortunately it's not  
really true. For example, the following function should be entirely  
reasonable:

Definition funny_fac' (rec : nat -> Delay nat) (n : nat) : Delay nat :=
  match n with
  | O => fac 1
  | S m => bindD (rec m) (fun m' => returnD (S m * m'))
  end.

Definition funny_fac (n : nat) : Delay nat :=
  lfp_fac funny_fac' n.

But it diverges.

Edsko