Root kind signatures

The four-feature vocabulary of [BKG20]'s root typology (ch. 5): LexKind with the book's collocational order (state < result < cause, manner isolated), and a root's kind signature — the kinds of lexical entailment it carries — as a Finset LexKind, so signatures inherit the Boolean lattice of finite sets (≤ is "carries at most these kinds"). Well-formedness is downward-closedness in the collocational order, and close — the induced lower closure, packaged as a mathlib ClosureOperator — repairs any signature to a well-formed one.

This file is Root-free: consumers that map other objects to signatures (e.g. Levin classes, the salience classifier) can import it without the root substrate.

Main declarations

• LexKind, with its collocational PartialOrder
• Root.Kinds := Finset LexKind
• Root.Kinds.close, Root.Kinds.closeOp, Root.Kinds.WellFormed
• canonical signatures (propertyConcept, pureResult, causativeResult, pureManner, mannerResult, fullSpec, minimal)

Lexical entailment kinds

inductive Verb.LexKind : Type

The four kinds of lexical entailment of [BKG20]'s root typology.

• state : LexKind
• manner : LexKind
• result : LexKind
• cause : LexKind

@[instance_reducible]

instance Verb.instDecidableEqLexKind : DecidableEq LexKind

Equations

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

@[instance_reducible]

instance Verb.instFintypeLexKind : Fintype LexKind

Equations

• Verb.instFintypeLexKind = { elems := { val := ↑Verb.LexKind.enumList, nodup := Verb.LexKind.enumList_nodup }, complete := Verb.instFintypeLexKind._proof_1 }

@[instance_reducible]

instance Verb.instReprLexKind : Repr LexKind

Equations

• Verb.instReprLexKind = { reprPrec := Verb.instReprLexKind.repr }

def Verb.instReprLexKind.repr : LexKind → ℕ → Std.Format

Equations

• Verb.instReprLexKind.repr Verb.LexKind.state prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Verb.LexKind.state")).group prec✝
• Verb.instReprLexKind.repr Verb.LexKind.manner prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Verb.LexKind.manner")).group prec✝
• Verb.instReprLexKind.repr Verb.LexKind.result prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Verb.LexKind.result")).group prec✝
• Verb.instReprLexKind.repr Verb.LexKind.cause prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Verb.LexKind.cause")).group prec✝

@[instance_reducible]

instance Verb.LexKind.instPartialOrder : PartialOrder LexKind

The collocational order of [BKG20]: state < result < cause (a cause presupposes a result, a result presupposes a state), with manner incomparable to the chain.

Equations

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

@[instance_reducible]

instance Verb.LexKind.instDecidableLE : DecidableLE LexKind

Equations

• x✝¹.instDecidableLE x✝ = instDecidableEqBool (Verb.LexKind.leB✝ x✝¹ x✝) true

Kind signatures

@[reducible, inline]

abbrev Verb.Root.Kinds : Type

A root kind signature: the set of entailment kinds carried. ≤ (= ⊆) and the lattice operations come from Finset.

Equations

• Verb.Root.Kinds = Finset Verb.LexKind

def Verb.Root.Kinds.close (s : Kinds) : Kinds

The collocational closure: a signature carrying cause is completed with result and state; one carrying result is completed with state. This is the lower closure under the LexKind order (mem_close_iff).

Equations

• s.close = (s ∪ if Verb.LexKind.cause ∈ s then {Verb.LexKind.result, Verb.LexKind.state} else ∅) ∪ if Verb.LexKind.result ∈ s then {Verb.LexKind.state} else ∅

theorem Verb.Root.Kinds.le_close (s : Kinds) : s ⊆ s.close

theorem Verb.Root.Kinds.close_idem (s : Kinds) : s.close.close = s.close

theorem Verb.Root.Kinds.close_mono {s t : Kinds} : s ⊆ t → s.close ⊆ t.close

theorem Verb.Root.Kinds.mem_close_iff (s : Kinds) (k : LexKind) : k ∈ s.close ↔ ∃ j ∈ s, k ≤ j

close is the lower closure under the collocational order: k is in the closure iff some kind in s dominates it.

def Verb.Root.Kinds.closeOp : ClosureOperator Kinds

The collocational closure as a mathlib ClosureOperator.

Equations

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

def Verb.Root.Kinds.WellFormed (s : Kinds) : Prop

A signature is well-formed iff it already satisfies the collocational constraints (it is a fixed point of close).

Equations

• s.WellFormed = (s.close = s)

@[instance_reducible]

instance Verb.Root.Kinds.instDecidableWellFormed (s : Kinds) : Decidable s.WellFormed

Equations

• s.instDecidableWellFormed = Verb.Root.Kinds.instDecidableWellFormed._aux_1 s

theorem Verb.Root.Kinds.wellFormed_iff_isLowerSet (s : Kinds) : s.WellFormed ↔ IsLowerSet ↑s

Well-formedness is downward-closedness in the LexKind order.

theorem Verb.Root.Kinds.close_wellFormed (s : Kinds) : s.close.WellFormed

Closure output is always well-formed — the collocational constraints hold of closed signatures by construction.

Canonical signatures

The attested rows of the root typology of [BKG20] ch. 5 (their example display (12), §5.4).

def Verb.Root.Kinds.propertyConcept : Kinds

+S −M −R −C: property concept roots (√FLAT, √DRY). Deadjectival COS verbs — the root names the result state. Complement position.

Equations

• Verb.Root.Kinds.propertyConcept = {Verb.LexKind.state}

def Verb.Root.Kinds.pureResult : Kinds

+S −M +R −C: internally caused result roots (√BLOSSOM, √RUST). Root entails both a state and a change to that state, but not external causation. Complement position.

Equations

• Verb.Root.Kinds.pureResult = {Verb.LexKind.state, Verb.LexKind.result}

def Verb.Root.Kinds.causativeResult : Kinds

+S −M +R +C: externally caused result roots (√CRACK, √BREAK). Root entails a state, change, AND causation. If roots subdivide by entailed causation, this may underlie Levin & Rappaport Hovav's (1995) externally vs internally caused change-of-state distinction ([BKG20], hedged as a possibility). Complement position.

Equations

• Verb.Root.Kinds.causativeResult = {Verb.LexKind.state, Verb.LexKind.result, Verb.LexKind.cause}

def Verb.Root.Kinds.pureManner : Kinds

−S +M −R −C: pure manner roots (√JOG, √RUN, √SWIM). Root specifies action manner without entailing any state. Adjoined position.

Equations

• Verb.Root.Kinds.pureManner = {Verb.LexKind.manner}

def Verb.Root.Kinds.mannerResult : Kinds

+S +M +R −C: manner + result without cause. Well-formed per the constraints; [BKG20] leave its attestation an open question ("whether a change and a manner can exist together in a single meaning without causation"), with candidate witnesses slide and motion-in-sound-emission buzz.

Equations

• Verb.Root.Kinds.mannerResult = {Verb.LexKind.state, Verb.LexKind.manner, Verb.LexKind.result}

def Verb.Root.Kinds.fullSpec : Kinds

+S +M +R +C: fully specified roots (√HAND adjoined, √DROWN and the other manner-of-killing roots in complement position; [BKG20] chs. 3–4). These are the attested MRC violators. The adjoined/complement contrast is carried by Root.Position, not by the signature.

Equations

• Verb.Root.Kinds.fullSpec = {Verb.LexKind.state, Verb.LexKind.manner, Verb.LexKind.result, Verb.LexKind.cause}

def Verb.Root.Kinds.minimal : Kinds

−S −M −R −C: minimal roots — no structural entailments. Conservative default for classes not yet studied under B&KG's framework. Not a row in B&KG's typology (which only lists roots with at least one positive feature).

Equations

• Verb.Root.Kinds.minimal = ∅

theorem Verb.Root.Kinds.canonical_wellFormed : propertyConcept.WellFormed ∧ pureResult.WellFormed ∧ causativeResult.WellFormed ∧ pureManner.WellFormed ∧ mannerResult.WellFormed ∧ fullSpec.WellFormed ∧ minimal.WellFormed

Every canonical signature is well-formed.