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.encInt: integers as a sign 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 integers.

Unary numbers

def Turing.MultiTapeTM.encUnary : ℕ ↪ List Bool

Natural numbers in unary: n is encoded by n ones.

@[simp]

theorem Turing.MultiTapeTM.encUnary_apply (n : ℕ) : encUnary n = List.replicate n true

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.encInt : ℤ ↪ List Bool

Integers: false followed by n in unary for n ≥ 0, and true followed by n in unary for -(n + 1).

@[simp]

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

@[simp]

theorem Turing.MultiTapeTM.encInt_natCast (n : ℕ) : encInt ↑n = false :: List.replicate n true

@[simp]

theorem Turing.MultiTapeTM.encInt_zero : encInt 0 = [false]

@[simp]

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

@[simp]

theorem Turing.MultiTapeTM.encInt_negSucc (n : ℕ) : encInt (Int.negSucc n) = true :: List.replicate n true

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

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

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

Equality

def Turing.MultiTapeTM.EqWords.step (s : List Bool × Bool) (b : Bool) : List Bool × Bool

One step of comparing a word with s.1, the part of the other word still to be matched; s.2 records whether the words agree so far.

theorem Turing.MultiTapeTM.EqWords.foldl_fst (l r : List Bool) (ok : Bool) : (List.foldl step (r, ok) l).1 = List.drop l.length r

theorem Turing.MultiTapeTM.EqWords.foldl_result (l r : List Bool) (ok : Bool) : ((List.foldl step (r, ok) l).2 && (List.foldl step (r, ok) l).1.isEmpty) = (ok && decide (l = r))

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.