Local phonological rewrite rules

A local rewrite rule is a triple (target, effect, context) denoting a featurally-conditioned transformation of segment strings. The SPE notation A → B / C __ D — "every segment matching natural class A becomes B between context C and D" — originates with Chomsky and Halle; the characterization of ordered SPE-rule cascades as regular relations is due to Johnson and to Kaplan and Kay, with pedagogical exposition in Hayes.

In the modern subregular setting these rules are a surface notation for the Input Strictly Local (ISL) functions of Chandlee and of Chandlee and Heinz, rather than a cognitive theory of phonological grammar (that role is held by constraint-based frameworks such as Phonology/OptimalityTheory/).

Main definitions

• ContextElem — a segment pattern or word boundary.
• Effect — feature merge, deletion, replacement, or assimilation of a feature class to a neighbour (SPE alpha-variables; node spreading when the class is natural).
• Rule — the target / effect / leftContext / rightContext schema, with Rule.leftReach and Rule.rightReach the input it inspects on each side.
• Rule.apply — a single left-to-right scan with simultaneous application.
• derive — an ordered-rule cascade (extrinsic ordering, the SPE convention).
• Rule.toISLRule, Rule.toSubsequentialTransducer — the two machine presentations of a rule.

Main results

• matchRightContext_take, matchLeftContext_rtake, Effect.apply_rtake, Effect.apply_append — contexts and effects read bounded windows, so a verdict factors through leftReach symbols to the left and rightReach to the right.
• Rule.length_apply, length_derive — a rule that does not delete, and a cascade of such rules, preserve the length of the word.
• Rule.isLeftInputStrictlyLocal — a rule reading nothing to its right is (leftReach + 1)-Left-ISL.
• Rule.isLeftSubsequential — over a finite segment alphabet every rule is Left-Subsequential, via a transducer that delays emission by rightReach symbols and flushes the buffer at the word end.

Implementation notes

Application is single-pass and simultaneous: context matches and copied values are read from the input, not the partially-rewritten output (Chomsky and Halle, Chandlee and Heinz). Effect covers feature change, deletion, replacement, and copying a feature class from the adjacent input segment — Chomsky and Halle's alpha-variables, which is Finset.piecewise on the class — so insertion, metathesis and coalescence are not expressible, and application is neither iterative/directional nor cyclic. Iterative spreading lies outside ISL, in the Output Strictly Local class (Subregular.OSLRule.spread_not_isLeftInputStrictlyLocal).

Todo

• Rule.apply over boundary-augmented input. Padding the string with word boundaries turns the right context into lookahead the padding pays for, and the rule becomes k-Left-ISL with k = r.leftReach + r.rightReach + 1. Over raw strings that statement does not hold in general — a bounded left window cannot see the right context — which is why Rule.isLeftInputStrictlyLocal assumes no right reach and Rule.isLeftSubsequential is what survives without it.

Context elements and effects

inductive Subregular.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 : Phonology.Segment → ContextElem

  A segment matching a natural-class pattern.

• wordBoundary : ContextElem

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

inductive Subregular.LocalRewrite.Effect : Type

The structural change effected by a rule.

• changeFeatures : Phonology.Segment → Effect

  Merging a feature bundle into the target segment, A → B in SPE notation with B a partial specification.

• delete : Effect

  Deleting the target segment, A → ∅ in SPE notation.

• replace : Phonology.Segment → Effect

  Replace the target segment by a given one, which may leave unspecified a feature the target specifies, as a change to an archiphoneme does.

• copyRight : Finset Phonology.Feature → Effect

  Assimilating the features of the class C to the following segment, which is the alpha-variable change A → [αF, βG, …] / __ [αF, βG, …] for C = {F, G, …} and the spreading of a class node when C is a natural class (Phonology/FeatureGeometry.lean).

• copyLeft : Finset Phonology.Feature → Effect

  Assimilate the features of the class C to the preceding segment.

def Subregular.LocalRewrite.Effect.leftReach : Effect → ℕ

How many segments to the left of the target an effect reads.

Equations

• (Subregular.LocalRewrite.Effect.copyLeft a).leftReach = 1
• x✝.leftReach = 0

def Subregular.LocalRewrite.Effect.rightReach : Effect → ℕ

How many segments to the right of the target an effect reads.

Equations

• (Subregular.LocalRewrite.Effect.copyRight a).rightReach = 1
• x✝.rightReach = 0

def Subregular.LocalRewrite.Effect.apply (e : Effect) (w : List Phonology.Segment) (s : Phonology.Segment) (d : List Phonology.Segment) : Option Phonology.Segment

The result of an effect on a target s standing between the prefix w and the suffix d, where none deletes the segment and a class copy takes the neighbour's values on the class, leaving the target unchanged at a word edge.

Equations

• (Subregular.LocalRewrite.Effect.changeFeatures change).apply w s d = some fun (f : Phonology.Feature) => (change f).or (s f)
• Subregular.LocalRewrite.Effect.delete.apply w s d = none
• (Subregular.LocalRewrite.Effect.replace t).apply w s d = some t
• (Subregular.LocalRewrite.Effect.copyRight C).apply w s d = some (d.head?.elim s fun (t : Phonology.Segment) => C.piecewise t s)
• (Subregular.LocalRewrite.Effect.copyLeft C).apply w s d = some (w.getLast?.elim s fun (t : Phonology.Segment) => C.piecewise t s)

theorem Subregular.LocalRewrite.Effect.apply_rtake (e : Effect) {n : ℕ} (h : e.leftReach ≤ n) (w : List Phonology.Segment) (s : Phonology.Segment) (d : List Phonology.Segment) : e.apply (w.rtake n) s d = e.apply w s d

An effect reads at most leftReach symbols of the prefix.

theorem Subregular.LocalRewrite.Effect.apply_append (e : Effect) (w : List Phonology.Segment) (s : Phonology.Segment) (d d' : List Phonology.Segment) (h : e.rightReach ≤ d.length) : e.apply w s (d ++ d') = e.apply w s d

An effect reads at most rightReach symbols of the suffix.

Rules

structure Subregular.LocalRewrite.Rule : Type

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

• target — natural class A matched by the affected segment.
• effect — the structural change B.
• 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 : Phonology.Segment
• effect : Effect
• leftContext : List ContextElem
• rightContext : List ContextElem

def Subregular.LocalRewrite.Rule.leftReach (r : Rule) : ℕ

r.leftReach is the number of input symbols to the left of the target that the rule reads, its left context and whatever its effect copies.

Equations

• r.leftReach = max r.leftContext.length r.effect.leftReach

def Subregular.LocalRewrite.Rule.rightReach (r : Rule) : ℕ

r.rightReach is the number of input symbols to the right of the target that the rule reads, its right context and whatever its effect copies.

Equations

• r.rightReach = max r.rightContext.length r.effect.rightReach

Context matching

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

Whether a right-context list matches the suffix right to the right of the current position, scanning both lists head-to-head from the segment immediately following the target.

Equations

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

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

Whether a left-context list matches 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, and both lists are reversed once and then scanned head-to-head.

Equations

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

Rule application

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

A single rule applied to a segment string, scanning left to right and applying the effect at every position where the target and contexts match. Application is simultaneous in the SPE sense (convention (39), Chomsky and Halle p. 344), matching contexts against the input rather than the partially-rewritten output. The prefix left accumulates the original segments, so a rule's own output never feeds its later matches (cf. Chandlee and Heinz).

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

Equations

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

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

Equations

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

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

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

Equations

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

Bounded context windows

A context list of length n inspects at most n symbols, so both matchers factor through a bounded window — the right one through a prefix, the left one through a suffix. The word boundary is what makes this delicate: it matches exactly when the string is exhausted, so a window must be long enough to tell a genuinely short string from a truncated one. A window of the context's own length is: it is exhausted only when the string is.

theorem Subregular.LocalRewrite.matchRightContext_take (ctx : List ContextElem) (right : List Phonology.Segment) : matchRightContext ctx (List.take ctx.length right) = matchRightContext ctx right

theorem Subregular.LocalRewrite.matchLeftContext_rtake (ctx : List ContextElem) (left : List Phonology.Segment) : matchLeftContext ctx (left.rtake ctx.length) = matchLeftContext ctx left

theorem Subregular.LocalRewrite.matchLeftContext_rtake_of_le (ctx : List ContextElem) {n : ℕ} (h : ctx.length ≤ n) (left : List Phonology.Segment) : matchLeftContext ctx (left.rtake n) = matchLeftContext ctx left

Any window at least as long as the context reads the same.

theorem Subregular.LocalRewrite.matchRightContext_append_of_le (ctx : List ContextElem) {d : List Phonology.Segment} (d' : List Phonology.Segment) (h : ctx.length ≤ d.length) : matchRightContext ctx (d ++ d') = matchRightContext ctx d

A suffix at least as long as the context reads the same as its extensions.

The verdict at a position

def Subregular.LocalRewrite.Rule.verdict (r : Rule) (w : List Phonology.Segment) (s : Phonology.Segment) (d : List Phonology.Segment) : List Phonology.Segment

r.verdict w s d is the output block the rule contributes at one position, which is the effect applied when target, left context w and right context d all match, and the untouched segment otherwise.

Equations

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

theorem Subregular.LocalRewrite.Rule.apply_go_cons (r : Rule) (left : List Phonology.Segment) (s : Phonology.Segment) (right : List Phonology.Segment) : apply.go r left (s :: right) = r.verdict left s right ++ apply.go r (left ++ [s]) right

Rule.apply emits one Rule.verdict per input position.

theorem Subregular.LocalRewrite.Rule.verdict_rtake (r : Rule) (w : List Phonology.Segment) (s : Phonology.Segment) (d : List Phonology.Segment) : r.verdict (w.rtake r.leftReach) s d = r.verdict w s d

The verdict reads only the last leftReach symbols of the prefix.

theorem Subregular.LocalRewrite.Rule.verdict_append (r : Rule) (w : List Phonology.Segment) (s : Phonology.Segment) (d e : List Phonology.Segment) (h : r.rightReach ≤ d.length) : r.verdict w s (d ++ e) = r.verdict w s d

The verdict reads only the first rightReach symbols of the suffix.

Length

A rule whose effect is not deletion rewrites each segment to one segment.

theorem Subregular.LocalRewrite.Effect.isSome_apply {e : Effect} (h : e ≠ delete) (w : List Phonology.Segment) (s : Phonology.Segment) (d : List Phonology.Segment) : (e.apply w s d).isSome = true

An effect other than deletion yields a segment.

theorem Subregular.LocalRewrite.Rule.length_verdict {r : Rule} (h : r.effect ≠ Effect.delete) (w : List Phonology.Segment) (s : Phonology.Segment) (d : List Phonology.Segment) : (r.verdict w s d).length = 1

theorem Subregular.LocalRewrite.Rule.length_apply {r : Rule} (h : r.effect ≠ Effect.delete) (input : List Phonology.Segment) : (r.apply input).length = input.length

A rule that does not delete preserves the length of the word.

theorem Subregular.LocalRewrite.length_derive {rules : List Rule} (h : ∀ r ∈ rules, r.effect ≠ Effect.delete) (input : List Phonology.Segment) : (derive rules input).length = input.length

A cascade of rules that do not delete preserves the length of the word.

The bounded-window scan

def Subregular.LocalRewrite.Rule.scan (r : Rule) (w : List Phonology.Segment) : List Phonology.Segment → List Phonology.Segment

r.scan is Rule.apply rewritten to carry only the last leftReach input symbols, the window the rule can inspect, in place of the unbounded prefix of Rule.apply.go.

Equations

• r.scan w [] = []
• r.scan w (s :: right) = r.verdict w s right ++ r.scan ((w ++ [s]).rtake r.leftReach) right

theorem Subregular.LocalRewrite.Rule.scan_rtake (r : Rule) (left right : List Phonology.Segment) : r.scan (left.rtake r.leftReach) right = apply.go r left right

Truncating the prefix to the rule's left reach loses nothing.

theorem Subregular.LocalRewrite.Rule.apply_eq_scan (r : Rule) : r.apply = r.scan []

Rule.apply is the bounded-window scan started from the empty window.

No right reach: Input Strict Locality

A rule that reads nothing to its right — no right context and no copy from the right — has a verdict depending only on the last leftReach input symbols and the current one, exactly the (leftReach + 1)-ISL window of Chandlee and of Chandlee and Heinz.

def Subregular.LocalRewrite.Rule.toISLRule (r : Rule) (_h : r.rightReach = 0) : ISLRule (r.leftReach + 1) Phonology.Segment Phonology.Segment

The ISL rule computing a rewrite with no right reach. The hypothesis is the applicability condition, since with a positive right reach the lookahead [] supplied here is the end-of-word one, not the one Rule.apply uses.

Equations

• r.toISLRule _h = { windowOutput := fun (w : List Phonology.Segment) (s : Phonology.Segment) => r.verdict w s [] }

theorem Subregular.LocalRewrite.Rule.toISLRule_apply (r : Rule) (h : r.rightReach = 0) : (r.toISLRule h).apply = r.apply

theorem Subregular.LocalRewrite.Rule.isLeftInputStrictlyLocal (r : Rule) (h : r.rightReach = 0) : IsLeftInputStrictlyLocal (r.leftReach + 1) r.apply

A rewrite rule with no right reach is Left-ISL, with k one more than its left reach.

The general case: left-subsequentiality

A positive right reach is lookahead, which a left-to-right scan cannot have. The transducer buys it with delay: it leaves the last rightReach segments unjudged in a buffer, so that the oldest buffered segment always has its full right context in hand, and judges what remains buffered against the word end in finalOutput. That final flush is what the right context costs — ofWindow, and with it every ISL rule, emits nothing at the end.

@[reducible, inline]

abbrev Subregular.LocalRewrite.Rule.State (r : Rule) : Type

The delayed-emission state, pairing the left window of the oldest undecided segment with the lookahead buffer of segments whose right context is still incomplete.

Equations

• r.State = ({ l : List Phonology.Segment // l.length ≤ r.leftReach } × { l : List Phonology.Segment // l.length ≤ r.rightReach })

def Subregular.LocalRewrite.Rule.toSubsequentialTransducer (r : Rule) : SubsequentialTransducer r.State Phonology.Segment Phonology.Segment

The delayed transducer for an arbitrary rewrite rule. Reading x appends it to the buffer, and whatever that pushes out of the buffer has acquired its full right context, so it is judged and enters the left window. finalOutput judges the remaining buffer against the end of the word, where a short lookahead is exactly what matchRightContext expects.

Equations

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

theorem Subregular.LocalRewrite.Rule.runFrom_toSubsequentialTransducer (r : Rule) (s : r.State) (input : List Phonology.Segment) : r.toSubsequentialTransducer.runFrom s input = r.scan (↑s.1) (↑s.2 ++ input)

From any state the delayed transducer judges the buffer and the remaining input together, so the delay is invisible in the total output.

theorem Subregular.LocalRewrite.Rule.run_toSubsequentialTransducer (r : Rule) : r.toSubsequentialTransducer.run = r.apply

The delayed transducer computes the rule.

theorem Subregular.LocalRewrite.Rule.isLeftSubsequential [Fintype Phonology.Segment] (r : Rule) : IsLeftSubsequential r.apply

Every local rewrite rule is Left-Subsequential. Segment is a partial valuation of the 26 features of Hayes, so it is finite but carries no Fintype instance (its Flat slots are deliberately opaque), and the hypothesis supplies the finite alphabet Mohri assumes without forcing a 3 ^ 26-element enumeration on every consumer of this file.