Documentation

def Morphology.PFM.instDecidableEqMorphPropertySet.decEq {Feature✝ : Type} [DecidableEq Feature✝] (x✝ x✝¹ : MorphPropertySet Feature✝) :

Decidable (x✝ = x✝¹)

Equations

Morphology.PFM.instDecidableEqMorphPropertySet.decEq { features := a } { features := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

Instances For

@[instance_reducible]

instance Morphology.PFM.instDecidableEqMorphPropertySet {Feature✝ : Type} [DecidableEq Feature✝] :

DecidableEq (MorphPropertySet Feature✝)

Equations

Morphology.PFM.instDecidableEqMorphPropertySet = Morphology.PFM.instDecidableEqMorphPropertySet.decEq

def Morphology.PFM.instReprMorphPropertySet.repr {Feature✝ : Type} [Repr Feature✝] :

MorphPropertySet Feature✝ → ℕ → Std.Format

Equations

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

Instances For

@[instance_reducible]

instance Morphology.PFM.instReprMorphPropertySet {Feature✝ : Type} [Repr Feature✝] :

Repr (MorphPropertySet Feature✝)

Equations

Morphology.PFM.instReprMorphPropertySet = { reprPrec := Morphology.PFM.instReprMorphPropertySet.repr }

def Morphology.PFM.instBEqMorphPropertySet.beq {Feature✝ : Type} [BEq Feature✝] :

MorphPropertySet Feature✝ → MorphPropertySet Feature✝ → Bool

Equations

Morphology.PFM.instBEqMorphPropertySet.beq { features := a } { features := b } = (a == b)
Morphology.PFM.instBEqMorphPropertySet.beq x✝¹ x✝ = false

Instances For

@[instance_reducible]

instance Morphology.PFM.instBEqMorphPropertySet {Feature✝ : Type} [BEq Feature✝] :

BEq (MorphPropertySet Feature✝)

Equations

Morphology.PFM.instBEqMorphPropertySet = { beq := Morphology.PFM.instBEqMorphPropertySet.beq }

structure Morphology.PFM.Lexeme :

name : String
category : String
stem : String

Instances For

@[instance_reducible]

instance Morphology.PFM.instDecidableEqLexeme :

DecidableEq Lexeme

Equations

Morphology.PFM.instDecidableEqLexeme = Morphology.PFM.instDecidableEqLexeme.decEq

def Morphology.PFM.instDecidableEqLexeme.decEq (x✝ x✝¹ : Lexeme) :

Decidable (x✝ = x✝¹)

Equations

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

Instances For

def Morphology.PFM.instReprLexeme.repr :

Lexeme → ℕ → Std.Format

Equations

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

Instances For

@[instance_reducible]

instance Morphology.PFM.instReprLexeme :

Repr Lexeme

Equations

Morphology.PFM.instReprLexeme = { reprPrec := Morphology.PFM.instReprLexeme.repr }

structure Morphology.PFM.RealizationRule (Feature : Type) :

context : List Feature
category : String
realize : String → String
specificity : ℕ

Instances For

def Morphology.PFM.RealizationRule.matches {Feature : Type} [BEq Feature] (rr : RealizationRule Feature) (σ : MorphPropertySet Feature) (lex : Lexeme) :

Bool

Equations

rr.matches σ lex = (lex.category == rr.category && rr.context.all fun (x : Feature) => σ.features.contains x)

Instances For

structure Morphology.PFM.RuleBlock (Feature : Type) :

label : String
rules : List (RealizationRule Feature)

Instances For

def Morphology.PFM.RuleBlock.apply {Feature : Type} [BEq Feature] (block : RuleBlock Feature) (σ : MorphPropertySet Feature) (lex : Lexeme) (stem : String) :

Option String

Equations

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

Instances For

structure Morphology.PFM.ParadigmFunction (Feature : Type) :

blocks : List (RuleBlock Feature)

Instances For

def Morphology.PFM.ParadigmFunction.apply {Feature : Type} [BEq Feature] (pf : ParadigmFunction Feature) (σ : MorphPropertySet Feature) (lex : Lexeme) :

String

Equations

pf.apply σ lex = List.foldl (fun (stem : String) (block : Morphology.PFM.RuleBlock Feature) => (block.apply σ lex stem).getD stem) lex.stem pf.blocks

Instances For

structure Morphology.PFM.RuleOfReferral (Feature : Type) :

source : MorphPropertySet Feature
target : MorphPropertySet Feature

Instances For

def Morphology.PFM.RuleOfReferral.apply {Feature : Type} [BEq Feature] (ref : RuleOfReferral Feature) (pf : ParadigmFunction Feature) (σ : MorphPropertySet Feature) (lex : Lexeme) :

Option String

Equations

ref.apply pf σ lex = if (σ == ref.source) = true then some (pf.apply ref.target lex) else none

Instances For

def Morphology.PFM.derive {Feature : Type} [BEq Feature] (pf : ParadigmFunction Feature) (referrals : List (RuleOfReferral Feature)) (σ : MorphPropertySet Feature) (lex : Lexeme) :

String

Equations

Morphology.PFM.derive pf referrals σ lex = match List.findSome? (fun (x : Morphology.PFM.RuleOfReferral Feature) => x.apply pf σ lex) referrals with | some form => form | none => pf.apply σ lex

Instances For

theorem Morphology.PFM.ParadigmFunction.apply_eq_linkage_realize {Feature : Type} [BEq Feature] (pf : ParadigmFunction Feature) (lex : Lexeme) (σ : MorphPropertySet Feature) :

Finset.image Prod.fst ((Linkage.canonical id).realize (fun (l : Lexeme) (τ : MorphPropertySet Feature) => pf.apply τ l) lex σ) = {pf.apply σ lex}

PFM's paradigm function is the word form of the [Stu16] realized paradigm under the canonical linkage: taking each lexeme as its own single stem and the identity property mapping, PF(⟨lex, σ⟩) = PF(Corr(⟨lex, σ⟩)) recovers pf.apply σ lex. PFM's realization is thus the mismatch-free case — deponency or heteroclisis would require a non-identity pm or multiple stems (Morphology/Paradigm/Linkage.lean, Studies/Stump2016.lean).

theorem Morphology.PFM.paradigmFunction_linkage_isCanonical {Feature : Type} :

(Linkage.canonical id).IsCanonical

The linkage PFM instantiates is canonical ([Stu16] §7.1): identity property mapping and one stem per lexeme.

[KBC+26] (§3.2) argue that solving the wordhood problem requires distinguishing at minimum two notions of "word":

ms-word (morphosyntactic/grammatical word): a constituent containing one or more morphemes, contained in a morphosyntactic phrase. Identified by cohesiveness, fixed internal order, selectivity, and domainhood for morphological operations (§3.2.1).
p-word (phonological/prosodic word): a constituent containing one or more syllables grouped into feet, contained in a phonological phrase. Identified by phonotactic bounding and edge phenomena (§3.2.2).

Crossing ms-boundedness (bound vs free) with p-boundedness yields a four-way typology of morpheme attachment (Table 3).

inductive Morphology.Wordhood.MSBoundedness :

Morphosyntactic boundedness. [KBC+26] §3.2.1.

free : MSBoundedness
bound : MSBoundedness

Instances For

@[instance_reducible]

instance Morphology.Wordhood.instDecidableEqMSBoundedness :

DecidableEq MSBoundedness

Equations

Morphology.Wordhood.instDecidableEqMSBoundedness x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Morphology.Wordhood.instReprMSBoundedness :

Repr MSBoundedness

Equations

Morphology.Wordhood.instReprMSBoundedness = { reprPrec := Morphology.Wordhood.instReprMSBoundedness.repr }

def Morphology.Wordhood.instReprMSBoundedness.repr :

MSBoundedness → ℕ → Std.Format

Equations

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

Instances For

inductive Morphology.Wordhood.PBoundedness :

Phonological/prosodic boundedness. [KBC+26] §3.2.2.

free : PBoundedness
bound : PBoundedness

Instances For

@[instance_reducible]

instance Morphology.Wordhood.instDecidableEqPBoundedness :

DecidableEq PBoundedness

Equations

Morphology.Wordhood.instDecidableEqPBoundedness x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Morphology.Wordhood.instReprPBoundedness.repr :

PBoundedness → ℕ → Std.Format

Equations

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

Instances For

@[instance_reducible]

instance Morphology.Wordhood.instReprPBoundedness :

Repr PBoundedness

Equations

Morphology.Wordhood.instReprPBoundedness = { reprPrec := Morphology.Wordhood.instReprPBoundedness.repr }

structure Morphology.Wordhood.WordhoodProfile :

A morpheme's wordhood profile. [KBC+26] Table 3.

ms : MSBoundedness
p : PBoundedness

Instances For

@[instance_reducible]

instance Morphology.Wordhood.instDecidableEqWordhoodProfile :

DecidableEq WordhoodProfile

Equations

Morphology.Wordhood.instDecidableEqWordhoodProfile = Morphology.Wordhood.instDecidableEqWordhoodProfile.decEq

def Morphology.Wordhood.instDecidableEqWordhoodProfile.decEq (x✝ x✝¹ : WordhoodProfile) :

Decidable (x✝ = x✝¹)

Equations

Morphology.Wordhood.instDecidableEqWordhoodProfile.decEq { ms := a, p := a_1 } { ms := b, p := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

Instances For

def Morphology.Wordhood.instReprWordhoodProfile.repr :

WordhoodProfile → ℕ → Std.Format

Equations

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

Instances For

@[instance_reducible]

instance Morphology.Wordhood.instReprWordhoodProfile :

Repr WordhoodProfile

Equations

Morphology.Wordhood.instReprWordhoodProfile = { reprPrec := Morphology.Wordhood.instReprWordhoodProfile.repr }

inductive Morphology.Wordhood.WordhoodClass :

The four-way classification of morpheme attachment. [KBC+26] §3.2.3.

canonicalWord : WordhoodClass
ms-free, p-free: an independent word by both criteria.
simpleClitic : WordhoodClass
ms-free, p-bound: syntactically independent but phonologically dependent. [Zwi77]
nonCoheringAffix : WordhoodClass
ms-bound, p-free: morphosyntactically part of a word but phonologically independent.
canonicalAffix : WordhoodClass
ms-bound, p-bound: part of a word by both criteria.

Instances For

@[instance_reducible]

instance Morphology.Wordhood.instDecidableEqWordhoodClass :

DecidableEq WordhoodClass

Equations

Morphology.Wordhood.instDecidableEqWordhoodClass x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Morphology.Wordhood.instReprWordhoodClass :

Repr WordhoodClass

Equations

Morphology.Wordhood.instReprWordhoodClass = { reprPrec := Morphology.Wordhood.instReprWordhoodClass.repr }

def Morphology.Wordhood.instReprWordhoodClass.repr :

WordhoodClass → ℕ → Std.Format

Equations

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

Instances For

def Morphology.Wordhood.WordhoodProfile.classify :

WordhoodProfile → WordhoodClass

Classify a wordhood profile into the four-way typology.

Equations

Instances For

theorem Morphology.Wordhood.canonicalWord_is_doubly_free :

{ ms := MSBoundedness.free, p := PBoundedness.free }.classify = WordhoodClass.canonicalWord

theorem Morphology.Wordhood.simpleClitic_is_ms_free_p_bound :

{ ms := MSBoundedness.free, p := PBoundedness.bound }.classify = WordhoodClass.simpleClitic

theorem Morphology.Wordhood.nonCoheringAffix_is_ms_bound_p_free :

{ ms := MSBoundedness.bound, p := PBoundedness.free }.classify = WordhoodClass.nonCoheringAffix

theorem Morphology.Wordhood.canonicalAffix_is_doubly_bound :

{ ms := MSBoundedness.bound, p := PBoundedness.bound }.classify = WordhoodClass.canonicalAffix

theorem Morphology.Wordhood.classify_total (w : WordhoodProfile) :

w.classify = WordhoodClass.canonicalWord ∨ w.classify = WordhoodClass.simpleClitic ∨ w.classify = WordhoodClass.nonCoheringAffix ∨ w.classify = WordhoodClass.canonicalAffix

The four classes are exhaustive.

theorem Morphology.Wordhood.classify_injective (w₁ w₂ : WordhoodProfile) (h : w₁.classify = w₂.classify) :

w₁ = w₂

The four classes are mutually exclusive.

Connects two independent formalizations:

Wordhood typology (Morphology.Wordhood): K-B 2026 §3.2 two- dimensional classification (ms-boundedness × p-boundedness → 4 wordhood classes).
Clitic vs. affix diagnostics (Morphology.Diagnostics): [ZP83]'s six criteria for affix-vs-clitic.

The bridge: ZP's criteria diagnose ms-boundedness. The p-boundedness dimension is orthogonal (determined by prosodic diagnostics).

Diagnostics.MorphStatus → Wordhood.MSBoundedness

def Morphology.WordhoodBridge.morphStatusToMSBound :

Map a morpheme's morphological status to its ms-boundedness.

Equations

Instances For

morphStatusToMSBound Diagnostics.MorphStatus.freeWord = Wordhood.MSBoundedness.free

theorem Morphology.WordhoodBridge.freeWord_is_ms_free :

morphStatusToMSBound Diagnostics.MorphStatus.simpleClitic = Wordhood.MSBoundedness.free

theorem Morphology.WordhoodBridge.simpleClitic_is_ms_free :

morphStatusToMSBound Diagnostics.MorphStatus.inflAffix = Wordhood.MSBoundedness.bound

theorem Morphology.WordhoodBridge.inflAffix_is_ms_bound :

morphStatusToMSBound Diagnostics.MorphStatus.derivAffix = Wordhood.MSBoundedness.bound

theorem Morphology.WordhoodBridge.derivAffix_is_ms_bound :

morphStatusToMSBound p.classify = Wordhood.MSBoundedness.bound

theorem Morphology.WordhoodBridge.zpAffix_implies_ms_bound (p : Diagnostics.CliticAffixProfile) (h : p.classify = Diagnostics.MorphStatus.inflAffix) :

morphStatusToMSBound p.classify = Wordhood.MSBoundedness.free

theorem Morphology.WordhoodBridge.zpClitic_implies_ms_free (p : Diagnostics.CliticAffixProfile) (h : p.classify = Diagnostics.MorphStatus.simpleClitic) :

def Morphology.WordhoodBridge.wordhoodProfile (status : Diagnostics.MorphStatus) (prosody : Wordhood.PBoundedness) :

Wordhood.WordhoodProfile

Construct a wordhood profile from MorphStatus + prosodic boundedness.

Equations

Morphology.WordhoodBridge.wordhoodProfile status prosody = { ms := Morphology.WordhoodBridge.morphStatusToMSBound status, p := prosody }

Instances For

(wordhoodProfile Diagnostics.MorphStatus.simpleClitic Wordhood.PBoundedness.bound).classify = Wordhood.WordhoodClass.simpleClitic

theorem Morphology.WordhoodBridge.simpleClitic_p_bound_is_simpleClitic :

(wordhoodProfile Diagnostics.MorphStatus.inflAffix Wordhood.PBoundedness.bound).classify = Wordhood.WordhoodClass.canonicalAffix

theorem Morphology.WordhoodBridge.inflAffix_p_bound_is_canonicalAffix :

(wordhoodProfile Diagnostics.MorphStatus.inflAffix Wordhood.PBoundedness.free).classify = Wordhood.WordhoodClass.nonCoheringAffix

theorem Morphology.WordhoodBridge.inflAffix_p_free_is_nonCoheringAffix :

(wordhoodProfile Diagnostics.MorphStatus.freeWord Wordhood.PBoundedness.free).classify = Wordhood.WordhoodClass.canonicalWord

theorem Morphology.WordhoodBridge.freeWord_p_free_is_canonicalWord :

theorem Morphology.WordhoodBridge.morphStatus_exhaustive (s : Diagnostics.MorphStatus) :

morphStatusToMSBound s = Wordhood.MSBoundedness.free ∨ morphStatusToMSBound s = Wordhood.MSBoundedness.bound

theorem Morphology.WordhoodBridge.affix_iff_ms_bound (s : Diagnostics.MorphStatus) :

s.IsAffix ↔ morphStatusToMSBound s = Wordhood.MSBoundedness.bound

morphStatusToMSBound s = Wordhood.MSBoundedness.free

theorem Morphology.WordhoodBridge.clitic_implies_ms_free (s : Diagnostics.MorphStatus) (h : s.IsClitic) :

def Morphology.WordhoodBridge.prWdMembershipToPBound (isPrWdInternal : Bool) :

Wordhood.PBoundedness

Map Word membership to p-boundedness.

Equations

Morphology.WordhoodBridge.prWdMembershipToPBound isPrWdInternal = if isPrWdInternal = true then Morphology.Wordhood.PBoundedness.bound else Morphology.Wordhood.PBoundedness.free

Instances For

[KBC+26]: The Morphology/Syntax Interface #

[KBC+26]

This study file verifies the core contributions of [KBC+26]'s Elements in Generative Syntax survey against Linglib's independent formalizations of DM, PFM, Nanosyntax, and the Wordhood typology.

Structure #

§1: Theory space (§2 of the Element) — verify that Linglib's theory-specific modules occupy the correct positions in the 4-dimensional classification, and that impossible combinations are ruled out.
§2: Wordhood (§3) — verify the two-dimensional typology and its connection to ZP diagnostics and ProsodicWord.
§3: Form-meaning mapping (§4) — verify coverage of the seven descriptive types.
§4: Cross-module integration — theorems connecting the independent formalizations.

inductive KalinBjorkmanEtAl2026.Lexicalism :

Whether the Morphology is a dedicated component separate from the Syntax (lexicalist) or uses the same computational system (non-lexicalist). [KBC+26] §2.1.1.

lexicalist : Lexicalism
Morphology is a separate component; the Lexical Integrity Hypothesis holds (syntax cannot manipulate sub-word pieces).
nonLexicalist : Lexicalism
Morphological and syntactic computation operate with the same kinds of principles and processes.

Instances For

@[instance_reducible]

instance KalinBjorkmanEtAl2026.instDecidableEqLexicalism :

DecidableEq Lexicalism

Equations

KalinBjorkmanEtAl2026.instDecidableEqLexicalism x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def KalinBjorkmanEtAl2026.instReprLexicalism.repr :

Lexicalism → ℕ → Std.Format

Equations

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

Instances For

@[instance_reducible]

instance KalinBjorkmanEtAl2026.instReprLexicalism :

Repr Lexicalism

Equations

KalinBjorkmanEtAl2026.instReprLexicalism = { reprPrec := KalinBjorkmanEtAl2026.instReprLexicalism.repr }

inductive KalinBjorkmanEtAl2026.Architecture :

The relative ordering of morphological and syntactic computation. [KBC+26] §2.1.2.

Lexicalist theories use preSyntactic or parallel architectures. Non-lexicalist theories use syntactic or postSyntactic.

preSyntactic : Architecture
Morphology feeds the Syntax (input to syntactic computation). Lexicalist.
parallel : Architecture
Morphology and Syntax run independently, mapping to each other. Lexicalist.
syntactic : Architecture
Morphology is the Syntax (no separate morphological component). Non-lexicalist.
postSyntactic : Architecture
Syntax feeds the Morphology (morphology operates on syntactic output). Non-lexicalist.

Instances For

@[instance_reducible]

instance KalinBjorkmanEtAl2026.instDecidableEqArchitecture :

DecidableEq Architecture

Equations

KalinBjorkmanEtAl2026.instDecidableEqArchitecture x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance KalinBjorkmanEtAl2026.instReprArchitecture :

Repr Architecture

Equations

KalinBjorkmanEtAl2026.instReprArchitecture = { reprPrec := KalinBjorkmanEtAl2026.instReprArchitecture.repr }

def KalinBjorkmanEtAl2026.instReprArchitecture.repr :

Architecture → ℕ → Std.Format

Equations

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

Instances For

inductive KalinBjorkmanEtAl2026.Exponence :

Whether complex morphological forms result from combining discrete stored pieces (Item-and-Arrangement) or from applying rules to stems (Item-and-Process). [KBC+26] §2.1.3.

pieceBased : Exponence
Complex words = combination of discrete, independently-stored morphemes. Traditional morphemes are primitive.
processBased : Exponence
Complex words = result of applying (morpho)phonological modifications (processes) to a stem. Morphemes are not primitive; affixation is one possible output of a rule.

Instances For

@[instance_reducible]

instance KalinBjorkmanEtAl2026.instDecidableEqExponence :

DecidableEq Exponence

Equations

KalinBjorkmanEtAl2026.instDecidableEqExponence x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance KalinBjorkmanEtAl2026.instReprExponence :

Repr Exponence

Equations

KalinBjorkmanEtAl2026.instReprExponence = { reprPrec := KalinBjorkmanEtAl2026.instReprExponence.repr }

def KalinBjorkmanEtAl2026.instReprExponence.repr :

Exponence → ℕ → Std.Format

Equations

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

Instances For

inductive KalinBjorkmanEtAl2026.Mapping :

Whether phonological exponents are independent of or unified with the meanings/functions they realize. [KBC+26] §2.1.4.

realizational : Mapping
Features/meanings precede or are independent of phonological exponents. Exponents realize already-present features. Late Insertion is the prototypical realizational mechanism.
incremental : Mapping
Form and meaning are built up in lockstep. A morpheme is a pairing of form and meaning; adding it adds both simultaneously.

Instances For

@[instance_reducible]

instance KalinBjorkmanEtAl2026.instDecidableEqMapping :

DecidableEq Mapping

Equations

KalinBjorkmanEtAl2026.instDecidableEqMapping x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def KalinBjorkmanEtAl2026.instReprMapping.repr :

Mapping → ℕ → Std.Format

Equations

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

Instances For

@[instance_reducible]

instance KalinBjorkmanEtAl2026.instReprMapping :

Repr Mapping

Equations

KalinBjorkmanEtAl2026.instReprMapping = { reprPrec := KalinBjorkmanEtAl2026.instReprMapping.repr }

structure KalinBjorkmanEtAl2026.TheoryPosition :

A position in the four-dimensional theory space. [KBC+26] Table 2.

lexicalism : Lexicalism
architecture : Architecture
exponence : Exponence
mapping : Mapping

Instances For

@[instance_reducible]

instance KalinBjorkmanEtAl2026.instDecidableEqTheoryPosition :

DecidableEq TheoryPosition

Equations

KalinBjorkmanEtAl2026.instDecidableEqTheoryPosition = KalinBjorkmanEtAl2026.instDecidableEqTheoryPosition.decEq

def KalinBjorkmanEtAl2026.instDecidableEqTheoryPosition.decEq (x✝ x✝¹ : TheoryPosition) :

Decidable (x✝ = x✝¹)

Equations

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

Instances For

@[instance_reducible]

instance KalinBjorkmanEtAl2026.instReprTheoryPosition :

Repr TheoryPosition

Equations

KalinBjorkmanEtAl2026.instReprTheoryPosition = { reprPrec := KalinBjorkmanEtAl2026.instReprTheoryPosition.repr }

def KalinBjorkmanEtAl2026.instReprTheoryPosition.repr :

TheoryPosition → ℕ → Std.Format

Equations

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

Instances For

def KalinBjorkmanEtAl2026.dm :

Distributed Morphology ([HM93]). Non-lexicalist, post-syntactic, piece-based, realizational.

Equations

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

Instances For

def KalinBjorkmanEtAl2026.pfm :

Paradigm Function Morphology ([Stu01]). Lexicalist, parallel, process-based, realizational.

Equations

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

Instances For

def KalinBjorkmanEtAl2026.nanosyntax :

Nanosyntax ([Sta09a]). Non-lexicalist, post-syntactic, piece-based, realizational. Shares DM's position on all four dimensions; differs in the size of spellout (phrasal, not terminal).

Equations

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

Instances For

def KalinBjorkmanEtAl2026.mas :

Morphology as Syntax ([CK23]). Non-lexicalist, syntactic (integrated), piece-based, incremental.

Equations

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

Instances For

def KalinBjorkmanEtAl2026.TheoryPosition.wellFormed (t : TheoryPosition) :

Bool

A theory position is well-formed if its dimension values respect the structural dependencies identified by [KBC+26]:

Process-based → lexicalist (syntax is piece-based)
Syntactic/post-syntactic architecture → non-lexicalist
Pre-syntactic/parallel architecture → lexicalist

Equations

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

Instances For

theorem KalinBjorkmanEtAl2026.dm_wellFormed :

dm.wellFormed = true

theorem KalinBjorkmanEtAl2026.pfm_wellFormed :

pfm.wellFormed = true

theorem KalinBjorkmanEtAl2026.nanosyntax_wellFormed :

nanosyntax.wellFormed = true

theorem KalinBjorkmanEtAl2026.mas_wellFormed :

mas.wellFormed = true

theorem KalinBjorkmanEtAl2026.dm_eq_nanosyntax :

dm = nanosyntax

DM and Nanosyntax agree on all four dimensions.

theorem KalinBjorkmanEtAl2026.dm_pfm_share_mapping :

dm.mapping = pfm.mapping

DM and PFM agree only on mapping (both realizational).

theorem KalinBjorkmanEtAl2026.dm_pfm_differ_lexicalism :

dm.lexicalism ≠ pfm.lexicalism

theorem KalinBjorkmanEtAl2026.dm_pfm_differ_exponence :

dm.exponence ≠ pfm.exponence

theorem KalinBjorkmanEtAl2026.dm_mas_share_lexicalism :

dm.lexicalism = mas.lexicalism

DM and MaS agree only on lexicalism and exponence.

theorem KalinBjorkmanEtAl2026.dm_mas_share_exponence :

dm.exponence = mas.exponence

theorem KalinBjorkmanEtAl2026.dm_mas_differ_architecture :

dm.architecture ≠ mas.architecture

theorem KalinBjorkmanEtAl2026.dm_mas_differ_mapping :

dm.mapping ≠ mas.mapping

theorem KalinBjorkmanEtAl2026.pfm_unique_processBased :

pfm.exponence = Exponence.processBased ∧ dm.exponence = Exponence.pieceBased ∧ nanosyntax.exponence = Exponence.pieceBased ∧ mas.exponence = Exponence.pieceBased

PFM is the only major theory that is process-based.

theorem KalinBjorkmanEtAl2026.mas_unique_incremental :

mas.mapping = Mapping.incremental ∧ dm.mapping = Mapping.realizational ∧ nanosyntax.mapping = Mapping.realizational ∧ pfm.mapping = Mapping.realizational

MaS is the only major theory that is incremental.

theorem KalinBjorkmanEtAl2026.nonLexicalist_processBased_illFormed (a : Architecture) (m : Mapping) :

{ lexicalism := Lexicalism.nonLexicalist, architecture := a, exponence := Exponence.processBased, mapping := m }.wellFormed = false

A non-lexicalist, process-based theory is ill-formed: syntax is piece-based, so non-lexicalist morphology (which shares the syntactic computation) must also be piece-based.

theorem KalinBjorkmanEtAl2026.lexicalist_syntactic_illFormed (e : Exponence) (m : Mapping) :

{ lexicalism := Lexicalism.lexicalist, architecture := Architecture.syntactic, exponence := e, mapping := m }.wellFormed = false

A lexicalist theory cannot have syntactic architecture (morphology is syntax contradicts morphology being separate).

1a. The four major theories occupy correct positions #

theorem KalinBjorkmanEtAl2026.dm_position :

dm.lexicalism = Lexicalism.nonLexicalist ∧ dm.architecture = Architecture.postSyntactic ∧ dm.exponence = Exponence.pieceBased ∧ dm.mapping = Mapping.realizational

DM is non-lexicalist, post-syntactic, piece-based, realizational.

theorem KalinBjorkmanEtAl2026.pfm_position :

pfm.lexicalism = Lexicalism.lexicalist ∧ pfm.architecture = Architecture.parallel ∧ pfm.exponence = Exponence.processBased ∧ pfm.mapping = Mapping.realizational

PFM is lexicalist, parallel, process-based, realizational.

theorem KalinBjorkmanEtAl2026.mas_position :

mas.lexicalism = Lexicalism.nonLexicalist ∧ mas.architecture = Architecture.syntactic ∧ mas.exponence = Exponence.pieceBased ∧ mas.mapping = Mapping.incremental

MaS is non-lexicalist, syntactic, piece-based, incremental.

theorem KalinBjorkmanEtAl2026.all_theories_wellFormed :

dm.wellFormed = true ∧ pfm.wellFormed = true ∧ nanosyntax.wellFormed = true ∧ mas.wellFormed = true

All four theories are well-formed (satisfy structural constraints).

1b. DM and Nanosyntax are indistinguishable on these dimensions #

[KBC+26] §2: DM and Nanosyntax agree on all four dimensions. Their differences (Subset vs Superset Principle, terminal vs phrasal spellout) are mechanism-level, not dimension-level.

theorem KalinBjorkmanEtAl2026.dm_nanosyntax_same_position :

dm = nanosyntax

DM and Nanosyntax occupy the same position in the theory space. Their differences are in mechanism, not architecture.

1c. Structural impossibilities #

[KBC+26] §2.1: not all 2⁴ = 16 combinations are possible. Process-based theories must be lexicalist (syntax is piece-based).

theorem KalinBjorkmanEtAl2026.no_nonLexicalist_processBased (a : Architecture) (m : Mapping) :

{ lexicalism := Lexicalism.nonLexicalist, architecture := a, exponence := Exponence.processBased, mapping := m }.wellFormed = false

No non-lexicalist, process-based theory is well-formed.

theorem KalinBjorkmanEtAl2026.no_lexicalist_syntactic (e : Exponence) (m : Mapping) :

{ lexicalism := Lexicalism.lexicalist, architecture := Architecture.syntactic, exponence := e, mapping := m }.wellFormed = false

No lexicalist theory can have syntactic architecture.

1d. Distinguishing features of each theory #

theorem KalinBjorkmanEtAl2026.pfm_uniquely_processBased :

pfm.exponence = Exponence.processBased ∧ dm.exponence ≠ Exponence.processBased ∧ mas.exponence ≠ Exponence.processBased

PFM is the only process-based theory among the four.

theorem KalinBjorkmanEtAl2026.mas_uniquely_incremental :

mas.mapping = Mapping.incremental ∧ dm.mapping ≠ Mapping.incremental ∧ pfm.mapping ≠ Mapping.incremental

MaS is the only incremental theory among the four.

2a. The 2×2 wordhood typology is exhaustive and injective #

theorem KalinBjorkmanEtAl2026.wordhood_exhaustive (w : Morphology.Wordhood.WordhoodProfile) :

w.classify = Morphology.Wordhood.WordhoodClass.canonicalWord ∨ w.classify = Morphology.Wordhood.WordhoodClass.simpleClitic ∨ w.classify = Morphology.Wordhood.WordhoodClass.nonCoheringAffix ∨ w.classify = Morphology.Wordhood.WordhoodClass.canonicalAffix

Every combination of ms- and p-boundedness yields a wordhood class.

theorem KalinBjorkmanEtAl2026.wordhood_injective (w₁ w₂ : Morphology.Wordhood.WordhoodProfile) (h : w₁.classify = w₂.classify) :

w₁ = w₂

Distinct profiles yield distinct classes.

2b. ZP diagnostics determine ms-boundedness #

[KBC+26] §3.2.1: the six criteria from [ZP83] diagnose whether a morpheme is ms-bound. This is formalized in WordhoodBridge.

theorem KalinBjorkmanEtAl2026.affix_iff_msbound (s : Morphology.Diagnostics.MorphStatus) :

s.IsAffix ↔ Morphology.WordhoodBridge.morphStatusToMSBound s = Morphology.Wordhood.MSBoundedness.bound

Affixhood (in MorphStatus) is equivalent to ms-boundedness.

Morphology.WordhoodBridge.morphStatusToMSBound s = Morphology.Wordhood.MSBoundedness.free

theorem KalinBjorkmanEtAl2026.clitic_implies_msfree (s : Morphology.Diagnostics.MorphStatus) (h : s.IsClitic) :

Clitichood implies ms-freedom.

2c. Word diagnostics determine p-boundedness #

[KBC+26] §3.2.2: prosodic diagnostics (vowel harmony scope, minimal word constraints, hiatus resolution) diagnose p-boundedness. This is formalized via the ProsodicWord bridge.

theorem KalinBjorkmanEtAl2026.zpAffix_plus_prWdInternal :

(Morphology.WordhoodBridge.wordhoodProfile Morphology.Diagnostics.MorphStatus.inflAffix (Morphology.WordhoodBridge.prWdMembershipToPBound true)).classify = Morphology.Wordhood.WordhoodClass.canonicalAffix

An inflectional suffix (Word-internal) combined with ms-boundedness from the ZP criteria yields canonical affix.

theorem KalinBjorkmanEtAl2026.zpClitic_plus_prWdInternal :

(Morphology.WordhoodBridge.wordhoodProfile Morphology.Diagnostics.MorphStatus.simpleClitic (Morphology.WordhoodBridge.prWdMembershipToPBound true)).classify = Morphology.Wordhood.WordhoodClass.simpleClitic

A clitic (ms-free) that is Word-internal (p-bound) yields simple clitic — the canonical configuration for Romance clitics.

theorem KalinBjorkmanEtAl2026.zpAffix_plus_prWdExternal :

(Morphology.WordhoodBridge.wordhoodProfile Morphology.Diagnostics.MorphStatus.inflAffix (Morphology.WordhoodBridge.prWdMembershipToPBound false)).classify = Morphology.Wordhood.WordhoodClass.nonCoheringAffix

An affix (ms-bound) that is Word-external (p-free) yields non-cohering affix — the configuration for Dutch non-cohering prefixes.

§4 of [KBC+26] identifies seven descriptive types of form-meaning mapping — the relationships between phonological exponents and morphosyntactic features/functions.

inductive KalinBjorkmanEtAl2026.Morphology.FormMeaningMapping.MappingType :

The seven descriptive types of form-meaning mapping. [KBC+26] §4.

oneToOne : MappingType
One meaning/function ↔ one exponent, invariant. Example: root cat is always \/kæt\/.
allomorphy : MappingType
One meaning/function → multiple competing exponents (context-sensitive selection). Example: English plural -z, -s, -ɪz, -ən, ∅. §4.1.
multipleExponence : MappingType
One meaning/function → multiple co-occurring exponents (non-competing, simultaneous expression). Example: Amharic k'al-at-otʃtʃ 'words' (two plural markers). §4.2.
syncretism : MappingType
Multiple related meanings/functions → one exponent (non-co-occurring contexts share a form). Example: English -ed for past tense and past participle. §4.3.
portmanteau : MappingType
Multiple co-occurring meanings/functions → one exponent (bundled into a single form). Example: French du = de + le. §4.4.
morphologicalGap : MappingType
A meaning/function has no corresponding form — the paradigm cell is empty. Example: English stride lacks a standard past participle. §4.5.1.
emptyMorph : MappingType
A form has no corresponding meaning/function. Example: Romance theme vowels, compound linkers. §4.5.2.

Instances For

@[instance_reducible]

instance KalinBjorkmanEtAl2026.Morphology.FormMeaningMapping.instDecidableEqMappingType :

DecidableEq MappingType

Equations

KalinBjorkmanEtAl2026.Morphology.FormMeaningMapping.instDecidableEqMappingType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def KalinBjorkmanEtAl2026.Morphology.FormMeaningMapping.instReprMappingType.repr :

MappingType → ℕ → Std.Format

Equations

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

Instances For

@[instance_reducible]

instance KalinBjorkmanEtAl2026.Morphology.FormMeaningMapping.instReprMappingType :

Repr MappingType

Equations

KalinBjorkmanEtAl2026.Morphology.FormMeaningMapping.instReprMappingType = { reprPrec := KalinBjorkmanEtAl2026.Morphology.FormMeaningMapping.instReprMappingType.repr }

3a. The seven descriptive types #

[KBC+26] §4 identifies seven form-meaning mapping types. Any theory of morphology must account for all of them.

theorem KalinBjorkmanEtAl2026.mappingTypes_distinct :

The seven types are mutually exclusive.

4a. *ABA impossibility (Nanosyntax contribution) #

[Cah09]: the fseq-based Superset Principle derives the *ABA constraint. If entry β beats entry α for case Y, β also beats α for all cases below Y on the fseq — Morphology.Containment.isContiguous_spellout in general.

theorem KalinBjorkmanEtAl2026.starABA_verified :

Morphology.Containment.spellout [{ exponent := "A", spans := 0, context := none }, { exponent := "B", spans := 2, context := none }] 0 = some "A" ∧ Morphology.Containment.spellout [{ exponent := "A", spans := 0, context := none }, { exponent := "B", spans := 2, context := none }] 1 = some "B" ∧ Morphology.Containment.spellout [{ exponent := "A", spans := 0, context := none }, { exponent := "B", spans := 2, context := none }] 2 = some "B" ∧ Morphology.IsContiguous (Morphology.Containment.spellout [{ exponent := "A", spans := 0, context := none }, { exponent := "B", spans := 2, context := none }])

An attempted ABA lexicon — "A" sized for the bottom grade, "B" for the top — produces ABB instead: the larger entry also wins the middle grade, and its pattern is contiguous by isContiguous_spellout.

4b. PFM's Paradigm Function architecture #

[Stu01]: PFM is the only major theory that is both process-based and parallel in architecture. This combination is well-formed because process-based requires lexicalism, and parallel is a lexicalist architecture.

theorem KalinBjorkmanEtAl2026.pfm_processBased_parallel_consistent :

pfm.exponence = Exponence.processBased ∧ pfm.architecture = Architecture.parallel ∧ pfm.wellFormed = true

PFM's combination of process-based exponence and parallel architecture is well-formed precisely because both are lexicalist.

5. Theory × mapping-type matrix #

[KBC+26] Table 4 captures the culminating insight of the Element: different theories handle form-meaning mapping complexities differently, and simplification in theory trades off against empirical coverage. Each cell records whether a theory handles a mapping type:

yes: natively, via basic mechanisms
no: must reanalyze as a different phenomenon
extra: can handle, but requires an additional mechanism

Key mechanisms referenced:

DM: VI (allomorphy), Impoverishment (metasyncretism), Fission (multiple exponence), Fusion (portmanteau), Dissociated nodes (empty morphs)
PFM: Rules of Referral (metasyncretism), rule blocks spanning (portmanteau), morphomic class indices (empty morphs)
Nanosyntax: Superset Principle + containment (syncretism), phrasal spellout (portmanteau)
MaS: strict one-to-one; all non-one-to-one phenomena must be reanalyzed as involving distinct morphemes or features

inductive KalinBjorkmanEtAl2026.Coverage :

How a morphological theory handles a form-meaning mapping type. [KBC+26] Table 4.

yes : Coverage
Handled natively by the theory's basic mechanisms.
no : Coverage
Must be reanalyzed as a different phenomenon.
extra : Coverage
Requires an extra mechanism beyond the basics.

Instances For

@[instance_reducible]

instance KalinBjorkmanEtAl2026.instDecidableEqCoverage :

DecidableEq Coverage

Equations

KalinBjorkmanEtAl2026.instDecidableEqCoverage x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance KalinBjorkmanEtAl2026.instReprCoverage :

Repr Coverage

Equations

KalinBjorkmanEtAl2026.instReprCoverage = { reprPrec := KalinBjorkmanEtAl2026.instReprCoverage.repr }

def KalinBjorkmanEtAl2026.instReprCoverage.repr :

Coverage → ℕ → Std.Format

Equations

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

Instances For

@[instance_reducible]

instance KalinBjorkmanEtAl2026.instBEqCoverage :

BEq Coverage

Equations

KalinBjorkmanEtAl2026.instBEqCoverage = { beq := KalinBjorkmanEtAl2026.instBEqCoverage.beq }

def KalinBjorkmanEtAl2026.instBEqCoverage.beq :

Coverage → Coverage → Bool

Equations

KalinBjorkmanEtAl2026.instBEqCoverage.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

inductive KalinBjorkmanEtAl2026.TheoryName :

The four named theories from [KBC+26].

pfm : TheoryName
mas : TheoryName
nanosyntax : TheoryName
dm : TheoryName

Instances For

@[instance_reducible]

instance KalinBjorkmanEtAl2026.instDecidableEqTheoryName :

DecidableEq TheoryName

Equations

KalinBjorkmanEtAl2026.instDecidableEqTheoryName x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def KalinBjorkmanEtAl2026.instReprTheoryName.repr :

TheoryName → ℕ → Std.Format

Equations

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

Instances For

@[instance_reducible]

instance KalinBjorkmanEtAl2026.instReprTheoryName :

Repr TheoryName

Equations

KalinBjorkmanEtAl2026.instReprTheoryName = { reprPrec := KalinBjorkmanEtAl2026.instReprTheoryName.repr }

@[instance_reducible]

instance KalinBjorkmanEtAl2026.instBEqTheoryName :

BEq TheoryName

Equations

KalinBjorkmanEtAl2026.instBEqTheoryName = { beq := KalinBjorkmanEtAl2026.instBEqTheoryName.beq }

def KalinBjorkmanEtAl2026.instBEqTheoryName.beq :

TheoryName → TheoryName → Bool

Equations

KalinBjorkmanEtAl2026.instBEqTheoryName.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

def KalinBjorkmanEtAl2026.TheoryName.position :

TheoryName → TheoryPosition

Map a named theory to its position in the theory space.

Equations

Instances For

def KalinBjorkmanEtAl2026.table4 :

Morphology.FormMeaningMapping.MappingType → TheoryName → List Coverage

[KBC+26] Table 4: for each (mapping type, theory) pair, the coverage verdicts across subcases.

Multiple values indicate different subcases receive different verdicts. For example, DM handles some portmanteaux natively (pre-syntactic feature bundling), must reanalyze others (allomorphy in disguise), and needs Fusion for the rest.

Equations

Instances For

def KalinBjorkmanEtAl2026.handlesNatively (m : Morphology.FormMeaningMapping.MappingType) (t : TheoryName) :

Bool

Whether a theory natively handles a mapping type (has at least one yes verdict across subcases).

Equations

KalinBjorkmanEtAl2026.handlesNatively m t = (KalinBjorkmanEtAl2026.table4 m t).any fun (x : KalinBjorkmanEtAl2026.Coverage) => x == KalinBjorkmanEtAl2026.Coverage.yes

Instances For

5a. All theories agree on one-to-one #

theorem KalinBjorkmanEtAl2026.all_handle_oneToOne (t : TheoryName) :

table4 Morphology.FormMeaningMapping.MappingType.oneToOne t = [Coverage.yes]

Every theory handles one-to-one mappings natively.

5b. DM is uniquely suited for allomorphy #

Only DM handles allomorphy natively, via Vocabulary Insertion with contextual conditioning. PFM subsumes it under multiple exponence; Nanosyntax reanalyzes structurally; MaS treats allomorphs as distinct morphemes.

theorem KalinBjorkmanEtAl2026.only_dm_handles_allomorphy :

handlesNatively Morphology.FormMeaningMapping.MappingType.allomorphy TheoryName.dm = true ∧ handlesNatively Morphology.FormMeaningMapping.MappingType.allomorphy TheoryName.pfm = false ∧ handlesNatively Morphology.FormMeaningMapping.MappingType.allomorphy TheoryName.mas = false ∧ handlesNatively Morphology.FormMeaningMapping.MappingType.allomorphy TheoryName.nanosyntax = false

DM is the only theory that handles allomorphy natively.

5c. PFM is uniquely suited for multiple exponence #

PFM's process-based, ordered rule-block architecture means independent blocks can reference the same feature, producing multiple exponence without any special mechanism.

theorem KalinBjorkmanEtAl2026.only_pfm_handles_multipleExponence :

handlesNatively Morphology.FormMeaningMapping.MappingType.multipleExponence TheoryName.pfm = true ∧ handlesNatively Morphology.FormMeaningMapping.MappingType.multipleExponence TheoryName.dm = false ∧ handlesNatively Morphology.FormMeaningMapping.MappingType.multipleExponence TheoryName.mas = false ∧ handlesNatively Morphology.FormMeaningMapping.MappingType.multipleExponence TheoryName.nanosyntax = false

PFM is the only theory that handles multiple exponence natively.

5d. Morphological gaps are universally problematic #

table4 Morphology.FormMeaningMapping.MappingType.morphologicalGap t = [Coverage.no]

theorem KalinBjorkmanEtAl2026.no_theory_handles_gaps (t : TheoryName) :

No theory handles morphological gaps natively.

5e. MaS is the most restrictive theory #

MaS's incremental mapping (form and meaning built in lockstep) forces strict one-to-one correspondence. Every apparent non-one-to-one mapping must be reanalyzed.

theorem KalinBjorkmanEtAl2026.mas_rejects_all_complex (m : Morphology.FormMeaningMapping.MappingType) (h : m ≠ Morphology.FormMeaningMapping.MappingType.oneToOne) :

table4 m TheoryName.mas = [Coverage.no]

MaS says "no" to every non-one-to-one mapping type.

5f. Realizational vs incremental split #

[KBC+26] §4.6: realizational theories handle at least some non-one-to-one mappings natively, because separating features from exponents makes mismatches structurally possible. Incremental theories (MaS) must reanalyze all of them.