[Agda] Termination proof in partiality monad

[Luke Palmer]

On Mon, Nov 17, 2008 at 6:47 AM, Edsko de Vries <devriese at cs.tcd.ie> wrote:
> PS. I asked this before on the Coq mailing list but received no replies;
> perhaps my previous email was too low-level. Hence this repost.

FWIW I did see your mail and experimented with your code for quite a
while, without making very much progress.  The problem I kept running
into is that I could not re-fold the definition of lfp (I think... I'm
doing this from memory) because there was an extra f in the
definition.  I suspect that a lemma to the effect of:

   lfp f = f (lfp f)

Would do the trick.  However that lemma cannot be stated the way you
formalized things.  I tried changing the terminates inductive to
terminatesWith, which encodes the value that it terminates with as
well, but that ended up being a pain and I just gave up.  I think the
above lemma is the key.

If you resolve this, I'd love to see it.

You might also be interested in Bertot and Komendantsky's recent
paper: http://hal.inria.fr/docs/00/30/57/08/PDF/ppdp19-bertot.pdf

Very interesting stuff, but it is quite complicated.

Luke