Element Theory

In Element Theory a segment is built from six privative elements, |A I U ʔ H L|, rather than from binary features. A melodic expression is a set of elements, some of which are its heads, and a segment has one expression at each of its manner, place and laryngeal nodes. Expressions are ordered by containment, a headed element lying above its unheaded self, and they form a distributive lattice. Its join is the union by which elements combine, so that docking a floating expression onto a host is host ⊔ floating, and what a set of segments shares is their meet.

Main definitions

• ElementTheory.Element, ElementTheory.Element.gridEquiv: the six elements, which are three antagonistic pairs with a dark and a light member each.
• ElementTheory.Element.AntagonismFree: a set of elements holding at most one of each pair.
• ElementTheory.MR: a melodic expression.
• ElementTheory.Segment: an expression at each node.
• ElementTheory.Segment.WellFormed: each node holds only elements that it hosts.

Main results

• ElementTheory.MR.simplex_lt_headedSimplex: a headed element properly contains its unheaded self.
• ElementTheory.Segment.WellFormed.sup: docking preserves well-formedness.

Implementation notes

• The heads of an expression are a set of its elements, so that the rival conditions on heads are predicates on one type. Most versions of the theory allow an expression one head, m.heads.card ≤ 1. Backley's later proposal allows one for each fundamental, Element.AntagonismFree m.heads, which the former implies (Element.AntagonismFree.of_card_le_one).
• Antagonism is a predicate and not a condition on expressions, since languages differ in which antagonistic pairs they let combine.
• The inventory, the pairs and the fundamentals are Backley's, and the three nodes with the elements they host follow Harris as Cavirani and Vanden Wyngaerd adopt them.

References

• [Bac11]
• [Bac17]
• [Har94b]
• [KLV85]
• [CVW26]

The six elements

inductive ElementTheory.Fundamental : Type

The three fundamentals of spoken language to which the elements refer.

• colour : Fundamental

  Colour, with |U| dark and |I| bright.

• resonance : Fundamental

  Resonance, with |A| resonant and |ʔ| not.

• frequency : Fundamental

  Frequency, with |L| low and |H| high.

@[instance_reducible]

instance ElementTheory.instDecidableEqFundamental : DecidableEq Fundamental

Equations

• ElementTheory.instDecidableEqFundamental x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance ElementTheory.instReprFundamental : Repr Fundamental

Equations

• ElementTheory.instReprFundamental = { reprPrec := ElementTheory.instReprFundamental.repr }

def ElementTheory.instReprFundamental.repr : Fundamental → ℕ → Std.Format

Equations

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

inductive ElementTheory.Polarity : Type

The two opposing values of a fundamental.

• dark : Polarity
• light : Polarity

@[instance_reducible]

instance ElementTheory.instDecidableEqPolarity : DecidableEq Polarity

Equations

• ElementTheory.instDecidableEqPolarity x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance ElementTheory.instReprPolarity : Repr Polarity

Equations

• ElementTheory.instReprPolarity = { reprPrec := ElementTheory.instReprPolarity.repr }

def ElementTheory.instReprPolarity.repr : Polarity → ℕ → Std.Format

Equations

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

inductive ElementTheory.Element : Type

The six privative elements.

• A : Element

  The element |A| of aperture, a high first formant.

• I : Element

  The element |I| of palatality, a high second formant.

• U : Element

  The element |U| of labiality and velarity, a lowering of all formants.

• glottal : Element

  The element |ʔ| of occlusion, an abrupt and sustained drop in amplitude.

• H : Element

  The element |H| of noise, voicelessness and high tone, high-frequency energy.

• L : Element

  The element |L| of nasality, voicing and low tone, low-frequency energy.

@[instance_reducible]

instance ElementTheory.instDecidableEqElement : DecidableEq Element

Equations

• ElementTheory.instDecidableEqElement x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def ElementTheory.instReprElement.repr : Element → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• ElementTheory.instReprElement.repr ElementTheory.Element.A prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ElementTheory.Element.A")).group prec✝
• ElementTheory.instReprElement.repr ElementTheory.Element.I prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ElementTheory.Element.I")).group prec✝
• ElementTheory.instReprElement.repr ElementTheory.Element.U prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ElementTheory.Element.U")).group prec✝
• ElementTheory.instReprElement.repr ElementTheory.Element.H prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ElementTheory.Element.H")).group prec✝
• ElementTheory.instReprElement.repr ElementTheory.Element.L prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ElementTheory.Element.L")).group prec✝

@[instance_reducible]

instance ElementTheory.instReprElement : Repr Element

Equations

• ElementTheory.instReprElement = { reprPrec := ElementTheory.instReprElement.repr }

def ElementTheory.Element.gridEquiv : Element ≃ Fundamental × Polarity

The elements are three antagonistic pairs, one for each fundamental, and each pair has a dark and a light member.

Equations

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

def ElementTheory.Element.fundamental (e : Element) : Fundamental

The fundamental to which an element refers.

Equations

• e.fundamental = (ElementTheory.Element.gridEquiv e).1

def ElementTheory.Element.polarity (e : Element) : Polarity

The value that an element marks on its fundamental.

Equations

• e.polarity = (ElementTheory.Element.gridEquiv e).2

def ElementTheory.Element.AntagonismFree (s : Finset Element) : Prop

A set of elements is antagonism-free if it holds at most one element of each antagonistic pair.

Equations

• ElementTheory.Element.AntagonismFree s = Set.InjOn ElementTheory.Element.fundamental ↑s

@[instance_reducible]

instance ElementTheory.Element.instDecidableAntagonismFree (s : Finset Element) : Decidable (AntagonismFree s)

Equations

• ElementTheory.Element.instDecidableAntagonismFree s = { decide := decide (Multiset.map ElementTheory.Element.fundamental s.val).Nodup, reflects_decide := ⋯ }

theorem ElementTheory.Element.AntagonismFree.subset {s t : Finset Element} (ht : AntagonismFree t) (h : s ⊆ t) : AntagonismFree s

theorem ElementTheory.Element.AntagonismFree.of_card_le_one {s : Finset Element} (h : s.card ≤ 1) : AntagonismFree s

A set of at most one element is antagonism-free.

Melodic expressions

structure ElementTheory.MR : Type

A melodic expression is a set of elements, some of which are its heads.

• elements : Finset Element

  The elements of the expression.

• heads : Finset Element

  The heads of the expression.

• heads_subset : self.heads ⊆ self.elements

  The heads are among the elements.

theorem ElementTheory.MR.ext_iff {x y : MR} : x = y ↔ x.elements = y.elements ∧ x.heads = y.heads

theorem ElementTheory.MR.ext {x y : MR} (elements : x.elements = y.elements) (heads : x.heads = y.heads) : x = y

def ElementTheory.MR.toProd (m : MR) : Finset Element × Finset Element

An expression as the pair of its elements and its heads.

Equations

• m.toProd = (m.elements, m.heads)

theorem ElementTheory.MR.toProd_injective : Function.Injective toProd

@[instance_reducible]

instance ElementTheory.MR.instDecidableEq : DecidableEq MR

Equations

• ElementTheory.MR.instDecidableEq = ElementTheory.MR.toProd_injective.decidableEq

@[instance_reducible]

instance ElementTheory.MR.instLE : LE MR

Equations

• ElementTheory.MR.instLE = { le := fun (m₁ m₂ : ElementTheory.MR) => m₁.elements ⊆ m₂.elements ∧ m₁.heads ⊆ m₂.heads }

@[instance_reducible]

instance ElementTheory.MR.instLT : LT MR

Equations

• ElementTheory.MR.instLT = { lt := fun (m₁ m₂ : ElementTheory.MR) => m₁ ≤ m₂ ∧ ¬m₂ ≤ m₁ }

theorem ElementTheory.MR.le_def {m₁ m₂ : MR} : m₁ ≤ m₂ ↔ m₁.elements ⊆ m₂.elements ∧ m₁.heads ⊆ m₂.heads

@[instance_reducible]

instance ElementTheory.MR.instDecidableLE : DecidableLE MR

Equations

• x✝¹.instDecidableLE x✝ = decidable_of_iff' (x✝¹.elements ⊆ x✝.elements ∧ x✝¹.heads ⊆ x✝.heads) ⋯

@[instance_reducible]

instance ElementTheory.MR.instDecidableLT : DecidableLT MR

Equations

• x✝¹.instDecidableLT x✝ = { decide := decide (x✝¹ ≤ x✝) && decide ¬x✝ ≤ x✝¹, reflects_decide := ⋯ }

@[instance_reducible]

instance ElementTheory.MR.instMax : Max MR

Equations

• ElementTheory.MR.instMax = { max := fun (m₁ m₂ : ElementTheory.MR) => { elements := m₁.elements ∪ m₂.elements, heads := m₁.heads ∪ m₂.heads, heads_subset := ⋯ } }

@[instance_reducible]

instance ElementTheory.MR.instMin : Min MR

Equations

• ElementTheory.MR.instMin = { min := fun (m₁ m₂ : ElementTheory.MR) => { elements := m₁.elements ∩ m₂.elements, heads := m₁.heads ∩ m₂.heads, heads_subset := ⋯ } }

@[instance_reducible]

instance ElementTheory.MR.instDistribLattice : DistribLattice MR

Equations

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

@[instance_reducible]

instance ElementTheory.MR.instOrderBot : OrderBot MR

The empty expression is least.

Equations

• ElementTheory.MR.instOrderBot = { bot := { elements := ∅, heads := ∅, heads_subset := ElementTheory.MR.instOrderBot._proof_1 }, bot_le := ElementTheory.MR.instOrderBot._proof_2 }

@[simp]

theorem ElementTheory.MR.sup_elements (m₁ m₂ : MR) : (m₁ ⊔ m₂).elements = m₁.elements ∪ m₂.elements

@[simp]

theorem ElementTheory.MR.sup_heads (m₁ m₂ : MR) : (m₁ ⊔ m₂).heads = m₁.heads ∪ m₂.heads

@[simp]

theorem ElementTheory.MR.inf_elements (m₁ m₂ : MR) : (m₁ ⊓ m₂).elements = m₁.elements ∩ m₂.elements

@[simp]

theorem ElementTheory.MR.inf_heads (m₁ m₂ : MR) : (m₁ ⊓ m₂).heads = m₁.heads ∩ m₂.heads

@[simp]

theorem ElementTheory.MR.bot_elements : ⊥.elements = ∅

@[simp]

theorem ElementTheory.MR.bot_heads : ⊥.heads = ∅

def ElementTheory.MR.simplex (e : Element) : MR

The simplex expression |e| is the element e alone, unheaded.

Equations

• ElementTheory.MR.simplex e = { elements := {e}, heads := ∅, heads_subset := ⋯ }

def ElementTheory.MR.headedSimplex (e : Element) : MR

The headed simplex expression is the element e alone, as head.

Equations

• ElementTheory.MR.headedSimplex e = { elements := {e}, heads := {e}, heads_subset := ⋯ }

@[simp]

theorem ElementTheory.MR.simplex_elements (e : Element) : (simplex e).elements = {e}

@[simp]

theorem ElementTheory.MR.simplex_heads (e : Element) : (simplex e).heads = ∅

@[simp]

theorem ElementTheory.MR.headedSimplex_elements (e : Element) : (headedSimplex e).elements = {e}

@[simp]

theorem ElementTheory.MR.headedSimplex_heads (e : Element) : (headedSimplex e).heads = {e}

@[simp]

theorem ElementTheory.MR.simplex_le_iff {m : MR} {e : Element} : simplex e ≤ m ↔ e ∈ m.elements

An expression contains |e| just when e is one of its elements.

@[simp]

theorem ElementTheory.MR.headedSimplex_le_iff {m : MR} {e : Element} : headedSimplex e ≤ m ↔ e ∈ m.heads

An expression contains headed |e| just when e is one of its heads.

theorem ElementTheory.MR.simplex_lt_headedSimplex (e : Element) : simplex e < headedSimplex e

A headed element properly contains its unheaded self.

Segments

structure ElementTheory.Segment : Type

A segment has a melodic expression at each of its manner, place and laryngeal nodes, empty unless given.

• manner : MR

  The expression at the manner node.

• place : MR

  The expression at the place node.

• laryngeal : MR

  The expression at the laryngeal node.

theorem ElementTheory.Segment.ext {x y : Segment} (manner : x.manner = y.manner) (place : x.place = y.place) (laryngeal : x.laryngeal = y.laryngeal) : x = y

theorem ElementTheory.Segment.ext_iff {x y : Segment} : x = y ↔ x.manner = y.manner ∧ x.place = y.place ∧ x.laryngeal = y.laryngeal

def ElementTheory.Segment.toProd (s : Segment) : MR × MR × MR

A segment as the triple of the expressions at its nodes.

Equations

• s.toProd = (s.manner, s.place, s.laryngeal)

theorem ElementTheory.Segment.toProd_injective : Function.Injective toProd

@[instance_reducible]

instance ElementTheory.Segment.instDecidableEq : DecidableEq Segment

Equations

• ElementTheory.Segment.instDecidableEq = ElementTheory.Segment.toProd_injective.decidableEq

@[instance_reducible]

instance ElementTheory.Segment.instLE : LE Segment

Equations

• ElementTheory.Segment.instLE = { le := fun (s₁ s₂ : ElementTheory.Segment) => s₁.manner ≤ s₂.manner ∧ s₁.place ≤ s₂.place ∧ s₁.laryngeal ≤ s₂.laryngeal }

@[instance_reducible]

instance ElementTheory.Segment.instLT : LT Segment

Equations

• ElementTheory.Segment.instLT = { lt := fun (s₁ s₂ : ElementTheory.Segment) => s₁ ≤ s₂ ∧ ¬s₂ ≤ s₁ }

theorem ElementTheory.Segment.le_def {s₁ s₂ : Segment} : s₁ ≤ s₂ ↔ s₁.manner ≤ s₂.manner ∧ s₁.place ≤ s₂.place ∧ s₁.laryngeal ≤ s₂.laryngeal

@[instance_reducible]

instance ElementTheory.Segment.instDecidableLE : DecidableLE Segment

Equations

• x✝¹.instDecidableLE x✝ = decidable_of_iff' (x✝¹.manner ≤ x✝.manner ∧ x✝¹.place ≤ x✝.place ∧ x✝¹.laryngeal ≤ x✝.laryngeal) ⋯

@[instance_reducible]

instance ElementTheory.Segment.instDecidableLT : DecidableLT Segment

Equations

• x✝¹.instDecidableLT x✝ = { decide := decide (x✝¹ ≤ x✝) && decide ¬x✝ ≤ x✝¹, reflects_decide := ⋯ }

@[instance_reducible]

instance ElementTheory.Segment.instMax : Max Segment

Equations

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

@[instance_reducible]

instance ElementTheory.Segment.instMin : Min Segment

Equations

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

@[instance_reducible]

instance ElementTheory.Segment.instDistribLattice : DistribLattice Segment

Equations

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

@[instance_reducible]

instance ElementTheory.Segment.instOrderBot : OrderBot Segment

The segment with every node empty is least.

Equations

• ElementTheory.Segment.instOrderBot = { bot := { }, bot_le := ElementTheory.Segment.instOrderBot._proof_1 }

@[simp]

theorem ElementTheory.Segment.sup_manner (s₁ s₂ : Segment) : (s₁ ⊔ s₂).manner = s₁.manner ⊔ s₂.manner

@[simp]

theorem ElementTheory.Segment.sup_place (s₁ s₂ : Segment) : (s₁ ⊔ s₂).place = s₁.place ⊔ s₂.place

@[simp]

theorem ElementTheory.Segment.sup_laryngeal (s₁ s₂ : Segment) : (s₁ ⊔ s₂).laryngeal = s₁.laryngeal ⊔ s₂.laryngeal

@[simp]

theorem ElementTheory.Segment.inf_manner (s₁ s₂ : Segment) : (s₁ ⊓ s₂).manner = s₁.manner ⊓ s₂.manner

@[simp]

theorem ElementTheory.Segment.inf_place (s₁ s₂ : Segment) : (s₁ ⊓ s₂).place = s₁.place ⊓ s₂.place

@[simp]

theorem ElementTheory.Segment.inf_laryngeal (s₁ s₂ : Segment) : (s₁ ⊓ s₂).laryngeal = s₁.laryngeal ⊓ s₂.laryngeal

@[simp]

theorem ElementTheory.Segment.bot_manner : ⊥.manner = ⊥

@[simp]

theorem ElementTheory.Segment.bot_place : ⊥.place = ⊥

@[simp]

theorem ElementTheory.Segment.bot_laryngeal : ⊥.laryngeal = ⊥

Well-formedness

def ElementTheory.Segment.WellFormed (s : Segment) : Prop

A segment is well-formed if each node holds only elements that it hosts: |ʔ H L A| at the manner node, |I U A| at the place node and |L H| at the laryngeal node.

Equations

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

@[instance_reducible]

instance ElementTheory.Segment.instDecidablePredWellFormed : DecidablePred WellFormed

Equations

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

theorem ElementTheory.Segment.wellFormed_bot : ⊥.WellFormed

theorem ElementTheory.Segment.WellFormed.sup {s₁ s₂ : Segment} (h₁ : s₁.WellFormed) (h₂ : s₂.WellFormed) : (s₁ ⊔ s₂).WellFormed

Docking preserves well-formedness.