Broe 1993: structured specification

This file formalizes the treatment of redundancy in [Bro93a]. Underspecified matrices and redundancy rules are replaced by a lattice: the descriptions a feature set supports, ordered by inclusion of their denotations, and redundancy read off its dominance relation. naturalClasses computes that lattice's extents from an inventory and the extents of its feature values, in any meet-semilattice of extents, and is shown to be the closure system they generate, the construction Broe takes from formal concept analysis. The Quileute vowel system and its gapped variant are the worked examples of §5.2.2.

Main definitions

• naturalClasses: the extents generated by an inventory and its attribute extents

Main results

• mem_naturalClasses: a class is a meet of the inventory with attribute extents
• inf_mem_naturalClasses, naturalClasses_minimal: the classes are the closure system those extents generate
• quileute_no_redundancy, quileutePrime_redundancy: a gapless system has no dominance among its attribute extents; the gapped one has Broe's two redundancies

References

• [Bro93a]

def Broe1993.addMeets {α : Type u_1} [SemilatticeInf α] [DecidableEq α] (a : α) (acc : List α) : List α

One step of the construction: the meets of the attribute extent a with the classes so far, added once each.

Equations

• Broe1993.addMeets a acc = List.foldl (fun (l : List α) (s : α) => List.insert (a ⊓ s) l) acc acc

theorem Broe1993.mem_addMeets {α : Type u_1} [SemilatticeInf α] [DecidableEq α] {a s : α} {l : List α} : s ∈ addMeets a l ↔ s ∈ l ∨ ∃ t ∈ l, s = a ⊓ t

theorem Broe1993.nodup_addMeets {α : Type u_1} [SemilatticeInf α] [DecidableEq α] {a : α} {l : List α} (hl : l.Nodup) : (addMeets a l).Nodup

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

The extents of the lattice of representations (§5.2.2): every meet of the inventory base with attribute extents drawn from attrs, each once. Descriptions with the same denotation collapse to one class, and an unsatisfiable description to the least class.

Equations

• Broe1993.naturalClasses base attrs = List.foldr Broe1993.addMeets [base] attrs

theorem Broe1993.mem_naturalClasses_cons {α : Type u_1} [SemilatticeInf α] [DecidableEq α] {base a s : α} {attrs : List α} : s ∈ naturalClasses base (a :: attrs) ↔ s ∈ naturalClasses base attrs ∨ ∃ t ∈ naturalClasses base attrs, s = a ⊓ t

theorem Broe1993.nodup_naturalClasses {α : Type u_1} [SemilatticeInf α] [DecidableEq α] (base : α) (attrs : List α) : (naturalClasses base attrs).Nodup

theorem Broe1993.base_mem_naturalClasses {α : Type u_1} [SemilatticeInf α] [DecidableEq α] (base : α) (attrs : List α) : base ∈ naturalClasses base attrs

The inventory itself is a natural class, the lattice's top.

theorem Broe1993.inf_mem_naturalClasses {α : Type u_1} [SemilatticeInf α] [DecidableEq α] {base a s : α} {attrs : List α} (ha : a ∈ attrs) (hs : s ∈ naturalClasses base attrs) : a ⊓ s ∈ naturalClasses base attrs

Meeting a natural class with an attribute extent gives a natural class: the classes are closed under the meets that generate them.

theorem Broe1993.mem_naturalClasses {α : Type u_1} [SemilatticeInf α] [DecidableEq α] {base s : α} {attrs : List α} : s ∈ naturalClasses base attrs ↔ ∃ (sub : List α), (∀ a ∈ sub, a ∈ attrs) ∧ s = List.foldr (fun (x1 x2 : α) => x1 ⊓ x2) base sub

A natural class is the inventory met with attribute extents, and every such meet is a natural class.

theorem Broe1993.naturalClasses_minimal {α : Type u_1} [SemilatticeInf α] [DecidableEq α] {base : α} {attrs : List α} {C : Set α} (hbase : base ∈ C) (hclosed : ∀ a ∈ attrs, ∀ s ∈ C, a ⊓ s ∈ C) (s : α) : s ∈ naturalClasses base attrs → s ∈ C

Every collection that contains the inventory and is closed under meeting with the attribute extents contains all the natural classes: the construction is the closure system the attribute extents generate, not a larger collection.

theorem Broe1993.mem_naturalClasses_filter {α : Type u_1} [SemilatticeInf α] [DecidableEq α] {base c s : α} {attrs : List α} [DecidableLE α] : s ∈ naturalClasses base (List.filter (fun (x : α) => decide (c ≤ x)) attrs) ∧ c ≤ s ↔ s ∈ naturalClasses base attrs ∧ c ≤ s

The classes above c are generated by the attribute extents above c alone.

theorem Broe1993.mem_naturalClasses_inf {α : Type u_1} [SemilatticeInf α] [DecidableEq α] {base p s : α} {attrs : List α} (hp : p ∈ attrs) : s ∈ naturalClasses (p ⊓ base) attrs ↔ s ∈ naturalClasses base attrs ∧ s ≤ p

The classes below an attribute extent p are the classes of the sub-inventory p defines.

Quileute

inductive Broe1993.Quileute : Type

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

• 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 informative: the lattice of diagram (6) — all four two-vowel classes, all four singletons, top, and bottom.

theorem Broe1993.quileute_no_redundancy (a b : Finset Quileute) (ha : a ∈ quileuteContext) (hb : b ∈ quileuteContext) (hab : a ⊆ b) : a = b

No feature value can be predicted from another: no attribute extent dominates another, so the gapless system carries no redundancy.

def Broe1993.quileutePrimeContext : List (Finset Quileute)

The reduced system without /a/ (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 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 the extent inclusions the gapless system lacked.