Re: [isabelle] Termination Proof ``fun'' ;)
Scott West schrieb:
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.
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"
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?
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.
Maybe it is a better idea to eliminate the use of foldr (if possible)
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 ;).
Thanks again for the help!
No problem, so far!
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"
"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)"
lemma lim_eq: "lim k (k#ks) = lim k ks"
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
"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
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
case goal2 thus ?case by auto
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
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
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) ))"
"((A, B) \<in> finite_psubset) = (A \<subset> B \<and> finite B)"
unfolding finite_psubset_def by simp
proof (relation "my_term_ord")
case goal1 thus ?case by (auto intro: wf_finite_psubset)
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
case (goal3 k ks a) thus ?case apply simp sorry --"easy to proof"
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"
This archive was generated by a fusion of
Pipermail (Mailman edition) and