Heterogeneous Fold via Reverse + While Loop

This file decomposes tm0Het_fold_blockRealizable into two TM0RealizesBlock operations:

1. Reverse: TM0RealizesBlock _ List.reverse (from tm0_reverse_block)
2. While loop: TM0RealizesBlock _ (hetFoldWhile f), where the body pops the leftmost Sum.inl tag and applies f to the accumulator.

Architecture

The while-loop body is expressed as a TM0RealizesBlockCond, which extends TM0RealizesBlock with conditional halting: the body machine halts at a designated continuation state q_cont when the loop should continue (an inl tag was processed), and at a different state when no inl tag remains (loop terminates).

The general combinator tm0RealizesBlock_while builds a TM0RealizesBlock from a TM0RealizesBlockCond body using tm0WhileLoop.

Tape Layout

Throughout the while loop, the tape holds a single contiguous non-default block of the form:

  [some(inl tⱼ), ..., some(inl t₁), some(inr g₁), ..., some(inr gₖ)]

where tⱼ, ..., t₁ are the remaining unprocessed tags and g₁, ..., gₖ is the current accumulator. All elements are some _, hence non-default (none), so this is a valid block for TM0RealizesBlock (Option (T ⊕ Γ₀)).

Fold Identity

The fold identity List.foldr f [] w = List.foldl (fun a t => f t a) [] w.reverse connects the right-to-left fold to the left-to-right while loop on the reversed input.

Key results

• tm0RealizesBlock_while: generic TM0 while-loop combinator for blocks.
• hetFold_decomp: decomposition of the heterogeneous fold into reverse plus while-loop iteration.
• tm0Het_fold_blockRealizable': block-realizability of the heterogeneous fold.

While-loop TM0 combinator

noncomputable def tm0WhileLoop {Γ Λ : Type} [Inhabited Γ] [Inhabited Λ] [DecidableEq Λ] (M : Turing.TM0.Machine Γ Λ) (q_continue : Λ) : Turing.TM0.Machine Γ Λ

While-loop TM0 machine. Runs M repeatedly; when M halts at q_continue, it restarts M. When M halts at any other state, it halts.

Equations

• tm0WhileLoop M q_continue q a = match M q a with | some (q', s) => some (q', s) | none => if q = q_continue then M default a else none

theorem tm0WhileLoop_step_some {Γ Λ : Type} [Inhabited Γ] [Inhabited Λ] [DecidableEq Λ] (M : Turing.TM0.Machine Γ Λ) (q_continue q : Λ) (a : Γ) (q' : Λ) (s : Turing.TM0.Stmt Γ) (h : M q a = some (q', s)) : tm0WhileLoop M q_continue q a = some (q', s)

theorem tm0WhileLoop_halt {Γ Λ : Type} [Inhabited Γ] [Inhabited Λ] [DecidableEq Λ] (M : Turing.TM0.Machine Γ Λ) (q_continue q : Λ) (a : Γ) (hne : q ≠ q_continue) (h : M q a = none) : tm0WhileLoop M q_continue q a = none

theorem tm0WhileLoop_reaches_of_M {Γ Λ : Type} [Inhabited Γ] [Inhabited Λ] [DecidableEq Λ] (M : Turing.TM0.Machine Γ Λ) (q_continue : Λ) (c₁ c₂ : Turing.TM0.Cfg Γ Λ) (h : Turing.Reaches (Turing.TM0.step M) c₁ c₂) : Turing.Reaches (Turing.TM0.step (tm0WhileLoop M q_continue)) c₁ c₂

Conditional Block Realizability

def TM0RealizesBlockCond {Γ : Type} [Inhabited Γ] (step : List Γ → List Γ) (cond : List Γ → Prop) [DecidablePred cond] : Prop

A TM0 block step with conditional continuation.

When cond block holds: transforms block to step block, halts at q_cont. When ¬cond block: leaves block unchanged, halts at state ≠ q_cont.

This models a single iteration of a while loop body. The halting state signals whether the loop should continue or terminate.

Equations

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

Fuel-Bounded While-Loop Iteration

def blockIterateWhile {Γ : Type} (step : List Γ → List Γ) (cond : List Γ → Prop) [DecidablePred cond] : ℕ → List Γ → List Γ

Iterate a step function while a condition holds, bounded by fuel. Returns the block after at most n applications of step.

Equations

• blockIterateWhile step cond 0 x✝ = x✝
• blockIterateWhile step cond n.succ x✝ = if cond x✝ then blockIterateWhile step cond n (step x✝) else x✝

theorem blockIterateWhile_succ_true {Γ : Type} (step : List Γ → List Γ) (cond : List Γ → Prop) [DecidablePred cond] (n : ℕ) (block : List Γ) (hcond : cond block) : blockIterateWhile step cond (n + 1) block = blockIterateWhile step cond n (step block)

theorem blockIterateWhile_succ_false {Γ : Type} (step : List Γ → List Γ) (cond : List Γ → Prop) [DecidablePred cond] (n : ℕ) (block : List Γ) (hcond : ¬cond block) : blockIterateWhile step cond (n + 1) block = block

While-Loop Helper Lemmas

theorem whileLoop_eval_not_cont {Γ Λ : Type} [Inhabited Γ] [Inhabited Λ] [DecidableEq Λ] (M : Turing.TM0.Machine Γ Λ) (q_cont : Λ) (l : List Γ) (h_body_dom : (TM0Seq.evalCfg M l).Dom) (h_body_q : ((TM0Seq.evalCfg M l).get h_body_dom).q ≠ q_cont) : (TM0Seq.evalCfg (tm0WhileLoop M q_cont) l).Dom ∧ ∀ (h : (TM0Seq.evalCfg (tm0WhileLoop M q_cont) l).Dom), ((TM0Seq.evalCfg (tm0WhileLoop M q_cont) l).get h).Tape = ((TM0Seq.evalCfg M l).get h_body_dom).Tape

theorem whileLoop_step_restart_eq {Γ Λ : Type} [Inhabited Γ] [Inhabited Λ] [DecidableEq Λ] (M : Turing.TM0.Machine Γ Λ) (q_cont : Λ) (T : Turing.Tape Γ) (h_halt : M q_cont T.head = none) : Turing.TM0.step (tm0WhileLoop M q_cont) { q := q_cont, Tape := T } = Turing.TM0.step (tm0WhileLoop M q_cont) { q := default, Tape := T }

theorem whileLoop_eval_cont {Γ Λ : Type} [Inhabited Γ] [Inhabited Λ] [DecidableEq Λ] (M : Turing.TM0.Machine Γ Λ) (q_cont : Λ) (l l' : List Γ) (h_body_dom : (TM0Seq.evalCfg M l).Dom) (h_body_q : ((TM0Seq.evalCfg M l).get h_body_dom).q = q_cont) (h_body_tape : ((TM0Seq.evalCfg M l).get h_body_dom).Tape = Turing.Tape.mk₁ l') (h_W_dom' : (TM0Seq.evalCfg (tm0WhileLoop M q_cont) l').Dom) : (TM0Seq.evalCfg (tm0WhileLoop M q_cont) l).Dom ∧ ∀ (h : (TM0Seq.evalCfg (tm0WhileLoop M q_cont) l).Dom), ((TM0Seq.evalCfg (tm0WhileLoop M q_cont) l).get h).Tape = ((TM0Seq.evalCfg (tm0WhileLoop M q_cont) l').get h_W_dom').Tape

While-Loop Block Realizability Combinator

theorem tm0RealizesBlock_while {Γ : Type} [Inhabited Γ] [DecidableEq Γ] [Fintype Γ] (step result : List Γ → List Γ) (cond : List Γ → Prop) [DecidablePred cond] (hbody : TM0RealizesBlockCond step cond) (hstep_nd : ∀ (block : List Γ), (∀ g ∈ block, g ≠ default) → cond block → ∀ g ∈ step block, g ≠ default) (hresult_eq : ∀ (block : List Γ), (∀ g ∈ block, g ≠ default) → ∃ (n : ℕ), result block = blockIterateWhile step cond n block ∧ ¬cond (blockIterateWhile step cond n block)) (_hresult_nd : ∀ (block : List Γ), (∀ g ∈ block, g ≠ default) → ∀ g ∈ result block, g ≠ default) : TM0RealizesBlock Γ result

While-loop block realizability combinator.

Given a conditionally block-realizable body (TM0RealizesBlockCond), a result function that equals the iterated application of step with sufficient fuel, the result function is block-realizable.

The TM0 machine is built using tm0WhileLoop M_body q_cont, which reruns M_body whenever it halts at q_cont, and halts when M_body halts at any other state.

Generic Prefix Fold

noncomputable def prefixFoldStep {Gamma Tag : Type} (tagOf : Gamma → Option Tag) (F : Tag → List Gamma → List Gamma) : List Gamma → List Gamma

A generic fold step over one ambient alphabet.

The fold layer only knows how to decode the first cell as a tag. The body already operates on the same alphabet as the tape block.

Equations

• prefixFoldStep tagOf F (c :: rest) = match tagOf c with | some t => F t rest | none => c :: rest
• prefixFoldStep tagOf F [] = []

def hasTagHead {Gamma Tag : Type} (tagOf : Gamma → Option Tag) : List Gamma → Prop

Generic head condition for the prefix fold.

Equations

• hasTagHead tagOf (c :: rest) = ((tagOf c).isSome = true)
• hasTagHead tagOf [] = False

instance instDecidablePredListHasTagHead {Gamma Tag : Type} (tagOf : Gamma → Option Tag) : DecidablePred (hasTagHead tagOf)

Equations

• instDecidablePredListHasTagHead tagOf [] = isFalse ⋯
• instDecidablePredListHasTagHead tagOf (c :: tail) = id inferInstance

def isTagCell {Gamma Tag : Type} (tagOf : Gamma → Option Tag) (c : Gamma) : Bool

Boolean predicate used for the fuel bound of the prefix fold.

Equations

• isTagCell tagOf c = (tagOf c).isSome

noncomputable def prefixFoldWhile {Gamma Tag : Type} (tagOf : Gamma → Option Tag) (F : Tag → List Gamma → List Gamma) (block : List Gamma) : List Gamma

Generic while-style fold over a leading tag prefix.

This is the folding mechanism. It is deliberately independent of any embedding/decoding between alphabets.

Equations

• prefixFoldWhile tagOf F block = blockIterateWhile (prefixFoldStep tagOf F) (hasTagHead tagOf) (List.takeWhile (isTagCell tagOf) block).length block

Generic Separated Layout Mapping

def separatedMix {Gamma Tag Acc : Type} (tagEmb : Tag → Gamma) (sep : Gamma) (accEmb : Acc → Gamma) (tags : List Tag) (acc : List Acc) : List Gamma

Generic separated block layout: remaining tags, one explicit separator, then accumulator content. The concrete alphabet is supplied by the embeddings.

Equations

• separatedMix tagEmb sep accEmb tags acc = List.map tagEmb tags ++ [sep] ++ List.map accEmb acc

noncomputable def separatedAccLift {Gamma Tag Acc : Type} (isTag : Gamma → Bool) (sep : Gamma) (decodeAcc : Gamma → Option Acc) (accEmb : Acc → Gamma) (f : Tag → List Acc → List Acc) (t : Tag) : List Gamma → List Gamma

Generic layout/mapping adapter over a separated block.

It keeps the tag prefix, consumes exactly the first non-tag cell as separator, decodes the accumulator suffix, applies the accumulator operation, and writes the result back using accEmb.

This is not the fold. It is the alphabet/layout bridge that turns an accumulator-alphabet operation into an ambient-alphabet block operation.

Equations

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

noncomputable def separatedFoldAdapt {Gamma Tag Acc : Type} (isTag : Gamma → Bool) (sep : Gamma) (decodeAcc : Gamma → Option Acc) (accEmb : Acc → Gamma) (f : Tag → List Acc → List Acc) (t : Tag) : List Gamma → List Gamma

Backwards-compatible name for the separated layout adapter.

Equations

• separatedFoldAdapt isTag sep decodeAcc accEmb f t = separatedAccLift isTag sep decodeAcc accEmb f t

theorem tm0_separatedAccLift_block_of_sameAlphabet {Gamma Tag Acc : Type} [Inhabited Gamma] [DecidableEq Gamma] [Fintype Gamma] [Inhabited Acc] [DecidableEq Acc] [Fintype Acc] (isTag : Gamma → Bool) (sep : Gamma) (decodeAcc : Gamma → Option Acc) (accEmb : Acc → Gamma) (f : Tag → List Acc → List Acc) (t : Tag) (hf : TM0RealizesBlock Gamma (separatedAccLift isTag sep decodeAcc accEmb f t)) : TM0RealizesBlock Gamma (separatedAccLift isTag sep decodeAcc accEmb f t)

Trivial same-alphabet interface for the generic separated adapter.

The old statement tried to derive this from an accumulator-alphabet block machine. That is not valid without stronger assumptions on the concrete encoding/decoding and on suffix preservation. Callers should provide the same-alphabet block machine for the actual adapter they use.

theorem tm0_separatedFoldAdapt_block_of_sameAlphabet {Gamma Tag Acc : Type} [Inhabited Gamma] [DecidableEq Gamma] [Fintype Gamma] [Inhabited Acc] [DecidableEq Acc] [Fintype Acc] (isTag : Gamma → Bool) (sep : Gamma) (decodeAcc : Gamma → Option Acc) (accEmb : Acc → Gamma) (f : Tag → List Acc → List Acc) (t : Tag) (hf : TM0RealizesBlock Gamma (separatedFoldAdapt isTag sep decodeAcc accEmb f t)) : TM0RealizesBlock Gamma (separatedFoldAdapt isTag sep decodeAcc accEmb f t)

Trivial same-alphabet interface for the separated layout adapter.

Heterogeneous Fold Definitions

def isHetInl {T Γ₀ : Type} (x : Option (T ⊕ Γ₀)) : Bool

Check if a het block element is an inl tag.

Equations

• isHetInl (some (Sum.inl val)) = true
• isHetInl x = false

def hetTagDecode {T Γ₀ : Type} : Option (T ⊕ Γ₀) → Option T

Decode fold tags from the concrete heterogeneous alphabet.

Equations

• hetTagDecode (some (Sum.inl val)) = some val
• hetTagDecode x✝ = none

def hasHetInlHead {T Γ₀ : Type} : List (Option (T ⊕ Γ₀)) → Prop

Condition: block starts with an inl tag (signals the while loop should continue).

Equations

• hasHetInlHead (some (Sum.inl val) :: tail) = True
• hasHetInlHead x✝ = False

instance instDecidablePredListOptionSumHasHetInlHead {T Γ₀ : Type} : DecidablePred hasHetInlHead

Equations

• instDecidablePredListOptionSumHasHetInlHead (some (Sum.inl val) :: tail) = isTrue trivial
• instDecidablePredListOptionSumHasHetInlHead [] = isFalse ⋯
• instDecidablePredListOptionSumHasHetInlHead (none :: tail) = isFalse ⋯
• instDecidablePredListOptionSumHasHetInlHead (some (Sum.inr val) :: tail) = isFalse ⋯

def hetSep {T Γ₀ : Type} [Inhabited Γ₀] : Option (T ⊕ Γ₀)

Explicit separator between the remaining inl tags and the inr accumulator. The accumulator invariant excludes default : Γ₀, so some (Sum.inr default) is fresh for accumulator contents while still being a nonblank tape symbol.

Equations

• hetSep = some (Sum.inr default)

def hetTagEmb {T Γ₀ : Type} (t : T) : Option (T ⊕ Γ₀)

Embed fold tags into the concrete heterogeneous alphabet.

Equations

• hetTagEmb t = some (Sum.inl t)

def hetAccEmb {T Γ₀ : Type} (g : Γ₀) : Option (T ⊕ Γ₀)

Embed accumulator symbols into the concrete heterogeneous alphabet.

Equations

• hetAccEmb g = some (Sum.inr g)

def hetAccDecode {T Γ₀ : Type} : Option (T ⊕ Γ₀) → Option Γ₀

Decode accumulator cells from the concrete heterogeneous alphabet.

Equations

• hetAccDecode (some (Sum.inr g)) = some g
• hetAccDecode x✝ = none

def hetMixSep {T Γ₀ : Type} (sep : Option (T ⊕ Γ₀)) (ts : List T) (acc : List Γ₀) : List (Option (T ⊕ Γ₀))

Mixed het block representation with an explicit separator: inl tags, then sep, then the inr accumulator.

Equations

• hetMixSep sep ts acc = separatedMix hetTagEmb sep hetAccEmb ts acc

def hetMix {T Γ₀ : Type} [Inhabited Γ₀] (ts : List T) (acc : List Γ₀) : List (Option (T ⊕ Γ₀))

Default concrete het layout separator. Prefer proving generic facts about hetMixSep when the separator matters.

Equations

• hetMix ts acc = hetMixSep hetSep ts acc

noncomputable def hetFoldStep {T Γ₀ : Type} (F : T → List (Option (T ⊕ Γ₀)) → List (Option (T ⊕ Γ₀))) : List (Option (T ⊕ Γ₀)) → List (Option (T ⊕ Γ₀))

One step of the het fold while loop. Pops the leftmost inl t tag and runs the same-alphabet step F t on the remaining block.

The fact that F t preserves the remaining tags and updates only the accumulator is a function-level obligation, not part of this generic fold construction.

Equations

• hetFoldStep F = prefixFoldStep hetTagDecode F

noncomputable def hetFoldWhile {T Γ₀ : Type} (F : T → List (Option (T ⊕ Γ₀)) → List (Option (T ⊕ Γ₀))) (block : List (Option (T ⊕ Γ₀))) : List (Option (T ⊕ Γ₀))

The full while-loop result function, defined as iterated application of hetFoldStep with fuel equal to the number of leading inl tags.

This directly models what the tm0WhileLoop machine computes: iterate hetFoldStep while hasHetInlHead, stopping when no more inl tags remain at the head.

Equations

• hetFoldWhile F block = blockIterateWhile (hetFoldStep F) hasHetInlHead (List.takeWhile isHetInl block).length block

noncomputable def hetFoldAdaptSep {T Γ₀ : Type} (sep : Option (T ⊕ Γ₀)) (f : T → List Γ₀ → List Γ₀) (t : T) : List (Option (T ⊕ Γ₀)) → List (Option (T ⊕ Γ₀))

Function-level adapter from an accumulator operation to a homogeneous het-tape operation.

This is intentionally not part of the generic fold theorem. Any machine realizability proof for this adapter must account for the alphabet/layout boundary explicitly.

Equations

• hetFoldAdaptSep sep f t = separatedAccLift isHetInl sep hetAccDecode hetAccEmb f t

noncomputable def hetFoldAdapt {T Γ₀ : Type} [Inhabited Γ₀] (f : T → List Γ₀ → List Γ₀) (t : T) : List (Option (T ⊕ Γ₀)) → List (Option (T ⊕ Γ₀))

Concrete default separator instantiation of hetFoldAdaptSep.

Equations

• hetFoldAdapt f t = hetFoldAdaptSep hetSep f t

theorem tm0_hetFoldAdaptSep_block_of_sameAlphabet {T Γ₀ : Type} (sep : Option (T ⊕ Γ₀)) (f : T → List Γ₀ → List Γ₀) (t : T) (hf : TM0RealizesBlock (Option (T ⊕ Γ₀)) (hetFoldAdaptSep sep f t)) : TM0RealizesBlock (Option (T ⊕ Γ₀)) (hetFoldAdaptSep sep f t)

Same-alphabet machine obligation for hetFoldAdaptSep.

This theorem deliberately no longer claims that an accumulator-alphabet machine is enough. Preserving the leading inl tail is a concrete same-alphabet obligation.

theorem tm0_hetFoldAdapt_block_of_sameAlphabet {T Γ₀ : Type} [Inhabited Γ₀] (f : T → List Γ₀ → List Γ₀) (t : T) (hf : TM0RealizesBlock (Option (T ⊕ Γ₀)) (hetFoldAdapt f t)) : TM0RealizesBlock (Option (T ⊕ Γ₀)) (hetFoldAdapt f t)

Mathematical Correctness

theorem hasHetInlHead_hetMix_cons {T Γ₀ : Type} [Inhabited Γ₀] (t : T) (ts : List T) (acc : List Γ₀) : hasHetInlHead (hetMix (t :: ts) acc)

hetMix with a non-empty tag list starts with inl.

theorem not_hasHetInlHead_hetMix_nil {T Γ₀ : Type} [Inhabited Γ₀] (acc : List Γ₀) : ¬hasHetInlHead (hetMix [] acc)

hetMix with empty tag list does NOT start with inl.

theorem hetFoldStep_hetMix {T Γ₀ : Type} [Inhabited Γ₀] (F : T → List (Option (T ⊕ Γ₀)) → List (Option (T ⊕ Γ₀))) (f : T → List Γ₀ → List Γ₀) (hF : ∀ (t : T) (ts : List T) (acc : List Γ₀), F t (hetMix ts acc) = hetMix ts (f t acc)) (t : T) (ts : List T) (acc : List Γ₀) : hetFoldStep F (hetMix (t :: ts) acc) = hetMix ts (f t acc)

One step is correct on hetMix when the same-alphabet step has the intended function-level behavior.

theorem hetFoldAdapt_hetMix {T Γ₀ : Type} [Inhabited Γ₀] (f : T → List Γ₀ → List Γ₀) (t : T) (ts : List T) (acc : List Γ₀) : hetFoldAdapt f t (hetMix ts acc) = hetMix ts (f t acc)

theorem takeWhile_isHetInl_hetMix {T Γ₀ : Type} [Inhabited Γ₀] (ts : List T) (acc : List Γ₀) : List.takeWhile isHetInl (hetMix ts acc) = List.map (some ∘ Sum.inl) ts

theorem hetFoldWhile_hetMix {T Γ₀ : Type} [Inhabited Γ₀] (F : T → List (Option (T ⊕ Γ₀)) → List (Option (T ⊕ Γ₀))) (f : T → List Γ₀ → List Γ₀) (hF : ∀ (t : T) (ts : List T) (acc : List Γ₀), F t (hetMix ts acc) = hetMix ts (f t acc)) (ts : List T) (acc : List Γ₀) : hetFoldWhile F (hetMix ts acc) = hetMix [] (List.foldl (fun (a : List Γ₀) (t : T) => f t a) acc ts)

hetFoldWhile is correct on hetMix: computes foldl.

theorem foldl_flip_reverse_eq_foldr {α β : Type} (f : α → β → β) (z : β) (w : List α) : List.foldl (fun (a : β) (t : α) => f t a) z w.reverse = List.foldr f z w

The fold identity: foldl on the reversed list equals foldr.

theorem hetFold_decomp {T Γ₀ : Type} [Inhabited Γ₀] (F : T → List (Option (T ⊕ Γ₀)) → List (Option (T ⊕ Γ₀))) (f : T → List Γ₀ → List Γ₀) (hF : ∀ (t : T) (ts : List T) (acc : List Γ₀), F t (hetMix ts acc) = hetMix ts (f t acc)) (w : List T) : hetFoldWhile F ((List.map (some ∘ Sum.inl) w).reverse ++ [hetSep]) = hetMix [] (List.foldr f [] w)

Decomposition identity: hetFoldWhile ∘ reverse on a pure inl block equals the foldr result.

Non-Defaultness

theorem hetMix_ne_default {T Γ₀ : Type} [Inhabited Γ₀] (ts : List T) (acc : List Γ₀) (_hacc : ∀ g ∈ acc, g ≠ default) (g : Option (T ⊕ Γ₀)) : g ∈ hetMix ts acc → g ≠ default

All elements of hetMix are non-default (some _).

theorem map_inl_ne_default {T Γ₀ : Type} (w : List T) (g : Option (T ⊕ Γ₀)) : g ∈ List.map (some ∘ Sum.inl) w → g ≠ default

Elements of w.map (some ∘ Sum.inl) are non-default.

theorem hetFoldStep_ne_default {T Γ₀ : Type} (F : T → List (Option (T ⊕ Γ₀)) → List (Option (T ⊕ Γ₀))) (hF_nd : ∀ (t : T) (block : List (Option (T ⊕ Γ₀))), (∀ g ∈ block, g ≠ default) → ∀ g ∈ F t block, g ≠ default) (block : List (Option (T ⊕ Γ₀))) (hblock : ∀ g ∈ block, g ≠ default) (hcond : hasHetInlHead block) (g : Option (T ⊕ Γ₀)) : g ∈ hetFoldStep F block → g ≠ default

hetFoldStep preserves non-defaultness when the condition holds.

theorem hetFoldWhile_ne_default {T Γ₀ : Type} (F : T → List (Option (T ⊕ Γ₀)) → List (Option (T ⊕ Γ₀))) (hF_nd : ∀ (t : T) (block : List (Option (T ⊕ Γ₀))), (∀ g ∈ block, g ≠ default) → ∀ g ∈ F t block, g ≠ default) (block : List (Option (T ⊕ Γ₀))) (hblock : ∀ g ∈ block, g ≠ default) (g : Option (T ⊕ Γ₀)) : g ∈ hetFoldWhile F block → g ≠ default

Invariant-Restricted Block Realizability

def TM0RealizesBlockCondInv {Γ : Type} [Inhabited Γ] (step : List Γ → List Γ) (cond : List Γ → Prop) [DecidablePred cond] (blockInv : List Γ → Prop) : Prop

A conditional block step with an invariant restricting which blocks the machine must handle.

This weakens TM0RealizesBlockCond by only requiring the machine to work on blocks satisfying blockInv, with empty suffix. This is necessary for the het fold step because each conditional step is only specified on well-formed blocks, where inl heads and inr payloads are properly separated. Keeping the suffix empty prevents the block machine contract from needing to preserve unrelated heterogeneous tape cells beyond the active block.

Equations

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

def isWellFormedHetBlock {T Γ₀ : Type} [Inhabited Γ₀] (block : List (Option (T ⊕ Γ₀))) : Prop

Well-formedness predicate for het blocks: the block is of the form hetMix ts acc for some tag list ts and accumulator acc with all accumulator elements non-default.

Equations

• isWellFormedHetBlock block = ∃ (ts : List T) (acc : List Γ₀), block = hetMix ts acc ∧ ∀ g ∈ acc, g ≠ default

def TM0RealizesHetFoldBody {T Γ₀ : Type} [Inhabited Γ₀] (F : T → List (Option (T ⊕ Γ₀)) → List (Option (T ⊕ Γ₀))) : Prop

A fold body machine only needs to run on well-formed het blocks.

This is intentionally weaker than TM0RealizesBlock: the fold step erases one leading tag and then invokes the tag-specific body on the remaining hetMix ts acc. It never invokes that body on arbitrary malformed blocks.

Equations

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

While-Loop with Invariant

theorem tm0RealizesBlock_while_inv {Γ : Type} [Inhabited Γ] [DecidableEq Γ] [Fintype Γ] (step result : List Γ → List Γ) (cond : List Γ → Prop) [DecidablePred cond] (blockInv : List Γ → Prop) (hbody : TM0RealizesBlockCondInv step cond blockInv) (hinv_step : ∀ (block : List Γ), blockInv block → (∀ g ∈ block, g ≠ default) → cond block → blockInv (step block)) (hstep_nd : ∀ (block : List Γ), (∀ g ∈ block, g ≠ default) → cond block → ∀ g ∈ step block, g ≠ default) (hresult_eq : ∀ (block : List Γ), (∀ g ∈ block, g ≠ default) → blockInv block → ∃ (n : ℕ), result block = blockIterateWhile step cond n block ∧ ¬cond (blockIterateWhile step cond n block)) (_hresult_nd : ∀ (block : List Γ), (∀ g ∈ block, g ≠ default) → blockInv block → ∀ g ∈ result block, g ≠ default) : ∃ (Λ : Type) (x : Inhabited Λ) (x_1 : Fintype Λ) (M : Turing.TM0.Machine Γ Λ), ∀ (block : List Γ), blockInv block → (∀ g ∈ block, g ≠ default) → (∀ g ∈ result block, g ≠ default) → (TM0Seq.evalCfg M (block ++ [default])).Dom ∧ ∀ (h : (TM0Seq.evalCfg M (block ++ [default])).Dom), ((TM0Seq.evalCfg M (block ++ [default])).get h).Tape = Turing.Tape.mk₁ (result block ++ [default])

While-loop combinator with block invariant (empty suffix).

Like tm0RealizesBlock_while but:

• The body only needs to work on blocks satisfying blockInv
• Only empty suffix is required
• The invariant must be preserved by step

Block Realizability

@[reducible, inline]

abbrev HetFoldStepState (T : Type) (Λ : T → Type) : Type

Equations

• HetFoldStepState T Λ = (Unit ⊕ Unit ⊕ T ⊕ (t : T) × Λ t)

def HetFoldStepState.start {T : Type} {Λ : T → Type} : HetFoldStepState T Λ

Equations

• HetFoldStepState.start = Sum.inl ()

def HetFoldStepState.cont {T : Type} {Λ : T → Type} : HetFoldStepState T Λ

Equations

• HetFoldStepState.cont = Sum.inr (Sum.inl ())

def HetFoldStepState.move {T : Type} {Λ : T → Type} (t : T) : HetFoldStepState T Λ

Equations

• HetFoldStepState.move t = Sum.inr (Sum.inr (Sum.inl t))

def HetFoldStepState.run {T : Type} {Λ : T → Type} (t : T) (q : Λ t) : HetFoldStepState T Λ

Equations

• HetFoldStepState.run t q = Sum.inr (Sum.inr (Sum.inr ⟨t, q⟩))

instance HetFoldStepState.instInhabited {T : Type} {Λ : T → Type} : Inhabited (HetFoldStepState T Λ)

Equations

• HetFoldStepState.instInhabited = { default := HetFoldStepState.start }

noncomputable def tm0HetFoldStepMachine {T Γ₀ : Type} [DecidableEq T] (Λ : T → Type) [(t : T) → Inhabited (Λ t)] (M : (t : T) → Turing.TM0.Machine (Option (T ⊕ Γ₀)) (Λ t)) : Turing.TM0.Machine (Option (T ⊕ Γ₀)) (HetFoldStepState T Λ)

Equations

• One or more equations did not get rendered due to their size.
• tm0HetFoldStepMachine Λ M (Sum.inl PUnit.unit) (some (Sum.inl val)) = some (HetFoldStepState.move val, Turing.TM0.Stmt.write default)
• tm0HetFoldStepMachine Λ M (Sum.inl PUnit.unit) a = none
• tm0HetFoldStepMachine Λ M (Sum.inr (Sum.inl PUnit.unit)) a = none
• tm0HetFoldStepMachine Λ M (Sum.inr (Sum.inr (Sum.inl t))) a = some (HetFoldStepState.run t default, Turing.TM0.Stmt.move Turing.Dir.right)

theorem tm0HetFoldStepMachine_run_step {T Γ₀ : Type} [DecidableEq T] (Λ : T → Type) [(t : T) → Inhabited (Λ t)] (M : (t : T) → Turing.TM0.Machine (Option (T ⊕ Γ₀)) (Λ t)) (t : T) {c c' : Turing.TM0.Cfg (Option (T ⊕ Γ₀)) (Λ t)} (h : c' ∈ Turing.TM0.step (M t) c) : { q := HetFoldStepState.run t c'.q, Tape := c'.Tape } ∈ Turing.TM0.step (tm0HetFoldStepMachine Λ M) { q := HetFoldStepState.run t c.q, Tape := c.Tape }

theorem tm0HetFoldStepMachine_run_reaches {T Γ₀ : Type} [DecidableEq T] (Λ : T → Type) [(t : T) → Inhabited (Λ t)] (M : (t : T) → Turing.TM0.Machine (Option (T ⊕ Γ₀)) (Λ t)) (t : T) {l : List (Option (T ⊕ Γ₀))} {c : Turing.TM0.Cfg (Option (T ⊕ Γ₀)) (Λ t)} (h : Turing.Reaches (Turing.TM0.step (M t)) (Turing.TM0.init l) c) : Turing.Reaches (Turing.TM0.step (tm0HetFoldStepMachine Λ M)) { q := HetFoldStepState.run t default, Tape := Turing.Tape.mk₁ l } { q := HetFoldStepState.run t c.q, Tape := c.Tape }

theorem tm0RealizesBlockCond_hetFoldStep {T : Type} [DecidableEq T] [Fintype T] {Γ₀ : Type} [Inhabited Γ₀] (F : T → List (Option (T ⊕ Γ₀)) → List (Option (T ⊕ Γ₀))) (hf_body : TM0RealizesHetFoldBody F) : TM0RealizesBlockCondInv (hetFoldStep F) hasHetInlHead isWellFormedHetBlock

Het fold step is conditionally block-realizable (with invariant).

This is the local machine-construction obligation for one fold-body step.

theorem isWellFormedHetBlock_step {T Γ₀ : Type} [Inhabited Γ₀] (F : T → List (Option (T ⊕ Γ₀)) → List (Option (T ⊕ Γ₀))) (f : T → List Γ₀ → List Γ₀) (hF : ∀ (t : T) (ts : List T) (acc : List Γ₀), F t (hetMix ts acc) = hetMix ts (f t acc)) (hf_nd : ∀ (t : T) (block : List Γ₀), (∀ g ∈ block, g ≠ default) → ∀ g ∈ f t block, g ≠ default) (block : List (Option (T ⊕ Γ₀))) (hInv : isWellFormedHetBlock block) (hblock : ∀ g ∈ block, g ≠ default) (hcond : hasHetInlHead block) : isWellFormedHetBlock (hetFoldStep F block)

isWellFormedHetBlock is preserved by hetFoldStep when the condition holds.

theorem hetFoldWhile_eq_iterateWhile_wf {T Γ₀ : Type} [Inhabited Γ₀] (F : T → List (Option (T ⊕ Γ₀)) → List (Option (T ⊕ Γ₀))) (f : T → List Γ₀ → List Γ₀) (hF : ∀ (t : T) (ts : List T) (acc : List Γ₀), F t (hetMix ts acc) = hetMix ts (f t acc)) (block : List (Option (T ⊕ Γ₀))) (hInv : isWellFormedHetBlock block) : ∃ (n : ℕ), hetFoldWhile F block = blockIterateWhile (hetFoldStep F) hasHetInlHead n block ∧ ¬hasHetInlHead (blockIterateWhile (hetFoldStep F) hasHetInlHead n block)

hetFoldWhile equals an iteration that has actually stopped on well-formed blocks. The semantic hF is the important assumption: each successful step removes one leading tag from the hetMix block.

theorem tm0RealizesBlock_hetFoldWhile_inv {T : Type} [DecidableEq T] [Fintype T] {Γ₀ : Type} [Inhabited Γ₀] [DecidableEq Γ₀] [Fintype Γ₀] (F : T → List (Option (T ⊕ Γ₀)) → List (Option (T ⊕ Γ₀))) (f : T → List Γ₀ → List Γ₀) (hF : ∀ (t : T) (ts : List T) (acc : List Γ₀), F t (hetMix ts acc) = hetMix ts (f t acc)) (hf_body : TM0RealizesHetFoldBody F) (hF_nd : ∀ (t : T) (block : List (Option (T ⊕ Γ₀))), (∀ g ∈ block, g ≠ default) → ∀ g ∈ F t block, g ≠ default) (hf_nd : ∀ (t : T) (block : List Γ₀), (∀ g ∈ block, g ≠ default) → ∀ g ∈ f t block, g ≠ default) : ∃ (Λ : Type) (x : Inhabited Λ) (x_1 : Fintype Λ) (M : Turing.TM0.Machine (Option (T ⊕ Γ₀)) Λ), ∀ (block : List (Option (T ⊕ Γ₀))), isWellFormedHetBlock block → (∀ g ∈ block, g ≠ default) → (∀ g ∈ hetFoldWhile F block, g ≠ default) → (TM0Seq.evalCfg M (block ++ [default])).Dom ∧ ∀ (h : (TM0Seq.evalCfg M (block ++ [default])).Dom), ((TM0Seq.evalCfg M (block ++ [default])).get h).Tape = Turing.Tape.mk₁ (hetFoldWhile F block ++ [default])

Het fold while loop machine exists for well-formed blocks.

Derived from:

• a supplied conditional body machine for hetFoldStep
• tm0RealizesBlock_while_inv (while-loop combinator with invariant)
• hetFoldWhile_eq_iterateWhile_wf (iteration equals definition)

theorem isWellFormedHetBlock_map_inl_sep {T Γ₀ : Type} [Inhabited Γ₀] (w : List T) : isWellFormedHetBlock (List.map (some ∘ Sum.inl) w ++ [hetSep])

w.map (some ∘ Sum.inl) ++ [hetSep] forms a well-formed het block.

theorem isWellFormedHetBlock_reverse_map_inl_sep {T Γ₀ : Type} [Inhabited Γ₀] (w : List T) : isWellFormedHetBlock ((List.map (some ∘ Sum.inl) w).reverse ++ [hetSep])

Reversed well-formed het block is still well-formed.

Deriving the Original Fold Spec

theorem tm0Het_fold_blockRealizable' (T : Type) [DecidableEq T] [Fintype T] {Γ₀ : Type} [Inhabited Γ₀] [DecidableEq Γ₀] [Fintype Γ₀] (F : T → List (Option (T ⊕ Γ₀)) → List (Option (T ⊕ Γ₀))) (f : T → List Γ₀ → List Γ₀) (hF : ∀ (t : T) (ts : List T) (acc : List Γ₀), F t (hetMix ts acc) = hetMix ts (f t acc)) (hf_body : TM0RealizesHetFoldBody F) (hF_nd : ∀ (t : T) (block : List (Option (T ⊕ Γ₀))), (∀ g ∈ block, g ≠ default) → ∀ g ∈ F t block, g ≠ default) (hf_nd : ∀ (t : T) (block : List Γ₀), (∀ g ∈ block, g ≠ default) → ∀ g ∈ f t block, g ≠ default) : ∃ (Λ : Type) (x : Inhabited Λ) (x_1 : Fintype Λ) (M : Turing.TM0.Machine (Option (T ⊕ Γ₀)) Λ), ∀ (w : List T), (TM0Seq.evalCfg M (List.map (some ∘ Sum.inl) w)).Dom ∧ ∀ (h : (TM0Seq.evalCfg M (List.map (some ∘ Sum.inl) w)).Dom), ((TM0Seq.evalCfg M (List.map (some ∘ Sum.inl) w)).get h).Tape = Turing.Tape.mk₁ (List.map (some ∘ Sum.inr) (List.foldr f [] w))