[Agda] Termination proof in partiality monad

[Shin-Cheng Mu]

On Nov 17, 2008, at 1:47 PM, Edsko de Vries wrote:
> Now I have a simple question: given an inductive characterization of
> termination, how would one prove that fac terminates? I have tried
> various approaches (in Coq) but am making no progress at all.


I hope my previous experiments are relevant:

   http://www.iis.sinica.edu.tw/~scm/2008/general-recursion-using-coindutive-monad/
   http://www.iis.sinica.edu.tw/~scm/2008/general-recursion-using-coinductive-monad-got-right/

These are basically Adam Megacz's work (in Coq) ported to Agda:

   http://portal.acm.org/citation.cfm?id=1292597.1292601

Megacz's monad, on the other hand, is an extension of Venanzio
Capretta's approach, which is probably closer to Dan Doel's
monad.

It should be even easier to prove the termination of
factorial, since we only need an induction (rather than
strong induction) to prove that fact n converges for
all n.

sincerely,
Shin