Documentation

Linglib.Core.Lexical.Binominal

Binominal Noun Phrase Classification #

Cross-linguistic types for binominal (N₁-of-N₂) constructions.

Binominal NPs surface across languages with a linking element (English of, Spanish de, French de) but differ in internal structure, headedness, and N₁ semantics. This module provides a shared taxonomy drawn from @cite{saab-2026} (Spanish) and @cite{ten-wolde-2023} (English).

Taxonomy #

The six-way classification follows @cite{ten-wolde-2023}'s hierarchy, which subsumes @cite{saab-2026}'s three-way Spanish split:

Type	Example	N₁ function	Head
nPP	the beast of the field	referential	N₁
headClassifier	a cake of rye	classifies N₂	N₁
pseudoPartitive	a glass of water	quantizes N₂	N₂
evaluative	that idiot of a doctor	evaluates N₂	N₂
evaluativeModifier	a hell of a time	[N₁ of a] modifies N₂	N₂
binominalIntensifier	a whale of a good time	[N₁ of a] intensifies Adj	N₂

The first three are quantifying BNPs; the last three are quality BNPs (@cite{ten-wolde-2023}).

inductive Core.Lexical.Binominal.BinominalType :

The three-way binominal classification (@cite{saab-2026}).

This coarser-grained taxonomy covers the structural types attested across Romance binominals. The finer-grained English subtypes are captured by OfBinominalType.

pseudoPartitive : BinominalType
quantificational : BinominalType
qualitative : BinominalType

Instances For

instance Core.Lexical.Binominal.instDecidableEqBinominalType :

DecidableEq BinominalType

Equations

Core.Lexical.Binominal.instDecidableEqBinominalType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Core.Lexical.Binominal.instBEqBinominalType :

BEq BinominalType

Equations

Core.Lexical.Binominal.instBEqBinominalType = { beq := Core.Lexical.Binominal.instBEqBinominalType.beq }

def Core.Lexical.Binominal.instBEqBinominalType.beq :

BinominalType → BinominalType → Bool

Equations

Core.Lexical.Binominal.instBEqBinominalType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

def Core.Lexical.Binominal.instReprBinominalType.repr :

BinominalType → Nat → Std.Format

Equations

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

Instances For

instance Core.Lexical.Binominal.instReprBinominalType :

Repr BinominalType

Equations

Core.Lexical.Binominal.instReprBinominalType = { reprPrec := Core.Lexical.Binominal.instReprBinominalType.repr }

def Core.Lexical.Binominal.BinominalType.licensesNPE :

BinominalType → Bool

Does this binominal type license NP-ellipsis? @cite{saab-2026}: pseudo-partitive and quantificational yes; qualitative no.

Equations

Instances For

def Core.Lexical.Binominal.BinominalType.hasNumE :

BinominalType → Bool

Does the Num head in this structure carry [E]? @cite{saab-2026}: Num[E] is present iff the complement of Num is a standard nP (not an EquP with an indexical empty noun).

Equations

Instances For

theorem Core.Lexical.Binominal.npe_iff_numE (b : BinominalType) :

b.licensesNPE = b.hasNumE

Core result: NP-ellipsis is licensed iff Num has [E].

inductive Core.Lexical.Binominal.BNPHead :

Which noun is the semantic head of the binominal construction.

n₁ : BNPHead
n₂ : BNPHead

Instances For

def Core.Lexical.Binominal.instReprBNPHead.repr :

BNPHead → Nat → Std.Format

Equations

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

Instances For

instance Core.Lexical.Binominal.instReprBNPHead :

Equations

Core.Lexical.Binominal.instReprBNPHead = { reprPrec := Core.Lexical.Binominal.instReprBNPHead.repr }

instance Core.Lexical.Binominal.instDecidableEqBNPHead :

DecidableEq BNPHead

Equations

Core.Lexical.Binominal.instDecidableEqBNPHead x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Core.Lexical.Binominal.instBEqBNPHead :

Equations

Core.Lexical.Binominal.instBEqBNPHead = { beq := Core.Lexical.Binominal.instBEqBNPHead.beq }

def Core.Lexical.Binominal.instBEqBNPHead.beq :

BNPHead → BNPHead → Bool

Equations

Core.Lexical.Binominal.instBEqBNPHead.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

inductive Core.Lexical.Binominal.OfBinominalType :

The six types of of-binominal construction (@cite{ten-wolde-2023}).

The ordering reflects the grammaticalization cline: N+PP → Head-Classifier → Pseudo-partitive / Evaluative → EM → BI.

nPP : OfBinominalType
N+PP: N₁ denotes a referent, PP ascribes a property. the beast of the field, the hell of the damned
headClassifier : OfBinominalType
Head-classifier: PP classifies the type or material of N₁. a cake of rye, a beast of prey
pseudoPartitive : OfBinominalType
Pseudo-partitive: N₁ quantizes, N₂ is semantic head. a glass of water, a piece of cake, a bunch of flowers
evaluative : OfBinominalType
Evaluative BNP (EBNP): N₁ ascribes evaluative property to N₂. that idiot of a doctor, a whale of a man
evaluativeModifier : OfBinominalType
Evaluative Modifier (EM): [N₁ of a] is a complex modifier. a hell of a time, a whale of a job
binominalIntensifier : OfBinominalType
Binominal Intensifier (BI): [N₁ of a] intensifies Adj/Quant. a hell of a good time, a whale of a lot of fun

Instances For

instance Core.Lexical.Binominal.instReprOfBinominalType :

Repr OfBinominalType

Equations

Core.Lexical.Binominal.instReprOfBinominalType = { reprPrec := Core.Lexical.Binominal.instReprOfBinominalType.repr }

def Core.Lexical.Binominal.instReprOfBinominalType.repr :

OfBinominalType → Nat → Std.Format

Equations

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

Instances For

instance Core.Lexical.Binominal.instDecidableEqOfBinominalType :

DecidableEq OfBinominalType

Equations

Core.Lexical.Binominal.instDecidableEqOfBinominalType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Core.Lexical.Binominal.instBEqOfBinominalType.beq :

OfBinominalType → OfBinominalType → Bool

Equations

Core.Lexical.Binominal.instBEqOfBinominalType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

instance Core.Lexical.Binominal.instBEqOfBinominalType :

BEq OfBinominalType

Equations

Core.Lexical.Binominal.instBEqOfBinominalType = { beq := Core.Lexical.Binominal.instBEqOfBinominalType.beq }

def Core.Lexical.Binominal.OfBinominalType.head :

OfBinominalType → BNPHead

Which noun is the semantic head of each construction type.

For evaluative BNPs, N₂ is the semantic and discourse head, though syntactic evidence for headedness is inconclusive (@cite{ten-wolde-2023} Table 4.2). For EM and BI, N₂ is semantic, syntactic, and discourse head.

Equations

Instances For

def Core.Lexical.Binominal.OfBinominalType.n₁IsEvaluative :

OfBinominalType → Bool

Is N₁ evaluative (expresses speaker attitude)?

Equations

Instances For

def Core.Lexical.Binominal.OfBinominalType.n₁IsReferential :

OfBinominalType → Bool

Is N₁ referential (denotes an entity in the world)?

Equations

Instances For

def Core.Lexical.Binominal.OfBinominalType.n₁Bleached :

OfBinominalType → Bool

Does N₁ undergo semantic bleaching (loss of lexical content)? Bleaching increases along the grammaticalization cline.

The nature of bleaching differs: pseudo-partitive N₁ (glass, piece) bleaches from referential noun → quantizing measure term; evaluative N₁ bleaches from gradable predicate (EBNP) → evaluative modifier (EM) → degree intensifier (BI).

Equations

Instances For

def Core.Lexical.Binominal.OfBinominalType.ofIsLinker :

OfBinominalType → Bool

Does of function as a linking device (no independent semantics)? In earlier constructions, of retains prepositional meaning (location, possession); in later ones it is a pure linker.

Equations

Instances For

def Core.Lexical.Binominal.OfBinominalType.n₁AllowsPlural :

OfBinominalType → Bool

Can N₁ appear in plural form? Along the cline, N₁ loses the ability to inflect.

Equations

Instances For

def Core.Lexical.Binominal.OfBinominalType.det₂MarksNumber :

OfBinominalType → Bool

Does Det₂ still mark number? In the EBNP, the second determiner marks number; in EM and BI it no longer does (@cite{ten-wolde-2023} Table 4.2).

Equations

Instances For

def Core.Lexical.Binominal.OfBinominalType.ofReplaceableByCopula :

OfBinominalType → Bool

Can of be replaced by a copular verb? In EBNP, of can sometimes be paraphrased with be (e.g., "the doctor is an idiot"); in EM and BI it cannot (@cite{ten-wolde-2023} §4.3.4, §4.4.5).

Equations

Instances For

def Core.Lexical.Binominal.OfBinominalType.n₁OfAIsConstituent :

OfBinominalType → Bool

Does [N₁ of a] function as a single constituent (modifier phrase)? The reanalysis of [N₁ of a] into a modifier unit is the defining structural change at the EM stage (@cite{ten-wolde-2023} §4.3.5).

Equations

Instances For

def Core.Lexical.Binominal.OfBinominalType.n₁AllowsDescriptivePremod :

OfBinominalType → Bool

Does N₁ allow descriptive premodification? @cite{ten-wolde-2023} Ch. 7: EBNP strongly favors premodification of N₁ (a total idiot of a doctor); EM and BI block it because [N₁ of a] has been reanalyzed as a unit. Earlier constructions (N+PP, HC, PP) allow free premodification of N₁.

Equations

Instances For

def Core.Lexical.Binominal.OfBinominalType.n₂AllowsMass :

OfBinominalType → Bool

Can N₂ be a mass noun? EBNP and EM restrict N₂ to count and collective nouns; BI extends to mass nouns (sporadically — not freely productive), reflecting the structural change where [N₁ of a] modifies a following adjective rather than N₂ directly (@cite{ten-wolde-2023} Table 4.2). Earlier types (N+PP, HC, PP) have no such restriction.

Equations

Instances For

inductive Core.Lexical.Binominal.AgreementLevel :

Level of number agreement between N₁ and N₂.

agree : AgreementLevel
N₁ and N₂ agree in number.
usuallyAgree : AgreementLevel
N₁ and N₂ usually agree, with some exceptions.
noAgreement : AgreementLevel
N₁ and N₂ do not have to agree in number.

Instances For

def Core.Lexical.Binominal.instReprAgreementLevel.repr :

AgreementLevel → Nat → Std.Format

Equations

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

Instances For

instance Core.Lexical.Binominal.instReprAgreementLevel :

Repr AgreementLevel

Equations

Core.Lexical.Binominal.instReprAgreementLevel = { reprPrec := Core.Lexical.Binominal.instReprAgreementLevel.repr }

instance Core.Lexical.Binominal.instDecidableEqAgreementLevel :

DecidableEq AgreementLevel

Equations

Core.Lexical.Binominal.instDecidableEqAgreementLevel x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Core.Lexical.Binominal.instBEqAgreementLevel.beq :

AgreementLevel → AgreementLevel → Bool

Equations

Core.Lexical.Binominal.instBEqAgreementLevel.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

instance Core.Lexical.Binominal.instBEqAgreementLevel :

BEq AgreementLevel

Equations

Core.Lexical.Binominal.instBEqAgreementLevel = { beq := Core.Lexical.Binominal.instBEqAgreementLevel.beq }

def Core.Lexical.Binominal.AgreementLevel.toNat :

AgreementLevel → Nat

Numeric encoding: agreement loosens over time.

Equations

Instances For

instance Core.Lexical.Binominal.instLEAgreementLevel :

LE AgreementLevel

Equations

Core.Lexical.Binominal.instLEAgreementLevel = { le := fun (a b : Core.Lexical.Binominal.AgreementLevel) => a.toNat ≤ b.toNat }

instance Core.Lexical.Binominal.instDecidableLeAgreementLevel (a b : AgreementLevel) :

Decidable (a ≤ b)

Equations

Core.Lexical.Binominal.instDecidableLeAgreementLevel a b = inferInstanceAs (Decidable (a.toNat ≤ b.toNat))

def Core.Lexical.Binominal.OfBinominalType.n₁N₂Agreement :

OfBinominalType → AgreementLevel

N₁ & N₂ number agreement along the cline. Agreement loosens as grammaticalization proceeds: full agreement → usually agree → no agreement required (@cite{ten-wolde-2023} Table 4.2).

Equations

Instances For

def Core.Lexical.Binominal.OfBinominalType.ofObligatory :

OfBinominalType → Bool

Is of obligatory in the construction? Mandatory for all types except BI, where it can be absent in reduced forms like helluva, hella (@cite{ten-wolde-2023} Table 4.2).

Equations

Instances For

def Core.Lexical.Binominal.OfBinominalType.clinePosition :

OfBinominalType → Nat

Position on the grammaticalization cline (0 = most lexical, 5 = most grammatical).

Supported by diachronic corpus evidence (@cite{ten-wolde-2023}): constructions appear in English in this order historically, and N₁ nouns progress through these stages with increasing semantic bleaching.

Equations

Instances For

theorem Core.Lexical.Binominal.cline_injective (t₁ t₂ : OfBinominalType) :

t₁.clinePosition = t₂.clinePosition → t₁ = t₂

The cline is a total order: each type has a unique position.

theorem Core.Lexical.Binominal.bleaching_after_position_2 (t : OfBinominalType) :

2 ≤ t.clinePosition → t.n₁Bleached = true

Bleaching increases along the cline: all types at position ≥ 2 are bleached.

theorem Core.Lexical.Binominal.head_switches_at_2 (t : OfBinominalType) :

(t.head = BNPHead.n₁) = (t.clinePosition < 2)

Head switches from N₁ to N₂ at position 2.

theorem Core.Lexical.Binominal.plural_lost_at_4 (t : OfBinominalType) :

4 ≤ t.clinePosition → t.n₁AllowsPlural = false

N₁ plural ability is lost at position 4 (EM).

theorem Core.Lexical.Binominal.det₂_number_lost_at_4 (t : OfBinominalType) :

4 ≤ t.clinePosition → t.det₂MarksNumber = false

Det₂ number marking is lost at the same point as N₁ plural (position 4).

theorem Core.Lexical.Binominal.n₁_of_a_constituent_at_4 (t : OfBinominalType) :

4 ≤ t.clinePosition → t.n₁OfAIsConstituent = true

[N₁ of a] constituency emerges at position 4 (EM).

theorem Core.Lexical.Binominal.premod_lost_at_4 (t : OfBinominalType) :

4 ≤ t.clinePosition → t.n₁AllowsDescriptivePremod = false

N₁ descriptive premodification is lost at position 4 (EM), together with N₁ plural and [N₁ of a] constituency.

theorem Core.Lexical.Binominal.premod_loss_monotone (t₁ t₂ : OfBinominalType) :

t₁.clinePosition ≤ t₂.clinePosition → t₁.n₁AllowsDescriptivePremod = false → t₂.n₁AllowsDescriptivePremod = false

Monotonicity: once N₁ premodification is lost, it stays lost.

theorem Core.Lexical.Binominal.copula_only_evaluative (t : OfBinominalType) :

t.ofReplaceableByCopula = true → t = OfBinominalType.evaluative

Copula replacement is unique to evaluative BNPs.

theorem Core.Lexical.Binominal.evaluative_is_n₂_headed (t : OfBinominalType) :

t.n₁IsEvaluative = true → t.head = BNPHead.n₂

Evaluative types are always N₂-headed.

theorem Core.Lexical.Binominal.referential_is_n₁_headed (t : OfBinominalType) :

t.n₁IsReferential = true → t.head = BNPHead.n₁

Referential types are always N₁-headed.

theorem Core.Lexical.Binominal.bleaching_monotone (t₁ t₂ : OfBinominalType) :

t₁.clinePosition ≤ t₂.clinePosition → t₁.n₁Bleached = true → t₂.n₁Bleached = true

Monotonicity: once bleaching starts, it never reverses.

theorem Core.Lexical.Binominal.plural_loss_monotone (t₁ t₂ : OfBinominalType) :

t₁.clinePosition ≤ t₂.clinePosition → t₁.n₁AllowsPlural = false → t₂.n₁AllowsPlural = false

Monotonicity: once N₁ plural is lost, it stays lost.

theorem Core.Lexical.Binominal.agreement_loosens_monotone (t₁ t₂ : OfBinominalType) :

t₁.clinePosition ≤ t₂.clinePosition → t₁.n₁N₂Agreement.toNat ≤ t₂.n₁N₂Agreement.toNat

Agreement loosens monotonically along the cline.

theorem Core.Lexical.Binominal.n₂_mass_nonmonotone :

OfBinominalType.nPP.n₂AllowsMass = true ∧ OfBinominalType.evaluative.n₂AllowsMass = false ∧ OfBinominalType.binominalIntensifier.n₂AllowsMass = true

N₂ mass restriction is non-monotone: it narrows at the evaluative stage (positions 3–4) and widens again at BI (position 5), reflecting the structural change where [N₁ of a] shifts into AdjP.

theorem Core.Lexical.Binominal.of_optional_only_at_bi (t : OfBinominalType) :

t.ofObligatory = false → t.clinePosition = 5

of becomes optional only at the most grammaticalized stage (BI).

def Core.Lexical.Binominal.BinominalType.toOfBinominalType :

BinominalType → OfBinominalType

Map the three-way Spanish type to the six-way English type.

Equations

Instances For

theorem Core.Lexical.Binominal.qualitative_is_evaluative :

BinominalType.qualitative.toOfBinominalType.head = BNPHead.n₂

Spanish qualitative maps to an evaluative (N₂-headed) English type.

theorem Core.Lexical.Binominal.quantifying_is_n₂_headed (b : BinominalType) :

b = BinominalType.pseudoPartitive ∨ b = BinominalType.quantificational → b.toOfBinominalType.head = BNPHead.n₂

Spanish pseudo-partitive/quantificational map to N₂-headed types.