Nanosyntax: Tree-Based Spellout

[TTML18] [Cah09] [Sta09a]

Extension of rank-based Superset spellout (Morphology/Containment/Superset.lean) to tree-structured spellout. Implements the Superset Principle (SP) for trees: a lexical entry M ↔ S' can spell out syntactic target S if S' structurally contains S (NanoTree.Contains). Among matching entries, the Elsewhere Condition selects the smallest (by tree size).

The SP on trees is a consequence of [Sta09a]'s Matching relation (formalized in [TTML18] as (35)): M matches S iff there exists a node N in M's stored tree such that S and N have the same root label and mutually matching daughters. For the right-branching single-daughter trees used in Bantu class prefix analysis, structural containment and bidirectional Matching coincide; the implementation uses containment as the simpler equivalent formulation.

Main declarations

• NanoTree: feature trees; NanoTree.Contains: sub-constituency
• TreeLexEntry: a stored tree paired with an exponent; TreeLexEntry.Matches
• treeSpellout: Superset Principle + Elsewhere Condition
• FootConditionMet: [TTML18]'s constraint on backtracking
• chain_contains_iff_le: for right-branching chains, tree containment reduces to rank comparison — tree-based spellout generalizes (not replaces) rank-based spellout

NanoTree

inductive Morphology.Nanosyntax.NanoTree (F : Type u_1) : Type u_1

A nanosyntactic feature tree. Simpler than Syntax — no traces, no binding, no category/word split. Just labeled nodes with an ordered list of daughters.

leaf f = a terminal feature. node f children = feature f dominating daughters.

• leaf {F : Type u_1} : F → NanoTree F
• node {F : Type u_1} : F → List (NanoTree F) → NanoTree F

@[implicit_reducible]

instance Morphology.Nanosyntax.instReprNanoTree {F✝ : Type u_1} [Repr F✝] : Repr (NanoTree F✝)

Equations

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

partial def Morphology.Nanosyntax.instReprNanoTree.repr {F✝ : Type u_1} [Repr F✝] : NanoTree F✝ → ℕ → Std.Format

Decidable equality

Defined by structural recursion (not deriving DecidableEq, which routes the nested List through well-founded recursion and does not kernel-reduce; decide-style spellout evaluations need the structural form).

def Morphology.Nanosyntax.NanoTree.decEq {F : Type u_1} [DecidableEq F] (s t : NanoTree F) : Decidable (s = t)

Structural decidable equality on trees.

Equations

• One or more equations did not get rendered due to their size.
• (Morphology.Nanosyntax.NanoTree.leaf f).decEq (Morphology.Nanosyntax.NanoTree.leaf g) = if h : f = g then isTrue ⋯ else isFalse ⋯
• (Morphology.Nanosyntax.NanoTree.leaf a).decEq (Morphology.Nanosyntax.NanoTree.node a_1 a_2) = isFalse ⋯
• (Morphology.Nanosyntax.NanoTree.node a a_1).decEq (Morphology.Nanosyntax.NanoTree.leaf a_2) = isFalse ⋯

def Morphology.Nanosyntax.NanoTree.decEq.decEqList {F : Type u_1} [DecidableEq F] (cs ds : List (NanoTree F)) : Decidable (cs = ds)

Structural decidable equality on daughter lists.

Equations

• One or more equations did not get rendered due to their size.
• Morphology.Nanosyntax.NanoTree.decEq.decEqList [] [] = isTrue ⋯
• Morphology.Nanosyntax.NanoTree.decEq.decEqList [] (head :: tail) = isFalse ⋯
• Morphology.Nanosyntax.NanoTree.decEq.decEqList (head :: tail) [] = isFalse ⋯

@[implicit_reducible]

instance Morphology.Nanosyntax.NanoTree.instDecidableEq {F : Type u_1} [DecidableEq F] : DecidableEq (NanoTree F)

Equations

• Morphology.Nanosyntax.NanoTree.instDecidableEq = Morphology.Nanosyntax.NanoTree.decEq

Size

def Morphology.Nanosyntax.NanoTree.size {F : Type u_1} : NanoTree F → ℕ

Number of nodes in the tree. Used by the Elsewhere Condition to select the smallest matching entry.

Equations

• (Morphology.Nanosyntax.NanoTree.leaf a).size = 1
• (Morphology.Nanosyntax.NanoTree.node a a_1).size = 1 + Morphology.Nanosyntax.NanoTree.size.sizeList a_1

def Morphology.Nanosyntax.NanoTree.size.sizeList {F : Type u_1} : List (NanoTree F) → ℕ

Equations

• Morphology.Nanosyntax.NanoTree.size.sizeList [] = 0
• Morphology.Nanosyntax.NanoTree.size.sizeList (t :: ts) = t.size + Morphology.Nanosyntax.NanoTree.size.sizeList ts

Containment (Superset Principle on trees)

inductive Morphology.Nanosyntax.NanoTree.Contains {F : Type u_1} : NanoTree F → NanoTree F → Prop

Contains self target: target occurs in self as a sub-constituent. Implements the tree-generalized Superset Principle ([Cah09] §2.2, [TTML18] (36)): entry M matches target S if M's stored tree contains S.

For right-branching single-daughter trees (all Bantu class prefix structures), this is equivalent to the bidirectional Matching relation ([TTML18] (35)).

For 1D chains: a chain of depth n contains all chains of depth k ≤ n, matching ExponenceRule.Matches (chain_contains_iff_le).

• refl {F : Type u_1} (t : NanoTree F) : t.Contains t
• child {F : Type u_1} {f : F} {cs : List (NanoTree F)} {c target : NanoTree F} : c ∈ cs → c.Contains target → (node f cs).Contains target

@[simp]

theorem Morphology.Nanosyntax.NanoTree.contains_leaf_iff {F : Type u_1} {f : F} {t : NanoTree F} : (leaf f).Contains t ↔ leaf f = t

theorem Morphology.Nanosyntax.NanoTree.contains_node_iff {F : Type u_1} {f : F} {cs : List (NanoTree F)} {t : NanoTree F} : (node f cs).Contains t ↔ node f cs = t ∨ ∃ c ∈ cs, c.Contains t

def Morphology.Nanosyntax.NanoTree.decContains {F : Type u_1} [DecidableEq F] (s t : NanoTree F) : Decidable (s.Contains t)

Structural decision procedure for containment (kernel-reducible).

Equations

• One or more equations did not get rendered due to their size.
• (Morphology.Nanosyntax.NanoTree.leaf f).decContains x✝ = if h : Morphology.Nanosyntax.NanoTree.leaf f = x✝ then isTrue ⋯ else isFalse ⋯

def Morphology.Nanosyntax.NanoTree.decContains.decAny {F : Type u_1} [DecidableEq F] (cs : List (NanoTree F)) (t : NanoTree F) : Decidable (∃ c ∈ cs, c.Contains t)

Does some member of cs contain t?

Equations

• One or more equations did not get rendered due to their size.
• Morphology.Nanosyntax.NanoTree.decContains.decAny [] t = isFalse ⋯

@[implicit_reducible]

instance Morphology.Nanosyntax.NanoTree.instDecidableContainsOfDecidableEq {F : Type u_1} [DecidableEq F] (s t : NanoTree F) : Decidable (s.Contains t)

Equations

• s.instDecidableContainsOfDecidableEq t = s.decContains t

Foot

def Morphology.Nanosyntax.NanoTree.foot {F : Type u_1} : NanoTree F → F

The foot of a tree: the feature at the bottom of the leftmost spine. For right-branching chains [Fn [... [F0]]], the foot is F0 — the deepest feature on the functional sequence.

Equations

• (Morphology.Nanosyntax.NanoTree.leaf f).foot = f
• (Morphology.Nanosyntax.NanoTree.node f []).foot = f
• (Morphology.Nanosyntax.NanoTree.node a (child :: tail)).foot = child.foot

Tree lexical entry

structure Morphology.Nanosyntax.TreeLexEntry (F : Type u_1) (α : Type u_2) : Type (max u_1 u_2)

A nanosyntactic lexical entry storing a tree rather than a scalar rank, paired with an exponent of type α (String in concrete fragments). The tree encodes the full feature geometry that the morpheme lexicalizes.

Contrast with ExponenceRule (Morphology/Containment/Vocabulary.lean) which stores only a span (depth on a 1D functional sequence).

• tree : NanoTree F

  The stored feature tree.

• exponent : α

  The exponent.

• morphType : MorphType

  Morphological type (suffix or prefix).

def Morphology.Nanosyntax.instReprTreeLexEntry.repr {F✝ : Type u_1} {α✝ : Type u_2} [Repr F✝] [Repr α✝] : TreeLexEntry F✝ α✝ → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Morphology.Nanosyntax.instReprTreeLexEntry {F✝ : Type u_1} {α✝ : Type u_2} [Repr F✝] [Repr α✝] : Repr (TreeLexEntry F✝ α✝)

Equations

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

def Morphology.Nanosyntax.TreeLexEntry.Matches {F : Type u_1} {α : Type u_2} (entry : TreeLexEntry F α) (target : NanoTree F) : Prop

A tree-based entry matches a target under the Superset Principle iff its stored tree contains the target as a sub-constituent.

Equations

• entry.Matches target = entry.tree.Contains target

@[implicit_reducible]

instance Morphology.Nanosyntax.instDecidableMatchesOfDecidableEq {F : Type u_1} {α : Type u_2} [DecidableEq F] (entry : TreeLexEntry F α) (target : NanoTree F) : Decidable (entry.Matches target)

Equations

• Morphology.Nanosyntax.instDecidableMatchesOfDecidableEq entry target = Morphology.Nanosyntax.instDecidableMatchesOfDecidableEq._aux_1 entry target

Tree spellout (Elsewhere Condition)

def Morphology.Nanosyntax.treeSpellout {F : Type u_1} {α : Type u_2} [DecidableEq F] (entries : List (TreeLexEntry F α)) (target : NanoTree F) : Option α

Phrasal spellout via the tree-generalized Superset Principle: among entries whose tree contains the target, select the one with the smallest tree (most specific match).

Parallels Morphology.Containment.spellout, but the matching relation is tree containment instead of rank comparison, and the specificity metric is tree size instead of rank.

Equations

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

Foot Condition

def Morphology.Nanosyntax.FootConditionMet {F : Type u_1} {α : Type u_2} (entry : TreeLexEntry F α) (syntacticTree : NanoTree F) : Prop

The Foot Condition ([TTML18]): the foot of a lexical entry's stored tree must be present as a feature in the syntactic structure being spelled out.

If entry M stores [X [...[Z]]], the Foot Condition requires that Z appear in the structure. This constrains backtracking: when spellout fails and the derivation splits the target into specifier + complement, only entries whose foot matches a feature in the remaining structure are eligible.

Equations

• Morphology.Nanosyntax.FootConditionMet entry syntacticTree = syntacticTree.Contains (Morphology.Nanosyntax.NanoTree.leaf entry.tree.foot)

@[implicit_reducible]

instance Morphology.Nanosyntax.instDecidableFootConditionMetOfDecidableEq {F : Type u_1} {α : Type u_2} [DecidableEq F] (entry : TreeLexEntry F α) (tree : NanoTree F) : Decidable (FootConditionMet entry tree)

Equations

• Morphology.Nanosyntax.instDecidableFootConditionMetOfDecidableEq entry tree = Morphology.Nanosyntax.instDecidableFootConditionMetOfDecidableEq._aux_1 entry tree

Chain trees (bridge to 1D)

def Morphology.Nanosyntax.chainTree {F : Type u_1} (feat : ℕ → F) : ℕ → NanoTree F

Build a right-branching chain tree of depth n. chainTree feat 0 = leaf (feat 0) chainTree feat 1 = node (feat 1) [leaf (feat 0)] chainTree feat n = node (feat n) [chainTree feat (n-1)]

A chain of depth n is isomorphic to an ExponenceRule spanning grade n in the 1D nanosyntax.

Equations

• Morphology.Nanosyntax.chainTree feat 0 = Morphology.Nanosyntax.NanoTree.leaf (feat 0)
• Morphology.Nanosyntax.chainTree feat n.succ = Morphology.Nanosyntax.NanoTree.node (feat (n + 1)) [Morphology.Nanosyntax.chainTree feat n]

Bridge theorems

theorem Morphology.Nanosyntax.chainTree_succ {F : Type u_1} (feat : ℕ → F) (n : ℕ) : chainTree feat (n + 1) = NanoTree.node (feat (n + 1)) [chainTree feat n]

theorem Morphology.Nanosyntax.chainTree_size {F : Type u_1} (feat : ℕ → F) (n : ℕ) : (chainTree feat n).size = n + 1

Chain tree size is n + 1 (one node per feature level).

theorem Morphology.Nanosyntax.chainTree_foot {F : Type u_1} (feat : ℕ → F) (n : ℕ) : (chainTree feat n).foot = feat 0

The foot of a chain tree is always feat 0 — the bottom of the functional sequence.

theorem Morphology.Nanosyntax.chainTree_injective {F : Type u_1} (feat : ℕ → F) : Function.Injective (chainTree feat)

Chains of distinct depths are distinct trees, regardless of the feature assignment — depth alone separates them.

theorem Morphology.Nanosyntax.chain_contains_iff_le {F : Type u_1} (feat : ℕ → F) (re r : ℕ) : (chainTree feat re).Contains (chainTree feat r) ↔ r ≤ re

For right-branching chains, tree containment reduces to rank comparison: a chain of depth re contains a chain of depth r iff r ≤ re. This is exactly the matching condition of the rank-based ExponenceRule.Matches, establishing that tree-based spellout generalizes (not replaces) rank-based spellout.

Unlike the previous Bool formulation, no injectivity of feat is needed: chain depth alone drives both directions.

Rose-tree interface instances

NanoTree joins the Core.Order.Branching tower. The structural size/decEq/decContains above remain the kernel-computable specializations ([file-level generality discipline]: WF-derived generics do not kernel-reduce, so decide-style spell-out evaluations need the structural forms).

@[implicit_reducible]

instance Morphology.Nanosyntax.NanoTree.instBranching {F : Type u_1} : Core.Order.Branching (NanoTree F)

Equations

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

@[simp]

theorem Morphology.Nanosyntax.NanoTree.branching_children_leaf {F : Type u_1} (f : F) : Core.Order.Branching.children (leaf f) = []

@[simp]

theorem Morphology.Nanosyntax.NanoTree.branching_children_node {F : Type u_1} (f : F) (cs : List (NanoTree F)) : Core.Order.Branching.children (node f cs) = cs

instance Morphology.Nanosyntax.NanoTree.instIsFiniteBranching {F : Type u_1} : Core.Order.IsFiniteBranching (NanoTree F)