Consonantal Roots

Single source of truth for the Semitic-style notion of a consonantal root: an ordered melody of segments stored independently of vocalization or template.

The segment type α is parametric. Studies of Tarifit Berber may instantiate α := Phonology.Sonority.Class (sonority-class roots, used by [AZ25b]); studies of Hebrew or Amharic typically instantiate α := String for IPA symbols.

Theory-laden questions about the cognitive reality of roots (e.g. Ussishkin 2000, Bat-El 2003) are orthogonal to the data type itself — Root is a sequence; what status linguistic theory gives that sequence is a separate matter, parameterized at the study level.

Namespace separation

Morphology.Root (this file): a consonantal melody, a morphological primitive (the underlying form of a morpheme). The root-level Root (Semantics/Lexical/Roots/Basic.lean): a bundle of LexEntailment atoms in the [BKG20] sense — same English word, different concept. Root.Profile (Semantics/Lexical/Roots/Profile.lean): semantic quality dimensions on a verb root — orthogonal to both.

structure Morphology.Root (α : Type) : Type

A consonantal root: an ordered list of segments. Polymorphic in the segment type so that fragments may pick the granularity they need (sonority class, IPA symbol, full feature matrix).

• segments : List α

@[implicit_reducible]

instance Morphology.instReprRoot {α✝ : Type} [Repr α✝] : Repr (Root α✝)

Equations

• Morphology.instReprRoot = { reprPrec := Morphology.instReprRoot.repr }

def Morphology.instReprRoot.repr {α✝ : Type} [Repr α✝] : Root α✝ → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Morphology.instDecidableEqRoot {α✝ : Type} [DecidableEq α✝] : DecidableEq (Root α✝)

Equations

• Morphology.instDecidableEqRoot = Morphology.instDecidableEqRoot.decEq

def Morphology.instDecidableEqRoot.decEq {α✝ : Type} [DecidableEq α✝] (x✝ x✝¹ : Root α✝) : Decidable (x✝ = x✝¹)

Equations

• Morphology.instDecidableEqRoot.decEq { segments := a } { segments := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

def Morphology.Root.arity {α : Type} (r : Root α) : ℕ

The number of root segments.

Equations

• r.arity = r.segments.length

def Morphology.Root.isFinal {α : Type} (r : Root α) (i : ℕ) : Bool

Position i is the final root position.

Equations

• r.isFinal i = (i + 1 == r.arity)

def Morphology.Root.isNonfinal {α : Type} (r : Root α) (i : ℕ) : Bool

Position i is nonfinal (some position strictly past it exists). Used by *Misalignment ([Fau26] (2)).

Equations

• r.isNonfinal i = decide (i + 1 < r.arity)

def Morphology.Root.biradical {α : Type} (r : Root α) : Bool

A root with exactly two segments (e.g. √qt → QaTaT-template biradicals in Hebrew, [McC81]).

Equations

• r.biradical = (r.arity == 2)

def Morphology.Root.triradical {α : Type} (r : Root α) : Bool

A root with exactly three segments (the unmarked Semitic case).

Equations

• r.triradical = (r.arity == 3)

def Morphology.Root.quadriradical {α : Type} (r : Root α) : Bool

A root with exactly four segments (e.g. quadriliteral verbs).

Equations

• r.quadriradical = (r.arity == 4)

def Morphology.Root.finalSegment {α : Type} (r : Root α) : Option α

The last segment of the root, if any.

Equations

• r.finalSegment = r.segments.getLast?

def Morphology.Root.segmentAt {α : Type} (r : Root α) (i : ℕ) : Option α

The segment at position i, if in range.

Equations

• r.segmentAt i = r.segments[i]?

def Morphology.Root.IsOCPClean {α : Type} [DecidableEq α] (r : Root α) : Prop

Root-level OCP ([McC81], [Fau26]): a consonantal root has no two adjacent identical segments. Segment-level and theory-neutral — it commits to no tier projection or feature decomposition (stronger tier-relative variants go through OCP.IsCleanOn). Definitionally the segment tier being OCP.IsClean.

Equations

• r.IsOCPClean = OCP.IsClean r.segments

@[implicit_reducible]

instance Morphology.Root.instDecidablePredIsOCPClean {α : Type} [DecidableEq α] : DecidablePred IsOCPClean

Equations

• r.instDecidablePredIsOCPClean = Morphology.Root.instDecidablePredIsOCPClean._aux_1 r