Documentation

Studies.KalinBjorkmanEtAl2026

Kalin et al. (2026): The Morphology/Syntax Interface #

This file formalizes Kalin, Bjorkman et al.'s map of the morphology/syntax interface. Section 2 sets out the dimensions along which theories vary: whether the morphology is a component separate from the syntax, lexicalism; the timing of the two computations, an architecture that is parallel or pre-syntactic exactly in the lexicalist theories and syntactic or post-syntactic in the non-lexicalist ones, (4); whether complex forms arise from pieces or from processes, which implicates lexicalism; and whether exponents are independent of the features they realize, realizational, or built up with them, incremental. Table 2 places seven theories in the space of lexicalism, mapping and exponence, and its two empty cells are exactly the non-lexicalist process-based ones (unattested_iff), the four representative theories' architectures agreeing with their lexicalism (architecture_lexicalism). Section 3 separates the morphosyntactic word, diagnosed by cohesiveness, fixed order, selectivity and domainhood, from the phonological word, and crosses the two kinds of boundness into Table 3's cells (WordhoodProfile.classify, rows_cells); Zwicky and Pullum's diagnostics place the English plural affix in the canonical-affix cell and the auxiliary clitic in the simple-clitic cell (plural_s_canonicalAffix). Section 4 distinguishes seven form-meaning mappings and Table 4 records how each representative theory treats each; the theories that treat some non-one-to-one mapping as genuine are exactly the realizational ones (handlesNatively_iff_realizational), the purely syntactic Morphology as Syntax reanalyses every one (mas_reanalyses), and no theory treats morphological gaps natively (no_theory_handles_gaps).

Implementation notes #

Table 4 is the Element's own classification of the theories, carried as data; the theorems over it are the Element's readings of the table, and the cross-table theorem relates it to Table 2.
The p-boundness of an element is not derived; the wordhood rows carry both boundnesses and the cell, and only the morphosyntactic side of the English affix and clitic is read off Zwicky and Pullum's profiles.

References #

The dimensions of the interface (Section 2.1) #

inductive KalinBjorkmanEtAl2026.Lexicalism :

Whether the morphology is a component separate from the syntax, Section 2.1.1.

lexicalist : Lexicalism
nonLexicalist : Lexicalism

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 }

@[instance_reducible]

instance KalinBjorkmanEtAl2026.instFintypeLexicalism :

Fintype Lexicalism

Equations

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

inductive KalinBjorkmanEtAl2026.Architecture :

The timing of morphology and syntax, (4).

syntactic : Architecture
parallel : Architecture
preSyntactic : Architecture
postSyntactic : Architecture

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

@[instance_reducible]

instance KalinBjorkmanEtAl2026.instFintypeArchitecture :

Fintype Architecture

Equations

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

def KalinBjorkmanEtAl2026.Architecture.lexicalism :

Architecture → Lexicalism

An architecture's lexicalism, Section 2.1.2: the parallel and pre-syntactic architectures are inherently lexicalist, the syntactic and post-syntactic ones inherently not.

Equations

Instances For

inductive KalinBjorkmanEtAl2026.Exponence :

Whether complex forms arise from the concatenation of stored pieces or from processes applied to a stem, Section 2.1.3.

pieceBased : Exponence
processBased : Exponence

Instances For

@[instance_reducible]

instance KalinBjorkmanEtAl2026.instDecidableEqExponence :

DecidableEq Exponence

Equations

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

def KalinBjorkmanEtAl2026.instReprExponence.repr :

Exponence → ℕ → Std.Format

Equations

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

Instances For

@[instance_reducible]

instance KalinBjorkmanEtAl2026.instReprExponence :

Equations

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

@[instance_reducible]

instance KalinBjorkmanEtAl2026.instFintypeExponence :

Fintype Exponence

Equations

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

inductive KalinBjorkmanEtAl2026.Mapping :

Whether exponents realize features given in advance or are built up with them, Section 2.1.4.

realizational : Mapping
incremental : Mapping

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 :

Equations

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

@[instance_reducible]

instance KalinBjorkmanEtAl2026.instFintypeMapping :

Fintype Mapping

Equations

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

structure KalinBjorkmanEtAl2026.Cell :

A cell of Table 2.

lexicalism : Lexicalism
mapping : Mapping
exponence : Exponence

Instances For

@[instance_reducible]

instance KalinBjorkmanEtAl2026.instDecidableEqCell :

DecidableEq Cell

Equations

KalinBjorkmanEtAl2026.instDecidableEqCell = KalinBjorkmanEtAl2026.instDecidableEqCell.decEq

def KalinBjorkmanEtAl2026.instDecidableEqCell.decEq (x✝ x✝¹ : Cell) :

Decidable (x✝ = x✝¹)

Equations

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

Instances For

@[instance_reducible]

instance KalinBjorkmanEtAl2026.instReprCell :

Repr Cell

Equations

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

def KalinBjorkmanEtAl2026.instReprCell.repr :

Cell → ℕ → Std.Format

Equations

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

Instances For

@[instance_reducible]

instance KalinBjorkmanEtAl2026.instFintypeCell :

Fintype Cell

Equations

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

inductive KalinBjorkmanEtAl2026.Theory :

The seven theories Table 2 places.

harmonicSerialismMorphology : Theory
distributedMorphology : Theory
nanosyntax : Theory
paradigmFunctionMorphology : Theory
minimalistMorphology : Theory
morphologyAsSyntax : Theory
articulatedMorphology : Theory

Instances For

@[instance_reducible]

instance KalinBjorkmanEtAl2026.instDecidableEqTheory :

DecidableEq Theory

Equations

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

def KalinBjorkmanEtAl2026.instReprTheory.repr :

Theory → ℕ → Std.Format

Equations

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

Instances For

@[instance_reducible]

instance KalinBjorkmanEtAl2026.instReprTheory :

Equations

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

@[instance_reducible]

instance KalinBjorkmanEtAl2026.instFintypeTheory :

Fintype Theory

Equations

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

def KalinBjorkmanEtAl2026.Theory.cell :

Theory → Cell

Table 2.

Equations

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

Instances For

theorem KalinBjorkmanEtAl2026.unattested_iff (c : Cell) :

(∀ (t : Theory), t.cell ≠ c) ↔ c.lexicalism = Lexicalism.nonLexicalist ∧ c.exponence = Exponence.processBased

Table 2's empty cells are exactly the non-lexicalist process-based ones, Section 2.4: a process-based morphology computes unlike the syntax, Section 2.1.3.

theorem KalinBjorkmanEtAl2026.dm_nanosyntax_cell :

Theory.distributedMorphology.cell = Theory.nanosyntax.cell

Distributed Morphology and Nanosyntax share a cell; they differ in mechanism, phrasal against terminal spellout, not in these dimensions.

inductive KalinBjorkmanEtAl2026.Representative :

The four theories Sections 2.2 and 2.3 present in detail and Table 4 compares.

Instances For

@[instance_reducible]

instance KalinBjorkmanEtAl2026.instDecidableEqRepresentative :

DecidableEq Representative

Equations

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

def KalinBjorkmanEtAl2026.instReprRepresentative.repr :

Representative → ℕ → Std.Format

Equations

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

Instances For

@[instance_reducible]

instance KalinBjorkmanEtAl2026.instReprRepresentative :

Repr Representative

Equations

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

@[instance_reducible]

instance KalinBjorkmanEtAl2026.instFintypeRepresentative :

Fintype Representative

Equations

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

def KalinBjorkmanEtAl2026.Representative.theory :

Representative → Theory

The theory a column of Table 4 names.

Equations

Instances For

def KalinBjorkmanEtAl2026.Representative.architecture :

Representative → Architecture

The architectures of Sections 2.2 and 2.3: Paradigm Function Morphology is parallel, Morphology as Syntax syntactic, Distributed Morphology and Nanosyntax post-syntactic.

Equations

Instances For

theorem KalinBjorkmanEtAl2026.architecture_lexicalism (r : Representative) :

r.architecture.lexicalism = r.theory.cell.lexicalism

Each representative theory's architecture has the lexicalism of its Table 2 cell.

Wordhood (Section 3.2) #

inductive KalinBjorkmanEtAl2026.MSBoundness :

Morphosyntactic boundness, Section 3.2.1: necessarily internal to a morphosyntactic word.

free : MSBoundness
bound : MSBoundness

Instances For

@[instance_reducible]

instance KalinBjorkmanEtAl2026.instDecidableEqMSBoundness :

DecidableEq MSBoundness

Equations

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

@[instance_reducible]

instance KalinBjorkmanEtAl2026.instReprMSBoundness :

Repr MSBoundness

Equations

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

def KalinBjorkmanEtAl2026.instReprMSBoundness.repr :

MSBoundness → ℕ → Std.Format

Equations

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

Instances For

@[instance_reducible]

instance KalinBjorkmanEtAl2026.instFintypeMSBoundness :

Fintype MSBoundness

Equations

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

inductive KalinBjorkmanEtAl2026.PBoundness :

Phonological boundness, Section 3.2.2: necessarily internal to a phonological word.

free : PBoundness
bound : PBoundness

Instances For

@[instance_reducible]

instance KalinBjorkmanEtAl2026.instDecidableEqPBoundness :

DecidableEq PBoundness

Equations

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

def KalinBjorkmanEtAl2026.instReprPBoundness.repr :

PBoundness → ℕ → Std.Format

Equations

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

Instances For

@[instance_reducible]

instance KalinBjorkmanEtAl2026.instReprPBoundness :

Repr PBoundness

Equations

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

@[instance_reducible]

instance KalinBjorkmanEtAl2026.instFintypePBoundness :

Fintype PBoundness

Equations

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

structure KalinBjorkmanEtAl2026.WordhoodProfile :

An element's two boundnesses.

ms : MSBoundness
p : PBoundness

Instances For

def KalinBjorkmanEtAl2026.instDecidableEqWordhoodProfile.decEq (x✝ x✝¹ : WordhoodProfile) :

Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance KalinBjorkmanEtAl2026.instDecidableEqWordhoodProfile :

DecidableEq WordhoodProfile

Equations

KalinBjorkmanEtAl2026.instDecidableEqWordhoodProfile = KalinBjorkmanEtAl2026.instDecidableEqWordhoodProfile.decEq

def KalinBjorkmanEtAl2026.instReprWordhoodProfile.repr :

WordhoodProfile → ℕ → Std.Format

Equations

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

Instances For

@[instance_reducible]

instance KalinBjorkmanEtAl2026.instReprWordhoodProfile :

Repr WordhoodProfile

Equations

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

@[instance_reducible]

instance KalinBjorkmanEtAl2026.instFintypeWordhoodProfile :

Fintype WordhoodProfile

Equations

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

inductive KalinBjorkmanEtAl2026.WordhoodClass :

The cells of Table 3.

canonicalWord : WordhoodClass
simpleClitic : WordhoodClass
nonCoheringAffix : WordhoodClass
canonicalAffix : WordhoodClass

Instances For

@[instance_reducible]

instance KalinBjorkmanEtAl2026.instDecidableEqWordhoodClass :

DecidableEq WordhoodClass

Equations

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

@[instance_reducible]

instance KalinBjorkmanEtAl2026.instReprWordhoodClass :

Repr WordhoodClass

Equations

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

def KalinBjorkmanEtAl2026.instReprWordhoodClass.repr :

WordhoodClass → ℕ → Std.Format

Equations

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

Instances For

@[instance_reducible]

instance KalinBjorkmanEtAl2026.instFintypeWordhoodClass :

Fintype WordhoodClass

Equations

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

def KalinBjorkmanEtAl2026.WordhoodProfile.classify :

WordhoodProfile → WordhoodClass

Table 3: crossing the two boundnesses.

Equations

Instances For

def KalinBjorkmanEtAl2026.classifyEquiv :

WordhoodProfile ≃ WordhoodClass

Table 3 is a bijection between profiles and cells.

Equations

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

Instances For

def KalinBjorkmanEtAl2026.msBoundness :

Morphology.Diagnostics.MorphStatus → MSBoundness

A morphosyntactic status of [ZP83]'s diagnostics is a boundness, Section 3.2.3: a clitic is a morphosyntactically free element, an affix a bound one.

Equations

Instances For

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

msBoundness s = MSBoundness.bound ↔ s.IsAffix

theorem KalinBjorkmanEtAl2026.plural_s_canonicalAffix :

{ ms := msBoundness ZwickyPullum1983.affixPluralS.classify, p := PBoundness.bound }.classify = WordhoodClass.canonicalAffix ∧ { ms := msBoundness ZwickyPullum1983.cliticS.classify, p := PBoundness.bound }.classify = WordhoodClass.simpleClitic

The English plural is a canonical affix and the auxiliary clitic a simple clitic: their morphosyntactic side from [ZP83]'s profiles, both phonologically bound.

structure KalinBjorkmanEtAl2026.WordhoodRow :

A row of Table 3: the two boundnesses and the cell.

profile : WordhoodProfile
cell : WordhoodClass

Instances For

def KalinBjorkmanEtAl2026.instDecidableEqWordhoodRow.decEq (x✝ x✝¹ : WordhoodRow) :

Decidable (x✝ = x✝¹)

Equations

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

Instances For

@[instance_reducible]

instance KalinBjorkmanEtAl2026.instDecidableEqWordhoodRow :

DecidableEq WordhoodRow

Equations

KalinBjorkmanEtAl2026.instDecidableEqWordhoodRow = KalinBjorkmanEtAl2026.instDecidableEqWordhoodRow.decEq

def KalinBjorkmanEtAl2026.msOf :

String → Option MSBoundness

Equations

KalinBjorkmanEtAl2026.msOf "free" = some KalinBjorkmanEtAl2026.MSBoundness.free
KalinBjorkmanEtAl2026.msOf "bound" = some KalinBjorkmanEtAl2026.MSBoundness.bound
KalinBjorkmanEtAl2026.msOf x✝ = none

Instances For

def KalinBjorkmanEtAl2026.pOf :

String → Option PBoundness

Equations

KalinBjorkmanEtAl2026.pOf "free" = some KalinBjorkmanEtAl2026.PBoundness.free
KalinBjorkmanEtAl2026.pOf "bound" = some KalinBjorkmanEtAl2026.PBoundness.bound
KalinBjorkmanEtAl2026.pOf x✝ = none

Instances For

def KalinBjorkmanEtAl2026.cellOf :

String → Option WordhoodClass

Equations

KalinBjorkmanEtAl2026.cellOf "canonicalWord" = some KalinBjorkmanEtAl2026.WordhoodClass.canonicalWord
KalinBjorkmanEtAl2026.cellOf "simpleClitic" = some KalinBjorkmanEtAl2026.WordhoodClass.simpleClitic
KalinBjorkmanEtAl2026.cellOf "nonCoheringAffix" = some KalinBjorkmanEtAl2026.WordhoodClass.nonCoheringAffix
KalinBjorkmanEtAl2026.cellOf "canonicalAffix" = some KalinBjorkmanEtAl2026.WordhoodClass.canonicalAffix
KalinBjorkmanEtAl2026.cellOf x✝ = none

Instances For

def KalinBjorkmanEtAl2026.WordhoodRow.ofDatum (e : Datum) :

Option WordhoodRow

A row from the paper's features.

Equations

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

Instances For

def KalinBjorkmanEtAl2026.wordhoodRows :

List WordhoodRow

The Element's printed examples of three of the four cells: cat, plural -s and possessive -s; the fourth, the non-cohering affixes, it describes in prose only.

Equations

KalinBjorkmanEtAl2026.wordhoodRows = List.filterMap KalinBjorkmanEtAl2026.WordhoodRow.ofDatum KalinBjorkmanEtAl2026.Examples.all

Instances For

theorem KalinBjorkmanEtAl2026.rows_cells (r : WordhoodRow) :

r ∈ wordhoodRows → r.profile.classify = r.cell

Each example sits in the cell its boundnesses give.

Form-meaning mappings (Section 4) #

inductive KalinBjorkmanEtAl2026.MappingType :

The seven descriptive form-meaning mappings of Section 4: abundance on the form side, allomorphy and multiple exponence; on the meaning side, syncretism and portmanteaux; and absence on either, gaps and empty morphs.

oneToOne : MappingType
allomorphy : MappingType
multipleExponence : MappingType
syncretism : MappingType
portmanteau : MappingType
morphologicalGap : MappingType
emptyMorph : MappingType

Instances For

@[instance_reducible]

instance KalinBjorkmanEtAl2026.instDecidableEqMappingType :

DecidableEq MappingType

Equations

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

def KalinBjorkmanEtAl2026.instReprMappingType.repr :

MappingType → ℕ → Std.Format

Equations

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

Instances For

@[instance_reducible]

instance KalinBjorkmanEtAl2026.instReprMappingType :

Repr MappingType

Equations

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

@[instance_reducible]

instance KalinBjorkmanEtAl2026.instFintypeMappingType :

Fintype MappingType

Equations

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

inductive KalinBjorkmanEtAl2026.Coverage :

How a theory treats a mapping in Table 4: as a genuine non-one-to-one mapping by its basic mechanisms, by reanalysis as another mapping, or by an extra mechanism.

yes : Coverage
no : Coverage
extra : Coverage

Instances For

@[instance_reducible]

instance KalinBjorkmanEtAl2026.instDecidableEqCoverage :

DecidableEq Coverage

Equations

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

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

Equations

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

@[instance_reducible]

instance KalinBjorkmanEtAl2026.instFintypeCoverage :

Fintype Coverage

Equations

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

def KalinBjorkmanEtAl2026.table4 :

MappingType → Representative → List Coverage

Table 4, a list where the subcases of a mapping receive different verdicts.

Equations

Instances For

def KalinBjorkmanEtAl2026.HandlesNatively (m : MappingType) (r : Representative) :

A theory treats a mapping natively when some subcase is a genuine mapping for it.

Equations

KalinBjorkmanEtAl2026.HandlesNatively m r = (KalinBjorkmanEtAl2026.Coverage.yes ∈ KalinBjorkmanEtAl2026.table4 m r)

Instances For

@[instance_reducible]

instance KalinBjorkmanEtAl2026.instDecidableHandlesNatively (m : MappingType) (r : Representative) :

Decidable (HandlesNatively m r)

Equations

KalinBjorkmanEtAl2026.instDecidableHandlesNatively m r = { decide := decide (List.elem KalinBjorkmanEtAl2026.Coverage.yes (KalinBjorkmanEtAl2026.table4 m r) = true), reflects_decide := ⋯ }

theorem KalinBjorkmanEtAl2026.mas_reanalyses (m : MappingType) (h : m ≠ MappingType.oneToOne) :

table4 m Representative.mas = [Coverage.no]

Morphology as Syntax denies every non-one-to-one mapping, reanalysing each, Section 4.6.

theorem KalinBjorkmanEtAl2026.no_theory_handles_gaps (r : Representative) :

table4 MappingType.morphologicalGap r = [Coverage.no]

No theory treats a morphological gap natively.

theorem KalinBjorkmanEtAl2026.handlesNatively_iff_realizational (r : Representative) :

(∃ (m : MappingType), m ≠ MappingType.oneToOne ∧ HandlesNatively m r) ↔ r.theory.cell.mapping = Mapping.realizational

The theories that treat some non-one-to-one mapping as genuine are exactly the realizational ones of Table 2: separating exponents from features is what makes a mismatch possible, Section 4.6.

theorem KalinBjorkmanEtAl2026.allomorphy_multipleExponence (r : Representative) :

(HandlesNatively MappingType.allomorphy r ↔ r = Representative.dm) ∧ (HandlesNatively MappingType.multipleExponence r ↔ r = Representative.pfm)

Distributed Morphology alone treats allomorphy natively, by contextual Vocabulary Insertion, and Paradigm Function Morphology alone multiple exponence, by independent rule blocks, Sections 4.1 and 4.2.