Paradigm Function Morphology ([Stu01]) — a lexicalist, parallel, process-based, realizational theory used by K-B 2026 §2.2 as one of the four positions in the theory space.

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

features : List Feature

Instances For

source

@[implicit_reducible]

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

DecidableEq (MorphPropertySet Feature✝)

Equations

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

source

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

source

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

source

@[implicit_reducible]

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

Repr (MorphPropertySet Feature✝)

Equations

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

source

@[implicit_reducible]

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

BEq (MorphPropertySet Feature✝)

Equations

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

source

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

source

structure Morphology.PFM.Lexeme :

Type

name : String
category : String
stem : String

Instances For

source

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

source

@[implicit_reducible]

instance Morphology.PFM.instDecidableEqLexeme :

DecidableEq Lexeme

Equations

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

source

def Morphology.PFM.instReprLexeme.repr :

Lexeme → ℕ → Std.Format

Equations

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

Instances For

source

@[implicit_reducible]

instance Morphology.PFM.instReprLexeme :

Repr Lexeme

Equations

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

source

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

Type

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

Instances For

source

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

source

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

Type

label : String
rules : List (RealizationRule Feature)

Instances For

source

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

source

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

Type

blocks : List (RuleBlock Feature)

Instances For

source

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

source

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

Type

source : MorphPropertySet Feature
target : MorphPropertySet Feature

Instances For

source

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

source

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

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

source

inductive Morphology.Wordhood.MSBoundedness :

Type

Morphosyntactic boundedness. [KBC+26] §3.2.1.

free : MSBoundedness
bound : MSBoundedness

Instances For

source

@[implicit_reducible]

instance Morphology.Wordhood.instDecidableEqMSBoundedness :

DecidableEq MSBoundedness

Equations

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

source

def Morphology.Wordhood.instReprMSBoundedness.repr :

MSBoundedness → ℕ → Std.Format

Equations

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

Instances For

source

@[implicit_reducible]

instance Morphology.Wordhood.instReprMSBoundedness :

Repr MSBoundedness

Equations

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

source

inductive Morphology.Wordhood.PBoundedness :

Type

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

free : PBoundedness
bound : PBoundedness

Instances For

source

@[implicit_reducible]

instance Morphology.Wordhood.instDecidableEqPBoundedness :

DecidableEq PBoundedness

Equations

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

source

@[implicit_reducible]

instance Morphology.Wordhood.instReprPBoundedness :

Repr PBoundedness

Equations

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

source

def Morphology.Wordhood.instReprPBoundedness.repr :

PBoundedness → ℕ → Std.Format

Equations

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

Instances For

source

structure Morphology.Wordhood.WordhoodProfile :

Type

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

ms : MSBoundedness
p : PBoundedness

Instances For

source

@[implicit_reducible]

instance Morphology.Wordhood.instDecidableEqWordhoodProfile :

DecidableEq WordhoodProfile

Equations

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

source

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

source

@[implicit_reducible]

instance Morphology.Wordhood.instReprWordhoodProfile :

Repr WordhoodProfile

Equations

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

source

def Morphology.Wordhood.instReprWordhoodProfile.repr :

WordhoodProfile → ℕ → Std.Format

Equations

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

Instances For

source

inductive Morphology.Wordhood.WordhoodClass :

Type

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

source

@[implicit_reducible]

instance Morphology.Wordhood.instDecidableEqWordhoodClass :

DecidableEq WordhoodClass

Equations

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

source

def Morphology.Wordhood.instReprWordhoodClass.repr :

WordhoodClass → ℕ → Std.Format

Equations

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

Instances For

source

@[implicit_reducible]

instance Morphology.Wordhood.instReprWordhoodClass :

Repr WordhoodClass

Equations

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

source

def Morphology.Wordhood.WordhoodProfile.classify :

WordhoodProfile → WordhoodClass

Classify a wordhood profile into the four-way typology.

Equations

Instances For

source

theorem Morphology.Wordhood.canonicalWord_is_doubly_free :

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

source

theorem Morphology.Wordhood.simpleClitic_is_ms_free_p_bound :

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

source

theorem Morphology.Wordhood.nonCoheringAffix_is_ms_bound_p_free :

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

source

theorem Morphology.Wordhood.canonicalAffix_is_doubly_bound :

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

source

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.

source

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

source

def Morphology.WordhoodBridge.morphStatusToMSBound :

MorphStatus → Wordhood.MSBoundedness

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

Equations

Instances For

source

theorem Morphology.WordhoodBridge.freeWord_is_ms_free :

morphStatusToMSBound MorphStatus.freeWord = Wordhood.MSBoundedness.free

source

theorem Morphology.WordhoodBridge.simpleClitic_is_ms_free :

morphStatusToMSBound MorphStatus.simpleClitic = Wordhood.MSBoundedness.free

source

theorem Morphology.WordhoodBridge.inflAffix_is_ms_bound :

morphStatusToMSBound MorphStatus.inflAffix = Wordhood.MSBoundedness.bound

source

theorem Morphology.WordhoodBridge.derivAffix_is_ms_bound :

morphStatusToMSBound MorphStatus.derivAffix = Wordhood.MSBoundedness.bound

source

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

morphStatusToMSBound p.classify = Wordhood.MSBoundedness.bound

source

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

morphStatusToMSBound p.classify = Wordhood.MSBoundedness.free

source

def Morphology.WordhoodBridge.wordhoodProfile (status : 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

source

theorem Morphology.WordhoodBridge.simpleClitic_p_bound_is_simpleClitic :

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

source

theorem Morphology.WordhoodBridge.inflAffix_p_bound_is_canonicalAffix :

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

source

theorem Morphology.WordhoodBridge.inflAffix_p_free_is_nonCoheringAffix :

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

source

theorem Morphology.WordhoodBridge.freeWord_p_free_is_canonicalWord :

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

source

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

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

source

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

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

source

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

morphStatusToMSBound s = Wordhood.MSBoundedness.free

source

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.

1a. The four major theories occupy correct positions #

source

theorem KalinBjorkmanEtAl2026.dm_position :

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

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

source

theorem KalinBjorkmanEtAl2026.pfm_position :

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

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

source

theorem KalinBjorkmanEtAl2026.mas_position :

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

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

source

theorem KalinBjorkmanEtAl2026.all_theories_wellFormed :

Morphology.TheorySpace.dm.wellFormed = true ∧ Morphology.TheorySpace.pfm.wellFormed = true ∧ Morphology.TheorySpace.nanosyntax.wellFormed = true ∧ Morphology.TheorySpace.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.

source

theorem KalinBjorkmanEtAl2026.dm_nanosyntax_same_position :

Morphology.TheorySpace.dm = Morphology.TheorySpace.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).

source

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

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

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

source

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

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

No lexicalist theory can have syntactic architecture.

1d. Distinguishing features of each theory #

source

theorem KalinBjorkmanEtAl2026.pfm_uniquely_processBased :

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

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

source

theorem KalinBjorkmanEtAl2026.mas_uniquely_incremental :

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

MaS is the only incremental theory among the four.

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

source

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.

source

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.

source

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

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

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

source

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

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

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.

source

theorem KalinBjorkmanEtAl2026.zpAffix_plus_prWdInternal :

(Morphology.WordhoodBridge.wordhoodProfile Morphology.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.

source

theorem KalinBjorkmanEtAl2026.zpClitic_plus_prWdInternal :

(Morphology.WordhoodBridge.wordhoodProfile Morphology.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.

source

theorem KalinBjorkmanEtAl2026.zpAffix_plus_prWdExternal :

(Morphology.WordhoodBridge.wordhoodProfile Morphology.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.

source

inductive KalinBjorkmanEtAl2026.Morphology.FormMeaningMapping.MappingType :

Type

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

source

@[implicit_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 ⋯

source

@[implicit_reducible]

instance KalinBjorkmanEtAl2026.Morphology.FormMeaningMapping.instReprMappingType :

Repr MappingType

Equations

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

source

def KalinBjorkmanEtAl2026.Morphology.FormMeaningMapping.instReprMappingType.repr :

MappingType → ℕ → Std.Format

Equations

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

Instances For

3a. The seven descriptive types #

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

source

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.

source

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

source

theorem KalinBjorkmanEtAl2026.pfm_processBased_parallel_consistent :

Morphology.TheorySpace.pfm.exponence = Morphology.TheorySpace.Exponence.processBased ∧ Morphology.TheorySpace.pfm.architecture = Morphology.TheorySpace.Architecture.parallel ∧ Morphology.TheorySpace.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

source

inductive KalinBjorkmanEtAl2026.Coverage :

Type

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

source

@[implicit_reducible]

instance KalinBjorkmanEtAl2026.instDecidableEqCoverage :

DecidableEq Coverage

Equations

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

source

@[implicit_reducible]

instance KalinBjorkmanEtAl2026.instReprCoverage :

Repr Coverage

Equations

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

source

def KalinBjorkmanEtAl2026.instReprCoverage.repr :

Coverage → ℕ → Std.Format

Equations

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

Instances For

source

def KalinBjorkmanEtAl2026.instBEqCoverage.beq :

Coverage → Coverage → Bool

Equations

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

Instances For

source

@[implicit_reducible]

instance KalinBjorkmanEtAl2026.instBEqCoverage :

BEq Coverage

Equations

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

source

inductive KalinBjorkmanEtAl2026.TheoryName :

Type

The four named theories from [KBC+26].

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

Instances For

source

@[implicit_reducible]

instance KalinBjorkmanEtAl2026.instDecidableEqTheoryName :

DecidableEq TheoryName

Equations

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

source

@[implicit_reducible]

instance KalinBjorkmanEtAl2026.instReprTheoryName :

Repr TheoryName

Equations

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

source

def KalinBjorkmanEtAl2026.instReprTheoryName.repr :

TheoryName → ℕ → Std.Format

Equations

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

Instances For

source

def KalinBjorkmanEtAl2026.instBEqTheoryName.beq :

TheoryName → TheoryName → Bool

Equations

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

Instances For

source

@[implicit_reducible]

instance KalinBjorkmanEtAl2026.instBEqTheoryName :

BEq TheoryName

Equations

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

source

def KalinBjorkmanEtAl2026.TheoryName.position :

TheoryName → Morphology.TheorySpace.TheoryPosition

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

Equations

Instances For

source

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

source

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 #

source

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.

source

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.

source

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 #

source

theorem KalinBjorkmanEtAl2026.no_theory_handles_gaps (t : TheoryName) :

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

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.

source

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.

source

theorem KalinBjorkmanEtAl2026.syncretism_splits_on_realizational :