Derivational Economy

@cite{chomsky-1995} @cite{chomsky-2000}

Economy principles constrain syntactic derivations by comparing competing derivations that converge on the same PF string and LF interpretation, selecting the one with fewest operations.

Key Principles

• Least Effort: Among derivations yielding the same PF string and LF interpretation, prefer the one with fewest operations and fewest lexical resources drawn from the numeration.
• Pronunciation Economy: PF-reducing operations (ellipsis) may apply only if they have an effect on pronunciation. This bans vacuous deletion — eliding material that is already unpronounced.

Design

Economy is formalized as a COMPARISON between derivation costs, not as a constraint on individual derivations. This captures the global, transderivational character of economy: the grammar evaluates the full set of convergent derivations and selects the cheapest.

DerivationCost is abstract — it counts operations by type without committing to a particular derivation model. Both the core Derivation (step-based) and FullDerivation (workspace-based) models can project onto DerivationCost.

structure Minimalism.DerivationCost : Type

Cost of a syntactic derivation, measured by operation and resource counts.

The four dimensions capture the resources consumed:

• lexicalItems: items drawn from the numeration (lexical resources)
• mergeOps: External + Internal Merge (structure building)
• agreeOps: Agree operations (feature checking)
• ellipsisOps: E-feature triggered deletions at PF

• lexicalItems : ℕ
• mergeOps : ℕ
• agreeOps : ℕ
• ellipsisOps : ℕ

instance Minimalism.instReprDerivationCost : Repr DerivationCost

Equations

• Minimalism.instReprDerivationCost = { reprPrec := Minimalism.instReprDerivationCost.repr }

def Minimalism.instReprDerivationCost.repr : DerivationCost → ℕ → Std.Format

Equations

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

instance Minimalism.instDecidableEqDerivationCost : DecidableEq DerivationCost

Equations

• Minimalism.instDecidableEqDerivationCost = Minimalism.instDecidableEqDerivationCost.decEq

def Minimalism.instDecidableEqDerivationCost.decEq (x✝ x✝¹ : DerivationCost) : Decidable (x✝ = x✝¹)

Equations

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

def Minimalism.DerivationCost.totalOps (c : DerivationCost) : ℕ

Total number of syntactic operations (excluding lexical selection).

Equations

• c.totalOps = c.mergeOps + c.agreeOps + c.ellipsisOps

def Minimalism.Derivation.cost (d : Derivation) : DerivationCost

Extract cost from a core Derivation (step-based model).

Counts emL/emR as External Merge and im as Internal Merge. Agree and ellipsis are not tracked in the core model.

Equations

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

def Minimalism.atLeastAsEconomical (c1 c2 : DerivationCost) : Prop

Derivation c1 is at least as economical as c2: no more operations and no more lexical resources on any dimension.

Equations

• Minimalism.atLeastAsEconomical c1 c2 = (c1.totalOps ≤ c2.totalOps ∧ c1.lexicalItems ≤ c2.lexicalItems)

def Minimalism.strictlyMoreEconomical (c1 c2 : DerivationCost) : Prop

Derivation c1 is strictly more economical than c2: at least as economical, and strictly better on at least one dimension.

Equations

• Minimalism.strictlyMoreEconomical c1 c2 = (Minimalism.atLeastAsEconomical c1 c2 ∧ (c1.totalOps < c2.totalOps ∨ c1.lexicalItems < c2.lexicalItems))

theorem Minimalism.atLeastAsEconomical_refl (c : DerivationCost) : atLeastAsEconomical c c

Economy comparison is reflexive.

theorem Minimalism.atLeastAsEconomical_trans {c1 c2 c3 : DerivationCost} (h12 : atLeastAsEconomical c1 c2) (h23 : atLeastAsEconomical c2 c3) : atLeastAsEconomical c1 c3

Economy comparison is transitive.

theorem Minimalism.strictlyMoreEconomical_irrefl (c : DerivationCost) : ¬strictlyMoreEconomical c c

Strict economy is irreflexive.

theorem Minimalism.strictlyMoreEconomical_trans {c1 c2 c3 : DerivationCost} (h12 : strictlyMoreEconomical c1 c2) (h23 : strictlyMoreEconomical c2 c3) : strictlyMoreEconomical c1 c3

Strict economy is transitive.

theorem Minimalism.strictlyMoreEconomical_asymm {c1 c2 : DerivationCost} (h : strictlyMoreEconomical c1 c2) : ¬strictlyMoreEconomical c2 c1

Strict economy is asymmetric.

def Minimalism.pronunciationEconomy (pfBefore pfAfter : List String) : Prop

Pronunciation Economy: ellipsis may apply only if it changes the PF output.

An ellipsis operation that targets material already unpronounced (e.g., because a prior deletion already removed it) is vacuous and therefore banned.

pfBefore: the PF string before ellipsis applies. pfAfter: the PF string after ellipsis applies.

Equations

• Minimalism.pronunciationEconomy pfBefore pfAfter = (pfBefore ≠ pfAfter)

def Minimalism.vacuousEllipsis (pfBefore pfAfter : List String) : Prop

Vacuous ellipsis: the PF output is unchanged by the deletion.

Equations

• Minimalism.vacuousEllipsis pfBefore pfAfter = (pfBefore = pfAfter)

theorem Minimalism.pronEcon_iff_not_vacuous (pf1 pf2 : List String) : pronunciationEconomy pf1 pf2 ↔ ¬vacuousEllipsis pf1 pf2

Pronunciation Economy holds iff ellipsis is not vacuous.

def Minimalism.pfEquivalent (so1 so2 : SyntacticObject) : Prop

Two syntactic objects are PF-equivalent if they produce the same phonological string (left-to-right leaf yield).

Equations

• Minimalism.pfEquivalent so1 so2 = (so1.phonYield = so2.phonYield)

theorem Minimalism.pfEquivalent_refl (so : SyntacticObject) : pfEquivalent so so

PF equivalence is reflexive.

theorem Minimalism.pfEquivalent_symm {so1 so2 : SyntacticObject} (h : pfEquivalent so1 so2) : pfEquivalent so2 so1

PF equivalence is symmetric.

theorem Minimalism.pfEquivalent_trans {so1 so2 so3 : SyntacticObject} (h12 : pfEquivalent so1 so2) (h23 : pfEquivalent so2 so3) : pfEquivalent so1 so3

PF equivalence is transitive.