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 [CH68]; the characterization of ordered SPE-rule cascades as regular relations is [Joh72], [KK94], with pedagogical exposition in [Hay09].

In the modern subregular setting these rules are a surface notation for the Input Strictly Local (ISL) functions of [Cha14a], [CH18], 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 or deletion.
• Rule — the target / effect / leftContext / rightContext schema.
• 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 — a context of length n reads at most n symbols, so both matchers factor through a bounded window.
• Rule.isLeftInputStrictlyLocal — a rule with no right context is (|leftContext| + 1)-Left-ISL.
• Rule.isLeftSubsequential — over a finite segment alphabet every rule is Left-Subsequential, via a transducer that delays emission by |rightContext| symbols and flushes the buffer at the word end.

Implementation notes

Application is single-pass and simultaneous: context matches are evaluated against the input, not the partially-rewritten output ([CH68], [CH18]). Effect covers only feature change and deletion, so insertion, metathesis, coalescence, and alpha-notation agreement variables are not expressible, and application is neither iterative/directional nor cyclic. Iterative spreading lies in the strictly larger Output Strictly Local class (Subregular.OSLRule).

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.leftContext.length + r.rightContext.length + 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 an empty right context 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

  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 Subregular.LocalRewrite.Effect.apply (e : Effect) (s : Phonology.Segment) : Option Phonology.Segment

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

Equations

• (Subregular.LocalRewrite.Effect.changeFeatures change).apply s = some (Features.Bundle.merge change s)
• Subregular.LocalRewrite.Effect.delete.apply s = none

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 — 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 : Phonology.Segment
• effect : Effect
• leftContext : List ContextElem
• rightContext : List ContextElem

Context matching

def Subregular.LocalRewrite.matchRightContext : List ContextElem → List Phonology.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

• 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

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

• 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

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 in the SPE sense (convention (39), [CH68] p. 344): contexts are matched against the input, not the partially-rewritten output — the prefix left accumulates the original segments, so a rule's own output never feeds its later matches. Cf. [CH18].

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

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

The output block a rule contributes at one position: 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.leftContext.length) s d = r.verdict w s d

The verdict reads only the last |leftContext| 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.rightContext.length ≤ d.length) : r.verdict w s (d ++ e) = r.verdict w s d

The verdict reads only the first |rightContext| symbols of the suffix.

The bounded-window scan

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

Rule.apply rewritten to carry only the last |leftContext| input symbols: the unbounded prefix of Rule.apply.go is replaced by the window the rule can actually inspect.

Equations

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

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

Truncating the prefix to the rule's left-context length 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 context: Input Strict Locality

With rightContext = [] a verdict depends only on the last |leftContext| input symbols and the current one — exactly the (|leftContext| + 1)-ISL window of [Cha14a], [CH18].

def Subregular.LocalRewrite.Rule.toISLRule (r : Rule) (_h : r.rightContext = []) : ISLRule (r.leftContext.length + 1) Phonology.Segment Phonology.Segment

The ISL rule computing a rewrite with no right context. The hypothesis is the applicability condition: with a nonempty rightContext 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.rightContext = []) : (r.toISLRule h).apply = r.apply

theorem Subregular.LocalRewrite.Rule.isLeftInputStrictlyLocal (r : Rule) (h : r.rightContext = []) : IsLeftInputStrictlyLocal (r.leftContext.length + 1) r.apply

A rewrite rule with no right context is Left-ISL, with k one more than the length of its left context.

The general case: left-subsequentiality

A nonempty right context is lookahead, which a left-to-right scan cannot have. The transducer buys it with delay: it leaves the last |rightContext| 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: the left window of the oldest undecided segment, paired with the lookahead buffer of segments whose right context is still incomplete.

Equations

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

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; 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: 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 [Hay09], so it is finite but carries no Fintype instance (its Flat slots are deliberately opaque); the hypothesis supplies the finite alphabet [Moh97] assumes without forcing a 3 ^ 26-element enumeration on every consumer of this file.