Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Does this function terminate


view this post on Zulip Email Gateway (Aug 04 2022 at 10:50):

From: Li Yongjian <lyj238@gmail.com>
Dear experts:

The following function is transformed from a function defined in a
lazy-evaluated function language HAWK.

[image: image.png]
I. change it into Isabelle Form, but can' t prove its termination. I think
Isabelle's evaluation is not lazy, so its termination can't be proved?

function nextSig::"bool signal⇒ nat signal" and
outputSig ::"bool signal ⇒ nat signal" where
next1:"nextSig bS=delay 0 (outputSig bS)" |
output1:"outputSig bS = sel bS (constantInt 0) (inc (nextSig bS)) "
apply pat_completeness
by auto
termination

see the attached file

regards!
image.png
hawk.thy

view this post on Zulip Email Gateway (Aug 05 2022 at 00:30):

From: Wenda Li <wl302@cam.ac.uk>
Dear Yongjian,

In you case, I believe you need a bound function of type “bool signal => nat" such that with each recursion the output of this function decreases.

For example, in HOL-Computational_Algebra.Polynomial the bound function ‘degree’ is needed to show that the polynomial derivative function terminates:

function pderiv :: "('a :: {comm_semiring_1,semiring_no_zero_divisors}) poly ⇒ 'a poly"
where "pderiv (pCons a p) = (if p = 0 then 0 else p + pCons 0 (pderiv p))"
by (auto intro: pCons_cases)
termination pderiv
by (relation "measure degree") simp_all

Hope this helps,
Wenda

view this post on Zulip Email Gateway (Aug 05 2022 at 08:45):

From: Thomas Sewell <tals4@cam.ac.uk>
You're in a fiddly situation here, unfortunately.

You typically begin such a termination proof with the "measure" command. There used to be another way, but apparently the relevant theorems were hidden (?).

If you apply "measure X" after "termination" in your problem, you'll see what needs to be true of your measure. Unfortunately, it's impossible, at the moment.

The first problem is that your signal functions aren't passing arguments to each other that are decreasing in some measure. In this case, you can apply the clumsy fix of eta-expanding all the rules of the function definition:

function nextSig::"bool signal⇒ nat signal" and
outputSig ::"bool signal ⇒ nat signal" where
next1:"nextSig bS x = delay 0 (outputSig bS) x" |
output1:"outputSig bS x = sel bS (constantInt 0) (inc (nextSig bS)) x"
apply pat_completeness
by auto

The value "x" is now being passed through the recursion in a way that it decreases. But, that's a byproduct of the way that the combinators delay, sel and inc work. To provide this information to the function package, you need to add congruence rules that look like this:

lemma inc_cong[fundef_cong]:
"(⋀j. n = j ⟹ f j = f' j) ⟹ n = n' ⟹ inc f n = inc f' n'"
by (simp add: inc_def lift_def)

This shape of congruence is used to allow either the simplifier or the fundef package to know that the parameter passed to "f" in "inc f n" will be the same n. Add the correct collection of congruences, and the goal you'll see after "measure" in termination will start to look provable. In fact, the fun package can pick the measure and prove it all by itself, once it has the right information available.

I attach a partly completed version of your theory.

The above approach is pretty clunky. There has been a lot of work on supporting other styles of termination/fixpoint definition. See, perhaps, Alexander Krauss' PhD at https://www21.in.tum.de/~krauss/ ? Is there a more up-to-date reference? Anyway, it might be possible to sidestep the manual eta-expansion above, especially if the signal type ends up needing more features than just its evolution over time.

Good luck with it,
Thomas.

This recursive function isn't exactly terminating because it's passing an argument that's getting smaller. Rather, it's passing an argument that becomes more precise with each iteration. Unfortunately the function package doesn't do the right thing by default.
image.png
hawk.thy

view this post on Zulip Email Gateway (Aug 05 2022 at 09:22):

From: Lawrence Paulson <lp15@cam.ac.uk>
This looks like a job for co-recursion, not terminating recursion, and I hope that an expert on that topic can provide a precise solution.

Larry Paulson

view this post on Zulip Email Gateway (Aug 07 2022 at 09:52):

From: Andreas Lochbihler <mail@andreas-lochbihler.de>
Dear Li,

as Larry pointed out, this is really something for corecursion. Isabelle's support for
friendly corecursion (http://dx.doi.org/10.1007/978-3-662-54434-1_5) can handle all the
definitions in the theory without trouble. I've attached a commented theory of how this
could look like.

The implementation of the BNF_Corec package has still a few rough edges and limitations,
but it worked out of the box for the examples in your theory. Please let us know if you
run into any trouble and we'll be happy to figure out some workaround when possible.

Hope this helps,
Andreas
hawk.thy


Last updated: Mar 29 2024 at 12:28 UTC