Syntactic categories

A syntactic category is a lexical category, named by its Universal Dependencies part of speech, or the clause S, which projects from no head. A category carries no level of projection: a noun phrase and the noun that heads it both have the category N, and whether a node is a minimal, an intermediate or a maximal projection is read off the tree from its head daughters (Syntax/Tree/Projection.lean). This is the category stripped of bar level that HPSG's head value records. PhraseStructure.Cat is the default category type of PhraseStructure.Tree.

Implementation notes

The complementizer C is SCONJ, the tag UD gives complementizers, and Neg is PART, the tag of English not and of other particles.

References

• [PS94]
• [dMMNZ21]

inductive PhraseStructure.Cat : Type

A syntactic category is a lexical category or the clause.

• lex : UD.UPOS → Cat

  lex pos is the lexical category of part of speech pos.

• S : Cat

  S is the clause, which projects from no head.

@[instance_reducible]

instance PhraseStructure.instDecidableEqCat : DecidableEq Cat

Equations

• PhraseStructure.instDecidableEqCat = PhraseStructure.instDecidableEqCat.decEq

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

Equations

• PhraseStructure.instDecidableEqCat.decEq (PhraseStructure.Cat.lex a) (PhraseStructure.Cat.lex b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• PhraseStructure.instDecidableEqCat.decEq (PhraseStructure.Cat.lex a) PhraseStructure.Cat.S = isFalse ⋯
• PhraseStructure.instDecidableEqCat.decEq PhraseStructure.Cat.S (PhraseStructure.Cat.lex a) = isFalse ⋯
• PhraseStructure.instDecidableEqCat.decEq PhraseStructure.Cat.S PhraseStructure.Cat.S = isTrue ⋯

@[instance_reducible]

instance PhraseStructure.instReprCat : Repr Cat

Equations

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

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

Equations

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

@[instance_reducible]

instance PhraseStructure.Cat.instInhabited : Inhabited Cat

Equations

• PhraseStructure.Cat.instInhabited = { default := PhraseStructure.Cat.S }

Traditional names

Each name is a match_pattern, so it can be used in pattern position.

@[reducible, match_pattern, inline]

abbrev PhraseStructure.Cat.N : Cat

Equations

• PhraseStructure.Cat.N = PhraseStructure.Cat.lex UD.UPOS.NOUN

@[reducible, match_pattern, inline]

abbrev PhraseStructure.Cat.V : Cat

Equations

• PhraseStructure.Cat.V = PhraseStructure.Cat.lex UD.UPOS.VERB

@[reducible, match_pattern, inline]

abbrev PhraseStructure.Cat.Det : Cat

Equations

• PhraseStructure.Cat.Det = PhraseStructure.Cat.lex UD.UPOS.DET

@[reducible, match_pattern, inline]

abbrev PhraseStructure.Cat.Adj : Cat

Equations

• PhraseStructure.Cat.Adj = PhraseStructure.Cat.lex UD.UPOS.ADJ

@[reducible, match_pattern, inline]

abbrev PhraseStructure.Cat.Adv : Cat

Equations

• PhraseStructure.Cat.Adv = PhraseStructure.Cat.lex UD.UPOS.ADV

@[reducible, match_pattern, inline]

abbrev PhraseStructure.Cat.P : Cat

Equations

• PhraseStructure.Cat.P = PhraseStructure.Cat.lex UD.UPOS.ADP

@[reducible, match_pattern, inline]

abbrev PhraseStructure.Cat.Conj : Cat

Equations

• PhraseStructure.Cat.Conj = PhraseStructure.Cat.lex UD.UPOS.CCONJ

@[reducible, match_pattern, inline]

abbrev PhraseStructure.Cat.Neg : Cat

Equations

• PhraseStructure.Cat.Neg = PhraseStructure.Cat.lex UD.UPOS.PART

@[reducible, match_pattern, inline]

abbrev PhraseStructure.Cat.C : Cat

Equations

• PhraseStructure.Cat.C = PhraseStructure.Cat.lex UD.UPOS.SCONJ

@[reducible, match_pattern, inline]

abbrev PhraseStructure.Cat.Num : Cat

Equations

• PhraseStructure.Cat.Num = PhraseStructure.Cat.lex UD.UPOS.NUM

@[reducible, match_pattern, inline]

abbrev PhraseStructure.Cat.Pron : Cat

Equations

• PhraseStructure.Cat.Pron = PhraseStructure.Cat.lex UD.UPOS.PRON

@[reducible, match_pattern, inline]

abbrev PhraseStructure.Cat.Aux : Cat

Equations

• PhraseStructure.Cat.Aux = PhraseStructure.Cat.lex UD.UPOS.AUX