Docs / Morphology / Exponence / Decomposition

Feature-decomposition exponence and the Subset Principle

import Linglib.Morphology.Exponence.Decomposition · namespace Morphology.Decomposition

In privative feature-decomposition accounts of syncretism, as Caha's and Bobaljik's, each cell is decomposed into a set of features D : Cell → Finset K, and a rule applies where its feature specification is contained in the cell's, the Subset Principle. Competition is Halle's feature counting, the applicable rule of greatest specification winning. Specifications ordered by inclusion need not be nested, so counting is specificity only when the applicable specifications are; the linear containment engine is the chain decomposition Finset.Iic (Containment.pattern_toDecomposition).

Main definitions

Decomposition.Rule: a feature specification with an exponent.
Decomposition.pattern: the exponent at each cell of the applicable rule with the most features.
Decomposition.IsWinner: strict feature-count competition.

Main results

Decomposition.noABA: a cell nested between two others is realized by any rule winning both.

References

Bobaljik 2012, Universals in comparative morphology: Suppletion, superlatives, and the structure of words formalized
Caha 2009, The Nanosyntax of Case formalized
Halle 1997, Distributed Morphology: Impoverishment and Fission

Declarations

A rule of exponence over a feature decomposition D pairs a feature specification with an exponent. It applies where its features are a subset of the cell's, the Subset Principle (Halle 1997).

structure Rule L43–51

{K : Type u_1} (Cell : Type u_2) (D : Cell → Finset K) (F : Type u_3) :

Type (max u_1 u_3)

feats : Finset K
The rule's feature specification.
exponent : F
The exponent inserted.

Derives DecidableEq.

Used by instRuleRule, applies_iff, IsWinner, pattern, noABA

Used in Morphology/Exponence/Containment/Selection, ChristopoulosZompi2023, Zompi2023

L55–56

L58–59

In strict competition r beats every other applicable rule on feature cardinality.

def IsWinner L61–64

{K : Type u_1} {Cell : Type u_2} {F : Type u_3} {D : Cell → Finset K} (v : Exponence.RuleSet (Rule Cell D F)) (c : Cell) (r : Rule Cell D F) :

Prop

IsWinner v c r = (r ∈ v ∧ r.feats ⊆ D c ∧ ∀ s ∈ v, s.feats ⊆ D c → s ≠ r → s.feats.card < r.feats.card)

Built from

Used by noABA

Used in ChristopoulosZompi2023

L68–69

The surface pattern of a rule set is, at each cell, the exponent of the most highly specified applicable rule, the Elsewhere Principle as selectBy on feature cardinality (Halle 1997's counting formulation).

def pattern L71–75

{K : Type u_1} {Cell : Type u_2} {F : Type u_3} {D : Cell → Finset K} [DecidableEq K] (v : Exponence.RuleSet (Rule Cell D F)) (c : Cell) :

Option F

pattern v c = Option.map Rule.exponent (v.selectBy (fun (r : Rule Cell D F) => r.feats.card) c)

Built from

Used in Morphology/Exponence/Containment/Selection, ChristopoulosZompi2023, Zompi2023

When the middle cell y nests between the outer cells, with D y ⊆ D z (appliers at y persist to z) and D x ∩ D z ⊆ D y (appliers at both outer cells reach y), a rule winning both x and z also wins y, so no exponent can interrupt an A_A pattern with a distinct middle B. This is *ABA order-theoretically. The hypotheses are the shared profile of Strong and Weak Case Containment, and No Case Containment violates the first.

theorem noABA L77–91

{K : Type u_1} {Cell : Type u_2} {F : Type u_3} {D : Cell → Finset K} [DecidableEq K] {v : Exponence.RuleSet (Rule Cell D F)} {A B : Rule Cell D F} {x y z : Cell} (h1 : D y ⊆ D z) (h2 : D x ∩ D z ⊆ D y) (hx : IsWinner v x A) (hz : IsWinner v z A) (hy : IsWinner v y B) :

B = A

Built from ,