De Clercq et al. (2025): Nanosyntax: State of the art and recent developments

De Clercq, Caha, Starke and Vanden Wyngaerd present the lexicalization algorithm through case studies, which this file runs. In the degrees of comparison the size of the root decides how many suffixes an adjective takes, and an entry matching a larger phrase overrides the exponents inside it. In Czech declension a root that lexicalizes the accusative by itself shrinks in the genitive, the derivation going back to an earlier merger. A root may also store the structure evacuation builds, the noun beside the remnant it left. Such a root lexicalizes the bare noun and the whole structure and nothing in between, which gives Kalenjin its marked singulars and the Friulian verb bati a suffix in the second person alone. A suffix may store such a structure too, as in the Friulian verb finî.

Main results

• english_degrees, armenian_degrees, czech_degrees: the lexicalization table of the degrees of comparison.
• czech_declension, genitive_levels: the genitive is -a in both noun classes, with the same structure.
• kalenjin_number, peel_plural_overrides: the root peel is bare in the plural and marked in the singular.
• bati_present, fini_present: the first and third person are alike and the second has a suffix more.

Implementation notes

The chapter's prefixes are built in a workspace of their own, which the engine does not model. The Czech superlative nej- is such a prefix, so czech_degrees shows only that the movement steps do not derive the superlative. For Kalenjin the chapter gives no entry for the plural suffix -tiin of roots like kipaw 'rhino', so that class is left out.

References

• [DCCSVW25]
• [Sta18]

Degrees of comparison

inductive DeClercqEtAl2025.Deg : Type

The features of the adjectival sequence are the adjective, gradability, the comparative and the superlative.

• a : Deg
• q : Deg
• cmpr : Deg
• sprl : Deg

@[instance_reducible]

instance DeClercqEtAl2025.instDecidableEqDeg : DecidableEq Deg

Equations

• DeClercqEtAl2025.instDecidableEqDeg x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance DeClercqEtAl2025.instReprDeg : Repr Deg

Equations

• DeClercqEtAl2025.instReprDeg = { reprPrec := DeClercqEtAl2025.instReprDeg.repr }

def DeClercqEtAl2025.instReprDeg.repr : Deg → ℕ → Std.Format

Equations

• DeClercqEtAl2025.instReprDeg.repr DeClercqEtAl2025.Deg.a prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "DeClercqEtAl2025.Deg.a")).group prec✝
• DeClercqEtAl2025.instReprDeg.repr DeClercqEtAl2025.Deg.q prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "DeClercqEtAl2025.Deg.q")).group prec✝
• DeClercqEtAl2025.instReprDeg.repr DeClercqEtAl2025.Deg.cmpr prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "DeClercqEtAl2025.Deg.cmpr")).group prec✝
• DeClercqEtAl2025.instReprDeg.repr DeClercqEtAl2025.Deg.sprl prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "DeClercqEtAl2025.Deg.sprl")).group prec✝

def DeClercqEtAl2025.tall : Morphology.Exponence.RuleSet (Morphology.Nanosyntax.LexicalEntry (Option Deg) String)

English tall stores the gradable adjective, -er the comparative alone and -est the superlative over the comparative.

Equations

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

def DeClercqEtAl2025.bad : Morphology.Exponence.RuleSet (Morphology.Nanosyntax.LexicalEntry (Option Deg) String)

English bad beside worse, a root storing the comparative.

Equations

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

def DeClercqEtAl2025.partsrahasag : Morphology.Exponence.RuleSet (Morphology.Nanosyntax.LexicalEntry (Option Deg) String)

Armenian partsrahasag 'tall' stores the superlative.

Equations

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

def DeClercqEtAl2025.inteligent : Morphology.Exponence.RuleSet (Morphology.Nanosyntax.LexicalEntry (Option Deg) String)

Czech inteligent- stores the bare adjective, with the adjectivizer -n and the comparative -ějš storing one feature each.

Equations

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

def DeClercqEtAl2025.chytr : Morphology.Exponence.RuleSet (Morphology.Nanosyntax.LexicalEntry (Option Deg) String)

Czech chytr- 'smart' stores the gradable adjective.

Equations

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

def DeClercqEtAl2025.degrees : List (List Deg)

The sequences of the positive, the comparative and the superlative.

Equations

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

theorem DeClercqEtAl2025.english_degrees : List.map (Morphology.Nanosyntax.exponents tall) degrees = [some ["tall"], some ["tall", "er"], some ["tall", "est"]] ∧ Morphology.Nanosyntax.exponents bad [Deg.a, Deg.q, Deg.cmpr] = some ["worse"]

English tall, tall-er, tall-est: the comparative suffix follows the evacuated root and the superlative suffix overrides it. With worse in the lexicon the comparative needs no evacuation, so it is worse and not badd-er.

theorem DeClercqEtAl2025.armenian_degrees : List.map (Morphology.Nanosyntax.exponents partsrahasag) degrees = [some ["partsrahasag"], some ["partsrahasag"], some ["partsrahasag"]]

Armenian has the one form in all three degrees, each phrase a subtree of the stored one.

theorem DeClercqEtAl2025.czech_degrees : List.map (Morphology.Nanosyntax.exponents inteligent) degrees = [some ["inteligent", "n"], some ["inteligent", "n", "ějš"], none] ∧ Morphology.Nanosyntax.exponents chytr [Deg.a, Deg.q, Deg.cmpr] = some ["chytr", "ějš"]

Czech inteligent-n-(í), inteligent-n-ějš-(í) and chytř-ejš-(í): the smaller root takes a suffix more. The movement steps do not derive the superlative, no entry storing the superlative feature with a unary foot, and the algorithm's last resort builds the prefix nej-.

Czech declension

inductive DeClercqEtAl2025.Case : Type

The features of the nominal sequence are the noun, the singular, and one each for the nominative, the accusative and the genitive.

• n : Case
• sg : Case
• k1 : Case
• k2 : Case
• k3 : Case

@[instance_reducible]

instance DeClercqEtAl2025.instDecidableEqCase : DecidableEq Case

Equations

• DeClercqEtAl2025.instDecidableEqCase x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance DeClercqEtAl2025.instReprCase : Repr Case

Equations

• DeClercqEtAl2025.instReprCase = { reprPrec := DeClercqEtAl2025.instReprCase.repr }

def DeClercqEtAl2025.instReprCase.repr : Case → ℕ → Std.Format

Equations

• DeClercqEtAl2025.instReprCase.repr DeClercqEtAl2025.Case.n prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "DeClercqEtAl2025.Case.n")).group prec✝
• DeClercqEtAl2025.instReprCase.repr DeClercqEtAl2025.Case.sg prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "DeClercqEtAl2025.Case.sg")).group prec✝
• DeClercqEtAl2025.instReprCase.repr DeClercqEtAl2025.Case.k1 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "DeClercqEtAl2025.Case.k1")).group prec✝
• DeClercqEtAl2025.instReprCase.repr DeClercqEtAl2025.Case.k2 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "DeClercqEtAl2025.Case.k2")).group prec✝
• DeClercqEtAl2025.instReprCase.repr DeClercqEtAl2025.Case.k3 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "DeClercqEtAl2025.Case.k3")).group prec✝

def DeClercqEtAl2025.suffixA : Morphology.Nanosyntax.LexicalEntry (Option Case) String

The suffix -a stores the genitive down to the singular.

Equations

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

def DeClercqEtAl2025.chleb : Morphology.Exponence.RuleSet (Morphology.Nanosyntax.LexicalEntry (Option Case) String)

chleb- 'bread' stores the bare noun.

Equations

• DeClercqEtAl2025.chleb = [{ tree := Morphology.Nanosyntax.spine DeClercqEtAl2025.Case.n [], exponent := "chleb" }, DeClercqEtAl2025.suffixA]

def DeClercqEtAl2025.jazyk : Morphology.Exponence.RuleSet (Morphology.Nanosyntax.LexicalEntry (Option Case) String)

jazyk 'tongue' stores the accusative.

Equations

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

def DeClercqEtAl2025.cases : List (List Case)

The sequences of the nominative, the accusative and the genitive.

Equations

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

theorem DeClercqEtAl2025.czech_declension : List.map (Morphology.Nanosyntax.exponents chleb) cases = [some ["chleb", "a"], some ["chleb", "a"], some ["chleb", "a"]] ∧ List.map (Morphology.Nanosyntax.exponents jazyk) cases = [some ["jazyk"], some ["jazyk"], some ["jazyk", "a"]]

chleb-a in all three cases, and jazyk, jazyk, jazyk-a.

theorem DeClercqEtAl2025.genitive_levels : Morphology.Nanosyntax.lexicalize jazyk [Case.n, Case.sg, Case.k1, Case.k2, Case.k3] = Morphology.Nanosyntax.lexicalize chleb [Case.n, Case.sg, Case.k1, Case.k2, Case.k3]

In the genitive the root jazyk cannot grow, and no entry lexicalizes the genitive feature alone, so the derivation goes back to the merger of the singular and evacuates the noun there. Its structure is then that of chleb-a, the two classes levelled.

Inverse number marking

inductive DeClercqEtAl2025.Num : Type

The features of the number sequence are the noun, the singular and the plural.

• n : Num
• sg : Num
• pl : Num

@[instance_reducible]

instance DeClercqEtAl2025.instDecidableEqNum : DecidableEq Num

Equations

• DeClercqEtAl2025.instDecidableEqNum x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance DeClercqEtAl2025.instReprNum : Repr Num

Equations

• DeClercqEtAl2025.instReprNum = { reprPrec := DeClercqEtAl2025.instReprNum.repr }

def DeClercqEtAl2025.instReprNum.repr : Num → ℕ → Std.Format

Equations

• DeClercqEtAl2025.instReprNum.repr DeClercqEtAl2025.Num.n prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "DeClercqEtAl2025.Num.n")).group prec✝
• DeClercqEtAl2025.instReprNum.repr DeClercqEtAl2025.Num.sg prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "DeClercqEtAl2025.Num.sg")).group prec✝
• DeClercqEtAl2025.instReprNum.repr DeClercqEtAl2025.Num.pl prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "DeClercqEtAl2025.Num.pl")).group prec✝

def DeClercqEtAl2025.numberSuffixes : Morphology.Exponence.RuleSet (Morphology.Nanosyntax.LexicalEntry (Option Num) String)

The Kalenjin singular suffix -yaan stores the singular alone and the plural suffix -een the plural over it.

Equations

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

def DeClercqEtAl2025.peel : Morphology.Exponence.RuleSet (Morphology.Nanosyntax.LexicalEntry (Option Num) String)

peel 'elephant' stores the noun beside the plural phrase it has evacuated from.

Equations

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

def DeClercqEtAl2025.pata : Morphology.Exponence.RuleSet (Morphology.Nanosyntax.LexicalEntry (Option Num) String)

pata 'duck' stores the bare noun.

Equations

• DeClercqEtAl2025.pata = { tree := Morphology.Nanosyntax.spine DeClercqEtAl2025.Num.n [], exponent := "pata" } :: DeClercqEtAl2025.numberSuffixes

def DeClercqEtAl2025.numbers : List (List Num)

The sequences of the bare root, the singular and the plural.

Equations

• DeClercqEtAl2025.numbers = [[DeClercqEtAl2025.Num.n], [DeClercqEtAl2025.Num.n, DeClercqEtAl2025.Num.sg], [DeClercqEtAl2025.Num.n, DeClercqEtAl2025.Num.sg, DeClercqEtAl2025.Num.pl]]

theorem DeClercqEtAl2025.kalenjin_number : List.map (Morphology.Nanosyntax.exponents peel) numbers = [some ["peel"], some ["peel", "yaan"], some ["peel"]] ∧ List.map (Morphology.Nanosyntax.exponents pata) numbers = [some ["pata"], some ["pata", "yaan"], some ["pata", "een"]]

peel, peel-yaan, peel and pata, pata-yaan, pat-een. The stored structure of peel contains the bare noun and no singular phrase over a noun, so the singular needs -yaan, and the plural, once the noun has evacuated, is that structure again.

theorem DeClercqEtAl2025.peel_plural_overrides : Morphology.Nanosyntax.lexicalize peel [Num.n, Num.sg, Num.pl] = Morphology.Nanosyntax.lexicalize pata [Num.n, Num.sg, Num.pl] ∧ Option.map List.length (Morphology.Nanosyntax.lexicalize peel [Num.n, Num.sg, Num.pl]) = some 2

The plural of peel has the two constituents of pat-een, the noun and a remnant that -een lexicalizes. The root's entry matches the object they form, and being the larger lexicalized constituent it is what is pronounced.

The Friulian present

inductive DeClercqEtAl2025.Phi : Type

The features of the verbal sequence are tense, number, person, participant and speaker.

• t : Phi
• num : Phi
• π : Phi
• part : Phi
• spkr : Phi

@[instance_reducible]

instance DeClercqEtAl2025.instDecidableEqPhi : DecidableEq Phi

Equations

• DeClercqEtAl2025.instDecidableEqPhi x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def DeClercqEtAl2025.instReprPhi.repr : Phi → ℕ → Std.Format

Equations

• DeClercqEtAl2025.instReprPhi.repr DeClercqEtAl2025.Phi.t prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "DeClercqEtAl2025.Phi.t")).group prec✝
• DeClercqEtAl2025.instReprPhi.repr DeClercqEtAl2025.Phi.num prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "DeClercqEtAl2025.Phi.num")).group prec✝
• DeClercqEtAl2025.instReprPhi.repr DeClercqEtAl2025.Phi.π prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "DeClercqEtAl2025.Phi.π")).group prec✝
• DeClercqEtAl2025.instReprPhi.repr DeClercqEtAl2025.Phi.part prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "DeClercqEtAl2025.Phi.part")).group prec✝
• DeClercqEtAl2025.instReprPhi.repr DeClercqEtAl2025.Phi.spkr prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "DeClercqEtAl2025.Phi.spkr")).group prec✝

@[instance_reducible]

instance DeClercqEtAl2025.instReprPhi : Repr Phi

Equations

• DeClercqEtAl2025.instReprPhi = { reprPrec := DeClercqEtAl2025.instReprPhi.repr }

def DeClercqEtAl2025.suffixS : Morphology.Nanosyntax.LexicalEntry (Option Phi) String

The second-person suffix -s stores the participant alone.

Equations

• DeClercqEtAl2025.suffixS = { tree := Morphology.Nanosyntax.spine DeClercqEtAl2025.Phi.part [], exponent := "s" }

def DeClercqEtAl2025.bat : Morphology.Exponence.RuleSet (Morphology.Nanosyntax.LexicalEntry (Option Phi) String)

Tualis Friulian bat- 'hit' stores the person phrase beside the speaker phrase it has evacuated from.

Equations

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

def DeClercqEtAl2025.fin : Morphology.Exponence.RuleSet (Morphology.Nanosyntax.LexicalEntry (Option Phi) String)

fin- 'finish' stores number over tense, and its suffix -iʃ the speaker over a person phrase stranded beside the participant.

Equations

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

def DeClercqEtAl2025.persons : List (List Phi)

The sequences of the third, the second and the first person.

Equations

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

theorem DeClercqEtAl2025.bati_present : List.map (Morphology.Nanosyntax.exponents bat) persons = [some ["bat"], some ["bat", "s"], some ["bat"]]

bat, bat-s, bat. The root's entry contains the third-person phrase and no participant phrase over it, so the second person needs -s, and the first person, once the person phrase has evacuated, is the stored structure again.

theorem DeClercqEtAl2025.fini_present : List.map (Morphology.Nanosyntax.exponents fin) persons = [some ["fin", "iʃ"], some ["fin", "iʃ", "s"], some ["fin", "iʃ"]]

fin-iʃ, fin-iʃ-s, fin-iʃ. In the first person the verb evacuates alone from under the speaker feature, which strands the person and the participant phrases in the shape -iʃ stores.