Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Proving termination of a recursive function

Email Gateway (Aug 22 2022 at 11:57):

From: Michael Walker <mike@barrucadu.co.uk>
Hi,

I've been getting into Isabelle recently, and I have a problem with
function termination: I have a recursive data type, and a function
checking some property of it, but I'm not sure how to approach the
termination proof:

theory MinimalExample
imports Main "~~/src/HOL/Library/FSet" Map
begin

datatype ThreadId = UserThread nat

datatype POR = POR "ThreadId fset" "ThreadId fset" "ThreadId ⇀ POR"

function
  por_well_formed :: "POR ⇒ bool"
where
  "por_well_formed por ⟷ (case por of (POR runnable todo done) ⇒
   ( todo |⊆| runnable
   ∧ dom done ⊆ fset runnable
   ∧ fset todo ∩ dom done = {})
   ∧ (∀ p ∈ ran done. por_well_formed p))"
by auto
termination sorry

end

My informal termination argument goes like this: because POR is data,
not codata, there can't be an infinite sequence POR1 -> POR2 -> POR3
-> ... (following the links in the map). This means that the recursive
case in por_well_formed will terminate. However, I'm not sure how to
formalise that.

Any suggestions for this in particular, or termination proofs in
general, would be greatly appreciated.

Email Gateway (Aug 22 2022 at 11:57):

From: Manuel Eberl <eberlm@in.tum.de>
Just to document it for the mailing list: this question was also asked
in the #isabelle IRC channel on Freenode yesterday, and it received two
answers, one by someone called ‘int-e’ and one by me:

int-e's answer was:

termination
proof -
let ?R = "{(y,POR runnable todo don) | runnable todo don y s. s ∈ range don ∧ y ∈ set_option s }"
{
fix P x
assume *: "⋀x. (⋀y. (y, x) ∈ ?R ⟹ P y) ⟹ P x"
have "P x"
by (induct x rule: POR.induct) (auto intro: *)
}
then have "wf ?R" by (auto simp: wf_def)
then show ?thesis
by (relation ?R) (auto simp: ran_def image_def, metis)
qed

It's really stupid because it's a bona fide inductive definition on the data type definition; morally it is primitive recursive. but the underlying well-founded relation on POR is not readily available; that's what I'm defining as ?R in the proof (or so I believe, I'd be happy to be shown wrong)

My answer was:

definition por_well_formed where "por_well_formed = rec_POR (λrunnable
todo done. todo |⊆| runnable ∧ dom done ⊆ fset runnable ∧ fset todo ∩
dom done = {} ∧ (∀p ∈ ran done. snd p))" lemma por_well_formed_simps:
"por_well_formed (POR runnable todo done) ⟷ ( todo |⊆| runnable ∧ dom
done ⊆ fset runnable ∧ fset todo ∩ dom done = {}) ∧ (∀ p ∈ ran done.
por_well_formed p)" unfolding por_well_formed_def by (simp add:
dom_map_option ran_map_option o_def)

int-e is correct, this is a primitively-recursive function, so the easiest way to define it is to define it as one.
The problem is that "primrec" is apparently not smart enough to figure out that your definition is primitively-recursive I just did it by hand and proved the "simp" rule separately afterwards

Two more remarks:

1. your datatype is essentially an infinitely-branching tree, which means you can have potentially unbounded traversal paths in it, so there simply is no sensible "size" function for them, which makes proving termination more painful (although in this case, it can be done with relatively little effort, as shown by int-e)

2. your function implicitly enforces the domain of "done" to be finite, so you could actually define a "size" function for this case, and it would be something "size (POR _ _ done) = 1 + Max (size ` ran done)". But you'd also have to add conj_cong as a fundef_cong rule or rewrite your definition with if _ then _ else in order to be able to use the fact that "done" has finite domain

Email Gateway (Aug 22 2022 at 11:58):

From: Dmitriy Traytel <traytel@inf.ethz.ch>
Primec supports a syntactic fragment where for nested recursion (here nesting through the function type and option) one has to use the corresponding map functions. For the function type this is “o” (which is allowed to be unfolded as well, see below) and for option this is map_option. So tuning the function’s specification a bit makes it accepted by primrec:

primrec
por_well_formed :: "POR ⇒ bool"
where
"por_well_formed (POR runnable todo done) =
( todo |⊆| runnable
∧ dom done ⊆ fset runnable
∧ fset todo ∩ dom done = {}
∧ (∀ p. map_option por_well_formed (done p) ≠ Some False))”

Then one can derive the original equation by (induct por) (auto simp: ran_def).

Dmitriy

Last updated: Nov 21 2024 at 12:39 UTC