Local Phonological Rewrite Rules

A local rewrite rule is a triple (target, effect, context) that specifies a featurally-conditioned transformation of segment strings. The canonical SPE notation A → B / C __ D originates with @cite{chomsky-halle-1968} The Sound Pattern of English; the formal-language characterization of ordered SPE-rule cascades as regular relations is @cite{johnson-1972} and @cite{kaplan-kay-1994}. Pedagogical exposition: @cite{hayes-2009} Ch 6. The notation denotes the function "every segment matching natural class A becomes B when preceded by context C and followed by context D."

Theoretical framing (2026)

Local rewrite rules are not a theory of phonology in the 2026 sense — the cognitive-theory claim that ordered rules with extrinsic ordering correctly model phonological grammars is a 1960s framing largely superseded by Optimality Theory (OptimalityTheory/) and its constraint-based descendants. What survives in 2026 mainstream computational phonology is the formal-language-theoretic role: local rewrite rules characterize a particular subclass of regular relations — specifically the Input Strictly Local (ISL) functions of @cite{chandlee-2014} @cite{chandlee-heinz-2018}.

This file therefore frames Rule as a convenient surface notation for local maps, with the formal claim grounded in Core/Computability/Subregular/Function/ISL.lean. The connection is made explicit by Rule.apply_isInputStrictlyLocal (currently a documented sorry — the construction of the witness ISLRule requires careful handling of word-boundary contexts via the augmented alphabet Option Segment, deferred to a follow-up PR).

Sibling architectures

Framework	Key file	Relation to LocalRewrite
Tier-based alternation	Process/Alternation.lean	TierRule (Belth 2026); a single tier-adjacent context LocalRewrite.Rule is subsumed by TierRule (subsumption bridge deferred).
Optimality Theory	OptimalityTheory/	Constraint-ranking (parallel evaluation); SPE-vs-OT is the central theoretical fault line of late-20th-century phonology.
Harmonic Serialism	Core/Constraint/OT/HarmonicSerialism.lean	Iterative constraint-based; named in HS docstring as architecturally-distinct alternative for counterfeeding.
Stratal OT	OptimalityTheory/Stratal.lean	Constraint-ranking within strata, with extrinsic strata ordering — keeps SPE-style derivationality at the stratum boundary.
Output-driven (OSL/WD)	Core/Computability/Subregular/Function/{OSL,Hierarchy}.lean	Iterative spreading and bidirectional harmony — strictly above the ISL class that LocalRewrite occupies.

What this file does NOT cover

• Alpha-notation / agreement variables — the SPE [α voice] → [α voice] device for assimilation. The current schema cannot state Yawelmani vowel harmony, Sanskrit ruki, or Turkish backness/rounding harmony as single rules without explosion.
• Insertion / metathesis / coalescence — Effect covers only feature change and deletion. SPE rules of the form ∅ → V / __ (epenthesis) or AB → BA (metathesis) are not expressible.
• Iterative / directional application — apply is single-pass simultaneous. Iterative left-to-right or right-to-left application (Howard 1972, Johnson 1972) requires a different architecture; the modern subregular characterization places iterative spreading in the Output Strictly Local class (Function/OSL.lean), which is strictly above ISL.
• Cyclic / stratal application — handled in OptimalityTheory/Stratal.lean.
• Tone, autosegmental representations — Jardine 2016 shows tone phenomena are non-subsequential; out of scope for any subregular function class. See Theories/Phonology/Autosegmental/.

Main definitions

• ContextElem — segment pattern or word boundary.
• Effect — feature merge or deletion.
• Rule — target / effect / leftContext / rightContext schema.
• Rule.apply — left-to-right scan, simultaneous application.
• derive — ordered-rule cascade (extrinsic ordering).

This file replaces Process/RuleBased/Defs.lean (deleted), which framed the substrate as "the SPE rule formalism following Hayes Ch 6."

inductive Phonology.LocalRewrite.ContextElem : Type

An element of a rule's structural description. Context positions hold either a segment pattern (a natural class via Segment partial specification) or a word boundary marker.

• seg : Segment → ContextElem

  A segment matching a natural-class pattern.

• wordBoundary : ContextElem

  A word boundary (Hayes notation: ]word or #).

inductive Phonology.LocalRewrite.Effect : Type

The structural change effected by a rule.

• changeFeatures : Segment → Effect

  Merge a feature bundle into the target segment. SPE notation: A → B where B is a partial specification.

• delete : Effect

  Delete the target segment. SPE notation: A → ∅.

def Phonology.LocalRewrite.Effect.apply (e : Effect) (s : Segment) : Option Segment

Apply an effect to a target segment. Returns none if the segment is deleted; some s' if features are merged into s'.

Equations

• (Phonology.LocalRewrite.Effect.changeFeatures change).apply s = some (s.applyChanges change)
• Phonology.LocalRewrite.Effect.delete.apply s = none

structure Phonology.LocalRewrite.Rule : Type

A local rewrite rule in SPE notation A → B / C __ D.

• target — natural class A matched by the affected segment.
• effect — structural change B: feature merge or deletion.
• leftContext — preceding context C, ordered left-to-right (so the rightmost element is closest to the target).
• rightContext — following context D, ordered left-to-right.

The name field is informational.

• name : String
• target : Segment
• effect : Effect
• leftContext : List ContextElem
• rightContext : List ContextElem

def Phonology.LocalRewrite.matchRightContext : List ContextElem → List Segment → Bool

Match a right-context list against the suffix right to the right of the current position. Both lists are scanned head-to-head: right's head is the segment immediately following the target.

Equations

• Phonology.LocalRewrite.matchRightContext [] x✝ = true
• Phonology.LocalRewrite.matchRightContext (Phonology.LocalRewrite.ContextElem.wordBoundary :: rest) [] = Phonology.LocalRewrite.matchRightContext rest []
• Phonology.LocalRewrite.matchRightContext (Phonology.LocalRewrite.ContextElem.wordBoundary :: tail) (head :: tail_1) = false
• Phonology.LocalRewrite.matchRightContext (Phonology.LocalRewrite.ContextElem.seg p :: rest) (s :: rs) = (s.matchesPattern p && Phonology.LocalRewrite.matchRightContext rest rs)
• Phonology.LocalRewrite.matchRightContext (Phonology.LocalRewrite.ContextElem.seg a :: tail) [] = false

def Phonology.LocalRewrite.matchLeftContext (ctx : List ContextElem) (left : List Segment) : Bool

Match a left-context list against the prefix left to the left of the current position. Context elements are ordered left-to-right (so the rightmost element is closest to the target); we reverse both lists once and then scan head-to-head.

Equations

• Phonology.LocalRewrite.matchLeftContext ctx left = Phonology.LocalRewrite.matchRightContext ctx.reverse left.reverse

def Phonology.LocalRewrite.Rule.apply (r : Rule) (input : List Segment) : List Segment

Apply a single rule to a segment string. Scans left-to-right; at every position where the target and contexts match, applies the effect. Application is simultaneous: context matches are evaluated against the input (the prefix left accumulates original segments, not their post-rule values), per the SPE default (@cite{chomsky-halle-1968} p. 344; @cite{chandlee-heinz-2018} §5.1).

The recursion is structural on right (the unprocessed suffix), so Rule.apply reduces cleanly under decide for finite inputs.

Equations

• r.apply input = Phonology.LocalRewrite.Rule.apply.go r [] input

def Phonology.LocalRewrite.Rule.apply.go (r : Rule) : List Segment → List Segment → List Segment

Equations

• One or more equations did not get rendered due to their size.
• Phonology.LocalRewrite.Rule.apply.go r a✝ [] = []

def Phonology.LocalRewrite.derive (rules : List Rule) (input : List Segment) : List Segment

Apply an ordered sequence of rules. Each rule sees the output of the previous rule (extrinsic ordering, the SPE convention).

Equations

• Phonology.LocalRewrite.derive rules input = List.foldl (fun (s : List Phonology.Segment) (r : Phonology.LocalRewrite.Rule) => r.apply s) input rules

Headline classification (deferred)

Every Rule.apply is conjecturally a k-Left-ISL function in the sense of @cite{chandlee-heinz-2018}, where k = r.leftContext.length + r.rightContext.length + 1. The construction exhibits an ISLRule k (Option Segment) (Option Segment) whose windowOutput:

1. Augments input to List (Option Segment) with none as the word boundary (mirroring Subregular/Basic.lean's Augmented α pattern).
2. Fires the rule when the window's central position matches target and the surrounding window matches both contexts (wordBoundary ↦ none).
3. For rules with right context of length n, the FST emits output delayed by n symbols (Chandlee-Heinz §4 simulation; see Function/Hierarchy.lean::ISLRule.toSFST for the analogous simulation pattern at the abstract level).
4. Strips boundary markers from the output to recover List Segment.

The theorem is not stated in this PR rather than stated with sorry — the right-context output-delay construction is non-trivial and the audit (mathlib reviewer B2) flagged the previous sorry'd shape (∃ k, IsInputStrictlyLocal k (fun input : List (Option Segment) => …)) as malformed: the function should live over List Segment directly with boundary handling internalised, and the existential k should be the explicit r.leftContext.length + r.rightContext.length + 1. Land the witness construction in a dedicated Theories/Phonology/Process/ LocalRewriteISL.lean follow-up file once a Studies consumer needs the explicit classification (the MeinhardtEtAl2024.lean Studies file demonstrates substrate use without going through Rule.apply).