Quantifier-free logical transductions

A quantifier-free logical transduction maps strings to strings by a copy set and, per copy, an ordered list of guarded output clauses, where each guard is a Subregular.WindowFormula 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.
• Transduction.relabel: the one-copy relabelling transduction of a quantifier-free docking process (Subregular.Docking.ofQF) over a finite alphabet.

Main results

• Transduction.emitAt_eq_of_agree: a left-local transduction emits the same block at positions whose bounded left contexts agree.
• Transduction.apply_relabel: on words over the alphabet, the relabelling transduction of a quantifier-free docking process computes its map.

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.

References

• [Cha14a]
• [CJ19]

@[reducible, inline]

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

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

Equations

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

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

A quantifier-free order-preserving logical transduction has 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 β

Running the transduction emits, 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 ∈ T.clause c, Subregular.WindowFormula.BackBounded r cl.1

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 ≤ r, w[n - j]? = w'[n' - j]?) (hedge : ∀ 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.

Relabelling transductions

theorem Subregular.WindowFormula.realize_label_var_iff {α : Type u_1} [DecidableEq α] {w : List α} {n : ℕ} {a : α} : Realize w n (label a Walk.var) ↔ w[n]? = some a

def Subregular.Transduction.relabel {α : Type u_1} (φ : WindowFormula α) (dock : α → α) (alphabet : List α) : Transduction α α

The one-copy relabelling transduction of a quantifier-free docking process over the symbols alphabet has, for each symbol, a clause docking it under the guard and then a faithful clause.

Equations

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

theorem Subregular.Transduction.apply_relabel {α : Type u_1} [DecidableEq α] {φ : WindowFormula α} {dock : α → α} {alphabet w : List α} (hw : ∀ a ∈ w, a ∈ alphabet) : (relabel φ dock alphabet).apply w = (Docking.ofQF φ dock).map w

On a word over the alphabet, the relabelling transduction computes the docking map.

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