Interpretation of machine codes

Code.toTM interprets a well-formed machine code as an operational multi-input Turing machine (MIPRE.TM.MultiInput.Deterministic) over the alphabet Fin alphabetSize and state set Fin stateCount: the transition function looks up the dense table at the canonical position (Code.actionAt) and converts the raw entry into a transition output (Code.interpretAction), with every range fact supplied by well-formedness through the Code.actionAt_* lemmas. Code.toTM_tr records that this is definitional.

The machine code is the primary object and toTM its interpretation — never the other way around. Everything here is executable: no Fintype.elems, no choice, no noncomputable (planning/tm-infrastructure.md, decision D5 and Milestone B).

Bit-level input/output: coded machines read and write the reserved symbols 0/1 (Code.bitEmbedding, Code.bitInputs); every symbol they emit is one of the two bit symbols (Code.outputSymbol_isBit), so decoding outputs as bit strings (Code.decodeBitOutput) is total and faithful (Code.decodeBitOutput_map_bitEmbedding).

@[reducible, inline]

abbrev Turing.Code.Symbol {i : ℕ} (c : Code i) : Type

The alphabet of a coded machine.

Equations

• c.Symbol = Fin c.alphabetSize

@[reducible, inline]

abbrev Turing.Code.State {i : ℕ} (c : Code i) : Type

The state set of a coded machine.

Equations

• c.State = Fin c.stateCount

def Turing.Code.bitEmbedding {i : ℕ} (c : Code i) : Bool ↪ c.Symbol

The two reserved I/O symbols of a coded machine: false ↦ 0, true ↦ 1 (the alphabet has size at least two by well-formedness).

Equations

• c.bitEmbedding = { toFun := fun (b : Bool) => ⟨if b = true then 1 else 0, ⋯⟩, inj' := ⋯ }

def Turing.Code.bitInputs {i : ℕ} (c : Code i) (x : Fin i → List Bool) : Fin i → List c.Symbol

Present a tuple of bit strings as input strings over the machine alphabet.

Equations

• c.bitInputs x j = List.map (fun (b : Bool) => c.bitEmbedding b) (x j)

def Turing.Code.interpretAction {i : ℕ} (c : Code i) (a : RawAction) (hmoves : a.inputMoves.size = i) (hworks : a.workActions.size = c.workTapeCount) (hwrite : ∀ wa ∈ a.workActions, ∀ (s : ℕ), wa.write = RawWrite.symbol s → s < c.alphabetSize) (hnext : ∀ q' ∈ a.nextState, q' < c.stateCount) : MultiInputTM.TransitionOut i c.workTapeCount c.Symbol c.State

Interpret one table entry as a transition output, given the well-formedness facts for that entry: input moves and work actions are read off positionally, written symbols and successor states are cast into Fin using their range facts, and the output bit is embedded as a reserved I/O symbol.

Equations

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

def Turing.Code.toTM {i : ℕ} (c : Code i) : MultiInputTM i c.workTapeCount c.Symbol c.State

The operational machine denoted by a code: start in the coded start state, and transition by looking up the dense table at the canonical position.

Equations

• c.toTM = { q₀ := ⟨c.startState, ⋯⟩, tr := fun (q : c.State) (as : Fin i → Option c.Symbol) (bs : Fin c.workTapeCount → Option c.Symbol) => c.interpretAction (c.actionAt q as bs) ⋯ ⋯ ⋯ ⋯ }

@[simp]

theorem Turing.Code.toTM_q₀ {i : ℕ} (c : Code i) : c.toTM.q₀ = ⟨c.startState, ⋯⟩

theorem Turing.Code.toTM_tr {i : ℕ} (c : Code i) (q : c.State) (as : Fin i → Option c.Symbol) (bs : Fin c.workTapeCount → Option c.Symbol) : c.toTM.tr q as bs = c.interpretAction (c.actionAt q as bs) ⋯ ⋯ ⋯ ⋯

The transition function of Code.toTM is, definitionally, the interpretation of the canonical table entry.

@[simp]

theorem Turing.Code.interpretAction_outS {i : ℕ} (c : Code i) (a : RawAction) (h₁ : a.inputMoves.size = i) (h₂ : a.workActions.size = c.workTapeCount) (h₃ : ∀ wa ∈ a.workActions, ∀ (s : ℕ), wa.write = RawWrite.symbol s → s < c.alphabetSize) (h₄ : ∀ q' ∈ a.nextState, q' < c.stateCount) : (c.interpretAction a h₁ h₂ h₃ h₄).outS = Option.map (fun (b : Bool) => c.bitEmbedding b) a.output

@[simp]

theorem Turing.Code.toTM_tr_outS {i : ℕ} (c : Code i) (q : c.State) (as : Fin i → Option c.Symbol) (bs : Fin c.workTapeCount → Option c.Symbol) : (c.toTM.tr q as bs).outS = Option.map (fun (b : Bool) => c.bitEmbedding b) (c.actionAt q as bs).output

The emitted symbol of a coded transition, at the level of raw data.

theorem Turing.Code.interpretAction_q'_map_val {i : ℕ} (c : Code i) (a : RawAction) (h₁ : a.inputMoves.size = i) (h₂ : a.workActions.size = c.workTapeCount) (h₃ : ∀ wa ∈ a.workActions, ∀ (s : ℕ), wa.write = RawWrite.symbol s → s < c.alphabetSize) (h₄ : ∀ q' ∈ a.nextState, q' < c.stateCount) : Option.map Fin.val (c.interpretAction a h₁ h₂ h₃ h₄).q' = a.nextState

The successor state of a coded transition, at the level of raw data.

theorem Turing.Code.toTM_tr_q'_map_val {i : ℕ} (c : Code i) (q : c.State) (as : Fin i → Option c.Symbol) (bs : Fin c.workTapeCount → Option c.Symbol) : Option.map Fin.val (c.toTM.tr q as bs).q' = (c.actionAt q as bs).nextState

The successor state of Code.toTM, at the level of raw data.

theorem Turing.Code.toTM_tr_q'_eq_none_iff {i : ℕ} (c : Code i) (q : c.State) (as : Fin i → Option c.Symbol) (bs : Fin c.workTapeCount → Option c.Symbol) : (c.toTM.tr q as bs).q' = none ↔ (c.actionAt q as bs).nextState = none

A coded machine halts on an observation exactly when the table entry says to.

theorem Turing.Code.outputSymbol_isBit {i : ℕ} (c : Code i) {input : Fin i → List c.Symbol} (cfg : MultiInputTM.Cfg i c.workTapeCount c.Symbol c.State input) : MultiInputTM.outputSymbol cfg = none ∨ ∃ (b : Bool), MultiInputTM.outputSymbol cfg = some (c.bitEmbedding b)

Every symbol a coded machine emits is one of the two reserved bit symbols.

def Turing.Code.decodeBitOutput {i : ℕ} (c : Code i) (l : List c.Symbol) : List Bool

Decode a machine-alphabet string as a bit string: symbol 1 is true, every other symbol is false. On outputs of coded machines this is faithful, because only the two bit symbols are ever emitted (Code.outputSymbol_isBit).

Equations

• c.decodeBitOutput l = List.map (fun (s : c.Symbol) => ↑s == 1) l

@[simp]

theorem Turing.Code.decodeBitOutput_map_bitEmbedding {i : ℕ} (c : Code i) (l : List Bool) : c.decodeBitOutput (List.map (fun (b : Bool) => c.bitEmbedding b) l) = l