Basic functions within linear work space

Arithmetic on binary naturals and operations on lists, computable within work space linear in the lengths of their encoded arguments, for Turing.MultiTapeTM.ComputableInSpace. Combinators keep a computation within a fixed space budget.

Main results

• Turing.MultiTapeTM.ComputableInSpace.natDivMod: the quotient and the remainder.
• Turing.MultiTapeTM.ComputableInSpace.natMul: multiplication.
• Turing.MultiTapeTM.ComputableInSpace.getD: the element of a list at an index.
• Turing.MultiTapeTM.ComputableInSpace.set: replacing the element at an index.
• Turing.MultiTapeTM.ComputableInSpace.budget_natAdd, Turing.MultiTapeTM.ComputableInSpace.budget_cons and their siblings: arithmetic and list operations on values computed within a fixed budget stay within it.
• Turing.MultiTapeTM.ComputableInSpace.budget_optionSome, Turing.MultiTapeTM.ComputableInSpace.budget_optionGetD, Turing.MultiTapeTM.ComputableInSpace.budget_optionIsSome: building and reading options.
• Turing.MultiTapeTM.ComputableInSpace.dispatch: a case distinction on the element of a fixed list at a computed index.

Computing within a space budget

theorem Turing.MultiTapeTM.ComputableInSpace.budget_comp {α β γ : Type} {encIn : α ↪ List Bool} {encB : β ↪ List Bool} {encC : γ ↪ List Bool} {Bs : α → ℕ} {f : α → β} {g : β → γ} {Sg : β → ℕ} (hg : ComputableInSpace g encB encC Sg) (hf : ComputableInSpace f encIn encB Bs) (hS : BigOLe (fun (x : α) => Sg (f x)) Bs) : ComputableInSpace (fun (x : α) => g (f x)) encIn encC Bs

theorem Turing.MultiTapeTM.ComputableInSpace.budget_comp_linear {α β γ : Type} {encIn : α ↪ List Bool} {encB : β ↪ List Bool} {encC : γ ↪ List Bool} {Bs : α → ℕ} {f : α → β} {g : β → γ} (hg : ComputableInSpace g encB encC fun (b : β) => (encB b).length) (hf : ComputableInSpace f encIn encB Bs) : ComputableInSpace (fun (x : α) => g (f x)) encIn encC Bs

theorem Turing.MultiTapeTM.ComputableInSpace.linear_mul {β : Type} {encB : β ↪ List Bool} (k : ℕ) : BigOLe (fun (b : β) => k * ((encB b).length + 1)) fun (b : β) => (encB b).length

A multiple of the length of the argument, plus a constant, is linear in it.

theorem Turing.MultiTapeTM.ComputableInSpace.linear_succ {β : Type} {encB : β ↪ List Bool} : BigOLe (fun (b : β) => (encB b).length + 1) fun (b : β) => (encB b).length

theorem Turing.MultiTapeTM.ComputableInSpace.budget_comp_lin {α β γ : Type} {encIn : α ↪ List Bool} {encB : β ↪ List Bool} {encC : γ ↪ List Bool} {Bs : α → ℕ} {f : α → β} {g : β → γ} {Sg : β → ℕ} (hg : ComputableInSpace g encB encC Sg) (hSg : BigOLe Sg fun (b : β) => (encB b).length) (hf : ComputableInSpace f encIn encB Bs) : ComputableInSpace (fun (x : α) => g (f x)) encIn encC Bs

Composition with a function computed in space linear in its argument: no side condition, as the argument is computed within the budget.

theorem Turing.MultiTapeTM.ComputableInSpace.budget_prod {α β γ : Type} {encIn : α ↪ List Bool} {encB : β ↪ List Bool} {encC : γ ↪ List Bool} {Bs : α → ℕ} {f : α → β} {g : α → γ} (hf : ComputableInSpace f encIn encB Bs) (hg : ComputableInSpace g encIn encC Bs) : ComputableInSpace (fun (x : α) => (f x, g x)) encIn (encPair encB encC) Bs

theorem Turing.MultiTapeTM.ComputableInSpace.budget_ite {α β : Type} {encIn : α ↪ List Bool} {encB : β ↪ List Bool} {Bs : α → ℕ} {c : α → Bool} {f g : α → β} (hc : ComputableInSpace c encIn encBool Bs) (hf : ComputableInSpace f encIn encB Bs) (hg : ComputableInSpace g encIn encB Bs) : ComputableInSpace (fun (x : α) => if c x = true then f x else g x) encIn encB Bs

theorem Turing.MultiTapeTM.ComputableInSpace.budget_const {α β : Type} {encIn : α ↪ List Bool} {encB : β ↪ List Bool} {Bs : α → ℕ} (b : β) (hl : BigOLe (fun (x : α) => (encIn x).length) Bs) : ComputableInSpace (fun (x : α) => b) encIn encB Bs

theorem Turing.MultiTapeTM.ComputableInSpace.budget_finite {α β γ : Type} {encIn : α ↪ List Bool} {encB : β ↪ List Bool} {encC : γ ↪ List Bool} {Bs : α → ℕ} {f : α → β} [Finite β] (g : β → γ) (hf : ComputableInSpace f encIn encB Bs) : ComputableInSpace (fun (x : α) => g (f x)) encIn encC Bs

theorem Turing.MultiTapeTM.ComputableInSpace.budget_iterate {α β : Type} {encIn : α ↪ List Bool} {encB : β ↪ List Bool} {Bs : α → ℕ} [Inhabited β] {n : α → ℕ} {init : α → β} {step : β → β} {B : α → ℕ} (hn : ComputableInSpace n encIn encNat Bs) (hinit : ComputableInSpace init encIn encB Bs) (hstep : ComputableInSpace step encB encB fun (b : β) => (encB b).length) (hstate : ∀ (x : α), ∀ k ≤ n x, (encB (step^[k] (init x))).length ≤ B x) (hB : BigOLe B Bs) : ComputableInSpace (fun (x : α) => step^[n x] (init x)) encIn encB Bs

Iterating a step computed in linear space, a computed number of times, within a budget that covers the states.

Direct linear list and framing helpers

theorem Turing.MultiTapeTM.ComputableInSpace.cons {ε : Type} (enc : ε ↪ List Bool) : ComputableInSpace (fun (p : ε × List ε) => p.1 :: p.2) (encPair enc (encList enc)) (encList enc) fun (p : ε × List ε) => ((encPair enc (encList enc)) p).length

Prepending an element to an encoded list in linear space.

theorem Turing.MultiTapeTM.ComputableInSpace.snoc {ε : Type} (enc : ε ↪ List Bool) : ComputableInSpace (fun (p : List ε × ε) => p.1 ++ [p.2]) (encPair (encList enc) enc) (encList enc) fun (p : List ε × ε) => ((encPair (encList enc) enc) p).length

Appending an element at the end of an encoded list in linear space.

theorem Turing.MultiTapeTM.ComputableInSpace.frame {ε : Type} (enc : ε ↪ List Bool) : ComputableInSpace (fun (a : ε) => MultiTapeTM.frame (enc a)) enc encBits fun (a : ε) => (enc a).length

Framing an encoded value in linear space.

Arithmetic

theorem Turing.MultiTapeTM.ComputableInSpace.natSucc : ComputableInSpace (fun (x : ℕ) => x + 1) encNat encNat fun (n : ℕ) => (encNat n).length + 1

theorem Turing.MultiTapeTM.ComputableInSpace.natPred : ComputableInSpace (fun (x : ℕ) => x - 1) encNat encNat fun (n : ℕ) => (encNat n).length + 1

theorem Turing.MultiTapeTM.ComputableInSpace.natIsZero : ComputableInSpace (fun (n : ℕ) => decide (n = 0)) encNat encBool fun (n : ℕ) => (encNat n).length

theorem Turing.MultiTapeTM.ComputableInSpace.natEq : ComputableInSpace (fun (p : ℕ × ℕ) => decide (p.1 = p.2)) (encPair encNat encNat) encBool fun (p : ℕ × ℕ) => ((encPair encNat encNat) p).length

theorem Turing.MultiTapeTM.ComputableInSpace.natLt : ComputableInSpace (fun (p : ℕ × ℕ) => decide (p.1 < p.2)) (encPair encNat encNat) encBool fun (p : ℕ × ℕ) => ((encPair encNat encNat) p).length + 1

theorem Turing.MultiTapeTM.ComputableInSpace.natSub : ComputableInSpace (fun (p : ℕ × ℕ) => p.2 - p.1) (encPair encNat encNat) encNat fun (p : ℕ × ℕ) => ((encPair encNat encNat) p).length + 1

Truncated subtraction, b - a from (a, b): the second component minus the first.

theorem Turing.MultiTapeTM.ComputableInSpace.natAdd : ComputableInSpace (fun (p : ℕ × ℕ) => p.1 + p.2) (encPair encNat encNat) encNat fun (p : ℕ × ℕ) => ((encPair encNat encNat) p).length + 1

theorem Turing.MultiTapeTM.ComputableInSpace.dispatch {α β : Type} {encIn : α ↪ List Bool} {encB : β ↪ List Bool} {κ : Type u_1} (l : List κ) (d : κ) (F : κ → α → β) (hF : ∀ (x : κ), ComputableInSpace (F x) encIn encB fun (a : α) => (encIn a).length) {i : α → ℕ} (hi : ComputableInSpace i encIn encNat fun (a : α) => (encIn a).length) : ComputableInSpace (fun (a : α) => F (l.getD (i a) d) a) encIn encB fun (a : α) => (encIn a).length

Dispatching on the element of a fixed list at a computed index: if F x is computed in linear space for every x, and the index is computed in linear space, then so is F (l.getD (i a) d) a. A finite case distinction, as on the instruction at the current label of a program.

def Turing.MultiTapeTM.ComputableInSpace.divStep (s : ℕ × ℕ × ℕ) : ℕ × ℕ × ℕ

A step of division: subtract the divisor from the remainder and count, while it fits.

theorem Turing.MultiTapeTM.ComputableInSpace.iterate_divStep (d r k : ℕ) : divStep^[k] (d, 0, r) = (d, min k (r / d), r - d * min k (r / d))

theorem Turing.MultiTapeTM.ComputableInSpace.iterate_divStep_self (d r : ℕ) : divStep^[r] (d, 0, r) = (d, r / d, r % d)

theorem Turing.MultiTapeTM.ComputableInSpace.divStep_inSpace : ComputableInSpace divStep encNat3 encNat3 fun (s : ℕ × ℕ × ℕ) => (encNat3 s).length + 1

theorem Turing.MultiTapeTM.ComputableInSpace.natDivMod : ComputableInSpace (fun (p : ℕ × ℕ) => (p.1 / p.2, p.1 % p.2)) (encPair encNat encNat) (encPair encNat encNat) fun (p : ℕ × ℕ) => 16 * (((encPair encNat encNat) p).length + 1)

The quotient and the remainder, (r / d, r % d) from (r, d).

theorem Turing.MultiTapeTM.ComputableInSpace.natDiv : ComputableInSpace (fun (p : ℕ × ℕ) => p.1 / p.2) (encPair encNat encNat) encNat fun (p : ℕ × ℕ) => 16 * (((encPair encNat encNat) p).length + 1)

The quotient.

theorem Turing.MultiTapeTM.ComputableInSpace.natMod : ComputableInSpace (fun (p : ℕ × ℕ) => p.1 % p.2) (encPair encNat encNat) encNat fun (p : ℕ × ℕ) => 16 * (((encPair encNat encNat) p).length + 1)

The remainder.

theorem Turing.MultiTapeTM.ComputableInSpace.natMul : ComputableInSpace (fun (p : ℕ × ℕ) => p.1 * p.2) (encPair encNat encNat) encNat fun (p : ℕ × ℕ) => 32 * (((encPair encNat encNat) p).length + 1)

Multiplication in binary.

Lists of naturals

theorem Turing.MultiTapeTM.ComputableInSpace.getD : ComputableInSpace (fun (p : List ℕ × ℕ) => p.1.getD p.2 0) (encPair (encList encNat) encNat) encNat fun (p : List ℕ × ℕ) => 8 * (((encPair (encList encNat) encNat) p).length + 1)

The element at an index, l.getD i 0 from (l, i).

def Turing.MultiTapeTM.ComputableInSpace.setStep (s : (ℕ × ℕ) × ℕ × List ℕ) (a : ℕ) : (ℕ × ℕ) × ℕ × List ℕ

A step of rebuilding a list with the element at i replaced by v.

theorem Turing.MultiTapeTM.ComputableInSpace.foldl_setStep (i v : ℕ) (l : List ℕ) (j : ℕ) (acc : List ℕ) : List.foldl setStep ((i, v), j, acc) l = ((i, v), j + l.length, acc ++ List.mapIdx (fun (k a : ℕ) => if j + k = i then v else a) l)

theorem Turing.MultiTapeTM.ComputableInSpace.set_eq_mapIdx (l : List ℕ) (i v : ℕ) : l.set i v = List.mapIdx (fun (k a : ℕ) => if k = i then v else a) l

@[reducible, inline]

abbrev Turing.MultiTapeTM.ComputableInSpace.encSetState : (ℕ × ℕ) × ℕ × List ℕ ↪ List Bool

The encoding of the states of setStep.

theorem Turing.MultiTapeTM.ComputableInSpace.setStep_inSpace : ComputableInSpace (fun (q : ((ℕ × ℕ) × ℕ × List ℕ) × ℕ) => setStep q.1 q.2) (encPair encSetState encNat) encSetState fun (q : ((ℕ × ℕ) × ℕ × List ℕ) × ℕ) => 4 * (((encPair encSetState encNat) q).length + 1)

theorem Turing.MultiTapeTM.ComputableInSpace.set : ComputableInSpace (fun (p : List ℕ × ℕ × ℕ) => p.1.set p.2.1 p.2.2) (encPair (encList encNat) (encPair encNat encNat)) (encList encNat) fun (p : List ℕ × ℕ × ℕ) => 128 * (((encPair (encList encNat) (encPair encNat encNat)) p).length + 1)

Replacing the element at an index, l.set i v from (l, i, v).

Building and measuring lists

theorem Turing.MultiTapeTM.ComputableInSpace.iterate_cons {ε : Type} (a : ε) (l : List ε) (k : ℕ) : (fun (q : ε × List ε) => (q.1, q.1 :: q.2))^[k] (a, l) = (a, List.replicate k a ++ l)

theorem Turing.MultiTapeTM.ComputableInSpace.replicate {ε : Type} {enc : ε ↪ List Bool} [Inhabited ε] : ComputableInSpace (fun (p : ℕ × ε) => List.replicate p.1 p.2) (encPair encNat enc) (encList enc) fun (p : ℕ × ε) => 64 * ((p.1 + 1) * (((encPair encNat enc) p).length + 1))

A list of copies, List.replicate n a from (n, a); its work space is that of the list.

theorem Turing.MultiTapeTM.ComputableInSpace.length {ε : Type} {enc : ε ↪ List Bool} : ComputableInSpace (fun (l : List ε) => l.length) (encList enc) encNat fun (l : List ε) => 8 * (((encList enc) l).length + 1)

The length of a list.

theorem Turing.MultiTapeTM.ComputableInSpace.mapWith {α : Type} {encIn : α ↪ List Bool} {ε : Type} {enc : ε ↪ List Bool} {π κ : Type} {encP : π ↪ List Bool} {encK : κ ↪ List Bool} {f : π × ε → κ} {Sf : π × ε → ℕ} {par : α → π} {list : α → List ε} {Sp Sl : α → ℕ} (hf : ComputableInSpace f (encPair encP enc) encK Sf) (hpar : ComputableInSpace par encIn encP Sp) (hlist : ComputableInSpace list encIn (encList enc) Sl) : ComputableInSpace (fun (x : α) => List.map (fun (a : ε) => f (par x, a)) (list x)) encIn (encList encK) fun (x : α) => (encIn x).length + Sp x + Sl x + (encP (par x)).length + ((encList enc) (list x)).length + ((encList encK) (List.map (fun (a : ε) => f (par x, a)) (list x))).length + listMax (fun (a : ε) => Sf (par x, a)) (list x)

Mapping with a parameter, within the space of the parameter, of the list, of the mapped list and of the largest application.

Operations within a fixed budget

theorem Turing.MultiTapeTM.ComputableInSpace.budget_cons {α : Type} {encIn : α ↪ List Bool} {Bs : α → ℕ} {ε : Type} {enc : ε ↪ List Bool} {a : α → ε} {l : α → List ε} (ha : ComputableInSpace a encIn enc Bs) (hl : ComputableInSpace l encIn (encList enc) Bs) : ComputableInSpace (fun (x : α) => a x :: l x) encIn (encList enc) Bs

Adding an element in front of a list, within the budget.

theorem Turing.MultiTapeTM.ComputableInSpace.budget_snoc {α : Type} {encIn : α ↪ List Bool} {Bs : α → ℕ} {ε : Type} {enc : ε ↪ List Bool} {l : α → List ε} {a : α → ε} (hl : ComputableInSpace l encIn (encList enc) Bs) (ha : ComputableInSpace a encIn enc Bs) : ComputableInSpace (fun (x : α) => l x ++ [a x]) encIn (encList enc) Bs

Appending an element at the end of a list, within the budget.

theorem Turing.MultiTapeTM.ComputableInSpace.budget_headD {α : Type} {encIn : α ↪ List Bool} {Bs : α → ℕ} {ε : Type} {enc : ε ↪ List Bool} (d : ε) {l : α → List ε} (hl : ComputableInSpace l encIn (encList enc) Bs) : ComputableInSpace (fun (x : α) => (l x).headD d) encIn enc Bs

The head of a list, within the budget.

theorem Turing.MultiTapeTM.ComputableInSpace.budget_tail {α : Type} {encIn : α ↪ List Bool} {Bs : α → ℕ} {ε : Type} {enc : ε ↪ List Bool} {l : α → List ε} (hl : ComputableInSpace l encIn (encList enc) Bs) : ComputableInSpace (fun (x : α) => (l x).tail) encIn (encList enc) Bs

The tail of a list, within the budget.

theorem Turing.MultiTapeTM.ComputableInSpace.budget_isEmpty {α : Type} {encIn : α ↪ List Bool} {Bs : α → ℕ} {ε : Type} {enc : ε ↪ List Bool} {l : α → List ε} (hl : ComputableInSpace l encIn (encList enc) Bs) : ComputableInSpace (fun (x : α) => (l x).isEmpty) encIn encBool Bs

Whether a list is empty, within the budget.

theorem Turing.MultiTapeTM.ComputableInSpace.budget_length {α : Type} {encIn : α ↪ List Bool} {Bs : α → ℕ} {ε : Type} {enc : ε ↪ List Bool} {l : α → List ε} (hl : ComputableInSpace l encIn (encList enc) Bs) : ComputableInSpace (fun (x : α) => (l x).length) encIn encNat Bs

The length of a list, within the budget.

theorem Turing.MultiTapeTM.ComputableInSpace.budget_natSucc {α : Type} {encIn : α ↪ List Bool} {Bs a : α → ℕ} (ha : ComputableInSpace a encIn encNat Bs) : ComputableInSpace (fun (x : α) => a x + 1) encIn encNat Bs

The successor, within the budget.

theorem Turing.MultiTapeTM.ComputableInSpace.budget_natPred {α : Type} {encIn : α ↪ List Bool} {Bs a : α → ℕ} (ha : ComputableInSpace a encIn encNat Bs) : ComputableInSpace (fun (x : α) => a x - 1) encIn encNat Bs

The predecessor, within the budget.

theorem Turing.MultiTapeTM.ComputableInSpace.budget_natIsZero {α : Type} {encIn : α ↪ List Bool} {Bs a : α → ℕ} (ha : ComputableInSpace a encIn encNat Bs) : ComputableInSpace (fun (x : α) => decide (a x = 0)) encIn encBool Bs

The zero test, within the budget.

theorem Turing.MultiTapeTM.ComputableInSpace.budget_natEq {α : Type} {encIn : α ↪ List Bool} {Bs a b : α → ℕ} (ha : ComputableInSpace a encIn encNat Bs) (hb : ComputableInSpace b encIn encNat Bs) : ComputableInSpace (fun (x : α) => decide (a x = b x)) encIn encBool Bs

Equality of numbers, within the budget.

theorem Turing.MultiTapeTM.ComputableInSpace.budget_natAdd {α : Type} {encIn : α ↪ List Bool} {Bs a b : α → ℕ} (ha : ComputableInSpace a encIn encNat Bs) (hb : ComputableInSpace b encIn encNat Bs) : ComputableInSpace (fun (x : α) => a x + b x) encIn encNat Bs

The sum, within the budget.

theorem Turing.MultiTapeTM.ComputableInSpace.budget_natMul {α : Type} {encIn : α ↪ List Bool} {Bs a b : α → ℕ} (ha : ComputableInSpace a encIn encNat Bs) (hb : ComputableInSpace b encIn encNat Bs) : ComputableInSpace (fun (x : α) => a x * b x) encIn encNat Bs

The product, within the budget.

theorem Turing.MultiTapeTM.ComputableInSpace.budget_natDiv {α : Type} {encIn : α ↪ List Bool} {Bs a b : α → ℕ} (ha : ComputableInSpace a encIn encNat Bs) (hb : ComputableInSpace b encIn encNat Bs) : ComputableInSpace (fun (x : α) => a x / b x) encIn encNat Bs

The quotient, within the budget.

theorem Turing.MultiTapeTM.ComputableInSpace.budget_natSub {α : Type} {encIn : α ↪ List Bool} {Bs a b : α → ℕ} (ha : ComputableInSpace a encIn encNat Bs) (hb : ComputableInSpace b encIn encNat Bs) : ComputableInSpace (fun (x : α) => a x - b x) encIn encNat Bs

Truncated subtraction, within the budget.

theorem Turing.MultiTapeTM.ComputableInSpace.budget_natMod {α : Type} {encIn : α ↪ List Bool} {Bs a b : α → ℕ} (ha : ComputableInSpace a encIn encNat Bs) (hb : ComputableInSpace b encIn encNat Bs) : ComputableInSpace (fun (x : α) => a x % b x) encIn encNat Bs

The remainder, within the budget.

theorem Turing.MultiTapeTM.ComputableInSpace.budget_natLt {α : Type} {encIn : α ↪ List Bool} {Bs a b : α → ℕ} (ha : ComputableInSpace a encIn encNat Bs) (hb : ComputableInSpace b encIn encNat Bs) : ComputableInSpace (fun (x : α) => decide (a x < b x)) encIn encBool Bs

The strict comparison, within the budget.

theorem Turing.MultiTapeTM.ComputableInSpace.budget_natPow {α : Type} {encIn : α ↪ List Bool} {Bs a : α → ℕ} (ha : ComputableInSpace a encIn encNat Bs) (hin : BigOLe (fun (x : α) => (encIn x).length) Bs) (d : ℕ) : ComputableInSpace (fun (x : α) => a x ^ d) encIn encNat Bs

A fixed natural power, within the budget.

theorem Turing.MultiTapeTM.ComputableInSpace.budget_finMod {α : Type} {encIn : α ↪ List Bool} {Bs : α → ℕ} {w : ℕ} (hw : 0 < w) {m : α → ℕ} (hm : ComputableInSpace m encIn encNat Bs) (hin : BigOLe (fun (x : α) => (encIn x).length) Bs) : ComputableInSpace (fun (x : α) => ⟨m x % w, ⋯⟩) encIn (Fin.valEmbedding.trans encNat) Bs

The remainder modulo a positive constant, as an element of Fin w.

theorem Turing.MultiTapeTM.ComputableInSpace.budget_optionSome {α β : Type} {encIn : α ↪ List Bool} {encB : β ↪ List Bool} {Bs : α → ℕ} {a : α → β} (ha : ComputableInSpace a encIn encB Bs) : ComputableInSpace (fun (x : α) => some (a x)) encIn (encOption encB) Bs

some of a value, within the budget.

theorem Turing.MultiTapeTM.ComputableInSpace.budget_optionGetD {α β : Type} {encIn : α ↪ List Bool} {encB : β ↪ List Bool} {Bs : α → ℕ} {o : α → Option β} (d : β) (ho : ComputableInSpace o encIn (encOption encB) Bs) : ComputableInSpace (fun (x : α) => (o x).getD d) encIn encB Bs

The value of an option with a fixed default, within the budget.

theorem Turing.MultiTapeTM.ComputableInSpace.budget_optionIsSome {α β : Type} {encIn : α ↪ List Bool} {encB : β ↪ List Bool} {Bs : α → ℕ} {o : α → Option β} (ho : ComputableInSpace o encIn (encOption encB) Bs) : ComputableInSpace (fun (x : α) => (o x).isSome) encIn encBool Bs

Whether an option holds a value, within the budget.