Derivational economy

Economy of derivation ([chomsky-1991], [chomsky-1995]) compares the derivations that converge on the same string with the same interpretation and keeps the least costly. A cost is a count per dimension: the lexical items drawn and the Merge operations, which are the distinct terms of the object built, its lexical leaves and its internal vertices each once, so that a shared constituent is built once; and the Agree operations and applications of ellipsis that [citko-gracanin-yuksek-2025] weigh alongside them. Costs are ordered pointwise: a derivation is more economical than another when it is no worse on every dimension and better on one. The order is well-founded (Dickson's lemma, Pi.wellFoundedLT), so every reference set has a winner (WellFoundedLT.exists_minimal). The cost of a planar object is read off its terms by Minimalist.planarCost in Linearization/Chain.lean.

Main definitions

• CostDimension, DerivationCost: the dimensions and a count per dimension.

References

• [N. Chomsky, Some notes on economy of derivation and representation (1991)][chomsky-1991]
• [N. Chomsky, The Minimalist Program (1995)][chomsky-1995]
• [B. Citko and M. Gračanin-Yuksek, Economy in PF reduction (2025)][citko-gracanin-yuksek-2025]

inductive Minimalist.CostDimension : Type

The dimensions of derivational cost.

• lexicalItems : CostDimension
• mergeOps : CostDimension
• agreeOps : CostDimension
• ellipsisOps : CostDimension

@[instance_reducible]

instance Minimalist.instDecidableEqCostDimension : DecidableEq CostDimension

Equations

• Minimalist.instDecidableEqCostDimension x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Minimalist.instFintypeCostDimension : Fintype CostDimension

Equations

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

def Minimalist.instReprCostDimension.repr : CostDimension → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Minimalist.instReprCostDimension : Repr CostDimension

Equations

• Minimalist.instReprCostDimension = { reprPrec := Minimalist.instReprCostDimension.repr }

@[reducible, inline]

abbrev Minimalist.DerivationCost : Type

The cost of a derivation: a count per dimension, ordered pointwise.

Equations

• Minimalist.DerivationCost = (Minimalist.CostDimension → ℕ)

@[instance_reducible]

instance Minimalist.instDecidableLEDerivationCost : DecidableLE DerivationCost

Equations

• Minimalist.instDecidableLEDerivationCost a b = Fintype.decidableForallFintype

@[instance_reducible]

instance Minimalist.instDecidableLTDerivationCost : DecidableLT DerivationCost

Equations

• Minimalist.instDecidableLTDerivationCost a b = decidable_of_iff (a ≤ b ∧ ¬b ≤ a) ⋯