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

[Dan Doel]

On Wednesday 19 November 2008 5:56:12 am Edsko de Vries wrote:
> Hi all,
>
> I was experimenting with Vladimir's suggestion (based on Capretta's
> equivalence relation), when a collegue (Wendy Verbruggen) realized
> that the fixed point definition I had been using is wrong (Dan, I
> think this is the definition you're using too, right?)
>
> CoFixpoint lfpAux (A B:Set)
>      (k:A -> Delay B)
>      (f:(A -> Delay B) -> (A -> Delay B))
>      (a:A) : Delay B :=
>    match f k a with
>
>    | Now a => Now a
>    | Later d' => Later (lfpAux (f k) f a)
>
>    end.
>
> Definition lfp (A B:Set)
>      (f:(A -> Delay B) -> (A -> Delay B))
>      (a:A) : Delay B :=
>    lfpAux (fun x => bottom) f a.
>
> At least, we *think* this is wrong: it is missing some notion of
> searching for the least fixed point (called 'omegarace' in
> http://www.informatik.uni-bonn.de/~ralf/WG2.8/22/slides/tarmo.pdf or
> 'parallel_search' in Caprettas paper). As a result, in some of our
> experiments computations were diverging that shouldn't be.
> Unfortunately, correcting this makes the unfolding of factorial much
> more complicated still and and we're now even further removed from
> proving anything about fac :/

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

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).

Anyhow, I guess the proofs I did were too easy. Oh well. :)

-- Dan