Documentation

Linglib.Phenomena.Constructions.Resultatives.Data

Resultative Construction — Empirical Data #

@cite{goldberg-jackendoff-2004}

Theory-neutral grammaticality judgments and aspectual contrasts for English resultative constructions, drawn from @cite{goldberg-jackendoff-2004} "The English Resultative as a Family of Constructions" (Language 80(3):532–568).

Phenomena covered #

Causative property resultatives: "hammer the metal flat"
Causative path resultatives: "kick the ball into the field"
Noncausative property resultatives: "the river froze solid"
Noncausative path resultatives: "the ball rolled into the field"
Fake reflexive resultatives: "She laughed herself silly"
Aspectual contrasts: telic vs atelic frame tests
Unacceptable resultatives: semantic coherence violations

Datum structure #

inductive Phenomena.Constructions.Resultatives.ResultativeType :

What type of resultative is exemplified.

causativeProperty : ResultativeType
causativePath : ResultativeType
noncausativeProperty : ResultativeType
noncausativePath : ResultativeType
fakeReflexive : ResultativeType
anticausativeProperty : ResultativeType
Anticausative: verb doesn't alternate alone; construction licenses it (@cite{levin-2026}). Distinct from noncausativeProperty (e.g., freeze solid) where the verb independently shows the causative alternation.

Instances For

instance Phenomena.Constructions.Resultatives.instReprResultativeType :

Repr ResultativeType

Equations

Phenomena.Constructions.Resultatives.instReprResultativeType = { reprPrec := Phenomena.Constructions.Resultatives.instReprResultativeType.repr }

def Phenomena.Constructions.Resultatives.instReprResultativeType.repr :

ResultativeType → Nat → Std.Format

Equations

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

Instances For

instance Phenomena.Constructions.Resultatives.instDecidableEqResultativeType :

DecidableEq ResultativeType

Equations

Phenomena.Constructions.Resultatives.instDecidableEqResultativeType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.Constructions.Resultatives.instBEqResultativeType :

BEq ResultativeType

Equations

Phenomena.Constructions.Resultatives.instBEqResultativeType = { beq := Phenomena.Constructions.Resultatives.instBEqResultativeType.beq }

def Phenomena.Constructions.Resultatives.instBEqResultativeType.beq :

ResultativeType → ResultativeType → Bool

Equations

Phenomena.Constructions.Resultatives.instBEqResultativeType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

structure Phenomena.Constructions.Resultatives.ResultativeDatum :

A single resultative example with judgment data.

exId : String
Example identifier
sentence : String
The sentence
judgment : Core.Empirical.Acceptability
Acceptability judgment
resType : ResultativeType
Which resultative subtype
phenomenon : String
What phenomenon this illustrates

Instances For

def Phenomena.Constructions.Resultatives.instReprResultativeDatum.repr :

ResultativeDatum → Nat → Std.Format

Equations

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

Instances For

instance Phenomena.Constructions.Resultatives.instReprResultativeDatum :

Repr ResultativeDatum

Equations

Phenomena.Constructions.Resultatives.instReprResultativeDatum = { reprPrec := Phenomena.Constructions.Resultatives.instReprResultativeDatum.repr }

instance Phenomena.Constructions.Resultatives.instBEqResultativeDatum :

BEq ResultativeDatum

Equations

Phenomena.Constructions.Resultatives.instBEqResultativeDatum = { beq := Phenomena.Constructions.Resultatives.instBEqResultativeDatum.beq }

def Phenomena.Constructions.Resultatives.instBEqResultativeDatum.beq :

ResultativeDatum → ResultativeDatum → Bool

Equations

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

Instances For

1. Causative property resultatives (§2, Table 1) #

def Phenomena.Constructions.Resultatives.hammer_flat :

ResultativeDatum

Equations

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

Instances For

def Phenomena.Constructions.Resultatives.wipe_clean :

ResultativeDatum

Equations

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

Instances For

def Phenomena.Constructions.Resultatives.paint_red :

ResultativeDatum

Equations

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

Instances For

2. Causative path resultatives (§2, Table 1) #

def Phenomena.Constructions.Resultatives.kick_into_field :

ResultativeDatum

Equations

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

Instances For

def Phenomena.Constructions.Resultatives.push_off_table :

ResultativeDatum

Equations

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

Instances For

3. Noncausative property resultatives (§2, Table 1) #

def Phenomena.Constructions.Resultatives.freeze_solid :

ResultativeDatum

Equations

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

Instances For

def Phenomena.Constructions.Resultatives.swing_shut :

ResultativeDatum

Equations

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

Instances For

4. Noncausative path resultatives (§2, Table 1) #

def Phenomena.Constructions.Resultatives.roll_into_field :

ResultativeDatum

Equations

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

Instances For

def Phenomena.Constructions.Resultatives.slide_off_table :

ResultativeDatum

Equations

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

Instances For

5. Fake reflexive resultatives (§5) #

def Phenomena.Constructions.Resultatives.laugh_silly :

ResultativeDatum

Equations

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

Instances For

def Phenomena.Constructions.Resultatives.drink_sick :

ResultativeDatum

Equations

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

Instances For

def Phenomena.Constructions.Resultatives.run_ragged :

ResultativeDatum

Equations

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

Instances For

6. Aspectual contrasts (§4, Principle 27) #

Resultatives are telic: they accept in-adverbials and reject for-adverbials. Bare activity verbs are atelic: they accept for and reject in.

structure Phenomena.Constructions.Resultatives.AspectualContrast :

An aspectual contrast pair.

sentence : String
Sentence with temporal adverbial
judgment : Core.Empirical.Acceptability
Acceptability
adverbialType : String
Which adverbial type
description : String
Description

Instances For

def Phenomena.Constructions.Resultatives.instReprAspectualContrast.repr :

AspectualContrast → Nat → Std.Format

Equations

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

Instances For

instance Phenomena.Constructions.Resultatives.instReprAspectualContrast :

Repr AspectualContrast

Equations

Phenomena.Constructions.Resultatives.instReprAspectualContrast = { reprPrec := Phenomena.Constructions.Resultatives.instReprAspectualContrast.repr }

def Phenomena.Constructions.Resultatives.instBEqAspectualContrast.beq :

AspectualContrast → AspectualContrast → Bool

Equations

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

Instances For

instance Phenomena.Constructions.Resultatives.instBEqAspectualContrast :

BEq AspectualContrast

Equations

Phenomena.Constructions.Resultatives.instBEqAspectualContrast = { beq := Phenomena.Constructions.Resultatives.instBEqAspectualContrast.beq }

def Phenomena.Constructions.Resultatives.hammer_flat_in :

AspectualContrast

Equations

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

Instances For

def Phenomena.Constructions.Resultatives.hammer_flat_for :

AspectualContrast

Equations

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

Instances For

def Phenomena.Constructions.Resultatives.hammer_bare_for :

AspectualContrast

Equations

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

Instances For

def Phenomena.Constructions.Resultatives.hammer_bare_in :

AspectualContrast

Equations

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

Instances For

7. Unacceptable resultatives (§6, semantic coherence violations) #

def Phenomena.Constructions.Resultatives.eat_full :

ResultativeDatum

Equations

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

Instances For

def Phenomena.Constructions.Resultatives.sleep_flat :

ResultativeDatum

Equations

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

Instances For

All data #

def Phenomena.Constructions.Resultatives.allExamples :

List ResultativeDatum

Equations

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

Instances For

def Phenomena.Constructions.Resultatives.aspectualContrasts :

List AspectualContrast

Equations

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

Instances For

Verification theorems #

theorem Phenomena.Constructions.Resultatives.has_all_resultative_types :

(allExamples.any fun (x : ResultativeDatum) => x.resType == ResultativeType.causativeProperty) = true ∧ (allExamples.any fun (x : ResultativeDatum) => x.resType == ResultativeType.causativePath) = true ∧ (allExamples.any fun (x : ResultativeDatum) => x.resType == ResultativeType.noncausativeProperty) = true ∧ (allExamples.any fun (x : ResultativeDatum) => x.resType == ResultativeType.noncausativePath) = true ∧ (allExamples.any fun (x : ResultativeDatum) => x.resType == ResultativeType.fakeReflexive) = true

All four resultative types are attested in the data.

theorem Phenomena.Constructions.Resultatives.has_both_judgments :

(allExamples.any fun (x : ResultativeDatum) => x.judgment == Core.Empirical.Acceptability.ok) = true ∧ (allExamples.any fun (x : ResultativeDatum) => x.judgment == Core.Empirical.Acceptability.unacceptable) = true

Both grammatical and ungrammatical examples are represented.

theorem Phenomena.Constructions.Resultatives.aspectual_both_adverbials :

(aspectualContrasts.any fun (x : AspectualContrast) => x.adverbialType == "in-adverbial") = true ∧ (aspectualContrasts.any fun (x : AspectualContrast) => x.adverbialType == "for-adverbial") = true

The aspectual contrast data includes both in- and for-adverbials.

theorem Phenomena.Constructions.Resultatives.telic_adverbial_pattern :

(hammer_flat_in.judgment == Core.Empirical.Acceptability.ok) = true ∧ (hammer_flat_for.judgment == Core.Empirical.Acceptability.unacceptable) = true

Telic resultatives accept in-adverbials and reject for-adverbials.

theorem Phenomena.Constructions.Resultatives.atelic_adverbial_pattern :

(hammer_bare_for.judgment == Core.Empirical.Acceptability.ok) = true

Atelic bare activities accept for-adverbials.