Re: [isabelle] Proving termination of a recursive function



Primec supports a syntactic fragment where for nested recursion (here nesting through the function type and option) one has to use the corresponding map functions. For the function type this is âoâ (which is allowed to be unfolded as well, see below) and for option this is map_option. So tuning the functionâs specification a bit makes it accepted by primrec:

primrec
 por_well_formed :: "POR â bool"
where
 "por_well_formed (POR runnable todo done) =
  ( todo |â| runnable
  â dom done â fset runnable
  â fset todo â dom done = {}
  â (â p. map_option por_well_formed (done p) â Some False))â

Then one can derive the original equation by (induct por) (auto simp: ran_def).

Dmitriy


> On 18 Nov 2015, at 13:29, Manuel Eberl <eberlm at in.tum.de> wrote:
> 
> 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.