Divide and conquer

A divide-and-conquer recursion (Turing.MultiTapeTM.DivConq) solves a base problem directly and otherwise solves a first subproblem, derives a second subproblem and some saved data from the problem and the first solution, solves the second subproblem, and combines the saved data with the second solution. Its evaluation with a cost is the inductive relation Turing.MultiTapeTM.DivConq.Eval: a node costs its two subproblems plus a cost of its own.

If the parts are computable, the solution is computable within the cost of the evaluation, when the cost of every node covers the costs of its parts and the lengths of the words it touches (Turing.MultiTapeTM.ComputableInO.divConq). The machine runs the recursion as a Turing.MultiTapeTM.StackLoop, keeping the pending problems and saved data on a stack, so a node does not pay for the frames of its ancestors.

Main definitions

• Turing.MultiTapeTM.DivConq: the parts of a divide-and-conquer recursion.
• Turing.MultiTapeTM.DivConq.Eval: evaluation with a cost.

Main results

• Turing.MultiTapeTM.ComputableInO.divConq: divide and conquer within the cost of the evaluation.

structure Turing.MultiTapeTM.DivConq (α β γ : Type) : Type

The parts of a divide-and-conquer recursion: a test for base problems, their solutions, the first subproblem, the second subproblem and saved data from the problem and the first solution, and the solution from the saved data and the second solution.

• isBase : α → Bool

  Whether a problem is solved directly.

• base : α → β

  The solution of a base problem.

• left : α → α

  The first subproblem.

• mid : α × β → α × γ

  The second subproblem and the saved data, from the problem and the first solution.

• join : γ × β → β

  The solution, from the saved data and the second solution.

inductive Turing.MultiTapeTM.DivConq.Eval {α β γ : Type} (D : DivConq α β γ) (cb : α → ℕ) (cn : α → β → β → ℕ) : α → β → ℕ → Prop

D.Eval cb cn a b c: the recursion solves a with b, at cost c, where a base problem a costs cb a and a node a with solutions b₁ and b₂ of its subproblems costs cn a b₁ b₂ on top of its subproblems.

• base {α β γ : Type} {D : DivConq α β γ} {cb : α → ℕ} {cn : α → β → β → ℕ} {a : α} : D.isBase a = true → D.Eval cb cn a (D.base a) (cb a)

  A base problem.

• node {α β γ : Type} {D : DivConq α β γ} {cb : α → ℕ} {cn : α → β → β → ℕ} {a : α} {b₁ b₂ : β} {c₁ c₂ : ℕ} : D.isBase a = false → D.Eval cb cn (D.left a) b₁ c₁ → D.Eval cb cn (D.mid (a, b₁)).1 b₂ c₂ → D.Eval cb cn a (D.join ((D.mid (a, b₁)).2, b₂)) (c₁ + c₂ + cn a b₁ b₂)

  A node: the first subproblem, then the second.

theorem Turing.MultiTapeTM.DivConq.Eval.scale {α β γ : Type} {D : DivConq α β γ} {cb : α → ℕ} {cn : α → β → β → ℕ} (k : ℕ) {a : α} {b : β} {c : ℕ} (h : D.Eval cb cn a b c) : D.Eval (fun (a : α) => k * cb a) (fun (a : α) (b₁ b₂ : β) => k * cn a b₁ b₂) a b (k * c)

Scaling the costs of base problems and nodes scales the cost of an evaluation.

theorem Turing.MultiTapeTM.DivConq.Eval.length_le {α β γ : Type} {D : DivConq α β γ} {cb : α → ℕ} {cn : α → β → β → ℕ} {encA : α ↪ List Bool} {encB : β ↪ List Bool} (hb : ∀ (a : α), D.isBase a = true → (encA a).length + (encB (D.base a)).length ≤ cb a) (hn : ∀ (a : α) (b₁ b₂ : β), D.isBase a = false → (encA a).length + (encB (D.join ((D.mid (a, b₁)).2, b₂))).length ≤ cn a b₁ b₂) {a : α} {b : β} {c : ℕ} (h : D.Eval cb cn a b c) : (encA a).length + (encB b).length ≤ c

The problem and its solution are within the cost of an evaluation, when the cost of every base problem and node covers them.

The recursion as a stack loop

Certificates for the rounds

theorem Turing.MultiTapeTM.ComputableInO.divConq {δ α β γ : Type} {encIn : δ ↪ List Bool} {encA : α ↪ List Bool} {encB : β ↪ List Bool} {encG : γ ↪ List Bool} (D : DivConq α β γ) {init : δ → α} {F : δ → β} {C : δ → ℕ} {cb : α → ℕ} {cn : α → β → β → ℕ} {Ti Si : δ → ℕ} {Tt St Tb Sb Tl Sl : α → ℕ} {Tm Sm : α × β → ℕ} {Tj Sj : γ × β → ℕ} (hinit : ComputableInO init encIn encA Ti Si) (hisBase : ComputableInO D.isBase encA encBool Tt St) (hbase : ComputableInO D.base encA encB Tb Sb) (hleft : ComputableInO D.left encA encA Tl Sl) (hmid : ComputableInO D.mid (encPair encA encB) (encPair encA encG) Tm Sm) (hjoin : ComputableInO D.join (encPair encG encB) encB Tj Sj) (hcb : ∀ (a : α), D.isBase a = true → Tt a + St a + Tb a + Sb a + (encA a).length + (encB (D.base a)).length + 1 ≤ cb a) (hcn : ∀ (a : α) (b₁ b₂ : β), D.isBase a = false → Tt a + St a + Tl a + Sl a + Tm (a, b₁) + Sm (a, b₁) + Tj ((D.mid (a, b₁)).2, b₂) + Sj ((D.mid (a, b₁)).2, b₂) + (encA a).length + (encA (D.left a)).length + (encB b₁).length + (encA (D.mid (a, b₁)).1).length + (encG (D.mid (a, b₁)).2).length + (encB b₂).length + (encB (D.join ((D.mid (a, b₁)).2, b₂))).length + 1 ≤ cn a b₁ b₂) (heval : ∀ (x : δ), D.Eval cb cn (init x) (F x) (C x)) : ComputableInO F encIn encB (fun (x : δ) => (encIn x).length + Ti x + Si x + C x) fun (x : δ) => (encIn x).length + Ti x + Si x + C x

Divide and conquer. If the parts of a divide-and-conquer recursion are computable and every input x is solved with F x at cost C x, then F is computable within the cost of the evaluation plus the initialization. The cost of a base problem must cover its test, its solution and the lengths of the problem and its solution; the cost of a node must cover its test, the first subproblem, the middle and the combination, and the lengths of all the values they read and write.