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

[Edsko de Vries]

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 :/

Edsko