Sparse unbounded TM configurations in RAM registers

This layout is independent of an input-length or time bound. State, heads, and scratch occupy a fixed prefix determined only by the machine's tape count. Tape cells are interleaved after that prefix at cellBase + position * (n + 2) + tape. A fixed RAM program can therefore compute every cell address using multiplication and addition while allocating new tape positions on demand.

@[reducible, inline]

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

State field followed by every named head and every named tape cell.

Equations

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

def Complexity.RAM.TMConfig.Sparse.stateReg : ℕ

State register.

Equations

• Complexity.RAM.TMConfig.Sparse.stateReg = 0

def Complexity.RAM.TMConfig.Sparse.headReg {n : ℕ} (tape : Fin (n + 2)) : ℕ

Fixed head register for one named tape.

Equations

• Complexity.RAM.TMConfig.Sparse.headReg tape = 1 + ↑tape

def Complexity.RAM.TMConfig.Sparse.zeroReg (n : ℕ) : ℕ

Constant-zero scratch register.

Equations

• Complexity.RAM.TMConfig.Sparse.zeroReg n = n + 3

def Complexity.RAM.TMConfig.Sparse.oneReg (n : ℕ) : ℕ

Constant-one scratch register.

Equations

• Complexity.RAM.TMConfig.Sparse.oneReg n = n + 4

def Complexity.RAM.TMConfig.Sparse.tapeCountReg (n : ℕ) : ℕ

Constant n + 2, used to compute interleaved cell addresses.

Equations

• Complexity.RAM.TMConfig.Sparse.tapeCountReg n = n + 5

def Complexity.RAM.TMConfig.Sparse.stateScratchReg (n : ℕ) : ℕ

Destructive finite-state dispatch register.

Equations

• Complexity.RAM.TMConfig.Sparse.stateScratchReg n = n + 6

def Complexity.RAM.TMConfig.Sparse.addressReg (n : ℕ) : ℕ

Indirect cell-address scratch register.

Equations

• Complexity.RAM.TMConfig.Sparse.addressReg n = n + 7

def Complexity.RAM.TMConfig.Sparse.valueReg (n : ℕ) : ℕ

Writable-symbol scratch register.

Equations

• Complexity.RAM.TMConfig.Sparse.valueReg n = n + 8

def Complexity.RAM.TMConfig.Sparse.symbolReg (n : ℕ) (tape : Fin (n + 2)) : ℕ

Loaded head-symbol register for one named tape.

Equations

• Complexity.RAM.TMConfig.Sparse.symbolReg n tape = n + 9 + ↑tape

def Complexity.RAM.TMConfig.Sparse.cellBase (n : ℕ) : ℕ

Exclusive end of the fixed control/scratch prefix and first tape-cell register.

Equations

• Complexity.RAM.TMConfig.Sparse.cellBase n = 2 * n + 11

def Complexity.RAM.TMConfig.Sparse.cellReg (n : ℕ) (tape : Fin (n + 2)) (position : ℕ) : ℕ

Address of one tape cell in the fixed interleaved layout.

Equations

• Complexity.RAM.TMConfig.Sparse.cellReg n tape position = Complexity.RAM.TMConfig.Sparse.cellBase n + position * (n + 2) + ↑tape

def Complexity.RAM.TMConfig.Sparse.fieldReg {n : ℕ} : Field n → ℕ

Concrete address of a sparse configuration field.

Equations

• Complexity.RAM.TMConfig.Sparse.fieldReg (Sum.inl val) = Complexity.RAM.TMConfig.Sparse.stateReg
• Complexity.RAM.TMConfig.Sparse.fieldReg (Sum.inr (Sum.inl tape)) = Complexity.RAM.TMConfig.Sparse.headReg tape
• Complexity.RAM.TMConfig.Sparse.fieldReg (Sum.inr (Sum.inr (tape, position))) = Complexity.RAM.TMConfig.Sparse.cellReg n tape position

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

Semantic value of one sparse configuration field.

Equations

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

def Complexity.RAM.TMConfig.Sparse.Represents {n : ℕ} (tm : TM n) (cfg : Complexity.Cfg n tm.Q) (store : Structured.Store) : Prop

A store represents the complete unbounded TM configuration. Scratch registers in the fixed gap are deliberately unconstrained.

Equations

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

def Complexity.RAM.TMConfig.Sparse.decodeCellTape (n reg : ℕ) : Fin (n + 2)

Decode the tape slot of an interleaved cell register.

Equations

• Complexity.RAM.TMConfig.Sparse.decodeCellTape n reg = ⟨(reg - Complexity.RAM.TMConfig.Sparse.cellBase n) % (n + 2), ⋯⟩

def Complexity.RAM.TMConfig.Sparse.decodeCellPosition (n reg : ℕ) : ℕ

Decode the position of an interleaved cell register.

Equations

• Complexity.RAM.TMConfig.Sparse.decodeCellPosition n reg = (reg - Complexity.RAM.TMConfig.Sparse.cellBase n) / (n + 2)

noncomputable def Complexity.RAM.TMConfig.Sparse.encodeRegs {n : ℕ} (tm : TM n) (cfg : Complexity.Cfg n tm.Q) : Structured.Store

Canonical sparse register encoding.

Equations

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

noncomputable def Complexity.RAM.TMConfig.Sparse.decodeTape (n : ℕ) (store : Structured.Store) (tape : Fin (n + 2)) : Tape

Decode one complete sparse tape.

Equations

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

noncomputable def Complexity.RAM.TMConfig.Sparse.decode {n : ℕ} (tm : TM n) (store : Structured.Store) : Complexity.Cfg n tm.Q

Decode a complete sparse store into a TM configuration.

Equations

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