Stream: General

Topic: ✔ Partial termination proofs

Johannes Neubrand (Mar 17 2022 at 01:26):

I'm trying to prove termination of a partial function. I've read functions.pdf, but I can't figure out a nice way to do exactly what I'm looking for. Ideally, I'd like to be able to provide an “expected” domain to some tactic, and then be required to prove that

• recursive calls stay within that expected domain and
• show that some provided measure decreases on each recursive call, as with the relation method.

Background info: The function in my use case is a tail-recursive variant of Tree.subtrees that returns a 'a tree list, and which has been compiled (for lack of a better word) to use nat as an argument & return type. The termination of the non-encoded version can't be shown by fun, but there's a somewhat simple measure that works with relation. Because of this, my gut feeling is that I should use relation to prove termination of the encoded variant. However, when arguments that don't represent valid 'a tree or 'a tree list values under the encoding are passed in, the function might not actually terminate.

function even_to_zero :: "nat ⇒ nat" where
  "even_to_zero 0 = 0"
| "even_to_zero (Suc n) = (case n of (Suc n') ⇒ even_to_zero n' | 0 ⇒ even_to_zero (Suc 0))"
  using not0_implies_Suc apply blast
  by simp_all

lemma even_to_zero_all_dom: "All even_to_zero_dom"
  apply (relation "(λx. x) <*mlex*> {}")
proof -
  show "wf ((λx. x) <*mlex*> {})" by (simp add: wf_mlex)
next
  show "⋀n. n = 0 ⟹ (Suc 0, Suc n) ∈ (λx. x) <*mlex*> {}" sorry
next
  show "⋀n n'. n = Suc n' ⟹ (n', Suc n) ∈ (λx. x) <*mlex*> {}" sorry
qed

inductive_set even :: "nat set" where
  "0 ∈ even"
| "n ∈ even ⟹ Suc (Suc n) ∈ even"

lemma even_to_zero_even_dom: "x ∈ even ⟹ even_to_zero_dom x"
  apply (relation "(λx. x) <*mlex*> {}")  (* changeme *)
proof -
  show "wf ((λx. x) <*mlex*> {})" by (simp add: wf_mlex)
next
  show "⋀n. Suc n ∈ even ⟹ n = 0 ⟹ (Suc 0, Suc n) ∈ (λx. x) <*mlex*> {} ∧ Suc 0 ∈ even"
    by (auto simp add: mlex_iff elim: even.cases)
next
  show "⋀n n'. Suc n ∈ even ⟹ n = Suc n' ⟹ (n', Suc n) ∈ (λx. x) <*mlex*> {} ∧ n' ∈ even"
    by (auto simp add: mlex_iff elim: even.cases)
qed

Does anyone here have pointers for next steps? Am I missing something obvious? I've tried staring at the definition of relation itself, but that just made my eyes glaze over :)

Christoph Madlener (Mar 17 2022 at 09:48):

One way to deal with "partial" functions I've seen and used myself is to use conditional equations. I'm not going to refer to your given example, since you could just split your patterins into Suc 0 and Suc (Suc n) to achieve the same effect. Instead I'll try to give you hints for your actual use-case:
I imagine you have some kind of (inductive) definition of which naturals encode a tree.

definition is_tree :: "nat ⇒ bool" where
  "is_tree n ≡ True"

You can then use that predicate to "restrict" your function to your desired domain.

function subtrees' :: "nat ⇒ nat" where
  "subtrees' n = undefined" if "is_tree n" ― ‹definition for wellformed input›
| "subtrees' n = undefined" if "¬is_tree n" ― ‹some dummy value for inputs outside your domain›
  by auto

You can then (hopefully) proceed with your termination proof using relation again (depending on how your actual definition of subtrees' looks). The conditional equations should then give you your required assumptions in the specific cases.

termination subtrees'
  apply (relation "(λx. x) <*mlex*> {}")
  ...

Mohammad Abdulaziz (Mar 17 2022 at 11:43):

Since the function is tail recursive, I propose you use the partial_function command. It is much nicer to deal with than the domain predicate generated by the function package.

Mohammad Abdulaziz (Mar 17 2022 at 11:45):

Take a look at the induction pcpl and other thms it produces, and see if they are usable.

Johannes Neubrand (Mar 17 2022 at 16:37):

Thanks for the replies!

Both the … if "n ∈ …" and partial_function approaches seem to have the drawback that code equations aren't generated by Isabelle. This is really unfortunate — am I missing something obvious here? Found [code]:, that seems to work fine.

The restricted function version certainly expects me to prove things that look much better than before when using relation. I'm not super excited about having to deal with weirder (or more!) simp rules, but it might be manageable. Regardless, I tried out Mohammad's suggestion first since I'm trying to avoid changing the generated code :)

partial_function's induction scheme certainly doesn't look fun. However, I managed to avoid it completely for a correctness lemma for the generated function, using the original (non-partial and non-encoded) function's induction scheme instead. I had to add an additional conclusion, namely that the generated function's result is a valid encoding—this is needed as an IH.

If I understand this correctly, then, is proving an equation like subtreest' abc = encode (subtreest (decode (abc))) (simplified for sake the of this question) sufficient to convince isabelle that subtreest' terminates on input abc? I'm not sure how much that HOL equality actually means—undefined still makes me nervous :) I did find Manuel's post on stackoverflow here as an explanation of undefined in general, but this still feels wrong as an approach to proving function termination.

Mohammad Abdulaziz (Mar 17 2022 at 18:01):

No, partial_function, by definition, gives you a function that does not necessarily terminate on all inputs. This means that the correctness theorem you prove is only for the inputs on which it terminates. Hence it is called partial correctness. That thm should have the assumption characterising the domain on which it termiantes, however.

Mohammad Abdulaziz (Mar 17 2022 at 18:02):

Also, your approach of using the original function's IH is the right one, at least in my experience of using partial_function.

Johannes Neubrand (Mar 17 2022 at 18:06):

This means that the correctness theorem you prove is only for the inputs on which it terminates.

I understand this, and in my case, the argument domain is implicitly restricted by the encode functions wrapped around subtrees' arguments in the lemma statement. I guess what I'm wondering is whether the partial correctness proof is “all I need” to prove partial termination. Maybe this stems from a misunderstanding on my side of the definition of termination in Isabelle.

Mohammad Abdulaziz (Mar 17 2022 at 18:10):

Yes, that is all you need. The proof of termination is inherent in the induction principle coming from the original function.

Manuel Eberl (Mar 18 2022 at 10:33):

Note that you can also call function with the option (domintros). That gives you a bunch of rules that allow you to reason explicitly about the domain of the function.

Mohammad Abdulaziz (Mar 18 2022 at 13:25):

I think that is what he wants to avoid since he already has a termination proof for a function that does the same recursion as the partial function.

Notification Bot (Mar 18 2022 at 18:04):

Johannes Neubrand has marked this topic as resolved.

Last updated: Dec 21 2024 at 16:20 UTC