Linking Theory Interface

@cite{beavers-koontz-garboden-2020} @cite{dowty-1991} @cite{goldberg-1995} @cite{kratzer-1996} @cite{levin-2004} @cite{levin-hovav-1995} @cite{pesetsky-1995} @cite{pylkknen-2008} @cite{rappaport-hovav-levin-1998}

General interface for theories of argument realization — how verbs' arguments get their thematic roles.

Theta Roles

Theta roles are derived convenience labels that name clusters in entailment-profile space (EntailmentProfile.lean). They are NOT primitives: the authoritative representation of argument semantics is the entailment profile, and role labels are computed from it via EntailmentProfile.toRole.

The field consensus (@cite{levin-2019}) is that discrete thematic roles have been superseded by entailment-based representations. Role labels remain useful as a shared interface vocabulary for linking theories, neo-Davidsonian logical forms, and cross-framework comparison.

Linking Theories

Theories in the literature differ along three dimensions:

1. What the verb contributes (lexical semantics, meaning components, event structure templates, root meaning, entailment profiles)
2. What the structure contributes (Voice flavor, applicative type, sub-event decomposition, construction type, causal chain position)
3. Which direction the mapping goes (verb → role, structure → role, or both jointly)

The LinkingTheory structure captures this variation by parameterizing over BOTH the verb representation type (Verb) and the structural context type (Ctx). Theories that ignore structure use Unit for Ctx; theories that care about Voice use VoiceFlavor; theories with richer decompositions bring their own types.

The role output is always ThetaRole — the shared vocabulary that makes theories comparable against fragment data.

The compatible field captures gradient verb–construction pairing: a verb may be compatible with multiple structural contexts (causative alternation verbs appear with both agentive and non-thematic Voice). Singleton lists express categorical predictions; multi-element lists express gradient compatibility.

Coverage

Accounts expressible via this interface (non-exhaustive):

Account	Ctx	compatible	predict uses verb?
Severing	VoiceFlavor	verb-constrained	no
Lexicalist	Unit	always []	yes
Zero morphology	(custom)	verb-constrained	yes
First Phase Syntax	(custom)	verb-constrained	yes
CxG	(custom)	broad	no
Proto-roles	Unit	always []	yes (via ASP)
Applicatives	(custom)	verb-constrained	no

inductive ThetaRole : Type

Theta roles — derived convenience labels that name clusters in entailment-profile space. These are NOT primitives: the authoritative representation is the EntailmentProfile, and role labels are computed from it via EntailmentProfile.toRole.

The field consensus (@cite{levin-2019}) is that discrete thematic roles have been superseded by entailment-based representations. Role labels remain useful as shared interface vocabulary for linking theories, neo-Davidsonian logical forms, and cross-framework comparison.

• agent : ThetaRole
• patient : ThetaRole
• theme : ThetaRole
• experiencer : ThetaRole
• goal : ThetaRole
• source : ThetaRole
• instrument : ThetaRole
• stimulus : ThetaRole

instance instDecidableEqThetaRole : DecidableEq ThetaRole

Equations

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

def instReprThetaRole.repr : ThetaRole → Nat → Std.Format

Equations

• instReprThetaRole.repr ThetaRole.agent prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ThetaRole.agent")).group prec✝
• instReprThetaRole.repr ThetaRole.patient prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ThetaRole.patient")).group prec✝
• instReprThetaRole.repr ThetaRole.theme prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ThetaRole.theme")).group prec✝
• instReprThetaRole.repr ThetaRole.experiencer prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ThetaRole.experiencer")).group prec✝
• instReprThetaRole.repr ThetaRole.goal prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ThetaRole.goal")).group prec✝
• instReprThetaRole.repr ThetaRole.source prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ThetaRole.source")).group prec✝
• instReprThetaRole.repr ThetaRole.instrument prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ThetaRole.instrument")).group prec✝
• instReprThetaRole.repr ThetaRole.stimulus prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ThetaRole.stimulus")).group prec✝

instance instReprThetaRole : Repr ThetaRole

Equations

• instReprThetaRole = { reprPrec := instReprThetaRole.repr }

instance instBEqThetaRole : BEq ThetaRole

Equations

• instBEqThetaRole = { beq := instBEqThetaRole.beq }

def instBEqThetaRole.beq : ThetaRole → ThetaRole → Bool

Equations

• instBEqThetaRole.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Semantics.Lexical.Verb.EntailmentProfile.EntailmentProfile.toRole (p : EntailmentProfile) : Option ThetaRole

Derive a convenience theta-role label from an entailment profile.

This is the canonical direction: profiles are authoritative, labels are derived. The function uses feature-based heuristics to assign the most natural label:

• Volition → agent
• Sentience without causation → experiencer
• Causation without sentience → stimulus
• P-Patient features without P-Agent → patient (if CoS) or theme
• IE only → goal (ambiguous with source)
• No distinguishing features → none

Note: instrument and stimulus have identical canonical profiles ({causation, IE}), as do goal and source ({IE}). The function defaults to stimulus and goal respectively. Disambiguation requires external context (e.g., VerbCore.causalSource).

Equations

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

def ThetaRole.canonicalProfile : ThetaRole → Semantics.Lexical.Verb.EntailmentProfile.EntailmentProfile

Map each ThetaRole label back to its canonical entailment profile.

This is the inverse direction — from convenience labels to the underlying entailment structure. Each label names a prototypical combination of entailments.

Round-trip: toRole (canonicalProfile θ) = some θ' where θ' is the canonical representative. Note that instrument→stimulus and source→goal collapse because their canonical profiles are identical.

Equations

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

theorem toRole_canonical_agent : ThetaRole.agent.canonicalProfile.toRole = some ThetaRole.agent

Agent survives round-trip.

theorem toRole_canonical_patient : ThetaRole.patient.canonicalProfile.toRole = some ThetaRole.patient

Patient survives round-trip.

theorem toRole_canonical_theme : ThetaRole.theme.canonicalProfile.toRole = some ThetaRole.theme

Theme survives round-trip.

theorem toRole_canonical_experiencer : ThetaRole.experiencer.canonicalProfile.toRole = some ThetaRole.experiencer

Experiencer survives round-trip.

theorem toRole_canonical_stimulus : ThetaRole.stimulus.canonicalProfile.toRole = some ThetaRole.stimulus

Stimulus survives round-trip.

theorem toRole_canonical_goal : ThetaRole.goal.canonicalProfile.toRole = some ThetaRole.goal

Goal survives round-trip.

theorem toRole_canonical_instrument : ThetaRole.instrument.canonicalProfile.toRole = some ThetaRole.stimulus

Instrument collapses to stimulus (identical profiles: {C, IE}).

theorem toRole_canonical_source : ThetaRole.source.canonicalProfile.toRole = some ThetaRole.goal

Source collapses to goal (identical profiles: {IE}).

theorem kick_subject_toRole : Semantics.Lexical.Verb.EntailmentProfile.kickSubjectProfile.toRole = some ThetaRole.agent

"kick" subject profile → agent.

theorem kick_object_toRole : Semantics.Lexical.Verb.EntailmentProfile.kickObjectProfile.toRole = some ThetaRole.patient

"kick" object profile → patient.

theorem see_subject_toRole : Semantics.Lexical.Verb.EntailmentProfile.seeSubjectProfile.toRole = some ThetaRole.experiencer

"see" subject profile → experiencer.

theorem arrive_subject_toRole : Semantics.Lexical.Verb.EntailmentProfile.arriveSubjectProfile.toRole = none

"arrive" subject profile → none (mixed P-Agent + P-Patient: movement disqualifies).

theorem die_subject_toRole : Semantics.Lexical.Verb.EntailmentProfile.dieSubjectProfile.toRole = some ThetaRole.patient

"die" subject profile → patient (pure P-Patient).

theorem agent_outranks_patient : Semantics.Lexical.Verb.EntailmentProfile.outranksForSubject ThetaRole.agent.canonicalProfile ThetaRole.patient.canonicalProfile = true

Agent outranks patient for subjecthood (lattice: {V,S,C,M,IE} ⊃ {}).

theorem agent_outranks_instrument : Semantics.Lexical.Verb.EntailmentProfile.outranksForSubject ThetaRole.agent.canonicalProfile ThetaRole.instrument.canonicalProfile = true

Agent outranks instrument (lattice: {V,S,C,M,IE} ⊃ {C,IE}).

theorem agent_outranks_experiencer : Semantics.Lexical.Verb.EntailmentProfile.outranksForSubject ThetaRole.agent.canonicalProfile ThetaRole.experiencer.canonicalProfile = true

Agent outranks experiencer (lattice: {V,S,C,M,IE} ⊃ {S,IE}).

theorem experiencer_instrument_alternation : Semantics.Lexical.Verb.EntailmentProfile.allowsAlternation ThetaRole.experiencer.canonicalProfile ThetaRole.instrument.canonicalProfile = true

Experiencer and instrument have incomparable P-Agent sets ({S,IE} ⊥ {C,IE}), but also equal P-Patient (both 0) → alternation predicted.

theorem experiencer_stimulus_alternation : Semantics.Lexical.Verb.EntailmentProfile.allowsAlternation ThetaRole.experiencer.canonicalProfile ThetaRole.stimulus.canonicalProfile = true

Experiencer and stimulus have equal profiles → alternation (like/please).

theorem agent_pAgent_score : ThetaRole.agent.canonicalProfile.pAgentScore = 5

theorem patient_pAgent_score : ThetaRole.patient.canonicalProfile.pAgentScore = 0

theorem agent_pPatient_score : ThetaRole.agent.canonicalProfile.pPatientScore = 0

theorem patient_pPatient_score : ThetaRole.patient.canonicalProfile.pPatientScore = 3

theorem canonical_agent_wellformed : ThetaRole.agent.canonicalProfile.wellFormedInternal = true

theorem canonical_experiencer_wellformed : ThetaRole.experiencer.canonicalProfile.wellFormedInternal = true

theorem canonical_patient_wellformed : ThetaRole.patient.canonicalProfile.wellFormedInternal = true

inductive Interfaces.SyntaxSemantics.ArgPosition : Type

Which argument position in the clause we're asking about. Theory-neutral: expressed as grammatical functions, not structural positions (Spec-vP, Comp-VP, etc.), so that theories with different structural vocabularies can all target the same output.

• subject : ArgPosition
• directObject : ArgPosition
• indirectObject : ArgPosition
• oblique : ArgPosition
• applied : ArgPosition

instance Interfaces.SyntaxSemantics.instDecidableEqArgPosition : DecidableEq ArgPosition

Equations

• Interfaces.SyntaxSemantics.instDecidableEqArgPosition x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Interfaces.SyntaxSemantics.instBEqArgPosition.beq : ArgPosition → ArgPosition → Bool

Equations

• Interfaces.SyntaxSemantics.instBEqArgPosition.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Interfaces.SyntaxSemantics.instBEqArgPosition : BEq ArgPosition

Equations

• Interfaces.SyntaxSemantics.instBEqArgPosition = { beq := Interfaces.SyntaxSemantics.instBEqArgPosition.beq }

def Interfaces.SyntaxSemantics.instReprArgPosition.repr : ArgPosition → Nat → Std.Format

Equations

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

instance Interfaces.SyntaxSemantics.instReprArgPosition : Repr ArgPosition

Equations

• Interfaces.SyntaxSemantics.instReprArgPosition = { reprPrec := Interfaces.SyntaxSemantics.instReprArgPosition.repr }

structure Interfaces.SyntaxSemantics.LinkingTheory (Verb Ctx : Type) : Type

A linking theory, parameterized by verb representation and structural context type.

• Verb: what the theory needs to know about the verb. Typically VerbCore, but could be EntailmentProfile (Dowty) or EventTemplate (Rappaport Hovav & Levin).
• Ctx: what the theory considers relevant about the syntactic structure beyond the verb itself:
  • Unit for theories that derive everything from the verb
  • VoiceFlavor for the severing account
  • A richer type for Ramchand, Goldberg, Pylkkänen, etc.

The theory provides two functions:

• compatible: which structural contexts can this verb appear in?
• predict: in a given context, what theta role does each position get?

This separation captures the key theoretical distinction:

• Pure constructional (Borer, strong Goldberg): compatible is broad — the verb is promiscuous; structure determines roles
• Pure lexicalist (Levin): compatible always returns [] — there is nothing structural to vary
• Hybrid: compatible returns a verb-constrained subset — gradient compatibility

• compatible : Verb → List Ctx

  Which structural contexts this verb is compatible with. Singleton = categorical. Multiple = gradient (alternation).

• predict : Verb → Ctx → ArgPosition → Option ThetaRole

  Predict each argument's theta role in a given context. Returns none for positions the theory is silent about.

def Interfaces.SyntaxSemantics.LinkingTheory.matchesAt {Verb Ctx : Type} [BEq Ctx] (th : LinkingTheory Verb Ctx) (v : Verb) (pos : ArgPosition) (actual : Option ThetaRole) : Bool

Does the theory's prediction match the observed role at a given position, for at least one compatible structural context?

For alternation verbs (multiple compatible contexts), the test passes if ANY context produces the correct prediction — the fragment entry records one use of the verb, not all possible uses.

Equations

• th.matchesAt v pos actual = (th.compatible v).any fun (ctx : Ctx) => th.predict v ctx pos == actual