Word operations and pairing in logarithmic space

The word operations underlying the encodings of pairs, options and lists — framing, reading and dropping the first frame, prepending true, dropping or keeping the first symbol, testing for emptiness, mapping a Boolean function over a bit word, and folding a finite-state transition function over an encoded word — are computed by finite-state transducers, without work tapes (Turing.MultiTapeTM.Transducer.computableInLogSpace). They are therefore computable in logarithmic space, as are the projections of pairs.

Concatenating or pairing two logspace functions of the same input runs both machines one after the other; the work space is the sum of the two (Turing.MultiTapeTM.ComputableTidilyInTimeAndSpace.append). Case distinctions run the condition test and then the selected branch (Turing.MultiTapeTM.ComputableTidilyInTimeAndSpace.ite). Together with word concatenation, these give logspace operations on options, lists, bit words, and unary numbers, as well as bounded-count batch evaluation (map_range_const, map_range_of_le, mapToBits_range_const, mapToBits_range_of_le).

Main results

• Turing.MultiTapeTM.ComputableInLogSpace.of_frame, .of_unframe, .of_dropFrame, .of_cons_true, .of_tail, .of_drop, .of_take_one, .of_isEmpty, .of_foldl_bool: word operations.
• Turing.MultiTapeTM.ComputableInLogSpace.restrict, .ite_subtype, .ite, .of_isEmpty_ite: restriction and case distinctions.
• Turing.MultiTapeTM.ComputableInLogSpace.append, Turing.MultiTapeTM.ComputableInLogSpace.fst, Turing.MultiTapeTM.ComputableInLogSpace.snd, Turing.MultiTapeTM.ComputableInLogSpace.pair: concatenation and pairing.
• Turing.MultiTapeTM.ComputableInLogSpace.optionSome, .optionGetD: option operations.
• Turing.MultiTapeTM.ComputableInLogSpace.listSingleton, .listCons, .listAppend, .listHeadD, .listLength: framed-list operations.
• Turing.MultiTapeTM.ComputableInLogSpace.bitsAppend, .bitsHeadD, .bitsMap, .bitsFoldl, .bitsAll, .bitsAny: bit-word operations.
• Turing.MultiTapeTM.ComputableInLogSpace.unaryAdd, .unaryMulConst, .unaryLeConst, .unaryBoundedMap: unary-number operations.
• Turing.MultiTapeTM.ComputableInLogSpace.map_range_const, .map_range_of_le, .mapToBits_range_const, .mapToBits_range_of_le: bounded-count batch evaluation.
• Turing.MultiTapeTM.ComputableInLogSpace.fst', .snd', .bool_and, .bool_or, .ite_decide: projections of a computed pair, Boolean connectives and case distinctions on decidable propositions, in the form used by fun_prop, with which the closure rules and word operations above are registered.

References

• M. Sipser, Introduction to the Theory of Computation, Section 8.5

theorem Turing.MultiTapeTM.ComputableInLogSpace.of_frame {α β : Type} {encIn : α ↪ List Bool} {encOut : β ↪ List Bool} {f : α → β} (h : ∀ (a : α), encOut (f a) = frame (encIn a)) : ComputableInLogSpace f encIn encOut

Framing an encoded value.

theorem Turing.MultiTapeTM.ComputableInLogSpace.of_unframe {α β : Type} {encIn : α ↪ List Bool} {encOut : β ↪ List Bool} {f : α → β} (h : ∀ (a : α), encOut (f a) = unframe (encIn a)) : ComputableInLogSpace f encIn encOut

Reading the word framed at the start of an encoded value.

theorem Turing.MultiTapeTM.ComputableInLogSpace.of_dropFrame {α β : Type} {encIn : α ↪ List Bool} {encOut : β ↪ List Bool} {f : α → β} (h : ∀ (a : α), encOut (f a) = dropFrame (encIn a)) : ComputableInLogSpace f encIn encOut

Dropping the frame at the start of an encoded value.

theorem Turing.MultiTapeTM.ComputableInLogSpace.of_cons_true {α β : Type} {encIn : α ↪ List Bool} {encOut : β ↪ List Bool} {f : α → β} (h : ∀ (a : α), encOut (f a) = true :: encIn a) : ComputableInLogSpace f encIn encOut

Prepending true to an encoded value.

theorem Turing.MultiTapeTM.ComputableInLogSpace.of_tail {α β : Type} {encIn : α ↪ List Bool} {encOut : β ↪ List Bool} {f : α → β} (h : ∀ (a : α), encOut (f a) = (encIn a).tail) : ComputableInLogSpace f encIn encOut

Dropping the first symbol of an encoded value.

theorem Turing.MultiTapeTM.ComputableInLogSpace.of_drop {α β : Type} {encIn : α ↪ List Bool} {encOut : β ↪ List Bool} {f : α → β} (k : ℕ) (h : ∀ (a : α), encOut (f a) = List.drop k (encIn a)) : ComputableInLogSpace f encIn encOut

Dropping the first k symbols of an encoded value.

theorem Turing.MultiTapeTM.ComputableInLogSpace.of_take_one {α β : Type} {encIn : α ↪ List Bool} {encOut : β ↪ List Bool} {f : α → β} (h : ∀ (a : α), encOut (f a) = List.take 1 (encIn a)) : ComputableInLogSpace f encIn encOut

Keeping just the first symbol of an encoded value.

theorem Turing.MultiTapeTM.ComputableInLogSpace.of_isEmpty {α : Type} {encIn : α ↪ List Bool} {f : α → Bool} (h : ∀ (a : α), f a = (encIn a).isEmpty) : ComputableInLogSpace f encIn encBool

Testing an encoded value for emptiness.

theorem Turing.MultiTapeTM.ComputableInLogSpace.restrict {α β : Type} {encIn : α ↪ List Bool} {encOut : β ↪ List Bool} {f : α → β} (h : ComputableInLogSpace f encIn encOut) (p : α → Prop) : ComputableInLogSpace (f ∘ Subtype.val) ((Function.Embedding.subtype p).trans encIn) encOut

A function computable in logarithmic space on all inputs is computable in logarithmic space on the inputs satisfying p, by the same machine.

theorem Turing.MultiTapeTM.ComputableInLogSpace.ite_subtype {α β : Type} {encIn : α ↪ List Bool} {encOut : β ↪ List Bool} {encC : Bool ↪ List Bool} {c : α → Bool} {f g : α → β} (hc : ComputableInLogSpace c encIn encC) (hf : ComputableInLogSpace (f ∘ Subtype.val) ((Function.Embedding.subtype fun (x : α) => c x = true).trans encIn) encOut) (hg : ComputableInLogSpace (g ∘ Subtype.val) ((Function.Embedding.subtype fun (x : α) => c x = false).trans encIn) encOut) : ComputableInLogSpace (fun (a : α) => if c a = true then f a else g a) encIn encOut

Case distinctions in logarithmic space, with each branch certified on the inputs where it is taken.

theorem Turing.MultiTapeTM.ComputableInLogSpace.ite {α β : Type} {encIn : α ↪ List Bool} {encOut : β ↪ List Bool} {encC : Bool ↪ List Bool} {c : α → Bool} {f g : α → β} (hc : ComputableInLogSpace c encIn encC) (hf : ComputableInLogSpace f encIn encOut) (hg : ComputableInLogSpace g encIn encOut) : ComputableInLogSpace (fun (a : α) => if c a = true then f a else g a) encIn encOut

Case distinction: if c, f and g are computable in logarithmic space on a common input, so is fun a => if c a then f a else g a.

theorem Turing.MultiTapeTM.ComputableInLogSpace.of_isEmpty_ite {α β : Type} {encIn : α ↪ List Bool} {encOut : β ↪ List Bool} {f : α → β} (d : β) (hd : ∀ (a : α), encIn a = [] → f a = d) (h : ComputableInLogSpace (f ∘ Subtype.val) ((Function.Embedding.subtype fun (a : α) => (encIn a).isEmpty = false).trans encIn) encOut) : ComputableInLogSpace f encIn encOut

A function with a fixed value d on the input encoded by the empty word, and computable in logarithmic space on the other inputs.

theorem Turing.MultiTapeTM.ComputableInLogSpace.append {α β : Type} {encIn : α ↪ List Bool} {encOut : β ↪ List Bool} {β₁ β₂ : Type} {enc₁ : β₁ ↪ List Bool} {enc₂ : β₂ ↪ List Bool} {f₁ : α → β₁} {f₂ : α → β₂} {g : α → β} (h₁ : ComputableInLogSpace f₁ encIn enc₁) (h₂ : ComputableInLogSpace f₂ encIn enc₂) (hg : ∀ (a : α), encOut (g a) = enc₁ (f₁ a) ++ enc₂ (f₂ a)) : ComputableInLogSpace g encIn encOut

Word concatenation: if f₁ and f₂ are computable in logarithmic space on a common input and encOut (g a) = enc₁ (f₁ a) ++ enc₂ (f₂ a) for all a, then g is computable in logarithmic space.

theorem Turing.MultiTapeTM.ComputableInLogSpace.fst {β₁ β₂ : Type} (enc₁ : β₁ ↪ List Bool) (enc₂ : β₂ ↪ List Bool) : ComputableInLogSpace Prod.fst (encPair enc₁ enc₂) enc₁

The first component of a pair.

theorem Turing.MultiTapeTM.ComputableInLogSpace.snd {β₁ β₂ : Type} (enc₁ : β₁ ↪ List Bool) (enc₂ : β₂ ↪ List Bool) : ComputableInLogSpace Prod.snd (encPair enc₁ enc₂) enc₂

The second component of a pair.

theorem Turing.MultiTapeTM.ComputableInLogSpace.pair {α : Type} {encIn : α ↪ List Bool} {β₁ β₂ : Type} {enc₁ : β₁ ↪ List Bool} {enc₂ : β₂ ↪ List Bool} {f₁ : α → β₁} {f₂ : α → β₂} (h₁ : ComputableInLogSpace f₁ encIn enc₁) (h₂ : ComputableInLogSpace f₂ encIn enc₂) : ComputableInLogSpace (fun (a : α) => (f₁ a, f₂ a)) encIn (encPair enc₁ enc₂)

Pairing: the values of two logspace functions of the same input, framed first value followed by the second, are computed in logarithmic space.

Options, framed lists, bit words, and unary numbers

theorem Turing.MultiTapeTM.ComputableInLogSpace.optionSome {β : Type} {encOut : β ↪ List Bool} : ComputableInLogSpace some encOut (encOption encOut)

Wrapping a value in some in logarithmic space.

theorem Turing.MultiTapeTM.ComputableInLogSpace.optionGetD {β : Type} {encOut : β ↪ List Bool} (d : β) : ComputableInLogSpace (fun (o : Option β) => o.getD d) (encOption encOut) encOut

Unwrapping an option with a default value d in logarithmic space.

theorem Turing.MultiTapeTM.ComputableInLogSpace.listSingleton {β : Type} {encOut : β ↪ List Bool} : ComputableInLogSpace (fun (b : β) => [b]) encOut (encList encOut)

Forming a singleton framed list in logarithmic space.

theorem Turing.MultiTapeTM.ComputableInLogSpace.listCons {α β : Type} {encIn : α ↪ List Bool} {encOut : β ↪ List Bool} {f₁ : α → β} {f₂ : α → List β} (h₁ : ComputableInLogSpace f₁ encIn encOut) (h₂ : ComputableInLogSpace f₂ encIn (encList encOut)) : ComputableInLogSpace (fun (a : α) => f₁ a :: f₂ a) encIn (encList encOut)

Prepending a computed element to a computed framed list in logarithmic space.

theorem Turing.MultiTapeTM.ComputableInLogSpace.listAppend {α β : Type} {encIn : α ↪ List Bool} {encOut : β ↪ List Bool} {f₁ f₂ : α → List β} (h₁ : ComputableInLogSpace f₁ encIn (encList encOut)) (h₂ : ComputableInLogSpace f₂ encIn (encList encOut)) : ComputableInLogSpace (fun (a : α) => f₁ a ++ f₂ a) encIn (encList encOut)

Concatenating two framed lists computed in logarithmic space from a common input.

theorem Turing.MultiTapeTM.ComputableInLogSpace.listHeadD {β : Type} {encOut : β ↪ List Bool} (d : β) : ComputableInLogSpace (fun (l : List β) => l.headD d) (encList encOut) encOut

Reading the head of a framed list with a default value d in logarithmic space.

theorem Turing.MultiTapeTM.ComputableInLogSpace.listLength {β : Type} {encOut : β ↪ List Bool} : ComputableInLogSpace (fun (l : List β) => l.length) (encList encOut) encUnary

The length of a framed list, in unary, in logarithmic space.

theorem Turing.MultiTapeTM.ComputableInLogSpace.bitsAppend {α : Type} {encIn : α ↪ List Bool} {f₁ f₂ : α → List Bool} (h₁ : ComputableInLogSpace f₁ encIn encBits) (h₂ : ComputableInLogSpace f₂ encIn encBits) : ComputableInLogSpace (fun (a : α) => f₁ a ++ f₂ a) encIn encBits

Concatenating two bit words computed in logarithmic space from a common input.

theorem Turing.MultiTapeTM.ComputableInLogSpace.bitsHeadD (d : Bool) : ComputableInLogSpace (fun (l : List Bool) => l.headD d) encBits encBool

Reading the head of a bit word with a default value d in logarithmic space.

theorem Turing.MultiTapeTM.ComputableInLogSpace.bitsMap (g : Bool → Bool) : ComputableInLogSpace (List.map g) encBits encBits

Mapping a Boolean function over a bit word is computable in logarithmic space.

theorem Turing.MultiTapeTM.ComputableInLogSpace.of_foldl_bool {α : Type} {encIn : α ↪ List Bool} {Q : Type} [Finite Q] (q₀ : Q) (step : Q → Bool → Q) (out : Q → Bool) {f : α → Bool} (h : ∀ (a : α), f a = out (List.foldl step q₀ (encIn a))) : ComputableInLogSpace f encIn encBool

Folding a finite-state transition function over an encoded word and projecting the final state to a Boolean is computable in logarithmic space.

theorem Turing.MultiTapeTM.ComputableInLogSpace.bitsFoldl (op : Bool → Bool → Bool) (init : Bool) : ComputableInLogSpace (fun (xs : List Bool) => List.foldl op init xs) encBits encBool

Folding a binary Boolean operation over a bit word is computable in logarithmic space.

theorem Turing.MultiTapeTM.ComputableInLogSpace.bitsAll (p : Bool → Bool) : ComputableInLogSpace (fun (xs : List Bool) => xs.all p) encBits encBool

Testing whether all bits of a word satisfy p is computable in logarithmic space.

theorem Turing.MultiTapeTM.ComputableInLogSpace.bitsAny (p : Bool → Bool) : ComputableInLogSpace (fun (xs : List Bool) => xs.any p) encBits encBool

Testing whether any bit of a word satisfies p is computable in logarithmic space.

theorem Turing.MultiTapeTM.ComputableInLogSpace.unaryAdd {α : Type} {encIn : α ↪ List Bool} {f₁ f₂ : α → ℕ} (h₁ : ComputableInLogSpace f₁ encIn encUnary) (h₂ : ComputableInLogSpace f₂ encIn encUnary) : ComputableInLogSpace (fun (a : α) => f₁ a + f₂ a) encIn encUnary

Adding two unary-encoded natural numbers computed in logarithmic space from a common input.

theorem Turing.MultiTapeTM.ComputableInLogSpace.unaryMulConst {α : Type} {encIn : α ↪ List Bool} {f : α → ℕ} (k : ℕ) (hf : ComputableInLogSpace f encIn encUnary) : ComputableInLogSpace (fun (a : α) => f a * k) encIn encUnary

Multiplying a unary-encoded natural number by a fixed constant k in logarithmic space.

theorem Turing.MultiTapeTM.ComputableInLogSpace.unaryLeConst {α : Type} {encIn : α ↪ List Bool} (k : ℕ) {r : α → ℕ} (hr : ComputableInLogSpace r encIn encUnary) : ComputableInLogSpace (fun (a : α) => decide (r a ≤ k)) encIn encBool

Testing whether a unary-encoded natural number is at most a fixed constant k.

theorem Turing.MultiTapeTM.ComputableInLogSpace.unaryBoundedMap {β : Type} {encOut : β ↪ List Bool} (M : ℕ) (g : ℕ → β) : ComputableInLogSpace (fun (n : ℕ) => g (min n M)) encUnary encOut

Evaluating any function g : ℕ → β on a unary input clamped at a fixed constant M is computable in logarithmic space.

Bounded-count batch evaluation

theorem Turing.MultiTapeTM.ComputableInLogSpace.map_range_const {α β : Type} {encIn : α ↪ List Bool} {encOut : β ↪ List Bool} (k : ℕ) {f : α × ℕ → β} (hf : ComputableInLogSpace f (encPair encIn encUnary) encOut) : ComputableInLogSpace (fun (a : α) => List.map (fun (i : ℕ) => f (a, i)) (List.range k)) encIn (encList encOut)

Evaluating a logspace family f : α × ℕ → β at the first k indices 0, …, k - 1, for a fixed constant k, is computable in logarithmic space.

theorem Turing.MultiTapeTM.ComputableInLogSpace.map_range_of_le {α β : Type} {encIn : α ↪ List Bool} {encOut : β ↪ List Bool} (k : ℕ) {r : α → ℕ} {f : α × ℕ → β} (hr : ComputableInLogSpace r encIn encUnary) (hrk : ∀ (a : α), r a ≤ k) (hf : ComputableInLogSpace f (encPair encIn encUnary) encOut) : ComputableInLogSpace (fun (a : α) => List.map (fun (i : ℕ) => f (a, i)) (List.range (r a))) encIn (encList encOut)

Evaluating a logspace family f : α × ℕ → β at indices 0, …, r a - 1, where r : α → ℕ is computable in logarithmic space and bounded by a constant k, is computable in logarithmic space.

theorem Turing.MultiTapeTM.ComputableInLogSpace.mapToBits_range_const {α : Type} {encIn : α ↪ List Bool} (k : ℕ) {f : α × ℕ → Bool} (hf : ComputableInLogSpace f (encPair encIn encUnary) encBool) : ComputableInLogSpace (fun (a : α) => List.map (fun (i : ℕ) => f (a, i)) (List.range k)) encIn encBits

Evaluating a logspace Boolean family f : α × ℕ → Bool at the first k indices 0, …, k - 1, for a fixed constant k, is computable in logarithmic space.

theorem Turing.MultiTapeTM.ComputableInLogSpace.mapToBits_range_of_le {α : Type} {encIn : α ↪ List Bool} (k : ℕ) {r : α → ℕ} {f : α × ℕ → Bool} (hr : ComputableInLogSpace r encIn encUnary) (hrk : ∀ (a : α), r a ≤ k) (hf : ComputableInLogSpace f (encPair encIn encUnary) encBool) : ComputableInLogSpace (fun (a : α) => List.map (fun (i : ℕ) => f (a, i)) (List.range (r a))) encIn encBits

Evaluating a logspace Boolean family f : α × ℕ → Bool at indices 0, …, r a - 1, where r : α → ℕ is computable in logarithmic space and bounded by a constant k, is computable in logarithmic space.

Automation

The closure rules for pairing, projections and case distinctions, and the word operations, are registered with fun_prop. Projections are stated for a computed pair, so the pair certificate fixes the encodings of the components.

theorem Turing.MultiTapeTM.ComputableInLogSpace.fst' {α : Type} {encIn : α ↪ List Bool} {β₁ β₂ : Type} {enc₁ : β₁ ↪ List Bool} {enc₂ : β₂ ↪ List Bool} {f : α → β₁ × β₂} (hf : ComputableInLogSpace f encIn (encPair enc₁ enc₂)) : ComputableInLogSpace (fun (a : α) => (f a).1) encIn enc₁

The first component of a computed pair, in the form used by fun_prop.

theorem Turing.MultiTapeTM.ComputableInLogSpace.snd' {α : Type} {encIn : α ↪ List Bool} {β₁ β₂ : Type} {enc₁ : β₁ ↪ List Bool} {enc₂ : β₂ ↪ List Bool} {f : α → β₁ × β₂} (hf : ComputableInLogSpace f encIn (encPair enc₁ enc₂)) : ComputableInLogSpace (fun (a : α) => (f a).2) encIn enc₂

The second component of a computed pair, in the form used by fun_prop.

theorem Turing.MultiTapeTM.ComputableInLogSpace.bool_and {α : Type} {encIn : α ↪ List Bool} {c₁ c₂ : α → Bool} (h₁ : ComputableInLogSpace c₁ encIn encBool) (h₂ : ComputableInLogSpace c₂ encIn encBool) : ComputableInLogSpace (fun (a : α) => c₁ a && c₂ a) encIn encBool

The conjunction of two computed Booleans.

theorem Turing.MultiTapeTM.ComputableInLogSpace.bool_or {α : Type} {encIn : α ↪ List Bool} {c₁ c₂ : α → Bool} (h₁ : ComputableInLogSpace c₁ encIn encBool) (h₂ : ComputableInLogSpace c₂ encIn encBool) : ComputableInLogSpace (fun (a : α) => c₁ a || c₂ a) encIn encBool

The disjunction of two computed Booleans.

theorem Turing.MultiTapeTM.ComputableInLogSpace.ite_decide {α β : Type} {encIn : α ↪ List Bool} {encOut : β ↪ List Bool} {encC : Bool ↪ List Bool} {p : α → Prop} {x✝ : DecidablePred p} {f g : α → β} (hp : ComputableInLogSpace (fun (a : α) => decide (p a)) encIn encC) (hf : ComputableInLogSpace f encIn encOut) (hg : ComputableInLogSpace g encIn encOut) : ComputableInLogSpace (fun (a : α) => if p a then f a else g a) encIn encOut

A case distinction on a decidable proposition whose truth value is computed.