Documentation

Linglib.Theories.Morphology.DM.Allosemy

Allosemy: Contextual Meaning Variation of Functional Heads #

@cite{benz-2025} @cite{wood-2023} @cite{kratzer-1996}

@cite{benz-2025} "Structure and Interpretation Across Categories" examines allosemy — the meaning-side analog of allomorphy in Distributed Morphology. Where allomorphy concerns contextually conditioned variation in form (PF), allosemy concerns contextually conditioned variation in meaning (LF).

The key claim: several functional heads (v, n, Voice, α) systematically receive different interpretations depending on their syntactic context, and these meaning alternations are not tracked by morphosyntactic features. The syntax does not distinguish Voice_Agent from Voice_Holder featurally; the distinction is resolved at LF by the semantics of the VP complement.

Existing infrastructure as allosemy instances #

linglib already formalizes several cases of allosemy without naming them:

CategorizerSemantics.NSemanticType: n has three allosemes (relational/sortal/alienator), selected by selectsD and context
Minimalist.VoiceFlavor: Voice has six flavors (agentive/causer/ nonThematic/expletive/impersonal/passive), each with different semantics
RootType / RootClassification.changeType: roots vary in whether they entail change, conditioning the semantics of the v that embeds them

This module provides the general abstraction: AllosemicEntry and AllosemicHead capture the pattern that a single morpheme has multiple context-dependent meanings. The module then instantiates this for v (critical for @cite{benz-2025} Ch. 3 on nominalizations) and retroactively classifies existing n and Voice types as allosemy.

structure Morphology.DM.Allosemy.SyntacticContext :

A syntactic context that conditions alloseme selection.

§2.4: allosemy is conditioned by the semantics of a previously interpreted domain (below) or the syntactic features of the next higher head (above). Both cyclic locality and linear adjacency play a role, but the exact locality conditions are an open question.

We represent context minimally as what is structurally below and above the allosemic head.

belowCat : Option Categorizer
Category of the complement (below). none = no complement.
aboveCat : Option Categorizer
Category of the embedding head (above). none = root context.
complementIsEventive : Bool
Does the complement denote an event?

Instances For

def Morphology.DM.Allosemy.instDecidableEqSyntacticContext.decEq (x✝ x✝¹ : SyntacticContext) :

Decidable (x✝ = x✝¹)

Equations

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

Instances For

@[implicit_reducible]

instance Morphology.DM.Allosemy.instDecidableEqSyntacticContext :

DecidableEq SyntacticContext

Equations

Morphology.DM.Allosemy.instDecidableEqSyntacticContext = Morphology.DM.Allosemy.instDecidableEqSyntacticContext.decEq

@[implicit_reducible]

instance Morphology.DM.Allosemy.instReprSyntacticContext :

Repr SyntacticContext

Equations

Morphology.DM.Allosemy.instReprSyntacticContext = { reprPrec := Morphology.DM.Allosemy.instReprSyntacticContext.repr }

def Morphology.DM.Allosemy.instReprSyntacticContext.repr :

SyntacticContext → ℕ → Std.Format

Equations

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

Instances For

structure Morphology.DM.Allosemy.AllosemicEntry (Sem : Type) :

A single alloseme: a labeled meaning available in a particular context.

label : String
Human-readable label for this alloseme.
denotation : Sem
The semantic contribution.
context : SyntacticContext
The conditioning context.

Instances For

def Morphology.DM.Allosemy.instBEqAllosemicEntry.beq {Sem✝ : Type} [BEq Sem✝] :

AllosemicEntry Sem✝ → AllosemicEntry Sem✝ → Bool

Equations

Morphology.DM.Allosemy.instBEqAllosemicEntry.beq { label := a, denotation := a_1, context := a_2 } { label := b, denotation := b_1, context := b_2 } = (a == b && (a_1 == b_1 && a_2 == b_2))
Morphology.DM.Allosemy.instBEqAllosemicEntry.beq x✝¹ x✝ = false

Instances For

@[implicit_reducible]

instance Morphology.DM.Allosemy.instBEqAllosemicEntry {Sem✝ : Type} [BEq Sem✝] :

BEq (AllosemicEntry Sem✝)

Equations

Morphology.DM.Allosemy.instBEqAllosemicEntry = { beq := Morphology.DM.Allosemy.instBEqAllosemicEntry.beq }

@[implicit_reducible]

instance Morphology.DM.Allosemy.instReprAllosemicEntry {Sem✝ : Type} [Repr Sem✝] :

Repr (AllosemicEntry Sem✝)

Equations

Morphology.DM.Allosemy.instReprAllosemicEntry = { reprPrec := Morphology.DM.Allosemy.instReprAllosemicEntry.repr }

def Morphology.DM.Allosemy.instReprAllosemicEntry.repr {Sem✝ : Type} [Repr Sem✝] :

AllosemicEntry Sem✝ → ℕ → Std.Format

Equations

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

Instances For

structure Morphology.DM.Allosemy.AllosemicHead (Sem : Type) :

An allosemic head: a functional morpheme with multiple context-dependent meanings.

§2.6: "This dissertation is about examining the principal promise of allosemy as a tool in syntactic theory."

morpheme : Categorizer
Which functional head (n, v, a).
entries : List (AllosemicEntry Sem)
The available allosemes in their contexts.

Instances For

@[implicit_reducible]

instance Morphology.DM.Allosemy.instReprAllosemicHead {Sem✝ : Type} [Repr Sem✝] :

Repr (AllosemicHead Sem✝)

Equations

Morphology.DM.Allosemy.instReprAllosemicHead = { reprPrec := Morphology.DM.Allosemy.instReprAllosemicHead.repr }

def Morphology.DM.Allosemy.instReprAllosemicHead.repr {Sem✝ : Type} [Repr Sem✝] :

AllosemicHead Sem✝ → ℕ → Std.Format

Equations

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

Instances For

def Morphology.DM.Allosemy.AllosemicHead.allosemeCount {Sem : Type} (h : AllosemicHead Sem) :

ℕ

Number of distinct meanings available for this head.

Equations

h.allosemeCount = h.entries.length

Instances For

inductive Morphology.DM.Allosemy.VAlloseme :

Allosemes of the verbal categorizer v.

@cite{benz-2025} §2.2 / @cite{wood-2023} Ch. 5: v can be semantically null (identity function) or contribute eventive semantics, depending on its syntactic context. This distinction drives the nominalization reading typology:

eventive: v introduces an event variable and contributes the normal verbal interpretation. Yields CEN reading in nominalizations ("the frequent observation of the sky").
zero: v is semantically Ø (identity function). The root combines directly with n, yielding SEN or RN readings depending on n's alloseme. @cite{wood-2023} Ch. 5: "When n is semantically zero and v gets its ordinary verbal interpretation" (CEN); "when the v head is Ø" the root interacts directly with n (SEN/RN).

In nominalization contexts, both allosemes are available for the same root — the ambiguity between CEN and RN/SEN readings arises from v's alloseme varying, not from the root changing.

eventive : VAlloseme
zero : VAlloseme

Instances For

@[implicit_reducible]

instance Morphology.DM.Allosemy.instDecidableEqVAlloseme :

DecidableEq VAlloseme

Equations

Morphology.DM.Allosemy.instDecidableEqVAlloseme x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Morphology.DM.Allosemy.instReprVAlloseme :

Equations

Morphology.DM.Allosemy.instReprVAlloseme = { reprPrec := Morphology.DM.Allosemy.instReprVAlloseme.repr }

def Morphology.DM.Allosemy.instReprVAlloseme.repr :

VAlloseme → ℕ → Std.Format

Equations

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

Instances For

def Morphology.DM.Allosemy.VAlloseme.introducesEvent :

VAlloseme → Bool

Does this v alloseme introduce an event variable?

Equations

Instances For

def Morphology.DM.Allosemy.vAllosemic :

AllosemicHead VAlloseme

v allosemy as an AllosemicHead.

Equations

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

Instances For

theorem Morphology.DM.Allosemy.v_has_two_allosemes :

vAllosemic.allosemeCount = 2

v has exactly two allosemes.

def Morphology.DM.Allosemy.VAlloseme.fromRootType :

RootType → VAlloseme

Root change-type conditions v alloseme selection.

Result roots (entailing prior change) yield eventive v — the change entailed by the root requires an event variable in v. Property concept roots yield stative v — no inherent change event.

This connects @cite{beavers-etal-2021}'s root typology to v allosemy: the root's lexical semantics determines which v alloseme is selected.

Equations

Instances For

theorem Morphology.DM.Allosemy.result_root_eventive :

VAlloseme.fromRootType RootType.result = VAlloseme.eventive

Result roots yield eventive v.

theorem Morphology.DM.Allosemy.pc_root_zero :

VAlloseme.fromRootType RootType.propertyConcept = VAlloseme.zero

PC roots yield zero v.

theorem Morphology.DM.Allosemy.fromRootType_iff_entailsChange (rt : RootType) :

(VAlloseme.fromRootType rt).introducesEvent = rt.entailsChange

The bridge preserves the change entailment information: eventive v iff the root entails change.

inductive Morphology.DM.Allosemy.NAlloseme :

n allosemy: the three semantic types from CategorizerSemantics are allosemes of n conditioned by morphosyntactic features.

@cite{benz-2025} Ch. 3 adds a content possibility for content nominalizations. @cite{wood-2023} Ch. 5 adds zero (identity function, yielding CEN reading) and simpleEvent (yielding SEN).

The full inventory:

relational: introduces a relation (body-part-of); type ⟨e,⟨e,t⟩⟩
sortal: bare categorization; type ⟨e,t⟩
alienator: existentially closes possessor; type ⟨e,t⟩
content: selects CP complement (CCN reading, @cite{benz-2025})
zero: semantically Ø (identity), noun = verb meaning (CEN, @cite{wood-2023} Ch. 5 (5.4e))
simpleEvent: λP⟨e,t⟩λx∃e. P(x) & x = e — picks out entities equal to an event (SEN, @cite{wood-2023} Ch. 5 (5.4c))
result: λP⟨s,t⟩λx∃e. P(e) & result(x)(e) — picks out entity created as result of event (@cite{wood-2023} Ch. 6 (6.30))
state: λP⟨e,t⟩λx∃e. P(x) & x = e — picks out states (@cite{wood-2023} Ch. 1 (1.18), Ch. 6 §6.2)
entity: λP⟨e,t⟩λx. P(x) — picks out entities described by the root, no event connection (@cite{wood-2023} Ch. 5 (5.4d))

relational : NAlloseme
sortal : NAlloseme
alienator : NAlloseme
content : NAlloseme
zero : NAlloseme
simpleEvent : NAlloseme
result : NAlloseme
state : NAlloseme
entity : NAlloseme

Instances For

@[implicit_reducible]

instance Morphology.DM.Allosemy.instDecidableEqNAlloseme :

DecidableEq NAlloseme

Equations

Morphology.DM.Allosemy.instDecidableEqNAlloseme x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Morphology.DM.Allosemy.instReprNAlloseme.repr :

NAlloseme → ℕ → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance Morphology.DM.Allosemy.instReprNAlloseme :

Equations

Morphology.DM.Allosemy.instReprNAlloseme = { reprPrec := Morphology.DM.Allosemy.instReprNAlloseme.repr }

def Morphology.DM.Allosemy.NAlloseme.ofNSemanticType :

CategorizerSemantics.NSemanticType → NAlloseme

Bridge: NSemanticType from CategorizerSemantics maps to NAlloseme.

Equations

Instances For

theorem Morphology.DM.Allosemy.content_is_new (t : CategorizerSemantics.NSemanticType) :

NAlloseme.ofNSemanticType t ≠ NAlloseme.content

The content alloseme is genuinely new — it has no pre-existing NSemanticType counterpart.

def Morphology.DM.Allosemy.nAllosemic :

AllosemicHead NAlloseme

n has nine allosemes (extending the three from CategorizerSemantics with content from @cite{benz-2025} and zero/simpleEvent/result/state/ entity from @cite{wood-2023}).

Equations

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

Instances For

theorem Morphology.DM.Allosemy.n_has_nine_allosemes :

nAllosemic.allosemeCount = 9

inductive Morphology.DM.Allosemy.VoiceAlloseme :

Voice allosemy: the thematic interpretation of the external argument depends on the semantics of the VP it combines with.

@cite{kratzer-1996}: "What we cannot do, however, is combine the holder function with the denotation of an action predicate or the agent function with the denotation of a stative predicate."

§2.3: while Voice_{D} must introduce a DP argument, the thematic interpretation of that argument can be left to allosemy. The denotations in @cite{kratzer-1996} correspond not to separate syntactic heads, but to allosemes of a single Voice head.

@cite{myler-2016} Ch. 4 extends this to four allosemes, adding the engineer role (for ECM have) and the expletive/identity alloseme (for relational and light-verb have where Voice assigns no θ-role). The conditioning environments (98a–d):

agent: ⟦Voice⟧ = λx.λe. Agent(x,e) / ___(agentive, dynamic event)
holder: ⟦Voice⟧ = λx.λe. Holder(x,e) / ___(stative eventuality)
engineer: ⟦Voice⟧ = λx.λe. Engineer(x,e) / ___v_BE Eventive-VoiceP⟨s,t⟩
expletive:⟦Voice⟧ = λx.x / ___(elsewhere)

agent : VoiceAlloseme
holder : VoiceAlloseme
engineer : VoiceAlloseme
expletive : VoiceAlloseme

Instances For

@[implicit_reducible]

instance Morphology.DM.Allosemy.instDecidableEqVoiceAlloseme :

DecidableEq VoiceAlloseme

Equations

Morphology.DM.Allosemy.instDecidableEqVoiceAlloseme x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Morphology.DM.Allosemy.instReprVoiceAlloseme :

Repr VoiceAlloseme

Equations

Morphology.DM.Allosemy.instReprVoiceAlloseme = { reprPrec := Morphology.DM.Allosemy.instReprVoiceAlloseme.repr }

def Morphology.DM.Allosemy.instReprVoiceAlloseme.repr :

VoiceAlloseme → ℕ → Std.Format

Equations

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

Instances For

def Morphology.DM.Allosemy.VoiceAlloseme.assignsTheta :

VoiceAlloseme → Bool

Does this Voice alloseme assign a thematic role to the external argument?

Equations

Instances For

def Morphology.DM.Allosemy.VoiceAlloseme.fromComplement (complementIsEventiveVoiceP : Prop) [Decidable complementIsEventiveVoiceP] (complementIsStative : Prop) [Decidable complementIsStative] :

Voice alloseme selection from complement properties.

@cite{myler-2016} table (100): the alloseme is determined by the nature of have's complement and whether the VP is eventive. Engineer is the most specific: it requires a saturated eventive VoiceP as complement. The elsewhere case is expletive (identity).

Equations

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

Instances For

def Morphology.DM.Allosemy.VoiceAlloseme.toFlavor :

VoiceAlloseme → Minimalist.VoiceFlavor

Bridge: Voice allosemes to syntactic VoiceFlavor.

@cite{myler-2016}: syntactically, all four allosemes realize the same Voice_{D} — transitive Voice with a DP specifier. The θ-role distinction is resolved at LF, not in the syntax. We map to the flavor that best captures the syntactic behavior: agent/engineer → agentive (phase head, assigns θ); holder → experiencer (assigns θ, stative); expletive → expletive (no θ, no semantics).

Equations

Instances For

theorem Morphology.DM.Allosemy.voice_alloseme_theta_consistent (a : VoiceAlloseme) :

a.assignsTheta = true ↔ { flavor := a.toFlavor, hasD := true }.AssignsTheta

All θ-assigning Voice allosemes map to θ-assigning syntactic flavors; the non-θ expletive maps to a non-θ flavor.

inductive Morphology.DM.Allosemy.NominalizationReading :

Reading types for deverbal nominalizations.

@cite{wood-2023} Ch. 1 (1.18) identifies five terminal reading types; @cite{benz-2025} Ch. 3 adds the CCN for German, yielding six:

CEN (Complex Event Nominal): v eventive + n zero. Noun inherits full verb meaning including event variable and argument structure.
SEN (Simple Event Nominal): v zero + n simpleEvent. Event reading without full argument structure; event comes from n's alloseme.
Result/Product Nominal: v eventive + n result. Entity whose existence is the result of an event (e.g. prentun 'printing' = the printed object). Built off verbal meaning, retains event variable.
Simple State Nominal: v zero + n state. State reading (e.g. aðdáun 'admiration' as a lasting state, þrælkun 'slavery').
Simple Entity Nominal: v zero + n entity. Entity reading with no event connection (e.g. þvottur 'laundry' = the clothes).
CCN (Complex Content Nominal): v eventive + n content. Takes CP complement (@cite{benz-2025}).

Instances For

@[implicit_reducible]

instance Morphology.DM.Allosemy.instDecidableEqNominalizationReading :

DecidableEq NominalizationReading

Equations

Morphology.DM.Allosemy.instDecidableEqNominalizationReading x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Morphology.DM.Allosemy.instReprNominalizationReading :

Repr NominalizationReading

Equations

Morphology.DM.Allosemy.instReprNominalizationReading = { reprPrec := Morphology.DM.Allosemy.instReprNominalizationReading.repr }

def Morphology.DM.Allosemy.instReprNominalizationReading.repr :

NominalizationReading → ℕ → Std.Format

Equations

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

Instances For

def Morphology.DM.Allosemy.readingFromAllosemes :

VAlloseme → NAlloseme → Option NominalizationReading

Derive the nominalization reading from the allosemes of v and n.

Integrates @cite{benz-2025} Ch. 3 and @cite{wood-2023} Ch. 5–6:

v_eventive + n_zero → CEN (n is identity, noun = verb meaning)
v_eventive + n_sortal → CEN (@cite{benz-2025} mapping)
v_eventive + n_result → result/product RN (entity from event)
v_zero + n_simpleEvent → SEN (v absent, n picks out event-entity)
v_zero + n_state → simple state (v absent, n picks out state)
v_zero + n_entity → simple entity RN (no event connection)
v_zero + n_sortal → simple entity RN (@cite{benz-2025} mapping)
v_eventive + n_content → CCN (content requires eventive v)
v_zero + n_content → impossible (content requires eventive v)

Equations

Instances For

theorem Morphology.DM.Allosemy.cen_from_zero_n :

readingFromAllosemes VAlloseme.eventive NAlloseme.zero = some NominalizationReading.complexEvent

CEN from eventive v + zero n (@cite{wood-2023} Ch. 5).

theorem Morphology.DM.Allosemy.cen_from_sortal_n :

readingFromAllosemes VAlloseme.eventive NAlloseme.sortal = some NominalizationReading.complexEvent

CEN from eventive v + sortal n (@cite{benz-2025}).

theorem Morphology.DM.Allosemy.result_from_eventive_v :

readingFromAllosemes VAlloseme.eventive NAlloseme.result = some NominalizationReading.result

Result/product RN from eventive v + result n (@cite{wood-2023} Ch. 6 (6.30)).

theorem Morphology.DM.Allosemy.sen_from_zero_v :

readingFromAllosemes VAlloseme.zero NAlloseme.simpleEvent = some NominalizationReading.simpleEvent

SEN from zero v + simpleEvent n (@cite{wood-2023} Ch. 5).

theorem Morphology.DM.Allosemy.state_from_zero_v :

readingFromAllosemes VAlloseme.zero NAlloseme.state = some NominalizationReading.simpleState

Simple state from zero v + state n (@cite{wood-2023} Ch. 1 (1.18)).

theorem Morphology.DM.Allosemy.simpleEntity_from_entity_n :

readingFromAllosemes VAlloseme.zero NAlloseme.entity = some NominalizationReading.simpleEntity

Simple entity from zero v + entity n (@cite{wood-2023} Ch. 5).

theorem Morphology.DM.Allosemy.simpleEntity_from_sortal_n :

readingFromAllosemes VAlloseme.zero NAlloseme.sortal = some NominalizationReading.simpleEntity

Simple entity from zero v + sortal n (@cite{benz-2025}).

theorem Morphology.DM.Allosemy.ccn_requires_eventive_content :

readingFromAllosemes VAlloseme.eventive NAlloseme.content = some NominalizationReading.content

CCN requires eventive v AND content n.

theorem Morphology.DM.Allosemy.no_content_without_event :

readingFromAllosemes VAlloseme.zero NAlloseme.content = none

Content reading is impossible with zero v.

theorem Morphology.DM.Allosemy.readings_distinct :

NominalizationReading.complexEvent ≠ NominalizationReading.simpleEvent ∧ NominalizationReading.complexEvent ≠ NominalizationReading.result ∧ NominalizationReading.complexEvent ≠ NominalizationReading.simpleState ∧ NominalizationReading.complexEvent ≠ NominalizationReading.simpleEntity ∧ NominalizationReading.complexEvent ≠ NominalizationReading.content ∧ NominalizationReading.simpleEvent ≠ NominalizationReading.result ∧ NominalizationReading.simpleEvent ≠ NominalizationReading.simpleState ∧ NominalizationReading.simpleEvent ≠ NominalizationReading.simpleEntity ∧ NominalizationReading.simpleEvent ≠ NominalizationReading.content ∧ NominalizationReading.result ≠ NominalizationReading.simpleState ∧ NominalizationReading.result ≠ NominalizationReading.simpleEntity ∧ NominalizationReading.result ≠ NominalizationReading.content ∧ NominalizationReading.simpleState ≠ NominalizationReading.simpleEntity ∧ NominalizationReading.simpleState ≠ NominalizationReading.content ∧ NominalizationReading.simpleEntity ≠ NominalizationReading.content

The six readings are pairwise distinct.

inductive Morphology.DM.Allosemy.AllomorphyAnalogyPosition :

Ch. 2 evaluates three positions on the relationship between allosemy and allomorphy:

The allomorphy analogy is deeply flawed and should be abandoned.
Only phenomena that closely mirror allomorphy count as allosemy.
The analogy holds in some respects but the relationship is fundamentally different.

Benz favors position 3: allosemy shares locality properties with allomorphy (cyclic domains, adjacency effects) but Roots are far more flexible in meaning than in form.

abandoned : AllomorphyAnalogyPosition
strictParallel : AllomorphyAnalogyPosition
partialAnalogy : AllomorphyAnalogyPosition

Instances For

@[implicit_reducible]

instance Morphology.DM.Allosemy.instDecidableEqAllomorphyAnalogyPosition :

DecidableEq AllomorphyAnalogyPosition

Equations

Morphology.DM.Allosemy.instDecidableEqAllomorphyAnalogyPosition x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Morphology.DM.Allosemy.instReprAllomorphyAnalogyPosition.repr :

AllomorphyAnalogyPosition → ℕ → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance Morphology.DM.Allosemy.instReprAllomorphyAnalogyPosition :

Repr AllomorphyAnalogyPosition

Equations

Morphology.DM.Allosemy.instReprAllomorphyAnalogyPosition = { reprPrec := Morphology.DM.Allosemy.instReprAllomorphyAnalogyPosition.repr }

def Morphology.DM.Allosemy.benzPosition :

AllomorphyAnalogyPosition

Benz's position.

Equations

Morphology.DM.Allosemy.benzPosition = Morphology.DM.Allosemy.AllomorphyAnalogyPosition.partialAnalogy

Instances For