Arithmetic on unary numbers, in logarithmic space

Counter programs (Turing.CounterProgram) that read a pair of unary numbers a, b into registers with Turing.CounterProgram.Words.headerCode and evaluate an arithmetic expression (Turing.CounterProgram.Expr) in them. The value is emitted in unary (a counting loop), in binary (a loop over the powers of two up to the value), or compared with the value of a second expression. Because every expression grows at most polynomially in the register values (Turing.CounterProgram.Expr.exists_eval_le_pow), the registers stay polynomially bounded in the input length, so any function given by an expression is computable in logarithmic space by Turing.CounterProgram.computableInLogSpace_of_reachesOut.

The instances are unary multiplication, truncated subtraction, quotient, remainder, minimum and maximum, the comparisons <, ≤ and =, and the conversion from unary to binary, stated for functions computed in logarithmic space from a common input; all but the conversion are registered with fun_prop. Counting the digits of the binary form gives the binary length Nat.size and ⌊log₂⌋ of a unary number, and the length of a bit word in unary is a finite-state transduction.

Main definitions

• Turing.CounterProgram.Unary.unaryProgram, .binaryProgram, .ltProgram: emitting the value of an expression in unary or binary, and comparing the values of two expressions.

Main results

• Turing.CounterProgram.Expr.exists_eval_le_pow: every expression grows at most polynomially in the register values.
• Turing.CounterProgram.Unary.computableInLogSpace_unary, Turing.CounterProgram.Unary.computableInLogSpace_binary: a function of two unary numbers given by an expression, with unary or binary output, in logarithmic space.
• Turing.CounterProgram.Unary.computableInLogSpace_lt: comparing two such functions.
• Turing.MultiTapeTM.ComputableInLogSpace.unaryMul, .unarySub, .unaryDiv, .unaryMod, .unaryMin, .unaryMax, .unaryLt, .unaryLe, .unaryEq, .unaryToBinary: the instances.
• Turing.MultiTapeTM.ComputableInLogSpace.bitsLength, .unarySize, .unaryLog2: lengths and logarithms in unary.

References

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

Programs

def Turing.CounterProgram.Unary.unaryProgram (e : Expr) : CounterProgram

The program emitting the value of e in unary: after the header, label 4 stores the value in register 3, and the counting loop at 5 emits a true for each value of register 2 below it.

def Turing.CounterProgram.Unary.binaryProgram (e : Expr) : CounterProgram

The program emitting the value of e in binary, least significant bit first: after the header, label 4 stores the value v in register 3; register 2 runs over the powers of two p ≤ v, and for each the program emits the bit v / p % 2.

def Turing.CounterProgram.Unary.ltProgram (e₁ e₂ : Expr) : CounterProgram

The program comparing the values of e₁ and e₂: after the header, it accepts if the value of e₁ is less than that of e₂, and rejects otherwise.

Runs

theorem Turing.CounterProgram.Expr.exists_eval_le_pow (e : Expr) : ∃ (d : ℕ), ∀ {regs : List ℕ} {m : ℕ}, 2 ≤ m → (∀ x ∈ regs, x ≤ m) → eval regs e ≤ m ^ d

Every counter-program expression grows at most polynomially in a bound m ≥ 2 on the register values.

Logarithmic space

theorem Turing.CounterProgram.Unary.computableInLogSpace_unary {F : ℕ → ℕ → ℕ} (e : Expr) (he : ∀ (a b : ℕ), Expr.eval [a, b, 0, 0] e = F a b) : MultiTapeTM.ComputableInLogSpace (fun (p : ℕ × ℕ) => F p.1 p.2) (MultiTapeTM.encPair MultiTapeTM.encUnary MultiTapeTM.encUnary) MultiTapeTM.encUnary

A function of two unary numbers given by an expression, with unary output, is computable in logarithmic space. The expression e is evaluated with a in register 0, b in register 1, and the other registers zero.

theorem Turing.CounterProgram.Unary.computableInLogSpace_binary {F : ℕ → ℕ → ℕ} (e : Expr) (he : ∀ (a b : ℕ), Expr.eval [a, b, 0, 0] e = F a b) : MultiTapeTM.ComputableInLogSpace (fun (p : ℕ × ℕ) => F p.1 p.2) (MultiTapeTM.encPair MultiTapeTM.encUnary MultiTapeTM.encUnary) MultiTapeTM.encNat

A function of two unary numbers given by an expression, with binary output, is computable in logarithmic space. The expression e is evaluated with a in register 0, b in register 1, and the other registers zero.

theorem Turing.CounterProgram.Unary.computableInLogSpace_lt {F₁ F₂ : ℕ → ℕ → ℕ} (e₁ e₂ : Expr) (h₁ : ∀ (a b : ℕ), Expr.eval [a, b, 0, 0] e₁ = F₁ a b) (h₂ : ∀ (a b : ℕ), Expr.eval [a, b, 0, 0] e₂ = F₂ a b) : MultiTapeTM.ComputableInLogSpace (fun (p : ℕ × ℕ) => decide (F₁ p.1 p.2 < F₂ p.1 p.2)) (MultiTapeTM.encPair MultiTapeTM.encUnary MultiTapeTM.encUnary) MultiTapeTM.encBool

Comparing two functions of two unary numbers given by expressions is computable in logarithmic space.

Instances

theorem Turing.MultiTapeTM.ComputableInLogSpace.unaryMul {γ : 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

Multiplying unary numbers computed in logarithmic space from a common input.

theorem Turing.MultiTapeTM.ComputableInLogSpace.unarySub {γ : 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

Truncated subtraction of unary numbers computed in logarithmic space from a common input.

theorem Turing.MultiTapeTM.ComputableInLogSpace.unaryDiv {γ : 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

The quotient of unary numbers computed in logarithmic space from a common input.

theorem Turing.MultiTapeTM.ComputableInLogSpace.unaryMod {γ : 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

The remainder of unary numbers computed in logarithmic space from a common input.

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

The minimum of unary numbers computed in logarithmic space from a common input.

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

The maximum of unary numbers computed in logarithmic space from a common input.

theorem Turing.MultiTapeTM.ComputableInLogSpace.unaryLt {γ : Type} {encIn : γ ↪ List Bool} {f₁ f₂ : γ → ℕ} (h₁ : ComputableInLogSpace f₁ encIn encUnary) (h₂ : ComputableInLogSpace f₂ encIn encUnary) : ComputableInLogSpace (fun (a : γ) => decide (f₁ a < f₂ a)) encIn encBool

Comparing unary numbers with <, computed in logarithmic space from a common input.

theorem Turing.MultiTapeTM.ComputableInLogSpace.unaryLe {γ : Type} {encIn : γ ↪ List Bool} {f₁ f₂ : γ → ℕ} (h₁ : ComputableInLogSpace f₁ encIn encUnary) (h₂ : ComputableInLogSpace f₂ encIn encUnary) : ComputableInLogSpace (fun (a : γ) => decide (f₁ a ≤ f₂ a)) encIn encBool

Comparing unary numbers with ≤, computed in logarithmic space from a common input.

theorem Turing.MultiTapeTM.ComputableInLogSpace.unaryEq {γ : Type} {encIn : γ ↪ List Bool} {f₁ f₂ : γ → ℕ} (h₁ : ComputableInLogSpace f₁ encIn encUnary) (h₂ : ComputableInLogSpace f₂ encIn encUnary) : ComputableInLogSpace (fun (a : γ) => decide (f₁ a = f₂ a)) encIn encBool

Testing unary numbers for equality, computed in logarithmic space from a common input.

theorem Turing.MultiTapeTM.ComputableInLogSpace.unaryToBinary {γ : Type} {encIn : γ ↪ List Bool} {f : γ → ℕ} (hf : ComputableInLogSpace f encIn encUnary) : ComputableInLogSpace f encIn encNat

Converting a unary number to binary, computed in logarithmic space. It changes only the output encoding, so it is not registered with fun_prop.

theorem Turing.MultiTapeTM.ComputableInLogSpace.bitsLength : ComputableInLogSpace List.length encBits encUnary

The length of a bit word, in unary, by a finite-state transducer that replaces every bit by true.

theorem Turing.MultiTapeTM.ComputableInLogSpace.unarySize {γ : Type} {encIn : γ ↪ List Bool} {f : γ → ℕ} (hf : ComputableInLogSpace f encIn encUnary) : ComputableInLogSpace (fun (a : γ) => (f a).size) encIn encUnary

The binary length of a unary number, in unary: convert it to binary and count the digits.

theorem Turing.MultiTapeTM.ComputableInLogSpace.unaryLog2 {γ : Type} {encIn : γ ↪ List Bool} {f : γ → ℕ} (hf : ComputableInLogSpace f encIn encUnary) : ComputableInLogSpace (fun (a : γ) => (f a).log2) encIn encUnary

⌊log₂⌋ of a unary number, in unary: one less than its binary length.