Block Realizability Framework

This file defines block-realizability abstractions for composing TM0 machines that operate on contiguous blocks.

Main definitions

• TM0RealizesBlockSep Γ sep f: a TM0 machine processes the cells before the first designated separator sep, preserving the separator and tail.
• TM0RealizesBlock Γ f: the old blank-delimited specialization where sep = default.

Main results

• tm0RealizesBlock_comp: sequential composition of block-realizable functions
• tm0RealizesBlock_iterate: iterated application
• tm0_reverse_block: list reverse is block-realizable
• tm0_cons_block: prepending a constant is block-realizable

Block Realizability Definitions

def TM0RealizesBlockSep (Γ : Type) [Inhabited Γ] (sep : Γ) (f : List Γ → List Γ) : Prop

A TM0 that operates on a block ending at a designated separator.

Given a tape block ++ [sep] ++ suffix, the TM0 transforms it to f block ++ [sep] ++ suffix. The assumptions state that the input block is really the part before the first separator, that the active finite tape has no interior blanks, and that f block is again a valid block for the same separator.

Equations

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

def TM0RealizesBlockSepAnySuffix (Γ : Type) [Inhabited Γ] (sep : Γ) (f : List Γ → List Γ) : Prop

Strong separator-delimited block realizability: no invariant is required of the suffix after the separator.

Equations

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

def TM0RealizesBlock (Γ : Type) [Inhabited Γ] (f : List Γ → List Γ) : Prop

A TM0 that operates on a contiguous block of non-default cells, preserving everything after the first blank.

Given a tape block ++ [default] ++ suffix, the TM0 transforms it to f(block) ++ [default] ++ suffix, leaving suffix unchanged. This enables "serialized" composition of elementary operations.

Equations

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

def TM0RealizesBlockAnySuffix (Γ : Type) [Inhabited Γ] (f : List Γ → List Γ) : Prop

Strong blank-delimited block realizability: no invariant is required of the suffix after the delimiter.

Equations

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

theorem tm0RealizesBlockSep_of_anySuffix {Γ : Type} [Inhabited Γ] {sep : Γ} {f : List Γ → List Γ} (hf : TM0RealizesBlockSepAnySuffix Γ sep f) : TM0RealizesBlockSep Γ sep f

theorem tm0RealizesBlock_of_anySuffix {Γ : Type} [Inhabited Γ] {f : List Γ → List Γ} (hf : TM0RealizesBlockAnySuffix Γ f) : TM0RealizesBlock Γ f

theorem tm0RealizesBlockSepAnySuffix_default_of_block {Γ : Type} [Inhabited Γ] {f : List Γ → List Γ} (hf : TM0RealizesBlockAnySuffix Γ f) : TM0RealizesBlockSepAnySuffix Γ default f

theorem tm0RealizesBlockAnySuffix_of_sep_default {Γ : Type} [Inhabited Γ] {f : List Γ → List Γ} (hf : TM0RealizesBlockSepAnySuffix Γ default f) : TM0RealizesBlockAnySuffix Γ f

theorem tm0RealizesBlockSep_default_of_block {Γ : Type} [Inhabited Γ] {f : List Γ → List Γ} (hf : TM0RealizesBlock Γ f) : TM0RealizesBlockSep Γ default f

theorem tm0RealizesBlock_of_sep_default {Γ : Type} [Inhabited Γ] {f : List Γ → List Γ} (hf : TM0RealizesBlockSep Γ default f) : TM0RealizesBlock Γ f

Composition

theorem tm0RealizesBlockSepAnySuffix_comp {Γ : Type} [Inhabited Γ] {sep : Γ} {f g : List Γ → List Γ} (hf : TM0RealizesBlockSepAnySuffix Γ sep f) (hg : TM0RealizesBlockSepAnySuffix Γ sep g) (hf_nd : ∀ (block : List Γ), (∀ g ∈ block, g ≠ default) → ∀ g ∈ f block, g ≠ default) (hf_nsep : ∀ (block : List Γ), (∀ g ∈ block, g ≠ sep) → ∀ g ∈ f block, g ≠ sep) : TM0RealizesBlockSepAnySuffix Γ sep (g ∘ f)

Composition for strong separator-delimited block-realizable functions.

theorem tm0RealizesBlockAnySuffix_comp {Γ : Type} [Inhabited Γ] {f g : List Γ → List Γ} (hf : TM0RealizesBlockAnySuffix Γ f) (hg : TM0RealizesBlockAnySuffix Γ g) (hf_nd : ∀ (block : List Γ), (∀ g ∈ block, g ≠ default) → ∀ g ∈ f block, g ≠ default) : TM0RealizesBlockAnySuffix Γ (g ∘ f)

Composition for strong blank-delimited block-realizable functions.

theorem tm0RealizesBlockSep_comp {Γ : Type} [Inhabited Γ] {sep : Γ} {f g : List Γ → List Γ} (hf : TM0RealizesBlockSep Γ sep f) (hg : TM0RealizesBlockSep Γ sep g) (hf_nd : ∀ (block : List Γ), (∀ g ∈ block, g ≠ default) → ∀ g ∈ f block, g ≠ default) (hf_nsep : ∀ (block : List Γ), (∀ g ∈ block, g ≠ sep) → ∀ g ∈ f block, g ≠ sep) : TM0RealizesBlockSep Γ sep (g ∘ f)

Composition for separator-delimited block-realizable functions.

theorem tm0RealizesBlock_comp {Γ : Type} [Inhabited Γ] {f g : List Γ → List Γ} (hf : TM0RealizesBlock Γ f) (hg : TM0RealizesBlock Γ g) (hf_nd : ∀ (block : List Γ), (∀ g ∈ block, g ≠ default) → ∀ g ∈ f block, g ≠ default) : TM0RealizesBlock Γ (g ∘ f)

Composition of block-realizable functions. Requires f to preserve non-defaultness so that M_g can process f(block) as a valid block.

Iteration

theorem tm0RealizesBlockSep_iterate {Γ : Type} [Inhabited Γ] {sep : Γ} {f : List Γ → List Γ} (hf : TM0RealizesBlockSep Γ sep f) (hf_nd : ∀ (block : List Γ), (∀ g ∈ block, g ≠ default) → ∀ g ∈ f block, g ≠ default) (hf_nsep : ∀ (block : List Γ), (∀ g ∈ block, g ≠ sep) → ∀ g ∈ f block, g ≠ sep) (n : ℕ) : TM0RealizesBlockSep Γ sep f^[n]

Iterated separator-delimited block operations preserve realizability.

theorem tm0RealizesBlockSepAnySuffix_iterate {Γ : Type} [Inhabited Γ] {sep : Γ} {f : List Γ → List Γ} (hf : TM0RealizesBlockSepAnySuffix Γ sep f) (hf_nd : ∀ (block : List Γ), (∀ g ∈ block, g ≠ default) → ∀ g ∈ f block, g ≠ default) (hf_nsep : ∀ (block : List Γ), (∀ g ∈ block, g ≠ sep) → ∀ g ∈ f block, g ≠ sep) (n : ℕ) : TM0RealizesBlockSepAnySuffix Γ sep f^[n]

Iterated strong separator-delimited block operations preserve realizability.

theorem tm0RealizesBlock_iterate {Γ : Type} [Inhabited Γ] {f : List Γ → List Γ} (hf : TM0RealizesBlock Γ f) (hf_nd : ∀ (block : List Γ), (∀ g ∈ block, g ≠ default) → ∀ g ∈ f block, g ≠ default) (n : ℕ) : TM0RealizesBlock Γ f^[n]

Iterated block operations preserve block-realizability.

theorem iterate_preserves_nd {Γ₀ : Type} [Inhabited Γ₀] {f : List Γ₀ → List Γ₀} (hf : ∀ (block : List Γ₀), (∀ g ∈ block, g ≠ default) → ∀ g ∈ f block, g ≠ default) (n : ℕ) (block : List Γ₀) (hblock : ∀ g ∈ block, g ≠ default) (g : Γ₀) : g ∈ f^[n] block → g ≠ default

Iteration of a non-defaultness-preserving function preserves non-defaultness.

theorem iterate_preserves_nsep {Γ₀ : Type} [Inhabited Γ₀] {f : List Γ₀ → List Γ₀} {sep : Γ₀} (hf : ∀ (block : List Γ₀), (∀ g ∈ block, g ≠ sep) → ∀ g ∈ f block, g ≠ sep) (n : ℕ) (block : List Γ₀) (hblock : ∀ g ∈ block, g ≠ sep) (g : Γ₀) : g ∈ f^[n] block → g ≠ sep

Iteration preserves the "not equal to separator" invariant.

Utility Lemmas

theorem listBlank_mk_append_default {Γ : Type} [Inhabited Γ] (l : List Γ) : Turing.ListBlank.mk (l ++ [default]) = Turing.ListBlank.mk l

Generic: appending default to a ListBlank is identity.

theorem tape_mk₁_append_default {Γ : Type} [Inhabited Γ] (l : List Γ) : Turing.Tape.mk₁ (l ++ [default]) = Turing.Tape.mk₁ l

Generic: Tape.mk₁ with trailing default is identity.

theorem evalCfg_append_default {Γ Λ : Type} [Inhabited Γ] [Inhabited Λ] (M : Turing.TM0.Machine Γ Λ) (l : List Γ) : TM0Seq.evalCfg M (l ++ [default]) = TM0Seq.evalCfg M l

TM0Seq.evalCfg with trailing default input is the same.

theorem reverse_ne_default {Γ : Type} [Inhabited Γ] (block : List Γ) (hblock : ∀ g ∈ block, g ≠ default) (g : Γ) : g ∈ block.reverse → g ≠ default

Reverse preserves non-defaultness.

Reverse is block-realizable

theorem tm0_reverse_blockSep_anySuffix {Γ : Type} [Inhabited Γ] [DecidableEq Γ] [Fintype Γ] {sep : Γ} : TM0RealizesBlockSepAnySuffix Γ sep List.reverse

List reverse is block-realizable before any separator. The underlying machine RevBlock.MSep uses sep for right-boundary detection and default for left-boundary detection.

theorem tm0_reverse_blockSep {Γ : Type} [Inhabited Γ] [DecidableEq Γ] [Fintype Γ] {sep : Γ} : TM0RealizesBlockSep Γ sep List.reverse

theorem tm0_reverse_block_anySuffix {Γ : Type} [Inhabited Γ] [DecidableEq Γ] [Fintype Γ] : TM0RealizesBlockAnySuffix Γ List.reverse

List reverse is block-realizable. A TM0 can reverse a contiguous block of non-default cells while preserving the suffix.

theorem tm0_reverse_block {Γ : Type} [Inhabited Γ] [DecidableEq Γ] [Fintype Γ] : TM0RealizesBlock Γ List.reverse

Cons (prepend) is block-realizable

noncomputable def consSimpleMachine {Γ : Type} [Inhabited Γ] [DecidableEq Γ] (c : Γ) : Turing.TM0.Machine Γ (Fin 3)

The simple cons machine: move left, write c, halt. Prepends c to the tape by writing at position −1.

Equations

• consSimpleMachine c 0 x✝ = some (1, Turing.TM0.Stmt.move Turing.Dir.left)
• consSimpleMachine c 1 x✝ = some (2, Turing.TM0.Stmt.write c)
• consSimpleMachine c 2 x✝ = none

theorem consSimpleMachine_halts {Γ : Type} [Inhabited Γ] [DecidableEq Γ] (c : Γ) (l : List Γ) : (TM0Seq.evalCfg (consSimpleMachine c) l).Dom

theorem tape_write_move_left_mk₁ {Γ : Type} [Inhabited Γ] (c : Γ) (l : List Γ) : Turing.Tape.write c (Turing.Tape.move Turing.Dir.left (Turing.Tape.mk₁ l)) = Turing.Tape.mk₁ (c :: l)

Writing c after moving left from Tape.mk₁ l gives Tape.mk₁ (c :: l).

theorem consSimpleMachine_eval_eq {Γ : Type} [Inhabited Γ] [DecidableEq Γ] (c : Γ) (l : List Γ) : { q := 2, Tape := Turing.Tape.write c (Turing.Tape.move Turing.Dir.left (Turing.Tape.mk₁ l)) } ∈ TM0Seq.evalCfg (consSimpleMachine c) l

theorem consSimpleMachine_tape {Γ : Type} [Inhabited Γ] [DecidableEq Γ] (c : Γ) (l : List Γ) (h : (TM0Seq.evalCfg (consSimpleMachine c) l).Dom) : ((TM0Seq.evalCfg (consSimpleMachine c) l).get h).Tape = Turing.Tape.mk₁ (c :: l)

theorem tm0_cons_blockSep_anySuffix {Γ : Type} [Inhabited Γ] [DecidableEq Γ] [Fintype Γ] {sep : Γ} (c : Γ) : TM0RealizesBlockSepAnySuffix Γ sep fun (x : List Γ) => c :: x

Prepending a fixed element is block-realizable before any separator.

The cons machine (consSimpleMachine) moves left, writes c, and halts. It never inspects any cell to detect a block boundary, so it works with any separator.

theorem tm0_cons_blockSep {Γ : Type} [Inhabited Γ] [DecidableEq Γ] [Fintype Γ] {sep : Γ} (c : Γ) : TM0RealizesBlockSep Γ sep fun (x : List Γ) => c :: x

theorem tm0_cons_block_anySuffix {Γ : Type} [Inhabited Γ] [DecidableEq Γ] [Fintype Γ] (c : Γ) (_hc : c ≠ default) : TM0RealizesBlockAnySuffix Γ fun (x : List Γ) => c :: x

Prepending a fixed non-default element is block-realizable.

theorem tm0_cons_block {Γ : Type} [Inhabited Γ] [DecidableEq Γ] [Fintype Γ] (c : Γ) (_hc : c ≠ default) : TM0RealizesBlock Γ fun (x : List Γ) => c :: x

Identity is block-realizable

theorem tm0_id_blockSep_anySuffix {Γ : Type} [Inhabited Γ] {sep : Γ} : TM0RealizesBlockSepAnySuffix Γ sep id

The identity function is realizable before any separator.

A trivial TM0 machine that halts immediately on any input tape.

theorem tm0_id_blockSep {Γ : Type} [Inhabited Γ] {sep : Γ} : TM0RealizesBlockSep Γ sep id

theorem tm0_id_block_anySuffix {Γ : Type} [Inhabited Γ] : TM0RealizesBlockAnySuffix Γ id

The identity function is block-realizable.

theorem tm0_id_block {Γ : Type} [Inhabited Γ] : TM0RealizesBlock Γ id

Prepend list is block-realizable

theorem prependList_ne_default' {Γ : Type} [Inhabited Γ] (pref block : List Γ) (hpref : ∀ g ∈ pref, g ≠ default) (hblock : ∀ g ∈ block, g ≠ default) (g : Γ) : g ∈ pref ++ block → g ≠ default

Appending a non-default prefix preserves non-defaultness.

theorem reverse_ne_sep {Γ : Type} {sep : Γ} (block : List Γ) (hblock : ∀ g ∈ block, g ≠ sep) (g : Γ) : g ∈ block.reverse → g ≠ sep

Reverse preserves the "not equal to separator" invariant.

theorem tm0_prependList_blockSep_anySuffix {Γ : Type} [Inhabited Γ] [DecidableEq Γ] [Fintype Γ] {sep : Γ} (pref : List Γ) (hpref_nd : ∀ g ∈ pref, g ≠ default) (hpref_nsep : ∀ g ∈ pref, g ≠ sep) : TM0RealizesBlockSepAnySuffix Γ sep fun (block : List Γ) => pref ++ block

Prepending a fixed non-default, non-sep list is realizable before a separator.

theorem tm0_prependList_blockSep {Γ : Type} [Inhabited Γ] [DecidableEq Γ] [Fintype Γ] {sep : Γ} (pref : List Γ) (hpref_nd : ∀ g ∈ pref, g ≠ default) (hpref_nsep : ∀ g ∈ pref, g ≠ sep) : TM0RealizesBlockSep Γ sep fun (block : List Γ) => pref ++ block