Root Kind Signatures #
The four-feature vocabulary of [BKG20]'s root
typology (ch. 5): a root's kind signature records which kinds
of lexical entailment it carries — state, manner, result, cause — as a
Finset LexKind, so signatures inherit the Boolean lattice of finite
sets (≤ is "carries at most these kinds").
LexKind carries the book's collocational order (state < result < cause, with manner isolated): "+result entails being +state, since
become′ entails something that has come about… +cause entails being
+result, since cause′ entails that there is a caused event. These are
not root-specific stipulations." Well-formedness of a signature is
downward-closedness in this 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) can import it without the root
substrate.
Main declarations #
LexKind, with its collocationalPartialOrderRoot.Kinds := Finset LexKindRoot.Kinds.close,Root.Kinds.closeOp,Root.Kinds.WellFormed- canonical signatures (
propertyConcept,pureResult,causativeResult,pureManner,mannerResult,fullSpec,minimal) Root.Kinds.ViolatesBifurcation,Root.Kinds.HasMannerAndResult
Lexical entailment kinds #
Equations
- Verb.instDecidableEqLexKind x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯
Equations
- Verb.instFintypeLexKind = { elems := { val := ↑Verb.LexKind.enumList, nodup := Verb.LexKind.enumList_nodup }, complete := Verb.instFintypeLexKind._proof_1 }
Equations
- Verb.instReprLexKind = { reprPrec := Verb.instReprLexKind.repr }
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✝
Instances For
Equations
- x✝¹.instDecidableLE x✝ = instDecidableEqBool (Verb.LexKind.leB✝ x✝¹ x✝) true
Kind signatures #
A root kind signature: the set of entailment kinds carried.
≤ (= ⊆) and the lattice operations come from Finset.
Equations
- Verb.Root.Kinds = Finset Verb.LexKind
Instances For
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 ∅
Instances For
The collocational closure as a mathlib ClosureOperator.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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)
Instances For
Well-formedness is downward-closedness in the LexKind order.
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).
+S −M −R −C: property concept roots (√FLAT, √DRY). Deadjectival COS verbs — the root names the result state. Complement position.
Equations
Instances For
+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
Instances For
+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
Instances For
−S +M −R −C: pure manner roots (√JOG, √RUN, √SWIM). Root specifies action manner without entailing any state. Adjoined position.
Equations
Instances For
+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
Instances For
+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
Instances For
−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
Instances For
Every canonical signature is well-formed.
The two theses, at signature level #
The ontological kinds — all the Bifurcation Thesis allows a root to carry.
Equations
Instances For
A signature violates the Bifurcation Thesis ([Emb09]; the
assumption of [Ara05]) iff it carries templatic (eventive)
content — it is not bounded by ontological.
Equations
Instances For
Bifurcation violation is monotone: adding entailments cannot repair a violation. (Equivalently, the thesis carves out a lower set of the signature lattice.)
A signature has both manner and result — the configuration Manner/Result Complementarity ([RHL10]) claims no root realizes.
Equations
Instances For
MRC violation is monotone in the signature order.