Email Gateway (Aug 22 2022 at 14:10): Email Gateway (Aug 22 2022 at 14:10):From: Edward Pierzchalski <e.a.pierzchalski@gmail.com>
Hi, I'm running into issues delegating the "boring"/homomorphic parts of
recursion over a datatype. Consider the following:
datatype t = N nat | A t | B t t
fun boring :: "(t => t) => t => t" where
"boring f (N n) = N n"
| "boring f (A t) = A (f (boring f t))"
| "boring f (B t1 t2) = B (f (boring f t1)) (f (boring f t2))"
function (sequential) interesting :: "nat => t => t" where
"interesting k (N n) = N (n + k)"
| "interesting k (A t) = A (interesting (k + 1) t)"
| "interesting k t = boring (interesting k) t"
by pat_completeness auto
I hope you can convince yourself that interesting should terminate by
size of the second recursive call argument. Unfortunately, since the
recursive call is hidden by boring, the standard relation "measure ..."
technique doesn't work (you end up with a goal like !!k x l r. ((k, x),
(k, B l r)) \in measure ... for arbitrary x, which doesn't look provable).
Does anyone know how to proceed?
Regards,
--Ed
Email Gateway (Aug 22 2022 at 14:10):From: Manuel Eberl <eberlm@in.tum.de>
Unfortunately, it's not that easy.
You pass the "interesting" function to the "boring" function as a
parameter, and the "boring" function applies that function that it is
given to things. In order for this to work, you need to essentially show
that the "interesting" function that you are defining is only called on
values for which it terminates (i.e. that are smaller than the original
argument that it got)
Normally, this is done with a fundef_cong rule, but in this case, I
don't see how that is possible, because the values that "interesting" is
called on by "boring" are "boring f t1" and "boring f t2" – that means
that you are relying on the fact that the "interesting" function does
not increase the size of its argument.
Showing that "interesting" is size-preserving is actually straightforward:
lemma same_size_boring:
assumes "⋀y. size (f y) = size y"
shows "size (boring f x) = size x"
using assms by (induction x) simp_all
lemma size_interesting_aux:
assumes "interesting_dom (k, t)"
shows "size (interesting k t) = size t"
using assms
by (induction rule: interesting.pinduct) (simp_all add:
interesting.psimps same_size_boring)
However, I have no idea how you would then go on and prove termination.
Termination proofs depend on the call graph that is computed for the
recursive definition, and if you don't have a fundef_cong rule for
boring, that call graph – as you discovered yourself – will be too
coarse (i.e. you will not have the information that you need in your
termination proof). However, as I see it, any cong rule for "boring"
would have to be conditional, which is, as far as I am aware, not
possible for fundef_cong rules.
What you are trying to do may therefore very well be outside of what the
function package can do. (although I'm not 100% sure about that – still,
even if it is possible, I would bet it will be ugly)
My advice would be: try to define your functions in a simpler way.
Proofs involving nested recursion tend to get very ugly very quickly,
because the termination of your function depends on the semantics of
your function, and semantic properties are difficult to use without a
full termination proof.
Cheers,
Manuel
Email Gateway (Aug 22 2022 at 14:10):From: Christian Sternagel <c.sternagel@gmail.com>
Dear Ed,
as Manuel indicated, you'll likely have to define your function in
another way.
One way would be to use mutual recursion:
function (sequential)
interesting :: "nat ⇒ t ⇒ t" and
boring :: "nat ⇒ t ⇒ t"
where
"interesting k (N n) = N (n + k)"
| "interesting k (A t) = A (interesting (k + 1) t)"
| "interesting k t = boring k t"
| "boring k (N n) = N n"
| "boring k (A t) = A (interesting k (boring k t))"
| "boring k (B t1 t2) = B (interesting k (boring k t1)) (interesting k
(boring k t2))"
by (pat_completeness) auto
where your "boring" is replaced by a variant that only takes "k" as
parameter. Then we can prove that both functions are size-preserving, as
already suggested by Manuel.
lemma [termination_simp]:
shows "interesting_boring_dom (Inl (k, t)) ⟹ size (interesting k t) =
size t"
and "interesting_boring_dom (Inr (k, t)) ⟹ size (boring k t) = size t"
by (induct k t and k t rule: interesting_boring.pinduct)
(simp_all add: interesting.psimps boring.psimps)
Which incidentally suffices for termination:
termination by (lexicographic_order)
It remains to show that this actually corresponds to your original
function specification. Here, I use "boring'" for your "boring".
fun boring' :: "(t ⇒ t) ⇒ t ⇒ t" where
"boring' f (N n) = N n"
| "boring' f (A t) = A (f (boring' f t))"
| "boring' f (B t1 t2) = B (f (boring' f t1)) (f (boring' f t2))"
Your definition of "interesting" (modulo "case" on the right vs.
pattern-matching on the left) can be obtained by mutual induction:
lemma
shows "interesting k s =
(case s of
N n ⇒ N (n + k)
| A t ⇒ A (interesting (k + 1) t)
| t ⇒ boring' (interesting k) t)"
and "boring k s = boring' (interesting k) s"
by (induct k s and k s rule: interesting_boring.induct) auto
cheers
chris
PS: For those who care and know what I'm talking about: termination of
the TRS corresponding to "interesting" and "boring" is trivial for
modern termination tools. Maybe a reason to revive IsaFoR/TermFun? ;)
Email Gateway (Aug 22 2022 at 14:10):From: Thomas.Sewell@data61.csiro.au
With some extra thought, you can make these definitions work by
explicitly forcing "boring" to be size-preserving.
datatype t = N nat | A t | B t t
definition
"size_constrain f v = (if size (f v) = size v then f v else v)"
lemma size_size_constrain[simp]:
"size (size_constrain f v) = size v"
by (simp add: size_constrain_def)
fun boring :: "(t => t) => t => t" where
"boring f (N n) = N n"
| "boring f (A t) = A (size_constrain f (boring f t))"
| "boring f (B t1 t2) = B (size_constrain f (boring f t1))
(size_constrain f (boring f t2))"
lemma boring_size[simp]:
"size (boring f t) = size t"
by (induct t, simp_all)
lemma boring_fundef_cong[fundef_cong]:
"⟦ ⋀t'. size t' < size t ⟹ f t' = f' t' ⟧
⟹ boring f t = boring f' t"
by (induct t, simp_all add: size_constrain_def)
fun interesting :: "nat => t => t" where
"interesting k (N n) = N (n + k)"
| "interesting k (A t) = A (interesting (k + 1) t)"
| "interesting k t = boring (interesting k) t"
lemma interesting_size[simp]:
"size (interesting k t) = size t"
by (induct t arbitrary: k , simp_all)
lemma interesting_size_constrain[simp]:
"size_constrain (interesting k) = interesting k"
by (simp add: size_constrain_def fun_eq_iff)
That's a bit of a pain but it works with standard tools and gets you
roughly what you want.
It might also be possible to relax the size constraint slightly to allow
size reduction, for instance.
Cheers,
Thomas.
Last updated: Apr 18 2024 at 16:19 UTC