Basic functions with bounds of given degrees

Functions on unary numbers and integers, in linear time and space, and equality tests, in quadratic time and space.

Main definitions

• Turing.MultiTapeTM.encUnary: natural numbers in unary.
• Turing.MultiTapeTM.encIntUnary: integers in unary, as a sign bit followed by a unary magnitude.

Main results

• Turing.MultiTapeTM.ComputableTidilyInDegree.eq: equality, for any encoding.
• successor, predecessor and zero test in unary, and adding one or subtracting one on unary integers.

Unary numbers

theorem Turing.MultiTapeTM.ComputableTidilyInDegree.unary_succ : ComputableTidilyInDegree (fun (x : ℕ) => x + 1) encUnary encUnary 1 1

theorem Turing.MultiTapeTM.ComputableTidilyInDegree.unary_pred : ComputableTidilyInDegree (fun (x : ℕ) => x - 1) encUnary encUnary 1 1

theorem Turing.MultiTapeTM.ComputableTidilyInDegree.unary_isZero : ComputableTidilyInDegree (fun (n : ℕ) => decide (n = 0)) encUnary encBool 1 1

Integers

def Turing.MultiTapeTM.encIntUnary : ℤ ↪ List Bool

Integers in unary: false followed by n ones for n ≥ 0, and true followed by n ones for -(n + 1). The code of z has z.natAbs + 1 bits when 0 ≤ z and z.natAbs bits when z < 0; Turing.MultiTapeTM.encIntBin is the binary sign-magnitude encoding.

@[simp]

theorem Turing.MultiTapeTM.encIntUnary_ofNat (n : ℕ) : encIntUnary (Int.ofNat n) = false :: List.replicate n true

@[simp]

theorem Turing.MultiTapeTM.encIntUnary_natCast (n : ℕ) : encIntUnary ↑n = false :: List.replicate n true

@[simp]

theorem Turing.MultiTapeTM.encIntUnary_zero : encIntUnary 0 = [false]

@[simp]

theorem Turing.MultiTapeTM.encIntUnary_natCast_add_one (n : ℕ) : encIntUnary (↑n + 1) = false :: true :: List.replicate n true

@[simp]

theorem Turing.MultiTapeTM.encIntUnary_negSucc (n : ℕ) : encIntUnary (Int.negSucc n) = true :: List.replicate n true

theorem Turing.MultiTapeTM.length_encIntUnary (z : ℤ) : (encIntUnary z).length = if z < 0 then (-z).toNat else z.toNat + 1

theorem Turing.MultiTapeTM.length_encIntUnary_add_one_le (z : ℤ) : (encIntUnary (z + 1)).length ≤ (encIntUnary z).length + 1

theorem Turing.MultiTapeTM.length_encIntUnary_sub_one_le (z : ℤ) : (encIntUnary (z - 1)).length ≤ (encIntUnary z).length + 1

theorem Turing.MultiTapeTM.ComputableTidilyInDegree.int_succ : ComputableTidilyInDegree (fun (x : ℤ) => x + 1) encIntUnary encIntUnary 1 1

theorem Turing.MultiTapeTM.ComputableTidilyInDegree.int_pred : ComputableTidilyInDegree (fun (x : ℤ) => x - 1) encIntUnary encIntUnary 1 1

Equality

theorem Turing.MultiTapeTM.ComputableTidilyInDegree.eqWordsStep : ComputableTidilyInDegree (fun (q : (List Bool × Bool) × Bool) => EqWords.step q.1 q.2) (encPair (encPair encBits encBool) encBool) (encPair encBits encBool) 1 1

A step of comparing words.

theorem Turing.MultiTapeTM.ComputableTidilyInDegree.eqWordsResult : ComputableTidilyInDegree (fun (s : List Bool × Bool) => s.2 && s.1.isEmpty) (encPair encBits encBool) encBool 1 0

The result of comparing words, from the state after the last step.

theorem Turing.MultiTapeTM.ComputableTidilyInDegree.eqWords : ComputableTidilyInDegree (fun (p : List Bool × List Bool) => decide (p.1 = p.2)) (encPair encBits encBits) encBool 2 0

Equality of words.

theorem Turing.MultiTapeTM.ComputableTidilyInDegree.eq {α : Type} [DecidableEq α] (enc : α ↪ List Bool) : ComputableTidilyInDegree (fun (p : α × α) => decide (p.1 = p.2)) (encPair enc enc) encBool 2 0

Equality, for any encoding.