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{pylkkanen-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

@[implicit_reducible]

instance instDecidableEqThetaRole : DecidableEq ThetaRole

Equations

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

@[implicit_reducible]

instance instReprThetaRole : Repr ThetaRole

Equations

• instReprThetaRole = { reprPrec := instReprThetaRole.repr }

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✝

def Semantics.ArgumentStructure.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.ArgumentStructure.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 instrument_stimulus_same_profile : ThetaRole.instrument.canonicalProfile = ThetaRole.stimulus.canonicalProfile

Instrument and stimulus have identical canonical profiles — both are {causation, independentExistence}. toRole cannot distinguish them.

theorem goal_source_same_profile : ThetaRole.goal.canonicalProfile = ThetaRole.source.canonicalProfile

Goal and source have identical canonical profiles — both are {independentExistence} only. toRole cannot distinguish them.

theorem toRole_canonicalProfile_roundtrip (r : ThetaRole) : ∃ (r' : ThetaRole), r.canonicalProfile.toRole = some r' ∧ r'.canonicalProfile = r.canonicalProfile

toRole ∘ canonicalProfile is a retraction: it recovers a role whose canonical profile matches the input's. This partitions ThetaRole into equivalence classes under profile identity:

• Singletons: agent, patient, theme, experiencer (recoverable)
• {instrument, stimulus} — both map to stimulus
• {goal, source} — both map to goal

The proof is uniform: cases r splits into 8 constructors, and for each, both toRole and profile equality reduce by rfl.

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

"kick" subject profile → agent.

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

"kick" object profile → patient.

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

"see" subject profile → experiencer.

theorem arrive_subject_toRole : Semantics.ArgumentStructure.EntailmentProfile.arriveSubjectProfile.toRole = none

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

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

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

theorem agent_outranks_patient : Semantics.ArgumentStructure.EntailmentProfile.OutranksForSubject ThetaRole.agent.canonicalProfile ThetaRole.patient.canonicalProfile

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

theorem agent_outranks_instrument : Semantics.ArgumentStructure.EntailmentProfile.OutranksForSubject ThetaRole.agent.canonicalProfile ThetaRole.instrument.canonicalProfile

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

theorem agent_outranks_experiencer : Semantics.ArgumentStructure.EntailmentProfile.OutranksForSubject ThetaRole.agent.canonicalProfile ThetaRole.experiencer.canonicalProfile

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

theorem experiencer_instrument_alternation : Semantics.ArgumentStructure.EntailmentProfile.AllowsAlternation ThetaRole.experiencer.canonicalProfile ThetaRole.instrument.canonicalProfile

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.ArgumentStructure.EntailmentProfile.AllowsAlternation ThetaRole.experiencer.canonicalProfile ThetaRole.stimulus.canonicalProfile

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

theorem agent_maximal_pAgent : ThetaRole.agent.canonicalProfile.pAgentScore = 5 ∧ ThetaRole.agent.canonicalProfile.pPatientScore = 0

Agent is maximally proto-agentive and minimally proto-patientive — the archetype at one end of Dowty's continuum.

theorem patient_maximal_pPatient : ThetaRole.patient.canonicalProfile.pAgentScore = 0 ∧ ThetaRole.patient.canonicalProfile.pPatientScore = 3

Patient is maximally proto-patientive and minimally proto-agentive — the archetype at the opposite end.

theorem canonical_profiles_wellformed (r : ThetaRole) : r.canonicalProfile.WellFormedInternal

All canonical profiles satisfy the well-formedness constraint: volition entails sentience.

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

@[implicit_reducible]

instance Interfaces.SyntaxSemantics.instDecidableEqArgPosition : DecidableEq ArgPosition

Equations

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

@[implicit_reducible]

instance Interfaces.SyntaxSemantics.instReprArgPosition : Repr ArgPosition

Equations

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

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

Equations

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

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