Paradigm Function Morphology (@cite{stump-2001}) — 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

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

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

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

@[implicit_reducible]

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

BEq (MorphPropertySet Feature✝)

Equations

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

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

@[implicit_reducible]

instance Morphology.PFM.instReprLexeme :

Repr Lexeme

Equations

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

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

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

Connects two independent formalizations:

Wordhood typology (Core.Morphology.Wordhood): K-B 2026 §3.2 two- dimensional classification (ms-boundedness × p-boundedness → 4 wordhood classes).
Clitic vs. affix diagnostics (Morphology.Diagnostics): @cite{zwicky-pullum-1983}'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 :

Core.Morphology.MorphStatus → Core.Morphology.Wordhood.MSBoundedness

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

Equations

Instances For

source

theorem Morphology.WordhoodBridge.freeWord_is_ms_free :

morphStatusToMSBound Core.Morphology.MorphStatus.freeWord = Core.Morphology.Wordhood.MSBoundedness.free

source

theorem Morphology.WordhoodBridge.simpleClitic_is_ms_free :

morphStatusToMSBound Core.Morphology.MorphStatus.simpleClitic = Core.Morphology.Wordhood.MSBoundedness.free

source

theorem Morphology.WordhoodBridge.inflAffix_is_ms_bound :

morphStatusToMSBound Core.Morphology.MorphStatus.inflAffix = Core.Morphology.Wordhood.MSBoundedness.bound

source

theorem Morphology.WordhoodBridge.derivAffix_is_ms_bound :

morphStatusToMSBound Core.Morphology.MorphStatus.derivAffix = Core.Morphology.Wordhood.MSBoundedness.bound

source

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

morphStatusToMSBound p.classify = Core.Morphology.Wordhood.MSBoundedness.bound

source

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

morphStatusToMSBound p.classify = Core.Morphology.Wordhood.MSBoundedness.free

source

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

Core.Morphology.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 Core.Morphology.MorphStatus.simpleClitic Core.Morphology.Wordhood.PBoundedness.bound).classify = Core.Morphology.Wordhood.WordhoodClass.simpleClitic

source

theorem Morphology.WordhoodBridge.inflAffix_p_bound_is_canonicalAffix :

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

source

theorem Morphology.WordhoodBridge.inflAffix_p_free_is_nonCoheringAffix :

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

source

theorem Morphology.WordhoodBridge.freeWord_p_free_is_canonicalWord :

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

source

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

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

source

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

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

source

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

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

source

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

Core.Morphology.Wordhood.PBoundedness

Map PrWd membership to p-boundedness.

Equations

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

Instances For

source

theorem Morphology.WordhoodBridge.inflectional_is_p_bound :

prWdMembershipToPBound Phonology.ProsodicWord.MorphStatus.inflectional.isPrWdInternal = Core.Morphology.Wordhood.PBoundedness.bound

source

theorem Morphology.WordhoodBridge.agreement_is_p_bound :

prWdMembershipToPBound Phonology.ProsodicWord.MorphStatus.agreement.isPrWdInternal = Core.Morphology.Wordhood.PBoundedness.bound

source

theorem Morphology.WordhoodBridge.derivational_is_p_bound :

prWdMembershipToPBound Phonology.ProsodicWord.MorphStatus.derivational.isPrWdInternal = Core.Morphology.Wordhood.PBoundedness.bound

source

theorem Morphology.WordhoodBridge.postposition_is_p_free :

prWdMembershipToPBound Phonology.ProsodicWord.MorphStatus.postposition.isPrWdInternal = Core.Morphology.Wordhood.PBoundedness.free

source

theorem Morphology.WordhoodBridge.inflAffix_prWdInternal_is_canonicalAffix :

(wordhoodProfile Core.Morphology.MorphStatus.inflAffix (prWdMembershipToPBound Phonology.ProsodicWord.MorphStatus.inflectional.isPrWdInternal)).classify = Core.Morphology.Wordhood.WordhoodClass.canonicalAffix

source

theorem Morphology.WordhoodBridge.postposition_prWdExternal_is_canonicalWord :

(wordhoodProfile Core.Morphology.MorphStatus.freeWord (prWdMembershipToPBound Phonology.ProsodicWord.MorphStatus.postposition.isPrWdInternal)).classify = Core.Morphology.Wordhood.WordhoodClass.canonicalWord

@cite{kalin-bjorkman-etal-2026}: The Morphology/Syntax Interface #

@cite{kalin-bjorkman-etal-2026}

This study file verifies the core contributions of @cite{kalin-bjorkman-etal-2026}'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 #

@cite{kalin-bjorkman-etal-2026} §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 #

@cite{kalin-bjorkman-etal-2026} §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 : Core.Morphology.Wordhood.WordhoodProfile) :

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

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

source

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

w₁ = w₂

Distinct profiles yield distinct classes.

2b. ZP diagnostics determine ms-boundedness #

@cite{kalin-bjorkman-etal-2026} §3.2.1: the six criteria from @cite{zwicky-pullum-1983} diagnose whether a morpheme is ms-bound. This is formalized in WordhoodBridge.

source

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

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

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

source

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

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

Clitichood implies ms-freedom.

2c. PrWd diagnostics determine p-boundedness #

@cite{kalin-bjorkman-etal-2026} §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 Core.Morphology.MorphStatus.inflAffix (Morphology.WordhoodBridge.prWdMembershipToPBound true)).classify = Core.Morphology.Wordhood.WordhoodClass.canonicalAffix

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

source

theorem KalinBjorkmanEtAl2026.zpClitic_plus_prWdInternal :

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

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

source

theorem KalinBjorkmanEtAl2026.zpAffix_plus_prWdExternal :

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

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

3a. The seven descriptive types #

@cite{kalin-bjorkman-etal-2026} §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) #

@cite{caha-2009}: 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.

source

theorem KalinBjorkmanEtAl2026.starABA_verified :

Morphology.Nanosyntax.abaViolation Morphology.Nanosyntax.attemptedABA 0 1 2 = false

The *ABA derivation is verified by example: attempting an ABA lexicon produces ABB instead.

4b. PFM's Paradigm Function architecture #

@cite{stump-2001}: 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 #

@cite{kalin-bjorkman-etal-2026} 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. @cite{kalin-bjorkman-etal-2026} 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

@[implicit_reducible]

instance KalinBjorkmanEtAl2026.instBEqCoverage :

BEq Coverage

Equations

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

source

def KalinBjorkmanEtAl2026.instBEqCoverage.beq :

Coverage → Coverage → Bool

Equations

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

Instances For

source

inductive KalinBjorkmanEtAl2026.TheoryName :

Type

The four named theories from @cite{kalin-bjorkman-etal-2026}.

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

@[implicit_reducible]

instance KalinBjorkmanEtAl2026.instBEqTheoryName :

BEq TheoryName

Equations

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

source

def KalinBjorkmanEtAl2026.instBEqTheoryName.beq :

TheoryName → TheoryName → Bool

Equations

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

Instances For

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 :

Core.Morphology.FormMeaningMapping.MappingType → TheoryName → List Coverage

@cite{kalin-bjorkman-etal-2026} 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 : Core.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 Core.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 Core.Morphology.FormMeaningMapping.MappingType.allomorphy TheoryName.dm = true ∧ handlesNatively Core.Morphology.FormMeaningMapping.MappingType.allomorphy TheoryName.pfm = false ∧ handlesNatively Core.Morphology.FormMeaningMapping.MappingType.allomorphy TheoryName.mas = false ∧ handlesNatively Core.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 Core.Morphology.FormMeaningMapping.MappingType.multipleExponence TheoryName.pfm = true ∧ handlesNatively Core.Morphology.FormMeaningMapping.MappingType.multipleExponence TheoryName.dm = false ∧ handlesNatively Core.Morphology.FormMeaningMapping.MappingType.multipleExponence TheoryName.mas = false ∧ handlesNatively Core.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 Core.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 : Core.Morphology.FormMeaningMapping.MappingType) (h : m ≠ Core.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 #

@cite{kalin-bjorkman-etal-2026} §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 :