Cross-Theory Comparison: Resultative Argument Licensing

Three syntactic theories predict the same argument frames for resultatives but differ on how arguments are licensed. This module formalizes the convergence and divergence.

Theories compared

1. Minimalism: Theta Criterion — each theta role assigned to exactly one argument
2. CxG: FAR + Semantic Coherence — verb and construction args fuse when coherent
3. DG: Valency satisfaction — verb's argument structure must be fully saturated

Key result

All three theories predict the same surface argument frame for canonical resultatives like "She hammered the metal flat". They diverge on fake reflexives ("She laughed herself silly") where CxG handles the extra argument via construction-licensed roles while Minimalism requires special mechanisms.

§1. Three theories of argument licensing

inductive Phenomena.ArgumentStructure.Studies.TheoryComparison.ArgRole : Type

Semantic role label (theory-neutral).

• agent : ArgRole
• patient : ArgRole
• theme : ArgRole
• resultState : ArgRole
• path : ArgRole

instance Phenomena.ArgumentStructure.Studies.TheoryComparison.instReprArgRole : Repr ArgRole

Equations

• Phenomena.ArgumentStructure.Studies.TheoryComparison.instReprArgRole = { reprPrec := Phenomena.ArgumentStructure.Studies.TheoryComparison.instReprArgRole.repr }

def Phenomena.ArgumentStructure.Studies.TheoryComparison.instReprArgRole.repr : ArgRole → ℕ → Std.Format

Equations

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

instance Phenomena.ArgumentStructure.Studies.TheoryComparison.instDecidableEqArgRole : DecidableEq ArgRole

Equations

• Phenomena.ArgumentStructure.Studies.TheoryComparison.instDecidableEqArgRole x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.ArgumentStructure.Studies.TheoryComparison.instBEqArgRole : BEq ArgRole

Equations

• Phenomena.ArgumentStructure.Studies.TheoryComparison.instBEqArgRole = { beq := Phenomena.ArgumentStructure.Studies.TheoryComparison.instBEqArgRole.beq }

def Phenomena.ArgumentStructure.Studies.TheoryComparison.instBEqArgRole.beq : ArgRole → ArgRole → Bool

Equations

• Phenomena.ArgumentStructure.Studies.TheoryComparison.instBEqArgRole.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[reducible, inline]

abbrev Phenomena.ArgumentStructure.Studies.TheoryComparison.ArgFrame : Type

A predicted argument frame: ordered list of roles.

Equations

• Phenomena.ArgumentStructure.Studies.TheoryComparison.ArgFrame = List Phenomena.ArgumentStructure.Studies.TheoryComparison.ArgRole

Minimalist argument licensing

In Minimalism, theta roles drive External Merge. Each theta role must be assigned to exactly one argument (Theta Criterion).

def Phenomena.ArgumentStructure.Studies.TheoryComparison.minimalistFrame (roles : ArgFrame) : List Minimalism.MergeTrigger

Minimalist licensing: each theta role in the frame triggers External Merge via MergeTrigger.theta.

Equations

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

def Phenomena.ArgumentStructure.Studies.TheoryComparison.thetaCriterionSatisfied (frame : ArgFrame) : Bool

The theta criterion requires 1-to-1 mapping between roles and arguments. This is satisfied iff no duplicate roles appear.

Equations

• Phenomena.ArgumentStructure.Studies.TheoryComparison.thetaCriterionSatisfied frame = ((List.eraseDups frame).length == List.length frame)

CxG argument licensing

In CxG, both the verb and the construction contribute argument roles. Shared roles fuse (FAR); fusion requires semantic coherence.

structure Phenomena.ArgumentStructure.Studies.TheoryComparison.CxGFrame : Type

CxG frame: verb roles + construction roles, with fusion information.

• verbRoles : List ArgRole

  Roles contributed by the verb

• constructionRoles : List ArgRole

  Roles contributed by the construction

• fusedPairs : List (ArgRole × ArgRole)

  Which role pairs are fused

def Phenomena.ArgumentStructure.Studies.TheoryComparison.instReprCxGFrame.repr : CxGFrame → ℕ → Std.Format

Equations

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

instance Phenomena.ArgumentStructure.Studies.TheoryComparison.instReprCxGFrame : Repr CxGFrame

Equations

• Phenomena.ArgumentStructure.Studies.TheoryComparison.instReprCxGFrame = { reprPrec := Phenomena.ArgumentStructure.Studies.TheoryComparison.instReprCxGFrame.repr }

def Phenomena.ArgumentStructure.Studies.TheoryComparison.instBEqCxGFrame.beq : CxGFrame → CxGFrame → Bool

Equations

• One or more equations did not get rendered due to their size.
• Phenomena.ArgumentStructure.Studies.TheoryComparison.instBEqCxGFrame.beq x✝¹ x✝ = false

instance Phenomena.ArgumentStructure.Studies.TheoryComparison.instBEqCxGFrame : BEq CxGFrame

Equations

• Phenomena.ArgumentStructure.Studies.TheoryComparison.instBEqCxGFrame = { beq := Phenomena.ArgumentStructure.Studies.TheoryComparison.instBEqCxGFrame.beq }

def Phenomena.ArgumentStructure.Studies.TheoryComparison.CxGFrame.surfaceFrame (f : CxGFrame) : ArgFrame

The surface frame after fusion: construction roles with fused roles counted once.

Equations

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

def Phenomena.ArgumentStructure.Studies.TheoryComparison.CxGFrame.farSatisfied (f : CxGFrame) : Bool

Check FAR: all verb roles and all construction roles are realized.

Equations

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

def Phenomena.ArgumentStructure.Studies.TheoryComparison.CxGFrame.coherent (f : CxGFrame) : Bool

Check semantic coherence for all fused pairs.

Equations

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

DG argument licensing

In DG, the verb has a valency frame specifying required dependents. The resultative construction adds additional dependent slots.

structure Phenomena.ArgumentStructure.Studies.TheoryComparison.DGFrame : Type

DG frame: verb's base valency + construction-added deps.

• verbArgs : List DepGrammar.ArgSlot

  Verb's inherent argument requirements

• constructionArgs : List DepGrammar.ArgSlot

  Arguments added by the resultative construction

def Phenomena.ArgumentStructure.Studies.TheoryComparison.instReprDGFrame.repr : DGFrame → ℕ → Std.Format

Equations

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

instance Phenomena.ArgumentStructure.Studies.TheoryComparison.instReprDGFrame : Repr DGFrame

Equations

• Phenomena.ArgumentStructure.Studies.TheoryComparison.instReprDGFrame = { reprPrec := Phenomena.ArgumentStructure.Studies.TheoryComparison.instReprDGFrame.repr }

def Phenomena.ArgumentStructure.Studies.TheoryComparison.DGFrame.allArgs (f : DGFrame) : List DepGrammar.ArgSlot

The combined DG argument frame.

Equations

• f.allArgs = f.verbArgs ++ f.constructionArgs

§2. Convergence on canonical resultatives

All three theories predict the same argument frame for "She hammered the metal flat": [Agent, Patient, ResultState].

def Phenomena.ArgumentStructure.Studies.TheoryComparison.minimalist_hammer_flat : ArgFrame

Minimalist prediction for "hammer the metal flat".

Equations

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

def Phenomena.ArgumentStructure.Studies.TheoryComparison.cxg_hammer_flat : CxGFrame

CxG prediction for "hammer the metal flat".

Verb "hammer" contributes {agent, patient}. Construction contributes {agent, patient, resultState}. Agent fuses with agent; patient fuses with patient.

Equations

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

def Phenomena.ArgumentStructure.Studies.TheoryComparison.dg_hammer_flat : DGFrame

DG prediction for "hammer the metal flat".

Verb "hammer" has valency {subj, obj}. Resultative construction adds {result-complement}.

Equations

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

theorem Phenomena.ArgumentStructure.Studies.TheoryComparison.convergence_hammer_flat_arg_count : List.length minimalist_hammer_flat = 3 ∧ List.length cxg_hammer_flat.surfaceFrame = 3 ∧ dg_hammer_flat.allArgs.length = 3

All three theories predict the same number of surface arguments for "hammer flat": 3 (agent + patient + result).

theorem Phenomena.ArgumentStructure.Studies.TheoryComparison.theta_criterion_canonical : thetaCriterionSatisfied minimalist_hammer_flat = true

The theta criterion is satisfied for the canonical resultative.

theorem Phenomena.ArgumentStructure.Studies.TheoryComparison.far_canonical : cxg_hammer_flat.farSatisfied = true

FAR is satisfied for the canonical CxG resultative.

§3. Divergence on fake reflexives

"She laughed herself silly" reveals the key difference between the theories.

• CxG: "laugh" contributes {agent}; construction contributes {agent, patient, resultState}; agent fuses; "herself" fills the CONSTRUCTION's patient (not the verb's).
• Minimalism: "laugh" is intransitive (assigns only one theta role); "herself" needs a theta role but the verb can't provide one.
• DG: "laugh" has valency {subj}; "herself" is an argument added by the construction, not by the verb's subcategorization frame.

def Phenomena.ArgumentStructure.Studies.TheoryComparison.cxg_laugh_silly : CxGFrame

CxG analysis of "She laughed herself silly".

The verb "laugh" is intransitive: only {agent}. The construction adds {patient, resultState}. Only agent fuses. "Herself" is the construction's patient.

Equations

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

def Phenomena.ArgumentStructure.Studies.TheoryComparison.minimalist_laugh_silly_verb_roles : ArgFrame

Minimalist analysis of "She laughed herself silly".

"laugh" assigns only one theta role (agent to subject). "herself" needs a theta role, but the verb doesn't provide one. The extra role must come from somewhere — requiring special mechanisms (e.g., the small clause assigns a role).

Equations

• Phenomena.ArgumentStructure.Studies.TheoryComparison.minimalist_laugh_silly_verb_roles = [Phenomena.ArgumentStructure.Studies.TheoryComparison.ArgRole.agent]

def Phenomena.ArgumentStructure.Studies.TheoryComparison.minimalist_laugh_silly_full : ArgFrame

Equations

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

def Phenomena.ArgumentStructure.Studies.TheoryComparison.dg_laugh_silly : DGFrame

DG analysis of "She laughed herself silly".

"laugh" has valency {subj} only. The resultative construction adds {obj, result-complement}.

Equations

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

theorem Phenomena.ArgumentStructure.Studies.TheoryComparison.cxg_construction_adds_patient : cxg_laugh_silly.verbRoles.length < List.length cxg_laugh_silly.surfaceFrame

CxG: the verb contributes fewer roles than the surface frame. The construction licenses the extra argument ("herself").

theorem Phenomena.ArgumentStructure.Studies.TheoryComparison.cxg_fake_reflexive_far : cxg_laugh_silly.farSatisfied = true

CxG handles fake reflexives without stipulation: the construction adds the patient role, and the verb's agent fuses with the construction's agent. FAR is satisfied.

theorem Phenomena.ArgumentStructure.Studies.TheoryComparison.minimalist_verb_deficit : List.length minimalist_laugh_silly_verb_roles < List.length minimalist_laugh_silly_full

The Minimalist verb alone cannot license the reflexive: the verb has only 1 theta role but the surface has 3 arguments.

This is the core divergence: CxG's FAR allows the construction to add roles, while the theta criterion requires the verb to provide them.

theorem Phenomena.ArgumentStructure.Studies.TheoryComparison.dg_construction_adds_args : dg_laugh_silly.verbArgs.length = 1 ∧ dg_laugh_silly.constructionArgs.length = 2

DG: the construction adds 2 arguments to the verb's base valency of 1.

theorem Phenomena.ArgumentStructure.Studies.TheoryComparison.convergence_fake_reflexive_count : List.length minimalist_laugh_silly_full = 3 ∧ List.length cxg_laugh_silly.surfaceFrame = 3 ∧ dg_laugh_silly.allArgs.length = 3

Despite the different licensing mechanisms, all three theories predict the same surface argument count for the fake reflexive: 3.

§4. Semantic Coherence generalizes the Theta Criterion

The Theta Criterion is the special case of FAR + Semantic Coherence where the verb and construction have identical role sets (i.e., every role fuses).

When the sets differ (as in fake reflexives), CxG's system is more general: it allows the construction to ADD roles the verb lacks.

theorem Phenomena.ArgumentStructure.Studies.TheoryComparison.theta_criterion_is_full_fusion (roles : ArgFrame) : thetaCriterionSatisfied roles = true → (List.eraseDups roles).length = List.length roles

The theta criterion requires a 1-to-1 mapping between roles and arguments. This is equivalent to FAR when verb roles = construction roles (all roles fuse, no construction-only roles).

theorem Phenomena.ArgumentStructure.Studies.TheoryComparison.semanticCoherenceGeneralizesTheta : cxg_laugh_silly.farSatisfied = true ∧ cxg_laugh_silly.verbRoles.length < List.length cxg_laugh_silly.surfaceFrame

CxG's system is strictly more general: it handles cases where verb roles ⊂ construction roles (fake reflexives). The theta criterion alone cannot handle this without extra machinery.

Formally: there exists a CxG frame where FAR is satisfied but the verb alone does not provide enough theta roles.

Summary

Theory	Canonical ("hammer flat")	Fake reflexive ("laugh silly")
Minimalism	Theta assigns 3 roles	Verb has only 1 role → deficit
CxG	Verb + construction fuse	Construction adds patient
DG	Verb + construction deps	Construction adds obj + compl

All three predict the same surface frame [Agent, V, Patient, Result], but CxG handles argument augmentation via construction-licensed roles while Minimalism requires special mechanisms for fake reflexives.