Theory Worklist

section ‹Worklist algorithm›

theory Worklist
  imports Basics "Root_Balanced_Tree.Time_Monad"
begin


locale W =
  fixes T :: "'x ⇒ ('x, 'd :: complete_lattice) strategy_tree"
  assumes acc: "wf {(y::'d,x::'d). x < y}"
      and finite_vars: "finite (UNIV :: 'x set)"
begin

subsection ‹Definition of Worklist algorithm›

function (domintros) eval :: "'x ⇒ ('x, 'd) strategy_tree ⇒ ('x, 'x list) fmap ⇒ ('x, 'd) map
    ⇒ 'd × ('x,'x list) fmap" where
  "eval _ (Answer d) infl _ = (d, infl)" |
  "eval x (Query y g) infl σ =
    eval x (g (mlup σ y)) (fmupd y ((fmlookup_default infl [] y) @ [x]) infl) σ"
  by pat_completeness auto

termination eval
  by (relation "measure (λ(x,t,i,σ). rhs_length t σ)") auto

function (domintros) iterate :: "'x list ⇒ ('x, 'x list) fmap ⇒ ('x, 'd) map ⇒ ('x, 'd) map" where
  "iterate [] infl σ = σ"
| "iterate (x # xs) infl σ = (
    let (d, infl) = eval x (T x) infl σ in
    let d_new = mlup σ x ⊔ d in
    if d_new = mlup σ x then iterate xs infl σ
    else iterate (xs @ fmlookup_default infl [] x) (fmupd x [] infl) (σ(x↦d_new)))"
  by (metis neq_Nil_conv surj_pair) auto

fun solve :: "'x ⇒ ('x, 'd) map" where
  "solve x = iterate [x] fmempty Map.empty"


subsection‹Proving Termination for Lattices Fulfilling ACC›

text ‹For finding a measurement function for the termination of iterate, consider the following
  points:
  - The length of the worklist decreases, when a local fixpoint is reached for the currently
    iterated unknown.
  - The length of the worklist increases when the value of the currently iterated unknown changes.
    Then all the unknowns it directly depends on, i.e., the unknowns contained in its right-hand
    side are added to the worklist.
  - With monotonic right-hand sides an unknown may only change its value as often as the height of
    the lattice.
  - To exclude non-termination due to new unknowns being added infinitely often, one needs to
    guarantee that the set of visited unknowns is finite. Q: How can one formalise this assumption?
›

definition term_relation ::  "(('x list × ('x, 'x list) fmap × ('x, 'd) map)
    × ('x list × ('x, 'x list) fmap × ('x, 'd) map)) set" where
  "term_relation = inv_image (lex_prod sigma_increasing (measure length)) (λ(wl,infl,σ). (σ, wl))"

lemma wf_term_relation: "wf term_relation"
  by (simp add: term_relation_def wf_lex_prod wf_sigma_increasing[OF acc finite_vars])

termination iterate
proof (relation term_relation, goal_cases)
  case 1
  then show ?case using wf_term_relation by auto
next
  case (2 x xs infl σ _ d' infl' _)
  then show ?case by (simp add: term_relation_def)
next
  case (3 x xs infl σ _ xb y d'acc)
  obtain d' infl' where "(d', infl') = eval x (T x) infl σ" using 3(1,2) by blast
  have "mlup σ x < d'acc" using 3(3,4) by (simp add: order_neq_le_trans)
  then have "mlup σ x < mlup (σ(x ↦ d'acc)) x" by (simp add: mlup_def)
  moreover have "mlup σ u ≤ mlup (σ(x ↦ d'acc)) u" for u
  proof (cases "x = u")
    case True
    then show ?thesis using ‹mlup σ x < mlup (σ(x ↦ d'acc)) x› by auto
  next
    case False
    then show ?thesis by (simp add: mlup_def)
  qed
  ultimately have "(σ(x ↦ d'acc), σ) ∈ sigma_increasing"
    using sigma_increasing_def finite_vars by auto
  then show ?case unfolding term_relation_def lex_prod_def by force
qed


subsection ‹Definition of Worklist algorithm with timing monad›

text ‹We count the evaluations of right-hand sides, i.e., all top-level calls to eval, ignoring
  successive recursive calls to eval. The underlying assumption is, that the evaluation of
  right-hand sides is most costly, and the maintenance of the solver's data structures negligible
  in comparison.›

function (domintros) eval_tm :: "'x ⇒ ('x, 'd) strategy_tree ⇒ ('x, 'x list) fmap
    ⇒ ('x, 'd) map ⇒ ('d × ('x,'x list) fmap) tm" where
  "eval_tm _ (Answer d) infl _ = return (d, infl)" |
  "eval_tm x (Query y g) infl σ =
    eval_tm x (g (mlup σ y)) (fmupd y ((fmlookup_default infl [] y) @ [x]) infl) σ"
  by pat_completeness auto

termination eval_tm
  by (relation "measure (λ(x,t,i,σ). rhs_length t σ)") auto

function (domintros) iterate_tm
    :: "'x list ⇒ ('x, 'x list) fmap ⇒ ('x, 'd) map ⇒ (('x, 'd) map) tm" where
  "iterate_tm [] infl σ = return σ"
| "iterate_tm (x # xs) infl σ = (do {
    (d, infl) <- eval_tm x (T x) infl σ;
    let d_new = mlup σ x ⊔ d in
    if d_new = mlup σ x then iterate_tm xs infl σ
    else iterate_tm (xs @ fmlookup_default infl [] x) (fmupd x [] infl) (σ(x↦d_new))})"
  by (metis neq_Nil_conv surj_pair) auto

fun solve_tm :: "'x ⇒ (('x, 'd) map) tm" where
  "solve_tm x = iterate_tm [x] fmempty Map.empty"

termination iterate_tm
proof (relation term_relation, goal_cases)
  case 1
  then show ?case using wf_term_relation by auto
next
  case (2 x xs infl σ _ d' infl')
  then show ?case by (simp add: term_relation_def)
next
  case (3 x xs infl σ d' y d'acc)
  obtain d' infl' where "(d', infl') = Time_Monad.val (eval_tm x (T x) infl σ)"
    using 3(1,2) by blast
  have "mlup σ x < d'acc" using 3(2,3) by (simp add: order_neq_le_trans)
  then have "mlup σ x < mlup (σ(x ↦ d'acc)) x" by (simp add: mlup_def)
  moreover have "mlup σ u ≤ mlup (σ(x ↦ d'acc)) u" for u
  proof (cases "x = u")
    case True
    then show ?thesis using ‹mlup σ x < mlup (σ(x ↦ d'acc)) x› by auto
  next
    case False
    then show ?thesis by (simp add: mlup_def)
  qed
  ultimately have "(σ(x ↦ d'acc), σ) ∈ sigma_increasing"
    using sigma_increasing_def finite_vars by auto
  then show ?case unfolding term_relation_def lex_prod_def by force
qed


subsection‹Equivalence of the Original Solve and Timed Solve Function›

lemma eval_equiv: "eval x t infl σ = Time_Monad.val (eval_tm x t infl σ)"
  by (induction rule: eval.induct) auto

lemma iterate_dom_equiv: "iterate_tm_dom (wl, infl, σ) ⟷ iterate_dom (wl, infl, σ)"
proof (intro iffI, goal_cases)
  case 1
  then show ?case
  proof (induction rule: iterate_tm.pinduct)
    case (1 infl σ)
    then show ?case using iterate.domintros(1) by auto
  next
    case (2 x xs infl σ)
    then show ?case using iterate.domintros(2)[of x infl σ xs] eval_equiv by metis
  qed
next
  case 2
  then show ?case
  proof (induction rule: iterate.pinduct)
    case (1 infl σ)
    then show ?case using iterate_tm.domintros(1) by auto
  next
    case (2 x xs infl σ)
    then show ?case using eval_equiv iterate_tm.domintros(2) by force
  qed
qed

lemma iterate_equiv: "iterate wl infl σ = Time_Monad.val (iterate_tm wl infl σ)"
proof (induction wl infl σ rule: iterate.induct)
  case (1 infl σ)
  then show ?case by simp
next
  case (2 x xs infl σ)
  obtain d' infl' where defs: "eval x (T x) infl σ = (d', infl')" by fastforce
  then have tm_defs: "Time_Monad.val (eval_tm x (T x) infl σ) = (d', infl')"
    using eval_equiv[of x "T x" infl σ] by auto
  show ?case
  proof (cases "mlup σ x ⊔ d' = mlup σ x")
    case True
    have "iterate xs infl' σ = Time_Monad.val (iterate_tm xs infl' σ)"
      using True "2.IH" defs by fastforce
    then show ?thesis using True eval_equiv tm_defs by auto
  next
    case False
    have "iterate (xs @ fmlookup_default infl' [] x) (fmupd x [] infl') (σ(x ↦ mlup σ x ⊔ d')) =
        Time_Monad.val (iterate_tm (xs @ fmlookup_default infl' [] x) (fmupd x [] infl')
        (σ(x ↦ mlup σ x ⊔ d')))"
      using False "2.IH" defs by fastforce
    then show ?thesis by (simp add: False eval_equiv tm_defs)
  qed
qed

lemma solve_equiv: "solve x = Time_Monad.val (solve_tm x)"
  using iterate_equiv by fastforce

end

end