Re: [isabelle] Proving termination of a recursive function



Just to document it for the mailing list: this question was also asked in the #isabelle IRC channel on Freenode yesterday, and it received two answers, one by someone called âint-eâ and one by me:


int-e's answer was:

termination
proof -
  let ?R = "{(y,POR runnable todo don) | runnable todo don y s. s â range don â y â set_option s }"
  {
    fix P x
    assume *: "âx. (ây. (y, x) â ?R â P y) â P x"
    have "P x"
      by (induct x rule: POR.induct) (auto intro: *)
  }
  then have "wf ?R" by (auto simp: wf_def)
  then show ?thesis
    by (relation ?R) (auto simp: ran_def image_def, metis)
qed

It's really stupid because it's a bona fide inductive definition on the data type definition; morally it *is* primitive recursive. but the underlying well-founded relation on POR is not readily available; that's what I'm defining as ?R in the proof (or so I believe, I'd be happy to be shown wrong)



My answer was:

definition por_well_formed where "por_well_formed = rec_POR (Îrunnable todo done. todo |â| runnable â dom done â fset runnable â fset todo â dom done = {} â (âp â ran done. snd p))" lemma por_well_formed_simps: "por_well_formed (POR runnable todo done) â ( todo |â| runnable â dom done â fset runnable â fset todo â dom done = {}) â (â p â ran done. por_well_formed p)" unfolding por_well_formed_def by (simp add: dom_map_option ran_map_option o_def)

int-e is correct, this is a primitively-recursive function, so the easiest way to define it is to define it as one.
The problem is that "primrec" is apparently not smart enough to figure out that your definition is primitively-recursive I just did it by hand and proved the "simp" rule separately afterwards

Two more remarks:

1. your datatype is essentially an infinitely-branching tree, which means you can have potentially unbounded traversal paths in it, so there simply is no sensible "size" function for them, which makes proving termination more painful (although in this case, it can be done with relatively little effort, as shown by int-e)

2. your function implicitly enforces the domain of "done" to be finite, so you could actually define a "size" function for this case, and it would be something "size (POR _ _ done) = 1 + Max (size ` ran done)". But you'd also have to add conj_cong as a fundef_cong rule or rewrite your definition with if _ then _ else in order to be able to use the fact that "done" has finite domain

On 17/11/15 20:52, Michael Walker wrote:
Hi,

I've been getting into Isabelle recently, and I have a problem with
function termination: I have a recursive data type, and a function
checking some property of it, but I'm not sure how to approach the
termination proof:

~~~~
theory MinimalExample
imports Main "~~/src/HOL/Library/FSet" Map
begin

datatype ThreadId = UserThread nat

datatype POR = POR "ThreadId fset" "ThreadId fset" "ThreadId â POR"

function
   por_well_formed :: "POR â bool"
where
   "por_well_formed por â (case por of (POR runnable todo done) â
    ( todo |â| runnable
    â dom done â fset runnable
    â fset todo â dom done = {})
    â (â p â ran done. por_well_formed p))"
by auto
termination sorry

end
~~~~

My informal termination argument goes like this: because POR is data,
not codata, there can't be an infinite sequence POR1 -> POR2 -> POR3
-> ... (following the links in the map). This means that the recursive
case in por_well_formed will terminate. However, I'm not sure how to
formalise that.

Any suggestions for this in particular, or termination proofs in
general, would be greatly appreciated.




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