Raw syntax for coded multi-input Turing machines

First-order, serializable machine descriptions: plain data with no embedded functions, no well-formedness requirements, and derivable decidable equality. A RawCode i describes a multi-input machine (MIPRE.TM.MultiInput.Deterministic) with i input tapes through a dense transition table: one RawAction per observation (state, input symbols, work symbols), stored in the canonical order fixed by Turing.transitionIndex (MIPRE.TM.Code.Observation).

Well-formedness is a separate predicate (MIPRE.TM.Code.WellFormed), and only well-formed codes are interpreted as machines (MIPRE.TM.Code.Semantics). This "machine code first" layering is what later makes descriptions serializable, measurable (|𝒟|) and usable for self-reference; see planning/tm-infrastructure.md (Milestone B).

Input/output conventions

• The alphabet of a coded machine is Fin alphabetSize with alphabetSize ≥ 2 (enforced by well-formedness). Symbols 0 and 1 are reserved for binary input and output; symbols ≥ 2 may be used freely on the work tapes.
• A transition's output field is an Option Bool, not an optional symbol: coded machines emit bits, so decoding their output is total, while the internal alphabet may be larger.
• States are Fin stateCount; nextState = none halts the machine.

inductive Turing.Move : Type

A head movement of a coded machine.

• left : Move

  Move the head one cell to the left.

• stay : Move

  Do not move the head.

• right : Move

  Move the head one cell to the right.

@[instance_reducible]

instance Turing.instDecidableEqMove : DecidableEq Move

Equations

• Turing.instDecidableEqMove x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Turing.instReprMove.repr : Move → ℕ → Std.Format

Equations

• Turing.instReprMove.repr Turing.Move.left prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Turing.Move.left")).group prec✝
• Turing.instReprMove.repr Turing.Move.stay prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Turing.Move.stay")).group prec✝
• Turing.instReprMove.repr Turing.Move.right prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Turing.Move.right")).group prec✝

@[instance_reducible]

instance Turing.instReprMove : Repr Move

Equations

• Turing.instReprMove = { reprPrec := Turing.instReprMove.repr }

def Turing.Move.toSignType : Move → SignType

Interpret a Move as the SignType movement used by the operational model.

Equations

• Turing.Move.left.toSignType = SignType.neg
• Turing.Move.stay.toSignType = SignType.zero
• Turing.Move.right.toSignType = SignType.pos

inductive Turing.RawWrite : Type

What a coded machine writes on a work tape in one step: nothing (keep), the blank symbol (blank), or the alphabet symbol a (symbol a; well-formedness bounds a by the alphabet size).

• keep : RawWrite

  Leave the cell unchanged.

• blank : RawWrite

  Write the blank symbol.

• symbol (a : ℕ) : RawWrite

  Write the alphabet symbol a.

def Turing.instDecidableEqRawWrite.decEq (x✝ x✝¹ : RawWrite) : Decidable (x✝ = x✝¹)

Equations

• Turing.instDecidableEqRawWrite.decEq Turing.RawWrite.keep Turing.RawWrite.keep = isTrue ⋯
• Turing.instDecidableEqRawWrite.decEq Turing.RawWrite.keep Turing.RawWrite.blank = isFalse Turing.instDecidableEqRawWrite.decEq._proof_1
• Turing.instDecidableEqRawWrite.decEq Turing.RawWrite.keep (Turing.RawWrite.symbol a) = isFalse ⋯
• Turing.instDecidableEqRawWrite.decEq Turing.RawWrite.blank Turing.RawWrite.keep = isFalse Turing.instDecidableEqRawWrite.decEq._proof_3
• Turing.instDecidableEqRawWrite.decEq Turing.RawWrite.blank Turing.RawWrite.blank = isTrue ⋯
• Turing.instDecidableEqRawWrite.decEq Turing.RawWrite.blank (Turing.RawWrite.symbol a) = isFalse ⋯
• Turing.instDecidableEqRawWrite.decEq (Turing.RawWrite.symbol a) Turing.RawWrite.keep = isFalse ⋯
• Turing.instDecidableEqRawWrite.decEq (Turing.RawWrite.symbol a) Turing.RawWrite.blank = isFalse ⋯
• Turing.instDecidableEqRawWrite.decEq (Turing.RawWrite.symbol a) (Turing.RawWrite.symbol b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Turing.instDecidableEqRawWrite : DecidableEq RawWrite

Equations

• Turing.instDecidableEqRawWrite = Turing.instDecidableEqRawWrite.decEq

def Turing.instReprRawWrite.repr : RawWrite → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Turing.instReprRawWrite.repr Turing.RawWrite.keep prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Turing.RawWrite.keep")).group prec✝
• Turing.instReprRawWrite.repr Turing.RawWrite.blank prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Turing.RawWrite.blank")).group prec✝

@[instance_reducible]

instance Turing.instReprRawWrite : Repr RawWrite

Equations

• Turing.instReprRawWrite = { reprPrec := Turing.instReprRawWrite.repr }

structure Turing.RawWorkAction : Type

The action of a coded machine on one work tape: what to write, and how to move.

• write : RawWrite

  What to write on the cell under the head.

• move : Move

  How to move the head.

@[instance_reducible]

instance Turing.instDecidableEqRawWorkAction : DecidableEq RawWorkAction

Equations

• Turing.instDecidableEqRawWorkAction = Turing.instDecidableEqRawWorkAction.decEq

def Turing.instDecidableEqRawWorkAction.decEq (x✝ x✝¹ : RawWorkAction) : Decidable (x✝ = x✝¹)

Equations

• Turing.instDecidableEqRawWorkAction.decEq { write := a, move := a_1 } { write := b, move := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

def Turing.instReprRawWorkAction.repr : RawWorkAction → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Turing.instReprRawWorkAction : Repr RawWorkAction

Equations

• Turing.instReprRawWorkAction = { reprPrec := Turing.instReprRawWorkAction.repr }

structure Turing.RawAction : Type

One entry of a transition table: the action taken on one observation. The arity and work-tape count are not parameters of this type — well-formedness constrains inputMoves.size and workActions.size (see planning/tm-infrastructure.md, decision D2).

• inputMoves : Array Move

  The movement of each input head, in ascending tape order.

• workActions : Array RawWorkAction

  The action on each work tape, in ascending tape order.

• output : Option Bool

  The optionally emitted output bit.

• nextState : Option ℕ

  The successor state, or none to halt.

@[instance_reducible]

instance Turing.instDecidableEqRawAction : DecidableEq RawAction

Equations

• Turing.instDecidableEqRawAction = Turing.instDecidableEqRawAction.decEq

def Turing.instDecidableEqRawAction.decEq (x✝ x✝¹ : RawAction) : Decidable (x✝ = x✝¹)

Equations

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

def Turing.instReprRawAction.repr : RawAction → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Turing.instReprRawAction : Repr RawAction

Equations

• Turing.instReprRawAction = { reprPrec := Turing.instReprRawAction.repr }

structure Turing.RawCode (i : ℕ) : Type

A raw description of an i-input machine: header data and a dense transition table in the canonical observation order (Turing.transitionIndex). No well-formedness is imposed here; see RawCode.WellFormed.

• workTapeCount : ℕ

  The number of work tapes.

• alphabetSize : ℕ

  The alphabet size (well-formedness requires ≥ 2; symbols 0/1 are the I/O bits).

• stateCount : ℕ

  The number of states.

• startState : ℕ

  The initial state (well-formedness requires it to be < stateCount).

• table : Array RawAction

  The dense transition table: entry transitionIndex q as bs is the action taken on observation (q, as, bs). Well-formedness requires size stateCount * (alphabetSize + 1) ^ (i + workTapeCount).

@[instance_reducible]

instance Turing.instDecidableEqRawCode {i✝ : ℕ} : DecidableEq (RawCode i✝)

Equations

• Turing.instDecidableEqRawCode = Turing.instDecidableEqRawCode.decEq

def Turing.instDecidableEqRawCode.decEq {i✝ : ℕ} (x✝ x✝¹ : RawCode i✝) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Turing.instReprRawCode {i✝ : ℕ} : Repr (RawCode i✝)

Equations

• Turing.instReprRawCode = { reprPrec := Turing.instReprRawCode.repr }

def Turing.instReprRawCode.repr {i✝ : ℕ} : RawCode i✝ → ℕ → Std.Format

Equations

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