Argument structure in Construction Grammar

[Gol95]'s account of argument structure: clausal argument realization is not projected from verb entries alone but contributed by independent form–meaning pairings — argument structure constructions — whose meaning pole records the components they add beyond the verb. A verb appearing in a construction fuses its components with the construction's, deriving alternation behavior the verb lacks in isolation, and the constructions themselves form a network of polysemy and inheritance links.

Main definitions

• ditransitive, causedMotion, resultative, intransitiveMotion, conative: [Gol95]'s constructions
• isFullyCompositional: analyzable by the universal combination schemata alone
• PolysemyFamily, goldberg1995Network: one argument frame with many senses, and the ch. 2–3 network
• composedMeaning, predictedAlternationInConstruction: verb–construction fusion

Concrete argument structure constructions

An argument structure construction is a Construction MeaningComponents: its typed form is the argument frame, and its meaning pole records which meaning components ([Lev93]) the construction adds independently of the verb ([Gol95]) — .none for constructions that do not augment.

def ConstructionGrammar.ditransitive : Construction ArgumentStructure.MeaningComponents

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 : Construction ArgumentStructure.MeaningComponents

Caused-motion construction: [Subj V Obj Obl]. "X CAUSES Y to MOVE Z", Z a directional ("Pat sneezed the napkin off the table", p. 3). Contributes motion + causation: verbs that lexicalize neither (like sneeze) acquire both from the construction ([Gol95] p. 152–179).

Equations

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

def ConstructionGrammar.resultative : Construction ArgumentStructure.MeaningComponents

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 — [RHL98]'s Template Augmentation, cast lexically there (their appendix maps it onto the constructional approach); [Lev26] §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 : Construction ArgumentStructure.MeaningComponents

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 : Construction ArgumentStructure.MeaningComponents

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 ([Gol95] p. 3–4, 63–64).

Equations

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

Full compositionality

def ConstructionGrammar.isFullyCompositional {Sem : Type u_1} (c : Construction Sem) : Bool

Whether a construction is analyzable by universal combination schemata alone: fully abstract form and no pragmatic point — a Boolean proxy for [Mul13]'s structural criterion, approximating what [KM19] survey as a continuum.

Equations

• ConstructionGrammar.isFullyCompositional c = (c.specificity == ConstructionGrammar.Specificity.fullyAbstract && !c.pragmaticPoint)

Core theorems

theorem ConstructionGrammar.fullyAbstract_isFullyCompositional {Sem : Type u_1} (c : Construction Sem) (h₁ : c.specificity = Specificity.fullyAbstract) (h₂ : c.pragmaticPoint = false) : isFullyCompositional c = true

Fully abstract constructions without pragmatic point are fully compositional.

Polysemy families ([Gol95] §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 form, making it impossible for a polysemy extension to silently diverge in syntax.

structure ConstructionGrammar.PolysemyFamily (Sem : Type u_1) : Type u_1

A polysemy family: one argument frame, multiple meanings.

All constructions in a family share the same form 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 : TypedForm String

  The shared argument frame

• centralMeaning : Sem

  Central sense meaning

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

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

def ConstructionGrammar.PolysemyFamily.centralConstruction {Sem : Type u_1} (f : PolysemyFamily Sem) : Construction Sem

The central sense as a construction.

Equations

• f.centralConstruction = { name := f.name, form := f.form, meaning := f.centralMeaning }

def ConstructionGrammar.PolysemyFamily.extensionConstruction {Sem : Type u_1} (f : PolysemyFamily Sem) (ext : String × Sem × List String) : Construction Sem

An extension construction, sharing the family's form definitionally rather than by assertion.

Equations

• f.extensionConstruction ext = { name := f.name ++ "-" ++ ext.1, form := f.form, meaning := ext.2.1 }

def ConstructionGrammar.PolysemyFamily.extensionConstructions {Sem : Type u_1} (f : PolysemyFamily Sem) : List (Construction Sem)

All extension constructions.

Equations

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

def ConstructionGrammar.PolysemyFamily.allConstructions {Sem : Type u_1} (f : PolysemyFamily Sem) : List (Construction Sem)

All constructions (central + extensions).

Equations

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

def ConstructionGrammar.PolysemyFamily.polysemyLinks {Sem : Type u_1} (f : PolysemyFamily Sem) : List InheritanceLink

The polysemy links a family determines, one per extension.

Equations

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

theorem ConstructionGrammar.PolysemyFamily.central_form {Sem : Type u_1} (f : PolysemyFamily Sem) : f.centralConstruction.form = f.form

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

theorem ConstructionGrammar.PolysemyFamily.extension_form {Sem : Type u_1} (f : PolysemyFamily Sem) (ext : String × Sem × List String) : (f.extensionConstruction ext).form = f.form

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

Ditransitive polysemy network ([Gol95] 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.

inductive ConstructionGrammar.TransferModality : Type

The modality of the CAUSE-RECEIVE relation distinguishing the ditransitive's senses ([Gol95] pp. 75–77).

• actual : TransferModality

  Actual transfer: X CAUSES Y TO RECEIVE Z.

• satisfaction : TransferModality

  Conditions of satisfaction imply X CAUSES Y TO RECEIVE Z.

• enablement : TransferModality

  X ENABLES Y TO RECEIVE Z.

• negated : TransferModality

  X CAUSES Y NOT TO RECEIVE Z.

• intended : TransferModality

  X INTENDS TO CAUSE Y TO RECEIVE Z.

• future : TransferModality

  X ACTS TO CAUSE Y TO RECEIVE Z at some future point in time.

@[instance_reducible]

instance ConstructionGrammar.instDecidableEqTransferModality : DecidableEq TransferModality

Equations

• ConstructionGrammar.instDecidableEqTransferModality x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def ConstructionGrammar.instReprTransferModality.repr : TransferModality → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance ConstructionGrammar.instReprTransferModality : Repr TransferModality

Equations

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

def ConstructionGrammar.ditransitiveFamily : PolysemyFamily TransferModality

The ditransitive polysemy family: six senses sharing one argument frame ([Gol95] pp. 75–77; verb classes per Figure 2.2, p. 38). The extension labels are the formalizer's — Goldberg numbers the senses and calls the Intended extension "the benefactive construction" (Figure 3.2). Her warrant for the shared frame is exactly what PolysemyFamily enforces definitionally: "The syntactic specifications of the central sense are inherited by the extensions" (p. 75).

Equations

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

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 ([Gol95] p. 78, link annotated "I_S: cause"): the intransitive motion construction is a proper subpart of the caused-motion construction. The cause role is absent in the subpart, not overridden — I_S relates a proper subpart, so the override slot stays empty.

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 ([Gol95] 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.

The book's network as a constructicon

[Gol95] draws no single master figure; the network below assembles the per-link analyses under the book's own framing of "the entire collection of constructions as forming a lattice, with individual constructions related by specific types of asymmetric normal mode inheritance links" (§3.7, p. 99): the ditransitive polysemy family (pp. 75–77), the caused-motion → intransitive-motion subpart link (p. 78), and the caused-motion → resultative metaphorical link (§3.4.1, the "Change of State as Change of Location" metaphor, p. 99). The conative appears in the book's construction inventory (p. 4) but participates in no inheritance link — it is a node without edges, and linking it would be invention.

def ConstructionGrammar.goldberg1995Network : Constructicon Unit

The ch. 2–3 constructional network, with meaning poles erased: the network theorems concern the links and forms only, and the family's TransferModality meanings and the argument-structure constructions' MeaningComponents meanings live in different types.

Equations

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

theorem ConstructionGrammar.goldberg1995Network_wellFormed : goldberg1995Network.WellFormed

Every link of the network resolves to a member construction.

theorem ConstructionGrammar.resultative_parent : goldberg1995Network.parentsOf "Resultative" = [Construction.map (fun (x : ArgumentStructure.MeaningComponents) => ()) causedMotion]

The links, not hand-listed parents, determine the resultative's mother: the caused-motion construction, via the metaphorical link.

theorem ConstructionGrammar.PolysemyFamily.polysemyLinks_typed {Sem : Type u_1} (f : PolysemyFamily Sem) (l : InheritanceLink) : l ∈ f.polysemyLinks → l.linkType = some LinkType.polysemy

Every link a polysemy family derives is an I_P link — a fact about the construction, not about one table.

Verb–construction fusion

A verb appearing in a construction fuses its meaning components with the construction's — componentwise, so the composed meaning can have properties neither has alone ([Gol95]; [Lev26]): push lacks change of state and causation, but push in the resultative acquires both, and the causative alternation is predicted.

def ConstructionGrammar.composedMeaning (verbMC : ArgumentStructure.MeaningComponents) (cxn : Construction ArgumentStructure.MeaningComponents) : ArgumentStructure.MeaningComponents

The composed meaning of a verb in an argument structure construction: the verb's meaning components fused with the construction's meaning pole.

Equations

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

def ConstructionGrammar.predictedAlternationInConstruction (verbMC : ArgumentStructure.MeaningComponents) (cxn : Construction ArgumentStructure.MeaningComponents) (alt : ArgumentStructure.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.meaning = ArgumentStructure.MeaningComponents.none

Ditransitive contributes nothing beyond the verb (.none).

theorem ConstructionGrammar.no_augmentation_identity (mc : ArgumentStructure.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.meaning.changeOfState = true ∧ resultative.meaning.causation = true

The resultative adds CoS + causation.

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

The caused-motion construction adds motion + causation.

Construction-dependent alternation

Manner verbs participate in the causative alternation inside the resultative but not outside it: the component-based prediction fires on the fused result, with no alternation logic specific to constructions.

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

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

theorem ConstructionGrammar.manner_verb_alternates_in_resultative (mc : ArgumentStructure.MeaningComponents) (hInstr : mc.instrumentSpec = false) : predictedAlternationInConstruction mc resultative ArgumentStructure.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 ArgumentStructure.MeaningComponents.hit resultative ArgumentStructure.DiathesisAlternation.causativeInchoative = true

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

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

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

Multiple alternation flips from a single construction

Fusion can flip several alternation predictions at once: every alternation whose required components the augmented profile satisfies becomes available ([Gol95]).

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

Hit-class verbs alone permit neither the middle, the instrument-subject, nor the resultative alternation.

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

Hit-class verbs in the resultative permit all four component-derived alternations: the construction's change of state and causation complete the profile.

theorem ConstructionGrammar.hit_resultative_conative_preserved : ArgumentStructure.MeaningComponents.hit.predictedAlternation ArgumentStructure.DiathesisAlternation.conative = true ∧ predictedAlternationInConstruction ArgumentStructure.MeaningComponents.hit resultative ArgumentStructure.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 : ArgumentStructure.MeaningComponents.touch.predictedAlternation ArgumentStructure.DiathesisAlternation.conative = false ∧ ArgumentStructure.MeaningComponents.touch.predictedAlternation ArgumentStructure.DiathesisAlternation.instrumentSubject = false

Touch verbs alone: no conative, no instrumentSubject.

theorem ConstructionGrammar.touch_causedMotion_flips : predictedAlternationInConstruction ArgumentStructure.MeaningComponents.touch causedMotion ArgumentStructure.DiathesisAlternation.conative = true ∧ predictedAlternationInConstruction ArgumentStructure.MeaningComponents.touch causedMotion ArgumentStructure.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 : ArgumentStructure.MeaningComponents.touch.predictedAlternation ArgumentStructure.DiathesisAlternation.bodyPartPossessorAscension = true ∧ predictedAlternationInConstruction ArgumentStructure.MeaningComponents.touch causedMotion ArgumentStructure.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 : ArgumentStructure.LevinClass.mannerOfMotion.meaningComponents.predictedAlternation ArgumentStructure.DiathesisAlternation.causativeInchoative = false ∧ ArgumentStructure.LevinClass.mannerOfMotion.meaningComponents.predictedAlternation ArgumentStructure.DiathesisAlternation.middle = false ∧ ArgumentStructure.LevinClass.mannerOfMotion.meaningComponents.predictedAlternation ArgumentStructure.DiathesisAlternation.instrumentSubject = false

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

theorem ConstructionGrammar.mannerOfMotion_resultative_flips : predictedAlternationInConstruction ArgumentStructure.LevinClass.mannerOfMotion.meaningComponents resultative ArgumentStructure.DiathesisAlternation.causativeInchoative = true ∧ predictedAlternationInConstruction ArgumentStructure.LevinClass.mannerOfMotion.meaningComponents resultative ArgumentStructure.DiathesisAlternation.middle = true ∧ predictedAlternationInConstruction ArgumentStructure.LevinClass.mannerOfMotion.meaningComponents resultative ArgumentStructure.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 ArgumentStructure.MeaningComponents.hit ditransitive ArgumentStructure.DiathesisAlternation.causativeInchoative = false ∧ predictedAlternationInConstruction ArgumentStructure.MeaningComponents.hit ditransitive ArgumentStructure.DiathesisAlternation.middle = false ∧ predictedAlternationInConstruction ArgumentStructure.MeaningComponents.hit ditransitive ArgumentStructure.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 ArgumentStructure.MeaningComponents.cut resultative ArgumentStructure.DiathesisAlternation.causativeInchoative = false ∧ predictedAlternationInConstruction ArgumentStructure.MeaningComponents.cut resultative ArgumentStructure.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.