Saab (2026): NP-Ellipsis Patterns in Spanish Binominals

This file formalizes the paper's argument that pseudo-partitive and quantificational binominals (un grupo, un montón de estudiantes) and qualitative binominals (una mierda de departamento) have different underlying syntax. In the former the genitive coda is the nP complement of Num, a primeval genitive in the sense of [Pes13], so an [E]-feature on Num licenses NP-ellipsis of the coda under the usual identity condition of [Mer01], and Num controls verbal agreement; in the latter the coda is the specifier of an equative phrase relating it to an indexical empty noun, so no licensor can elide it and its gap is resolved by context rather than by an antecedent. A structure is the nominal that is the complement of Num together with the nominal in the specifier above it (Structure). NP-ellipsis of a nominal is licensed exactly when it is that complement and has internal structure (Structure.Elidable), and the verb agrees with the number of that complement. The same principle covers the paper's structural ambiguity of quantity nouns: under the descriptive reading the noun heads the projection, so it can be elided and the verb is singular, and under the quantificational reading the coda heads it, so the coda can be elided and the verb is plural (elidable_first_iff_singular). The rows are the paper's examples, with the type of each first noun read from the Spanish fragment, and their ellipsis, agreement and gap facts follow from the structure assigned to them (ellipsis_matches).

Implementation notes

Identity between an antecedent and an ellipsis site is taken modulo case and number, as the paper argues: case is assigned at PF or overwritten by D after identity is computed, and number sits on the licensing head outside the ellipsis domain. The paper's three kinds of nominal gap are distinguished by the recovery they need, a linguistic antecedent for ellipsis, a contextual assignment for the indexical empty noun and none for a silent noun. The first two are anaphoric, and their depth in the sense of [HS76] is read from the Minimalist model of null sites (Minimalist.NullSite): NP-ellipsis is the nP that [E] on Num silences, a surface anaphor, and the indexical empty noun is a null pro-form at n, a deep one. The sub-extraction and argument-structure diagnostics of the rows test for internal structure, and the context diagnostic for a deep anaphor. Pesetsky's derivation of genitive marking and the equations at the entity and proposition types are not formalized.

References

• [Saa26]
• [Pes13]
• [Mer01]
• [HS76]

Structures

inductive Saab2026.Nominal : Type

The nominals of a binominal are the first noun, the genitive coda, and the indexical empty noun of the equative structure.

• first : Nominal
• coda : Nominal
• index : Nominal

@[instance_reducible]

instance Saab2026.instDecidableEqNominal : DecidableEq Nominal

Equations

• Saab2026.instDecidableEqNominal x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Saab2026.instReprNominal : Repr Nominal

Equations

• Saab2026.instReprNominal = { reprPrec := Saab2026.instReprNominal.repr }

def Saab2026.instReprNominal.repr : Nominal → ℕ → Std.Format

Equations

• Saab2026.instReprNominal.repr Saab2026.Nominal.first prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Saab2026.Nominal.first")).group prec✝
• Saab2026.instReprNominal.repr Saab2026.Nominal.coda prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Saab2026.Nominal.coda")).group prec✝
• Saab2026.instReprNominal.repr Saab2026.Nominal.index prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Saab2026.Nominal.index")).group prec✝

@[instance_reducible]

instance Saab2026.instFintypeNominal : Fintype Nominal

Equations

• Saab2026.instFintypeNominal = { elems := { val := ↑Saab2026.Nominal.enumList, nodup := Saab2026.Nominal.enumList_nodup }, complete := Saab2026.instFintypeNominal._proof_1 }

structure Saab2026.Structure : Type

A structure records the nominal that is the complement of Num, the head of the extended projection, and the nominal in the specifier above it.

• head : Nominal
• spec : Option Nominal

def Saab2026.instDecidableEqStructure.decEq (x✝ x✝¹ : Structure) : Decidable (x✝ = x✝¹)

Equations

• Saab2026.instDecidableEqStructure.decEq { head := a, spec := a_1 } { head := b, spec := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[instance_reducible]

instance Saab2026.instDecidableEqStructure : DecidableEq Structure

Equations

• Saab2026.instDecidableEqStructure = Saab2026.instDecidableEqStructure.decEq

def Saab2026.instReprStructure.repr : Structure → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Saab2026.instReprStructure : Repr Structure

Equations

• Saab2026.instReprStructure = { reprPrec := Saab2026.instReprStructure.repr }

@[instance_reducible]

instance Saab2026.instFintypeStructure : Fintype Structure

Equations

• Saab2026.instFintypeStructure = Fintype.ofEquiv ((_ : Saab2026.Nominal) × Option Saab2026.Nominal) Saab2026.Structure.proxyTypeEquiv

def Saab2026.quantificational : Structure

In the primeval-genitive structure of pseudo-partitive and quantificational binominals the coda is the nP complement of Num and the quantity phrase sits in the specifier.

Equations

• Saab2026.quantificational = { head := Saab2026.Nominal.coda, spec := some Saab2026.Nominal.first }

def Saab2026.descriptive : Structure

Under the descriptive reading of a quantity noun the noun heads the projection and the coda is its complement.

Equations

• Saab2026.descriptive = { head := Saab2026.Nominal.first, spec := none }

def Saab2026.equative : Structure

In the equative structure of qualitative binominals the complement of Num is the indexical empty noun, which the equative head relates to the coda in its specifier.

Equations

• Saab2026.equative = { head := Saab2026.Nominal.index, spec := some Saab2026.Nominal.coda }

def Saab2026.Structure.site (s : Structure) : Minimalist.NullSite Minimalist.Ellipsis.nominalSpine

The gap a structure leaves when its coda is missing, as a null site of the nominal spine. With the indexical empty noun as the complement of Num the gap is that noun, a null pro-form at n whose value the assignment function supplies; otherwise it is the nP that [E] on Num silences.

Equations

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

def Saab2026.Structure.depth (s : Structure) : Anaphor.Depth

The depth of the gap, read from the Minimalist model of null sites.

Equations

• s.depth = Anaphor.DepthModel.depth s.site

theorem Saab2026.Structure.hasInternalStructure_depth_iff (s : Structure) : s.depth.HasInternalStructure ↔ s.site.Silences (Minimalist.ClauseSpine.Site.head Minimalist.Cat.N)

The gap has internal structure exactly when it contains the noun's position, where the noun's arguments and any sub-extracted material originate.

def Saab2026.Structure.Elidable (s : Structure) (x : Nominal) : Prop

A nominal can be elided when it is the complement of Num, whose [E]-feature licenses the ellipsis of its complement, and the gap has internal structure: the indexical empty noun is an atomic index, so eliding it is vacuous.

Equations

• s.Elidable x = (s.head = x ∧ s.depth.HasInternalStructure)

@[instance_reducible]

instance Saab2026.instDecidableElidable (s : Structure) (x : Nominal) : Decidable (s.Elidable x)

Equations

• Saab2026.instDecidableElidable s x = { decide := decide (s.head = x) && decide s.depth.HasInternalStructure, reflects_decide := ⋯ }

def Saab2026.Nominal.number (c : Number) : Nominal → Number

The number of a nominal, given the coda's. The first noun is singular, and the indexical empty noun takes the coda's number through the equation.

Equations

• Saab2026.Nominal.number c Saab2026.Nominal.first = Number.singular
• Saab2026.Nominal.number c Saab2026.Nominal.coda = c
• Saab2026.Nominal.number c Saab2026.Nominal.index = c

def Saab2026.Structure.agreement (s : Structure) (c : Number) : Number

The verb agrees with the Num head, whose number is that of its complement.

Equations

• s.agreement c = Saab2026.Nominal.number c s.head

theorem Saab2026.equative_not_elidable (x : Nominal) : ¬equative.Elidable x

Nothing in the equative structure can be elided, since the coda has no licensor and the index is atomic.

theorem Saab2026.quantificational_descriptive_elidable : quantificational.Elidable Nominal.coda ∧ ¬quantificational.Elidable Nominal.first ∧ descriptive.Elidable Nominal.first ∧ ¬descriptive.Elidable Nominal.coda

The quantificational structure elides its coda and not the quantity noun; the descriptive structure the reverse.

Readings

inductive Saab2026.Reading : Type

The two readings of a quantity noun.

• quantificational : Reading
• descriptive : Reading

@[instance_reducible]

instance Saab2026.instDecidableEqReading : DecidableEq Reading

Equations

• Saab2026.instDecidableEqReading x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Saab2026.instReprReading : Repr Reading

Equations

• Saab2026.instReprReading = { reprPrec := Saab2026.instReprReading.repr }

def Saab2026.instReprReading.repr : Reading → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Saab2026.instFintypeReading : Fintype Reading

Equations

• Saab2026.instFintypeReading = { elems := { val := ↑Saab2026.Reading.enumList, nodup := Saab2026.Reading.enumList_nodup }, complete := Saab2026.instFintypeReading._proof_1 }

def Saab2026.structureOf : Spanish.Binominals.BinominalType → Reading → Structure

The structure of a binominal of a given type under a reading.

Equations

• Saab2026.structureOf Spanish.Binominals.BinominalType.qualitative x✝ = Saab2026.equative
• Saab2026.structureOf x✝ Saab2026.Reading.quantificational = Saab2026.quantificational
• Saab2026.structureOf x✝ Saab2026.Reading.descriptive = Saab2026.descriptive

theorem Saab2026.elidable_first_iff_singular (b : Spanish.Binominals.BinominalType) (r : Reading) (hb : b ≠ Spanish.Binominals.BinominalType.qualitative) : (structureOf b r).Elidable Nominal.first ↔ (structureOf b r).agreement Number.plural = Number.singular

With a plural coda, a quantity noun can be elided exactly when the verb agrees in the singular: both follow from the noun heading the projection.

The paper's examples

def Saab2026.binominalType? (x : Datum) : Option Spanish.Binominals.BinominalType

A row's binominal type, from the fragment entry of its first noun.

Equations

• Saab2026.binominalType? x = (x.feature? "noun").bind fun (f : String) => Option.map (fun (x : Spanish.Binominals.BinominalNoun) => x.binominalType) (Spanish.Binominals.lookup f)

def Saab2026.readings : List (String × Reading)

Equations

• Saab2026.readings = [("quantificational", Saab2026.Reading.quantificational), ("descriptive", Saab2026.Reading.descriptive)]

def Saab2026.structure? (x : Datum) : Option Structure

The structure the paper assigns to a row follows from its first noun's type and, for a quantity noun, its reading, which is quantificational unless recorded otherwise.

Equations

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

def Saab2026.nominals : List (String × Nominal)

Equations

• Saab2026.nominals = [("first", Saab2026.Nominal.first), ("coda", Saab2026.Nominal.coda)]

def Saab2026.numbers : List (String × Number)

Equations

• Saab2026.numbers = [("singular", Number.singular), ("plural", Number.plural)]

def Saab2026.EllipsisAcceptable (x : Datum) : Prop

The ellipsis reading of a row is acceptable when the reading's judgment, or the row's if none is recorded for the reading, is acceptable.

Equations

• Saab2026.EllipsisAcceptable x = ((List.lookup "ellipsis" x.readings).getD x.judgment = Judgment.acceptable)

@[instance_reducible]

instance Saab2026.instDecidableEllipsisAcceptable (x : Datum) : Decidable (EllipsisAcceptable x)

Equations

• Saab2026.instDecidableEllipsisAcceptable x = id inferInstance

theorem Saab2026.structure?_isSome (x : Datum) : x ∈ Examples.all → (structure? x).isSome = true

Every row names a first noun of the fragment, so each of the theorems below speaks about all the rows.

theorem Saab2026.ellipsis_matches (x : Datum) : x ∈ Examples.all → ∀ (s : Structure), structure? x = some s → ∀ (e : Nominal), x.parse? "elided" nominals = some e → (EllipsisAcceptable x ↔ s.Elidable e)

In the rows that elide a nominal, the ellipsis reading is acceptable exactly when the row's structure licenses eliding that nominal.

theorem Saab2026.agreement_matches (x : Datum) : x ∈ Examples.all → ∀ (s : Structure), structure? x = some s → (x.feature? "agreement").isSome = true → x.parse? "agreement" numbers = Option.map s.agreement (x.parse? "codaNumber" numbers)

The rows that record verbal agreement agree with the Num head of the row's structure.

theorem Saab2026.diagnostics_match (x : Datum) : x ∈ Examples.all → ∀ (s : Structure), structure? x = some s → (x.feature? "diagnostic" = some "subextraction" ∨ x.feature? "diagnostic" = some "argumentStructure" → (x.judgment = Judgment.acceptable ↔ s.depth.HasInternalStructure)) ∧ (x.feature? "diagnostic" = some "contextResolved" → (x.judgment = Judgment.acceptable ↔ s.depth = Anaphor.Depth.deep))

In the diagnostic rows, sub-extraction and argument structure succeed exactly when the gap has internal structure, and resolution by the context exactly when it is a deep anaphor.