Derivational Operators

@cite{beavers-koontz-garboden-2020} @cite{rappaport-hovav-levin-1998}

A derivational operator is a language-specific morphological process that applies to a root subject to a structural condition on the root's entailments. The collection of operators that successfully apply to a root is the root's orbit under the inventory.

For Yukatek and other languages, partitioning roots by orbit recovers language-specific verb-stem classifications (Bohnemeyer's 5-way; Lucy's 3-way salience cut) as derived equivalence classes rather than stipulated enums. This means typological classes become predictions of (root features × operator inventory), not architectural primitives.

structure Morphology.Derivation.DerivOp : Type

A morphological operator: a name and a structural condition on roots specifying when the operator can apply.

The condition is a propositional predicate over Root, typically phrased in terms of B&K-G feature signatures, with a bundled DecidablePred instance so the predicate can drive List.filter and other computational uses. Whether such conditions are descriptively adequate is itself an empirical question — encoding them this way exposes the choice.

• name : String
• applies : Semantics.Lexical.Roots.Root → Prop
• decApplies : DecidablePred self.applies

@[reducible, inline]

abbrev Morphology.Derivation.Inventory : Type

An inventory: a finite list of derivational operators.

Equations

• Morphology.Derivation.Inventory = List Morphology.Derivation.DerivOp

def Morphology.Derivation.Inventory.orbit (inv : Inventory) (r : Semantics.Lexical.Roots.Root) : List String

The orbit of a root under an inventory: the names of operators that apply to it.

Equations

• inv.orbit r = List.map (fun (x : Morphology.Derivation.DerivOp) => x.name) (List.filter (fun (op : Morphology.Derivation.DerivOp) => decide (op.applies r)) inv)

def Morphology.Derivation.Inventory.Equivalent (inv : Inventory) (r₁ r₂ : Semantics.Lexical.Roots.Root) : Prop

Two roots are inventory-equivalent iff every operator in the inventory either applies to both or neither.

Equations

• inv.Equivalent r₁ r₂ = ∀ (op : Morphology.Derivation.DerivOp), op ∈ inv → (op.applies r₁ ↔ op.applies r₂)

@[implicit_reducible]

instance Morphology.Derivation.Inventory.instDecidableEquivalent (inv : Inventory) (r₁ r₂ : Semantics.Lexical.Roots.Root) : Decidable (inv.Equivalent r₁ r₂)

Equations

• inv.instDecidableEquivalent r₁ r₂ = id inferInstance