Root kind signatures

Which templatic components a root entails, the coarse, between-class half of a root's meaning; the fine, within-class half is Root.Content. The root typology of [beavers-koontz-garboden-2020] (§5.4.1) records which of four kinds of lexical entailment a root carries — state, manner, result, cause — under two collocational restrictions, that a change entails a state and a cause entails a change. The restrictions are the partial order state ≤ result ≤ cause on Root.Kind, with manner isolated. A root's kind signature is a Finset Root.Kind; it is well-formed when it is a lower set of that order, and close sends any signature to its lower closure. The named signatures are the attested rows of the typology's display (12), and changeType is [beavers-etal-2021]'s coarsening of the change-of-state rows into property-concept roots, which name a state, and result roots, whose state entails a prior change.

Main declarations

• Root.Kind, with the collocational PartialOrder
• Root.Kinds, Root.Kinds.close, Root.Kinds.WellFormed
• Root.Kinds.propertyConcept, pureResult, causativeResult, pureManner, fullSpec
• Root.ChangeType, Root.Kinds.changeType — property-concept or result root

References

• [beavers-koontz-garboden-2020]: The Roots of Verbal Meaning.
• [beavers-etal-2021]: States and changes of state.

Kinds

inductive Semantics.Root.Kind : Type

The kinds of lexical entailment in the root typology of [beavers-koontz-garboden-2020].

• state : Kind
• manner : Kind
• result : Kind
• cause : Kind

@[instance_reducible]

instance Semantics.Root.instDecidableEqKind : DecidableEq Kind

Equations

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

@[instance_reducible]

instance Semantics.Root.instFintypeKind : Fintype Kind

Equations

• Semantics.Root.instFintypeKind = { elems := { val := ↑Semantics.Root.Kind.enumList, nodup := Semantics.Root.Kind.enumList_nodup }, complete := Semantics.Root.instFintypeKind._proof_1 }

@[instance_reducible]

instance Semantics.Root.instReprKind : Repr Kind

Equations

• Semantics.Root.instReprKind = { reprPrec := Semantics.Root.instReprKind.repr }

def Semantics.Root.instReprKind.repr : Kind → ℕ → Std.Format

Equations

• Semantics.Root.instReprKind.repr Semantics.Root.Kind.state prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Semantics.Root.Kind.state")).group prec✝
• Semantics.Root.instReprKind.repr Semantics.Root.Kind.manner prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Semantics.Root.Kind.manner")).group prec✝
• Semantics.Root.instReprKind.repr Semantics.Root.Kind.result prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Semantics.Root.Kind.result")).group prec✝
• Semantics.Root.instReprKind.repr Semantics.Root.Kind.cause prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Semantics.Root.Kind.cause")).group prec✝

inductive Semantics.Root.Kind.LE : Kind → Kind → Prop

The collocational order, state ≤ result ≤ cause with manner isolated, since a change entails a state and a cause entails a change.

• refl (a : Kind) : a.LE a
• state_result : state.LE result
• state_cause : state.LE cause
• result_cause : result.LE cause

@[instance_reducible]

instance Semantics.Root.Kind.instLE : LE Kind

Equations

• Semantics.Root.Kind.instLE = { le := Semantics.Root.Kind.LE }

@[instance_reducible]

instance Semantics.Root.Kind.instDecidableLE : DecidableLE Kind

Equations

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

@[instance_reducible]

instance Semantics.Root.Kind.instPartialOrder : PartialOrder Kind

Equations

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

Signatures

@[reducible, inline]

abbrev Semantics.Root.Kinds : Type

A root kind signature, the set of kinds a root carries.

Equations

• Semantics.Root.Kinds = Finset Semantics.Root.Kind

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

The collocational closure of a signature, its lower closure in the kind order.

Equations

• s.close = {x : Semantics.Root.Kind | ∃ j ∈ s, x ≤ j}

@[simp]

theorem Semantics.Root.Kinds.mem_close {s : Kinds} {k : Kind} : k ∈ s.close ↔ ∃ j ∈ s, k ≤ j

@[simp]

theorem Semantics.Root.Kinds.coe_close (s : Kinds) : ↑s.close = ↑(lowerClosure ↑s)

theorem Semantics.Root.Kinds.subset_close (s : Kinds) : s ⊆ s.close

theorem Semantics.Root.Kinds.close_mono {s t : Kinds} (h : s ⊆ t) : s.close ⊆ t.close

theorem Semantics.Root.Kinds.close_close (s : Kinds) : s.close.close = s.close

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

A signature is well-formed if it respects the collocational restrictions, that is, if it is a lower set of the kind order.

Equations

• s.WellFormed = IsLowerSet ↑s

@[instance_reducible]

instance Semantics.Root.Kinds.instDecidablePredWellFormed : DecidablePred WellFormed

Equations

• s.instDecidablePredWellFormed = Semantics.Root.Kinds.instDecidablePredWellFormed._aux_1 s

theorem Semantics.Root.Kinds.wellFormed_iff_close_eq {s : Kinds} : s.WellFormed ↔ s.close = s

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

The attested rows of the typology

def Semantics.Root.Kinds.propertyConcept : Kinds

The signature of property-concept roots (√flat).

Equations

• Semantics.Root.Kinds.propertyConcept = {Semantics.Root.Kind.state}

def Semantics.Root.Kinds.pureResult : Kinds

The signature of result roots without causation (√blossom).

Equations

• Semantics.Root.Kinds.pureResult = {Semantics.Root.Kind.state, Semantics.Root.Kind.result}

def Semantics.Root.Kinds.causativeResult : Kinds

The signature of caused-result roots (√crack).

Equations

• Semantics.Root.Kinds.causativeResult = {Semantics.Root.Kind.state, Semantics.Root.Kind.result, Semantics.Root.Kind.cause}

def Semantics.Root.Kinds.pureManner : Kinds

The signature of pure manner roots (√jog).

Equations

• Semantics.Root.Kinds.pureManner = {Semantics.Root.Kind.manner}

def Semantics.Root.Kinds.fullSpec : Kinds

The signature of roots carrying every kind (√hand, √drown).

Equations

• Semantics.Root.Kinds.fullSpec = Finset.univ

Change type

inductive Semantics.Root.ChangeType : Type

The two types of change-of-state root, property-concept roots naming a gradable property (√flat, √red) and result roots naming the state an event brings about (√crack, √shatter) ([beavers-etal-2021] §3.1).

• propertyConcept : ChangeType
• result : ChangeType

@[instance_reducible]

instance Semantics.Root.instDecidableEqChangeType : DecidableEq ChangeType

Equations

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

@[instance_reducible]

instance Semantics.Root.instReprChangeType : Repr ChangeType

Equations

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

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

Equations

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

def Semantics.Root.Kinds.changeType (s : Kinds) : Option ChangeType

The change type of a signature, result when it carries result, propertyConcept when it carries state but not result, and undefined for signatures naming no state.

Equations

• s.changeType = if Semantics.Root.Kind.result ∈ s then some Semantics.Root.ChangeType.result else if Semantics.Root.Kind.state ∈ s then some Semantics.Root.ChangeType.propertyConcept else none

theorem Semantics.Root.Kinds.changeType_eq_some_result {s : Kinds} : s.changeType = some ChangeType.result ↔ Kind.result ∈ s

theorem Semantics.Root.Kinds.changeType_eq_some_propertyConcept {s : Kinds} : s.changeType = some ChangeType.propertyConcept ↔ Kind.state ∈ s ∧ Kind.result ∉ s