Canonical observation indexing for coded machines

An observation of an i-input machine with w work tapes over the alphabet Fin σ is a triple (q, as, bs) of a state q : Fin Q, the tuple as of symbols under the input heads, and the tuple bs of symbols under the work heads (each an Option (Fin σ), none being the blank). This file fixes, once and for all, the bijection between observations and positions in a dense transition table.

Normative order

This order is normative: the serialization format (Milestone C) and the universal machine's table lookup (Milestones E–G) cite it, and it must never change.

• transitionIndex q as bs = q * (σ + 1) ^ (i + w) + obs, where obs is the Horner evaluation (Turing.encodeDigits), in radix σ + 1, of the digit string consisting of the input-tape symbols in ascending tape order followed by the work-tape symbols in ascending tape order — input tape 0 is the most significant digit;
• the digit of the blank none is 0, and the digit of the symbol a : Fin σ is a + 1 (Turing.encodeSymbol?).

Nothing here depends on Fintype.elems, hash or enumeration order, a chosen basis, or choice: the order is fixed by the explicit recursions below (decision D5 of planning/tm-infrastructure.md; deliberately not finFunctionFinEquiv, whose digit order is owned by Mathlib). Both inverse laws are proved for symbols, observations, and transition indices; the decode direction is consumed by the Milestone C parser and by the universal machine.

Digit strings

def Turing.encodeDigits {r : ℕ} : List (Fin (r + 1)) → ℕ

Horner evaluation of a digit string in radix r + 1; the first digit is the most significant one.

Equations

• Turing.encodeDigits [] = 0
• Turing.encodeDigits (a :: l) = ↑a * (r + 1) ^ l.length + Turing.encodeDigits l

@[simp]

theorem Turing.encodeDigits_nil {r : ℕ} : encodeDigits [] = 0

theorem Turing.encodeDigits_cons {r : ℕ} (a : Fin (r + 1)) (l : List (Fin (r + 1))) : encodeDigits (a :: l) = ↑a * (r + 1) ^ l.length + encodeDigits l

theorem Turing.encodeDigits_lt {r : ℕ} (l : List (Fin (r + 1))) : encodeDigits l < (r + 1) ^ l.length

A digit string of length len encodes a number below (r + 1) ^ len.

def Turing.decodeDigits (r a✝ : ℕ) : ℕ → List (Fin (r + 1))

Decode len digits (most significant first) from a natural number.

Equations

• Turing.decodeDigits r 0 x✝ = []
• Turing.decodeDigits r len.succ x✝ = ⟨x✝ / (r + 1) ^ len % (r + 1), ⋯⟩ :: Turing.decodeDigits r len (x✝ % (r + 1) ^ len)

@[simp]

theorem Turing.decodeDigits_length (r len n : ℕ) : (decodeDigits r len n).length = len

theorem Turing.decodeDigits_encodeDigits {r : ℕ} (l : List (Fin (r + 1))) : decodeDigits r l.length (encodeDigits l) = l

Decoding inverts encoding on digit strings.

theorem Turing.encodeDigits_decodeDigits (r len n : ℕ) : n < (r + 1) ^ len → encodeDigits (decodeDigits r len n) = n

Encoding inverts decoding on numbers below (r + 1) ^ len.

Symbol digits

def Turing.encodeSymbol? {σ : ℕ} : Option (Fin σ) → Fin (σ + 1)

The digit of an optional symbol: blank none is 0, symbol a is a + 1.

Equations

• Turing.encodeSymbol? none = 0
• Turing.encodeSymbol? (some a) = a.succ

def Turing.decodeSymbol? {σ : ℕ} (d : Fin (σ + 1)) : Option (Fin σ)

Recover an optional symbol from its digit.

Equations

• Turing.decodeSymbol? d = if h : ↑d = 0 then none else some ⟨↑d - 1, ⋯⟩

@[simp]

theorem Turing.decodeSymbol?_encodeSymbol? {σ : ℕ} (a : Option (Fin σ)) : decodeSymbol? (encodeSymbol? a) = a

@[simp]

theorem Turing.encodeSymbol?_decodeSymbol? {σ : ℕ} (d : Fin (σ + 1)) : encodeSymbol? (decodeSymbol? d) = d

Observations

def Turing.observationDigits {σ i w : ℕ} (as : Fin i → Option (Fin σ)) (bs : Fin w → Option (Fin σ)) : List (Fin (σ + 1))

The digit string of an observation: input symbols then work symbols, both in ascending tape order, input tape 0 most significant.

Equations

• Turing.observationDigits as bs = (List.ofFn fun (j : Fin i) => Turing.encodeSymbol? (as j)) ++ List.ofFn fun (d : Fin w) => Turing.encodeSymbol? (bs d)

@[simp]

theorem Turing.observationDigits_length {σ i w : ℕ} (as : Fin i → Option (Fin σ)) (bs : Fin w → Option (Fin σ)) : (observationDigits as bs).length = i + w

def Turing.encodeObservation {σ i w : ℕ} (as : Fin i → Option (Fin σ)) (bs : Fin w → Option (Fin σ)) : Fin ((σ + 1) ^ (i + w))

The canonical position of an observation's symbol part, below (σ + 1) ^ (i + w).

Equations

• Turing.encodeObservation as bs = ⟨Turing.encodeDigits (Turing.observationDigits as bs), ⋯⟩

def Turing.decodeObservation {σ i w : ℕ} (n : Fin ((σ + 1) ^ (i + w))) : (Fin i → Option (Fin σ)) × (Fin w → Option (Fin σ))

Recover the symbol tuples from an observation position.

Equations

• Turing.decodeObservation n = (fun (j : Fin i) => Turing.decodeSymbol? (Turing.decodeDigits σ (i + w) ↑n)[↑j], fun (d : Fin w) => Turing.decodeSymbol? (Turing.decodeDigits σ (i + w) ↑n)[i + ↑d])

@[simp]

theorem Turing.decodeObservation_encodeObservation {σ i w : ℕ} (as : Fin i → Option (Fin σ)) (bs : Fin w → Option (Fin σ)) : decodeObservation (encodeObservation as bs) = (as, bs)

Decoding inverts encoding on observations.

@[simp]

theorem Turing.encodeObservation_decodeObservation {σ i w : ℕ} (n : Fin ((σ + 1) ^ (i + w))) : encodeObservation (decodeObservation n).1 (decodeObservation n).2 = n

Encoding inverts decoding on observation positions.

Transition indices

def Turing.transitionIndex {σ i w Q : ℕ} (q : Fin Q) (as : Fin i → Option (Fin σ)) (bs : Fin w → Option (Fin σ)) : Fin (Q * (σ + 1) ^ (i + w))

The canonical position of an observation in a dense transition table: q * (σ + 1) ^ (i + w) + obs. This order is normative (see the module docstring).

Equations

• Turing.transitionIndex q as bs = ⟨↑q * (σ + 1) ^ (i + w) + ↑(Turing.encodeObservation as bs), ⋯⟩

def Turing.decodeTransitionIndex {σ i w Q : ℕ} (n : Fin (Q * (σ + 1) ^ (i + w))) : Fin Q × (Fin i → Option (Fin σ)) × (Fin w → Option (Fin σ))

Recover the observation from its position in a dense transition table.

Equations

• Turing.decodeTransitionIndex n = (⟨↑n / (σ + 1) ^ (i + w), ⋯⟩, Turing.decodeObservation ⟨↑n % (σ + 1) ^ (i + w), ⋯⟩)

@[simp]

theorem Turing.decodeTransitionIndex_transitionIndex {σ i w Q : ℕ} (q : Fin Q) (as : Fin i → Option (Fin σ)) (bs : Fin w → Option (Fin σ)) : decodeTransitionIndex (transitionIndex q as bs) = (q, as, bs)

Decoding inverts encoding on transition indices.

@[simp]

theorem Turing.transitionIndex_decodeTransitionIndex {σ i w Q : ℕ} (n : Fin (Q * (σ + 1) ^ (i + w))) : transitionIndex (decodeTransitionIndex n).1 (decodeTransitionIndex n).2.1 (decodeTransitionIndex n).2.2 = n

Encoding inverts decoding on transition-table positions.