SPE Phonological Rules

Rule-based phonology following the SPE formalism, as presented in @cite{hayes-2009} Introductory Phonology, Chapter 6.

The core notation is A → B / C __ D: a segment matching natural class A undergoes structural change B when preceded by context C and followed by context D.

Design: We reuse Segment (a partial feature specification) as both concrete segment and natural class descriptor. An underspecified segment (many features none) IS a natural class — no separate pattern type needed.

This module provides:

• Segment construction and natural class matching utilities
• PhonRule: the SPE rule type (A → B / C __ D)
• Rule application to segment strings (left-to-right scan)
• Ordered derivation (rule cascade)
• Example rules from Hayes Ch 6

@cite{hayes-2009}

def Theories.Phonology.Segment.ofSpecs (specs : List (Feature × Bool)) : Segment

Create a segment from a list of (feature, value) pairs. Unmentioned features are unspecified (none), giving natural class semantics: ofSpecs [(continuant, false)] matches all [-cont] segments.

Equations

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

def Theories.Phonology.Segment.matchesPattern (s p : Segment) : Bool

Does segment s match pattern p? True when every feature specified in p has the same value in s. An unspecified feature in p matches anything (natural class semantics).

Hayes §6.2: "The target of a rule identifies a natural class of sounds — all segments sharing a particular set of feature values."

Equations

• s.matchesPattern p = Theories.Phonology.Feature.allFeatures.all fun (f : Theories.Phonology.Feature) => match p.spec f with | none => true | some v => s.spec f == some v

def Theories.Phonology.Segment.applyChanges (s change : Segment) : Segment

Apply feature changes from change to s: specified features in change override those in s, unspecified features are preserved.

This implements the structural change A → B when B is a partial specification — only the mentioned features change.

Equations

• s.applyChanges change = { spec := fun (f : Theories.Phonology.Feature) => match change.spec f with | some v => some v | none => s.spec f }

inductive Theories.Phonology.RuleBased.ContextElem : Type

An element of a phonological rule's structural description. Context positions can be segment patterns (natural classes) or word boundaries (Hayes §6.2: ]word or #).

• seg : Segment → ContextElem

  A segment matching this natural class.

• wordBoundary : ContextElem

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

inductive Theories.Phonology.RuleBased.RuleEffect : Type

The structural change of a phonological rule.

• changeFeatures : Segment → RuleEffect

  Change features: merge change into the target segment. Hayes §6.2: A → B where B is a feature bundle.

• delete : RuleEffect

  Delete the target segment. Hayes §6.4: A → ∅.

structure Theories.Phonology.RuleBased.PhonRule : Type

A phonological rule in SPE notation: A → B / C __ D.

• target: natural class A (segments this rule applies to)
• effect: structural change B (feature change or deletion)
• leftContext: C (what must precede the target)
• rightContext: D (what must follow the target)

Hayes Ch 6: "A rule consists of four parts: the target, which identifies the class of sounds to be changed; the structural change, specifying what happens; and the environment, specifying where the change occurs."

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

def Theories.Phonology.RuleBased.matchRightContext (segs : Array Segment) (pos : Nat) (ctx : List ContextElem) (len : Nat) : Bool

Does the right context match starting at position pos in segs (where pos is the index immediately after the target)? Scans rightward through the context list.

Equations

• One or more equations did not get rendered due to their size.
• Theories.Phonology.RuleBased.matchRightContext segs pos [] len = true

def Theories.Phonology.RuleBased.matchLeftContext (segs : Array Segment) (pos : Nat) (ctx : List ContextElem) (len : Nat) : Bool

Does the left context match ending at position pos in segs (where pos is the index immediately before the target)? Context is ordered left-to-right, so the rightmost element is closest to the target. We reverse to scan inward-to-outward (leftward).

Equations

• Theories.Phonology.RuleBased.matchLeftContext segs pos ctx len = Theories.Phonology.RuleBased.matchLeftContext.go segs pos ctx.reverse len

def Theories.Phonology.RuleBased.matchLeftContext.go (segs : Array Segment) (pos : Nat) (revCtx : List ContextElem) (len : Nat) : Bool

Equations

• One or more equations did not get rendered due to their size.
• Theories.Phonology.RuleBased.matchLeftContext.go segs pos [] len = true

def Theories.Phonology.RuleBased.applyEffect (s : Segment) (e : RuleEffect) : Option Segment

Apply effect to a segment: feature change merges, deletion removes.

Equations

• Theories.Phonology.RuleBased.applyEffect s (Theories.Phonology.RuleBased.RuleEffect.changeFeatures change) = some (s.applyChanges change)
• Theories.Phonology.RuleBased.applyEffect s Theories.Phonology.RuleBased.RuleEffect.delete = none

def Theories.Phonology.RuleBased.PhonRule.apply (r : PhonRule) (input : List Segment) : List Segment

Apply a phonological rule to a segment string. Scans left-to-right, applying the rule at every position where the target and context match. Returns the transformed string.

Equations

• r.apply input = (Theories.Phonology.RuleBased.PhonRule.apply.go input.toArray r 0 #[]).toList

@[irreducible]

def Theories.Phonology.RuleBased.PhonRule.apply.go (arr : Array Segment) (r : PhonRule) (pos : Nat) (acc : Array Segment) : Array Segment

Equations

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

def Theories.Phonology.RuleBased.derive (rules : List PhonRule) (input : List Segment) : List Segment

Apply an ordered sequence of rules (derivation). Rules apply in order, each seeing the output of the previous. This is the core of ordered rule application in SPE phonology.

Equations

• Theories.Phonology.RuleBased.derive rules input = List.foldl (fun (segs : List Theories.Phonology.Segment) (r : Theories.Phonology.RuleBased.PhonRule) => r.apply segs) input rules

def Theories.Phonology.RuleBased.preglottalization : PhonRule

Preglottalization (Hayes p.125): [-cont, -voice] → [+c.g.] / __]word

Voiceless stops become glottalized word-finally.

Equations

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

def Theories.Phonology.RuleBased.koreanNasalization : PhonRule

Korean Stop Nasalization (Hayes p.132): [-del.rel.] → [+nasal, +voice, +son] / __ [+nasal]

Non-affricate stops become nasalized before nasals.

Equations

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

def Theories.Phonology.RuleBased.postnasalDeletion : PhonRule

Postnasal /t/ Deletion (Hayes p.133): [-cont, +cor, +ant, -voice] → ∅ / [+nasal] __ [+syll]

Voiceless coronal stops delete between a nasal and a vowel.

Equations

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

theorem Theories.Phonology.RuleBased.matchesPattern_refl (s : Segment) : s.matchesPattern s = true

Every segment matches itself as a pattern.

theorem Theories.Phonology.RuleBased.applyChanges_ofSpecs_nil (s : Segment) : s.applyChanges (Segment.ofSpecs []) = s

Applying an empty change (no features specified) is the identity.

theorem Theories.Phonology.RuleBased.derive_nil (input : List Segment) : derive [] input = input

Derivation with no rules is the identity.