Email Gateway (Aug 22 2022 at 15:30): Email Gateway (Aug 22 2022 at 15:30):From: Thomas.Sewell@data61.csiro.au
Hello isabelle-users.
I've been thinking about partially-terminating recursive functions a
little over the
last day or two. Here's a silly example:
function
escalate :: "(nat => nat) => nat => nat => nat"
where
"escalate m lim n = (if n >= lim then n else escalate m lim (m n))"
by pat_completeness auto
Obviously this function doesn't always terminate, but perhaps it would if
we first assumed something about the function m, for instance that it
increases
n, or that it increases n on a key subset of the naturals.
I thought I recalled that the function package could be used for this.
If I inspect
the theorems exported by the "function" command above (before any matching
"termination), I see partial simp and induct rules named escalate.psimps
and escalate.pinduct. These are sufficient to prove what we need about the
escalate function, but only within its terminating domain "escalate_dom".
Here's the problem. We have no rules whatsoever with which to prove anything
about "escalate_dom". Everything is hidden. Even the rule
escalate.termination,
which I think I'm meant to use next, is hidden.
Also, escalate.termination is only useful for proving total termination.
To prove that
the function terminates on some limited domain will require some other
strategy.
In short, my recollection that the function package could easily be used for
partially terminating functions was totally wrong. Is there somewhere else
I'm forgetting to look?
In the attached theory, I use some ML-level tricks to "see" the hidden
rules, to see
through the abbreviation "escalate_dom", and to find the theorem
escalate_rel.cases
which I really need.
I also prove a variant of the acc/wf connection from Wellformed which
allows us to
prove that some subset of elements is within the accessible part, using
the regular
wf machinery. This is really needed if we're going to make much progress
here.
Finally I apply that to escalate, and prove a silly case about even numbers.
OK. Is anyone maintaining this? Should the theorem escalate.termination
really
be hidden? Would it be useful to other users to have the function package
expose something else, maybe a ptermination rule analagous to the
termination rule, with which to prove anything about partially terminating
functions?
It seems inconsistent to me that the package exposes these psimp rules but
no way to use them.
Anyway, hope this might be of help to someone.
Cheers,
Thomas.
Escalate.thy
Email Gateway (Aug 22 2022 at 15:30):From: Lars Hupel <hupel@in.tum.de>
Dear Thomas,
Here's the problem. We have no rules whatsoever with which to prove anything
about "escalate_dom". Everything is hidden. Even the rule
escalate.termination,
which I think I'm meant to use next, is hidden.
you might need to do some tricks to be able to use the theorems, but
probably not that low level.
The function package exposes the ML function "Function.get_info" to
obtain a bunch of results about a function. "R" is the relation you're
interested in, and "Inductive.the_inductive" will give you info about
that. The resulting theorems can be used in an ML tactic.
OK. Is anyone maintaining this? Should the theorem escalate.termination
really
be hidden? Would it be useful to other users to have the function package
expose something else, maybe a ptermination rule analagous to the
termination rule, with which to prove anything about partially terminating
functions?
Nobody is maintaining this. But it's probably just a matter of removing
some "concealed"s in the code.
Cheers
Lars
Email Gateway (Aug 22 2022 at 15:30):From: Dominic Mulligan via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
Hi Thomas,
It sounds like you want to use (domintros). For example:
function (domintros) foo :: "nat ⇒ nat" where
"foo x = x"
by pat_completeness auto
thm foo.domintros
Also, see Section 8.2 of the Function package documentation supplied
with Isabelle.
Thanks,
Dominic
Email Gateway (Aug 22 2022 at 15:30):From: Manuel Eberl <eberlm@in.tum.de>
I agree with Dominic that domintros is probably what you want to use and
that the function package documentation is a good way to start.
Here's how you could use domintros in your particular case:
lemma bounded_nat_gt_induct [case_names base gt]:
"(⋀n::nat. n ≥ m ⟹ P n) ⟹ (⋀n. n < m ⟹ (⋀n'. n' > n ⟹ P n') ⟹ P n) ⟹ P n"
by induction_schema (force, rule wf_measure[of "λn. m - n"], auto)
lemma
assumes "⋀x. x < lim ⟹ m x > x"
shows "escalate_dom (m, lim, n)"
proof (induction n rule: bounded_nat_gt_induct [of lim])
case (base n)
thus ?case by (auto intro: escalate.domintros)
next
case (gt n)
from gt.hyps have "escalate_dom (m, lim, m n)" by (intro gt.IH assms) auto
thus ?case by (rule escalate.domintros)
qed
There's also the "partial_function" command, which does not care about
termination at all. It has two modes, but the most useful one is
probably that where the function returns an "'a option" and
non-termination returns a "None".
Manuel
Email Gateway (Aug 22 2022 at 15:30):From: Peter Lammich <lammich@in.tum.de>
There's also the "partial_function" command, which does not care
about
termination at all. It has two modes, but the most useful one is
probably that where the function returns an "'a option" and
non-termination returns a "None".
Afterwards, one can prove that the function never returns None
(possibly with some preconditions), and use "the" to get the
corresponding plain function.
Email Gateway (Aug 22 2022 at 15:31):From: Thomas.Sewell@data61.csiro.au
Thanks for all the replies. Thanks indeed for pointing out Section 8.2
of the long function package document, which indeed seems to suggest
that some of the hidden theorems I've found are canonical for use,
curiously not including f.termination.
Yes, there are workarounds. I can use partial_function, or tailrec mode,
or declare a type of well-behaved inputs, and derive (eventually) the
function
I want. This seems like overkill, however, since the function package
defines
function exactly as I want by default, it just surprises me by
"hiding" the rules
I needed to proceed.
Yes, I could have inspected the package's ML interface. In principle,
anyway.
I'm embarrassed that I didn't read the manual, but I'm not embarrassed
that I didn't look at the ML level. For other Isabelle packages I've
found the
ML info available to be low-level, verbose, and prone to change with future
revisions.
The "domintros" mode is probably what I was looking for. Now the rules
provided
do actually fully characterise the function. Phew. Honestly, the form of
these rules
is annoying though. They really require me to phrase an inductive proof,
whereas
it feels easier to just supply a well-founded relation and a subdomain
as I did in the
example.
Thanks for the replies everyone.
Cheers,
Thomas.
Last updated: Apr 27 2024 at 04:17 UTC