Panagiotidis (2015): Categorial Features

This file formalizes the theory of word class in [Pan15]: lexical category is not a property of roots but of the categorizer heads n, v, and a that category-neutral roots merge with ([Mar97]), and the categorial features those heads bear are substantive and interpretable rather than diacritic, [N] imposing a sortal perspective and [V] a perspective extending into time on the root's concept. Nouns bear [N] only, verbs [V] only, adjectives both, and adpositions neither, the adposition being the default categorizer (categorizer_features, isCategorizer_iff). The functional heads of an extended projection carry uninterpretable copies of their categorizer's features, so a category's features are fixed by its family (categorialFeatures_eq_iff), and the diacritic features of [Cho70] cut the categories into the same four classes (chomsky_panagiotidis_agree). Category change is change of categorizer: an English root surfaces in all three categorized classes (RootFamily, all_families_tricategorial).

Implementation notes

The features of a category are read off its extended-projection family, since the book has every functional head carry a copy of its categorizer's features; the substrate's Cat.features reads Chomsky's features off the family the same way, so the two systems are compared as images of the family. The book's distinction between a categorizer's interpretable features and the copies on functional heads is not represented. The root families are the standard English illustrations of category-neutral roots from the Distributed Morphology literature rather than data from the book.

References

• [Pan15]
• [Cho70]
• [Mar97]

structure Panagiotidis2015.CategorialFeatures : Type

Panagiotidis's categorial features, [N] a sortal perspective and [V] a perspective extending into time, substantive and interpretable on a categorizer.

• hasN : Bool
• hasV : Bool

def Panagiotidis2015.instDecidableEqCategorialFeatures.decEq (x✝ x✝¹ : CategorialFeatures) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Panagiotidis2015.instDecidableEqCategorialFeatures : DecidableEq CategorialFeatures

Equations

• Panagiotidis2015.instDecidableEqCategorialFeatures = Panagiotidis2015.instDecidableEqCategorialFeatures.decEq

def Panagiotidis2015.instReprCategorialFeatures.repr : CategorialFeatures → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Panagiotidis2015.instReprCategorialFeatures : Repr CategorialFeatures

Equations

• Panagiotidis2015.instReprCategorialFeatures = { reprPrec := Panagiotidis2015.instReprCategorialFeatures.repr }

def Panagiotidis2015.CategorialFeatures.ofFamily : Minimalist.CatFamily → CategorialFeatures

The features of a family's categorizer, where n bears [N], v bears [V], a both, and the adposition, the default categorizer, neither.

Equations

• Panagiotidis2015.CategorialFeatures.ofFamily Minimalist.CatFamily.nominal = { hasN := true, hasV := false }
• Panagiotidis2015.CategorialFeatures.ofFamily Minimalist.CatFamily.verbal = { hasN := false, hasV := true }
• Panagiotidis2015.CategorialFeatures.ofFamily Minimalist.CatFamily.adjectival = { hasN := true, hasV := true }
• Panagiotidis2015.CategorialFeatures.ofFamily Minimalist.CatFamily.adpositional = { hasN := false, hasV := false }

theorem Panagiotidis2015.CategorialFeatures.ofFamily_injective : Function.Injective ofFamily

def Panagiotidis2015.categorialFeatures (c : Minimalist.Cat) : CategorialFeatures

The features of a category are those of its family's categorizer, which every functional head of the extended projection carries as an uninterpretable copy.

Equations

• Panagiotidis2015.categorialFeatures c = Panagiotidis2015.CategorialFeatures.ofFamily c.family

def Panagiotidis2015.IsCategorizer : Minimalist.Cat → Prop

The categorizers are v, n and a; the categorized lexical heads are root-plus-categorizer complexes.

Equations

• Panagiotidis2015.IsCategorizer Minimalist.Cat.v = True
• Panagiotidis2015.IsCategorizer Minimalist.Cat.n = True
• Panagiotidis2015.IsCategorizer Minimalist.Cat.a = True
• Panagiotidis2015.IsCategorizer x✝ = False

@[instance_reducible]

instance Panagiotidis2015.instDecidablePredCatIsCategorizer : DecidablePred IsCategorizer

Equations

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

theorem Panagiotidis2015.isCategorizer_iff (c : Minimalist.Cat) : IsCategorizer c ↔ c = Minimalist.Cat.v ∨ c = Minimalist.Cat.n ∨ c = Minimalist.Cat.a

theorem Panagiotidis2015.categorizer_features : categorialFeatures Minimalist.Cat.n = { hasN := true, hasV := false } ∧ categorialFeatures Minimalist.Cat.v = { hasN := false, hasV := true } ∧ categorialFeatures Minimalist.Cat.a = { hasN := true, hasV := true } ∧ categorialFeatures Minimalist.Cat.P = { hasN := false, hasV := false }

The lexical categorizers bear the substantive features, n [N], v [V], a both, and the adposition, the default categorizer, neither.

theorem Panagiotidis2015.categorialFeatures_eq_iff (c₁ c₂ : Minimalist.Cat) : categorialFeatures c₁ = categorialFeatures c₂ ↔ c₁.family = c₂.family

Features are fixed by the extended-projection family: every head of a projection carries its categorizer's [N] and [V] specification.

theorem Panagiotidis2015.chomsky_panagiotidis_agree (c₁ c₂ : Minimalist.Cat) : categorialFeatures c₁ = categorialFeatures c₂ ↔ c₁.features = c₂.features

Chomsky's diacritic features and Panagiotidis's substantive ones cut the categories into the same four classes, both being injective images of the family; the conceptual difference, P as [−V, −N] against P as the default categorizer, is invisible to the partition.

theorem Panagiotidis2015.fValue_of_isCategorizer {c : Minimalist.Cat} (h : IsCategorizer c) : c.fValue = 1

The categorizers sit at the first functional level of Grimshaw's sequence, above the lexical heads, which records Grimshaw's architecture rather than the book's claim that categorizers are the only lexical heads.

structure Panagiotidis2015.RootFamily : Type

A category-neutral root with the surface words it projects across the lexical categories, each stamped with its Universal Dependencies category ([Mar97]).

• rootLabel : String

  A label for the root; roots themselves are sub-morphemic.

• forms : List (String × UD.UPOS)

  The surface forms with their categories.

def Panagiotidis2015.RootFamily.HasCategory (rf : RootFamily) (c : UD.UPOS) : Prop

The family has a surface form in category c.

Equations

• rf.HasCategory c = ∃ f ∈ rf.forms, f.2 = c

@[instance_reducible]

instance Panagiotidis2015.instDecidableHasCategory (rf : RootFamily) (c : UD.UPOS) : Decidable (rf.HasCategory c)

Equations

• Panagiotidis2015.instDecidableHasCategory rf c = List.decidableBEx (fun (f : String × UD.UPOS) => f.2 = c) rf.forms

def Panagiotidis2015.destroy : RootFamily

The root √DESTROY surfaces as destroy, destruction and destructive.

Equations

• Panagiotidis2015.destroy = { rootLabel := "DESTROY", forms := [("destroy", UD.UPOS.VERB), ("destruction", UD.UPOS.NOUN), ("destructive", UD.UPOS.ADJ)] }

def Panagiotidis2015.beauty : RootFamily

The root √BEAUTY surfaces as beautify, beauty and beautiful.

Equations

• Panagiotidis2015.beauty = { rootLabel := "BEAUTY", forms := [("beautify", UD.UPOS.VERB), ("beauty", UD.UPOS.NOUN), ("beautiful", UD.UPOS.ADJ)] }

def Panagiotidis2015.clear : RootFamily

The root √CLEAR surfaces as clear, clarity and clear.

Equations

• Panagiotidis2015.clear = { rootLabel := "CLEAR", forms := [("clear", UD.UPOS.VERB), ("clarity", UD.UPOS.NOUN), ("clear", UD.UPOS.ADJ)] }

def Panagiotidis2015.produce : RootFamily

The root √PRODUCE surfaces as produce, production and productive.

Equations

• Panagiotidis2015.produce = { rootLabel := "PRODUCE", forms := [("produce", UD.UPOS.VERB), ("production", UD.UPOS.NOUN), ("productive", UD.UPOS.ADJ)] }

def Panagiotidis2015.create : RootFamily

The root √CREATE surfaces as create, creation and creative.

Equations

• Panagiotidis2015.create = { rootLabel := "CREATE", forms := [("create", UD.UPOS.VERB), ("creation", UD.UPOS.NOUN), ("creative", UD.UPOS.ADJ)] }

def Panagiotidis2015.act : RootFamily

The root √ACT surfaces as act, action and active.

Equations

• Panagiotidis2015.act = { rootLabel := "ACT", forms := [("act", UD.UPOS.VERB), ("action", UD.UPOS.NOUN), ("active", UD.UPOS.ADJ)] }

def Panagiotidis2015.allFamilies : List RootFamily

The sample root families.

Equations

• Panagiotidis2015.allFamilies = [Panagiotidis2015.destroy, Panagiotidis2015.beauty, Panagiotidis2015.clear, Panagiotidis2015.produce, Panagiotidis2015.create, Panagiotidis2015.act]

theorem Panagiotidis2015.all_families_tricategorial (rf : RootFamily) : rf ∈ allFamilies → rf.HasCategory UD.UPOS.VERB ∧ rf.HasCategory UD.UPOS.NOUN ∧ rf.HasCategory UD.UPOS.ADJ

Every root in the sample surfaces under each of the three categorizers.