[GJ04]: The English Resultative as a Family of Constructions

The English resultative is a family of four subconstructions — causative/noncausative × property/path RP, summarized as (97) — each pairing a verbal with a constructional subevent under a typed relation, constrained by Full Argument Realization (37), Semantic Coherence (44), telicity from RP boundedness (§4.1), and the temporal relation of the subevents (§4.2). The theory-side machinery lives in ConstructionGrammar.Resultatives; this file runs it on the paper's entries and projects the generated example rows (Data.Examples.GoldbergJackendoff2004) into typed data.

Main declarations

• GoldbergJackendoff2004.allEntries: the paper's resultative entries, with derived CAUSE/BECOME, telicity, and alternation predictions
• GoldbergJackendoff2004.ResultativeDatum, allExamples: the judgment rows, classified by subconstruction
• GoldbergJackendoff2004.aspectualContrasts: §4.1's for-adverbial contrasts (exx. 23–24)

Empirical data: resultative entries

def GoldbergJackendoff2004.hammerFlat : ConstructionGrammar.Resultatives.ResultativeEntry

Equations

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

def GoldbergJackendoff2004.pushOffSofa : ConstructionGrammar.Resultatives.ResultativeEntry

Equations

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

def GoldbergJackendoff2004.freezeSolid : ConstructionGrammar.Resultatives.ResultativeEntry

Equations

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

def GoldbergJackendoff2004.rollDownHill : ConstructionGrammar.Resultatives.ResultativeEntry

Equations

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

def GoldbergJackendoff2004.drinkDry : ConstructionGrammar.Resultatives.ResultativeEntry

Equations

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

def GoldbergJackendoff2004.yellHoarse : ConstructionGrammar.Resultatives.ResultativeEntry

Equations

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

def GoldbergJackendoff2004.bleedToDeath : ConstructionGrammar.Resultatives.ResultativeEntry

Equations

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

def GoldbergJackendoff2004.wipeClean : ConstructionGrammar.Resultatives.ResultativeEntry

Equations

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

def GoldbergJackendoff2004.allEntries : List ConstructionGrammar.Resultatives.ResultativeEntry

All resultative entries.

Equations

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

Derived predictions

Each theorem runs the theory's machinery (dualSubevent, fusedMC, resultativeAspect) on the entries' independent classifications and checks the derived profile against the paper's claim. Encoding invariants of the data itself are anonymous examples.

theorem GoldbergJackendoff2004.causative_entries_have_cause : ((List.filter (fun (x : ConstructionGrammar.Resultatives.ResultativeEntry) => x.subconstruction.isCausative) allEntries).all fun (x : ConstructionGrammar.Resultatives.ResultativeEntry) => x.dualSubevent.constructional.hasCause) = true

Causative entries have CAUSE in their derived constructional subevent.

theorem GoldbergJackendoff2004.noncausative_entries_no_cause : ((List.filter (fun (e : ConstructionGrammar.Resultatives.ResultativeEntry) => !e.subconstruction.isCausative) allEntries).all fun (e : ConstructionGrammar.Resultatives.ResultativeEntry) => !e.dualSubevent.constructional.hasCause) = true

Noncausative entries lack CAUSE in their derived constructional subevent.

theorem GoldbergJackendoff2004.all_constructional_have_become : (allEntries.all fun (x : ConstructionGrammar.Resultatives.ResultativeEntry) => x.dualSubevent.constructional.hasBecome) = true

All derived constructional subevents have BECOME.

theorem GoldbergJackendoff2004.bounded_entries_telic : ((List.filter (fun (x : ConstructionGrammar.Resultatives.ResultativeEntry) => x.rpBoundedness == ConstructionGrammar.Resultatives.Boundedness.bounded) allEntries).all fun (e : ConstructionGrammar.Resultatives.ResultativeEntry) => (ConstructionGrammar.Resultatives.resultativeAspect e.rpBoundedness).telicity == Features.Telicity.telic) = true

All entries with bounded RP are telic.

theorem GoldbergJackendoff2004.activity_entries_become_accomplishments : ((List.filter (fun (e : ConstructionGrammar.Resultatives.ResultativeEntry) => e.bareVerbClass == Features.VendlerClass.activity && e.rpBoundedness == ConstructionGrammar.Resultatives.Boundedness.bounded) allEntries).all fun (e : ConstructionGrammar.Resultatives.ResultativeEntry) => ConstructionGrammar.Resultatives.resultativeVendlerClass e.rpBoundedness == Features.VendlerClass.accomplishment) = true

Activity verbs in the data with bounded RPs become accomplishments.

Per-entry verb class participation

The construction-verb interaction across the Levin classes of the paper's example verbs: contact/force verbs (hammer, push), change-of-state verbs (freeze), motion verbs (roll), speech and emission verbs (yell, bleed), and surface-contact verbs (wipe).

theorem GoldbergJackendoff2004.all_entries_fused_cos : (allEntries.all fun (e : ConstructionGrammar.Resultatives.ResultativeEntry) => e.fusedMC.changeOfState) = true

All entries acquire CoS from the construction, regardless of verb class.

theorem GoldbergJackendoff2004.all_entries_resultative_alternation : (allEntries.all fun (e : ConstructionGrammar.Resultatives.ResultativeEntry) => ConstructionGrammar.predictedAlternationInConstruction e.verbMC e.subconstruction.toConstruction ArgumentStructure.DiathesisAlternation.resultative) = true

All entries participate in the resultative alternation (none are instrument-spec).

theorem GoldbergJackendoff2004.causative_entries_causative_alternation : ((List.filter (fun (x : ConstructionGrammar.Resultatives.ResultativeEntry) => x.subconstruction.isCausative) allEntries).all fun (e : ConstructionGrammar.Resultatives.ResultativeEntry) => ConstructionGrammar.predictedAlternationInConstruction e.verbMC e.subconstruction.toConstruction ArgumentStructure.DiathesisAlternation.causativeInchoative) = true

Causative entries all acquire the causative alternation.

theorem GoldbergJackendoff2004.noncausative_entries_no_new_causation : ((List.filter (fun (e : ConstructionGrammar.Resultatives.ResultativeEntry) => !e.subconstruction.isCausative) allEntries).all fun (e : ConstructionGrammar.Resultatives.ResultativeEntry) => decide (ConstructionGrammar.predictedAlternationInConstruction e.verbMC e.subconstruction.toConstruction ArgumentStructure.DiathesisAlternation.causativeInchoative = e.verbMC.predictedAlternation ArgumentStructure.DiathesisAlternation.causativeInchoative)) = true

Noncausative entries do NOT acquire the causative alternation (unless the verb already has causation — freeze/otherCoS does).

theorem GoldbergJackendoff2004.hammer_gains_cos_causation : hammerFlat.verbMC.changeOfState = false ∧ hammerFlat.verbMC.causation = false ∧ hammerFlat.fusedMC.changeOfState = true ∧ hammerFlat.fusedMC.causation = true

Hammer (hit-class): no CoS or causation alone → both added by causative construction.

theorem GoldbergJackendoff2004.freeze_already_has_cos : freezeSolid.verbMC.changeOfState = true ∧ freezeSolid.verbMC.causation = true ∧ freezeSolid.fusedMC = freezeSolid.verbMC

Freeze (otherCoS): already has CoS + causation → construction doesn't change profile.

theorem GoldbergJackendoff2004.roll_gains_cos_only : rollDownHill.verbMC.changeOfState = false ∧ rollDownHill.fusedMC.changeOfState = true ∧ rollDownHill.fusedMC.causation = false

Roll (manner-of-motion): gains CoS from construction; no causation (noncausative).

theorem GoldbergJackendoff2004.yell_gains_cos_causation : yellHoarse.verbMC.changeOfState = false ∧ yellHoarse.verbMC.causation = false ∧ yellHoarse.fusedMC.changeOfState = true ∧ yellHoarse.fusedMC.causation = true

Yell (manner of speaking): pure manner verb — construction adds CoS + causation.

theorem GoldbergJackendoff2004.wipe_already_has_everything : wipeClean.verbMC.changeOfState = true ∧ wipeClean.verbMC.causation = true ∧ wipeClean.fusedMC = wipeClean.verbMC

Wipe (wipe-class): already has full profile — construction is redundant.

Empirical data: grammaticality judgments

The stimuli live as generated rows in Data.Examples.GoldbergJackendoff2004 (from the per-paper JSON); this layer projects each row into a typed datum carrying the study's classification. Other studies (Dendikken, Tay, Levin) connect to this shared data through the datum layer or the rows directly.

inductive GoldbergJackendoff2004.ResultativeType : Type

What type of resultative is exemplified.

Extends the paper's 2×2 matrix (§2) with fake reflexives (§2, ex. 9) and anticausative property resultatives ([Lev26]).

• causativeProperty : ResultativeType
• causativePath : ResultativeType
• noncausativeProperty : ResultativeType
• noncausativePath : ResultativeType
• fakeReflexive : ResultativeType
• anticausativeProperty : ResultativeType

  Anticausative: verb doesn't alternate alone; construction licenses it ([Lev26]). Distinct from noncausativeProperty (e.g., freeze solid) where the verb independently shows the causative alternation.

@[instance_reducible]

instance GoldbergJackendoff2004.instReprResultativeType : Repr ResultativeType

Equations

• GoldbergJackendoff2004.instReprResultativeType = { reprPrec := GoldbergJackendoff2004.instReprResultativeType.repr }

def GoldbergJackendoff2004.instReprResultativeType.repr : ResultativeType → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance GoldbergJackendoff2004.instDecidableEqResultativeType : DecidableEq ResultativeType

Equations

• GoldbergJackendoff2004.instDecidableEqResultativeType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

structure GoldbergJackendoff2004.ResultativeDatum : Type

A single resultative example with judgment data.

• exId : String

  Example identifier (the paper's own example label)

• sentence : String

  The sentence

• judgment : Features.Judgment

  Acceptability judgment

• resType : ResultativeType

  Which resultative subtype

• phenomenon : String

  What phenomenon this illustrates

def GoldbergJackendoff2004.instReprResultativeDatum.repr : ResultativeDatum → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance GoldbergJackendoff2004.instReprResultativeDatum : Repr ResultativeDatum

Equations

• GoldbergJackendoff2004.instReprResultativeDatum = { reprPrec := GoldbergJackendoff2004.instReprResultativeDatum.repr }

@[instance_reducible]

instance GoldbergJackendoff2004.instBEqResultativeDatum : BEq ResultativeDatum

Equations

• GoldbergJackendoff2004.instBEqResultativeDatum = { beq := GoldbergJackendoff2004.instBEqResultativeDatum.beq }

def GoldbergJackendoff2004.instBEqResultativeDatum.beq : ResultativeDatum → ResultativeDatum → Bool

Equations

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

def GoldbergJackendoff2004.ResultativeDatum.ofExample (ex : Data.Examples.LinguisticExample) (resType : ResultativeType) (phenomenon : String) : ResultativeDatum

Project a generated example row into a typed datum. Sentence, label, and judgment come from the row; the ResultativeType classification and phenomenon gloss are the study's reading (mirrored in the row's paperFeatures).

Equations

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

Causative property resultatives (exx. 5a, 7a, 8a; §6.2)

def GoldbergJackendoff2004.hammer_flat : ResultativeDatum

Equations

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

def GoldbergJackendoff2004.water_flat : ResultativeDatum

Equations

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

def GoldbergJackendoff2004.drink_dry : ResultativeDatum

Equations

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

def GoldbergJackendoff2004.wipe_clean : ResultativeDatum

Equations

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

Causative path resultatives (exx. 5b, 7b, 8b)

def GoldbergJackendoff2004.laugh_off_stage : ResultativeDatum

Equations

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

def GoldbergJackendoff2004.break_into_pieces : ResultativeDatum

Equations

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

def GoldbergJackendoff2004.talk_into_stupor : ResultativeDatum

Equations

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

Noncausative property resultatives (exx. 6a, 45c)

def GoldbergJackendoff2004.freeze_solid : ResultativeDatum

Equations

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

def GoldbergJackendoff2004.bleed_to_death : ResultativeDatum

Equations

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

Noncausative path resultatives (exx. 6b, 97c)

def GoldbergJackendoff2004.roll_out_of_room : ResultativeDatum

Equations

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

def GoldbergJackendoff2004.rumble_into_station : ResultativeDatum

Equations

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

Fake reflexive resultatives (§2, ex. 9a)

The starred diagnostics — *We yelled ourselves (unselected without the RP) and *We yelled Harry hoarse (no alternation with other NPs) — live as the row's alternatives.

def GoldbergJackendoff2004.yell_hoarse : ResultativeDatum

Equations

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

Aspectual contrasts (§4.1, exx. 23–24)

structure GoldbergJackendoff2004.AspectualContrast : Type

An aspectual contrast pair.

• sentence : String

  Sentence with temporal adverbial

• judgment : Features.Judgment

  Acceptability

• adverbialType : String

  Which adverbial type

• description : String

  Description

@[instance_reducible]

instance GoldbergJackendoff2004.instReprAspectualContrast : Repr AspectualContrast

Equations

• GoldbergJackendoff2004.instReprAspectualContrast = { reprPrec := GoldbergJackendoff2004.instReprAspectualContrast.repr }

def GoldbergJackendoff2004.instReprAspectualContrast.repr : AspectualContrast → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance GoldbergJackendoff2004.instBEqAspectualContrast : BEq AspectualContrast

Equations

• GoldbergJackendoff2004.instBEqAspectualContrast = { beq := GoldbergJackendoff2004.instBEqAspectualContrast.beq }

def GoldbergJackendoff2004.instBEqAspectualContrast.beq : AspectualContrast → AspectualContrast → Bool

Equations

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

def GoldbergJackendoff2004.AspectualContrast.ofExample (ex : Data.Examples.LinguisticExample) (description : String) : AspectualContrast

Project a generated example row into an aspectual contrast.

Equations

• GoldbergJackendoff2004.AspectualContrast.ofExample ex description = { sentence := ex.primaryText, judgment := ex.judgment, adverbialType := "for-adverbial", description := description }

def GoldbergJackendoff2004.heat_hotter : AspectualContrast

Equations

• GoldbergJackendoff2004.heat_hotter = GoldbergJackendoff2004.AspectualContrast.ofExample GoldbergJackendoff2004.Examples.gj2004_23a "ex. 23a: non-end-bounded AP RP → atelic, for-adverbial OK"

def GoldbergJackendoff2004.hammer_ever_flatter : AspectualContrast

Equations

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

def GoldbergJackendoff2004.weave_longer : AspectualContrast

Equations

• GoldbergJackendoff2004.weave_longer = GoldbergJackendoff2004.AspectualContrast.ofExample GoldbergJackendoff2004.Examples.gj2004_23c "ex. 23c: non-end-bounded AP RP → atelic, for-adverbial OK"

def GoldbergJackendoff2004.float_into_cave_for : AspectualContrast

Equations

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

def GoldbergJackendoff2004.push_off_sofa_for : AspectualContrast

Equations

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

def GoldbergJackendoff2004.float_down_river_for : AspectualContrast

Equations

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

def GoldbergJackendoff2004.push_along_trail_for : AspectualContrast

Equations

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

Semantic coherence violations (§6.2, ex. 45)

def GoldbergJackendoff2004.yell_hoarse_bare : ResultativeDatum

Equations

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

def GoldbergJackendoff2004.cry_to_sleep : ResultativeDatum

Equations

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

Aggregate data

def GoldbergJackendoff2004.allExamples : List ResultativeDatum

Equations

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

def GoldbergJackendoff2004.aspectualContrasts : List AspectualContrast

Equations

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