Impoverishment (Distributed Morphology)

@cite{halle-marantz-1993} @cite{bonet-1991}

Impoverishment is a postsyntactic operation that deletes features from a terminal node before Vocabulary Insertion. It is the DM mechanism for deriving syncretism: when two morphosyntactic contexts share an exponent, this can be explained by one context losing a distinguishing feature, making it fall together with the other at VI.

Architecture

A rule is evaluated against a Neighborhood — the focus terminal plus its immediately adjacent terminals — and a Prop-valued condition. The focus/context split is what licenses the paradigmatic / syntagmatic distinction structurally: a rule whose condition factors through Neighborhood.focus is paradigmatic (refers to one node only); otherwise it is syntagmatic. This is a theorem about the rule, not a stipulation, so paradigmatic-vs- syntagmatic claims can be discharged by proof rather than annotation.

Connection to Mam

@cite{scott-2023} (ch. 4) analyzes pronoun reduction in SJA Mam as deletion of the pronominal base morpheme when its features are redundantly expressed by agreement. This is structurally parallel to Impoverishment: features on the pronoun node are deleted (at PF) when they are recoverable from agreement, yielding a reduced form. Mam's rule is paradigmatic — see Phenomena/Agreement/Studies/Scott2023.lean.

structure Morphology.DM.Impoverishment.Neighborhood : Type

The local context a postsyntactic rule may inspect. The focus bundle is the terminal targeted for deletion; leftCtx and rightCtx are the bundles of immediately adjacent terminals (left- and right-adjacent in the morphological structure).

Splitting focus from context is what makes the paradigmatic/syntagmatic distinction structural. A condition that only inspects focus is paradigmatic by construction; one that reads leftCtx or rightCtx is syntagmatic.

• focus : Minimalist.FeatureBundle
• leftCtx : List Minimalist.FeatureBundle
• rightCtx : List Minimalist.FeatureBundle

@[implicit_reducible]

instance Morphology.DM.Impoverishment.instReprNeighborhood : Repr Neighborhood

Equations

• Morphology.DM.Impoverishment.instReprNeighborhood = { reprPrec := Morphology.DM.Impoverishment.instReprNeighborhood.repr }

def Morphology.DM.Impoverishment.instReprNeighborhood.repr : Neighborhood → ℕ → Std.Format

Equations

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

def Morphology.DM.Impoverishment.Neighborhood.ofBundle (fb : Minimalist.FeatureBundle) : Neighborhood

A bundle, viewed as a context-free neighborhood.

Equations

• Morphology.DM.Impoverishment.Neighborhood.ofBundle fb = { focus := fb }

structure Morphology.DM.Impoverishment.ImpoverishmentRule : Type

An Impoverishment rule deletes target from the focus terminal when condition holds over the neighborhood.

condition is Prop-valued (the mathlib idiom — see CHANGELOG entry for GroszJoshiWeinstein1995.lean and the OT/Conditionals migrations); a DecidablePred witness is carried alongside so that applyImpoverishment reduces by decide on concrete inputs.

• condition : Neighborhood → Prop

  Does this rule apply at the given neighborhood?

• decCond : DecidablePred self.condition

  Decidability witness, exposed as an instance (see below).

• target : Minimalist.FeatureVal

  Which feature type is deleted from the focus bundle.

@[implicit_reducible]

instance Morphology.DM.Impoverishment.instDecidableCondition (rule : ImpoverishmentRule) (n : Neighborhood) : Decidable (rule.condition n)

Expose the rule's decidability as an instance so that if rule.condition n then ... else ... elaborates.

Equations

• Morphology.DM.Impoverishment.instDecidableCondition rule n = rule.decCond n

def Morphology.DM.Impoverishment.Paradigmatic (r : ImpoverishmentRule) : Prop

A rule is paradigmatic iff its condition factors through the focus bundle: any two neighborhoods with the same focus agree on the condition. This is the structural counterpart of @cite{arregi-nevins-2012}'s "rule conditioned by the features of only one node."

Crucially, this is a theorem about a rule, not a flag. Smart constructors below (paradigmatic, syntagmatic) discharge it automatically when the condition is built focus-only.

Equations

• Morphology.DM.Impoverishment.Paradigmatic r = ∀ (n₁ n₂ : Morphology.DM.Impoverishment.Neighborhood), n₁.focus = n₂.focus → (r.condition n₁ ↔ r.condition n₂)

def Morphology.DM.Impoverishment.Syntagmatic (r : ImpoverishmentRule) : Prop

A rule is syntagmatic iff it is not paradigmatic — i.e., there exist neighborhoods agreeing on focus that disagree on the condition, so the condition genuinely depends on context.

Equations

• Morphology.DM.Impoverishment.Syntagmatic r = ¬Morphology.DM.Impoverishment.Paradigmatic r

def Morphology.DM.Impoverishment.paradigmatic (focusCheck : Minimalist.FeatureBundle → Bool) (target : Minimalist.FeatureVal) : ImpoverishmentRule

Build a paradigmatic rule from a focus-only Boolean check. The Paradigmatic proof is automatic via paradigmatic_isParadigmatic.

Equations

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

theorem Morphology.DM.Impoverishment.paradigmatic_isParadigmatic (focusCheck : Minimalist.FeatureBundle → Bool) (target : Minimalist.FeatureVal) : Paradigmatic (paradigmatic focusCheck target)

A rule built by paradigmatic is paradigmatic by construction.

def Morphology.DM.Impoverishment.syntagmatic (cond : Neighborhood → Bool) (target : Minimalist.FeatureVal) : ImpoverishmentRule

Build a (potentially) syntagmatic rule from a full-neighborhood Boolean check. Whether the result is genuinely syntagmatic depends on cond — verify with a separate Syntagmatic proof if needed.

Equations

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

def Morphology.DM.Impoverishment.deleteFeature (fb : Minimalist.FeatureBundle) (target : Minimalist.FeatureVal) : Minimalist.FeatureBundle

Delete all features matching target from a bundle.

Equations

• Morphology.DM.Impoverishment.deleteFeature fb target = List.filter (fun (f : Minimalist.GramFeature) => !f.featureType.sameType target) fb

def Morphology.DM.Impoverishment.applyImpoverishment (rule : ImpoverishmentRule) (n : Neighborhood) : Minimalist.FeatureBundle

Apply an Impoverishment rule at a neighborhood: when the condition holds, return the focus with target deleted; otherwise return the focus unchanged.

Equations

• Morphology.DM.Impoverishment.applyImpoverishment rule n = if rule.condition n then Morphology.DM.Impoverishment.deleteFeature n.focus rule.target else n.focus

def Morphology.DM.Impoverishment.runChain {R : Type} (apply : R → Neighborhood → Minimalist.FeatureBundle) (rules : List R) (n : Neighborhood) : Minimalist.FeatureBundle

Generic postsyntactic chain: apply a list of rules to a neighborhood, threading the focus bundle through each step while holding the surrounding context fixed. This is the shared shape of one cycle of Impoverishment and one cycle of Metathesis (and any other focus-rewriting rule class).

Equations

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

theorem Morphology.DM.Impoverishment.runChain_append {R : Type} (apply : R → Neighborhood → Minimalist.FeatureBundle) (rs₁ rs₂ : List R) (n : Neighborhood) : runChain apply (rs₁ ++ rs₂) n = runChain apply rs₂ { focus := runChain apply rs₁ n, leftCtx := n.leftCtx, rightCtx := n.rightCtx }

Concatenating two chains is the same as running them sequentially: the second chain starts where the first left off. The proof is List.foldl_append. This lemma underwrites the strict-vs-interleaved equivalence in Theories/Morphology/DM/PostsyntacticDerivation.lean.

@[simp]

theorem Morphology.DM.Impoverishment.runChain_nil {R : Type} (apply : R → Neighborhood → Minimalist.FeatureBundle) (n : Neighborhood) : runChain apply [] n = n.focus

The empty chain is the identity on the focus.

def Morphology.DM.Impoverishment.applyImpoverishmentChain (rules : List ImpoverishmentRule) (n : Neighborhood) : Minimalist.FeatureBundle

Apply a sequence of impoverishment rules. Specializes runChain.

Equations

• Morphology.DM.Impoverishment.applyImpoverishmentChain rules n = Morphology.DM.Impoverishment.runChain Morphology.DM.Impoverishment.applyImpoverishment rules n

theorem Morphology.DM.Impoverishment.applyImpoverishmentChain_append (rs₁ rs₂ : List ImpoverishmentRule) (n : Neighborhood) : applyImpoverishmentChain (rs₁ ++ rs₂) n = applyImpoverishmentChain rs₂ { focus := applyImpoverishmentChain rs₁ n, leftCtx := n.leftCtx, rightCtx := n.rightCtx }

applyImpoverishmentChain distributes over list concatenation.

def Morphology.DM.Impoverishment.ImpoverishmentRule.applyToBundle (rule : ImpoverishmentRule) (fb : Minimalist.FeatureBundle) : Minimalist.FeatureBundle

Convenience: apply a rule to a bare focus bundle with no surrounding context. Useful for paradigmatic rules where context is irrelevant.

Equations

• rule.applyToBundle fb = Morphology.DM.Impoverishment.applyImpoverishment rule (Morphology.DM.Impoverishment.Neighborhood.ofBundle fb)

def Morphology.DM.Impoverishment.allRecoverable (recoverable pronFeatures : List Minimalist.FeatureVal) : Bool

A feature is redundant when it is recoverable from another source (e.g., agreement morphology on the verb). This is the mechanism underlying pronoun reduction in Mam (@cite{scott-2023}, ch. 4): when all features of the pronominal base are also expressed by agreement, the base is deleted at PF.

Equations

• Morphology.DM.Impoverishment.allRecoverable recoverable pronFeatures = pronFeatures.all fun (f : Minimalist.FeatureVal) => recoverable.any fun (x : Minimalist.FeatureVal) => f.sameType x

def Morphology.DM.Impoverishment.redundancyRule (source : List Minimalist.FeatureVal) (target : Minimalist.FeatureVal) : ImpoverishmentRule

Build a redundancy-based Impoverishment rule. The condition only inspects the focus bundle, so the rule is paradigmatic by construction.

Equations

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

theorem Morphology.DM.Impoverishment.redundancyRule_isParadigmatic (source : List Minimalist.FeatureVal) (target : Minimalist.FeatureVal) : Paradigmatic (redundancyRule source target)

Redundancy rules are paradigmatic.

theorem Morphology.DM.Impoverishment.deleteFeature_idempotent (fb : Minimalist.FeatureBundle) (target : Minimalist.FeatureVal) : deleteFeature (deleteFeature fb target) target = deleteFeature fb target

Deleting a feature then deleting it again is the same as deleting once. (Filter is idempotent when the predicate is stable.)