Re: [isabelle] Termination Proof ``fun'' ;)



Dear Scott,

Scott West schrieb:
Hello Alex,

Exactly! You will need to define a set "L" which contains all the nodes that can be "seen". Instead of "measures" I would prefer the use of "psubset" here.


I'll look at psubset, thanks!


But this is not the only problem you have here. Moreover the use of "foldr" complicates the proof. When you start your termination proof, you will notice, that there is no call of "foldr" anymore. Here the "Higher Order Recursion" (http://isabelle.in.tum.de/dist/Isabelle/doc/functions.pdf, chapter 9) comes into play. "foldr" is eliminated using the congruence rule 'foldr_cong' (from List.thy) I think. But this rule 'abstracts' over the second argument (of f), so that you are not able state anything about it (and you will need it to proof termination). Therefore you have probably first to find the right congruence rule for 'foldr' that somehow preserves the information, that the second argument of f is always a subset of "L".


I read the functions.pdf that you pointed me to, however I still dont' feel as if I know how the congruence mechanism works in practice. How does it `abstract' over the second argument of `f' ?

If I do need to reformulate the foldr_cong rule to fit my needs, are there any good examples of how these rules are applied during the proof, so I can see what's going wrong?
Well, I am not really sure if there are any. But I've created a small example, that I think addresses your problem. Instead of using foldr explicitly and to avoid the problems arise with congruence rules, I've just used mutual recursion (http://isabelle.in.tum.de/dist/Isabelle/doc/functions.pdf, Chapter 5) to achieve the same behavior. In my example (see Test.thy) the function 'f' is similar to your 'all_children' function, the (abstract) function 'g' is somewhat similar to your 'children' function. After the function definition is established and the completeness is proofed, the termination proof is considered, which relies on the fact, that there is an function called 'lim' which computes an upper bound for 'f' (and therefore for its second argument). So far, 'lim' is not really defined in my example (that's up to you), but requires some properties to be true (for example finiteness, etc.) After that a special partial termination property (called 'subset_prop') for the function 'f' and its mutual recursive counterpart 'foldr_f' is proofed, since it is required in the termination proof. This property is important and I don't think you can get a similar property when you use 'foldr' directly (but I've not verified that!) At the end the termination proof is established using a special termination ordering (called 'my_term_ord'), which is a lexicographical combination of 'finite_psubset' and the 'less_than' relation. The latter is needed since in my mutual recursive version the termination of the foldr replacement have to also to be proofed.

Maybe it is a better idea to eliminate the use of foldr (if possible) completely.


I do now have a version that I created without foldr that I can prove termination. However eventually I will be doing things where foldr becomes important (modeling imperative code, so the accumulated parameter will be the state). So I guess I'm going down a more difficult road ;).
Just try using the mutual recursive version that I've suggested in the example. After finishing the termination it is probably possible to proof, that the mutual recursive (helphing) funciton 'foldr_f' is in fact (in some sense) equal to the ordinary 'foldr' function, so that it can be replaced.

Thanks again for the help!
No problem, so far!


Regards,
Alex
theory Test
imports Main
begin

consts g :: "nat \<Rightarrow> nat list"

function f :: "nat \<Rightarrow> nat list \<Rightarrow> nat list"
     and foldr_f :: "[nat list, nat list] \<Rightarrow> nat list"
where
  "f k ks = (if k \<in> set ks then ks else foldr_f (g k) (k#ks))"
| "foldr_f [] a = a"
| "foldr_f (x#xs) a = f x (foldr_f xs a)"
by pat_completeness auto

consts lim :: "[nat, nat list] \<Rightarrow> nat set"
       --"lim takes the arguments of f and calculates all reachable nodes"

lemma lim_finite: "finite (lim k ks)"
sorry

lemma lim_eq: "lim k (k#ks) = lim k ks"
sorry

lemma lim_subset: "set ks \<subseteq> lim k ks" sorry

lemma lim_concat: "lim k (xs at ys) = lim k xs \<union> lim k ys" sorry

lemma lim_append: "lim k (x#xs) = lim k [x] \<union> lim k xs" using lim_concat[of k "[x]" xs] by auto

lemma lim_mem: "k\<in>set ks \<Longrightarrow> lim l (k#ks) = lim l ks" sorry


lemma subset_prop':
      "f_foldr_f_dom (Inl (k, a)) \<Longrightarrow> set a \<subseteq> set (f k a) \<and> lim l (f k a) = lim l (k#a)"
      "f_foldr_f_dom (Inr (ks, a)) \<Longrightarrow> set a \<subseteq> set (foldr_f ks a) \<and> lim l (foldr_f ks a) = lim l (ks at a)"
proof (induct a and a rule: f_foldr_f.pinduct)
  case goal1 thus ?case
  proof(cases "k\<in>set ks")
    case goal1 thus ?case using lim_mem by simp
  next
    case goal2
      hence "lim l (g k @ k # ks) = lim l (k#ks)" sorry
      --"This should be true, since lim should contain all 'child nodes' that are calculated by g."
      --"Therefore the right hand side should contain 'g k' implicitly."
      thus ?case using goal2 by simp
  qed
next
  case goal2 thus ?case by auto
next
  case (goal3 k' )
    have "lim l (k' # xs @ a) = lim l [k'] \<union> lim l (xs @ a)" using lim_append by blast
    moreover with goal3 have "\<dots> = lim l [k'] \<union> lim l (foldr_f xs a)" by auto
    moreover have "\<dots> = lim l (k' # foldr_f xs a)" using lim_append by blast
    moreover have "\<dots> = lim l (f k' (foldr_f xs a))" using goal3 by auto
    ultimately have "lim l (f k' (foldr_f xs a)) = lim l (k' # xs @ a)" by simp
    thus ?case using goal3 by auto
qed


lemma subset_prop: 
  assumes "f_foldr_f_dom (Inr (ks, a))"
    shows "set a \<subseteq> set (foldr_f ks a)"
      and "lim k (foldr_f ks a) = lim k (ks at a)"
using prems subset_prop' by auto


abbreviation
  "my_term_ord \<equiv>
     inv_image (finite_psubset <*lex*> less_than) (\<lambda>v. (case v of (Inr (ys, ks)) \<Rightarrow> (lim (hd ks) (ks at ys) - set ks, size ys)
                                                                | (Inl (k, ks)) \<Rightarrow> (lim k ks - set ks, 0) ))"


lemma in_finite_psubset[simp]:
  "((A, B) \<in> finite_psubset) = (A \<subset> B \<and> finite B)"
unfolding finite_psubset_def by simp


termination
proof (relation "my_term_ord")
  case goal1 thus ?case by (auto intro: wf_finite_psubset)
next
  case (goal2 k ks)
    hence "lim k (k#ks) - insert k (set ks) \<subset> lim k ks - set ks"
    unfolding lim_eq sorry --"easy to proof"
    moreover have "finite (lim k ks - set ks)" using lim_finite by auto
    moreover have "lim k (k # ks) = lim k (k # ks @ g k)" sorry --"see above"
    ultimately show ?case by simp
next
  case (goal3 k ks a) thus ?case apply simp sorry --"easy to proof"
next
  case (goal4 k ks a)
    hence "set a \<subseteq> set (foldr_f ks a)"
      and "lim k (foldr_f ks a) = lim k (ks at a)" using subset_prop by auto
    moreover have "lim (hd a) (a @ k # ks) = lim k (ks at a)" sorry -- "easy to proof"
    ultimately show ?case apply simp sorry -- "again easy, use the premise"
qed


end


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