Nanosyntax: Core

@cite{caha-2009}

Nanosyntax (@cite{caha-2009}, @cite{starke-2009}) is a non-lexicalist, post-syntactic, piece-based, realizational theory of morphology — identical to Distributed Morphology on all four of @cite{kalin-bjorkman-etal-2026}'s dimensions, but distinguished by two mechanism-level differences:

1. Phrasal spellout: lexical items spell out entire syntactic phrases (subtrees), not just individual terminals as in DM's Vocabulary Insertion.

2. The Superset Principle: a lexical entry matches a syntactic node if it has a sub-constituent identical to the node (@cite{caha-2009} §2.2). Among competing entries, the Elsewhere Condition selects the most specific (smallest) match.

The functional sequence (fseq)

The key structural assumption is that case features are ordered in a universal functional sequence (fseq):

NOM – ACC – GEN – DAT – INS – COM

Each case is built by successive Merge from atomic features, yielding a strictly right-branching tree:

NOM = [A]
ACC = [B [A]]
GEN = [C [B [A]]]
DAT = [D [C [B [A]]]]

Because the tree is strictly right-branching, each case is fully characterized by its rank (depth): NOM = 0, ACC = 1, GEN = 2, DAT = 3, etc. A lexical entry storing a tree of rank r contains all sub-constituents of rank ≤ r. This is exactly the containment hierarchy formalized in Core.Case.Allomorphy.

Deriving *ABA

The Superset Principle + fseq structure derives the *ABA constraint (@cite{caha-2009} §2.3). If entry β stores rank 2 (ACC-sized) and entry α stores rank 3 (GEN-sized), then:

• NOM (rank 0): both match, β wins (smaller) → β
• ACC (rank 1): both match, β wins (smaller) → β
• GEN (rank 2): only α matches → α

Result: β–β–α. There is no way to get α–β–α, because any entry that beats α for the intermediate case Y also beats α for all cases below Y (it matches them too, and it's smaller).

See Core.Case.Allomorphy for the *ABA constraint formalized independently via AllomorphyPattern.

structure Morphology.Nanosyntax.LexEntry : Type

A Nanosyntax lexical entry: a stored fseq rank paired with a phonological exponent. The rank represents how deep the entry's stored tree goes on the functional sequence.

An entry of rank r stores the tree [Fᵣ [... [F₁ [F₀]]]], which contains all sub-constituents of rank 0..r.

Contrast with DM's FeatureVI which stores a feature set (not necessarily contiguous on the fseq).

• rank : ℕ

  The rank (depth) of the stored tree on the fseq. Corresponds to Core.Case.Order.containmentRank.

• exponent : String

  The phonological exponent.

def Morphology.Nanosyntax.instDecidableEqLexEntry.decEq (x✝ x✝¹ : LexEntry) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Morphology.Nanosyntax.instDecidableEqLexEntry : DecidableEq LexEntry

Equations

• Morphology.Nanosyntax.instDecidableEqLexEntry = Morphology.Nanosyntax.instDecidableEqLexEntry.decEq

@[implicit_reducible]

instance Morphology.Nanosyntax.instReprLexEntry : Repr LexEntry

Equations

• Morphology.Nanosyntax.instReprLexEntry = { reprPrec := Morphology.Nanosyntax.instReprLexEntry.repr }

def Morphology.Nanosyntax.instReprLexEntry.repr : LexEntry → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Morphology.Nanosyntax.instBEqLexEntry : BEq LexEntry

Equations

• Morphology.Nanosyntax.instBEqLexEntry = { beq := Morphology.Nanosyntax.instBEqLexEntry.beq }

def Morphology.Nanosyntax.instBEqLexEntry.beq : LexEntry → LexEntry → Bool

Equations

• Morphology.Nanosyntax.instBEqLexEntry.beq { rank := a, exponent := a_1 } { rank := b, exponent := b_1 } = (a == b && a_1 == b_1)
• Morphology.Nanosyntax.instBEqLexEntry.beq x✝¹ x✝ = false

def Morphology.Nanosyntax.LexEntry.matches (entry : LexEntry) (targetRank : ℕ) : Bool

Does a lexical entry match a target under the Superset Principle? The entry matches if its stored tree contains the target as a sub-constituent — equivalently, if the entry's rank is at least as large as the target's rank.

@cite{caha-2009} §2.2: "A phonological exponent is inserted into a node if its lexical entry has a (sub-)constituent that is identical to the node."

Equations

• entry.matches targetRank = decide (entry.rank ≥ targetRank)

def Morphology.Nanosyntax.spellout (entries : List LexEntry) (targetRank : ℕ) : Option String

Phrasal spellout via the Superset Principle: among all entries that match the target (rank ≥ target rank), select the one with the smallest rank (= most specific, closest match).

This is the Nanosyntax counterpart of DM's vocabularyInsert. The competition logic is reversed:

• DM Subset Principle: VI features ⊆ target, largest VI wins
• Nanosyntax Superset Principle: entry rank ≥ target, smallest entry wins

Both converge on "the entry that wastes the least."

Equations

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

def Morphology.Nanosyntax.syncretic (entries : List LexEntry) (rank1 rank2 : ℕ) : Bool

Two cases are syncretic under a given lexicon if spellout assigns them the same exponent.

Equations

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

def Morphology.Nanosyntax.abaViolation (entries : List LexEntry) (x y z : ℕ) : Bool

Three ranks X < Y < Z exhibit an ABA pattern if X and Z receive the same exponent but Y receives a different one. The fseq-based Superset Principle predicts this cannot happen.

Equations

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

theorem Morphology.Nanosyntax.smaller_entry_dominates_below (α β : LexEntry) (rY rX : ℕ) (hX_le_Y : rX ≤ rY) (hβ_matches_Y : β.matches rY = true) (hα_matches_Y : α.matches rY = true) (hβ_beats_α : β.rank < α.rank) : β.matches rX = true ∧ α.matches rX = true ∧ β.rank < α.rank

If entry β (rank rβ) beats entry α (rank rα) for case Y (rank rY), then β also beats α for all cases X with rank rX ≤ rY. This is because:

1. β matches Y → β.rank ≥ rY ≥ rX → β matches X
2. β beats α for Y → β.rank < α.rank (both match, β is smaller)
3. Both match X, β is still smaller → β beats α for X too

Consequence: if β wins over α anywhere on the fseq, β wins for all cases below that point. There is no way for α to resurface below β — hence no ABA.

def Morphology.Nanosyntax.nom : ℕ

Case ranks on the fseq, matching containmentRank. NOM = 0, ACC = 1, GEN = 2, DAT = 3.

Equations

• Morphology.Nanosyntax.nom = 0

def Morphology.Nanosyntax.acc : ℕ

Equations

• Morphology.Nanosyntax.acc = 1

def Morphology.Nanosyntax.gen : ℕ

Equations

• Morphology.Nanosyntax.gen = 2

def Morphology.Nanosyntax.dat : ℕ

Equations

• Morphology.Nanosyntax.dat = 3

def Morphology.Nanosyntax.abbLexicon : List LexEntry

ABB pattern: entry A at rank 0 (NOM-sized), entry B at rank 3 (DAT-sized = covers everything).

• NOM: A (rank 0) vs B (rank 3), both match, A wins → "A"
• ACC: only B matches → "B"
• GEN: only B matches → "B"
• DAT: only B matches → "B"

Equations

• Morphology.Nanosyntax.abbLexicon = [{ rank := 0, exponent := "A" }, { rank := 3, exponent := "B" }]

theorem Morphology.Nanosyntax.abb_nom : spellout abbLexicon nom = some "A"

theorem Morphology.Nanosyntax.abb_acc : spellout abbLexicon acc = some "B"

theorem Morphology.Nanosyntax.abb_gen : spellout abbLexicon gen = some "B"

theorem Morphology.Nanosyntax.abb_dat : spellout abbLexicon dat = some "B"

theorem Morphology.Nanosyntax.abb_no_aba : abaViolation abbLexicon nom acc gen = false

ABB has no ABA violation.

def Morphology.Nanosyntax.aabLexicon : List LexEntry

AAB pattern: entry A at rank 2 (GEN-sized), entry B at rank 3 (DAT-sized).

• NOM: A (rank 2) vs B (rank 3), both match, A wins → "A"
• ACC: A vs B, A wins → "A"
• GEN: A vs B, A wins → "A"
• DAT: only B matches → "B"

Equations

• Morphology.Nanosyntax.aabLexicon = [{ rank := 2, exponent := "A" }, { rank := 3, exponent := "B" }]

theorem Morphology.Nanosyntax.aab_nom : spellout aabLexicon nom = some "A"

theorem Morphology.Nanosyntax.aab_acc : spellout aabLexicon acc = some "A"

theorem Morphology.Nanosyntax.aab_gen : spellout aabLexicon gen = some "A"

theorem Morphology.Nanosyntax.aab_dat : spellout aabLexicon dat = some "B"

def Morphology.Nanosyntax.aabbLexicon : List LexEntry

AABB pattern: entry A at rank 1 (ACC-sized), entry B at rank 3.

• NOM: A (rank 1) vs B (rank 3), A wins → "A"
• ACC: A vs B, A wins → "A"
• GEN: only B matches → "B"
• DAT: only B matches → "B"

Equations

• Morphology.Nanosyntax.aabbLexicon = [{ rank := 1, exponent := "A" }, { rank := 3, exponent := "B" }]

theorem Morphology.Nanosyntax.aabb_nom : spellout aabbLexicon nom = some "A"

theorem Morphology.Nanosyntax.aabb_acc : spellout aabbLexicon acc = some "A"

theorem Morphology.Nanosyntax.aabb_gen : spellout aabbLexicon gen = some "B"

theorem Morphology.Nanosyntax.aabb_dat : spellout aabbLexicon dat = some "B"

def Morphology.Nanosyntax.totalSyncretism : List LexEntry

Total syncretism: a single entry at rank 3 matches everything. One form for all cases.

Equations

• Morphology.Nanosyntax.totalSyncretism = [{ rank := 3, exponent := "A" }]

theorem Morphology.Nanosyntax.total_syncretic : syncretic totalSyncretism nom acc = true ∧ syncretic totalSyncretism acc gen = true ∧ syncretic totalSyncretism gen dat = true

def Morphology.Nanosyntax.attemptedABA : List LexEntry

*ABA is impossible. With entries at ranks 0 and 2 (trying to skip rank 1), the rank-2 entry matches rank 1 too — and beats the rank-0 entry for rank 0 as well! Result: B–B–B, not A–B–A.

Equations

• Morphology.Nanosyntax.attemptedABA = [{ rank := 0, exponent := "A" }, { rank := 2, exponent := "B" }]

theorem Morphology.Nanosyntax.attempted_aba_produces_abb : spellout attemptedABA nom = some "A" ∧ spellout attemptedABA acc = some "B" ∧ spellout attemptedABA gen = some "B"

theorem Morphology.Nanosyntax.attempted_aba_fails : abaViolation attemptedABA nom acc gen = false

def Morphology.Nanosyntax.threeEntryAttempt : List LexEntry

Even with three entries, *ABA is impossible. Adding a third entry at rank 2 with exponent "A" doesn't help — entries at the same rank compete, and only one can win. The fseq structure ensures contiguity.

Equations

• Morphology.Nanosyntax.threeEntryAttempt = [{ rank := 0, exponent := "A" }, { rank := 1, exponent := "B" }, { rank := 2, exponent := "A" }]

theorem Morphology.Nanosyntax.three_entry_is_aba : abaViolation threeEntryAttempt nom acc gen = true

def Morphology.Nanosyntax.caseToRank (c : Core.Case) : Option ℕ

Map a Core.Case to a Nanosyntax target rank via the existing containment hierarchy. Returns none for cases not on the standard fseq (e.g., ERG/ABS).

Equations

• Morphology.Nanosyntax.caseToRank c = c.containmentRank

def Morphology.Nanosyntax.spelloutCase (entries : List LexEntry) (c : Core.Case) : Option String

Spellout a case directly: look up the case's rank, then apply phrasal spellout.

Equations

• Morphology.Nanosyntax.spelloutCase entries c = match Morphology.Nanosyntax.caseToRank c with | some r => Morphology.Nanosyntax.spellout entries r | none => none

theorem Morphology.Nanosyntax.gap_propagates_upward (lex : List LexEntry) (r r' : ℕ) (h : spellout lex r = none) (hr : r ≤ r') : spellout lex r' = none

Paradigm gap monotonicity: if spellout fails at rank r, it fails at all higher ranks. This follows from the Superset Principle — an entry matching rank r' ≥ r would also match rank r.

inductive Morphology.Nanosyntax.MorphType : Type

Morphological type of an exponent derived from nanosyntactic spellout. Suffixes arise from spellout-driven movement (roll-up, unary foot); prefixes arise from subderivation (binary foot).

• suffix : MorphType
• prefix : MorphType

@[implicit_reducible]

instance Morphology.Nanosyntax.instDecidableEqMorphType : DecidableEq MorphType

Equations

• Morphology.Nanosyntax.instDecidableEqMorphType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Morphology.Nanosyntax.instReprMorphType.repr : MorphType → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Morphology.Nanosyntax.instReprMorphType : Repr MorphType

Equations

• Morphology.Nanosyntax.instReprMorphType = { reprPrec := Morphology.Nanosyntax.instReprMorphType.repr }

def Morphology.Nanosyntax.instBEqMorphType.beq : MorphType → MorphType → Bool

Equations

• Morphology.Nanosyntax.instBEqMorphType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[implicit_reducible]

instance Morphology.Nanosyntax.instBEqMorphType : BEq MorphType

Equations

• Morphology.Nanosyntax.instBEqMorphType = { beq := Morphology.Nanosyntax.instBEqMorphType.beq }