Documentation

Linglib.Phonology.Subregular.LocalityBridge

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 Term.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.

Main results #

source
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: 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 }
Instances For
    source
    theorem Subregular.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): 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 #

    source
    @[instance_reducible]
    instance Subregular.instDecidableEqSym_2 :
    DecidableEq Subregular.Sym✝
    Equations