Documentation

Linglib.Phonology.Segmental.Geometry

Feature geometry #

[Cle85] [Sag86]

The hierarchical organization of phonological features as autosegmental class nodes ([CH95b]):

Root [±syll, ±cons, ±son, ±approx, ±del.rel., ±tap, ±trill]
├── Laryngeal [±voice, ±s.g., ±c.g.]
└── Supralaryngeal [±cont]
    ├── Soft Palate [±nasal]
    └── Place
        ├── Labial [±lab, ±round, ±labiodental]
        ├── Coronal [±cor, ±ant, ±dist, ±lat, ±strid]
        └── Dorsal [±dor, ±high, ±low, ±front, ±back, ±tense]

The constituency from Root down to the three Place articulators is the consensus of [Cle85] and [Sag86]. The placement of individual terminals — notably [continuant], [nasal], and [lateral]/[strident] — is theory-specific and contested: [Sag86] argues [continuant] is articulator-level, against its Supralaryngeal placement here (the divergence is formalized in Studies/Sagey1986.lean). A feature's geometric node is also distinct from its manner-class (Feature.category): [lateral] attaches under Coronal yet is a manner feature, so the flat predicates (Feature.IsPlace &c.) do not coincide with single-node dominance.

Main definitions #

Node, Node.parent, Node.Dominates — the class nodes, the tree, and the reflexive-transitive ancestor relation.
Feature.node — each feature's dominating node (this geometry's assignment; rivals live in their study files).
Node.features — the natural class a node dominates.
Node.IsArticulator, Segment.activeArticulators, Segment.IsComplex — the place articulators and a segment's simultaneous (complex) articulations.

Main results #

Node.dominates_iff — dominance unrolls to the depth-≤ 3 parent chain, the decidable face the decide facts run through.
IsLaryngeal_iff_laryngeal_DominatedBy, IsDorsal_iff_dorsal_DominatedBy — two flat predicates coincide with single-node dominance; IsPlace is only a subset.
Segment.activeArticulators_nodup — complex-segment well-formedness holds by construction ([Sag86]).

Geometric nodes #

inductive Phonology.FeatureGeometry.Node :

The class nodes of the feature-geometry tree ([Cle85]; [Sag86]).

root : Node
The root node, dominating all others.
laryngeal : Node
The laryngeal node: voicing and glottal features.
supralaryngeal : Node
The supralaryngeal node, mediating root and place.
softPalate : Node
The soft-palate (velum) node: nasality.
place : Node
The place node, over the three oral articulators.
labial : Node
The labial articulator (the lips).
coronal : Node
The coronal articulator (the tongue blade/tip).
dorsal : Node
The dorsal articulator (the tongue body).

Instances For

@[implicit_reducible]

instance Phonology.FeatureGeometry.instDecidableEqNode :

DecidableEq Node

Equations

Phonology.FeatureGeometry.instDecidableEqNode x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Phonology.FeatureGeometry.instReprNode :

Repr Node

Equations

Phonology.FeatureGeometry.instReprNode = { reprPrec := Phonology.FeatureGeometry.instReprNode.repr }

def Phonology.FeatureGeometry.instReprNode.repr :

Node → ℕ → Std.Format

Equations

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

Instances For

Tree structure #

def Phonology.FeatureGeometry.Node.allNodes :

List Node

All eight nodes.

Equations

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

Instances For

def Phonology.FeatureGeometry.Node.children (n : Node) :

List Node

The children of n: the nodes whose parent is n.

Equations

n.children = List.filter (fun (k : Phonology.FeatureGeometry.Node) => k.parent == some n) Phonology.FeatureGeometry.Node.allNodes

Instances For

Dominance #

def Phonology.FeatureGeometry.Node.Dominates (n m : Node) :

n dominates m: it is m or one of its ancestors — the reflexive-transitive closure of "is the parent of", walked up from m. Depth-agnostic.

Equations

n.Dominates m = Relation.ReflTransGen (fun (a b : Phonology.FeatureGeometry.Node) => a.parent = some b) m n

Instances For

theorem Phonology.FeatureGeometry.Node.dominates_iff (n m : Node) :

n.Dominates m ↔ n = m ∨ m.parent = some n ∨ m.parent.bind parent = some n ∨ (m.parent.bind parent).bind parent = some n

Dominance unrolls to the depth-≤ 3 parent chain — the decidable face the decide facts below run through.

@[implicit_reducible]

instance Phonology.FeatureGeometry.instDecidableRelNodeDominates :

DecidableRel Node.Dominates

Equations

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

Feature-to-node mapping #

def Phonology.Feature.node :

Feature → FeatureGeometry.Node

Each terminal feature's dominating class node — this geometry's assignment (contested for [continuant]/[nasal]/[lateral]; see the module docstring).

Equations

Instances For

@[reducible]

def Phonology.Feature.DominatedBy (f : Feature) (n : FeatureGeometry.Node) :

Does node n dominate the node feature f belongs to?

Equations

f.DominatedBy n = n.Dominates f.node

Instances For

Natural classes #

def Phonology.FeatureGeometry.Node.features (n : Node) :

The features dominated by n — its natural class, the features that pattern together under processes targeting n.

Equations

n.features = List.filter (fun (g : Phonology.Feature) => decide (n.Dominates g.node)) Phonology.Feature.allFeatures

Instances For

Tree structure (verification) #

theorem Phonology.FeatureGeometry.root_has_no_parent :

Node.root.parent = none

theorem Phonology.FeatureGeometry.nonroot_has_parent (n : Node) (h : n ≠ Node.root) :

n.parent.isSome = true

theorem Phonology.FeatureGeometry.allNodes_complete (n : Node) :

n ∈ Node.allNodes

Natural class sizes #

[Hay09]'s complete 26-feature inventory.

theorem Phonology.FeatureGeometry.root_features_count :

Node.root.features.length = 26

theorem Phonology.FeatureGeometry.laryngeal_features_count :

Node.laryngeal.features.length = 3

theorem Phonology.FeatureGeometry.supralaryngeal_features_count :

Node.supralaryngeal.features.length = 16

theorem Phonology.FeatureGeometry.softPalate_features_count :

Node.softPalate.features.length = 1

theorem Phonology.FeatureGeometry.place_features_count :

Node.place.features.length = 14

theorem Phonology.FeatureGeometry.labial_features_count :

Node.labial.features.length = 3

theorem Phonology.FeatureGeometry.coronal_features_count :

Node.coronal.features.length = 5

theorem Phonology.FeatureGeometry.dorsal_features_count :

Node.dorsal.features.length = 6

Flat-predicate subsumption #

IsLaryngeal/IsDorsal coincide with single-node dominance; IsPlace is only a subset (manner features like [lateral]/[strident] sit geometrically under Coronal).

theorem Phonology.FeatureGeometry.IsLaryngeal_iff_laryngeal_DominatedBy (f : Feature) :

f.IsLaryngeal ↔ f.DominatedBy Node.laryngeal

theorem Phonology.FeatureGeometry.IsDorsal_iff_dorsal_DominatedBy (f : Feature) :

f.IsDorsal ↔ f.DominatedBy Node.dorsal

theorem Phonology.FeatureGeometry.IsPlace_implies_place_DominatedBy (f : Feature) :

f.IsPlace → f.DominatedBy Node.place

theorem Phonology.FeatureGeometry.lateral_geometrically_under_place :

Feature.lateral.DominatedBy Node.place

theorem Phonology.FeatureGeometry.strident_geometrically_under_place :

Feature.strident.DominatedBy Node.place

Complex and contour segments #

Complex segments have one root node with several place articulators active simultaneously (e.g. labiovelars [k͡p]); they fill one timing slot and their articulations are unordered. Contour segments have two root nodes on one timing slot, with articulations in sequence (e.g. affricates [ts]). A single-bundle Segment has one value per feature, so it can host only complex (one-root) segments, via activeArticulators; sequential contours need the multi-anchor autosegmental representation (Autosegmental/).

The geometry predicts which complex segments are possible: only those combining distinct articulators. Palatal–velar stops are impossible (both are dorsal); labiovelars are possible (labial and dorsal are independent).

Articulator nodes #

def Phonology.FeatureGeometry.Node.IsArticulator :

A place articulator — labial, coronal, or dorsal — the independent articulators whose distinct combinations give complex segments ([Sag86]).

Equations

Phonology.FeatureGeometry.Node.labial.IsArticulator = True
Phonology.FeatureGeometry.Node.coronal.IsArticulator = True
Phonology.FeatureGeometry.Node.dorsal.IsArticulator = True
x✝.IsArticulator = False

Instances For

@[implicit_reducible]

instance Phonology.FeatureGeometry.instDecidablePredNodeIsArticulator :

DecidablePred Node.IsArticulator

Equations

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

def Phonology.FeatureGeometry.articulatorNodes :

List Node

The articulator nodes.

Equations

Phonology.FeatureGeometry.articulatorNodes = List.filter (fun (n : Phonology.FeatureGeometry.Node) => decide n.IsArticulator) Phonology.FeatureGeometry.Node.allNodes

Instances For

Articulator geometry (verification) #

theorem Phonology.FeatureGeometry.articulatorNodes_count :

articulatorNodes.length = 3

theorem Phonology.FeatureGeometry.articulators_are_leaves (n : Node) :

n ∈ articulatorNodes → n.children = []

Articulators are exactly the leaf nodes.

theorem Phonology.FeatureGeometry.articulators_under_root (n : Node) :

n ∈ articulatorNodes → Node.root.Dominates n

Every articulator is dominated by root.

theorem Phonology.FeatureGeometry.articulators_under_place (n : Node) :

n ∈ articulatorNodes → Node.place.Dominates n

Every articulator is dominated by place.

theorem Phonology.FeatureGeometry.place_articulators_distinct :

Node.labial ≠ Node.coronal ∧ Node.labial ≠ Node.dorsal ∧ Node.coronal ≠ Node.dorsal

The three place articulators are pairwise distinct — giving three complex types (labio-coronal, labio-dorsal, corono-dorsal).

theorem Phonology.FeatureGeometry.softPalate_not_under_place :

¬Node.place.Dominates Node.softPalate

The soft palate is a sibling of place, not under it — so nasal assimilation (spreading soft palate) is independent of place assimilation.

theorem Phonology.FeatureGeometry.softPalate_not_articulator :

¬Node.softPalate.IsArticulator

The soft palate is not an articulator — a velar nasal [ŋ] is simple despite activating both dorsal and soft palate.

Active articulators #

def Phonology.Segment.activeArticulators (s : Segment) :

List FeatureGeometry.Node

The articulator nodes with at least one specified feature in s.

Equations

s.activeArticulators = List.filter (fun (n : Phonology.FeatureGeometry.Node) => n.features.any fun (g : Phonology.Feature) => Option.isSome (s g)) Phonology.FeatureGeometry.articulatorNodes

Instances For

def Phonology.Segment.articulatorCount (s : Segment) :

ℕ

The number of active articulator nodes in s.

Equations

s.articulatorCount = s.activeArticulators.length

Instances For

Complex segments #

def Phonology.Segment.IsComplex (s : Segment) :

A complex segment has two or more simultaneously active articulators — e.g. a labiovelar [k͡p] (labial + dorsal).

Equations

s.IsComplex = (s.articulatorCount ≥ 2)

Instances For

@[implicit_reducible]

instance Phonology.instDecidablePredSegmentIsComplex :

DecidablePred Segment.IsComplex

Equations

Phonology.instDecidablePredSegmentIsComplex x✝ = Phonology.instDecidablePredSegmentIsComplex._aux_1 x✝

theorem Phonology.Segment.activeArticulators_nodup (s : Segment) :

s.activeArticulators.Nodup

Complex-segment well-formedness holds by construction: a segment's active articulators are always distinct, being filtered from the duplicate-free articulatorNodes. The distinct-articulator condition is a theorem, not a separate constraint ([Sag86]).