Root: Cross-Cutting Primitive Types

@cite{beavers-etal-2021} @cite{dixon-1982} @cite{harley-2014} @cite{levin-1993} @cite{henderson-2019}

Framework-agnostic types for characterizing verb roots across theoretical modules. These types are used by Semantics (event structure, denotations), Syntax (argument structure, Voice), and Morphology (categorization, DM).

The theoretical content — why these types are what they are, and what they predict — lives in Theories/Morphology/RootTypology.lean and Theories/Morphology/DM/Categorizer.lean.

inductive RootType : Type

Two types of change-of-state verb roots (@cite{beavers-etal-2021} §3.1).

Property concept (PC) roots: underlie deadjectival CoS verbs. The root describes a gradable property (dimension, color, value, etc.). Examples: flat, red, long, warm.

Result roots: underlie non-deadjectival CoS verbs. The root describes a specific result state that arises from a particular kind of event (breaking, cooking, killing, etc.). Examples: crack, break, shatter.

• propertyConcept : RootType
• result : RootType

instance instDecidableEqRootType : DecidableEq RootType

Equations

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

instance instReprRootType : Repr RootType

Equations

• instReprRootType = { reprPrec := instReprRootType.repr }

def instReprRootType.repr : RootType → Nat → Std.Format

Equations

• instReprRootType.repr RootType.propertyConcept prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "RootType.propertyConcept")).group prec✝
• instReprRootType.repr RootType.result prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "RootType.result")).group prec✝

instance instBEqRootType : BEq RootType

Equations

• instBEqRootType = { beq := instBEqRootType.beq }

def instBEqRootType.beq : RootType → RootType → Bool

Equations

• instBEqRootType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def RootType.entailsChange : RootType → Bool

Whether a root lexically entails prior change (@cite{beavers-etal-2021} §3.6).

PC roots denote simple states that can hold without any prior change event. Result roots denote states that entail a prior change event.

Equations

• RootType.propertyConcept.entailsChange = false
• RootType.result.entailsChange = true

inductive RootArity : Type

Whether a root selects an internal (theme) argument.

@cite{coon-2019}: the central division of labor is that roots determine internal arguments while functional heads (v/Voice⁰) determine external arguments. This is orthogonal to change entailment.

• selectsTheme : RootArity
• noTheme : RootArity

instance instDecidableEqRootArity : DecidableEq RootArity

Equations

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

instance instReprRootArity : Repr RootArity

Equations

• instReprRootArity = { reprPrec := instReprRootArity.repr }

def instReprRootArity.repr : RootArity → Nat → Std.Format

Equations

• instReprRootArity.repr RootArity.selectsTheme prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "RootArity.selectsTheme")).group prec✝
• instReprRootArity.repr RootArity.noTheme prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "RootArity.noTheme")).group prec✝

def instBEqRootArity.beq : RootArity → RootArity → Bool

Equations

• instBEqRootArity.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance instBEqRootArity : BEq RootArity

Equations

• instBEqRootArity = { beq := instBEqRootArity.beq }

def RootArity.hasInternalArg : RootArity → Bool

Does this root arity entail an obligatory internal argument?

Equations

• RootArity.selectsTheme.hasInternalArg = true
• RootArity.noTheme.hasInternalArg = false

inductive RootDenotationType : Type

The semantic denotation domain of a root (@cite{coon-2019}, (3)).

• eventPred ⟨e, ⟨s,t⟩⟩: entity → event → truth-value (√TV, √ITV)
• measureFn ⟨e, ⟨s,d⟩⟩: entity → event → degree (√POS; @cite{henderson-2019})
• entityPred ⟨e,t⟩: entity → truth-value, no event (√NOM)

• eventPred : RootDenotationType
• measureFn : RootDenotationType
• entityPred : RootDenotationType

instance instDecidableEqRootDenotationType : DecidableEq RootDenotationType

Equations

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

instance instBEqRootDenotationType : BEq RootDenotationType

Equations

• instBEqRootDenotationType = { beq := instBEqRootDenotationType.beq }

def instBEqRootDenotationType.beq : RootDenotationType → RootDenotationType → Bool

Equations

• instBEqRootDenotationType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def instReprRootDenotationType.repr : RootDenotationType → Nat → Std.Format

Equations

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

instance instReprRootDenotationType : Repr RootDenotationType

Equations

• instReprRootDenotationType = { reprPrec := instReprRootDenotationType.repr }

structure Root : Type

Unified root characterization bundling all classification dimensions.

A root is characterized along five independent axes:

1. Arity: does it select an internal argument?
2. Change entailment: does it lexically entail a prior change event?
3. Denotation type (@cite{coon-2019}, (3)): event predicate, measure function, or entity predicate.
4. Quality dimensions (Spalek & McNally): within-class root content
5. Class membership: verb class taxonomy

Axes 1, 2, and 3 cross-classify: Coon's four Chuj root classes are recovered as (arity × denotationType) pairs: √TV = selectsTheme + eventPred, √ITV = noTheme + eventPred, √POS = noTheme + measureFn, √NOM = noTheme + entityPred.

• arity : RootArity

  Does this root select an internal argument?

• changeType : RootType

  Does this root lexically entail prior change?

• denotationType : Option RootDenotationType

  Semantic denotation domain (@cite{coon-2019}, (3)). Optional — not all roots have been annotated.

• profile : RootProfile

  Within-class quality dimensions (Spalek & McNally)

• levinClass : Option LevinClass

  Verb class membership

instance instBEqRoot : BEq Root

Equations

• instBEqRoot = { beq := instBEqRoot.beq }

def instBEqRoot.beq : Root → Root → Bool

Equations

• One or more equations did not get rendered due to their size.
• instBEqRoot.beq x✝¹ x✝ = false

instance instReprRoot : Repr Root

Equations

• instReprRoot = { reprPrec := instReprRoot.repr }

def instReprRoot.repr : Root → Nat → Std.Format

Equations

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

def Root.entailsChange (r : Root) : Bool

Does this root lexically entail prior change?

Equations

• r.entailsChange = r.changeType.entailsChange