Nanosyntax: the lexicalization algorithm

In nanosyntax features merge one at a time, and the phrase a merger creates must be lexicalized before the next feature merges. Starke's algorithm says what happens when no entry matches the new phrase. Material evacuates from the complement of the new feature, first the constituent holding the bottom of the sequence and then ever larger constituents around it, until the remnant is lexicalized. If no evacuation helps, the derivation returns to the previous merger and takes its next option. An evacuated constituent keeps its exponent and the remnant gets one of its own, so evacuation is what makes a suffix. A lexicalized constituent is pronounced as a whole, so an entry matching the new phrase, or the whole structure evacuation has built, overrides the exponents inside it.

Main definitions

• spine, merge, adjoin: syntactic objects, with labelled phrases and the unlabelled nodes evacuation creates.
• mergeOptions: the ways of lexicalizing a merger, in order of preference.
• derivations: the derivations of a feature sequence, in order of preference.
• spell: the exponents of a derivation, largest lexicalized constituents first.
• lexicalize, exponents: the first derivation and its exponents.

Main results

• derivations_append: deriving a sequence is deriving its first part and then, from each result in turn, the rest, which is backtracking.
• exists_matches_of_mem_lexicalize, exponents_eq_none_iff: every constituent of the derivation is matched by an entry, so a derivation is always pronounced.
• exponents_cons_of_forall_leaf, exponents_ofSupersetRule: where no entry lexicalizes a feature above the bottom alone the algorithm never evacuates, so on a lexicon of containment entries its one exponent is the containment engine's spellout.

Implementation notes

• A syntactic object is a tree with labels in Option F. A node labelled some f is the phrase of the feature f, with its complement as its one daughter, or none when the complement has evacuated. A node labelled none is unlabelled and has two daughters, an evacuated constituent and the remnant it left. Evacuation leaves no trace and projects no label.
• A derivation is the row of constituents along the left edge of its root. Its exponents are read off the finished structure, which is sound because a constituent once built is never changed, only merged over.
• mergeOptions follows the pied-piping formulation of the algorithm, which adds evacuations to Starke's original steps. On a lexicon whose trees have no unlabelled node only the original ones can be lexicalized (length_le_of_mem_mergeOptions).

TODO

• The algorithm's last resort, a specifier built in a workspace of its own, which is where prefixes come from. The literature differs on what such a derivation starts from.

References

• [Sta18]
• [DCCSVW25]
• [Cah09]

Syntactic objects

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

The right-branching phrase a feature sequence builds without evacuation, its first feature at the bottom.

Equations

• Morphology.Nanosyntax.spine f₀ fs = Morphology.Nanosyntax.phrase (some f₀) (List.map some fs)

@[reducible, inline]

abbrev Morphology.Nanosyntax.merge {F : Type u_1} (f : F) (t : RoseTree (Option F)) : RoseTree (Option F)

The phrase a feature projects over a complement.

Equations

• Morphology.Nanosyntax.merge f t = RoseTree.node (some f) [t]

@[reducible, inline]

abbrev Morphology.Nanosyntax.adjoin {F : Type u_1} (l r : RoseTree (Option F)) : RoseTree (Option F)

The unlabelled node an evacuated constituent forms with the remnant it left.

Equations

• Morphology.Nanosyntax.adjoin l r = RoseTree.node none [l, r]

@[simp]

theorem Morphology.Nanosyntax.spine_nil {F : Type u_1} (f₀ : F) : spine f₀ [] = RoseTree.leaf (some f₀)

@[simp]

theorem Morphology.Nanosyntax.spine_concat {F : Type u_1} (f₀ : F) (fs : List F) (f : F) : spine f₀ (fs ++ [f]) = merge f (spine f₀ fs)

@[reducible, inline]

abbrev Morphology.Nanosyntax.Derivation (F : Type u_3) : Type u_3

A derivation in progress is the row of constituents along the left edge of its root, the one holding the bottom of the feature sequence first and the remnants of evacuation after it.

Equations

• Morphology.Nanosyntax.Derivation F = List (RoseTree (Option F))

def Morphology.Nanosyntax.root {F : Type u_1} : Derivation F → Option (RoseTree (Option F))

The object a row of constituents forms, each remnant adjoined to what evacuated from it.

Equations

• Morphology.Nanosyntax.root [] = none
• Morphology.Nanosyntax.root (t :: ts) = some (List.foldl Morphology.Nanosyntax.adjoin t ts)

@[simp]

theorem Morphology.Nanosyntax.root_nil {F : Type u_1} : root [] = none

@[simp]

theorem Morphology.Nanosyntax.root_singleton {F : Type u_1} (t : RoseTree (Option F)) : root [t] = some t

theorem Morphology.Nanosyntax.root_concat {F : Type u_1} {d : Derivation F} (hd : d ≠ []) (t : RoseTree (Option F)) : root (d ++ [t]) = Option.map (fun (x : RoseTree (Option F)) => adjoin x t) (root d)

theorem Morphology.Nanosyntax.value_eq_none_of_root {F : Type u_1} {d : Derivation F} {t : RoseTree (Option F)} (h : root d = some t) (hd : 2 ≤ List.length d) : t.value = none

The root of a row of two or more constituents is unlabelled.

One merger

def Morphology.Nanosyntax.mergeOptions {F : Type u_1} {α : Type u_2} [DecidableEq F] (L : Exponence.RuleSet (LexicalEntry (Option F) α)) (d : Derivation F) (f : F) : List (Derivation F)

The ways of lexicalizing the merger of a feature with a derivation, in order of preference. The new phrase is lexicalized whole, or the first j constituents of its complement evacuate and the remnant is lexicalized, for j from one up to all of them.

Equations

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

theorem Morphology.Nanosyntax.mem_mergeOptions {F : Type u_1} {α : Type u_2} [DecidableEq F] {L : Exponence.RuleSet (LexicalEntry (Option F) α)} {f : F} {d d' : Derivation F} : d' ∈ mergeOptions L d f ↔ ∃ j ≤ List.length d, (treeSpellout L (RoseTree.node (some f) (root (List.drop j d)).toList)).isSome = true ∧ d' = List.take j d ++ [RoseTree.node (some f) (root (List.drop j d)).toList]

theorem Morphology.Nanosyntax.mergeOptions_nil {F : Type u_1} {α : Type u_2} [DecidableEq F] (L : Exponence.RuleSet (LexicalEntry (Option F) α)) (f : F) : mergeOptions L [] f = (Option.map (fun (x : α) => [RoseTree.leaf (some f)]) (treeSpellout L (RoseTree.leaf (some f)))).toList

The first feature is lexicalized as a phrase of its own.

theorem Morphology.Nanosyntax.mergeOptions_singleton {F : Type u_1} {α : Type u_2} [DecidableEq F] (L : Exponence.RuleSet (LexicalEntry (Option F) α)) (t : RoseTree (Option F)) (f : F) : mergeOptions L [t] f = (Option.map (fun (x : α) => [merge f t]) (treeSpellout L (merge f t))).toList ++ (Option.map (fun (x : α) => [t, RoseTree.leaf (some f)]) (treeSpellout L (RoseTree.leaf (some f)))).toList

A feature merged with a single constituent is lexicalized together with it, or else the constituent evacuates and the feature is lexicalized alone, as a suffix.

theorem Morphology.Nanosyntax.length_le_of_mem_mergeOptions {F : Type u_1} {α : Type u_2} [DecidableEq F] {L : Exponence.RuleSet (LexicalEntry (Option F) α)} {f : F} (hL : ∀ e ∈ L, ∀ (t : RoseTree (Option F)), t.IsSubtree e.tree → t.value ≠ none) {d d' : Derivation F} (h : d' ∈ mergeOptions L d f) : List.length d ≤ List.length d'

On a lexicon whose stored trees have no unlabelled node a merger never fuses constituents. It grows the last one, everything before it evacuating, or adds one, everything evacuating, which are the specifier-to-specifier and complement movements of Starke's original steps.

Derivations

def Morphology.Nanosyntax.derivations {F : Type u_1} {α : Type u_2} [DecidableEq F] (L : Exponence.RuleSet (LexicalEntry (Option F) α)) : Derivation F → List F → List (Derivation F)

The derivations of a feature sequence from a derivation, in order of preference. Each merger takes its options in turn and the rest of the sequence is derived from each.

Equations

• One or more equations did not get rendered due to their size.
• Morphology.Nanosyntax.derivations L x✝ [] = [x✝]

@[simp]

theorem Morphology.Nanosyntax.derivations_nil {F : Type u_1} {α : Type u_2} [DecidableEq F] {L : Exponence.RuleSet (LexicalEntry (Option F) α)} (d : Derivation F) : derivations L d [] = [d]

@[simp]

theorem Morphology.Nanosyntax.derivations_cons {F : Type u_1} {α : Type u_2} [DecidableEq F] {L : Exponence.RuleSet (LexicalEntry (Option F) α)} (d : Derivation F) (f : F) (fs : List F) : derivations L d (f :: fs) = List.flatMap (fun (x : Derivation F) => derivations L x fs) (mergeOptions L d f)

theorem Morphology.Nanosyntax.derivations_singleton {F : Type u_1} {α : Type u_2} [DecidableEq F] {L : Exponence.RuleSet (LexicalEntry (Option F) α)} (d : Derivation F) (f : F) : derivations L d [f] = mergeOptions L d f

theorem Morphology.Nanosyntax.derivations_append {F : Type u_1} {α : Type u_2} [DecidableEq F] {L : Exponence.RuleSet (LexicalEntry (Option F) α)} (d : Derivation F) (fs gs : List F) : derivations L d (fs ++ gs) = List.flatMap (fun (x : Derivation F) => derivations L x gs) (derivations L d fs)

Deriving a sequence is deriving its first part and then the rest from each result in turn, so a failure in the rest returns to the latest merger of the first part with an option left.

def Morphology.Nanosyntax.lexicalize {F : Type u_1} {α : Type u_2} [DecidableEq F] (L : Exponence.RuleSet (LexicalEntry (Option F) α)) (fs : List F) : Option (Derivation F)

The lexicalization algorithm returns the first derivation of a feature sequence, the bottom of the sequence first.

Equations

• Morphology.Nanosyntax.lexicalize L fs = (Morphology.Nanosyntax.derivations L [] fs).head?

Exponents

def Morphology.Nanosyntax.spellAux {F : Type u_1} {α : Type u_2} [DecidableEq F] (L : Exponence.RuleSet (LexicalEntry (Option F) α)) : Derivation F → Option (List α)

The exponents of a row given last constituent first. The whole row gets one exponent where an entry matches the object it forms, and otherwise its last constituent gets its own after the exponents of the rest.

Equations

• One or more equations did not get rendered due to their size.
• Morphology.Nanosyntax.spellAux L [] = some []

def Morphology.Nanosyntax.spell {F : Type u_1} {α : Type u_2} [DecidableEq F] (L : Exponence.RuleSet (LexicalEntry (Option F) α)) (d : Derivation F) : Option (List α)

The exponents of a derivation, in linear order. A lexicalized constituent is pronounced as a whole, so the longest initial part of the row forming a lexicalized object gets one exponent and each constituent after it its own.

Equations

• Morphology.Nanosyntax.spell L d = Morphology.Nanosyntax.spellAux L (List.reverse d)

@[simp]

theorem Morphology.Nanosyntax.spell_nil {F : Type u_1} {α : Type u_2} [DecidableEq F] {L : Exponence.RuleSet (LexicalEntry (Option F) α)} : spell L [] = some []

theorem Morphology.Nanosyntax.spell_concat {F : Type u_1} {α : Type u_2} [DecidableEq F] {L : Exponence.RuleSet (LexicalEntry (Option F) α)} (d : Derivation F) (t : RoseTree (Option F)) : spell L (d ++ [t]) = (Option.map (fun (x : α) => [x]) ((root (d ++ [t])).bind (treeSpellout L)) <|> (spell L d).bind fun (xs : List α) => Option.map (fun (x : α) => xs ++ [x]) (treeSpellout L t))

@[simp]

theorem Morphology.Nanosyntax.spell_singleton {F : Type u_1} {α : Type u_2} [DecidableEq F] {L : Exponence.RuleSet (LexicalEntry (Option F) α)} (t : RoseTree (Option F)) : spell L [t] = Option.map (fun (x : α) => [x]) (treeSpellout L t)

theorem Morphology.Nanosyntax.spell_isSome {F : Type u_1} {α : Type u_2} [DecidableEq F] {L : Exponence.RuleSet (LexicalEntry (Option F) α)} {d : Derivation F} (h : ∀ t ∈ d, (treeSpellout L t).isSome = true) : (spell L d).isSome = true

A row is pronounced as soon as each of its constituents is lexicalized.

def Morphology.Nanosyntax.exponents {F : Type u_1} {α : Type u_2} [DecidableEq F] (L : Exponence.RuleSet (LexicalEntry (Option F) α)) (fs : List F) : Option (List α)

The exponents the algorithm gives a feature sequence, in linear order.

Equations

• Morphology.Nanosyntax.exponents L fs = (Morphology.Nanosyntax.lexicalize L fs).bind (Morphology.Nanosyntax.spell L)

Soundness

theorem Morphology.Nanosyntax.exists_matches_of_mem_lexicalize {F : Type u_1} {α : Type u_2} [DecidableEq F] {L : Exponence.RuleSet (LexicalEntry (Option F) α)} {d : Derivation F} {fs : List F} (h : lexicalize L fs = some d) {t : RoseTree (Option F)} (ht : t ∈ d) : ∃ e ∈ L, e.Matches t

Every constituent of the derivation the algorithm returns is matched by an entry.

theorem Morphology.Nanosyntax.exponents_eq_none_iff {F : Type u_1} {α : Type u_2} [DecidableEq F] {L : Exponence.RuleSet (LexicalEntry (Option F) α)} {fs : List F} : exponents L fs = none ↔ lexicalize L fs = none

A sequence the algorithm derives is pronounced.

Short sequences

theorem Morphology.Nanosyntax.exponents_singleton {F : Type u_1} {α : Type u_2} [DecidableEq F] (L : Exponence.RuleSet (LexicalEntry (Option F) α)) (f : F) : exponents L [f] = Option.map (fun (x : α) => [x]) (treeSpellout L (RoseTree.leaf (some f)))

theorem Morphology.Nanosyntax.exponents_pair {F : Type u_1} {α : Type u_2} [DecidableEq F] (L : Exponence.RuleSet (LexicalEntry (Option F) α)) (f₁ f₂ : F) : exponents L [f₁, f₂] = (treeSpellout L (RoseTree.leaf (some f₁))).bind fun (x : α) => Option.map (fun (y : α) => [y]) (treeSpellout L (merge f₂ (RoseTree.leaf (some f₁)))) <|> (treeSpellout L (RoseTree.leaf (some f₂))).bind fun (y : α) => Option.map (fun (z : α) => [z]) (treeSpellout L (adjoin (RoseTree.leaf (some f₁)) (RoseTree.leaf (some f₂)))) <|> some [x, y]

A sequence of two features gets one exponent for its whole phrase, or else the exponent of its first feature followed by a suffix for the second, unless an entry matches the two phrases together.

Lexicons without suffixes

theorem Morphology.Nanosyntax.mergeOptions_singleton_of_leaf {F : Type u_1} {α : Type u_2} [DecidableEq F] {L : Exponence.RuleSet (LexicalEntry (Option F) α)} {f : F} (h : treeSpellout L (RoseTree.leaf (some f)) = none) (t : RoseTree (Option F)) : mergeOptions L [t] f = (Option.map (fun (x : α) => [merge f t]) (treeSpellout L (merge f t))).toList

Where no entry lexicalizes a feature alone, merging it with a single constituent can only grow the constituent.

theorem Morphology.Nanosyntax.derivations_cons_of_forall_leaf {F : Type u_1} {α : Type u_2} [DecidableEq F] {L : Exponence.RuleSet (LexicalEntry (Option F) α)} (f₀ : F) {fs : List F} (h : ∀ f ∈ fs, treeSpellout L (RoseTree.leaf (some f)) = none) : derivations L [] (f₀ :: fs) = (Option.map (fun (x : α) => [spine f₀ fs]) (treeSpellout L (spine f₀ fs))).toList

Where no entry lexicalizes a feature above the bottom alone, the algorithm never evacuates, and the sequence has at most one derivation, its one phrase lexicalized whole.

theorem Morphology.Nanosyntax.exponents_cons_of_forall_leaf {F : Type u_1} {α : Type u_2} [DecidableEq F] {L : Exponence.RuleSet (LexicalEntry (Option F) α)} (f₀ : F) {fs : List F} (h : ∀ f ∈ fs, treeSpellout L (RoseTree.leaf (some f)) = none) : exponents L (f₀ :: fs) = Option.map (fun (x : α) => [x]) (treeSpellout L (spine f₀ fs))

Where no entry lexicalizes a feature above the bottom alone, the sequence gets a single exponent, that of its one phrase, or none.

theorem Morphology.Nanosyntax.exponents_ofSupersetRule {F : Type u_1} {α : Type u_2} [DecidableEq F] {n : ℕ} {feat : ℕ → F} (hf : Function.Injective feat) (v : Exponence.RuleSet (Containment.SupersetRule n α)) (g : Fin n) : exponents (List.map (LexicalEntry.ofSupersetRule (some ∘ feat)) v) (List.map feat (List.range (↑g + 1))) = Option.map (fun (x : α) => [x]) (Containment.spellout v g)

On a lexicon of containment entries the algorithm never evacuates, and it gives each grade the single exponent the containment engine spells out there.