Feature Geometry @cite{clements-1985} @cite{sagey-1986} #

Hierarchical organization of phonological features following the standard feature geometry model. The tree synthesizes three sources:

@cite{clements-1985}: root, laryngeal, supralaryngeal, and place nodes
@cite{sagey-1986}: articulator sub-nodes under Place (labial, coronal, dorsal); soft palate node under Supralaryngeal
@cite{hayes-2009}: complete 26-feature inventory mapped to geometric nodes
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 flat classification predicates in Features.lean (isMajorClass, isPlace) do not exactly correspond to any single geometric node — see the subsumption theorems below.

source

inductive Phonology.FeatureGeometry.GeomNode :

Type

Class nodes in the feature geometry tree.

root : GeomNode
laryngeal : GeomNode
supralaryngeal : GeomNode
softPalate : GeomNode
place : GeomNode
labial : GeomNode
coronal : GeomNode
dorsal : GeomNode

Instances For

source

@[implicit_reducible]

instance Phonology.FeatureGeometry.instDecidableEqGeomNode :

DecidableEq GeomNode

Equations

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

source

@[implicit_reducible]

instance Phonology.FeatureGeometry.instReprGeomNode :

Repr GeomNode

Equations

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

source

def Phonology.FeatureGeometry.instReprGeomNode.repr :

GeomNode → Nat → Std.Format

Equations

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

Instances For

source

def Phonology.FeatureGeometry.GeomNode.parent :

GeomNode → Option GeomNode

Parent of each node in the geometry tree. The supralaryngeal node (@cite{clements-1985}, diagram (4)) mediates between root and place.

Equations

Instances For

source

def Phonology.FeatureGeometry.GeomNode.allNodes :

List GeomNode

All geometric nodes.

Equations

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

Instances For

source

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

List GeomNode

Children of a node: nodes whose parent is n.

Equations

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

Instances For

source

def Phonology.FeatureGeometry.GeomNode.depth :

GeomNode → Nat

Depth of a node in the tree (root = 0).

Equations

Instances For

source

@[reducible]

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

Prop

Does node n dominate node m? Reflexive-transitive closure of the parent relation, unrolled to depth 3 (the tree's maximum depth).

Equations

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

Instances For

source

def Phonology.Feature.node :

Feature → FeatureGeometry.GeomNode

Each terminal feature maps to its dominating class node.

Root: [syllabic], [consonantal], [sonorant], [approximant], [delayedRelease], [tap], [trill]
Laryngeal: [voice], [spreadGlottis], [constrGlottis]
Supralaryngeal: [continuant]
Soft Palate: [nasal]
Labial: [labial], [round], [labiodental]
Coronal: [coronal], [anterior], [distributed], [lateral], [strident]
Dorsal: [dorsal], [high], [low], [front], [back], [tense]

Equations