Logical transductions

Quantifier-free graph-to-graph logical transductions: a map from an input word model to an output word model, defined by a copy set and, per copy, output formulas (φ_lab(xᶜ)). A copy set of size k lets the output be larger than the input (insertion); per-copy guards that match nothing delete; relabelling copies rewrite a symbol in place.

We formalize the order-preserving fragment: the output is read off in the order (input position, copy index), so the output successor is induced rather than given by an explicit φ_succ(xᶜ, yᵈ). This is exactly the local fragment relevant to strict locality — relabelling, deletion, and insertion. Non-order-preserving maps (reordering via an explicit successor formula) are the non-local extension and are deliberately out of scope here.

Composition of transductions (applyComp) models an iterated derivation: each step is a local transduction; the composite is a regular function (closed under composition in SFST) though not in general itself quantifier-free.

Main definitions

• Subregular.Logic.Transduction — copy count + per-copy guarded output clauses.
• Transduction.apply — run a transduction, producing the output string (computable).
• Transduction.applyComp — composition of two transductions (one cyclic derivation step on top of another).

Implementation notes

A clause is a one-variable QF guard paired with an output symbol; per copy, the first clause whose guard holds at the input position fires, and a copy with no firing clause is absent. apply is a flatMap over input positions then copies, so it reduces under decide.

@[reducible, inline]

abbrev Subregular.Logic.Clause (α : Type u_4) (β : Type u_5) : Type (max u_4 u_5)

A per-copy output clause: a quantifier-free guard (one variable, the input position) and the output symbol emitted when it is the first matching clause.

Equations

• Subregular.Logic.Clause α β = (Subregular.Logic.QF α (Fin 1) × β)

structure Subregular.Logic.Transduction (α : Type u_4) (β : Type u_5) : Type (max u_4 u_5)

A quantifier-free order-preserving logical transduction: copies output copies of each input position, and for each copy an ordered list of guarded output clauses.

• copies : ℕ
• clause : Fin self.copies → List (Clause α β)

def Subregular.Logic.Transduction.emitAt {α : Type u_1} {β : Type u_2} [DecidableEq α] (T : Transduction α β) (w : WordModel α) (n : ℕ) : List β

The output symbols emitted at input position n (one per copy whose guard fires, in copy order).

Equations

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

def Subregular.Logic.Transduction.apply {α : Type u_1} {β : Type u_2} [DecidableEq α] (T : Transduction α β) (w : WordModel α) : WordModel β

Run the transduction: emit, left to right, the licensed copies of every input position.

Equations

• T.apply w = List.flatMap (T.emitAt w) (List.range (List.length w))

@[simp]

theorem Subregular.Logic.Transduction.apply_nil {α : Type u_1} {β : Type u_2} [DecidableEq α] (T : Transduction α β) : T.apply [] = []

def Subregular.Logic.Transduction.applyComp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [DecidableEq α] (T₂ : Transduction β γ) (T₁ : Transduction α β) [DecidableEq β] (w : WordModel α) : WordModel γ

Composition of transductions — one cyclic derivation step after another. The composite is a regular function (closed under composition in SFST), though not in general quantifier-free.

Equations

• T₂.applyComp T₁ w = T₂.apply (T₁.apply w)

Worked examples: feature change, deletion, epenthesis, and a cycle

@[implicit_reducible]

instance Subregular.Logic.instDecidableEqSym_1 : DecidableEq Subregular.Logic.Sym✝

Equations

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