Representing tape symbols by binary tracks

Each nonblank symbol has its own marked track. The blank symbol is represented by blank cells on every track. The decoding function is exact on these encodings.

noncomputable def Complexity.SymbolTracks.encode {Γ : Type u_1} [Inhabited Γ] (a b : Γ) : Option Bool

One track per source symbol; the blank symbol leaves every track blank.

Equations

• Complexity.SymbolTracks.encode a b = if a ≠ default ∧ b = a then some true else none

noncomputable def Complexity.SymbolTracks.decode {Γ : Type u_1} [Inhabited Γ] (v : Γ → Option Bool) : Γ

Decode a vector of tracks, inverse to the symbol encoding.

Equations

• Complexity.SymbolTracks.decode v = Function.invFun Complexity.SymbolTracks.encode v

theorem Complexity.SymbolTracks.encode_injective {Γ : Type u_1} [Inhabited Γ] : Function.Injective encode

Distinct source symbols have distinct vectors of tracks.

theorem Complexity.SymbolTracks.decode_encode {Γ : Type u_1} [Inhabited Γ] (a : Γ) : decode (encode a) = a

Decoding recovers every encoded source symbol.

theorem Complexity.SymbolTracks.encode_default {Γ : Type u_1} [Inhabited Γ] : encode default = fun (x : Γ) => none

A blank source cell is blank on every track.