The locality bridge: quantifier-free ⟹ strictly local

The load-bearing subregular result ([Cha14a], [CJ19]): a quantifier-free logical transduction whose guards look only at a bounded context is strictly local. Here we prove the left-directed half against Subregular's IsLeftInputStrictlyLocal: a transduction whose guards are backward (built from the variable and predecessors, no successor) with predecessor depth ≤ r is IsLeftInputStrictlyLocal (r + 1).

The mathematical crux is Term.eval_backward: a backward term of predecessor depth j, evaluated at position n, reads exactly position n - j (or falls off the left edge). Hence the truth of a backward guard at n depends only on the r + 1 symbols ending at n — the ISL window.

Main definitions

• Term.Backward / Term.pdepth — successor-free terms and their predecessor depth.
• Atom.Backward / QF.Backward / Transduction.LeftLocal — the bounded-left-context classes.

Main results

• Term.eval_backward — a backward term of depth j at position n evaluates to n - j.
• Transduction.leftLocal_isLeftISL — a backward-bounded (radius r) transduction is (r+1)-Left-Input-Strictly-Local.

Backward terms

Term.Backward and Term.pdepth live with the Term API in Logic/QFLogic.lean.

theorem Subregular.Logic.Term.eval_backward {α : Type u_1} {w : WordModel α} {n : ℕ} (hn : n < List.length w) {t : Term (Fin 1)} : t.Backward → eval w (fun (x : Fin 1) => n) t = if t.pdepth ≤ n then some (n - t.pdepth) else none

A backward term of predecessor depth j, evaluated at position n (in range), reads exactly position n - j — defined iff j ≤ n.

Bounded-left-context formulas and transductions

def Subregular.Logic.Atom.BackBounded {α : Type u_1} {V : Type u_3} (r : ℕ) : Atom α V → Prop

An atom is backward-bounded by r if every term it uses is backward with predecessor depth ≤ r (so it reads only the r + 1 symbols ending at the variable).

Equations

• Subregular.Logic.Atom.BackBounded r (Subregular.Logic.Atom.label a t) = (t.Backward ∧ t.pdepth ≤ r)
• Subregular.Logic.Atom.BackBounded r (Subregular.Logic.Atom.eq t₁ t₂) = ((t₁.Backward ∧ t₁.pdepth ≤ r) ∧ t₂.Backward ∧ t₂.pdepth ≤ r)
• Subregular.Logic.Atom.BackBounded r (Subregular.Logic.Atom.defined t) = (t.Backward ∧ t.pdepth ≤ r)

def Subregular.Logic.QF.BackBounded {α : Type u_1} {V : Type u_3} (r : ℕ) : QF α V → Prop

A quantifier-free formula is backward-bounded by r if all its atoms are.

Equations

• Subregular.Logic.QF.BackBounded r (Subregular.Logic.QF.atom a) = Subregular.Logic.Atom.BackBounded r a
• Subregular.Logic.QF.BackBounded r Subregular.Logic.QF.tru = True
• Subregular.Logic.QF.BackBounded r Subregular.Logic.QF.fls = True
• Subregular.Logic.QF.BackBounded r φ.neg = Subregular.Logic.QF.BackBounded r φ
• Subregular.Logic.QF.BackBounded r (φ.conj ψ) = (Subregular.Logic.QF.BackBounded r φ ∧ Subregular.Logic.QF.BackBounded r ψ)
• Subregular.Logic.QF.BackBounded r (φ.disj ψ) = (Subregular.Logic.QF.BackBounded r φ ∧ Subregular.Logic.QF.BackBounded r ψ)

def Subregular.Logic.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.Logic.Transduction.LeftLocal r T = ∀ (c : Fin T.copies), ∀ cl ∈ T.clause c, Subregular.Logic.QF.BackBounded r cl.1

def Subregular.Logic.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: read 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 }

Locality of emitAt and the window-threading invariant

The bridge reduces to two facts: a backward-bounded guard reads only the r + 1 symbols ending at its position (emitAt agrees on positions with matching bounded left context), and the ISL window threaded by applyAux stays exactly that bounded left context.

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

Locality bridge (left half), [Cha14a], [CJ19]: a transduction whose guards look only backward with predecessor depth ≤ r is (r+1)-Left-Input-Strictly-Local — its output depends on a bounded left window, the defining property of strict locality.

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

@[implicit_reducible]

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

Equations

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