Quantifier-free logical transductions

String-to-string logical transductions in the quantifier-free fragment ([Cha14a], [CJ19]): a map defined by a copy set and, per copy, an ordered list of guarded output clauses, where each guard is a Subregular.QF formula at the input position. A copy set of size k lets the output be larger than the input (insertion); 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 successor formula. This is exactly the fragment relevant to strict locality — relabelling, deletion, and insertion. Non-order-preserving maps (reordering via an explicit output successor) 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, though the composite is not in general itself quantifier-free.

Main definitions

• Subregular.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).
• Transduction.LeftLocal: every guard backward-bounded by r.

Main results

• Transduction.emitAt_eq_of_agree: a left-local transduction emits the same block at positions whose bounded left contexts agree.

Implementation notes

A clause is a quantifier-free 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.Clause (α : Type u_4) (β : Type u_5) : Type (max u_4 u_5)

A per-copy output clause: a quantifier-free guard at the input position and the output symbol emitted when it is the first matching clause.

Equations

• Subregular.Clause α β = (Subregular.QF α × β)

structure Subregular.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.Transduction.emitAt {α : Type u_1} {β : Type u_2} [DecidableEq α] (T : Transduction α β) (w : List α) (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.Transduction.apply {α : Type u_1} {β : Type u_2} [DecidableEq α] (T : Transduction α β) (w : List α) : List β

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 w.length)

@[simp]

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

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

Composition of transductions — one cyclic derivation step after another; the composite is not in general itself quantifier-free.

Equations

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

Left-local transductions

def Subregular.Transduction.LeftLocal {α : Type u_1} {β : Type u_2} (r : ℕ) (T : Transduction α β) : Prop

A transduction is left-local with radius r if every clause guard is backward-bounded by r: the output at a position is determined by that position and the r symbols before it.

Equations

• Subregular.Transduction.LeftLocal r T = ∀ (c : Fin T.copies) (cl : Subregular.Clause α β), cl ∈ T.clause c → Subregular.QF.BackBounded r cl.fst

theorem Subregular.Transduction.emitAt_eq_of_agree {α : Type u_1} {β : Type u_2} [DecidableEq α] {r : ℕ} {T : Transduction α β} (hT : LeftLocal r T) {w w' : List α} {n n' : ℕ} (hn : n < w.length) (hn' : n' < w'.length) (hlbl : ∀ (j : ℕ), j ≤ r → w[n - j]? = w'[n' - j]?) (hedge : ∀ (j : ℕ), j ≤ r → (j ≤ n ↔ j ≤ n')) : T.emitAt w n = T.emitAt w' n'

A left-local transduction emits the same block at positions whose bounded left contexts agree: every clause guard is backward-bounded, so its firing is determined by that context.

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

@[instance_reducible]

instance Subregular.instDecidableEqSym_1 : DecidableEq Subregular.Sym✝

Equations

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