Argument Structure Constructions

@cite{goldberg-1995} @cite{goldberg-shirtz-2025}

CxG's argument structure constructions and their decomposition into Müller's three universal schemata.

@cite{mueller-2013} argues "both directions right": the three universal schemata capture fully abstract constructions (ditransitive, caused-motion, resultative), but partially open and lexically specified constructions are irreducible phrasal patterns that only CxG can capture.

Key claims

1. Fully abstract constructions decompose into sequences of Head-Complement and Head-Specifier steps
2. Partially open constructions (PAL, let alone, WXDY) are irreducible — they cannot be decomposed into the three schemata
3. This is CxG's unique contribution: phrasal constructions beyond the schemata

Construction slots and argument frames

structure ConstructionGrammar.ConstructionSlot : Type

A slot in an argument structure construction.

Each slot specifies a syntactic category and a semantic role for one participant in the construction's event structure.

• cat : UD.UPOS

  Syntactic category of this slot (NP, V, PP, etc.)

• role : String

  Semantic role label

• isHead : Bool

  Whether this slot is the head of the construction

def ConstructionGrammar.instReprConstructionSlot.repr : ConstructionSlot → ℕ → Std.Format

Equations

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

instance ConstructionGrammar.instReprConstructionSlot : Repr ConstructionSlot

Equations

• ConstructionGrammar.instReprConstructionSlot = { reprPrec := ConstructionGrammar.instReprConstructionSlot.repr }

def ConstructionGrammar.instBEqConstructionSlot.beq : ConstructionSlot → ConstructionSlot → Bool

Equations

• ConstructionGrammar.instBEqConstructionSlot.beq { cat := a, role := a_1, isHead := a_2 } { cat := b, role := b_1, isHead := b_2 } = (a == b && (a_1 == b_1 && a_2 == b_2))
• ConstructionGrammar.instBEqConstructionSlot.beq x✝¹ x✝ = false

instance ConstructionGrammar.instBEqConstructionSlot : BEq ConstructionSlot

Equations

• ConstructionGrammar.instBEqConstructionSlot = { beq := ConstructionGrammar.instBEqConstructionSlot.beq }

structure ConstructionGrammar.ArgStructureConstruction : Type

An argument structure construction with explicit slot structure.

This extends the basic Construction with a decomposed argument frame, enabling formal analysis of how the construction relates to the three universal combination schemata.

The semanticContribution field captures which meaning components (@cite{levin-1993}) the construction adds independently of the verb (@cite{goldberg-1995}). When a verb fuses with a construction, the composed meaning = verb.meaningComponents.fuse cxn.semanticContribution. This is how constructions can license alternation behavior that verbs lack in isolation — e.g., the resultative adds CoS + causation, enabling the causative alternation for manner verbs (@cite{levin-2026}).

• construction : Construction

  The underlying construction

• slots : List ConstructionSlot

  The argument frame: ordered list of slots

• hasHead : (self.slots.any fun (x : ConstructionSlot) => x.isHead) = true

  At least one slot should be the head

• semanticContribution : MeaningComponents

  What meaning components this construction contributes independently of the verb. Defaults to .none (no augmentation).

def ConstructionGrammar.instReprArgStructureConstruction.repr : ArgStructureConstruction → ℕ → Std.Format

Equations

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

instance ConstructionGrammar.instReprArgStructureConstruction : Repr ArgStructureConstruction

Equations

• ConstructionGrammar.instReprArgStructureConstruction = { reprPrec := ConstructionGrammar.instReprArgStructureConstruction.repr }

Concrete argument structure constructions

def ConstructionGrammar.ditransitive : ArgStructureConstruction

Ditransitive construction: [Subj V Obj1 Obj2]. "X CAUSES Y to RECEIVE Z" (e.g., "She gave him a book").

Equations

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

def ConstructionGrammar.causedMotion : ArgStructureConstruction

Caused-motion construction: [Subj V Obj Obl]. "X CAUSES Y to MOVE to Z" (e.g., "She sneezed the napkin off the table"). Contributes motion + causation: verbs that lexicalize neither (like sneeze) acquire both from the construction (@cite{goldberg-1995} p. 152–179).

Equations

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

def ConstructionGrammar.resultative : ArgStructureConstruction

Resultative construction: [Subj V Obj Pred]. "X CAUSES Y to BECOME Z" (e.g., "She hammered the metal flat"). Contributes CoS + causation: manner verbs that lexicalize neither acquire both from the construction (@cite{rappaport-hovav-levin-1998}; @cite{levin-2026} §3). This is what enables the causative alternation for verbs like push that lack it in isolation.

Equations

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

def ConstructionGrammar.intransitiveMotion : ArgStructureConstruction

Intransitive motion construction: [Subj V Obl]. "X MOVES to Y" (e.g., "The ball rolled down the hill").

Equations

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

def ConstructionGrammar.conative : ArgStructureConstruction

Conative construction: [Subj V Obl_at]. "X DIRECTS ACTION at Y" (e.g., "Sam kicked at Bill"). The verb designates the intended result of the directed action; the at-PP marks the target without entailing contact (@cite{goldberg-1995} p. 3–4, 63–64).

Equations

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

Decomposition into combination schemata

def ConstructionGrammar.decompose (asc : ArgStructureConstruction) : List Core.CombinationKind

Decompose a fully abstract construction into a sequence of combination steps.

For a construction with slots [Subj, V, Obj1, Obj2]:

1. V + Obj2 → V' (Head-Complement)
2. V' + Obj1 → V'' (Head-Complement)
3. Subj + V'' → S (Head-Specifier)

The head slot determines which combinations are complements vs specifier.

Equations

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

def ConstructionGrammar.isFullyCompositional (c : Construction) : Bool

A construction is fully compositional if it has specificity fullyAbstract and no construction-specific pragmatic function.

This is a proxy for @cite{mueller-2013}'s structural criterion (whether the construction can be analyzed as a sequence of headed binary combinations). The proxy works because fully abstract constructions without pragmatic functions have no idiosyncratic form–meaning pairings that would resist decomposition into the three universal schemata.

Equations

• ConstructionGrammar.isFullyCompositional c = (c.specificity == ConstructionGrammar.Specificity.fullyAbstract && c.pragmaticFunction.isNone)

Core theorems

theorem ConstructionGrammar.ditransitive_decomposes : decompose ditransitive = [Core.CombinationKind.headSpecifier, Core.CombinationKind.headComplement, Core.CombinationKind.headComplement]

Ditransitive decomposes into Head-Specifier + Head-Complement + Head-Complement.

The ditransitive [Subj V Obj1 Obj2] decomposes as:

1. V + Obj2 → V' (Head-Complement)
2. V' + Obj1 → V'' (Head-Complement)
3. Subj + V'' → S (Head-Specifier)

theorem ConstructionGrammar.causedMotion_decomposes : decompose causedMotion = [Core.CombinationKind.headSpecifier, Core.CombinationKind.headComplement, Core.CombinationKind.headComplement]

Caused-motion decomposes into Head-Specifier + Head-Complement + Head-Complement.

theorem ConstructionGrammar.resultative_decomposes : decompose resultative = [Core.CombinationKind.headSpecifier, Core.CombinationKind.headComplement, Core.CombinationKind.headComplement]

Resultative decomposes into Head-Specifier + Head-Complement + Head-Complement.

theorem ConstructionGrammar.fullyAbstract_isFullyCompositional (c : Construction) (h₁ : c.specificity = Specificity.fullyAbstract) (h₂ : c.pragmaticFunction = none) : isFullyCompositional c = true

Fully abstract constructions without pragmatic functions are fully compositional.

theorem ConstructionGrammar.pal_irreducible : isFullyCompositional Studies.GoldbergShirtz2025.palConstruction = false

PAL construction is NOT fully compositional.

PAL is a phrasal construction where a phrase fills a word-level slot. This form-function pairing cannot be captured by the three schemata alone — it requires construction-specific knowledge.

theorem ConstructionGrammar.let_alone_irreducible : isFullyCompositional Studies.FillmoreKayOConnor1988.letAloneConstruction = false

Let alone construction is NOT fully compositional.

Let alone is a formal idiom with paired focus, scalar entailment, and NPI licensing requirements. These semantic/pragmatic properties cannot be derived from Head-Complement + Head-Specifier + Head-Filler.

theorem ConstructionGrammar.both_directions_right : (∀ (c : Construction), c.specificity = Specificity.fullyAbstract → c.pragmaticFunction = none → isFullyCompositional c = true) ∧ ∃ (c : Construction), isFullyCompositional c = false

Müller's "both directions right" (§3): the three schemata handle fully abstract constructions, but CxG's phrasal constructions are irreducible.

This formalizes the biconditional:

• Fully abstract → fully compositional (covered by universal schemata)
• There exist constructions that are not fully compositional (requires CxG)

theorem ConstructionGrammar.conative_decomposes : decompose conative = [Core.CombinationKind.headSpecifier, Core.CombinationKind.headComplement]

Conative decomposes into Head-Specifier + Head-Complement.

Polysemy families (@cite{goldberg-1995} §3.3.2, I_P links)

A polysemy family groups constructions that share one syntactic frame but differ in meaning. The shared form is enforced by construction — all senses are generated from the same slots, making it impossible for a polysemy extension to silently diverge in syntax.

structure ConstructionGrammar.PolysemyFamily : Type

A polysemy family: one argument frame, multiple meanings.

All constructions in a family share the same slots definitionally — there is no way to create an extension with different syntax. The polysemy links (I_P) are derived, not manually assembled.

• name : String

  Name of the construction family

• form : String

  Human-readable form description

• slots : List ConstructionSlot

  The shared argument frame

• hasHead : (self.slots.any fun (x : ConstructionSlot) => x.isHead) = true

  At least one slot is the head

• centralMeaning : String

  Central sense meaning

• extensions : List (String × String × List String)

  Extended senses: (extension name, meaning, overridden properties)

def ConstructionGrammar.PolysemyFamily.centralConstruction (f : PolysemyFamily) : ArgStructureConstruction

The central sense as an ArgStructureConstruction.

Equations

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

def ConstructionGrammar.PolysemyFamily.extensionConstruction (f : PolysemyFamily) (ext : String × String × List String) : ArgStructureConstruction

Build an extension construction. Uses the family's slots — shared by construction, not by assertion.

Equations

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

def ConstructionGrammar.PolysemyFamily.extensionConstructions (f : PolysemyFamily) : List ArgStructureConstruction

All extension constructions.

Equations

• f.extensionConstructions = List.map f.extensionConstruction f.extensions

def ConstructionGrammar.PolysemyFamily.allConstructions (f : PolysemyFamily) : List ArgStructureConstruction

All constructions (central + extensions).

Equations

• f.allConstructions = f.centralConstruction :: f.extensionConstructions

def ConstructionGrammar.PolysemyFamily.polysemyLinks (f : PolysemyFamily) : List InheritanceLink

Derive polysemy links from the family structure.

Equations

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

theorem ConstructionGrammar.PolysemyFamily.central_slots (f : PolysemyFamily) : f.centralConstruction.slots = f.slots

Central construction uses the family's slots (definitionally true).

theorem ConstructionGrammar.PolysemyFamily.extension_slots (f : PolysemyFamily) (ext : String × String × List String) : (f.extensionConstruction ext).slots = f.slots

Every extension uses the family's slots (definitionally true). This is the structural enforcement: shared syntax is impossible to violate because it follows from the definition, not from a proof.

theorem ConstructionGrammar.PolysemyFamily.all_same_decomposition (f : PolysemyFamily) (ext : String × String × List String) : decompose (f.extensionConstruction ext) = decompose f.centralConstruction

All members decompose identically (same slots → same decomposition).

Ditransitive polysemy network (@cite{goldberg-1995} pp. 75–77)

The ditransitive is not a single construction but a family of six related senses connected by polysemy links (I_P). Each sense inherits the ditransitive's syntactic form [Subj V Obj Obj₂] but differs in the semantic relation between the event participants.

def ConstructionGrammar.ditransitiveFamily : PolysemyFamily

The ditransitive polysemy family: six senses sharing one argument frame (@cite{goldberg-1995} pp. 75–77).

Equations

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

theorem ConstructionGrammar.ditransitiveFamily_matches : ditransitiveFamily.centralConstruction.slots = ditransitive.slots

The family's slots match the standalone ditransitive definition.

def ConstructionGrammar.ditransitivePolysemy : List InheritanceLink

Derived polysemy links.

Equations

• ConstructionGrammar.ditransitivePolysemy = ConstructionGrammar.ditransitiveFamily.polysemyLinks

def ConstructionGrammar.causedMotionSubpart : InheritanceLink

Subpart link (I_S) from caused-motion to intransitive motion (@cite{goldberg-1995} p. 78): the intransitive motion construction is a proper subpart of the caused-motion construction.

Equations

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

def ConstructionGrammar.causedMotionToResultative : InheritanceLink

Metaphorical extension link (I_M) from caused-motion to resultative (@cite{goldberg-1995} pp. 81–84): the resultative is a metaphorical extension of caused-motion via the systematic metaphor motion → change, location → state.

Equations

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

theorem ConstructionGrammar.polysemy_links_typed : (ditransitivePolysemy.all fun (x : InheritanceLink) => x.linkType == some LinkType.polysemy) = true

All polysemy links have link type I_P.

theorem ConstructionGrammar.subpart_link_typed : causedMotionSubpart.linkType = some LinkType.subpart

Subpart link has link type I_S.

theorem ConstructionGrammar.metaphorical_link_typed : causedMotionToResultative.linkType = some LinkType.metaphorical

Metaphorical link has link type I_M.

theorem ConstructionGrammar.all_link_types_instantiated : (ditransitivePolysemy.any fun (x : InheritanceLink) => x.linkType == some LinkType.polysemy) = true ∧ causedMotionToResultative.linkType = some LinkType.metaphorical ∧ causedMotionSubpart.linkType = some LinkType.subpart ∧ True

All four link types are instantiated across the network.

Verb–construction fusion

@cite{goldberg-1995}'s central claim: argument structure constructions are independent form–meaning pairings. When a verb appears in a construction, its meaning fuses with the construction's meaning. The composed meaning can have properties neither has alone.

At the level of @cite{levin-1993} meaning components, fusion is componentwise OR: if either the verb or the construction contributes a component, the composed meaning has it. This simple mechanism derives construction-dependent alternation behavior (@cite{levin-2026}):

• push alone: {−CoS, +contact, +motion, −causation} → no causative alternation
• push + resultative: {+CoS, +contact, +motion, +causation} → causative alternation predicted

The construction adds what the verb lacks; predictedAlternation on the fused result gives the correct prediction without any new alternation logic.

def ConstructionGrammar.composedMeaning (verbMC : MeaningComponents) (cxn : ArgStructureConstruction) : MeaningComponents

The composed meaning of a verb in an argument structure construction. Verb root semantics fused with the construction's semantic contribution.

Equations

• ConstructionGrammar.composedMeaning verbMC cxn = verbMC.fuse cxn.semanticContribution

def ConstructionGrammar.predictedAlternationInConstruction (verbMC : MeaningComponents) (cxn : ArgStructureConstruction) (alt : DiathesisAlternation) : Bool

Whether an alternation is predicted for a verb in a construction. Generalizes MeaningComponents.predictedAlternation to construction contexts.

Equations

• ConstructionGrammar.predictedAlternationInConstruction verbMC cxn alt = (ConstructionGrammar.composedMeaning verbMC cxn).predictedAlternation alt

Core theorems: constructions that don't augment

theorem ConstructionGrammar.ditransitive_no_augmentation : ditransitive.semanticContribution = MeaningComponents.none

Ditransitive contributes nothing beyond the verb (.none).

theorem ConstructionGrammar.no_augmentation_identity (mc : MeaningComponents) : composedMeaning mc ditransitive = mc

With no augmentation, the composed meaning equals the verb's own.

Core theorems: constructions that augment

theorem ConstructionGrammar.resultative_adds_cos_causation : resultative.semanticContribution.changeOfState = true ∧ resultative.semanticContribution.causation = true

The resultative adds CoS + causation.

theorem ConstructionGrammar.causedMotion_adds_motion_causation : causedMotion.semanticContribution.motion = true ∧ causedMotion.semanticContribution.causation = true

The caused-motion construction adds motion + causation.

Key derivation: construction-dependent alternation

The payoff: predictedAlternation on fused components derives that manner verbs participate in the causative alternation inside the resultative, even though they cannot outside it. No new alternation logic is needed — the existing component-based prediction (mc.changeOfState && mc.causation) fires on the fused result.

theorem ConstructionGrammar.manner_verb_no_alternation (mc : MeaningComponents) (hCoS : mc.changeOfState = false) (hCaus : mc.causation = false) : mc.predictedAlternation DiathesisAlternation.causativeInchoative = false

A pure manner verb (no CoS, no causation) cannot alternate alone.

theorem ConstructionGrammar.manner_verb_alternates_in_resultative (mc : MeaningComponents) (hInstr : mc.instrumentSpec = false) : predictedAlternationInConstruction mc resultative DiathesisAlternation.causativeInchoative = true

A pure manner verb in the resultative CAN alternate: the construction adds the CoS and causation the verb lacks.

theorem ConstructionGrammar.hit_alternates_in_resultative : predictedAlternationInConstruction MeaningComponents.hit resultative DiathesisAlternation.causativeInchoative = true

Concrete instance: hit-class components + resultative → causative alternation.

theorem ConstructionGrammar.hit_no_alternation_alone : MeaningComponents.hit.predictedAlternation DiathesisAlternation.causativeInchoative = false

Concrete instance: hit-class components alone → no causative alternation.

Multiple alternation flips from a single construction

The key architectural insight: fusing a construction's components with a verb's components can flip multiple alternation predictions simultaneously. The resultative adds CoS + causation, which unlocks not just causativeInchoative but also middle, instrumentSubject, and the resultative alternation itself — all from the same mechanism, with no new alternation logic.

This is the formal payoff of Goldbergian fusion (@cite{goldberg-1995}): constructions don't just license one new alternation — they systematically augment the verb's meaning component profile, and every alternation whose required components are now satisfied becomes available.

theorem ConstructionGrammar.hit_blocked_alone : MeaningComponents.hit.predictedAlternation DiathesisAlternation.middle = false ∧ MeaningComponents.hit.predictedAlternation DiathesisAlternation.instrumentSubject = false ∧ MeaningComponents.hit.predictedAlternation DiathesisAlternation.resultative = false

Hit-class verbs alone: no middle, no instrumentSubject, no resultative alternation.

theorem ConstructionGrammar.hit_resultative_full_profile : predictedAlternationInConstruction MeaningComponents.hit resultative DiathesisAlternation.causativeInchoative = true ∧ predictedAlternationInConstruction MeaningComponents.hit resultative DiathesisAlternation.middle = true ∧ predictedAlternationInConstruction MeaningComponents.hit resultative DiathesisAlternation.instrumentSubject = true ∧ predictedAlternationInConstruction MeaningComponents.hit resultative DiathesisAlternation.resultative = true

Hit-class in resultative: ALL FOUR component-derived alternations flip. The resultative adds CoS + causation → fused = ⟨true, true, true, true, false, false⟩. This unlocks causativeInchoative, middle, instrumentSubject, AND resultative.

theorem ConstructionGrammar.hit_resultative_conative_preserved : MeaningComponents.hit.predictedAlternation DiathesisAlternation.conative = true ∧ predictedAlternationInConstruction MeaningComponents.hit resultative DiathesisAlternation.conative = true

Conative stays true: hit already has contact + motion, and fusing preserves them.

Caused-motion fusion

The caused-motion construction adds motion + causation. For touch-class verbs (pure contact, no motion), this unlocks the conative alternation (requires contact + motion) and the instrument subject alternation (requires causation).

Touch alone: ⟨false, true, false, false, false, false⟩ — only BPPA (contact) Touch + caused-motion: ⟨false, true, true, true, false, false⟩ — conative + instrumentSubject too

theorem ConstructionGrammar.touch_blocked_alone : MeaningComponents.touch.predictedAlternation DiathesisAlternation.conative = false ∧ MeaningComponents.touch.predictedAlternation DiathesisAlternation.instrumentSubject = false

Touch verbs alone: no conative, no instrumentSubject.

theorem ConstructionGrammar.touch_causedMotion_flips : predictedAlternationInConstruction MeaningComponents.touch causedMotion DiathesisAlternation.conative = true ∧ predictedAlternationInConstruction MeaningComponents.touch causedMotion DiathesisAlternation.instrumentSubject = true

Touch + caused-motion: conative AND instrumentSubject flip to true. Motion + causation from the construction fill exactly what touch lacks.

theorem ConstructionGrammar.touch_causedMotion_bppa_preserved : MeaningComponents.touch.predictedAlternation DiathesisAlternation.bodyPartPossessorAscension = true ∧ predictedAlternationInConstruction MeaningComponents.touch causedMotion DiathesisAlternation.bodyPartPossessorAscension = true

Touch + caused-motion: BPPA stays true (contact preserved by fusion).

Manner-of-motion verbs in the resultative

Manner-of-motion verbs (⟨false, false, true, false, false, true⟩) have motion but no CoS or causation. In the resultative, they acquire both — unlocking causativeInchoative, middle, instrumentSubject, and resultative.

theorem ConstructionGrammar.mannerOfMotion_blocked_alone : LevinClass.mannerOfMotion.meaningComponents.predictedAlternation DiathesisAlternation.causativeInchoative = false ∧ LevinClass.mannerOfMotion.meaningComponents.predictedAlternation DiathesisAlternation.middle = false ∧ LevinClass.mannerOfMotion.meaningComponents.predictedAlternation DiathesisAlternation.instrumentSubject = false

Manner-of-motion verbs alone: no CI, no middle, no instrumentSubject.

theorem ConstructionGrammar.mannerOfMotion_resultative_flips : predictedAlternationInConstruction LevinClass.mannerOfMotion.meaningComponents resultative DiathesisAlternation.causativeInchoative = true ∧ predictedAlternationInConstruction LevinClass.mannerOfMotion.meaningComponents resultative DiathesisAlternation.middle = true ∧ predictedAlternationInConstruction LevinClass.mannerOfMotion.meaningComponents resultative DiathesisAlternation.instrumentSubject = true

Manner-of-motion + resultative: CI, middle, and instrumentSubject all flip.

Constructional augmentation summary

Each construction unlocks a characteristic set of alternations by augmenting the verb's meaning components. The table below summarizes what each construction contributes and which alternations it enables for verbs that lack the relevant components:

Construction	Adds	Unlocks
Resultative	CoS + causation	CI, middle, instrumentSubject, resultative
Caused-motion	motion + causation	conative (if +contact), instrumentSubject
Ditransitive	(nothing)	(nothing)

These predictions are all derived from the same predictedAlternation function — no construction-specific alternation logic exists. The construction simply changes the input to the general prediction function.

theorem ConstructionGrammar.hit_ditransitive_no_change : predictedAlternationInConstruction MeaningComponents.hit ditransitive DiathesisAlternation.causativeInchoative = false ∧ predictedAlternationInConstruction MeaningComponents.hit ditransitive DiathesisAlternation.middle = false ∧ predictedAlternationInConstruction MeaningComponents.hit ditransitive DiathesisAlternation.instrumentSubject = false

Ditransitive adds nothing: hit verbs stay blocked in all alternations that are blocked in isolation.

theorem ConstructionGrammar.cut_blocked_even_in_resultative : predictedAlternationInConstruction MeaningComponents.cut resultative DiathesisAlternation.causativeInchoative = false ∧ predictedAlternationInConstruction MeaningComponents.cut resultative DiathesisAlternation.resultative = false

Instrument specification survives fusion: cut-class verbs remain blocked from causativeInchoative and resultative even inside the resultative construction, because instrumentSpec = true persists through componentwise OR.