The locality bridge: left-local ⟹ input strictly local

A local transduction whose guards look only at a bounded left context is input strictly local: a transduction that is LeftLocal r (guards backward-bounded by r) is IsLeftInputStrictlyLocal (r + 1).

The mathematical crux is upstream (Transduction.emitAt_eq_of_agree, resting on Walk.eval_backward): a left-local transduction emits the same block at positions whose bounded left contexts agree. This file threads that fact through the ISL window: the window maintained by ISLRule.applyAux stays exactly the bounded left context, so the induced rule reproduces the transduction's output. This is the direction of the correspondence between quantifier-free transductions and input strictly local functions by which a definition reading only predecessors is input strictly local.

Main results

• Transduction.toISLRule: the ISL rule induced by a left-local transduction.
• Transduction.leftLocal_isLeftISL: a LeftLocal r transduction is (r+1)-Left-Input-Strictly-Local.

References

• [Cha14a]
• [CJ19]

def Subregular.Transduction.toISLRule {α : Type u_1} {β : Type u_2} [DecidableEq α] (T : Transduction α β) (r : ℕ) : ISLRule (r + 1) α β

The Left-ISL rule induced by a left-local transduction of radius r reads the output block at each position from the last r input symbols (window) and the current symbol x, by running the transduction's emitAt on window ++ [x] at its final position.

Equations

• T.toISLRule r = { windowOutput := fun (window : List α) (x : α) => T.emitAt (window ++ [x]) window.length }

theorem Subregular.Transduction.leftLocal_isLeftISL {α : Type u_1} {β : Type u_2} [DecidableEq α] {r : ℕ} {T : Transduction α β} (hT : LeftLocal r T) : IsLeftInputStrictlyLocal (r + 1) T.apply

A transduction whose guards look only backward with predecessor depth ≤ r is (r+1)-Left-Input-Strictly-Local, its output depending on a bounded left window.

Worked example: the bridge on a concrete left-local process