Documentation

Linglib.Syntax.ConstructionGrammar.Resultatives

The resultative construction family #

[GJ04]'s four-way resultative family — causative or noncausative, with a property or path result phrase — as a dual subevent structure: a verbal subevent related to a constructional subevent, with fusion linking verb meaning to constructional contribution.

Main definitions #

ResultativeSubconstruction: the 2 × 2 family, with its derived subevent structure (constructionalDesc) and constructions (toConstruction, resultativeNetwork)
SubeventDesc, DualSubevent, SubeventRelation: dual subevent structure
ResultativeEntry, ResultativeEntry.fusedMC: a verb in a subconstruction, and its fused meaning
farSatisfied, rolesCoherent, temporalConstraintSatisfied: the paper's three substantive constraints

Core types #

inductive ConstructionGrammar.Resultatives.SubeventKind :

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)

Instances For

@[instance_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.

Instances For

@[instance_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 :

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

means : SubeventRelation
The verbal subevent is the means of the constructional one — the default for all four core subconstructions: in "hammer the metal flat", hammering is the means of causing flatness.
result : SubeventRelation
The verbal subevent results from the constructional one, as in sound-emission ("the trolley rumbled through the tunnel", ex. 17a) and disappearance resultatives (ex. 21a).
instance_ : SubeventRelation
The verbal subevent is an instance of the constructional one, as in the follow-type cases ("Bill followed the thief into the library", ex. 50a).
coOccurrence : SubeventRelation
The subevents merely co-occur, as in the way construction ("the car honked its way down the road", ex. 19a).

Instances For

def ConstructionGrammar.Resultatives.instReprSubeventRelation.repr :

SubeventRelation → ℕ → Std.Format

Equations

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

Instances For

@[instance_reducible]

instance ConstructionGrammar.Resultatives.instReprSubeventRelation :

Repr SubeventRelation

Equations

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

@[instance_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 of result phrase.

property : RPType
Adjectival/property result: "flat", "clean", "solid"
path : RPType
Directional/path result: "into the field", "off the table"

Instances For

@[instance_reducible]

instance ConstructionGrammar.Resultatives.instReprRPType :

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.

Instances For

@[instance_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 :

The four subconstructions of the resultative family: causative or noncausative, crossed with a property or path result phrase ([GJ04] §2, summarized as (97)).

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

Instances For

def ConstructionGrammar.Resultatives.instReprResultativeSubconstruction.repr :

ResultativeSubconstruction → ℕ → Std.Format

Equations

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

Instances For

@[instance_reducible]

instance ConstructionGrammar.Resultatives.instReprResultativeSubconstruction :

Repr ResultativeSubconstruction

Equations

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

@[instance_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

Instances For

def ConstructionGrammar.Resultatives.ResultativeSubconstruction.isPropertyRP :

ResultativeSubconstruction → Bool

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

Equations

Instances For

def ConstructionGrammar.Resultatives.ResultativeSubconstruction.rpType :

ResultativeSubconstruction → RPType

The RP type of a subconstruction.

Equations

Instances For

Dual subevent structure (§3 of [GJ04]) #

structure ConstructionGrammar.Resultatives.SubeventDesc :

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

Instances For

@[instance_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.

Instances For

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

Instances For

@[instance_reducible]

instance ConstructionGrammar.Resultatives.instBEqSubeventDesc :

BEq SubeventDesc

Equations

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

@[instance_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.

Instances For

structure ConstructionGrammar.Resultatives.DualSubevent :

The dual subevent structure of a resultative ([GJ04] §3, the analysis in 14 and 16).

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

Instances For

def ConstructionGrammar.Resultatives.instReprDualSubevent.repr :

DualSubevent → ℕ → Std.Format

Equations

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

Instances For

@[instance_reducible]

instance ConstructionGrammar.Resultatives.instReprDualSubevent :

Repr DualSubevent

Equations

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

@[instance_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

Instances For

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

The constructional subevent description a subconstruction determines: CAUSE exactly for the causatives, BECOME for all four.

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 }

Instances For

def ConstructionGrammar.Resultatives.verbalSubeventDesc :

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

Equations

ConstructionGrammar.Resultatives.verbalSubeventDesc = { }

Instances For

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 #

[GJ04]'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 → ArgumentStructure.EventStructure.Template

Map subconstruction to the constructional subevent's event template.

Equations

Instances For

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 :

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

Instances For

@[instance_reducible]

instance ConstructionGrammar.Resultatives.instReprBoundedness :

Repr Boundedness

Equations

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

def ConstructionGrammar.Resultatives.instReprBoundedness.repr :

Boundedness → ℕ → Std.Format

Equations

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

Instances For

@[instance_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 [GJ04], 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 :

How the postverbal NP is selected (§2).

selected : ObjectSelection
Verb independently selects the object: "The gardener watered the flowers flat" (7a)
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: "We yelled ourselves hoarse" (cf. *We yelled Harry hoarse) (9a)

Instances For

@[instance_reducible]

instance ConstructionGrammar.Resultatives.instReprObjectSelection :

Repr ObjectSelection

Equations

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

def ConstructionGrammar.Resultatives.instReprObjectSelection.repr :

ObjectSelection → ℕ → Std.Format

Equations

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

Instances For

@[instance_reducible]

instance ConstructionGrammar.Resultatives.instDecidableEqObjectSelection :

DecidableEq ObjectSelection

Equations

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

@[instance_reducible]

instance ConstructionGrammar.Resultatives.instBEqObjectSelection :

BEq ObjectSelection

Equations

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

def ConstructionGrammar.Resultatives.instBEqObjectSelection.beq :

ObjectSelection → ObjectSelection → Bool

Equations

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

Instances For

def ConstructionGrammar.Resultatives.ResultativeSubconstruction.defaultObjectSelection :

ResultativeSubconstruction → Option ObjectSelection

Intransitive resultatives have no object selection.

Equations

Instances For

Resultative entry #

structure ConstructionGrammar.Resultatives.ResultativeEntry :

A resultative entry: a verb in a subconstruction, with aspectual and selectional features. The dual subevent structure is derived from the subconstruction, and the Levin class feeds compositional fusion.

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 : ArgumentStructure.LevinClass
Levin class of the verb, for MeaningComponents derivation

Instances For

def ConstructionGrammar.Resultatives.instReprResultativeEntry.repr :

ResultativeEntry → ℕ → Std.Format

Equations

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

Instances For

@[instance_reducible]

instance ConstructionGrammar.Resultatives.instReprResultativeEntry :

Repr ResultativeEntry

Equations

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

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

Instances For

@[instance_reducible]

instance ConstructionGrammar.Resultatives.instBEqResultativeEntry :

BEq ResultativeEntry

Equations

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

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

The dual subevent structure of an entry.

Equations

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

Instances For

def ConstructionGrammar.Resultatives.ResultativeEntry.verbMC (e : ResultativeEntry) :

ArgumentStructure.MeaningComponents

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

Equations

e.verbMC = e.levinClass.meaningComponents

Instances For

Aspectual profile (§4 of [GJ04], 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

The aspectual profile of a resultative, from RP boundedness.

Equations

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

Instances For

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

Features.VendlerClass

The Vendler class of a resultative.

Equations

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

Instances For

Semantic roles and argument licensing #

Uses the canonical ThetaRole from the linking interface rather than a paper-specific enum. [GJ04]'s four resultative-relevant roles map to: agent, patient, theme, goal (= "resultGoal" in their terminology).

structure ConstructionGrammar.Resultatives.ArgSource :

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

Instances For

def ConstructionGrammar.Resultatives.instReprArgSource.repr :

ArgSource → ℕ → Std.Format

Equations

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

Instances For

@[instance_reducible]

instance ConstructionGrammar.Resultatives.instReprArgSource :

Equations

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

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

Instances For

@[instance_reducible]

instance ConstructionGrammar.Resultatives.instBEqArgSource :

Equations

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

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)

Instances For

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

Instances For

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

Instances For

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.

Instances For

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 :

Temporal ordering between subevents.

verbalFirst : TemporalOrder
simultaneous : TemporalOrder
constructionalFirst : TemporalOrder

Instances For

@[instance_reducible]

instance ConstructionGrammar.Resultatives.instReprTemporalOrder :

Repr TemporalOrder

Equations

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

def ConstructionGrammar.Resultatives.instReprTemporalOrder.repr :

TemporalOrder → ℕ → Std.Format

Equations

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

Instances For

@[instance_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

Instances For

Closed-scale → bounded RP bridge (§8 of [GJ04], #

Principle 27)

[GJ04] §8: productive property RPs "tend to be nongradable" and "encode a clearly delimited state." The formal correlate ([Ken07]): 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.Order.Boundedness) :

Map [Ken07]'s scale boundedness to [GJ04]'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

ConstructionGrammar.Resultatives.adjScaleToRPBoundedness b = if b.HasMax then ConstructionGrammar.Resultatives.Boundedness.bounded else ConstructionGrammar.Resultatives.Boundedness.unbounded

Instances For

theorem ConstructionGrammar.Resultatives.closed_scale_bounded :

adjScaleToRPBoundedness Core.Order.Boundedness.closed = Boundedness.bounded

Closed scales yield bounded RPs.

theorem ConstructionGrammar.Resultatives.upper_bounded_scale_bounded :

adjScaleToRPBoundedness Core.Order.Boundedness.upperBounded = Boundedness.bounded

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

theorem ConstructionGrammar.Resultatives.open_scale_unbounded :

adjScaleToRPBoundedness Core.Order.Boundedness.open_ = Boundedness.unbounded

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

theorem ConstructionGrammar.Resultatives.lower_bounded_scale_unbounded :

adjScaleToRPBoundedness Core.Order.Boundedness.lowerBounded = Boundedness.unbounded

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

theorem ConstructionGrammar.Resultatives.closed_scale_telic_resultative (b : Core.Order.Boundedness) (hMax : b.HasMax) :

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.Order.Boundedness.upperBounded = Boundedness.bounded ∧ adjScaleToRPBoundedness Core.Order.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 → ArgumentStructure.MeaningComponents

The meaning components a subconstruction contributes. 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 }

Instances For

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.meaning

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

Instances For

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"

Instances For

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"

Instances For

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

Construction ArgumentStructure.MeaningComponents

The construction a subconstruction determines, its meaning pole the subconstruction's MeaningComponents contribution.

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.

Instances For

def ConstructionGrammar.Resultatives.ResultativeEntry.fusedMC (e : ResultativeEntry) :

ArgumentStructure.MeaningComponents

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

Equations

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

Instances For

def ConstructionGrammar.Resultatives.causativePropertyConstruction :

Construction ArgumentStructure.MeaningComponents

The causative property resultative as a construction.

Equations

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

Instances For

def ConstructionGrammar.Resultatives.causativePathConstruction :

Construction ArgumentStructure.MeaningComponents

The causative path resultative as a construction.

Equations

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

Instances For

def ConstructionGrammar.Resultatives.noncausativePropertyConstruction :

Construction ArgumentStructure.MeaningComponents

The noncausative property resultative as a construction.

Equations

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

Instances For

def ConstructionGrammar.Resultatives.noncausativePathConstruction :

Construction ArgumentStructure.MeaningComponents

The noncausative path resultative as a construction.

Equations

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

Instances For

def ConstructionGrammar.Resultatives.resultativeFamily :

List (Construction ArgumentStructure.MeaningComponents)

The full resultative family, derived from all four subconstructions.

Equations

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

Instances For

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

InheritanceLink

The inheritance link from a subconstruction to the parent resultative.

Equations

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

Instances For

def ConstructionGrammar.Resultatives.resultativeInheritance :

List InheritanceLink

All four inheritance links, derived.

Equations

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

Instances For

def ConstructionGrammar.Resultatives.resultativeNetwork :

Constructicon ArgumentStructure.MeaningComponents

The [GJ04] resultative family as a constructicon: the parent construction plus its four derived subconstructions and inheritance links.

Equations

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

Instances For

theorem ConstructionGrammar.Resultatives.resultativeNetwork_wellFormed :

resultativeNetwork.WellFormed

Every derived link resolves to a member construction.

theorem ConstructionGrammar.Resultatives.subconstruction_parent (sc : ResultativeSubconstruction) :

resultativeNetwork.parentsOf sc.toConstruction.name = [resultative]

The links determine each subconstruction's mother: the resultative.

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 : Construction ArgumentStructure.MeaningComponents) => c.specificity == Specificity.fullyAbstract) = true

All four subconstructions are fully abstract (decomposable).

theorem ConstructionGrammar.Resultatives.causative_are_transitive :

List.length causativePropertyConstruction.form = 4 ∧ List.length causativePathConstruction.form = 4

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

theorem ConstructionGrammar.Resultatives.noncausative_are_intransitive :

List.length noncausativePropertyConstruction.form = 3 ∧ List.length noncausativePathConstruction.form = 3

Schema-decomposition theorems for the subconstruction family (causative_decompose_like_parent, noncausative_fewer_steps) live with [Mul13]'s decomposition apparatus in Studies/Mueller2013.lean.

Verb–construction fusion (integration with ArgumentStructure.lean) #

theorem ConstructionGrammar.Resultatives.manner_verb_alternates_in_causative_sub (mc : ArgumentStructure.MeaningComponents) (hInstr : mc.instrumentSpec = false) (sc : ResultativeSubconstruction) (hCaus : sc.isCausative = true) :

predictedAlternationInConstruction mc sc.toConstruction ArgumentStructure.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 : ArgumentStructure.MeaningComponents) (hCoS : mc.changeOfState = false) (hCaus : mc.causation = false) (sc : ResultativeSubconstruction) (hNonCaus : sc.isCausative = false) :

predictedAlternationInConstruction mc sc.toConstruction ArgumentStructure.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 ArgumentStructure.MeaningComponents.hit causativePropertyConstruction ArgumentStructure.DiathesisAlternation.causativeInchoative = true

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

theorem ConstructionGrammar.Resultatives.hit_no_alternation_in_noncausativeProperty :

predictedAlternationInConstruction ArgumentStructure.MeaningComponents.hit noncausativePropertyConstruction ArgumentStructure.DiathesisAlternation.causativeInchoative = false

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

theorem ConstructionGrammar.Resultatives.causative_sub_fuse_matches_parent (mc : ArgumentStructure.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 : ArgumentStructure.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 : ArgumentStructure.MeaningComponents) (hInstr : mc.instrumentSpec = false) (sc : ResultativeSubconstruction) :

predictedAlternationInConstruction mc sc.toConstruction ArgumentStructure.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 [GJ04], 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.Order.Boundedness) (hMax : b.HasMax) :

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 : ArgumentStructure.MeaningComponents) (sc : ResultativeSubconstruction) (hInstr : mc.instrumentSpec = false) (hCausative : sc.isCausative = true) :

have fused := composedMeaning mc sc.toConstruction; fused.predictedAlternation ArgumentStructure.DiathesisAlternation.causativeInchoative = true ∧ fused.predictedAlternation ArgumentStructure.DiathesisAlternation.middle = true ∧ fused.predictedAlternation ArgumentStructure.DiathesisAlternation.instrumentSubject = true ∧ fused.predictedAlternation ArgumentStructure.DiathesisAlternation.resultative = true

Alternation chain: corollary of fuse_cos_caus_enables for causative resultative subconstructions.

theorem ConstructionGrammar.Resultatives.noncausative_partial_chain (mc : ArgumentStructure.MeaningComponents) (sc : ResultativeSubconstruction) (hInstr : mc.instrumentSpec = false) (hNonCaus : sc.isCausative = false) (hNoCaus : mc.causation = false) :

have fused := composedMeaning mc sc.toConstruction; fused.predictedAlternation ArgumentStructure.DiathesisAlternation.middle = true ∧ fused.predictedAlternation ArgumentStructure.DiathesisAlternation.resultative = true ∧ fused.predictedAlternation ArgumentStructure.DiathesisAlternation.causativeInchoative = false ∧ fused.predictedAlternation ArgumentStructure.DiathesisAlternation.instrumentSubject = false

Noncausative contrast: corollary of fuse_cos_only_partial.

theorem ConstructionGrammar.Resultatives.instrumentSpec_blocks_across_subconstructions (mc : ArgumentStructure.MeaningComponents) (sc : ResultativeSubconstruction) (hInstr : mc.instrumentSpec = true) :

have fused := composedMeaning mc sc.toConstruction; fused.predictedAlternation ArgumentStructure.DiathesisAlternation.causativeInchoative = false ∧ fused.predictedAlternation ArgumentStructure.DiathesisAlternation.instrumentSubject = false ∧ fused.predictedAlternation ArgumentStructure.DiathesisAlternation.resultative = false

instrumentSpec blocking: corollary of instrumentSpec_blocks_after_fuse.