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



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?


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 ;).

Thanks again for the help!

Regards,
Scott





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