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 TheoryComparison.ArgRole : Type

Semantic role label (theory-neutral).

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

def TheoryComparison.instReprArgRole.repr : ArgRole → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance TheoryComparison.instReprArgRole : Repr ArgRole

Equations

• TheoryComparison.instReprArgRole = { reprPrec := TheoryComparison.instReprArgRole.repr }

@[implicit_reducible]

instance TheoryComparison.instDecidableEqArgRole : DecidableEq ArgRole

Equations

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

@[reducible, inline]

abbrev TheoryComparison.ArgFrame : Type

A predicted argument frame: ordered list of roles.

Equations

• TheoryComparison.ArgFrame = List TheoryComparison.ArgRole

Minimalist argument licensing

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

inductive TheoryComparison.MergeTrigger : Type

What triggers Merge? In Minimalism, uninterpretable features drive operations. Used here as a descriptive enum for the comparison study; not part of the M-C-B substrate (M-C-B's Merge action is feature-driven via the coproduct, not via discrete triggers).

• selection : Minimalist.Cat → MergeTrigger
• epp : MergeTrigger
• theta : MergeTrigger

def TheoryComparison.instReprMergeTrigger.repr : MergeTrigger → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance TheoryComparison.instReprMergeTrigger : Repr MergeTrigger

Equations

• TheoryComparison.instReprMergeTrigger = { reprPrec := TheoryComparison.instReprMergeTrigger.repr }

def TheoryComparison.instDecidableEqMergeTrigger.decEq (x✝ x✝¹ : MergeTrigger) : Decidable (x✝ = x✝¹)

Equations

• TheoryComparison.instDecidableEqMergeTrigger.decEq (TheoryComparison.MergeTrigger.selection a) (TheoryComparison.MergeTrigger.selection b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• TheoryComparison.instDecidableEqMergeTrigger.decEq (TheoryComparison.MergeTrigger.selection a) TheoryComparison.MergeTrigger.epp = isFalse ⋯
• TheoryComparison.instDecidableEqMergeTrigger.decEq (TheoryComparison.MergeTrigger.selection a) TheoryComparison.MergeTrigger.theta = isFalse ⋯
• TheoryComparison.instDecidableEqMergeTrigger.decEq TheoryComparison.MergeTrigger.epp (TheoryComparison.MergeTrigger.selection a) = isFalse ⋯
• TheoryComparison.instDecidableEqMergeTrigger.decEq TheoryComparison.MergeTrigger.epp TheoryComparison.MergeTrigger.epp = isTrue ⋯
• TheoryComparison.instDecidableEqMergeTrigger.decEq TheoryComparison.MergeTrigger.epp TheoryComparison.MergeTrigger.theta = isFalse TheoryComparison.instDecidableEqMergeTrigger.decEq._proof_6
• TheoryComparison.instDecidableEqMergeTrigger.decEq TheoryComparison.MergeTrigger.theta (TheoryComparison.MergeTrigger.selection a) = isFalse ⋯
• TheoryComparison.instDecidableEqMergeTrigger.decEq TheoryComparison.MergeTrigger.theta TheoryComparison.MergeTrigger.epp = isFalse TheoryComparison.instDecidableEqMergeTrigger.decEq._proof_8
• TheoryComparison.instDecidableEqMergeTrigger.decEq TheoryComparison.MergeTrigger.theta TheoryComparison.MergeTrigger.theta = isTrue ⋯

@[implicit_reducible]

instance TheoryComparison.instDecidableEqMergeTrigger : DecidableEq MergeTrigger

Equations

• TheoryComparison.instDecidableEqMergeTrigger = TheoryComparison.instDecidableEqMergeTrigger.decEq

def TheoryComparison.minimalistFrame (roles : ArgFrame) : List MergeTrigger

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

Equations

• TheoryComparison.minimalistFrame roles = List.map (fun (x : TheoryComparison.ArgRole) => TheoryComparison.MergeTrigger.theta) roles

def 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

• 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 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

@[implicit_reducible]

instance TheoryComparison.instReprCxGFrame : Repr CxGFrame

Equations

• TheoryComparison.instReprCxGFrame = { reprPrec := TheoryComparison.instReprCxGFrame.repr }

def TheoryComparison.instReprCxGFrame.repr : CxGFrame → ℕ → Std.Format

Equations

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

def TheoryComparison.instBEqCxGFrame.beq : CxGFrame → CxGFrame → Bool

Equations

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

@[implicit_reducible]

instance TheoryComparison.instBEqCxGFrame : BEq CxGFrame

Equations

• TheoryComparison.instBEqCxGFrame = { beq := TheoryComparison.instBEqCxGFrame.beq }

def 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 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 TheoryComparison.CxGFrame.coherent (f : CxGFrame) : Bool

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 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 TheoryComparison.instReprDGFrame.repr : DGFrame → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance TheoryComparison.instReprDGFrame : Repr DGFrame

Equations

• TheoryComparison.instReprDGFrame = { reprPrec := TheoryComparison.instReprDGFrame.repr }

def 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 TheoryComparison.minimalist_hammer_flat : ArgFrame

Minimalist prediction for "hammer the metal flat".

Equations

• TheoryComparison.minimalist_hammer_flat = [TheoryComparison.ArgRole.agent, TheoryComparison.ArgRole.patient, TheoryComparison.ArgRole.resultState]

def 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 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 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 TheoryComparison.theta_criterion_canonical : thetaCriterionSatisfied minimalist_hammer_flat = true

The theta criterion is satisfied for the canonical resultative.

theorem 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 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 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

• TheoryComparison.minimalist_laugh_silly_verb_roles = [TheoryComparison.ArgRole.agent]

def TheoryComparison.minimalist_laugh_silly_full : ArgFrame

Equations

• TheoryComparison.minimalist_laugh_silly_full = [TheoryComparison.ArgRole.agent, TheoryComparison.ArgRole.patient, TheoryComparison.ArgRole.resultState]

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