Broe (1993) [Bro93a]

Specification theory: the treatment of redundancy in generative phonology replaces underspecified matrices and redundancy rules with structured specification: the descriptions supported by a feature set, ordered by inclusion of their denotations, form a lattice, and redundancy is read off its dominance relation (§5.2's three-stage construction, an instance of formal concept analysis). naturalClasses computes the stage-two lattice's nonempty extents — the natural classes of an inventory — as the closure of the attribute extents under intersection; the Quileute and reduced-Quileute vowel systems of §5.2 are the thesis's worked examples.

def Broe1993.naturalClasses {α : Type u_1} [DecidableEq α] (base : Finset α) (attrs : List (Finset α)) : List (Finset α)

The extents of the stage-two lattice of representations ([Bro93a] §5.2): every intersection of base with attribute extents drawn from attrs, deduplicated. Descriptions with the same denotation collapse to one class; a description with empty denotation collapses to ∅, the lattice's bottom.

Equations

• Broe1993.naturalClasses base attrs = List.foldr (fun (a : Finset α) (acc : List (Finset α)) => (acc ++ List.map (fun (x : Finset α) => a ∩ x) acc).dedup) [base] attrs

inductive Broe1993.Quileute : Type

The four-vowel Quileute system of §5.2, exhaustively classified by [high] and [back]: /i a ɑ u/.

• i : Quileute

  /i/ — [+high, −back].

• a : Quileute

  /a/ — [−high, −back].

• aBack : Quileute

  /ɑ/ — [−high, +back].

• u : Quileute

  /u/ — [+high, +back].

@[instance_reducible]

instance Broe1993.instDecidableEqQuileute : DecidableEq Quileute

Equations

• Broe1993.instDecidableEqQuileute x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Broe1993.quileuteContext : List (Finset Quileute)

The Quileute attribute extents: [+hi], [−hi], [+ba], [−ba].

Equations

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

theorem Broe1993.quileute_classes : (naturalClasses {Quileute.i, Quileute.a, Quileute.aBack, Quileute.u} quileuteContext).toFinset = {{Quileute.i, Quileute.a, Quileute.aBack, Quileute.u}, {Quileute.i, Quileute.u}, {Quileute.a, Quileute.aBack}, {Quileute.u, Quileute.aBack}, {Quileute.i, Quileute.a}, {Quileute.i}, {Quileute.a}, {Quileute.aBack}, {Quileute.u}, ∅}

Every feature combination is attested and every description is informative: the lattice of Broe's diagram (6) — all four two-vowel classes, all four singletons, top, and bottom.

def Broe1993.quileutePrimeContext : List (Finset Quileute)

The reduced system without /a/ (Broe's Quileuteʹ): the same four descriptions, with /a/ removed from the extents.

Equations

• Broe1993.quileutePrimeContext = [{Broe1993.Quileute.i, Broe1993.Quileute.u}, {Broe1993.Quileute.aBack}, {Broe1993.Quileute.u, Broe1993.Quileute.aBack}, {Broe1993.Quileute.i}]

theorem Broe1993.quileutePrime_classes : (naturalClasses {Quileute.i, Quileute.aBack, Quileute.u} quileutePrimeContext).toFinset = {{Quileute.i, Quileute.aBack, Quileute.u}, {Quileute.i, Quileute.u}, {Quileute.u, Quileute.aBack}, {Quileute.i}, {Quileute.aBack}, {Quileute.u}, ∅}

With the [−hi, −ba] gap, the lattice collapses to Broe's diagram (9): [−hi] and [−hi, +ba] become synonymous (one class {ɑ}), and the incompatible description [−hi, −ba] falls to bottom.

theorem Broe1993.quileutePrime_redundancy : {Quileute.i} ⊆ {Quileute.i, Quileute.u} ∧ {Quileute.aBack} ⊆ {Quileute.u, Quileute.aBack}

The redundancy rules Broe reads off the collapsed lattice's dominance relation (p. 104): [−back] → [+high] and [−high] → [+back], as extent inclusions.