Re: [isabelle] Common monadic programming idioms and termination



The problem is that you have a recursive call in an argument of the âbindâ function, and the function package has no idea what kind of parameter this call will get.

For instance, the âbindâ function could simply double the list it gets as the first input and call the function it gets as second input on it â then your function would never terminate.

So, what you need to do is you need to tell the function package a little bit about what kinds of inputs the âbindâ function will give to its function parameter. You can do that with a congruence rule:


lemma error_bind_cong [fundef_cong]:
  "(map_error f x = map_error f' x') â error_bind x f = error_bind x' f'"
  by (cases x; cases x') simp_all

This essentially implies that bind only calls the function you give it with a value contained in the error object you give it. Once you have proven this lemma and declared it as [fundef_cong], your proof obligation in the termination proof will look a lot saner.

Add two more simp lemmasâ

lemma set_error_fail [simp]: "set_error (error_fail m) = {}"
  by (simp add: error_fail_def)

lemma set_error_return [simp]: "set_error (error_return s) = {s}"
  by (simp add: error_return_def)

âand everything works automagically.


Cheers,

Manuel


the function package does not know anything about your âbindâ function.

On 23/10/15 17:24, Dominic Mulligan via Cl-isabelle-users wrote:
Hi all,

I have a problem with a development that I am working on (in Isabelle
2015).  A slimmed down and simplified version of the problematic code
has been attached in a dedicated theory file to this e-mail with the
problem annotated with an (* XXX *) comment.

The problem arises when trying to prove termination of recursive
functions that follow a fairly natural monadic programming style,
namely recursively calling your function on a decreasing argument that
is produced by earlier monadic code, hence lambda-bound following a
bind.  Here, the termination machinery seems to generate proof
obligations that are not solveable, demanding one prove that an
arbitrary list is shorter (according to the measure) than a non-empty
list, like so:

âxs xa. xs â [] â length xa < length xs

Interestingly, HOL4's termination machinery also seems to behave
similarly, and with the help of Anthony Fox the issue has been
reported to Konrad Slind.

Does anybody have any suggestions on how to proceed other than
completely rewriting all of my monadic code?  The problematic code is
automatically generated, and comes from a rather large model, so I'd
rather not have to rewrite everything.

Many thanks for any help proffered,
Dominic





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.