@cite{goldberg-jackendoff-2004}: The English Resultative as a Family of Constructions

@cite{goldberg-jackendoff-2004}

Formalization of the core claims from @cite{goldberg-jackendoff-2004}.

Key claims

1. The English resultative is not one construction but a family of four subconstructions organized along two dimensions: causative/noncausative × property/path RP
2. Every resultative has a dual subevent structure: a verbal subevent (from the verb) and a constructional subevent (CAUSE + BECOME/GO from the construction)
3. The verbal and constructional subevents are linked by typed semantic relations: MEANS, RESULT, INSTANCE, or CO-OCCURRENCE
4. Full Argument Realization (FAR): all obligatory arguments of both verb and construction must be syntactically realized; shared arguments fuse
5. Semantic Coherence: verb role rV and construction role rC may fuse only if rV is construable as an instance of rC
6. Aspectual constraint: resultatives are telic iff the RP denotes a bounded path/property
7. Temporal constraint: the constructional subevent cannot temporally precede the verbal subevent

Core types

inductive ConstructionGrammar.Studies.GoldbergJackendoff2004.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)

def ConstructionGrammar.Studies.GoldbergJackendoff2004.instReprSubeventKind.repr : SubeventKind → ℕ → Std.Format

Equations

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

instance ConstructionGrammar.Studies.GoldbergJackendoff2004.instReprSubeventKind : Repr SubeventKind

Equations

• ConstructionGrammar.Studies.GoldbergJackendoff2004.instReprSubeventKind = { reprPrec := ConstructionGrammar.Studies.GoldbergJackendoff2004.instReprSubeventKind.repr }

instance ConstructionGrammar.Studies.GoldbergJackendoff2004.instDecidableEqSubeventKind : DecidableEq SubeventKind

Equations

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

instance ConstructionGrammar.Studies.GoldbergJackendoff2004.instBEqSubeventKind : BEq SubeventKind

Equations

• ConstructionGrammar.Studies.GoldbergJackendoff2004.instBEqSubeventKind = { beq := ConstructionGrammar.Studies.GoldbergJackendoff2004.instBEqSubeventKind.beq }

def ConstructionGrammar.Studies.GoldbergJackendoff2004.instBEqSubeventKind.beq : SubeventKind → SubeventKind → Bool

Equations

• ConstructionGrammar.Studies.GoldbergJackendoff2004.instBEqSubeventKind.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

inductive ConstructionGrammar.Studies.GoldbergJackendoff2004.SubeventRelation : Type

How the verbal and constructional subevents are related (§3).

• means: The verbal subevent is the means by which the constructional subevent is brought about. E.g., "hammer metal flat" — hammering is the means of causing flatness.
• result: The constructional subevent is an independent result of the verbal subevent. E.g., "the river froze solid" — becoming solid results from freezing.
• instance_: The verbal subevent is an instance of the constructional subevent. E.g., "kick the ball into the field" — kicking IS a way of causing motion.
• coOccurrence: The two subevents merely co-occur without causal connection. E.g., "She sang her way down the road" — singing accompanies motion.

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

def ConstructionGrammar.Studies.GoldbergJackendoff2004.instReprSubeventRelation.repr : SubeventRelation → ℕ → Std.Format

Equations

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

instance ConstructionGrammar.Studies.GoldbergJackendoff2004.instReprSubeventRelation : Repr SubeventRelation

Equations

• ConstructionGrammar.Studies.GoldbergJackendoff2004.instReprSubeventRelation = { reprPrec := ConstructionGrammar.Studies.GoldbergJackendoff2004.instReprSubeventRelation.repr }

instance ConstructionGrammar.Studies.GoldbergJackendoff2004.instDecidableEqSubeventRelation : DecidableEq SubeventRelation

Equations

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

instance ConstructionGrammar.Studies.GoldbergJackendoff2004.instBEqSubeventRelation : BEq SubeventRelation

Equations

• ConstructionGrammar.Studies.GoldbergJackendoff2004.instBEqSubeventRelation = { beq := ConstructionGrammar.Studies.GoldbergJackendoff2004.instBEqSubeventRelation.beq }

def ConstructionGrammar.Studies.GoldbergJackendoff2004.instBEqSubeventRelation.beq : SubeventRelation → SubeventRelation → Bool

Equations

• ConstructionGrammar.Studies.GoldbergJackendoff2004.instBEqSubeventRelation.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

inductive ConstructionGrammar.Studies.GoldbergJackendoff2004.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"

def ConstructionGrammar.Studies.GoldbergJackendoff2004.instReprRPType.repr : RPType → ℕ → Std.Format

Equations

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

instance ConstructionGrammar.Studies.GoldbergJackendoff2004.instReprRPType : Repr RPType

Equations

• ConstructionGrammar.Studies.GoldbergJackendoff2004.instReprRPType = { reprPrec := ConstructionGrammar.Studies.GoldbergJackendoff2004.instReprRPType.repr }

instance ConstructionGrammar.Studies.GoldbergJackendoff2004.instDecidableEqRPType : DecidableEq RPType

Equations

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

def ConstructionGrammar.Studies.GoldbergJackendoff2004.instBEqRPType.beq : RPType → RPType → Bool

Equations

• ConstructionGrammar.Studies.GoldbergJackendoff2004.instBEqRPType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance ConstructionGrammar.Studies.GoldbergJackendoff2004.instBEqRPType : BEq RPType

Equations

• ConstructionGrammar.Studies.GoldbergJackendoff2004.instBEqRPType = { beq := ConstructionGrammar.Studies.GoldbergJackendoff2004.instBEqRPType.beq }

inductive ConstructionGrammar.Studies.GoldbergJackendoff2004.ResultativeSubconstruction : Type

The four subconstructions in the resultative family (§2, Table 1).

	Property RP	Path RP
Causative	causativeProperty	causativePath
Noncausative	noncausativeProperty	noncausativePath

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

instance ConstructionGrammar.Studies.GoldbergJackendoff2004.instReprResultativeSubconstruction : Repr ResultativeSubconstruction

Equations

• ConstructionGrammar.Studies.GoldbergJackendoff2004.instReprResultativeSubconstruction = { reprPrec := ConstructionGrammar.Studies.GoldbergJackendoff2004.instReprResultativeSubconstruction.repr }

def ConstructionGrammar.Studies.GoldbergJackendoff2004.instReprResultativeSubconstruction.repr : ResultativeSubconstruction → ℕ → Std.Format

Equations

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

instance ConstructionGrammar.Studies.GoldbergJackendoff2004.instDecidableEqResultativeSubconstruction : DecidableEq ResultativeSubconstruction

Equations

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

instance ConstructionGrammar.Studies.GoldbergJackendoff2004.instBEqResultativeSubconstruction : BEq ResultativeSubconstruction

Equations

• ConstructionGrammar.Studies.GoldbergJackendoff2004.instBEqResultativeSubconstruction = { beq := ConstructionGrammar.Studies.GoldbergJackendoff2004.instBEqResultativeSubconstruction.beq }

def ConstructionGrammar.Studies.GoldbergJackendoff2004.instBEqResultativeSubconstruction.beq : ResultativeSubconstruction → ResultativeSubconstruction → Bool

Equations

• ConstructionGrammar.Studies.GoldbergJackendoff2004.instBEqResultativeSubconstruction.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def ConstructionGrammar.Studies.GoldbergJackendoff2004.ResultativeSubconstruction.isCausative : ResultativeSubconstruction → Bool

Whether a subconstruction is causative.

Equations

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

def ConstructionGrammar.Studies.GoldbergJackendoff2004.ResultativeSubconstruction.isPropertyRP : ResultativeSubconstruction → Bool

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

Equations

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

def ConstructionGrammar.Studies.GoldbergJackendoff2004.ResultativeSubconstruction.rpType : ResultativeSubconstruction → RPType

Get the RP type of a subconstruction.

Equations

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

Dual subevent structure (§3)

structure ConstructionGrammar.Studies.GoldbergJackendoff2004.SubeventDesc : Type

Description of a subevent.

• description : String

  What the subevent describes

• hasCause : Bool

  Whether CAUSE is part of this subevent

• hasBecome : Bool

  Whether BECOME/GO is part of this subevent

def ConstructionGrammar.Studies.GoldbergJackendoff2004.instReprSubeventDesc.repr : SubeventDesc → ℕ → Std.Format

Equations

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

instance ConstructionGrammar.Studies.GoldbergJackendoff2004.instReprSubeventDesc : Repr SubeventDesc

Equations

• ConstructionGrammar.Studies.GoldbergJackendoff2004.instReprSubeventDesc = { reprPrec := ConstructionGrammar.Studies.GoldbergJackendoff2004.instReprSubeventDesc.repr }

instance ConstructionGrammar.Studies.GoldbergJackendoff2004.instBEqSubeventDesc : BEq SubeventDesc

Equations

• ConstructionGrammar.Studies.GoldbergJackendoff2004.instBEqSubeventDesc = { beq := ConstructionGrammar.Studies.GoldbergJackendoff2004.instBEqSubeventDesc.beq }

def ConstructionGrammar.Studies.GoldbergJackendoff2004.instBEqSubeventDesc.beq : SubeventDesc → SubeventDesc → Bool

Equations

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

structure ConstructionGrammar.Studies.GoldbergJackendoff2004.DualSubevent : Type

The dual subevent structure of a resultative (§3, Principle 25).

Every resultative has exactly two subevents linked by a semantic relation.

• 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.Studies.GoldbergJackendoff2004.instReprDualSubevent.repr : DualSubevent → ℕ → Std.Format

Equations

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

instance ConstructionGrammar.Studies.GoldbergJackendoff2004.instReprDualSubevent : Repr DualSubevent

Equations

• ConstructionGrammar.Studies.GoldbergJackendoff2004.instReprDualSubevent = { reprPrec := ConstructionGrammar.Studies.GoldbergJackendoff2004.instReprDualSubevent.repr }

def ConstructionGrammar.Studies.GoldbergJackendoff2004.instBEqDualSubevent.beq : DualSubevent → DualSubevent → Bool

Equations

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

instance ConstructionGrammar.Studies.GoldbergJackendoff2004.instBEqDualSubevent : BEq DualSubevent

Equations

• ConstructionGrammar.Studies.GoldbergJackendoff2004.instBEqDualSubevent = { beq := ConstructionGrammar.Studies.GoldbergJackendoff2004.instBEqDualSubevent.beq }

Boundedness and aspect

inductive ConstructionGrammar.Studies.GoldbergJackendoff2004.Boundedness : Type

Whether an RP denotes a bounded endpoint.

Property RPs are always bounded (reaching a property state). Path RPs are bounded iff the goal is specific ("into the field" = bounded; "along the road" = unbounded).

• bounded : Boundedness
• unbounded : Boundedness

instance ConstructionGrammar.Studies.GoldbergJackendoff2004.instReprBoundedness : Repr Boundedness

Equations

• ConstructionGrammar.Studies.GoldbergJackendoff2004.instReprBoundedness = { reprPrec := ConstructionGrammar.Studies.GoldbergJackendoff2004.instReprBoundedness.repr }

def ConstructionGrammar.Studies.GoldbergJackendoff2004.instReprBoundedness.repr : Boundedness → ℕ → Std.Format

Equations

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

instance ConstructionGrammar.Studies.GoldbergJackendoff2004.instDecidableEqBoundedness : DecidableEq Boundedness

Equations

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

def ConstructionGrammar.Studies.GoldbergJackendoff2004.instBEqBoundedness.beq : Boundedness → Boundedness → Bool

Equations

• ConstructionGrammar.Studies.GoldbergJackendoff2004.instBEqBoundedness.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance ConstructionGrammar.Studies.GoldbergJackendoff2004.instBEqBoundedness : BEq Boundedness

Equations

• ConstructionGrammar.Studies.GoldbergJackendoff2004.instBEqBoundedness = { beq := ConstructionGrammar.Studies.GoldbergJackendoff2004.instBEqBoundedness.beq }

Resultative entry

structure ConstructionGrammar.Studies.GoldbergJackendoff2004.ResultativeEntry : Type

A resultative entry: verb + subconstruction + subevent structure + aspect.

• verb : String

  The verb form

• subconstruction : ResultativeSubconstruction

  Which subconstruction

• subevents : DualSubevent

  The dual subevent structure

• rpBoundedness : Boundedness

  Boundedness of the result phrase

• bareVerbClass : Semantics.Tense.Aspect.LexicalAspect.VendlerClass

  Vendler class of the bare verb (without resultative)

def ConstructionGrammar.Studies.GoldbergJackendoff2004.instReprResultativeEntry.repr : ResultativeEntry → ℕ → Std.Format

Equations

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

instance ConstructionGrammar.Studies.GoldbergJackendoff2004.instReprResultativeEntry : Repr ResultativeEntry

Equations

• ConstructionGrammar.Studies.GoldbergJackendoff2004.instReprResultativeEntry = { reprPrec := ConstructionGrammar.Studies.GoldbergJackendoff2004.instReprResultativeEntry.repr }

instance ConstructionGrammar.Studies.GoldbergJackendoff2004.instBEqResultativeEntry : BEq ResultativeEntry

Equations

• ConstructionGrammar.Studies.GoldbergJackendoff2004.instBEqResultativeEntry = { beq := ConstructionGrammar.Studies.GoldbergJackendoff2004.instBEqResultativeEntry.beq }

def ConstructionGrammar.Studies.GoldbergJackendoff2004.instBEqResultativeEntry.beq : ResultativeEntry → ResultativeEntry → Bool

Equations

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

Aspectual profile (§4, 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.Studies.GoldbergJackendoff2004.resultativeAspect (b : Boundedness) : Semantics.Tense.Aspect.LexicalAspect.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.Studies.GoldbergJackendoff2004.resultativeVendlerClass (b : Boundedness) : Semantics.Tense.Aspect.LexicalAspect.VendlerClass

Derive the Vendler class of a resultative.

Equations

• ConstructionGrammar.Studies.GoldbergJackendoff2004.resultativeVendlerClass b = (ConstructionGrammar.Studies.GoldbergJackendoff2004.resultativeAspect b).toVendlerClass

Semantic roles and argument licensing

inductive ConstructionGrammar.Studies.GoldbergJackendoff2004.SemRole : Type

Semantic roles relevant to resultatives (§6).

• agent : SemRole
• patient : SemRole
• theme : SemRole
• resultGoal : SemRole

def ConstructionGrammar.Studies.GoldbergJackendoff2004.instReprSemRole.repr : SemRole → ℕ → Std.Format

Equations

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

instance ConstructionGrammar.Studies.GoldbergJackendoff2004.instReprSemRole : Repr SemRole

Equations

• ConstructionGrammar.Studies.GoldbergJackendoff2004.instReprSemRole = { reprPrec := ConstructionGrammar.Studies.GoldbergJackendoff2004.instReprSemRole.repr }

instance ConstructionGrammar.Studies.GoldbergJackendoff2004.instDecidableEqSemRole : DecidableEq SemRole

Equations

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

def ConstructionGrammar.Studies.GoldbergJackendoff2004.instBEqSemRole.beq : SemRole → SemRole → Bool

Equations

• ConstructionGrammar.Studies.GoldbergJackendoff2004.instBEqSemRole.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance ConstructionGrammar.Studies.GoldbergJackendoff2004.instBEqSemRole : BEq SemRole

Equations

• ConstructionGrammar.Studies.GoldbergJackendoff2004.instBEqSemRole = { beq := ConstructionGrammar.Studies.GoldbergJackendoff2004.instBEqSemRole.beq }

structure ConstructionGrammar.Studies.GoldbergJackendoff2004.ArgSource : Type

An argument with its source (verb or construction).

• role : SemRole

  The semantic role

• fromVerb : Bool

  Whether this argument comes from the verb

• fromConstruction : Bool

  Whether this argument comes from the construction

instance ConstructionGrammar.Studies.GoldbergJackendoff2004.instReprArgSource : Repr ArgSource

Equations

• ConstructionGrammar.Studies.GoldbergJackendoff2004.instReprArgSource = { reprPrec := ConstructionGrammar.Studies.GoldbergJackendoff2004.instReprArgSource.repr }

def ConstructionGrammar.Studies.GoldbergJackendoff2004.instReprArgSource.repr : ArgSource → ℕ → Std.Format

Equations

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

instance ConstructionGrammar.Studies.GoldbergJackendoff2004.instBEqArgSource : BEq ArgSource

Equations

• ConstructionGrammar.Studies.GoldbergJackendoff2004.instBEqArgSource = { beq := ConstructionGrammar.Studies.GoldbergJackendoff2004.instBEqArgSource.beq }

def ConstructionGrammar.Studies.GoldbergJackendoff2004.instBEqArgSource.beq : ArgSource → ArgSource → Bool

Equations

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

def ConstructionGrammar.Studies.GoldbergJackendoff2004.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.Studies.GoldbergJackendoff2004.farSatisfied (args : List ArgSource) : Bool

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

Equations

• ConstructionGrammar.Studies.GoldbergJackendoff2004.farSatisfied args = args.all fun (a : ConstructionGrammar.Studies.GoldbergJackendoff2004.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.Studies.GoldbergJackendoff2004.rolesCoherent (rV rC : SemRole) : Bool

Which role pairs are coherent for fusion.

Agent can fuse with agent; patient with patient or theme; theme with patient or theme.

Equations

• One or more equations did not get rendered due to their size.
• ConstructionGrammar.Studies.GoldbergJackendoff2004.rolesCoherent rV rC = false

def ConstructionGrammar.Studies.GoldbergJackendoff2004.semanticCoherenceSatisfied (args : List (SemRole × SemRole)) : 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, Principle 33)

The constructional subevent cannot temporally precede the verbal subevent.

inductive ConstructionGrammar.Studies.GoldbergJackendoff2004.TemporalOrder : Type

Temporal ordering between subevents.

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

instance ConstructionGrammar.Studies.GoldbergJackendoff2004.instReprTemporalOrder : Repr TemporalOrder

Equations

• ConstructionGrammar.Studies.GoldbergJackendoff2004.instReprTemporalOrder = { reprPrec := ConstructionGrammar.Studies.GoldbergJackendoff2004.instReprTemporalOrder.repr }

def ConstructionGrammar.Studies.GoldbergJackendoff2004.instReprTemporalOrder.repr : TemporalOrder → ℕ → Std.Format

Equations

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

instance ConstructionGrammar.Studies.GoldbergJackendoff2004.instDecidableEqTemporalOrder : DecidableEq TemporalOrder

Equations

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

def ConstructionGrammar.Studies.GoldbergJackendoff2004.instBEqTemporalOrder.beq : TemporalOrder → TemporalOrder → Bool

Equations

• ConstructionGrammar.Studies.GoldbergJackendoff2004.instBEqTemporalOrder.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance ConstructionGrammar.Studies.GoldbergJackendoff2004.instBEqTemporalOrder : BEq TemporalOrder

Equations

• ConstructionGrammar.Studies.GoldbergJackendoff2004.instBEqTemporalOrder = { beq := ConstructionGrammar.Studies.GoldbergJackendoff2004.instBEqTemporalOrder.beq }

def ConstructionGrammar.Studies.GoldbergJackendoff2004.temporalConstraintSatisfied (order : TemporalOrder) : Bool

Check the temporal constraint: constructional subevent does not precede verbal.

Equations

• ConstructionGrammar.Studies.GoldbergJackendoff2004.temporalConstraintSatisfied ConstructionGrammar.Studies.GoldbergJackendoff2004.TemporalOrder.verbalFirst = true
• ConstructionGrammar.Studies.GoldbergJackendoff2004.temporalConstraintSatisfied ConstructionGrammar.Studies.GoldbergJackendoff2004.TemporalOrder.simultaneous = true
• ConstructionGrammar.Studies.GoldbergJackendoff2004.temporalConstraintSatisfied ConstructionGrammar.Studies.GoldbergJackendoff2004.TemporalOrder.constructionalFirst = false

Empirical data: resultative entries

def ConstructionGrammar.Studies.GoldbergJackendoff2004.hammerFlat : ResultativeEntry

Equations

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

def ConstructionGrammar.Studies.GoldbergJackendoff2004.kickIntoField : ResultativeEntry

Equations

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

def ConstructionGrammar.Studies.GoldbergJackendoff2004.freezeSolid : ResultativeEntry

Equations

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

def ConstructionGrammar.Studies.GoldbergJackendoff2004.rollIntoField : ResultativeEntry

Equations

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

def ConstructionGrammar.Studies.GoldbergJackendoff2004.drinkSick : ResultativeEntry

Equations

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

def ConstructionGrammar.Studies.GoldbergJackendoff2004.laughSilly : ResultativeEntry

Equations

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

def ConstructionGrammar.Studies.GoldbergJackendoff2004.swingShut : ResultativeEntry

Equations

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

def ConstructionGrammar.Studies.GoldbergJackendoff2004.wipeClea : ResultativeEntry

Equations

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

def ConstructionGrammar.Studies.GoldbergJackendoff2004.allEntries : List ResultativeEntry

All resultative entries.

Equations

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

Per-datum verification theorems

theorem ConstructionGrammar.Studies.GoldbergJackendoff2004.hammerFlat_is_causativeProperty : hammerFlat.subconstruction = ResultativeSubconstruction.causativeProperty

theorem ConstructionGrammar.Studies.GoldbergJackendoff2004.kickIntoField_is_causativePath : kickIntoField.subconstruction = ResultativeSubconstruction.causativePath

theorem ConstructionGrammar.Studies.GoldbergJackendoff2004.freezeSolid_is_noncausativeProperty : freezeSolid.subconstruction = ResultativeSubconstruction.noncausativeProperty

theorem ConstructionGrammar.Studies.GoldbergJackendoff2004.rollIntoField_is_noncausativePath : rollIntoField.subconstruction = ResultativeSubconstruction.noncausativePath

theorem ConstructionGrammar.Studies.GoldbergJackendoff2004.hammerFlat_means : hammerFlat.subevents.relation = SubeventRelation.means

theorem ConstructionGrammar.Studies.GoldbergJackendoff2004.freezeSolid_result : freezeSolid.subevents.relation = SubeventRelation.result

theorem ConstructionGrammar.Studies.GoldbergJackendoff2004.drinkSick_means : drinkSick.subevents.relation = SubeventRelation.means

theorem ConstructionGrammar.Studies.GoldbergJackendoff2004.hammerFlat_has_cause : hammerFlat.subevents.constructional.hasCause = true

theorem ConstructionGrammar.Studies.GoldbergJackendoff2004.kickIntoField_has_cause : kickIntoField.subevents.constructional.hasCause = true

theorem ConstructionGrammar.Studies.GoldbergJackendoff2004.drinkSick_has_cause : drinkSick.subevents.constructional.hasCause = true

theorem ConstructionGrammar.Studies.GoldbergJackendoff2004.freezeSolid_no_cause : freezeSolid.subevents.constructional.hasCause = false

theorem ConstructionGrammar.Studies.GoldbergJackendoff2004.rollIntoField_no_cause : rollIntoField.subevents.constructional.hasCause = false

theorem ConstructionGrammar.Studies.GoldbergJackendoff2004.swingShut_no_cause : swingShut.subevents.constructional.hasCause = false

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

All causative entries have CAUSE in their constructional subevent.

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

All noncausative entries lack CAUSE in their constructional subevent.

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

All constructional subevents have BECOME.

theorem ConstructionGrammar.Studies.GoldbergJackendoff2004.bounded_rp_telic : resultativeVendlerClass Boundedness.bounded = Semantics.Tense.Aspect.LexicalAspect.VendlerClass.accomplishment

Bounded RP yields telic resultative (= accomplishment).

theorem ConstructionGrammar.Studies.GoldbergJackendoff2004.unbounded_rp_atelic : resultativeVendlerClass Boundedness.unbounded = Semantics.Tense.Aspect.LexicalAspect.VendlerClass.activity

Unbounded RP yields atelic resultative (= activity).

theorem ConstructionGrammar.Studies.GoldbergJackendoff2004.bounded_entries_telic : ((List.filter (fun (x : ResultativeEntry) => x.rpBoundedness == Boundedness.bounded) allEntries).all fun (e : ResultativeEntry) => (resultativeAspect e.rpBoundedness).telicity == Semantics.Tense.Aspect.LexicalAspect.Telicity.telic) = true

All entries with bounded RP are telic.

theorem ConstructionGrammar.Studies.GoldbergJackendoff2004.resultative_telicizes_activity : Semantics.Tense.Aspect.LexicalAspect.activityProfile.telicize.toVendlerClass = Semantics.Tense.Aspect.LexicalAspect.VendlerClass.accomplishment

Resultative telicizes an activity verb: adding bounded RP to an activity yields an accomplishment (§4, Principle 27).

theorem ConstructionGrammar.Studies.GoldbergJackendoff2004.resultative_aspect_matches_telicize (e : ResultativeEntry) (hVerb : e.bareVerbClass = Semantics.Tense.Aspect.LexicalAspect.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.

Inheritance network

The four subconstructions inherit from the existing resultative construction in ArgumentStructure.lean.

def ConstructionGrammar.Studies.GoldbergJackendoff2004.causativePropertyConstruction : ArgStructureConstruction

ArgStructureConstruction for each subconstruction.

Equations

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

def ConstructionGrammar.Studies.GoldbergJackendoff2004.causativePathConstruction : ArgStructureConstruction

Equations

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

def ConstructionGrammar.Studies.GoldbergJackendoff2004.noncausativePropertyConstruction : ArgStructureConstruction

Equations

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

def ConstructionGrammar.Studies.GoldbergJackendoff2004.noncausativePathConstruction : ArgStructureConstruction

Equations

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

def ConstructionGrammar.Studies.GoldbergJackendoff2004.resultativeFamily : List ArgStructureConstruction

The full resultative family: all four subconstructions.

Equations

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

def ConstructionGrammar.Studies.GoldbergJackendoff2004.resultativeInheritance : List InheritanceLink

Inheritance links from the four subconstructions to the parent resultative.

Equations

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

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

All inheritance links point to the same parent.

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

All four subconstructions are fully abstract (decomposable).

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

Causative subconstructions are transitive (4 slots).

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

Noncausative subconstructions are intransitive (3 slots).

theorem ConstructionGrammar.Studies.GoldbergJackendoff2004.causativeProperty_decomposes : decompose causativePropertyConstruction = [Core.CombinationKind.headSpecifier, Core.CombinationKind.headComplement, Core.CombinationKind.headComplement]

All four subconstructions decompose via the existing decompose function.

Causative subconstructions decompose to [HS, HC, HC]. Noncausative subconstructions decompose to [HS, HC].

theorem ConstructionGrammar.Studies.GoldbergJackendoff2004.causativePath_decomposes : decompose causativePathConstruction = [Core.CombinationKind.headSpecifier, Core.CombinationKind.headComplement, Core.CombinationKind.headComplement]

theorem ConstructionGrammar.Studies.GoldbergJackendoff2004.noncausativeProperty_decomposes : decompose noncausativePropertyConstruction = [Core.CombinationKind.headSpecifier, Core.CombinationKind.headComplement]

theorem ConstructionGrammar.Studies.GoldbergJackendoff2004.noncausativePath_decomposes : decompose noncausativePathConstruction = [Core.CombinationKind.headSpecifier, Core.CombinationKind.headComplement]

theorem ConstructionGrammar.Studies.GoldbergJackendoff2004.causative_match_parent : decompose causativePropertyConstruction = decompose resultative ∧ decompose causativePathConstruction = decompose resultative

The causative subconstructions have the same decomposition as the parent resultative construction.