Allosemy

Allosemy is contextual meaning variation of a single functional head — the LF analogue of allomorphy. The heads v, n, and Voice each carry several allosemes, selected by the syntactic context rather than tracked by morphosyntactic features, and the ambiguity of deverbal nominalizations between event, result, state, entity, and content readings is the visible trace of that selection. The reading typology readingFromAllosemes is grounded in typed denotations in Studies/Benz2025.lean, where it is shown to track definedness.

Main definitions

• Alloseme — the inventory carrier: contentful allosemes with the zero alloseme adjoined (Option, in the WithZero pattern)
• Verbalizer.Alloseme, Nominalizer.Alloseme, Voice.Alloseme — each head's inventory under its own API, from its Contentful type; Voice's expletive is the shared zero
• Verbalizer.vocabulary, Nominalizer.vocabulary, Voice.vocabulary — each head's List-3 vocabulary over the shared selection engine
• NominalizationReading, readingFromAllosemes — the reading typology of deverbal nominalizations and its alloseme table

Main statements

• Voice.theta_consistent — a Voice alloseme assigns a θ-role iff its syntactic flavor does
• Verbalizer.isAllosemous — v's contextual meaning variation on the shared Realization.Interpreted carrier

Implementation notes

An alloseme is a VocabularyItem whose exponent is a denotation, so DM's List 2 (form) and List 3 (meaning) run on one selection engine (subsetPrinciple, winner?_isElsewhereWinner); its specification conditions on the neighboring terminals, not on features of its own head. Voice.Alloseme.fromComplement is a worked List-3 competition on that engine; readingFromAllosemes is a different object — the composition of two already-selected allosemes. Existing infrastructure this module retroactively classifies as allosemy: Minimalist.Voice.Flavor (Voice) and root change-type conditioning of v.

References

• I. Benz, Structure and interpretation across categories
• J. Wood, Icelandic nominalizations and allosemy
• A. Kratzer, Severing the external argument from its verb
• N. Myler, Building and interpreting possession sentences
• L. J. Adamson, Gender assignment is local
• J. Beavers et al., States and changes of state

The alloseme carrier

Every head's inventory contains the zero alloseme trivially, so an inventory is the head's contentful allosemes with a zero adjoined: Option, in the WithZero pattern, with none the zero alloseme. Each head contributes only its Contentful type.

def DistributedMorphology.Allosemy.Alloseme (C : Type u_1) : Type u_1

The alloseme inventory over a head's contentful allosemes C: the contentful allosemes together with the zero alloseme every head has — mathlib's WithZero C, with the zero alloseme as its 0 (Benz's Ø). zero and of are the pattern-matchable faces of none and some.

Equations

• DistributedMorphology.Allosemy.Alloseme C = WithZero C

@[match_pattern]

def DistributedMorphology.Allosemy.Alloseme.zero {C : Type u_1} : Alloseme C

The zero alloseme: semantically Ø.

Equations

• DistributedMorphology.Allosemy.Alloseme.zero = none

@[match_pattern]

def DistributedMorphology.Allosemy.Alloseme.of {C : Type u_1} (c : C) : Alloseme C

A contentful alloseme.

Equations

• DistributedMorphology.Allosemy.Alloseme.of c = some c

@[instance_reducible]

instance DistributedMorphology.Allosemy.Alloseme.instDecidableEq {C : Type u_1} [DecidableEq C] : DecidableEq (Alloseme C)

Equations

• DistributedMorphology.Allosemy.Alloseme.instDecidableEq = DistributedMorphology.Allosemy.Alloseme.instDecidableEq._aux_1

@[instance_reducible]

instance DistributedMorphology.Allosemy.Alloseme.instRepr {C : Type u_1} [Repr C] : Repr (Alloseme C)

Equations

• DistributedMorphology.Allosemy.Alloseme.instRepr = { reprPrec := DistributedMorphology.Allosemy.Alloseme.instRepr._aux_1 }

@[instance_reducible]

instance DistributedMorphology.Allosemy.Alloseme.instFintype {C : Type u_1} [Fintype C] : Fintype (Alloseme C)

Equations

• DistributedMorphology.Allosemy.Alloseme.instFintype = { elems := DistributedMorphology.Allosemy.Alloseme.instFintype._aux_1, complete := ⋯ }

@[instance_reducible]

instance DistributedMorphology.Allosemy.Alloseme.instZero {C : Type u_1} : Zero (Alloseme C)

Equations

• DistributedMorphology.Allosemy.Alloseme.instZero = { zero := DistributedMorphology.Allosemy.Alloseme.instZero._aux_1 }

v allosemy

inductive DistributedMorphology.Allosemy.Verbalizer.Contentful : Type

The contentful alloseme of v: its verbal-domain interpretation, introducing the event variable and the Theme requirement alongside it. A single meaning here; verbal-domain flavors would extend this inventory without touching the zero structure.

• eventive : Contentful

@[instance_reducible]

instance DistributedMorphology.Allosemy.Verbalizer.instDecidableEqContentful : DecidableEq Contentful

Equations

• DistributedMorphology.Allosemy.Verbalizer.instDecidableEqContentful x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance DistributedMorphology.Allosemy.Verbalizer.instReprContentful : Repr Contentful

Equations

• DistributedMorphology.Allosemy.Verbalizer.instReprContentful = { reprPrec := DistributedMorphology.Allosemy.Verbalizer.instReprContentful.repr }

def DistributedMorphology.Allosemy.Verbalizer.instReprContentful.repr : Contentful → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance DistributedMorphology.Allosemy.Verbalizer.instFintypeContentful : Fintype Contentful

Equations

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

@[reducible, inline]

abbrev DistributedMorphology.Allosemy.Verbalizer.Alloseme : Type

The allosemes of the verbal categorizer v that the nominalization typology turns on: v is either interpreted exactly as in the verbal domain or receives the zero alloseme, in which case no internal-argument position enters the denotation. The proposal is symmetric in v and n: observation is eventive when v is interpreted and n vacuous, referential when n is interpreted and v vacuous — one root, one structure, the readings differing in which head's alloseme is contentful.

Equations

• DistributedMorphology.Allosemy.Verbalizer.Alloseme = DistributedMorphology.Allosemy.Alloseme DistributedMorphology.Allosemy.Verbalizer.Contentful

@[match_pattern]

def DistributedMorphology.Allosemy.Verbalizer.Alloseme.eventive : Alloseme

v interpreted as in the verbal domain (CEN contexts).

Equations

• DistributedMorphology.Allosemy.Verbalizer.Alloseme.eventive = DistributedMorphology.Allosemy.Alloseme.of DistributedMorphology.Allosemy.Verbalizer.Contentful.eventive

@[match_pattern]

def DistributedMorphology.Allosemy.Verbalizer.Alloseme.zero : Alloseme

Semantically Ø (SEN/RN contexts).

Equations

• DistributedMorphology.Allosemy.Verbalizer.Alloseme.zero = DistributedMorphology.Allosemy.Alloseme.zero

def DistributedMorphology.Allosemy.Verbalizer.Alloseme.introducesEvent : Alloseme → Bool

Does this v alloseme introduce an event variable?

Equations

• DistributedMorphology.Allosemy.Verbalizer.Alloseme.introducesEvent (some DistributedMorphology.Allosemy.Verbalizer.Contentful.eventive) = true
• DistributedMorphology.Allosemy.Verbalizer.Alloseme.introducesEvent none = false

Allosemic entries

An alloseme is a Vocabulary Item whose exponent is a denotation. Its specification mentions no feature of its own head — the vocabulary is the head's — and conditions on the neighbors: the complement below, toward the root, and the embedding head above — allosemy is conditioned by the interpreted domain below and the features of the next head above. The locality of the conditioning — the first category head's spell-out domain, across semantically null heads only — is Spine.Visible (Locality.lean).

inductive DistributedMorphology.Allosemy.Feature : Type

What an alloseme may require of a neighboring terminal: its category, or that it denotes an event or a state — the stative–dynamic split that conditions Voice.

• cat (c : Categorizer) : Feature
• eventive : Feature
• stative : Feature

def DistributedMorphology.Allosemy.instDecidableEqFeature.decEq (x✝ x✝¹ : Feature) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• DistributedMorphology.Allosemy.instDecidableEqFeature.decEq (DistributedMorphology.Allosemy.Feature.cat c) DistributedMorphology.Allosemy.Feature.eventive = isFalse ⋯
• DistributedMorphology.Allosemy.instDecidableEqFeature.decEq (DistributedMorphology.Allosemy.Feature.cat c) DistributedMorphology.Allosemy.Feature.stative = isFalse ⋯
• DistributedMorphology.Allosemy.instDecidableEqFeature.decEq DistributedMorphology.Allosemy.Feature.eventive (DistributedMorphology.Allosemy.Feature.cat c) = isFalse ⋯
• DistributedMorphology.Allosemy.instDecidableEqFeature.decEq DistributedMorphology.Allosemy.Feature.eventive DistributedMorphology.Allosemy.Feature.eventive = isTrue ⋯
• DistributedMorphology.Allosemy.instDecidableEqFeature.decEq DistributedMorphology.Allosemy.Feature.stative (DistributedMorphology.Allosemy.Feature.cat c) = isFalse ⋯
• DistributedMorphology.Allosemy.instDecidableEqFeature.decEq DistributedMorphology.Allosemy.Feature.stative DistributedMorphology.Allosemy.Feature.stative = isTrue ⋯

@[instance_reducible]

instance DistributedMorphology.Allosemy.instDecidableEqFeature : DecidableEq Feature

Equations

• DistributedMorphology.Allosemy.instDecidableEqFeature = DistributedMorphology.Allosemy.instDecidableEqFeature.decEq

def DistributedMorphology.Allosemy.instReprFeature.repr : Feature → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance DistributedMorphology.Allosemy.instReprFeature : Repr Feature

Equations

• DistributedMorphology.Allosemy.instReprFeature = { reprPrec := DistributedMorphology.Allosemy.instReprFeature.repr }

def DistributedMorphology.Allosemy.complement (fs : List Feature) : Neighborhood (List Feature)

A specification on the complement, the terminal below the head.

Equations

• DistributedMorphology.Allosemy.complement fs = { focus := [], leftCtx := [fs] }

def DistributedMorphology.Allosemy.embedding (fs : List Feature) : Neighborhood (List Feature)

A specification on the embedding head, the terminal above.

Equations

• DistributedMorphology.Allosemy.embedding fs = { focus := [], rightCtx := [fs] }

def DistributedMorphology.Allosemy.licensed {Sem : Type u_1} (v : List (VocabularyItem Feature Sem)) (n : Neighborhood (List Feature)) : List Sem

The denotations a vocabulary licenses in a context — the exponents of its applicable entries. Ambiguity in a context is non-singleton licensing; the canonical default among the licensed entries is the Elsewhere winner (winner?_isElsewhereWinner).

Equations

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

def DistributedMorphology.Allosemy.Verbalizer.vocabulary : List (VocabularyItem Feature Alloseme)

v's alloseme vocabulary: the eventive alloseme requires an eventive complement, while the zero alloseme is the unconditioned elsewhere option, available trivially in any context. Engine selection picks the more specific eventive alloseme in eventive contexts; licensed keeps both.

Equations

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

def DistributedMorphology.Allosemy.Verbalizer.Alloseme.fromRootType : Verb.Root.ChangeType → Alloseme

Root change-type conditions v alloseme selection: result roots, which entail a prior change, demand the event variable; property concept roots do not — the root typology feeding v allosemy.

Equations

• DistributedMorphology.Allosemy.Verbalizer.Alloseme.fromRootType Verb.Root.ChangeType.result = DistributedMorphology.Allosemy.Verbalizer.Alloseme.eventive
• DistributedMorphology.Allosemy.Verbalizer.Alloseme.fromRootType Verb.Root.ChangeType.propertyConcept = DistributedMorphology.Allosemy.Verbalizer.Alloseme.zero

theorem DistributedMorphology.Allosemy.Verbalizer.fromRootType_iff_entailsChange (rt : Verb.Root.ChangeType) : (Alloseme.fromRootType rt).introducesEvent = rt.entailsChange

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

n allosemy

inductive DistributedMorphology.Allosemy.Nominalizer.Contentful : Type

The contentful allosemes of the nominal categorizer n: the three root-attached types — relational (the body-part-of relation), sortal, and the alienator that closes a possessor slot (ArgumentStructure.Relational.ExPossessor) — the content alloseme, and the deverbal inventory. The deverbal denotations live in Studies/Benz2025.lean.

• relational : Contentful
• sortal : Contentful
• alienator : Contentful
• content : Contentful
• simpleEvent : Contentful
• result : Contentful
• state : Contentful
• entity : Contentful

@[instance_reducible]

instance DistributedMorphology.Allosemy.Nominalizer.instDecidableEqContentful : DecidableEq Contentful

Equations

• DistributedMorphology.Allosemy.Nominalizer.instDecidableEqContentful x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def DistributedMorphology.Allosemy.Nominalizer.instReprContentful.repr : Contentful → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance DistributedMorphology.Allosemy.Nominalizer.instReprContentful : Repr Contentful

Equations

• DistributedMorphology.Allosemy.Nominalizer.instReprContentful = { reprPrec := DistributedMorphology.Allosemy.Nominalizer.instReprContentful.repr }

@[instance_reducible]

instance DistributedMorphology.Allosemy.Nominalizer.instFintypeContentful : Fintype Contentful

Equations

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

@[reducible, inline]

abbrev DistributedMorphology.Allosemy.Nominalizer.Alloseme : Type

The allosemes of n: the contentful inventory or the zero alloseme — Ø / identity, on which the noun inherits the verb meaning (CEN).

Equations

• DistributedMorphology.Allosemy.Nominalizer.Alloseme = DistributedMorphology.Allosemy.Alloseme DistributedMorphology.Allosemy.Nominalizer.Contentful

@[match_pattern]

def DistributedMorphology.Allosemy.Nominalizer.Alloseme.relational : Alloseme

Equations

• DistributedMorphology.Allosemy.Nominalizer.Alloseme.relational = DistributedMorphology.Allosemy.Alloseme.of DistributedMorphology.Allosemy.Nominalizer.Contentful.relational

@[match_pattern]

def DistributedMorphology.Allosemy.Nominalizer.Alloseme.sortal : Alloseme

Equations

• DistributedMorphology.Allosemy.Nominalizer.Alloseme.sortal = DistributedMorphology.Allosemy.Alloseme.of DistributedMorphology.Allosemy.Nominalizer.Contentful.sortal

@[match_pattern]

def DistributedMorphology.Allosemy.Nominalizer.Alloseme.alienator : Alloseme

Equations

• DistributedMorphology.Allosemy.Nominalizer.Alloseme.alienator = DistributedMorphology.Allosemy.Alloseme.of DistributedMorphology.Allosemy.Nominalizer.Contentful.alienator

@[match_pattern]

def DistributedMorphology.Allosemy.Nominalizer.Alloseme.content : Alloseme

Equations

• DistributedMorphology.Allosemy.Nominalizer.Alloseme.content = DistributedMorphology.Allosemy.Alloseme.of DistributedMorphology.Allosemy.Nominalizer.Contentful.content

@[match_pattern]

def DistributedMorphology.Allosemy.Nominalizer.Alloseme.simpleEvent : Alloseme

Equations

• DistributedMorphology.Allosemy.Nominalizer.Alloseme.simpleEvent = DistributedMorphology.Allosemy.Alloseme.of DistributedMorphology.Allosemy.Nominalizer.Contentful.simpleEvent

@[match_pattern]

def DistributedMorphology.Allosemy.Nominalizer.Alloseme.result : Alloseme

Equations

• DistributedMorphology.Allosemy.Nominalizer.Alloseme.result = DistributedMorphology.Allosemy.Alloseme.of DistributedMorphology.Allosemy.Nominalizer.Contentful.result

@[match_pattern]

def DistributedMorphology.Allosemy.Nominalizer.Alloseme.state : Alloseme

Equations

• DistributedMorphology.Allosemy.Nominalizer.Alloseme.state = DistributedMorphology.Allosemy.Alloseme.of DistributedMorphology.Allosemy.Nominalizer.Contentful.state

@[match_pattern]

def DistributedMorphology.Allosemy.Nominalizer.Alloseme.entity : Alloseme

Equations

• DistributedMorphology.Allosemy.Nominalizer.Alloseme.entity = DistributedMorphology.Allosemy.Alloseme.of DistributedMorphology.Allosemy.Nominalizer.Contentful.entity

@[match_pattern]

def DistributedMorphology.Allosemy.Nominalizer.Alloseme.zero : Alloseme

Ø / identity: the noun inherits the verb meaning (CEN).

Equations

• DistributedMorphology.Allosemy.Nominalizer.Alloseme.zero = DistributedMorphology.Allosemy.Alloseme.zero

def DistributedMorphology.Allosemy.Nominalizer.vocabulary : List (VocabularyItem Feature Alloseme)

n's alloseme vocabulary: the non-deverbal allosemes are unconditioned (all-wildcard contexts), the deverbal ones require a verbal complement, with the CEN and result allosemes further demanding an eventive one.

Equations

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

Voice allosemy

inductive DistributedMorphology.Allosemy.Voice.Contentful : Type

The contentful (θ-assigning) allosemes of Voice: agent and holder — the severing argument observes that the holder function cannot combine with an action predicate, nor the agent function with a stative one, so the thematic role is fixed by the complement — and the engineer role for ECM have.

• agent : Contentful
• holder : Contentful
• engineer : Contentful

@[instance_reducible]

instance DistributedMorphology.Allosemy.Voice.instDecidableEqContentful : DecidableEq Contentful

Equations

• DistributedMorphology.Allosemy.Voice.instDecidableEqContentful x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def DistributedMorphology.Allosemy.Voice.instReprContentful.repr : Contentful → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance DistributedMorphology.Allosemy.Voice.instReprContentful : Repr Contentful

Equations

• DistributedMorphology.Allosemy.Voice.instReprContentful = { reprPrec := DistributedMorphology.Allosemy.Voice.instReprContentful.repr }

@[instance_reducible]

instance DistributedMorphology.Allosemy.Voice.instFintypeContentful : Fintype Contentful

Equations

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

@[reducible, inline]

abbrev DistributedMorphology.Allosemy.Voice.Alloseme : Type

The allosemes of Voice: a θ-role or the zero alloseme — the expletive identity for relational and light-verb have, where Voice assigns no θ-role. The expletive is the same zero every head has.

Equations

• DistributedMorphology.Allosemy.Voice.Alloseme = DistributedMorphology.Allosemy.Alloseme DistributedMorphology.Allosemy.Voice.Contentful

@[match_pattern]

def DistributedMorphology.Allosemy.Voice.Alloseme.agent : Alloseme

Equations

• DistributedMorphology.Allosemy.Voice.Alloseme.agent = DistributedMorphology.Allosemy.Alloseme.of DistributedMorphology.Allosemy.Voice.Contentful.agent

@[match_pattern]

def DistributedMorphology.Allosemy.Voice.Alloseme.holder : Alloseme

Equations

• DistributedMorphology.Allosemy.Voice.Alloseme.holder = DistributedMorphology.Allosemy.Alloseme.of DistributedMorphology.Allosemy.Voice.Contentful.holder

@[match_pattern]

def DistributedMorphology.Allosemy.Voice.Alloseme.engineer : Alloseme

Equations

• DistributedMorphology.Allosemy.Voice.Alloseme.engineer = DistributedMorphology.Allosemy.Alloseme.of DistributedMorphology.Allosemy.Voice.Contentful.engineer

@[match_pattern]

def DistributedMorphology.Allosemy.Voice.Alloseme.expletive : Alloseme

Identity; no θ-role: the zero alloseme of Voice.

Equations

• DistributedMorphology.Allosemy.Voice.Alloseme.expletive = DistributedMorphology.Allosemy.Alloseme.zero

def DistributedMorphology.Allosemy.Voice.Alloseme.AssignsTheta (a : Alloseme) : Prop

The alloseme assigns a thematic role to the external argument; only the expletive identity does not.

Equations

• a.AssignsTheta = (a ≠ DistributedMorphology.Allosemy.Voice.Alloseme.expletive)

@[instance_reducible]

instance DistributedMorphology.Allosemy.instDecidablePredAllosemeAssignsTheta : DecidablePred Voice.Alloseme.AssignsTheta

Equations

• DistributedMorphology.Allosemy.instDecidablePredAllosemeAssignsTheta x✝ = DistributedMorphology.Allosemy.instDecidablePredAllosemeAssignsTheta._aux_1 x✝

def DistributedMorphology.Allosemy.Voice.vocabulary : List (VocabularyItem Feature Alloseme)

The Voice allosemes as a competing exponence vocabulary: engineer for a saturated eventive VoiceP complement (most specified), holder for a stative one, expletive elsewhere (the all-wildcard default).

Equations

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

def DistributedMorphology.Allosemy.Voice.Alloseme.fromComplement (fs : List Feature) : Alloseme

Voice alloseme selection from the complement's features: Elsewhere competition over Voice.vocabulary, resolved by the shared exponence engine — the conditioning of the alloseme on the nature of have's complement.

Equations

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

def DistributedMorphology.Allosemy.Voice.Alloseme.toFlavor : Alloseme → Minimalist.Voice.Flavor

Bridge to the syntactic Flavor inventory. Syntactically all four allosemes realize the same Voice with a DP specifier; the θ-role distinction is resolved at LF. The map picks the flavor matching each alloseme's syntactic behavior.

Equations

• DistributedMorphology.Allosemy.Voice.Alloseme.toFlavor (some DistributedMorphology.Allosemy.Voice.Contentful.agent) = Minimalist.Voice.Flavor.agentive
• DistributedMorphology.Allosemy.Voice.Alloseme.toFlavor (some DistributedMorphology.Allosemy.Voice.Contentful.holder) = Minimalist.Voice.Flavor.experiencer
• DistributedMorphology.Allosemy.Voice.Alloseme.toFlavor (some DistributedMorphology.Allosemy.Voice.Contentful.engineer) = Minimalist.Voice.Flavor.agentive
• DistributedMorphology.Allosemy.Voice.Alloseme.toFlavor none = Minimalist.Voice.Flavor.expletive

theorem DistributedMorphology.Allosemy.Voice.theta_consistent (a : Alloseme) : a.AssignsTheta ↔ { flavor := a.toFlavor, hasD := true }.AssignsTheta

The bridge respects θ-assignment: an alloseme assigns a thematic role iff its syntactic flavor does.

Nominalization readings

inductive DistributedMorphology.Allosemy.NominalizationReading : Type

Reading types for deverbal nominalizations: the five terminal readings plus the complex content nominal.

• complexEvent : NominalizationReading
• simpleEvent : NominalizationReading
• result : NominalizationReading
• simpleState : NominalizationReading
• simpleEntity : NominalizationReading
• content : NominalizationReading

@[instance_reducible]

instance DistributedMorphology.Allosemy.instDecidableEqNominalizationReading : DecidableEq NominalizationReading

Equations

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

@[instance_reducible]

instance DistributedMorphology.Allosemy.instReprNominalizationReading : Repr NominalizationReading

Equations

• DistributedMorphology.Allosemy.instReprNominalizationReading = { reprPrec := DistributedMorphology.Allosemy.instReprNominalizationReading.repr }

def DistributedMorphology.Allosemy.instReprNominalizationReading.repr : NominalizationReading → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance DistributedMorphology.Allosemy.instFintypeNominalizationReading : Fintype NominalizationReading

Equations

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

def DistributedMorphology.Allosemy.readingFromAllosemes : Verbalizer.Alloseme → Nominalizer.Alloseme → Option NominalizationReading

The reading of a nominalization from the allosemes of v and n. The CEN pairs eventive v with zero n, the noun inheriting the verb meaning; the simple readings pair zero v with the event, state, and entity allosemes of n. The result and content readings admit both derivations — v vacuous, or the eventive component from v — and the choice is immaterial for what the nominal describes (Benz2025.result_options_pred_agree, Benz2025.content_options_agree); content needs no verbal source at all. The non-deverbal allosemes yield no nominalization reading: their semantics is the relationalizer and its possessor-closing ExPossessor.

Equations

• One or more equations did not get rendered due to their size.
• DistributedMorphology.Allosemy.readingFromAllosemes none (some DistributedMorphology.Allosemy.Nominalizer.Contentful.result) = some DistributedMorphology.Allosemy.NominalizationReading.result
• DistributedMorphology.Allosemy.readingFromAllosemes none (some DistributedMorphology.Allosemy.Nominalizer.Contentful.content) = some DistributedMorphology.Allosemy.NominalizationReading.content
• DistributedMorphology.Allosemy.readingFromAllosemes x✝ (some DistributedMorphology.Allosemy.Nominalizer.Contentful.sortal) = none
• DistributedMorphology.Allosemy.readingFromAllosemes x✝ (some DistributedMorphology.Allosemy.Nominalizer.Contentful.relational) = none
• DistributedMorphology.Allosemy.readingFromAllosemes x✝ (some DistributedMorphology.Allosemy.Nominalizer.Contentful.alienator) = none
• DistributedMorphology.Allosemy.readingFromAllosemes none none = none

The Realization.Interpreted view

An allosemic head is a List-3 object: a single morpheme whose interpretation is resolved in context by the shared exponence engine. Realization.Interpreted is exactly that carrier — an opaque index with a contextual interp map — with an empty List-2 form side, since allosemy is meaning-only. Contextual meaning variation, Benz's core claim that allosemy is allomorphy's LF analogue, is then literally Realization.Interpreted.IsAllosemous.

def DistributedMorphology.Allosemy.toInterpreted {Sem : Type} (v : List (VocabularyItem Feature Sem)) : Morphology.Realization.Interpreted Unit (Neighborhood (List Feature)) Unit Sem

The allosemy engine as a Realization.Interpreted view: one abstract head whose contextual interpretation is the alloseme the Subset Principle picks from the vocabulary (a singleton, ∅ at a semantic gap), with an empty List-2 form side.

Equations

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

theorem DistributedMorphology.Allosemy.Verbalizer.isAllosemous : (toInterpreted vocabulary).IsAllosemous ()

The verbal categorizer's meaning varies with context — eventive under an eventive complement, zero elsewhere — so v is IsAllosemous on the shared carrier: contextual meaning variation as non-constancy of the interp map.