Ternary registers for binary work tapes

A normalized StackTape Bool is a base-three natural number, with the cell nearest the head as its least significant digit. Blank is zero, false is one, and true is two. Normalization of the stored tail is essential: appending a blank at the far end does not change the code. The arithmetic push, pop and observation operations below agree with StackTape operations.

Main definitions

• Turing.MultiTapeNTM.ConfigurationGraph.symbolCode: ternary code for a cell.
• Turing.MultiTapeNTM.ConfigurationGraph.stackCode: ternary code for a normalized stack.

Main results

• Turing.MultiTapeNTM.ConfigurationGraph.stackCode_cons: push is multiplication by three.
• Turing.MultiTapeNTM.ConfigurationGraph.stackCode_head: observation is remainder by three.
• Turing.MultiTapeNTM.ConfigurationGraph.stackCode_tail: pop is division by three.
• Turing.MultiTapeNTM.ConfigurationGraph.stackCode_lt: the code fits exponentially in length.

References

Uses Bolton Bailey's normalized StackTape and BiTape APIs.

def Turing.MultiTapeNTM.ConfigurationGraph.symbolCode : Option Bool → ℕ

Blank, false and true are the ternary digits zero, one and two.

theorem Turing.MultiTapeNTM.ConfigurationGraph.symbolCode_lt (b : Option Bool) : symbolCode b < 3

theorem Turing.MultiTapeNTM.ConfigurationGraph.symbolCode_injective : Function.Injective symbolCode

def Turing.MultiTapeNTM.ConfigurationGraph.cellsCode : List (Option Bool) → ℕ

Little-endian base-three evaluation of a finite cell list.

def Turing.MultiTapeNTM.ConfigurationGraph.stackCode (t : Cslib.Turing.StackTape Bool) : ℕ

The ternary code of a normalized stack.

@[simp]

theorem Turing.MultiTapeNTM.ConfigurationGraph.stackCode_nil : stackCode Cslib.Turing.StackTape.nil = 0

theorem Turing.MultiTapeNTM.ConfigurationGraph.stackCode_cons (b : Option Bool) (t : Cslib.Turing.StackTape Bool) : stackCode (Cslib.Turing.StackTape.cons b t) = symbolCode b + 3 * stackCode t

The normalizing push still has the usual base-three arithmetic meaning.

theorem Turing.MultiTapeNTM.ConfigurationGraph.stackCode_head (t : Cslib.Turing.StackTape Bool) : symbolCode t.head = stackCode t % 3

The digit under the stack head is its least significant ternary digit.

theorem Turing.MultiTapeNTM.ConfigurationGraph.stackCode_tail (t : Cslib.Turing.StackTape Bool) : stackCode t.tail = stackCode t / 3

Removing the head divides the stack register by three.

theorem Turing.MultiTapeNTM.ConfigurationGraph.cellsCode_lt (l : List (Option Bool)) : cellsCode l < 3 ^ l.length

A stack with l stored cells has a ternary code smaller than 3^l.

theorem Turing.MultiTapeNTM.ConfigurationGraph.stackCode_lt (t : Cslib.Turing.StackTape Bool) : stackCode t < 3 ^ t.length

def Turing.MultiTapeNTM.ConfigurationGraph.tapeCode (t : Cslib.Turing.BiTape Bool) : ℕ × ℕ × ℕ

The registers of a bidirectional tape, in head/left/right order.

def Turing.MultiTapeNTM.ConfigurationGraph.tapeStep (a : Option (Option Bool) × SignType) (t : ℕ × ℕ × ℕ) : ℕ × ℕ × ℕ

Execute an optional write and a signed move on the three tape registers.

theorem Turing.MultiTapeNTM.ConfigurationGraph.tapeCode_step (t : Cslib.Turing.BiTape Bool) (a : Option (Option Bool) × SignType) : tapeCode (t.step a) = tapeStep a (tapeCode t)

Arithmetic tape instructions agree with the native finite tape action.