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 allosemes of a head whose contentful allosemes are C, with the zero alloseme (Benz's Ø) as 0.

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, which introduces the event variable and the Theme requirement.

• 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 v. A nominalization is eventive when v is interpreted and n vacuous, and referential when n is interpreted and v vacuous, as with observation.

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 ComplexHead.Sees (Locality.lean).

inductive DistributedMorphology.Allosemy.Feature : Type

A condition an alloseme places on a neighbouring terminal, on its category or on whether it denotes an event or a state.

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

@[instance_reducible]

instance DistributedMorphology.Allosemy.instDecidableEqFeature : DecidableEq Feature

Equations

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

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.instReprFeature : Repr Feature

Equations

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

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

Equations

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

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 : Morphology.Exponence.RuleSet (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

• DistributedMorphology.Allosemy.licensed v n = List.map (fun (x : DistributedMorphology.VocabularyItem DistributedMorphology.Allosemy.Feature Sem) => x.exponent) (v.applicable n)

def DistributedMorphology.Allosemy.Verbalizer.vocabulary : Morphology.Exponence.RuleSet (VocabularyItem Feature Alloseme)

The alloseme vocabulary of v. The eventive alloseme requires an eventive complement and the zero alloseme is the elsewhere case.

Equations

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

def DistributedMorphology.Allosemy.Verbalizer.Alloseme.fromRootType : Semantics.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 Semantics.Root.ChangeType.result = DistributedMorphology.Allosemy.Verbalizer.Alloseme.eventive
• DistributedMorphology.Allosemy.Verbalizer.Alloseme.fromRootType Semantics.Root.ChangeType.propertyConcept = DistributedMorphology.Allosemy.Verbalizer.Alloseme.zero

theorem DistributedMorphology.Allosemy.Verbalizer.fromRootType_eventive_iff (rt : Semantics.Root.ChangeType) : (Alloseme.fromRootType rt).introducesEvent = true ↔ rt = Semantics.Root.ChangeType.result

v is eventive iff the root entails change.

n allosemy

inductive DistributedMorphology.Allosemy.Nominalizer.Contentful : Type

The contentful allosemes of n. The relational, sortal and alienator allosemes attach to roots; the deverbal ones have their denotations 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 ⋯

@[instance_reducible]

instance DistributedMorphology.Allosemy.Nominalizer.instReprContentful : Repr Contentful

Equations

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

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

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

The zero alloseme of n, under which the noun inherits the verb meaning (CEN).

Equations

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

def DistributedMorphology.Allosemy.Nominalizer.vocabulary : Morphology.Exponence.RuleSet (VocabularyItem Feature Alloseme)

The alloseme vocabulary of n. The deverbal allosemes require a verbal complement, the CEN and result allosemes an eventive one, and the others are unconditioned.

Equations

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

Voice allosemy

inductive DistributedMorphology.Allosemy.Voice.Contentful : Type

The θ-assigning allosemes of Voice. The complement fixes the role, since the holder cannot combine with an action predicate nor the agent with a stative one.

• 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. The zero alloseme is the expletive of relational and light-verb have.

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

The zero alloseme of Voice, which assigns no θ-role.

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✝ = { decide := !decide (x✝ = DistributedMorphology.Allosemy.Voice.Alloseme.expletive), reflects_decide := ⋯ }

def DistributedMorphology.Allosemy.Voice.vocabulary : Morphology.Exponence.RuleSet (VocabularyItem Feature Alloseme)

The alloseme vocabulary of Voice. The engineer takes a saturated eventive complement, the holder a stative one, and the expletive is the elsewhere case.

Equations

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

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

The Voice alloseme selected from Voice.vocabulary by the complement's features.

Equations

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

def DistributedMorphology.Allosemy.Voice.Alloseme.toHead : Alloseme → Minimalist.Voice.Head

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

Equations

• DistributedMorphology.Allosemy.Voice.Alloseme.toHead (some DistributedMorphology.Allosemy.Voice.Contentful.agent) = Minimalist.Voice.agentive
• DistributedMorphology.Allosemy.Voice.Alloseme.toHead (some DistributedMorphology.Allosemy.Voice.Contentful.holder) = Minimalist.Voice.experiencer
• DistributedMorphology.Allosemy.Voice.Alloseme.toHead (some DistributedMorphology.Allosemy.Voice.Contentful.engineer) = Minimalist.Voice.agentive
• DistributedMorphology.Allosemy.Voice.Alloseme.toHead none = Minimalist.Voice.anticausative

theorem DistributedMorphology.Allosemy.Voice.theta_consistent (a : Alloseme) : a.AssignsTheta ↔ a.toHead.AssignsTheta

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

Nominalization readings

inductive DistributedMorphology.Allosemy.NominalizationReading : Type

The readings of a deverbal nominalization.

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

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.instReprNominalizationReading : Repr NominalizationReading

Equations

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

@[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 the closure of its possessor slot.

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 : Morphology.Exponence.RuleSet (VocabularyItem Feature Sem)) : Morphology.Realization.Interpreted Unit (Neighborhood (List Feature)) Unit Sem

The allosemy engine as a Realization.Interpreted view, whose one head is interpreted as the alloseme the Subset Principle picks.

Equations

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

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

The verbal categorizer is allosemous, eventive under an eventive complement and zero elsewhere.