Default Category System (UD-grounded)

Syntax.Cat — the default instantiation of Syntax.Tree's category parameter C, grounded in Universal Dependencies UPOS ([dMMNZ21]). Word-level categories via head : UPOS → Cat, phrasal via proj : UPOS → Cat, plus S and CP.

Split from Syntax/Tree/Basic.lean so that category-generic consumers (e.g. the type-driven composition engine, which ignores categories) do not carry the UD dataset in their transitive imports.

inductive Syntax.Cat : Type

Default syntactic category system grounded in Universal Dependencies UPOS ([dMMNZ21]).

• head pos — word-level (terminal): wraps a UPOS tag directly
• proj pos — maximal X-bar projection of a UPOS head
• S — sentence/clause (not a projection of a single lexical head)
• CP — complementizer phrase

Phrasal categories are derived systematically: NP = proj .NOUN, VP = proj .VERB, DP = proj .DET, ConjP = proj .CCONJ, etc.

This is one possible instantiation of Tree's C parameter. Framework-specific category systems (CCG functors, Minimalist feature bundles, etc.) can be used instead.

• head : UD.UPOS → Cat
• proj : UD.UPOS → Cat
• S : Cat
• CP : Cat

def Syntax.instDecidableEqCat.decEq (x✝ x✝¹ : Cat) : Decidable (x✝ = x✝¹)

Equations

• Syntax.instDecidableEqCat.decEq (Syntax.Cat.head a) (Syntax.Cat.head b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Syntax.instDecidableEqCat.decEq (Syntax.Cat.head a) (Syntax.Cat.proj a_1) = isFalse ⋯
• Syntax.instDecidableEqCat.decEq (Syntax.Cat.head a) Syntax.Cat.S = isFalse ⋯
• Syntax.instDecidableEqCat.decEq (Syntax.Cat.head a) Syntax.Cat.CP = isFalse ⋯
• Syntax.instDecidableEqCat.decEq (Syntax.Cat.proj a) (Syntax.Cat.head a_1) = isFalse ⋯
• Syntax.instDecidableEqCat.decEq (Syntax.Cat.proj a) (Syntax.Cat.proj b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Syntax.instDecidableEqCat.decEq (Syntax.Cat.proj a) Syntax.Cat.S = isFalse ⋯
• Syntax.instDecidableEqCat.decEq (Syntax.Cat.proj a) Syntax.Cat.CP = isFalse ⋯
• Syntax.instDecidableEqCat.decEq Syntax.Cat.S (Syntax.Cat.head a) = isFalse ⋯
• Syntax.instDecidableEqCat.decEq Syntax.Cat.S (Syntax.Cat.proj a) = isFalse ⋯
• Syntax.instDecidableEqCat.decEq Syntax.Cat.S Syntax.Cat.S = isTrue ⋯
• Syntax.instDecidableEqCat.decEq Syntax.Cat.S Syntax.Cat.CP = isFalse Syntax.instDecidableEqCat.decEq._proof_13
• Syntax.instDecidableEqCat.decEq Syntax.Cat.CP (Syntax.Cat.head a) = isFalse ⋯
• Syntax.instDecidableEqCat.decEq Syntax.Cat.CP (Syntax.Cat.proj a) = isFalse ⋯
• Syntax.instDecidableEqCat.decEq Syntax.Cat.CP Syntax.Cat.S = isFalse Syntax.instDecidableEqCat.decEq._proof_16
• Syntax.instDecidableEqCat.decEq Syntax.Cat.CP Syntax.Cat.CP = isTrue ⋯

@[implicit_reducible]

instance Syntax.instDecidableEqCat : DecidableEq Cat

Equations

• Syntax.instDecidableEqCat = Syntax.instDecidableEqCat.decEq

@[implicit_reducible]

instance Syntax.instReprCat : Repr Cat

Equations

• Syntax.instReprCat = { reprPrec := Syntax.instReprCat.repr }

def Syntax.instReprCat.repr : Cat → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Syntax.instReprCat.repr Syntax.Cat.S prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Syntax.Cat.S")).group prec✝
• Syntax.instReprCat.repr Syntax.Cat.CP prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Syntax.Cat.CP")).group prec✝

@[implicit_reducible]

instance Syntax.instInhabitedCat : Inhabited Cat

Equations

• Syntax.instInhabitedCat = { default := Syntax.Cat.S }

@[implicit_reducible]

instance Syntax.instBEqCat : BEq Cat

Equations

• Syntax.instBEqCat = { beq := fun (a b : Syntax.Cat) => decide (a = b) }

instance Syntax.instLawfulBEqCat : LawfulBEq Cat

@[reducible, match_pattern, inline]

abbrev Syntax.Cat.N : Cat

Equations

• Syntax.Cat.N = Syntax.Cat.head UD.UPOS.NOUN

@[reducible, match_pattern, inline]

abbrev Syntax.Cat.V : Cat

Equations

• Syntax.Cat.V = Syntax.Cat.head UD.UPOS.VERB

@[reducible, match_pattern, inline]

abbrev Syntax.Cat.Det : Cat

Equations

• Syntax.Cat.Det = Syntax.Cat.head UD.UPOS.DET

@[reducible, match_pattern, inline]

abbrev Syntax.Cat.Adj : Cat

Equations

• Syntax.Cat.Adj = Syntax.Cat.head UD.UPOS.ADJ

@[reducible, match_pattern, inline]

abbrev Syntax.Cat.Adv : Cat

Equations

• Syntax.Cat.Adv = Syntax.Cat.head UD.UPOS.ADV

@[reducible, match_pattern, inline]

abbrev Syntax.Cat.P : Cat

Equations

• Syntax.Cat.P = Syntax.Cat.head UD.UPOS.ADP

@[reducible, match_pattern, inline]

abbrev Syntax.Cat.Conj : Cat

Equations

• Syntax.Cat.Conj = Syntax.Cat.head UD.UPOS.CCONJ

@[reducible, match_pattern, inline]

abbrev Syntax.Cat.Neg : Cat

Equations

• Syntax.Cat.Neg = Syntax.Cat.head UD.UPOS.PART

@[reducible, match_pattern, inline]

abbrev Syntax.Cat.C : Cat

Equations

• Syntax.Cat.C = Syntax.Cat.head UD.UPOS.SCONJ

@[reducible, match_pattern, inline]

abbrev Syntax.Cat.Num : Cat

Equations

• Syntax.Cat.Num = Syntax.Cat.head UD.UPOS.NUM

@[reducible, match_pattern, inline]

abbrev Syntax.Cat.Pron : Cat

Equations

• Syntax.Cat.Pron = Syntax.Cat.head UD.UPOS.PRON

@[reducible, match_pattern, inline]

abbrev Syntax.Cat.Aux : Cat

Equations

• Syntax.Cat.Aux = Syntax.Cat.head UD.UPOS.AUX

@[reducible, match_pattern, inline]

abbrev Syntax.Cat.NP : Cat

Equations

• Syntax.Cat.NP = Syntax.Cat.proj UD.UPOS.NOUN

@[reducible, match_pattern, inline]

abbrev Syntax.Cat.VP : Cat

Equations

• Syntax.Cat.VP = Syntax.Cat.proj UD.UPOS.VERB

@[reducible, match_pattern, inline]

abbrev Syntax.Cat.DP : Cat

Equations

• Syntax.Cat.DP = Syntax.Cat.proj UD.UPOS.DET

@[reducible, match_pattern, inline]

abbrev Syntax.Cat.PP : Cat

Equations

• Syntax.Cat.PP = Syntax.Cat.proj UD.UPOS.ADP

@[reducible, match_pattern, inline]

abbrev Syntax.Cat.AdjP : Cat

Equations

• Syntax.Cat.AdjP = Syntax.Cat.proj UD.UPOS.ADJ

@[reducible, match_pattern, inline]

abbrev Syntax.Cat.AdvP : Cat

Equations

• Syntax.Cat.AdvP = Syntax.Cat.proj UD.UPOS.ADV

@[reducible, match_pattern, inline]

abbrev Syntax.Cat.ConjP : Cat

Equations

• Syntax.Cat.ConjP = Syntax.Cat.proj UD.UPOS.CCONJ

@[reducible, match_pattern, inline]

abbrev Syntax.Cat.NegP : Cat

Equations

• Syntax.Cat.NegP = Syntax.Cat.proj UD.UPOS.PART

@[reducible, match_pattern, inline]

abbrev Syntax.Cat.NumP : Cat

Equations

• Syntax.Cat.NumP = Syntax.Cat.proj UD.UPOS.NUM