The subregular function hierarchy

Inclusions among the directionality classes of Core/Computability/Subregular/Function/, assembled from the strictly-local, synchronous-subsequential (LetterSubsequential) and bimachine (Bimachine) substrate:

single-symbol ISL/OSL ⊆ IsLetterLeftSubsequential ⊆ IsBimachineWeaklyDeterministic ⊆ IsBimachineComputable

A left-subsequential transducer is the degenerate bimachine whose right automaton is trivial, so its cell output is a one-sided rule — non-interacting.

Main results

• IsBimachineWeaklyDeterministic.of_letterLeftSubsequential — subsequential ⊆ WD.
• IsBimachineComputable.of_weaklyDeterministic — WD ⊆ regular.
• weaklyDeterministic_strict_subset_regular — WD ⊊ regular is proper: the conjunctive change conjBM (a target raised iff a trigger occurs on both sides) is bimachine-computable but RequiresBothSides.
• isLetterLeftSubsequential_of_ISLRule / _of_OSLRule — single-symbol ISL/OSL ⊆ subsequential (the bounded window as a Mealy state); .of_ISLRule / .of_OSLRule extend the chain to WD.

TODO

• subsequential ⊊ WD is also proper, but a witness is not yet formalized here: a genuinely two-sided union is IsUnboundedCircumambient, hence not right-myopic (IsLetterLeftSubsequential.isRightMyopic), hence not left-subsequential, yet weakly deterministic.

Synchronous ⊆ block subsequential

A Mealy machine is an SFST emitting singleton blocks with an empty final flush, so the synchronous class embeds in the block class scanning the same direction.

def Subregular.Mealy.toSFST {σ : Type u_1} {α : Type u_2} {β : Type u_3} (T : Mealy σ α β) : SFST α β σ

View a synchronous transducer as a block SFST: singleton outputs, empty flush.

Equations

• T.toSFST = { start := T.initial, step := fun (s : σ) (x : α) => ((T.step s x).1, [(T.step s x).2]), finalOutput := fun (x : σ) => [] }

@[simp]

theorem Subregular.Mealy.toSFST_runFrom {σ : Type u_1} {α : Type u_2} {β : Type u_3} (T : Mealy σ α β) (s : σ) (xs : List α) : T.toSFST.runFrom s xs = T.runFrom s xs

@[simp]

theorem Subregular.Mealy.toSFST_run {σ : Type u_1} {α : Type u_2} {β : Type u_3} (T : Mealy σ α β) : T.toSFST.run = T.run

theorem Subregular.IsLetterLeftSubsequential.isLeftSubsequential {α : Type u_2} {β : Type u_3} {f : List α → List β} (hf : IsLetterLeftSubsequential f) : IsLeftSubsequential f

A letter-left-subsequential function is left-subsequential: synchronous ⊆ block.

theorem Subregular.IsBimachineWeaklyDeterministic.of_letterLeftSubsequential {α : Type u_1} [DecidableEq α] {f : List α → List α} (h : IsLetterLeftSubsequential f) : IsBimachineWeaklyDeterministic f

Subsequential ⊆ weakly deterministic. A synchronous left-subsequential function is computed by a non-interacting bimachine: the left automaton is the transducer, the right automaton is trivial, so the cell output is a one-sided rule (ωR is the identity).

theorem Subregular.IsBimachineComputable.of_weaklyDeterministic {α : Type u_1} [DecidableEq α] {f : List α → List α} (h : IsBimachineWeaklyDeterministic f) : IsBimachineComputable f

Weakly deterministic ⊆ regular. A non-interacting bimachine is a bimachine.

Strictness: WD ⊊ regular

A conjunctive change — a target raised iff a trigger occurs on both sides — is bimachine-computable but RequiresBothSides, so no non-interacting bimachine computes it.

inductive Subregular.ConjSym : Type

Toy alphabet for the conjunctive-change witness: a trigger, a recessive target, and its raised form.

• trig : ConjSym
• tgt : ConjSym
• raised : ConjSym

@[implicit_reducible]

instance Subregular.instDecidableEqConjSym : DecidableEq ConjSym

Equations

• Subregular.instDecidableEqConjSym x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Subregular.instReprConjSym : Repr ConjSym

Equations

• Subregular.instReprConjSym = { reprPrec := Subregular.instReprConjSym.repr }

def Subregular.instReprConjSym.repr : ConjSym → ℕ → Std.Format

Equations

• Subregular.instReprConjSym.repr Subregular.ConjSym.trig prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Subregular.ConjSym.trig")).group prec✝
• Subregular.instReprConjSym.repr Subregular.ConjSym.tgt prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Subregular.ConjSym.tgt")).group prec✝
• Subregular.instReprConjSym.repr Subregular.ConjSym.raised prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Subregular.ConjSym.raised")).group prec✝

@[implicit_reducible]

instance Subregular.instFintypeConjSym : Fintype ConjSym

Equations

• Subregular.instFintypeConjSym = { elems := {Subregular.ConjSym.trig, Subregular.ConjSym.tgt, Subregular.ConjSym.raised}, complete := Subregular.instFintypeConjSym._proof_1 }

def Subregular.conjBM : Bimachine Bool Bool ConjSym ConjSym

A target raises iff a trigger occurs on both sides — a flag bimachine (Bimachine.ofFlags) tracking a trigger on each side, whose cell genuinely needs both flags (l && r).

Equations

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

def Subregular.conjBase (d : ℕ) : List ConjSym

Witness word at distance d: a medial .tgt flanked by d neutral fillers and a .trig on each end. The two perturbations replace one end's .trig with a filler.

Equations

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

theorem Subregular.conjBM_requiresBothSides : RequiresBothSides conjBM.run

The conjunctive spread requires both sides: the base raises a medial target (a trigger on each side), but flipping either far trigger to a filler reverts it. The perturbations are List.sets of the base, so they agree with it off the flipped index (getElem?_set_ne), and the reverting cell output is read off via conjBM_run_at.

theorem Subregular.weaklyDeterministic_strict_subset_regular : ∃ (f : List ConjSym → List ConjSym), IsBimachineComputable f ∧ ¬IsBimachineWeaklyDeterministic f

The strictly-local lower end: single-symbol ISL/OSL ⊆ subsequential

The ISL/OSL classes are block-output (length-changing) in general, so they sit outside the length-preserving lattice. Their single-symbol (length-preserving) fragment embeds: the same bounded window that makes toFinSFST finite-state serves as a Mealy state, with the lone output symbol as the letter. This extends the chain to single-symbol ISL/OSL ⊆ subsequential ⊆ WD ⊆ regular.

def Subregular.ISLRule.toMealy {α : Type u_2} {β : Type u_3} {k : ℕ} [Fintype α] (r : ISLRule k α β) (hs : ∀ (w : List α) (x : α), (r.windowOutput w x).length = 1) : Mealy { l : List α // l.length ≤ k - 1 } α β

A length-preserving (single-symbol) left-ISL rule as a synchronous transducer: the bounded input window is the state, the lone output symbol the letter.

Equations

• r.toMealy hs = { initial := ⟨[], ⋯⟩, step := fun (w : { l : List α // l.length ≤ k - 1 }) (x : α) => (⟨(↑w ++ [x]).rtake (k - 1), ⋯⟩, (r.windowOutput (↑w) x).head ⋯) }

theorem Subregular.ISLRule.toMealy_run_eq_apply {α : Type u_2} {β : Type u_3} {k : ℕ} [Fintype α] (r : ISLRule k α β) (hs : ∀ (w : List α) (x : α), (r.windowOutput w x).length = 1) : (r.toMealy hs).run = r.apply

theorem Subregular.isLetterLeftSubsequential_of_ISLRule {α : Type u_2} {β : Type u_3} {k : ℕ} [Fintype α] (r : ISLRule k α β) (hs : ∀ (w : List α) (x : α), (r.windowOutput w x).length = 1) : IsLetterLeftSubsequential r.apply

Single-symbol left-ISL ⊆ left-subsequential.

def Subregular.OSLRule.toMealy {α : Type u_2} {β : Type u_3} {k : ℕ} (r : OSLRule k α β) (hs : ∀ (w : List β) (x : α), (r.windowOutput w x).length = 1) : Mealy { l : List β // l.length ≤ k - 1 } α β

A length-preserving (single-symbol) left-OSL rule as a synchronous transducer: the bounded output window is the state.

Equations

• r.toMealy hs = { initial := ⟨[], ⋯⟩, step := fun (w : { l : List β // l.length ≤ k - 1 }) (x : α) => (⟨(↑w ++ r.windowOutput (↑w) x).rtake (k - 1), ⋯⟩, (r.windowOutput (↑w) x).head ⋯) }

theorem Subregular.OSLRule.toMealy_run_eq_apply {α : Type u_2} {β : Type u_3} {k : ℕ} [Fintype β] (r : OSLRule k α β) (hs : ∀ (w : List β) (x : α), (r.windowOutput w x).length = 1) : (r.toMealy hs).run = r.apply

theorem Subregular.isLetterLeftSubsequential_of_OSLRule {α : Type u_2} {β : Type u_3} {k : ℕ} [Fintype β] (r : OSLRule k α β) (hs : ∀ (w : List β) (x : α), (r.windowOutput w x).length = 1) : IsLetterLeftSubsequential r.apply

Single-symbol left-OSL ⊆ left-subsequential.

theorem Subregular.IsBimachineWeaklyDeterministic.of_ISLRule {α : Type u_2} {k : ℕ} [Fintype α] [DecidableEq α] (r : ISLRule k α α) (hs : ∀ (w : List α) (x : α), (r.windowOutput w x).length = 1) : IsBimachineWeaklyDeterministic r.apply

Single-symbol left-ISL ⊆ WD — extends the lattice down through subsequential.

theorem Subregular.IsBimachineWeaklyDeterministic.of_OSLRule {α : Type u_2} {k : ℕ} [Fintype α] [DecidableEq α] (r : OSLRule k α α) (hs : ∀ (w : List α) (x : α), (r.windowOutput w x).length = 1) : IsBimachineWeaklyDeterministic r.apply

Single-symbol left-OSL ⊆ WD.