ConstructionGrammar.Resultatives — Theory of the resultative construction family

@cite{goldberg-jackendoff-2004}

Theory-side primitives for the four-way resultative construction family (causative/noncausative × property/path RP), the dual subevent structure, typed verbal/constructional subevent relations, and the compositional fusion machinery linking verb meaning to constructional contribution.

Paper data and per-datum verifications for @cite{goldberg-jackendoff-2004} itself live in Phenomena/Constructions/Resultatives/Studies/GoldbergJackendoff2004.lean, which imports this file.

Core types

• SubeventKind, SubeventRelation, RPType, Boundedness, ObjectSelection, TemporalOrder
• ResultativeSubconstruction — the 2×2 family
• SubeventDesc, DualSubevent — event-structural features
• ResultativeEntry — schema for any resultative datum
• ArgSource — argument-fusion bookkeeping

Key derivations (no per-paper data)

• ResultativeSubconstruction.constructionalDesc — derived hasCause/hasBecome
• resultativeAspect, resultativeVendlerClass — bounded RP → telic
• adjScaleToRPBoundedness — Kennedy 2007 scale → G&J boundedness
• ResultativeSubconstruction.toConstruction — derived family of ArgStructureConstruction instances + inheritanceLink
• farSatisfied, rolesCoherent, temporalConstraintSatisfied — the three substantive constraints (Principles 37, 44, §4.2)

The fusion theorems (alternation_chain, noncausative_partial_chain, instrumentSpec_blocks_across_subconstructions, etc.) are universally quantified over arbitrary MeaningComponents and ResultativeSubconstruction.

Core types

inductive ConstructionGrammar.Resultatives.SubeventKind : Type

The kind of subevent in a resultative.

• verbal : SubeventKind

  From the verb's lexical meaning (e.g., hammering, kicking)

• constructional : SubeventKind

  From the construction (CAUSE + BECOME/GO)

@[implicit_reducible]

instance ConstructionGrammar.Resultatives.instReprSubeventKind : Repr SubeventKind

Equations

• ConstructionGrammar.Resultatives.instReprSubeventKind = { reprPrec := ConstructionGrammar.Resultatives.instReprSubeventKind.repr }

def ConstructionGrammar.Resultatives.instReprSubeventKind.repr : SubeventKind → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance ConstructionGrammar.Resultatives.instDecidableEqSubeventKind : DecidableEq SubeventKind

Equations

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

inductive ConstructionGrammar.Resultatives.SubeventRelation : Type

How the verbal and constructional subevents are related (§3 of @cite{goldberg-jackendoff-2004}).

• means: The verbal subevent is the means by which the constructional subevent is brought about. This is the default relation for all four core subconstructions (97a–d). E.g., "hammer metal flat" — hammering is the means of causing flatness. Also holds for noncausative cases: "the river froze solid" — freezing is the means of becoming solid; "the ball rolled into the field" — rolling is the means of motion along the path.
• result: The verbal subevent is a result of the constructional subevent (reversed directionality from means). Reserved for sound-emission resultatives (ex. 20: "The trolley rumbled through the tunnel" — rumbling results from motion) and disappearance resultatives (ex. 21: "The witch vanished into the forest" — vanishing results from motion).
• instance_: The verbal subevent is an instance of the constructional subevent. For the follow-type cases (§7.1, ex. 55: "Bill followed the thief into the library" — following IS going-after) and ride/drive-type cases (ex. 56: "Bill rode a train to New York" — riding IS going-by-way-of).
• coOccurrence: The two subevents merely co-occur without causal connection. The way construction ("She sang her way down the road") uses this relation. Some speakers accept CO-OCCURRENCE for sound-emission resultatives as well.

• means : SubeventRelation
• result : SubeventRelation
• instance_ : SubeventRelation
• coOccurrence : SubeventRelation

@[implicit_reducible]

instance ConstructionGrammar.Resultatives.instReprSubeventRelation : Repr SubeventRelation

Equations

• ConstructionGrammar.Resultatives.instReprSubeventRelation = { reprPrec := ConstructionGrammar.Resultatives.instReprSubeventRelation.repr }

def ConstructionGrammar.Resultatives.instReprSubeventRelation.repr : SubeventRelation → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance ConstructionGrammar.Resultatives.instDecidableEqSubeventRelation : DecidableEq SubeventRelation

Equations

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

inductive ConstructionGrammar.Resultatives.RPType : Type

Type of result phrase.

• property : RPType

  Adjectival/property result: "flat", "clean", "solid"

• path : RPType

  Directional/path result: "into the field", "off the table"

@[implicit_reducible]

instance ConstructionGrammar.Resultatives.instReprRPType : Repr RPType

Equations

• ConstructionGrammar.Resultatives.instReprRPType = { reprPrec := ConstructionGrammar.Resultatives.instReprRPType.repr }

def ConstructionGrammar.Resultatives.instReprRPType.repr : RPType → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance ConstructionGrammar.Resultatives.instDecidableEqRPType : DecidableEq RPType

Equations

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

inductive ConstructionGrammar.Resultatives.ResultativeSubconstruction : Type

The four subconstructions in the resultative family (@cite{goldberg-jackendoff-2004} §2, Table 1).

	Property RP	Path RP
Causative	causativeProperty	causativePath
Noncausative	noncausativeProperty	noncausativePath

• causativeProperty : ResultativeSubconstruction
• causativePath : ResultativeSubconstruction
• noncausativeProperty : ResultativeSubconstruction
• noncausativePath : ResultativeSubconstruction

@[implicit_reducible]

instance ConstructionGrammar.Resultatives.instReprResultativeSubconstruction : Repr ResultativeSubconstruction

Equations

• ConstructionGrammar.Resultatives.instReprResultativeSubconstruction = { reprPrec := ConstructionGrammar.Resultatives.instReprResultativeSubconstruction.repr }

def ConstructionGrammar.Resultatives.instReprResultativeSubconstruction.repr : ResultativeSubconstruction → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance ConstructionGrammar.Resultatives.instDecidableEqResultativeSubconstruction : DecidableEq ResultativeSubconstruction

Equations

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

def ConstructionGrammar.Resultatives.ResultativeSubconstruction.isCausative : ResultativeSubconstruction → Bool

Whether a subconstruction is causative.

Equations

• ConstructionGrammar.Resultatives.ResultativeSubconstruction.causativeProperty.isCausative = true
• ConstructionGrammar.Resultatives.ResultativeSubconstruction.causativePath.isCausative = true
• ConstructionGrammar.Resultatives.ResultativeSubconstruction.noncausativeProperty.isCausative = false
• ConstructionGrammar.Resultatives.ResultativeSubconstruction.noncausativePath.isCausative = false

def ConstructionGrammar.Resultatives.ResultativeSubconstruction.isPropertyRP : ResultativeSubconstruction → Bool

Whether a subconstruction has a property (vs path) RP.

Equations

• ConstructionGrammar.Resultatives.ResultativeSubconstruction.causativeProperty.isPropertyRP = true
• ConstructionGrammar.Resultatives.ResultativeSubconstruction.causativePath.isPropertyRP = false
• ConstructionGrammar.Resultatives.ResultativeSubconstruction.noncausativeProperty.isPropertyRP = true
• ConstructionGrammar.Resultatives.ResultativeSubconstruction.noncausativePath.isPropertyRP = false

def ConstructionGrammar.Resultatives.ResultativeSubconstruction.rpType : ResultativeSubconstruction → RPType

Get the RP type of a subconstruction.

Equations

• ConstructionGrammar.Resultatives.ResultativeSubconstruction.causativeProperty.rpType = ConstructionGrammar.Resultatives.RPType.property
• ConstructionGrammar.Resultatives.ResultativeSubconstruction.causativePath.rpType = ConstructionGrammar.Resultatives.RPType.path
• ConstructionGrammar.Resultatives.ResultativeSubconstruction.noncausativeProperty.rpType = ConstructionGrammar.Resultatives.RPType.property
• ConstructionGrammar.Resultatives.ResultativeSubconstruction.noncausativePath.rpType = ConstructionGrammar.Resultatives.RPType.path

Dual subevent structure (§3 of @cite{goldberg-jackendoff-2004})

structure ConstructionGrammar.Resultatives.SubeventDesc : Type

Description of a subevent via event-structural features.

The two booleans encode the presence of CAUSE and BECOME/GO operators in the subevent's event template (cf. Template in EventStructure.lean). Verbal subevents are typically ⟨false, false⟩ (bare manner/activity); constructional subevents are ⟨true, true⟩ (causative) or ⟨false, true⟩ (noncausative change-of-state/motion).

• hasCause : Bool

  Whether CAUSE is part of this subevent

• hasBecome : Bool

  Whether BECOME/GO is part of this subevent

@[implicit_reducible]

instance ConstructionGrammar.Resultatives.instReprSubeventDesc : Repr SubeventDesc

Equations

• ConstructionGrammar.Resultatives.instReprSubeventDesc = { reprPrec := ConstructionGrammar.Resultatives.instReprSubeventDesc.repr }

def ConstructionGrammar.Resultatives.instReprSubeventDesc.repr : SubeventDesc → ℕ → Std.Format

Equations

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

def ConstructionGrammar.Resultatives.instBEqSubeventDesc.beq : SubeventDesc → SubeventDesc → Bool

Equations

• ConstructionGrammar.Resultatives.instBEqSubeventDesc.beq { hasCause := a, hasBecome := a_1 } { hasCause := b, hasBecome := b_1 } = (a == b && a_1 == b_1)
• ConstructionGrammar.Resultatives.instBEqSubeventDesc.beq x✝¹ x✝ = false

@[implicit_reducible]

instance ConstructionGrammar.Resultatives.instBEqSubeventDesc : BEq SubeventDesc

Equations

• ConstructionGrammar.Resultatives.instBEqSubeventDesc = { beq := ConstructionGrammar.Resultatives.instBEqSubeventDesc.beq }

@[implicit_reducible]

instance ConstructionGrammar.Resultatives.instDecidableEqSubeventDesc : DecidableEq SubeventDesc

Equations

• ConstructionGrammar.Resultatives.instDecidableEqSubeventDesc = ConstructionGrammar.Resultatives.instDecidableEqSubeventDesc.decEq

def ConstructionGrammar.Resultatives.instDecidableEqSubeventDesc.decEq (x✝ x✝¹ : SubeventDesc) : Decidable (x✝ = x✝¹)

Equations

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

structure ConstructionGrammar.Resultatives.DualSubevent : Type

The dual subevent structure of a resultative (@cite{goldberg-jackendoff-2004} §3, Principle 25).

• verbal : SubeventDesc

  The verbal subevent (from the verb's lexical semantics)

• constructional : SubeventDesc

  The constructional subevent (from the construction)

• relation : SubeventRelation

  How the subevents are related

def ConstructionGrammar.Resultatives.instReprDualSubevent.repr : DualSubevent → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance ConstructionGrammar.Resultatives.instReprDualSubevent : Repr DualSubevent

Equations

• ConstructionGrammar.Resultatives.instReprDualSubevent = { reprPrec := ConstructionGrammar.Resultatives.instReprDualSubevent.repr }

@[implicit_reducible]

instance ConstructionGrammar.Resultatives.instBEqDualSubevent : BEq DualSubevent

Equations

• ConstructionGrammar.Resultatives.instBEqDualSubevent = { beq := ConstructionGrammar.Resultatives.instBEqDualSubevent.beq }

def ConstructionGrammar.Resultatives.instBEqDualSubevent.beq : DualSubevent → DualSubevent → Bool

Equations

• One or more equations did not get rendered due to their size.
• ConstructionGrammar.Resultatives.instBEqDualSubevent.beq x✝¹ x✝ = false

Derived constructional subevent

The constructional subevent's event-structural features are fully determined by the subconstruction type: causative subconstructions have CAUSE + BECOME; noncausative subconstructions have BECOME only. Verbal subevents are always bare (no CAUSE, no BECOME) — the manner comes from the verb's lexical semantics, not from event-structural operators.

def ConstructionGrammar.Resultatives.ResultativeSubconstruction.constructionalDesc : ResultativeSubconstruction → SubeventDesc

Derive the constructional subevent description from the subconstruction. This replaces per-entry stipulation: causative ↔ hasCause, all have hasBecome.

Equations

• ConstructionGrammar.Resultatives.ResultativeSubconstruction.causativeProperty.constructionalDesc = { hasCause := true, hasBecome := true }
• ConstructionGrammar.Resultatives.ResultativeSubconstruction.causativePath.constructionalDesc = { hasCause := true, hasBecome := true }
• ConstructionGrammar.Resultatives.ResultativeSubconstruction.noncausativeProperty.constructionalDesc = { hasBecome := true }
• ConstructionGrammar.Resultatives.ResultativeSubconstruction.noncausativePath.constructionalDesc = { hasBecome := true }

def ConstructionGrammar.Resultatives.verbalSubeventDesc : SubeventDesc

The verbal subevent is always a bare manner/activity (no CAUSE, no BECOME).

Equations

• ConstructionGrammar.Resultatives.verbalSubeventDesc = { }

theorem ConstructionGrammar.Resultatives.causative_constructional_has_cause (sc : ResultativeSubconstruction) (h : sc.isCausative = true) : sc.constructionalDesc.hasCause = true

Causative subconstructions have CAUSE in their constructional subevent.

theorem ConstructionGrammar.Resultatives.noncausative_constructional_no_cause (sc : ResultativeSubconstruction) (h : sc.isCausative = false) : sc.constructionalDesc.hasCause = false

Noncausative subconstructions lack CAUSE.

theorem ConstructionGrammar.Resultatives.all_constructional_have_become_derived (sc : ResultativeSubconstruction) : sc.constructionalDesc.hasBecome = true

All subconstructions have BECOME in the constructional subevent.

Bridge to event structure templates

@cite{goldberg-jackendoff-2004}'s constructional subevent maps to Rappaport Hovav & Levin's event structure templates: causative → accomplishment template, noncausative → achievement template. The hasCause/hasBecome features of SubeventDesc are exactly Template.HasCause/Template.HasResultState.

def ConstructionGrammar.Resultatives.ResultativeSubconstruction.constructionalTemplate : ResultativeSubconstruction → Features.EventStructure.Template

Map subconstruction to the constructional subevent's event template.

Equations

• ConstructionGrammar.Resultatives.ResultativeSubconstruction.causativeProperty.constructionalTemplate = Features.EventStructure.Template.accomplishment
• ConstructionGrammar.Resultatives.ResultativeSubconstruction.causativePath.constructionalTemplate = Features.EventStructure.Template.accomplishment
• ConstructionGrammar.Resultatives.ResultativeSubconstruction.noncausativeProperty.constructionalTemplate = Features.EventStructure.Template.achievement
• ConstructionGrammar.Resultatives.ResultativeSubconstruction.noncausativePath.constructionalTemplate = Features.EventStructure.Template.achievement

theorem ConstructionGrammar.Resultatives.constructional_cause_matches_template (sc : ResultativeSubconstruction) : sc.constructionalDesc.hasCause = decide sc.constructionalTemplate.HasCause

The derived hasCause agrees with Template.HasCause.

theorem ConstructionGrammar.Resultatives.constructional_become_matches_template (sc : ResultativeSubconstruction) : sc.constructionalDesc.hasBecome = decide sc.constructionalTemplate.HasResultState

The derived hasBecome agrees with Template.HasResultState.

Boundedness and aspect

inductive ConstructionGrammar.Resultatives.Boundedness : Type

Whether an RP denotes a bounded endpoint.

Property RPs are typically bounded (reaching an endstate), but comparative/gradual APs ("hotter and hotter", "ever flatter") create unbounded property RPs (§4.1). Path RPs are bounded iff the goal is specific ("into the field" = bounded; "along the road" = unbounded).

• bounded : Boundedness
• unbounded : Boundedness

def ConstructionGrammar.Resultatives.instReprBoundedness.repr : Boundedness → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance ConstructionGrammar.Resultatives.instReprBoundedness : Repr Boundedness

Equations

• ConstructionGrammar.Resultatives.instReprBoundedness = { reprPrec := ConstructionGrammar.Resultatives.instReprBoundedness.repr }

@[implicit_reducible]

instance ConstructionGrammar.Resultatives.instDecidableEqBoundedness : DecidableEq Boundedness

Equations

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

Object selection (§2 of @cite{goldberg-jackendoff-2004}, ex. 7–9)

Within transitive resultatives, the object may be independently selected by the verb (selected) or licensed only by the construction (unselected). A special case of unselected: fake reflexives, where the object is a reflexive pronoun that cannot alternate with other NPs.

inductive ConstructionGrammar.Resultatives.ObjectSelection : Type

How the postverbal NP is selected (§2).

• selected : ObjectSelection

  Verb independently selects the object: "She watered the plants flat"

• unselected : ObjectSelection

  Construction licenses the object (verb doesn't take it independently): "They drank the pub dry" (cf. *They drank the pub)

• fakeReflexive : ObjectSelection

  Special unselected: reflexive object that cannot alternate with other NPs: "She laughed herself silly" (cf. *She laughed him silly)

def ConstructionGrammar.Resultatives.instReprObjectSelection.repr : ObjectSelection → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance ConstructionGrammar.Resultatives.instReprObjectSelection : Repr ObjectSelection

Equations

• ConstructionGrammar.Resultatives.instReprObjectSelection = { reprPrec := ConstructionGrammar.Resultatives.instReprObjectSelection.repr }

@[implicit_reducible]

instance ConstructionGrammar.Resultatives.instDecidableEqObjectSelection : DecidableEq ObjectSelection

Equations

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

def ConstructionGrammar.Resultatives.instBEqObjectSelection.beq : ObjectSelection → ObjectSelection → Bool

Equations

• ConstructionGrammar.Resultatives.instBEqObjectSelection.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[implicit_reducible]

instance ConstructionGrammar.Resultatives.instBEqObjectSelection : BEq ObjectSelection

Equations

• ConstructionGrammar.Resultatives.instBEqObjectSelection = { beq := ConstructionGrammar.Resultatives.instBEqObjectSelection.beq }

def ConstructionGrammar.Resultatives.ResultativeSubconstruction.defaultObjectSelection : ResultativeSubconstruction → Option ObjectSelection

Intransitive resultatives have no object selection.

Equations

• ConstructionGrammar.Resultatives.ResultativeSubconstruction.causativeProperty.defaultObjectSelection = some ConstructionGrammar.Resultatives.ObjectSelection.selected
• ConstructionGrammar.Resultatives.ResultativeSubconstruction.causativePath.defaultObjectSelection = some ConstructionGrammar.Resultatives.ObjectSelection.selected
• ConstructionGrammar.Resultatives.ResultativeSubconstruction.noncausativeProperty.defaultObjectSelection = none
• ConstructionGrammar.Resultatives.ResultativeSubconstruction.noncausativePath.defaultObjectSelection = none

Resultative entry

structure ConstructionGrammar.Resultatives.ResultativeEntry : Type

A resultative entry: verb + subconstruction + aspect.

The dual subevent structure is derived from the subconstruction:

• verbal desc: always verbalSubeventDesc (bare manner/activity)
• constructional desc: subconstruction.constructionalDesc The subevent relation defaults to MEANS for all four core subconstructions; RESULT is used only for sound-emission and disappearance subtypes.

The Levin class enables compositional fusion: verbMC.fuse cxn.semanticContribution derives predictions about alternation participation.

• verb : String

  The verb form

• subconstruction : ResultativeSubconstruction

  Which subconstruction

• subeventRelation : SubeventRelation

  How the subevents are related (default: MEANS for core subconstructions)

• rpBoundedness : Boundedness

  Boundedness of the result phrase

• bareVerbClass : Features.VendlerClass

  Vendler class of the bare verb (without resultative)

• objectSelection : Option ObjectSelection

  How the postverbal NP is selected (transitive only)

• levinClass : Semantics.Lexical.LevinClass

  Levin class of the verb, for MeaningComponents derivation

def ConstructionGrammar.Resultatives.instReprResultativeEntry.repr : ResultativeEntry → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance ConstructionGrammar.Resultatives.instReprResultativeEntry : Repr ResultativeEntry

Equations

• ConstructionGrammar.Resultatives.instReprResultativeEntry = { reprPrec := ConstructionGrammar.Resultatives.instReprResultativeEntry.repr }

@[implicit_reducible]

instance ConstructionGrammar.Resultatives.instBEqResultativeEntry : BEq ResultativeEntry

Equations

• ConstructionGrammar.Resultatives.instBEqResultativeEntry = { beq := ConstructionGrammar.Resultatives.instBEqResultativeEntry.beq }

def ConstructionGrammar.Resultatives.instBEqResultativeEntry.beq : ResultativeEntry → ResultativeEntry → Bool

Equations

• One or more equations did not get rendered due to their size.
• ConstructionGrammar.Resultatives.instBEqResultativeEntry.beq x✝¹ x✝ = false

def ConstructionGrammar.Resultatives.ResultativeEntry.dualSubevent (e : ResultativeEntry) : DualSubevent

Derive the full dual subevent structure from the entry.

Equations

• e.dualSubevent = { verbal := ConstructionGrammar.Resultatives.verbalSubeventDesc, constructional := e.subconstruction.constructionalDesc, relation := e.subeventRelation }

def ConstructionGrammar.Resultatives.ResultativeEntry.verbMC (e : ResultativeEntry) : Semantics.Lexical.MeaningComponents

The verb's inherent meaning components, from its Levin class.

Equations

• e.verbMC = e.levinClass.meaningComponents

Aspectual profile (§4 of @cite{goldberg-jackendoff-2004}, Principle 27)

The resultative's aspect is derived compositionally:

• Always dynamic (involves change)
• Always durative (extends over time)
• Telic iff the RP denotes a bounded path/property

def ConstructionGrammar.Resultatives.resultativeAspect (b : Boundedness) : Features.AspectualProfile

Derive the aspectual profile of a resultative from RP boundedness.

Equations

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

def ConstructionGrammar.Resultatives.resultativeVendlerClass (b : Boundedness) : Features.VendlerClass

Derive the Vendler class of a resultative.

Equations

• ConstructionGrammar.Resultatives.resultativeVendlerClass b = (ConstructionGrammar.Resultatives.resultativeAspect b).toVendlerClass

Semantic roles and argument licensing

Uses the canonical ThetaRole from the linking interface rather than a paper-specific enum. @cite{goldberg-jackendoff-2004}'s four resultative-relevant roles map to: agent, patient, theme, goal (= "resultGoal" in their terminology).

structure ConstructionGrammar.Resultatives.ArgSource : Type

An argument with its source (verb or construction).

• role : ThetaRole

  The semantic role

• fromVerb : Bool

  Whether this argument comes from the verb

• fromConstruction : Bool

  Whether this argument comes from the construction

def ConstructionGrammar.Resultatives.instReprArgSource.repr : ArgSource → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance ConstructionGrammar.Resultatives.instReprArgSource : Repr ArgSource

Equations

• ConstructionGrammar.Resultatives.instReprArgSource = { reprPrec := ConstructionGrammar.Resultatives.instReprArgSource.repr }

@[implicit_reducible]

instance ConstructionGrammar.Resultatives.instBEqArgSource : BEq ArgSource

Equations

• ConstructionGrammar.Resultatives.instBEqArgSource = { beq := ConstructionGrammar.Resultatives.instBEqArgSource.beq }

def ConstructionGrammar.Resultatives.instBEqArgSource.beq : ArgSource → ArgSource → Bool

Equations

• One or more equations did not get rendered due to their size.
• ConstructionGrammar.Resultatives.instBEqArgSource.beq x✝¹ x✝ = false

def ConstructionGrammar.Resultatives.ArgSource.isFused (a : ArgSource) : Bool

Whether an argument is fused (shared between verb and construction).

Equations

• a.isFused = (a.fromVerb && a.fromConstruction)

Full Argument Realization (FAR) — Principle 37, §6.1

All obligatory arguments of both the verb and the construction must be syntactically realized. Arguments shared between verb and construction fuse into a single syntactic position.

def ConstructionGrammar.Resultatives.farSatisfied (args : List ArgSource) : Bool

Check FAR: every role's source is accounted for.

Equations

• ConstructionGrammar.Resultatives.farSatisfied args = args.all fun (a : ConstructionGrammar.Resultatives.ArgSource) => a.fromVerb || a.fromConstruction

Semantic Coherence Principle — Principle 44, §6.2

A verb role rV and a construction role rC may fuse only if rV is construable as an instance of rC.

def ConstructionGrammar.Resultatives.rolesCoherent (rV rC : ThetaRole) : Bool

Which role pairs are coherent for fusion (Principle 44).

Agent can fuse with agent; patient with patient or theme; theme with patient or theme; goal with goal. All other combinations (experiencer, instrument, stimulus, source) are incoherent in the resultative construction.

Equations

• ConstructionGrammar.Resultatives.rolesCoherent ThetaRole.agent ThetaRole.agent = true
• ConstructionGrammar.Resultatives.rolesCoherent ThetaRole.patient ThetaRole.patient = true
• ConstructionGrammar.Resultatives.rolesCoherent ThetaRole.patient ThetaRole.theme = true
• ConstructionGrammar.Resultatives.rolesCoherent ThetaRole.theme ThetaRole.patient = true
• ConstructionGrammar.Resultatives.rolesCoherent ThetaRole.theme ThetaRole.theme = true
• ConstructionGrammar.Resultatives.rolesCoherent ThetaRole.goal ThetaRole.goal = true
• ConstructionGrammar.Resultatives.rolesCoherent rV rC = false

def ConstructionGrammar.Resultatives.semanticCoherenceSatisfied (args : List (ThetaRole × ThetaRole)) : Bool

Check semantic coherence: all fused arguments have coherent roles.

Equations

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

Temporal constraint (§4.2)

Temporal ordering between subevents is constrained by the subevent relation:

• MEANS: The verbal subevent must temporally overlap with or precede the constructional subevent. Constructional-first is ruled out because you cannot achieve a result before performing the means to it.
• RESULT: The constructional subevent CAN precede the verbal subevent. E.g., "The door banged open" — the opening (constructional) precedes the banging (verbal result of the motion).
• INSTANCE/CO-OCCURRENCE: Simultaneity expected (the verbal IS the constructional, or they merely co-occur).

inductive ConstructionGrammar.Resultatives.TemporalOrder : Type

Temporal ordering between subevents.

• verbalFirst : TemporalOrder
• simultaneous : TemporalOrder
• constructionalFirst : TemporalOrder

def ConstructionGrammar.Resultatives.instReprTemporalOrder.repr : TemporalOrder → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance ConstructionGrammar.Resultatives.instReprTemporalOrder : Repr TemporalOrder

Equations

• ConstructionGrammar.Resultatives.instReprTemporalOrder = { reprPrec := ConstructionGrammar.Resultatives.instReprTemporalOrder.repr }

@[implicit_reducible]

instance ConstructionGrammar.Resultatives.instDecidableEqTemporalOrder : DecidableEq TemporalOrder

Equations

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

def ConstructionGrammar.Resultatives.temporalConstraintSatisfied (rel : SubeventRelation) (order : TemporalOrder) : Bool

Check the temporal constraint given the subevent relation.

For MEANS, the constructional subevent cannot precede the verbal subevent. For RESULT, all orderings are acceptable (reversed directionality). For INSTANCE/CO-OCCURRENCE, simultaneity is expected but not enforced.

Equations

• ConstructionGrammar.Resultatives.temporalConstraintSatisfied ConstructionGrammar.Resultatives.SubeventRelation.means ConstructionGrammar.Resultatives.TemporalOrder.constructionalFirst = false
• ConstructionGrammar.Resultatives.temporalConstraintSatisfied rel order = true

Closed-scale → bounded RP bridge (§8 of @cite{goldberg-jackendoff-2004},

Principle 27)

@cite{goldberg-jackendoff-2004} §8: productive property RPs "tend to be nongradable" and "encode a clearly delimited state." The formal correlate (@cite{kennedy-2007}): productive RPs have a maximum endpoint on their scale. dry (upper-bounded, has max) is productive; wet (lower-bounded, no max) is not. flat, clean, shut, dead, open, full, empty are all closed-scale (has max).

The aspectual chain: hasMax → bounded RP → telic resultative.

def ConstructionGrammar.Resultatives.adjScaleToRPBoundedness (b : Core.Scale.Boundedness) : Boundedness

Map @cite{kennedy-2007}'s scale boundedness to @cite{goldberg-jackendoff-2004}'s RP boundedness. Scales with a maximum endpoint yield bounded RPs (the RP denotes a delimited endstate). Scales without a maximum yield unbounded RPs.

Equations

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

theorem ConstructionGrammar.Resultatives.closed_scale_bounded : adjScaleToRPBoundedness Core.Scale.Boundedness.closed = Boundedness.bounded

Closed scales yield bounded RPs.

theorem ConstructionGrammar.Resultatives.upper_bounded_scale_bounded : adjScaleToRPBoundedness Core.Scale.Boundedness.upperBounded = Boundedness.bounded

Upper-bounded scales yield bounded RPs (e.g., "dry").

theorem ConstructionGrammar.Resultatives.open_scale_unbounded : adjScaleToRPBoundedness Core.Scale.Boundedness.open_ = Boundedness.unbounded

Open scales yield unbounded RPs (e.g., "tall").

theorem ConstructionGrammar.Resultatives.lower_bounded_scale_unbounded : adjScaleToRPBoundedness Core.Scale.Boundedness.lowerBounded = Boundedness.unbounded

Lower-bounded scales yield unbounded RPs (e.g., "wet").

theorem ConstructionGrammar.Resultatives.closed_scale_telic_resultative (b : Core.Scale.Boundedness) (hMax : b.hasMax = true) : resultativeVendlerClass (adjScaleToRPBoundedness b) = Features.VendlerClass.accomplishment

The full aspectual chain: a closed-scale adjective as RP yields a telic resultative. hasMax → bounded → telic → accomplishment.

theorem ConstructionGrammar.Resultatives.dry_wet_contrast : adjScaleToRPBoundedness Core.Scale.Boundedness.upperBounded = Boundedness.bounded ∧ adjScaleToRPBoundedness Core.Scale.Boundedness.lowerBounded = Boundedness.unbounded

The dry/wet contrast: dry is productive (bounded → telic), wet is not (unbounded → atelic). Derives from scale structure alone.

Semantic contribution (meaning components)

Each subconstruction's semantic contribution is derived from the causativity dimension: causative subconstructions contribute CoS + causation (matching the parent resultative in ArgumentStructure.lean); noncausative ones contribute only CoS (BECOME without CAUSE). This is consistent with the constructionalDesc: hasCause ↔ causation, hasBecome ↔ changeOfState.

def ConstructionGrammar.Resultatives.ResultativeSubconstruction.semanticContribution : ResultativeSubconstruction → Semantics.Lexical.MeaningComponents

Derive the meaning components contributed by a subconstruction. Causative: CoS + causation (same as parent resultative). Noncausative: CoS only (BECOME without CAUSE).

Equations

• ConstructionGrammar.Resultatives.ResultativeSubconstruction.causativeProperty.semanticContribution = { changeOfState := true, contact := false, motion := false, causation := true }
• ConstructionGrammar.Resultatives.ResultativeSubconstruction.causativePath.semanticContribution = { changeOfState := true, contact := false, motion := false, causation := true }
• ConstructionGrammar.Resultatives.ResultativeSubconstruction.noncausativeProperty.semanticContribution = { changeOfState := true, contact := false, motion := false, causation := false }
• ConstructionGrammar.Resultatives.ResultativeSubconstruction.noncausativePath.semanticContribution = { changeOfState := true, contact := false, motion := false, causation := false }

theorem ConstructionGrammar.Resultatives.all_subconstructions_contribute_cos (sc : ResultativeSubconstruction) : sc.semanticContribution.changeOfState = true

All subconstructions contribute change-of-state (all have BECOME).

theorem ConstructionGrammar.Resultatives.causative_contributes_causation (sc : ResultativeSubconstruction) (h : sc.isCausative = true) : sc.semanticContribution.causation = true

Causative subconstructions contribute causation.

theorem ConstructionGrammar.Resultatives.noncausative_no_causation (sc : ResultativeSubconstruction) (h : sc.isCausative = false) : sc.semanticContribution.causation = false

Noncausative subconstructions do not contribute causation.

theorem ConstructionGrammar.Resultatives.semanticContribution_matches_constructionalDesc (sc : ResultativeSubconstruction) : sc.semanticContribution.causation = sc.constructionalDesc.hasCause ∧ sc.semanticContribution.changeOfState = sc.constructionalDesc.hasBecome

The semantic contribution is consistent with the constructional subevent: hasCause ↔ causation and hasBecome ↔ changeOfState.

theorem ConstructionGrammar.Resultatives.no_subconstruction_instrumentSpec (sc : ResultativeSubconstruction) : sc.semanticContribution.instrumentSpec = false

No subconstruction contributes instrument specificity.

theorem ConstructionGrammar.Resultatives.causative_sc_contribution (sc : ResultativeSubconstruction) (h : sc.isCausative = true) : sc.semanticContribution.changeOfState = true ∧ sc.semanticContribution.causation = true ∧ sc.semanticContribution.instrumentSpec = false

Bundled: causative subconstruction contributes CoS + causation + ¬instrumentSpec. Satisfies the hypotheses of fuse_cos_caus_enables.

theorem ConstructionGrammar.Resultatives.noncausative_sc_contribution (sc : ResultativeSubconstruction) (h : sc.isCausative = false) : sc.semanticContribution.changeOfState = true ∧ sc.semanticContribution.causation = false ∧ sc.semanticContribution.instrumentSpec = false

Bundled: noncausative subconstruction contributes CoS + ¬causation + ¬instrumentSpec. Satisfies the hypotheses of fuse_cos_only_partial.

theorem ConstructionGrammar.Resultatives.causative_semantics_match_parent (sc : ResultativeSubconstruction) (h : sc.isCausative = true) : sc.semanticContribution = resultative.semanticContribution

Causative subconstructions match the parent resultative's semantic contribution.

Derived construction network

The four subconstructions are derived from ResultativeSubconstruction rather than hard-coded. Each subconstruction inherits from the existing resultative parent in ArgumentStructure.lean.

The slot structure follows from two dimensions:

• Causative adds an agent subject + patient/theme object (4 slots)
• Noncausative has only a theme subject (3 slots)
• Property RP uses ADJ; Path RP uses ADP

def ConstructionGrammar.Resultatives.RPType.toUPOS : RPType → UD.UPOS

The UPOS category of the result phrase slot.

Equations

• ConstructionGrammar.Resultatives.RPType.property.toUPOS = UD.UPOS.ADJ
• ConstructionGrammar.Resultatives.RPType.path.toUPOS = UD.UPOS.ADP

def ConstructionGrammar.Resultatives.RPType.roleLabel : RPType → String

The role label for the result phrase slot.

Equations

• ConstructionGrammar.Resultatives.RPType.property.roleLabel = "result"
• ConstructionGrammar.Resultatives.RPType.path.roleLabel = "goal"

def ConstructionGrammar.Resultatives.ResultativeSubconstruction.nameSuffix : ResultativeSubconstruction → String

The name suffix for a subconstruction.

Equations

• ConstructionGrammar.Resultatives.ResultativeSubconstruction.causativeProperty.nameSuffix = "CausativeProperty"
• ConstructionGrammar.Resultatives.ResultativeSubconstruction.causativePath.nameSuffix = "CausativePath"
• ConstructionGrammar.Resultatives.ResultativeSubconstruction.noncausativeProperty.nameSuffix = "NoncausativeProperty"
• ConstructionGrammar.Resultatives.ResultativeSubconstruction.noncausativePath.nameSuffix = "NoncausativePath"

def ConstructionGrammar.Resultatives.ResultativeSubconstruction.toConstruction (sc : ResultativeSubconstruction) : ArgStructureConstruction

Derive the ArgStructureConstruction from a subconstruction.

Slots are determined by the two dimensions:

• Causative: [NOUN subj, VERB head, NOUN obj, RP-UPOS rp]
• Noncausative: [NOUN subj, VERB head, RP-UPOS rp]

Equations

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

def ConstructionGrammar.Resultatives.ResultativeEntry.fusedMC (e : ResultativeEntry) : Semantics.Lexical.MeaningComponents

The composed meaning: verb MC fused with the subconstruction's contribution.

Equations

• e.fusedMC = ConstructionGrammar.composedMeaning e.verbMC e.subconstruction.toConstruction

def ConstructionGrammar.Resultatives.causativePropertyConstruction : ArgStructureConstruction

Convenience aliases for downstream compatibility.

Equations

• ConstructionGrammar.Resultatives.causativePropertyConstruction = ConstructionGrammar.Resultatives.ResultativeSubconstruction.causativeProperty.toConstruction

def ConstructionGrammar.Resultatives.causativePathConstruction : ArgStructureConstruction

Equations

• ConstructionGrammar.Resultatives.causativePathConstruction = ConstructionGrammar.Resultatives.ResultativeSubconstruction.causativePath.toConstruction

def ConstructionGrammar.Resultatives.noncausativePropertyConstruction : ArgStructureConstruction

Equations

• ConstructionGrammar.Resultatives.noncausativePropertyConstruction = ConstructionGrammar.Resultatives.ResultativeSubconstruction.noncausativeProperty.toConstruction

def ConstructionGrammar.Resultatives.noncausativePathConstruction : ArgStructureConstruction

Equations

• ConstructionGrammar.Resultatives.noncausativePathConstruction = ConstructionGrammar.Resultatives.ResultativeSubconstruction.noncausativePath.toConstruction

def ConstructionGrammar.Resultatives.resultativeFamily : List ArgStructureConstruction

The full resultative family, derived from all four subconstructions.

Equations

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

def ConstructionGrammar.Resultatives.ResultativeSubconstruction.inheritanceLink (sc : ResultativeSubconstruction) : InheritanceLink

Derive an inheritance link from a subconstruction to the parent.

Equations

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

def ConstructionGrammar.Resultatives.resultativeInheritance : List InheritanceLink

All four inheritance links, derived.

Equations

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

theorem ConstructionGrammar.Resultatives.all_inherit_from_resultative : (resultativeInheritance.all fun (x : InheritanceLink) => x.parent == "Resultative") = true

All inheritance links point to the same parent.

theorem ConstructionGrammar.Resultatives.all_subconstructions_abstract : (resultativeFamily.all fun (c : ArgStructureConstruction) => c.construction.specificity == Specificity.fullyAbstract) = true

All four subconstructions are fully abstract (decomposable).

theorem ConstructionGrammar.Resultatives.causative_are_transitive : causativePropertyConstruction.slots.length = 4 ∧ causativePathConstruction.slots.length = 4

Causative subconstructions are transitive (4 slots); noncausative are intransitive (3 slots).

theorem ConstructionGrammar.Resultatives.noncausative_are_intransitive : noncausativePropertyConstruction.slots.length = 3 ∧ noncausativePathConstruction.slots.length = 3

theorem ConstructionGrammar.Resultatives.causative_match_parent : decompose causativePropertyConstruction = decompose resultative ∧ decompose causativePathConstruction = decompose resultative

Causative subconstructions decompose like the parent resultative.

theorem ConstructionGrammar.Resultatives.noncausative_fewer_steps : (decompose noncausativePropertyConstruction).length < (decompose causativePropertyConstruction).length

Noncausative subconstructions have one fewer decomposition step.

Verb–construction fusion (integration with ArgumentStructure.lean)

theorem ConstructionGrammar.Resultatives.manner_verb_alternates_in_causative_sub (mc : Semantics.Lexical.MeaningComponents) (hInstr : mc.instrumentSpec = false) (sc : ResultativeSubconstruction) (hCaus : sc.isCausative = true) : predictedAlternationInConstruction mc sc.toConstruction Semantics.Lexical.DiathesisAlternation.causativeInchoative = true

A manner verb (no CoS, no causation, no instrumentSpec) in a causative subconstruction acquires causative alternation: the subconstruction's semantic contribution adds CoS + causation via fuse.

theorem ConstructionGrammar.Resultatives.manner_verb_no_alternation_in_noncausative (mc : Semantics.Lexical.MeaningComponents) (hCoS : mc.changeOfState = false) (hCaus : mc.causation = false) (sc : ResultativeSubconstruction) (hNonCaus : sc.isCausative = false) : predictedAlternationInConstruction mc sc.toConstruction Semantics.Lexical.DiathesisAlternation.causativeInchoative = false

A manner verb in a noncausative subconstruction does NOT acquire the causative alternation: noncausative subconstructions lack causation.

theorem ConstructionGrammar.Resultatives.hit_alternates_in_causativeProperty : predictedAlternationInConstruction Semantics.Lexical.MeaningComponents.hit causativePropertyConstruction Semantics.Lexical.DiathesisAlternation.causativeInchoative = true

Concrete: hit-class verb in causativeProperty → causative alternation.

theorem ConstructionGrammar.Resultatives.hit_no_alternation_in_noncausativeProperty : predictedAlternationInConstruction Semantics.Lexical.MeaningComponents.hit noncausativePropertyConstruction Semantics.Lexical.DiathesisAlternation.causativeInchoative = false

Concrete: hit-class verb in noncausativeProperty → no alternation.

theorem ConstructionGrammar.Resultatives.causative_sub_fuse_matches_parent (mc : Semantics.Lexical.MeaningComponents) (sc : ResultativeSubconstruction) (h : sc.isCausative = true) : composedMeaning mc sc.toConstruction = composedMeaning mc resultative

The composed meaning in a causative subconstruction matches the composed meaning in the parent resultative construction.

theorem ConstructionGrammar.Resultatives.fused_always_has_cos (mc : Semantics.Lexical.MeaningComponents) (sc : ResultativeSubconstruction) : (composedMeaning mc sc.toConstruction).changeOfState = true

All subconstructions contribute CoS via toConstruction, so the composed meaning always has changeOfState = true regardless of the verb.

theorem ConstructionGrammar.Resultatives.resultative_alternation_predicted (mc : Semantics.Lexical.MeaningComponents) (hInstr : mc.instrumentSpec = false) (sc : ResultativeSubconstruction) : predictedAlternationInConstruction mc sc.toConstruction Semantics.Lexical.DiathesisAlternation.resultative = true

The resultative alternation itself is predicted for any non-instrument verb in any subconstruction (since all contribute CoS).

Universal aspect predictions

theorem ConstructionGrammar.Resultatives.bounded_rp_telic : resultativeVendlerClass Boundedness.bounded = Features.VendlerClass.accomplishment

Bounded RP yields telic resultative (= accomplishment).

theorem ConstructionGrammar.Resultatives.unbounded_rp_atelic : resultativeVendlerClass Boundedness.unbounded = Features.VendlerClass.activity

Unbounded RP yields atelic resultative (= activity).

theorem ConstructionGrammar.Resultatives.resultative_telicizes_activity : Features.activityProfile.telicize.toVendlerClass = Features.VendlerClass.accomplishment

Resultative telicizes an activity verb: adding bounded RP to an activity yields an accomplishment (§4 of @cite{goldberg-jackendoff-2004}, Principle 27).

theorem ConstructionGrammar.Resultatives.resultative_aspect_matches_telicize (e : ResultativeEntry) (hVerb : e.bareVerbClass = Features.VendlerClass.activity) (hBounded : e.rpBoundedness = Boundedness.bounded) : resultativeVendlerClass e.rpBoundedness = e.bareVerbClass.toProfile.telicize.toVendlerClass

The resultative's derived aspect matches telicization of the bare verb when the bare verb is an activity and the RP is bounded.

General chain theorems

The full derivation pipeline connecting adjective scale structure, RP boundedness, aspect, and alternation participation. These are universally quantified — they hold for ANY verb class and ANY subconstruction satisfying the hypotheses, not just the attested entries.

theorem ConstructionGrammar.Resultatives.aspect_chain (b : Core.Scale.Boundedness) (hMax : b.hasMax = true) : have rpB := adjScaleToRPBoundedness b; rpB = Boundedness.bounded ∧ resultativeVendlerClass rpB = Features.VendlerClass.accomplishment ∧ (resultativeVendlerClass rpB).telicity = Features.Telicity.telic

Aspect chain: any adjective with a scale maximum, used as an RP in a resultative, produces a telic accomplishment.

theorem ConstructionGrammar.Resultatives.alternation_chain (mc : Semantics.Lexical.MeaningComponents) (sc : ResultativeSubconstruction) (hInstr : mc.instrumentSpec = false) (hCausative : sc.isCausative = true) : have fused := composedMeaning mc sc.toConstruction; fused.predictedAlternation Semantics.Lexical.DiathesisAlternation.causativeInchoative = true ∧ fused.predictedAlternation Semantics.Lexical.DiathesisAlternation.middle = true ∧ fused.predictedAlternation Semantics.Lexical.DiathesisAlternation.instrumentSubject = true ∧ fused.predictedAlternation Semantics.Lexical.DiathesisAlternation.resultative = true

Alternation chain: corollary of fuse_cos_caus_enables for causative resultative subconstructions.

theorem ConstructionGrammar.Resultatives.noncausative_partial_chain (mc : Semantics.Lexical.MeaningComponents) (sc : ResultativeSubconstruction) (hInstr : mc.instrumentSpec = false) (hNonCaus : sc.isCausative = false) (hNoCaus : mc.causation = false) : have fused := composedMeaning mc sc.toConstruction; fused.predictedAlternation Semantics.Lexical.DiathesisAlternation.middle = true ∧ fused.predictedAlternation Semantics.Lexical.DiathesisAlternation.resultative = true ∧ fused.predictedAlternation Semantics.Lexical.DiathesisAlternation.causativeInchoative = false ∧ fused.predictedAlternation Semantics.Lexical.DiathesisAlternation.instrumentSubject = false

Noncausative contrast: corollary of fuse_cos_only_partial.

theorem ConstructionGrammar.Resultatives.instrumentSpec_blocks_across_subconstructions (mc : Semantics.Lexical.MeaningComponents) (sc : ResultativeSubconstruction) (hInstr : mc.instrumentSpec = true) : have fused := composedMeaning mc sc.toConstruction; fused.predictedAlternation Semantics.Lexical.DiathesisAlternation.causativeInchoative = false ∧ fused.predictedAlternation Semantics.Lexical.DiathesisAlternation.instrumentSubject = false ∧ fused.predictedAlternation Semantics.Lexical.DiathesisAlternation.resultative = false

instrumentSpec blocking: corollary of instrumentSpec_blocks_after_fuse.