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

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 (Core/Computability/Subregular/Function/OSL.lean).

Todo

• Prove Rule.apply is a k-Left-ISL function with k = r.leftContext.length + r.rightContext.length + 1, exhibiting an ISLRule over List Segment with word boundaries internalised (cf. Core/Computability/Subregular/Function/ISL.lean).

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