Root classification: change type, semantic type, and the annotation record

The cross-linguistic classification dimensions a change-of-state verb root is typed by: whether it lexically entails change (ChangeType), its semantic type (an Intensional.Ty — [Coo19] (3) types Chuj roots ⟨e,⟨s,t⟩⟩, ⟨e,⟨s,d⟩⟩, ⟨e,t⟩), Dixon's property-concept categories (PCClass), and the Classification annotation record for annotation-first fragments.

Anchoring and provenance

• ChangeType — [Dix82]'s (p. 50) split between property-concept states and "states that are the result of some action", recast at root level by [BKG20] and [BEJ+21] (the term "property concept" is later than Dixon — [BKG20] fn. 2 credit it to Thompson). [Lev93] supplies the English deadjectival vs non-deadjectival verb inventory. The reading that result roots lexically entail change is the Beavers et al. account, contested by the Distributed-Morphology camp; the split itself is theory-neutral.
• denotation types — actual semantic types (Intensional.Ty), not a bespoke enum: [Coo19] (3)'s four Chuj domains and [HKG25]'s three Wáshiw PC classes are finite inventories the anchoring studies state over concrete Ty values.
• PCClass — [Dix82]'s seven categories.

Main definitions

• ChangeType, ChangeType.ofKinds — the axis and its projection from kind signatures
• Classification — the annotation record
• Classification.salienceClass — the annotation-level salience hom

Main results

• Classification.salienceClass_ofKinds — on manner-free signatures the annotation-level classifier agrees with the signature-level SalienceClass.ofKinds

inductive Verb.Root.ChangeType : Type

Two types of change-of-state verb roots ([BEJ+21] §3.1; [Dix82] p. 50).

Property concept (PC) roots underlie deadjectival CoS verbs: the root describes a gradable property (flat, red, long, warm). Result roots underlie non-deadjectival CoS verbs: the root describes a specific result state arising from a particular event (crack, break, shatter).

• propertyConcept : ChangeType

  flat, red, long — deadjectival CoS (flatten, redden).

• result : ChangeType

  crack, break, shatter — non-deadjectival CoS.

@[instance_reducible]

instance Verb.Root.instDecidableEqChangeType : DecidableEq ChangeType

Equations

• Verb.Root.instDecidableEqChangeType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Verb.Root.instReprChangeType : Repr ChangeType

Equations

• Verb.Root.instReprChangeType = { reprPrec := Verb.Root.instReprChangeType.repr }

def Verb.Root.instReprChangeType.repr : ChangeType → ℕ → Std.Format

Equations

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

def Verb.Root.ChangeType.entailsChange : ChangeType → Bool

Whether a root lexically entails prior change ([BEJ+21] §3.6). PC roots denote simple states holding without prior change; result roots denote states entailing a prior change event. The change entailment is categorical; the morphological correlates (markedness, simple stative forms) are crosslinguistic tendencies with flagged exceptions.

Equations

• Verb.Root.ChangeType.propertyConcept.entailsChange = false
• Verb.Root.ChangeType.result.entailsChange = true

def Verb.Root.ChangeType.allowsRestitutiveAgain : ChangeType → Bool

PC roots allow restitutive again (scope over root only); result roots allow only repetitive again (scope over BECOME) ([BEJ+21] §3.4). Since a result root's state itself entails change, again over the root still entails a prior change event, collapsing into the repetitive reading. Their fn. 9 records speaker variation for particular result roots (thaw, return).

Equations

• Verb.Root.ChangeType.propertyConcept.allowsRestitutiveAgain = true
• Verb.Root.ChangeType.result.allowsRestitutiveAgain = false

def Verb.Root.ChangeType.ofKinds (s : Kinds) : ChangeType

The change-entailment type of a kind signature: a root entails change iff its signature carries result ([BEJ+21]). The projection is manner-blind — see Classification.salienceClass_ofKinds for what survives it.

Equations

• Verb.Root.ChangeType.ofKinds s = if Verb.LexKind.result ∈ s then Verb.Root.ChangeType.result else Verb.Root.ChangeType.propertyConcept

inductive Verb.Root.PCClass : Type

Property concept root subclasses ([Dix82]; [BEJ+21] ex. 5). [BEJ+21] exclude human propensity from their sample (fn. 5 to ex. 5): many of its verbal forms are stative, and their study targets change of state.

• dimension : PCClass

  large/big, small, long, short, deep, wide, tall/high.

• age : PCClass

  old/aged.

• value : PCClass

  bad/worse, good/improved.

• color : PCClass

  white, black, red, green, blue, brown.

• physicalProperty : PCClass

  cool/cold, warm/hot, dry/wet, soft/hard, smooth/rough.

• humanPropensity : PCClass

  angry, embarrassed ([BEJ+21] fn. 5).

• speed : PCClass

  fast, slow.

@[instance_reducible]

instance Verb.Root.instDecidableEqPCClass : DecidableEq PCClass

Equations

• Verb.Root.instDecidableEqPCClass x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Verb.Root.instReprPCClass : Repr PCClass

Equations

• Verb.Root.instReprPCClass = { reprPrec := Verb.Root.instReprPCClass.repr }

def Verb.Root.instReprPCClass.repr : PCClass → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Verb.Root.instReprPCClass.repr Verb.Root.PCClass.dimension prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Verb.Root.PCClass.dimension")).group prec✝
• Verb.Root.instReprPCClass.repr Verb.Root.PCClass.age prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Verb.Root.PCClass.age")).group prec✝
• Verb.Root.instReprPCClass.repr Verb.Root.PCClass.value prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Verb.Root.PCClass.value")).group prec✝
• Verb.Root.instReprPCClass.repr Verb.Root.PCClass.color prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Verb.Root.PCClass.color")).group prec✝
• Verb.Root.instReprPCClass.repr Verb.Root.PCClass.speed prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Verb.Root.PCClass.speed")).group prec✝

structure Verb.Root.Classification : Type

Annotation record for roots with no atom decomposition: stipulated coordinates over valency × change type × semantic type × transitive-Voice licensing, the annotation-first counterpart of the derived projections off Root.kinds. The stipulated and derived coordinates agree only by theorem (salienceClass_ofKinds), never by construction.

• valency : ArgumentStructure.Valency

  The core-argument positions the root introduces ([Coo19]: at most the internal argument — Valency.IsRootValency).

• changeType : ChangeType

  Does this root lexically entail prior change?

• denotationType : Option Intensional.Ty

  The root's semantic type ([Coo19] (3)). Optional — not all roots have been annotated.

• licensesTransitiveVoice : Bool

  Whether the root may combine with the transitive-forming v ~ Voice⁰ head that merges an agent — the coordinate separating [Coo19]'s √TV from her unaccusative √ITV (§3.3), which share both semantic type and internal-argument valency. Coon expressly declines to formalize its source ("I do not take a particular stance on the source of this distinction").

def Verb.Root.instDecidableEqClassification.decEq (x✝ x✝¹ : Classification) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Verb.Root.instDecidableEqClassification : DecidableEq Classification

Equations

• Verb.Root.instDecidableEqClassification = Verb.Root.instDecidableEqClassification.decEq

def Verb.Root.instReprClassification.repr : Classification → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Verb.Root.instReprClassification : Repr Classification

Equations

• Verb.Root.instReprClassification = { reprPrec := Verb.Root.instReprClassification.repr }

def Verb.Root.Classification.entailsChange (r : Classification) : Bool

Does this root lexically entail prior change?

Equations

• r.entailsChange = r.changeType.entailsChange

Salience through the annotation coordinates

def Verb.Root.Classification.salienceClass (c : Classification) : Option ArgumentStructure.SalienceClass

The salience class determined by the annotation coordinates. Agent-patient salience is transitive-Voice licensing — [Luc94]'s =∅ roots form transitive stems bare — not internal-argument introduction, which unaccusatives also have ([Coo19] §3.3). Partial where the coordinates underdetermine the class: ChangeType is manner-blind, so a non-transitivizing property-concept annotation cannot distinguish an agent-salient manner root from an unclassified stative.

Equations

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

theorem Verb.Root.Classification.salienceClass_ofKinds (s : Kinds) (v : ArgumentStructure.Valency) (h : LexKind.manner ∉ s) : { valency := v, changeType := ChangeType.ofKinds s, licensesTransitiveVoice := decide (ArgumentStructure.ArgPosition.internal ∈ v) }.salienceClass = ArgumentStructure.SalienceClass.ofKinds s v

On manner-free signatures the annotation-level classifier agrees with the signature-level one (SalienceClass.ofKinds) — the agree-by-theorem link between the stipulated and derived coordinates. The hypothesis is necessary: a manner root maps to .propertyConcept under ChangeType.ofKinds, where the annotation coordinates return none but the signature classifier sees agent salience.