Documentation

Linglib.Theories.Phonology.FeatureGeometry

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)
@cite{hayes-2009}: complete 26-feature inventory mapped to geometric nodes
Root [±syll, ±cons, ±son, ±approx, ±nas, ±del.rel., ±tap, ±trill] ├── Laryngeal [±voice, ±s.g., ±c.g.] └── Supralaryngeal [±cont] └── 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.

inductive Theories.Phonology.FeatureGeometry.GeomNode :

Class nodes in the feature geometry tree.

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

Instances For

instance Theories.Phonology.FeatureGeometry.instDecidableEqGeomNode :

DecidableEq GeomNode

Equations

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

def Theories.Phonology.FeatureGeometry.instBEqGeomNode.beq :

GeomNode → GeomNode → Bool

Equations

Theories.Phonology.FeatureGeometry.instBEqGeomNode.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

instance Theories.Phonology.FeatureGeometry.instBEqGeomNode :

Equations

Theories.Phonology.FeatureGeometry.instBEqGeomNode = { beq := Theories.Phonology.FeatureGeometry.instBEqGeomNode.beq }

instance Theories.Phonology.FeatureGeometry.instReprGeomNode :

Equations

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

def Theories.Phonology.FeatureGeometry.instReprGeomNode.repr :

GeomNode → Nat → Std.Format

Equations

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

Instances For

def Theories.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

def Theories.Phonology.FeatureGeometry.GeomNode.allNodes :

All geometric nodes.

Equations

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

Instances For

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

Children of a node: nodes whose parent is n.

Equations

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

Instances For

def Theories.Phonology.FeatureGeometry.GeomNode.dominates (n m : GeomNode) :

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

def Theories.Phonology.Feature.node :

Feature → FeatureGeometry.GeomNode

Each terminal feature maps to its dominating class node.

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

Equations

Instances For

def Theories.Phonology.Feature.dominatedBy (f : Feature) (n : FeatureGeometry.GeomNode) :

Does node n dominate the node that feature f belongs to?

Equations

f.dominatedBy n = n.dominates f.node

Instances For

def Theories.Phonology.FeatureGeometry.GeomNode.features (n : GeomNode) :

Features dominated by node n — a natural class in the feature-geometric sense: the features that pattern together under processes targeting n.

Equations

n.features = List.filter (fun (f : Theories.Phonology.Feature) => n.dominates f.node) Theories.Phonology.Feature.allFeatures

Instances For

theorem Theories.Phonology.FeatureGeometry.root_has_no_parent :

GeomNode.root.parent = none

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

n.parent.isSome = true

theorem Theories.Phonology.FeatureGeometry.parent_decreases_depth (n p : GeomNode) (h : n.parent = some p) :

p.depth < n.depth

theorem Theories.Phonology.FeatureGeometry.allNodes_complete (n : GeomNode) :

n ∈ GeomNode.allNodes

theorem Theories.Phonology.FeatureGeometry.root_depth :

GeomNode.root.depth = 0

theorem Theories.Phonology.FeatureGeometry.supralaryngeal_depth :

GeomNode.supralaryngeal.depth = 1

theorem Theories.Phonology.FeatureGeometry.place_depth :

GeomNode.place.depth = 2

theorem Theories.Phonology.FeatureGeometry.labial_depth :

GeomNode.labial.depth = 3

theorem Theories.Phonology.FeatureGeometry.coronal_depth :

GeomNode.coronal.depth = 3

theorem Theories.Phonology.FeatureGeometry.dorsal_depth :

GeomNode.dorsal.depth = 3

theorem Theories.Phonology.FeatureGeometry.root_features_count :

GeomNode.root.features.length = 26

theorem Theories.Phonology.FeatureGeometry.laryngeal_features_count :

GeomNode.laryngeal.features.length = 3

theorem Theories.Phonology.FeatureGeometry.supralaryngeal_features_count :

GeomNode.supralaryngeal.features.length = 15

theorem Theories.Phonology.FeatureGeometry.place_features_count :

GeomNode.place.features.length = 14

theorem Theories.Phonology.FeatureGeometry.labial_features_count :

GeomNode.labial.features.length = 3

theorem Theories.Phonology.FeatureGeometry.coronal_features_count :

GeomNode.coronal.features.length = 5

theorem Theories.Phonology.FeatureGeometry.dorsal_features_count :

GeomNode.dorsal.features.length = 6

theorem Theories.Phonology.FeatureGeometry.isLaryngeal_iff_laryngeal_dominates (f : Feature) :

f.isLaryngeal = f.dominatedBy GeomNode.laryngeal

theorem Theories.Phonology.FeatureGeometry.isDorsal_iff_dorsal_dominates (f : Feature) :

f.isDorsal = f.dominatedBy GeomNode.dorsal

theorem Theories.Phonology.FeatureGeometry.isPlace_implies_place_dominates (f : Feature) :

f.isPlace = true → f.dominatedBy GeomNode.place = true

theorem Theories.Phonology.FeatureGeometry.lateral_geometrically_under_place :

Feature.lateral.dominatedBy GeomNode.place = true

theorem Theories.Phonology.FeatureGeometry.strident_geometrically_under_place :

Feature.strident.dominatedBy GeomNode.place = true

def Theories.Phonology.FeatureGeometry.canSpreadUnder (n : GeomNode) (f : Feature) :

Can feature f spread under node n? True when f is dominated by n.

Equations

Theories.Phonology.FeatureGeometry.canSpreadUnder n f = n.dominates f.node

Instances For

def Theories.Phonology.FeatureGeometry.delinkedBy (n : GeomNode) (f : Feature) :

Does delinking node n remove feature f? True when n dominates f's node and n is not Root (delinking Root = deleting the segment).

Equations

Theories.Phonology.FeatureGeometry.delinkedBy n f = (n.dominates f.node && n != Theories.Phonology.FeatureGeometry.GeomNode.root)

Instances For