Bounded Turing-machine configurations in RAM registers

This file fixes the register representation used by the Turing-machine to RAM simulation. Register zero stores the finite-state code, the next n + 2 registers store the input/work/output head positions, and the remaining registers store a dense bounded window of every named tape.

Blank symbols use code zero. Consequently registers outside the representation and blank cells inside it agree with the RAM's finite-support convention.

@[reducible, inline]

abbrev Complexity.RAM.TMConfig.Field (n bound : ℕ) : Type

A field in a bounded configuration: state, a named tape head, or a named tape cell. Named tapes use input/work/output indices 0, 1..n, n+1.

Equations

• Complexity.RAM.TMConfig.Field n bound = (Fin 1 ⊕ Fin (n + 2) ⊕ Fin (n + 2) × Fin (bound + 1))

def Complexity.RAM.TMConfig.registerCount (n bound : ℕ) : ℕ

Number of registers occupied by a configuration with cells 0..bound.

Equations

• Complexity.RAM.TMConfig.registerCount n bound = 1 + (n + 2 + (n + 2) * (bound + 1))

noncomputable def Complexity.RAM.TMConfig.fieldEquiv (n bound : ℕ) : Field n bound ≃ Fin (registerCount n bound)

Explicit contiguous ordering of all fields in the bounded representation.

Equations

• Complexity.RAM.TMConfig.fieldEquiv n bound = ((Equiv.refl (Fin 1)).sumCongr (((Equiv.refl (Fin (n + 2))).sumCongr finProdFinEquiv).trans finSumFinEquiv)).trans finSumFinEquiv

def Complexity.RAM.TMConfig.stateField {n bound : ℕ} : Field n bound

The field holding the Turing-machine state.

Equations

• Complexity.RAM.TMConfig.stateField = Sum.inl ⟨0, Complexity.RAM.TMConfig.stateField._proof_2⟩

def Complexity.RAM.TMConfig.headField {n bound : ℕ} (tape : Fin (n + 2)) : Field n bound

The field holding one named tape's head position.

Equations

• Complexity.RAM.TMConfig.headField tape = Sum.inr (Sum.inl tape)

def Complexity.RAM.TMConfig.cellField {n bound : ℕ} (tape : Fin (n + 2)) (position : Fin (bound + 1)) : Field n bound

The field holding one cell of one named tape.

Equations

• Complexity.RAM.TMConfig.cellField tape position = Sum.inr (Sum.inr (tape, position))

noncomputable def Complexity.RAM.TMConfig.fieldReg {n bound : ℕ} (field : Field n bound) : ℕ

Concrete register address of a bounded-configuration field.

Equations

• Complexity.RAM.TMConfig.fieldReg field = ↑((Complexity.RAM.TMConfig.fieldEquiv n bound) field)

def Complexity.RAM.TMConfig.symbolCode : Γ → ℕ

Code the tape alphabet with blank represented by zero.

Equations

• Complexity.RAM.TMConfig.symbolCode Complexity.Γ.blank = 0
• Complexity.RAM.TMConfig.symbolCode Complexity.Γ.zero = 1
• Complexity.RAM.TMConfig.symbolCode Complexity.Γ.one = 2
• Complexity.RAM.TMConfig.symbolCode Complexity.Γ.start = 3

def Complexity.RAM.TMConfig.symbolDecode : ℕ → Γ

Decode a RAM word as a tape symbol; invalid words decode to blank.

Equations

• Complexity.RAM.TMConfig.symbolDecode 1 = Complexity.Γ.zero
• Complexity.RAM.TMConfig.symbolDecode 2 = Complexity.Γ.one
• Complexity.RAM.TMConfig.symbolDecode 3 = Complexity.Γ.start
• Complexity.RAM.TMConfig.symbolDecode x✝ = Complexity.Γ.blank

noncomputable def Complexity.RAM.TMConfig.stateCode {n : ℕ} (tm : TM n) (state : tm.Q) : ℕ

Canonical numeric code of a finite Turing-machine state.

Equations

• Complexity.RAM.TMConfig.stateCode tm state = ↑((Fintype.equivFin tm.Q) state)

noncomputable def Complexity.RAM.TMConfig.stateDecode {n : ℕ} (tm : TM n) (code : ℕ) : tm.Q

Decode a valid state code, using the start state as the default for an invalid RAM word.

Equations

• Complexity.RAM.TMConfig.stateDecode tm code = if h : code < Fintype.card tm.Q then (Fintype.equivFin tm.Q).symm ⟨code, h⟩ else tm.qstart

def Complexity.RAM.TMConfig.tapeAt {n : ℕ} {Q : Type} (cfg : Complexity.Cfg n Q) (tape : Fin (n + 2)) : Tape

Select a named tape by its input/work/output index.

Equations

• Complexity.RAM.TMConfig.tapeAt cfg tape = if hinput : ↑tape = 0 then cfg.input else if houtput : ↑tape = n + 1 then cfg.output else cfg.work ⟨↑tape - 1, ⋯⟩

def Complexity.RAM.TMConfig.TapeBounded (tape : Tape) (bound : ℕ) : Prop

A tape is contained in the encoded window when every later cell is blank.

Equations

• Complexity.RAM.TMConfig.TapeBounded tape bound = ∀ (position : ℕ), bound < position → tape.cells position = Complexity.Γ.blank

def Complexity.RAM.TMConfig.Bounded {n : ℕ} {Q : Type} (cfg : Complexity.Cfg n Q) (bound : ℕ) : Prop

Every named tape in a configuration is contained in the encoded window.

Equations

• Complexity.RAM.TMConfig.Bounded cfg bound = ∀ (tape : Fin (n + 2)), Complexity.RAM.TMConfig.TapeBounded (Complexity.RAM.TMConfig.tapeAt cfg tape) bound

def Complexity.RAM.TMConfig.HeadsBounded {n : ℕ} {Q : Type} (cfg : Complexity.Cfg n Q) (bound : ℕ) : Prop

Every named head lies inside the encoded cell window.

Equations

• Complexity.RAM.TMConfig.HeadsBounded cfg bound = ∀ (tape : Fin (n + 2)), (Complexity.RAM.TMConfig.tapeAt cfg tape).head ≤ bound

def Complexity.RAM.TMConfig.WithinWindow {n : ℕ} {Q : Type} (cfg : Complexity.Cfg n Q) (bound : ℕ) : Prop

A configuration can be stepped inside a bounded representation when both its nonblank cells and every named head lie in the represented window.

Equations

• Complexity.RAM.TMConfig.WithinWindow cfg bound = (Complexity.RAM.TMConfig.Bounded cfg bound ∧ Complexity.RAM.TMConfig.HeadsBounded cfg bound)

noncomputable def Complexity.RAM.TMConfig.fieldValue {n : ℕ} (tm : TM n) (bound : ℕ) (cfg : Complexity.Cfg n tm.Q) : Field n bound → ℕ

Natural-number value stored for one representation field.

Equations

• Complexity.RAM.TMConfig.fieldValue tm bound cfg (Sum.inl val) = Complexity.RAM.TMConfig.stateCode tm cfg.state
• Complexity.RAM.TMConfig.fieldValue tm bound cfg (Sum.inr (Sum.inl tape)) = (Complexity.RAM.TMConfig.tapeAt cfg tape).head
• Complexity.RAM.TMConfig.fieldValue tm bound cfg (Sum.inr (Sum.inr (tape, position))) = Complexity.RAM.TMConfig.symbolCode ((Complexity.RAM.TMConfig.tapeAt cfg tape).cells ↑position)

noncomputable def Complexity.RAM.TMConfig.encodeRegs {n : ℕ} (tm : TM n) (bound : ℕ) (cfg : Complexity.Cfg n tm.Q) : ℕ → ℕ

Register store containing a bounded Turing-machine configuration.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.RAM.TMConfig.Represents {n : ℕ} (tm : TM n) (bound : ℕ) (cfg : Complexity.Cfg n tm.Q) (regs : ℕ → ℕ) : Prop

A RAM store represents a bounded TM configuration when every state/head/cell field has its prescribed value. Scratch registers outside this interface are deliberately unconstrained, allowing successive simulation blocks to compose.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Complexity.RAM.TMConfig.encode {n : ℕ} (tm : TM n) (bound : ℕ) (cfg : Complexity.Cfg n tm.Q) : Cfg

RAM configuration positioned at the beginning of a simulation block.

Equations

• Complexity.RAM.TMConfig.encode tm bound cfg = { pc := 0, regs := Complexity.RAM.TMConfig.encodeRegs tm bound cfg }

noncomputable def Complexity.RAM.TMConfig.decodeTape {n : ℕ} (bound : ℕ) (regs : ℕ → ℕ) (tape : Fin (n + 2)) : Tape

Decode one tape from its head register and bounded cell block.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Complexity.RAM.TMConfig.decode {n : ℕ} (tm : TM n) (bound : ℕ) (regs : ℕ → ℕ) : Complexity.Cfg n tm.Q

Decode a bounded register layout into a Turing-machine configuration.

Equations

• One or more equations did not get rendered due to their size.