Nanosyntax: phrasal spellout over feature trees

In nanosyntax a lexical entry pairs an exponent with a stored tree of features, one feature per node. Caha, after Starke, lets an entry spell out a syntactic tree when the stored tree has a subtree identical to it, the Superset Principle, which is RoseTree.IsSubtree. When several entries match, the Elsewhere Condition prefers the one that matches in fewer environments, and since a matching stored tree exceeds the syntactic tree by exactly its superfluous material, that is the matching entry with the smallest tree. The Foot Condition asks the lowest feature of a stored tree to occur in what it spells out. Taraldsen's matching relation instead pairs a node of the stored tree with the root of the syntactic tree and requires their daughters to match each other both ways; it agrees with containment on right-branching chains, where tree spellout is also the spellout of the containment engine.

Main definitions

• LexicalEntry: a stored feature tree paired with an exponent.
• LexicalEntry.Matches, treeSelect, treeSpellout: the Superset Principle and the Elsewhere Condition.
• foot, FootConditionMet: the Foot Condition.
• Matching: Taraldsen's matching relation.
• chainTree, phrase, LexicalEntry.ofSupersetRule: right-branching chains, and the containment engine's entries read as chain entries.

Main results

• LexicalEntry.le_iff: specificity is reverse containment of the stored trees.
• treeSelect_isElsewhereWinner: smallest-tree selection picks an Elsewhere winner.
• footConditionMet_of_matches_chainTree: an entry storing a chain meets the Foot Condition wherever it matches, so the condition constrains only entries with branching trees.
• matching_chainTree_iff, exists_matching_not_isSubtree: Taraldsen's matching is containment on chains but ignores the order of daughters in general.
• treeSpellout_ofSupersetRule: on chains, tree spellout is the containment engine's spellout.

Implementation notes

• Trees are over any type of labels. The lexicalization algorithm (Nanosyntax/Lexicalization.lean) takes labels in Option F: a node labelled by a feature is that feature's phrase over its complement, and an unlabelled node joins an evacuated constituent to the remnant it left. A bare head merged as a complement is not told apart from a phrase of one feature, so a stored tree does not record whether its foot is unary or binary, the difference Starke draws between suffixes and prefixes.
• Matching is the rigid Superset Principle of Caha's (6), identity of a subtree. The algorithm follows the later formulation in which evacuation leaves no trace, so it needs no matching that ignores traces.

References

• [Sta09a]
• [Cah09]
• [Sta18]
• [Tar18]
• [TTML18]

Lexical entries and matching

structure Morphology.Nanosyntax.LexicalEntry (F : Type u_3) (α : Type u_4) : Type (max u_3 u_4)

A nanosyntactic lexical entry pairs a stored feature tree with its exponent.

• tree : RoseTree F

  The stored feature tree.

• exponent : α

  The exponent.

def Morphology.Nanosyntax.instReprLexicalEntry.repr {F✝ : Type u_3} {α✝ : Type u_4} [Repr F✝] [Repr α✝] : LexicalEntry F✝ α✝ → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Morphology.Nanosyntax.instReprLexicalEntry {F✝ : Type u_3} {α✝ : Type u_4} [Repr F✝] [Repr α✝] : Repr (LexicalEntry F✝ α✝)

Equations

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

def Morphology.Nanosyntax.LexicalEntry.Matches {F : Type u_1} {α : Type u_2} (e : LexicalEntry F α) (t : RoseTree F) : Prop

An entry matches a syntactic tree when its stored tree has a subtree identical to it, the Superset Principle of [Cah09] (6).

Equations

• e.Matches t = t.IsSubtree e.tree

@[instance_reducible]

instance Morphology.Nanosyntax.instDecidableMatchesOfDecidableEq {F : Type u_1} {α : Type u_2} [DecidableEq F] (e : LexicalEntry F α) (t : RoseTree F) : Decidable (e.Matches t)

Equations

• Morphology.Nanosyntax.instDecidableMatchesOfDecidableEq e t = { decide := decide (t ∈ e.tree.subtrees), reflects_decide := ⋯ }

@[instance_reducible]

instance Morphology.Nanosyntax.instRuleLexicalEntryRoseTree {F : Type u_1} {α : Type u_2} : Exponence.Rule (LexicalEntry F α) (RoseTree F) α

A lexical entry is a rule of the exponence core, applicable where it matches.

Equations

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

@[instance_reducible]

instance Morphology.Nanosyntax.instPreorderLexicalEntry {F : Type u_1} {α : Type u_2} : Preorder (LexicalEntry F α)

Equations

• Morphology.Nanosyntax.instPreorderLexicalEntry = Morphology.Exponence.toPreorder

theorem Morphology.Nanosyntax.LexicalEntry.le_iff {F : Type u_1} {α : Type u_2} {a b : LexicalEntry F α} : a ≤ b ↔ a.tree.IsSubtree b.tree

One entry is at least as specific as another exactly when the other's stored tree contains its stored tree.

Spellout

@[instance_reducible]

instance Morphology.Nanosyntax.instDecidableRelLexicalEntryRoseTreeApplies {F : Type u_1} {α : Type u_2} [DecidableEq F] : DecidableRel Exponence.Applies

Equations

• Morphology.Nanosyntax.instDecidableRelLexicalEntryRoseTreeApplies e t = { decide := decide (t ∈ e.tree.subtrees), reflects_decide := ⋯ }

def Morphology.Nanosyntax.treeSelect {F : Type u_1} {α : Type u_2} [DecidableEq F] (entries : Exponence.RuleSet (LexicalEntry F α)) (t : RoseTree F) : Option (LexicalEntry F α)

treeSelect entries t is the matching entry with the smallest stored tree, the first listed on ties.

Equations

• Morphology.Nanosyntax.treeSelect entries t = entries.selectBy (fun (e : Morphology.Nanosyntax.LexicalEntry F α) => OrderDual.toDual e.tree.numNodes) t

def Morphology.Nanosyntax.treeSpellout {F : Type u_1} {α : Type u_2} [DecidableEq F] (entries : Exponence.RuleSet (LexicalEntry F α)) (t : RoseTree F) : Option α

treeSpellout entries t is the exponent of the entry treeSelect picks.

Equations

• Morphology.Nanosyntax.treeSpellout entries t = Option.map (fun (x : Morphology.Nanosyntax.LexicalEntry F α) => x.exponent) (Morphology.Nanosyntax.treeSelect entries t)

theorem Morphology.Nanosyntax.treeSelect_isElsewhereWinner {F : Type u_1} {α : Type u_2} [DecidableEq F] {entries : Exponence.RuleSet (LexicalEntry F α)} {t : RoseTree F} {e : LexicalEntry F α} (h : treeSelect entries t = some e) : entries.IsElsewhereWinner t e

Smallest-tree selection picks an Elsewhere winner.

theorem Morphology.Nanosyntax.treeSpellout_isElsewhereWinner {F : Type u_1} {α : Type u_2} [DecidableEq F] {entries : Exponence.RuleSet (LexicalEntry F α)} {t : RoseTree F} {x : α} (h : treeSpellout entries t = some x) : ∃ e ∈ entries, e.exponent = x ∧ entries.IsElsewhereWinner t e

The spelled-out exponent is the exponent of an Elsewhere winner.

theorem Morphology.Nanosyntax.treeSpellout_eq_none_iff {F : Type u_1} {α : Type u_2} [DecidableEq F] {entries : Exponence.RuleSet (LexicalEntry F α)} {t : RoseTree F} : treeSpellout entries t = none ↔ ∀ e ∈ entries, ¬e.Matches t

A tree is spelled out exactly when some entry matches it.

theorem Morphology.Nanosyntax.treeSpellout_eq_none_of_isSubtree {F : Type u_1} {α : Type u_2} [DecidableEq F] {entries : Exponence.RuleSet (LexicalEntry F α)} {s t : RoseTree F} (hst : s.IsSubtree t) (h : treeSpellout entries s = none) : treeSpellout entries t = none

Spellout gaps propagate to containing trees, since an entry matching a tree matches its subtrees.

The Foot Condition

def Morphology.Nanosyntax.foot {F : Type u_1} (t : RoseTree F) : F

The foot of a tree is its lowest feature on the complement line, its last leaf.

Equations

• Morphology.Nanosyntax.foot t = t.leafList.getLast ⋯

def Morphology.Nanosyntax.FootConditionMet {F : Type u_1} {α : Type u_2} (e : LexicalEntry F α) (t : RoseTree F) : Prop

The Foot Condition ([TTML18] (39)) requires a syntactic tree an entry spells out to contain the foot of the entry's stored tree.

Equations

• Morphology.Nanosyntax.FootConditionMet e t = (Morphology.Nanosyntax.foot e.tree ∈ t.leafList)

@[instance_reducible]

instance Morphology.Nanosyntax.instDecidableFootConditionMetOfDecidableEq {F : Type u_1} {α : Type u_2} [DecidableEq F] (e : LexicalEntry F α) (t : RoseTree F) : Decidable (FootConditionMet e t)

Equations

• Morphology.Nanosyntax.instDecidableFootConditionMetOfDecidableEq e t = { decide := decide (List.elem (Morphology.Nanosyntax.foot e.tree) t.leafList = true), reflects_decide := ⋯ }

theorem Morphology.Nanosyntax.footConditionMet_of_foot_eq {F : Type u_1} {α : Type u_2} {e : LexicalEntry F α} {t : RoseTree F} (h : foot t = foot e.tree) : FootConditionMet e t

The Foot Condition holds of every syntactic tree that shares its foot with the stored tree.

Chains

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

chainTree feat n is the right-branching chain [feat n [… [feat 0]]].

Equations

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

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

theorem Morphology.Nanosyntax.leafList_chainTree {F : Type u_1} (feat : ℕ → F) (n : ℕ) : (chainTree feat n).leafList = [feat 0]

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

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

theorem Morphology.Nanosyntax.chainTree_isSubtree_iff {F : Type u_1} (feat : ℕ → F) (r k : ℕ) : (chainTree feat r).IsSubtree (chainTree feat k) ↔ r ≤ k

On chains, containment is rank comparison, whatever the features.

theorem Morphology.Nanosyntax.eq_chainTree_of_isSubtree {F : Type u_1} {feat : ℕ → F} {k : ℕ} {t : RoseTree F} (h : t.IsSubtree (chainTree feat k)) : ∃ r ≤ k, t = chainTree feat r

The subtrees of a chain are its lower segments.

def Morphology.Nanosyntax.phrase {F : Type u_1} (f₀ : F) (fs : List F) : RoseTree F

The right-branching phrase a feature sequence builds on its first feature, each feature taking what is below it as its complement.

Equations

• Morphology.Nanosyntax.phrase f₀ fs = List.foldl (fun (t : RoseTree F) (f : F) => RoseTree.node f [t]) (RoseTree.leaf f₀) fs

@[simp]

theorem Morphology.Nanosyntax.phrase_nil {F : Type u_1} (f₀ : F) : phrase f₀ [] = RoseTree.leaf f₀

@[simp]

theorem Morphology.Nanosyntax.phrase_concat {F : Type u_1} (f₀ : F) (fs : List F) (f : F) : phrase f₀ (fs ++ [f]) = RoseTree.node f [phrase f₀ fs]

theorem Morphology.Nanosyntax.chainTree_eq_phrase {F : Type u_1} (feat : ℕ → F) (k : ℕ) : chainTree feat k = phrase (feat 0) (List.map (feat ∘ Nat.succ) (List.range k))

theorem Morphology.Nanosyntax.footConditionMet_of_matches_chainTree {F : Type u_1} {α : Type u_2} {e : LexicalEntry F α} {feat : ℕ → F} {k : ℕ} (he : e.tree = chainTree feat k) {t : RoseTree F} (h : e.Matches t) : FootConditionMet e t

An entry storing a chain meets the Foot Condition wherever it matches.

Taraldsen's matching relation

@[irreducible]

def Morphology.Nanosyntax.MatchesRoot {F : Type u_1} : RoseTree F → RoseTree F → Prop

MatchesRoot s u holds when the roots of s and u carry the same feature and every daughter of each root-matches some daughter of the other, the two clauses of [Tar18] (3) and [TTML18] (35).

Equations

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

theorem Morphology.Nanosyntax.matchesRoot_node_iff {F : Type u_1} {f g : F} {cs ds : List (RoseTree F)} : MatchesRoot (RoseTree.node f cs) (RoseTree.node g ds) ↔ f = g ∧ (∀ c ∈ cs, ∃ d ∈ ds, MatchesRoot c d) ∧ ∀ d ∈ ds, ∃ c ∈ cs, MatchesRoot c d

theorem Morphology.Nanosyntax.MatchesRoot.refl {F : Type u_1} (t : RoseTree F) : MatchesRoot t t

def Morphology.Nanosyntax.Matching {F : Type u_1} (s t : RoseTree F) : Prop

A syntactic tree s matches a stored tree t when the root of s root-matches some node of t.

Equations

• Morphology.Nanosyntax.Matching s t = ∃ (u : RoseTree F), u.IsSubtree t ∧ Morphology.Nanosyntax.MatchesRoot s u

theorem Morphology.Nanosyntax.Matching.of_isSubtree {F : Type u_1} {s t : RoseTree F} (h : s.IsSubtree t) : Matching s t

A subtree matches, so the Superset Principle follows from Taraldsen's matching ([TTML18] (36)).

theorem Morphology.Nanosyntax.matchesRoot_chainTree_iff {F : Type u_1} (feat : ℕ → F) (r k : ℕ) : MatchesRoot (chainTree feat r) (chainTree feat k) ↔ r = k

On chains, root-matching is equality of depths.

theorem Morphology.Nanosyntax.matching_chainTree_iff {F : Type u_1} (feat : ℕ → F) (r k : ℕ) : Matching (chainTree feat r) (chainTree feat k) ↔ (chainTree feat r).IsSubtree (chainTree feat k)

On chains, Taraldsen's matching is containment.

theorem Morphology.Nanosyntax.exists_matching_not_isSubtree : ∃ (s : RoseTree Bool) (t : RoseTree Bool), Matching s t ∧ ¬s.IsSubtree t

Taraldsen's matching ignores the order of daughters, which containment does not. It also ignores repeated daughters.

Spellout over containment hierarchies

def Morphology.Nanosyntax.LexicalEntry.ofSupersetRule {F : Type u_1} {α : Type u_2} {n : ℕ} (feat : ℕ → F) (e : Containment.SupersetRule n α) : LexicalEntry F α

An entry of the containment engine read as an entry storing the chain up to its span.

Equations

• Morphology.Nanosyntax.LexicalEntry.ofSupersetRule feat e = { tree := Morphology.Nanosyntax.chainTree feat ↑e.spans, exponent := e.exponent }

theorem Morphology.Nanosyntax.treeSpellout_ofSupersetRule {F : Type u_1} {α : Type u_2} [DecidableEq F] {n : ℕ} (feat : ℕ → F) (v : Exponence.RuleSet (Containment.SupersetRule n α)) (g : Fin n) : treeSpellout (List.map (LexicalEntry.ofSupersetRule feat) v) (chainTree feat ↑g) = Containment.spellout v g

On chains, tree spellout is the spellout of the containment engine, since containment of chains is comparison of their ranks.