Nanosyntax: Basic Definitions

[Cah09] [Sta09a]

Nanosyntax is a non-lexicalist, post-syntactic, piece-based, realizational theory of morphology — identical to Distributed Morphology on all four of [KBC+26]'s dimensions, but distinguished by two mechanism-level differences: phrasal spellout (lexical items spell out subtrees, not just terminals) and the Superset Principle (an entry matches a node its stored constituent contains; the Elsewhere Condition selects the smallest match, [Cah09] §2.2).

The proved selection-rule core — Superset matching and Minimize Junk over ExponenceRule vocabularies on a linear fseq, with *ABA (isContiguous_spellout), completeness, gap monotonicity, and DM-equigenerativity theorems — lives in Morphology/Containment/Superset.lean. Tree-based phrasal spellout for branching structures lives in Morphology/Nanosyntax/TreeSpellout.lean. This file holds the framework's remaining shared vocabulary.

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) — [Dek21] for this diagnostic on indefinite markers.

• 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 → Nat → 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 }