Theory Roy_Floyd_Warshall
theory Roy_Floyd_Warshall
imports Main
begin
section ‹Transitive closure algorithm›
text ‹
The Roy-Floyd-Warshall algorithm takes a finite relation as input and
produces its transitive closure as output. It iterates over all elements of
the field of the relation and maintains a cumulative approximation of the
result: step ‹0› starts with the original relation, and step ‹Suc n›
connects all paths over the intermediate element ‹n›. The final
approximation coincides with the full transitive closure.
This algorithm is often named after ``Floyd'', ``Warshall'', or
``Floyd-Warshall'', but the earliest known description is due to B. Roy
\<^cite>‹"Roy:1959"›.
┉
Subsequently we use a direct mathematical model of the relation, bypassing
matrices and arrays that are usually seen in the literature. This is more
efficient for sparse relations: only the adjacency for immediate
predecessors and successors needs to be maintained, not the square of all
possible combinations. Moreover we do not have to worry about mutable data
structures in a multi-threaded environment. See also the graph
implementation in the Isabelle sources @{file
‹$ISABELLE_HOME/src/Pure/General/graph.ML›} and @{file
‹$ISABELLE_HOME/src/Pure/General/graph.scala›}.
›
type_synonym relation = "(nat × nat) set"
fun steps :: "relation ⇒ nat ⇒ relation"
where
"steps rel 0 = rel"
| "steps rel (Suc n) =
steps rel n ∪ {(x, y). (x, n) ∈ steps rel n ∧ (n, y) ∈ steps rel n}"
text ‹Implementation view on the relation:›
definition preds :: "relation ⇒ nat ⇒ nat set"
where "preds rel y = {x. (x, y) ∈ rel}"
definition succs :: "relation ⇒ nat ⇒ nat set"
where "succs rel x = {y. (x, y) ∈ rel}"
lemma
"steps rel (Suc n) =
steps rel n ∪ {(x, y). x ∈ preds (steps rel n) n ∧ y ∈ succs (steps rel n) n}"
by (simp add: preds_def succs_def)
text ‹
The main function requires an upper bound for the iteration, which is left
unspecified here (via Hilbert's choice).
›
definition is_bound :: "relation ⇒ nat ⇒ bool"
where "is_bound rel n ⟷ (∀m ∈ Field rel. m < n)"
definition "transitive_closure rel = steps rel (SOME n. is_bound rel n)"
section ‹Correctness proof›
subsection ‹Miscellaneous lemmas›
lemma finite_bound:
assumes "finite rel"
shows "∃n. is_bound rel n"
using assms
proof induct
case empty
then show ?case by (simp add: is_bound_def)
next
case (insert p rel)
then obtain n where n: "∀m ∈ Field rel. m < n"
unfolding is_bound_def by blast
obtain x y where "p = (x, y)" by (cases p)
then have "∀m ∈ Field (insert p rel). m < max (Suc x) (max (Suc y) n)"
using n by auto
then show ?case
unfolding is_bound_def by blast
qed
lemma steps_Suc: "(x, y) ∈ steps rel (Suc n) ⟷
(x, y) ∈ steps rel n ∨ (x, n) ∈ steps rel n ∧ (n, y) ∈ steps rel n"
by auto
lemma steps_cases:
assumes "(x, y) ∈ steps rel (Suc n)"
obtains (copy) "(x, y) ∈ steps rel n"
| (step) "(x, n) ∈ steps rel n" and "(n, y) ∈ steps rel n"
using assms by auto
lemma steps_rel: "(x, y) ∈ rel ⟹ (x, y) ∈ steps rel n"
by (induct n) auto
subsection ‹Bounded closure›
text ‹
The bounded closure connects all transitive paths over elements below a
given bound. For an upper bound of the relation, this coincides with the
full transitive closure.
›
inductive_set Clos :: "relation ⇒ nat ⇒ relation"
for rel :: relation and n :: nat
where
base: "(x, y) ∈ Clos rel n" if "(x, y) ∈ rel"
| step: "(x, y) ∈ Clos rel n" if "(x, z) ∈ Clos rel n" and "(z, y) ∈ Clos rel n" and "z < n"
theorem Clos_closure:
assumes "is_bound rel n"
shows "(x, y) ∈ Clos rel n ⟷ (x, y) ∈ rel⇧+"
proof
show "(x, y) ∈ rel⇧+" if "(x, y) ∈ Clos rel n"
using that by induct simp_all
show "(x, y) ∈ Clos rel n" if "(x, y) ∈ rel⇧+"
using that
proof (induct rule: trancl_induct)
case (base y)
then show ?case by (rule Clos.base)
next
case (step y z)
from ‹(y, z) ∈ rel› have 1: "(y, z) ∈ Clos rel n" by (rule base)
from ‹(y, z) ∈ rel› and ‹is_bound rel n› have 2: "y < n"
unfolding is_bound_def Field_def by blast
from step(3) 1 2 show ?case by (rule Clos.step)
qed
qed
lemma Clos_Suc:
assumes "(x, y) ∈ Clos rel n"
shows "(x, y) ∈ Clos rel (Suc n)"
using assms by induct (auto intro: Clos.intros)
text ‹
In each step of the algorithm the approximated relation is exactly the
bounded closure.
›
theorem steps_Clos_equiv: "(x, y) ∈ steps rel n ⟷ (x, y) ∈ Clos rel n"
proof (induct n arbitrary: x y)
case 0
show ?case
proof
show "(x, y) ∈ Clos rel 0" if "(x, y) ∈ steps rel 0"
proof -
from that have "(x, y) ∈ rel" by simp
then show ?thesis by (rule Clos.base)
qed
show "(x, y) ∈ steps rel 0" if "(x, y) ∈ Clos rel 0"
using that by cases simp_all
qed
next
case (Suc n)
show ?case
proof
show "(x, y) ∈ Clos rel (Suc n)" if "(x, y) ∈ steps rel (Suc n)"
using that
proof (cases rule: steps_cases)
case copy
with Suc(1) have "(x, y) ∈ Clos rel n" ..
then show ?thesis by (rule Clos_Suc)
next
case step
with Suc have "(x, n) ∈ Clos rel n" and "(n, y) ∈ Clos rel n"
by simp_all
then have "(x, n) ∈ Clos rel (Suc n)" and "(n, y) ∈ Clos rel (Suc n)"
by (simp_all add: Clos_Suc)
then show ?thesis by (rule Clos.step) simp
qed
show "(x, y) ∈ steps rel (Suc n)" if "(x, y) ∈ Clos rel (Suc n)"
using that
proof induct
case (base x y)
then show ?case by (simp add: steps_rel)
next
case (step x z y)
with Suc show ?case
by (auto simp add: steps_Suc less_Suc_eq intro: Clos.step)
qed
qed
qed
subsection ‹Main theorem›
text ‹
The main theorem follows immediately from the key observations above. Note
that the assumption of finiteness gives a bound for the iteration, although
the details are left unspecified. A concrete implementation could choose the
the maximum element + 1, or iterate directly over the data structures for
the @{term preds} and @{term succs} implementation.
›
theorem transitive_closure_correctness:
assumes "finite rel"
shows "transitive_closure rel = rel⇧+"
proof -
let ?N = "SOME n. is_bound rel n"
have is_bound: "is_bound rel ?N"
by (rule someI_ex) (rule finite_bound [OF ‹finite rel›])
have "(x, y) ∈ steps rel ?N ⟷ (x, y) ∈ rel⇧+" for x y
proof -
have "(x, y) ∈ steps rel ?N ⟷ (x, y) ∈ Clos rel ?N"
by (rule steps_Clos_equiv)
also have "… ⟷ (x, y) ∈ rel⇧+"
using is_bound by (rule Clos_closure)
finally show ?thesis .
qed
then show ?thesis unfolding transitive_closure_def by auto
qed
section ‹Alternative formulation›
text ‹
The core of the algorithm may be expressed more declaratively as follows,
using an inductive definition to imitate a logic-program. This is equivalent
to the function specification @{term steps} from above.
›
inductive Steps :: "relation ⇒ nat ⇒ nat × nat ⇒ bool"
for rel :: relation
where
base: "Steps rel 0 (x, y)" if "(x, y) ∈ rel"
| copy: "Steps rel (Suc n) (x, y)" if "Steps rel n (x, y)"
| step: "Steps rel (Suc n) (x, y)" if "Steps rel n (x, n)" and "Steps rel n (n, y)"
lemma steps_equiv: "(x, y) ∈ steps rel n ⟷ Steps rel n (x, y)"
proof
show "Steps rel n (x, y)" if "(x, y) ∈ steps rel n"
using that
proof (induct n arbitrary: x y)
case 0
then have "(x, y) ∈ rel" by simp
then show ?case by (rule base)
next
case (Suc n)
from Suc(2) show ?case
proof (cases rule: steps_cases)
case copy
with Suc(1) have "Steps rel n (x, y)" .
then show ?thesis by (rule Steps.copy)
next
case step
with Suc(1) have "Steps rel n (x, n)" and "Steps rel n (n, y)"
by simp_all
then show ?thesis by (rule Steps.step)
qed
qed
show "(x, y) ∈ steps rel n" if "Steps rel n (x, y)"
using that by induct simp_all
qed
end