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

*To*: Alexander Schimpf <info at hitstec.de>
*Subject*: Re: [isabelle] Termination Proof ``fun'' ;)
*From*: Scott West <scott.west at inf.ethz.ch>
*Date*: Mon, 04 May 2009 11:09:41 +0200
*Cc*: cl-isabelle-users at lists.cam.ac.uk
*In-reply-to*: <49F6EC46.4030909@hitstec.de>
*References*: <49F5AA3F.5040004@inf.ethz.ch> <49F6C9C6.2020201@loria.fr> <49F6EC46.4030909@hitstec.de>
*User-agent*: Thunderbird 2.0.0.21 (X11/20090409)

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.*