Nanosyntax: Tree-Based Spellout

@cite{taraldsen-et-al-2018} @cite{caha-2009} @cite{starke-2009}

Extension of rank-based nanosyntax (Core.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. Among matching entries, the Elsewhere Condition selects the smallest (by tree size).

The SP on trees is a consequence of @cite{starke-2009}'s Matching relation (formalized in @cite{taraldsen-et-al-2018} 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 (NanoTree.contains) and bidirectional Matching coincide. The implementation uses containment as the simpler equivalent formulation.

This generalization is needed for @cite{taraldsen-et-al-2018}'s analysis of Bantu class prefixes, where lexical entries store phrasal trees [# Nx] rather than scalar ranks on a case fseq.

Bridge to rank-based spellout

For right-branching chains (single-daughter trees), tree-based spellout reduces to rank-based spellout. A chain of depth n is isomorphic to a rank-n LexEntry from Core.lean.

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

A nanosyntactic feature tree. Simpler than Core.Tree — 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} : F → NanoTree F
• node {F : Type} : F → List (NanoTree F) → NanoTree F

@[implicit_reducible]

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

Equations

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

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

def Morphology.Nanosyntax.NanoTree.beq {F : Type} [BEq F] : NanoTree F → NanoTree F → Bool

Structural equality for nanosyntactic trees. Defined manually (not via deriving BEq) so that equations are transparent and available for rfl/simp proofs.

Equations

• (Morphology.Nanosyntax.NanoTree.leaf f).beq (Morphology.Nanosyntax.NanoTree.leaf g) = (f == g)
• (Morphology.Nanosyntax.NanoTree.node f cs).beq (Morphology.Nanosyntax.NanoTree.node g ds) = (f == g && Morphology.Nanosyntax.NanoTree.beq.beqList cs ds)
• x✝¹.beq x✝ = false

def Morphology.Nanosyntax.NanoTree.beq.beqList {F : Type} [BEq F] : List (NanoTree F) → List (NanoTree F) → Bool

Equations

• Morphology.Nanosyntax.NanoTree.beq.beqList [] [] = true
• Morphology.Nanosyntax.NanoTree.beq.beqList (a :: as) (b :: bs) = (a.beq b && Morphology.Nanosyntax.NanoTree.beq.beqList as bs)
• Morphology.Nanosyntax.NanoTree.beq.beqList a✝¹ a✝ = false

@[implicit_reducible]

instance Morphology.Nanosyntax.NanoTree.instBEq {F : Type} [BEq F] : BEq (NanoTree F)

Equations

• Morphology.Nanosyntax.NanoTree.instBEq = { beq := Morphology.Nanosyntax.NanoTree.beq }

@[simp]

theorem Morphology.Nanosyntax.NanoTree.beq_leaf_leaf {F : Type} [BEq F] (f g : F) : (leaf f == leaf g) = (f == g)

@[simp]

theorem Morphology.Nanosyntax.NanoTree.beq_leaf_node {F : Type} [BEq F] (f g : F) (cs : List (NanoTree F)) : (leaf f == node g cs) = false

@[simp]

theorem Morphology.Nanosyntax.NanoTree.beq_node_leaf {F : Type} [BEq F] (f : F) (cs : List (NanoTree F)) (g : F) : (node f cs == leaf g) = false

@[simp]

theorem Morphology.Nanosyntax.NanoTree.beq_node_node {F : Type} [BEq F] (f g : F) (cs ds : List (NanoTree F)) : (node f cs == node g ds) = (f == g && beq.beqList cs ds)

@[simp]

theorem Morphology.Nanosyntax.NanoTree.beqList_nil {F : Type} [BEq F] : beq.beqList [] [] = true

@[simp]

theorem Morphology.Nanosyntax.NanoTree.beqList_cons {F : Type} [BEq F] (a b : NanoTree F) (as bs : List (NanoTree F)) : beq.beqList (a :: as) (b :: bs) = (a == b && beq.beqList as bs)

def Morphology.Nanosyntax.NanoTree.size {F : Type} : 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} : 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

def Morphology.Nanosyntax.NanoTree.contains {F : Type} [BEq F] : NanoTree F → NanoTree F → Bool

Does self contain target as a sub-constituent? Implements the tree-generalized Superset Principle (@cite{caha-2009} §2.2, @cite{taraldsen-et-al-2018} (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 (@cite{taraldsen-et-al-2018} (35)).

For 1D chains: a chain of depth n contains all chains of depth k <= n, matching LexEntry.matches.

Equations

• (Morphology.Nanosyntax.NanoTree.leaf f).contains x✝ = (Morphology.Nanosyntax.NanoTree.leaf f == x✝)
• (Morphology.Nanosyntax.NanoTree.node f children).contains x✝ = (Morphology.Nanosyntax.NanoTree.node f children == x✝ || Morphology.Nanosyntax.NanoTree.contains.containsList children x✝)

def Morphology.Nanosyntax.NanoTree.contains.containsList {F : Type} [BEq F] : List (NanoTree F) → NanoTree F → Bool

Equations

• Morphology.Nanosyntax.NanoTree.contains.containsList [] a✝ = false
• Morphology.Nanosyntax.NanoTree.contains.containsList (c :: cs) a✝ = (c.contains a✝ || Morphology.Nanosyntax.NanoTree.contains.containsList cs a✝)

def Morphology.Nanosyntax.NanoTree.foot {F : Type} : 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

structure Morphology.Nanosyntax.TreeLexEntry (F : Type) : Type

A nanosyntactic lexical entry storing a tree rather than a scalar rank. The tree encodes the full feature geometry that the morpheme lexicalizes.

Contrast with LexEntry (Core.lean) which stores only a rank (depth on a 1D functional sequence).

• tree : NanoTree F

  The stored feature tree.

• exponent : String

  The phonological exponent.

• morphType : MorphType

  Morphological type (suffix or prefix).

def Morphology.Nanosyntax.instReprTreeLexEntry.repr {F✝ : Type} [Repr F✝] : 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} [Repr F✝] : Repr (TreeLexEntry F✝)

Equations

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

def Morphology.Nanosyntax.TreeLexEntry.matches {F : Type} [BEq F] (entry : TreeLexEntry F) (target : NanoTree F) : Bool

Does a tree-based entry match a target under the Superset Principle? The entry matches if its tree contains the target as a sub-constituent.

Equations

• entry.matches target = entry.tree.contains target

def Morphology.Nanosyntax.treeSpellout {F : Type} [BEq F] (entries : List (TreeLexEntry F)) (target : NanoTree F) : Option String

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 spellout from Core.lean, 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.

def Morphology.Nanosyntax.footConditionMet {F : Type} [BEq F] (entry : TreeLexEntry F) (syntacticTree : NanoTree F) : Bool

The Foot Condition (@cite{taraldsen-et-al-2018}): 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)

def Morphology.Nanosyntax.chainTree {F : Type} (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 a rank-n LexEntry 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]

theorem Morphology.Nanosyntax.chainTree_size {F : Type} (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} (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.chain_contains_iff_ge {F : Type} [DecidableEq F] (feat : ℕ → F) (hInj : Function.Injective feat) (re r : ℕ) : (chainTree feat re).contains (chainTree feat r) = decide (re ≥ r)

For right-branching chains with injective features, tree containment reduces to rank comparison: a chain of depth re contains a chain of depth r iff re >= r.

This is exactly the matching condition of the rank-based LexEntry.matches, establishing that tree-based spellout generalizes (not replaces) rank-based spellout.