Verb entries

Verb is the framework-neutral verb entry shared by every language's fragment. Its fields are grouped into the facets Verb.ArgStructure, Verb.Aspect, Verb.Presupposition and Verb.Attitude, beside the selectional and inflectional enums VoiceType, Verb.PerfectAuxiliary and SenseTag. A verb's valency is its participants and their diatheses, and a frame-conditioned attitude, opacity or control lives on a Verb.Reading row. The classifications of an entry, factive, implicative, trigger and so on, are read off these fields in Syntax/Category/Verb/Basic.lean.

Implementation notes

• Verb composes its facets by extends, so a field is reached flat, as v.valency, and a language fragment extends Verb with its inflectional paradigm.
• The citation form is the list morphs, and Verb.form is its surface string, so a fragment builds a derived form, a converb or a causative, by attaching morphs to v.morphs.
• The facets share their names with the theory namespaces whose values they hold, so a facet field names its type with _root_.

References

• [BS26a]
• [Day25]
• [Hei92]
• [Ica12]
• [Ken07b]
• [LRH95]
• [Mai15]
• [Pan11]
• [QOR+25]
• [RHL24]
• [RHL98]
• [SB24]

Selectional and inflectional enums

inductive VoiceType : Type

The external-argument dimension of a verb's frame, neutral between syntactic frameworks.

• agentive : VoiceType

  An external argument is introduced, as in transitives and unergatives.

• nonThematic : VoiceType

  No external argument is introduced, as in unaccusatives and anticausatives.

• expletive : VoiceType

  The head has no specifier and no semantics, as in the middle voice.

• reflexive : VoiceType

  An agent that binds the internal argument ([Woo15]).

• experiencer : VoiceType

  An experiencer external argument ([Woo15]).

@[instance_reducible]

instance instDecidableEqVoiceType : DecidableEq VoiceType

Equations

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

def instReprVoiceType.repr : VoiceType → ℕ → Std.Format

Equations

• instReprVoiceType.repr VoiceType.agentive prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "VoiceType.agentive")).group prec✝
• instReprVoiceType.repr VoiceType.nonThematic prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "VoiceType.nonThematic")).group prec✝
• instReprVoiceType.repr VoiceType.expletive prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "VoiceType.expletive")).group prec✝
• instReprVoiceType.repr VoiceType.reflexive prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "VoiceType.reflexive")).group prec✝
• instReprVoiceType.repr VoiceType.experiencer prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "VoiceType.experiencer")).group prec✝

@[instance_reducible]

instance instReprVoiceType : Repr VoiceType

Equations

• instReprVoiceType = { reprPrec := instReprVoiceType.repr }

def VoiceType.AssignsTheta (vt : VoiceType) : Prop

The voice type introduces an external argument.

Equations

• vt.AssignsTheta = (vt = VoiceType.agentive ∨ vt = VoiceType.reflexive ∨ vt = VoiceType.experiencer)

@[instance_reducible]

instance instDecidablePredVoiceTypeAssignsTheta : DecidablePred VoiceType.AssignsTheta

Equations

• instDecidablePredVoiceTypeAssignsTheta x✝ = { decide := decide (x✝ = VoiceType.agentive) || decide (x✝ = VoiceType.reflexive ∨ x✝ = VoiceType.experiencer), reflects_decide := ⋯ }

inductive Verb.PerfectAuxiliary : Type

The auxiliary of the perfect in a language that forms it with be or have, as Romance and Germanic languages do.

• be : PerfectAuxiliary

  Italian essere, French être, German sein, Dutch zijn.

• have : PerfectAuxiliary

  Italian avere, French avoir, German haben, Dutch hebben.

@[instance_reducible]

instance Verb.instDecidableEqPerfectAuxiliary : DecidableEq PerfectAuxiliary

Equations

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

def Verb.instReprPerfectAuxiliary.repr : PerfectAuxiliary → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Verb.instReprPerfectAuxiliary.repr Verb.PerfectAuxiliary.be prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Verb.PerfectAuxiliary.be")).group prec✝

@[instance_reducible]

instance Verb.instReprPerfectAuxiliary : Repr PerfectAuxiliary

Equations

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

@[instance_reducible]

instance Verb.instFintypePerfectAuxiliary : Fintype PerfectAuxiliary

Equations

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

inductive SenseTag : Type

The sense that distinguishes polysemous entries sharing a citation form, as remember the implicative and remember the question-embedding factive.

• default : SenseTag

  The primary sense.

• rogative : SenseTag

  The question-embedding sense.

• causative : SenseTag

  The causative use of an otherwise non-causative verb.

• instrumental : SenseTag

  The instrument-specific sense.

• occasion : SenseTag

  The occasion sense, with an agent-evocator subject ([SB24]).

• stative : SenseTag

  The stative reading of a polysemous verb, as positional suivre 'follow'.

@[instance_reducible]

instance instDecidableEqSenseTag : DecidableEq SenseTag

Equations

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

def instReprSenseTag.repr : SenseTag → ℕ → Std.Format

Equations

• instReprSenseTag.repr SenseTag.default prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "SenseTag.default")).group prec✝
• instReprSenseTag.repr SenseTag.rogative prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "SenseTag.rogative")).group prec✝
• instReprSenseTag.repr SenseTag.causative prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "SenseTag.causative")).group prec✝
• instReprSenseTag.repr SenseTag.instrumental prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "SenseTag.instrumental")).group prec✝
• instReprSenseTag.repr SenseTag.occasion prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "SenseTag.occasion")).group prec✝
• instReprSenseTag.repr SenseTag.stative prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "SenseTag.stative")).group prec✝

@[instance_reducible]

instance instReprSenseTag : Repr SenseTag

Equations

• instReprSenseTag = { reprPrec := instReprSenseTag.repr }

Field facets

Each facet groups a concern's fields; Verb composes them via extends, so flat access (v.valency) is preserved.

structure Verb.ArgStructure : Type

The argument structure and realization of a verb are its valency and voice. An implicit argument is a frame position (ArgumentFrame.objectDrop).

• valency : Valency

  The verb's participants, with the proto-role entailment profiles the entry records for them ([Dow91], [Gri11], [Lev20]), and its diatheses, the basic diathesis first; the default records no participant.

• voiceType : Option VoiceType

  The voice type, which fixes whether an external argument is introduced.

• passivizable : Bool

  Can the verb passivize?

• perfectAuxiliaries : Finset PerfectAuxiliary

  The auxiliaries the verb forms its perfect with, as its grammar gives them, both where it gives both; empty where the language has no choice or the entry records none.

def Verb.instBEqArgStructure.beq : ArgStructure → ArgStructure → Bool

Equations

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

@[instance_reducible]

instance Verb.instBEqArgStructure : BEq ArgStructure

Equations

• Verb.instBEqArgStructure = { beq := Verb.instBEqArgStructure.beq }

structure Verb.Aspect : Type

The aspectual class of a verb is its Vendler class, degree-achievement scale, direction of motion, incrementality and phasal class.

• vendlerClass : Option Aspect.VendlerClass

  [Ven57] aspectual class of the verb's base VP. For verbs whose class depends on the object NP (eat apples = activity, eat two apples = accomplishment), record the class with a quantized (bounded) object. none for verbs where Vendler class is inapplicable (e.g., clause-embedding verbs).

• scaleDimension : Option Degree.ScalarDimension

  The dimension of the scale along which a degree achievement measures change.

• scalePolarity : Polarity

  The pole of the dimension towards which a degree achievement measures change, negative for dry, a decrease in wetness.

• direction : Option Spatial.Path.Direction

  The direction of the path along which a verb of motion displaces its theme, relative to the ground ([Pan11]). It is .goal for arrive and come, .source for leave, and .place for a verb of manner of motion, which displaces its theme without a direction ([LRH95] p. 147, roll, walk, swim against arrive, come, fall), and none for a verb that says nothing of its theme's path.

• incrementality : Option Aspect.Incrementality

  The [Kri98] incrementality class of the theme relation, none for intransitives and clause-embedding verbs.

• phasal : Option Aspect.Phasal

  The phasal class of a phasal verb such as stop, start or continue.

def Verb.instReprAspect.repr : Aspect → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Verb.instReprAspect : Repr Aspect

Equations

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

@[instance_reducible]

instance Verb.instBEqAspect : BEq Aspect

Equations

• Verb.instBEqAspect = { beq := Verb.instBEqAspect.beq }

def Verb.instBEqAspect.beq : Aspect → Aspect → Bool

Equations

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

structure Verb.Presupposition : Type

The presupposition profile of a verb is its factivity class and its implication signature. Whether the verb triggers a presupposition is derived (Verb.IsTrigger).

• factivity : Option Presupposition.Factivity

  The [Kar71b] factivity class of a factive predicate; none for a non-factive.

• implicative : NaturalLogic.ImplicationSignature

  The [NCK06] implication signature of the verb, the polarity of the complement it implies in a positive and in a negative context; ⊥ for a verb that implies nothing.

@[instance_reducible]

instance Verb.instReprPresupposition : Repr Presupposition

Equations

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

def Verb.instReprPresupposition.repr : Presupposition → ℕ → Std.Format

Equations

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

def Verb.instBEqPresupposition.beq : Presupposition → Presupposition → Bool

Equations

• Verb.instBEqPresupposition.beq { factivity := a, implicative := a_1 } { factivity := b, implicative := b_1 } = (a == b && a_1 == b_1)
• Verb.instBEqPresupposition.beq x✝¹ x✝ = false

@[instance_reducible]

instance Verb.instBEqPresupposition : BEq Presupposition

Equations

• Verb.instBEqPresupposition = { beq := Verb.instBEqPresupposition.beq }

structure Verb.Reading : Type

A frame-conditioned reading of a verb ([Bon22] §4.4.3 hanaxa; Greek thimame) overrides the lexeme-level attitude and opacity for its frame (none inherits Verb.attitude and Verb.opaqueContext) and records the frame's control type.

• frame : ArgumentFrame

  The reading applies to every frame of the verb refining this one, in the refinement order on ArgumentFrame.

• attitude : Option _root_.Attitude

  Frame-conditioned attitude override.

• opaqueContext : Option Bool

  Frame-conditioned opacity override.

• control : Option ControlType

  Control type for this frame.

• size : Option Clause.Size

  The semantic sort of the complement on this frame ([WL23]).

def Verb.instDecidableEqReading.decEq (x✝ x✝¹ : Reading) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Verb.instDecidableEqReading : DecidableEq Reading

Equations

• Verb.instDecidableEqReading = Verb.instDecidableEqReading.decEq

def Verb.instReprReading.repr : Reading → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Verb.instReprReading : Repr Reading

Equations

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

structure Verb.Attitude : Type

The attitudinal and intensional properties of a verb are its attitude classification, opacity, question-embedding and complement monotonicity.

• opaqueContext : Bool

  Does the verb create an opaque context for its complement?

• attitude : Option _root_.Attitude

  The attitude the verb expresses, doxastic or preferential, if it is an attitude verb.

• readings : List Reading

  The frame-conditioned readings ([Bon22] §4.4.3), per-frame attitude and opacity overrides and control keyed to the frames of valency.

• complementSig : Option NaturalLogic.Signature

  Entailment signature of the complement position. Classifies this verb's monotonicity w.r.t. its clausal complement. .mono is upward monotone, the report closed under entailment of the complement, as in Hintikka-style doxastic semantics ([Hin62]). Set only where the classification is textbook consensus (believe, think, know); preferential attitudes (want, hope) are contested ([Hei92]) and stay none.

def Verb.instReprAttitude.repr : Attitude → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Verb.instReprAttitude : Repr Attitude

Equations

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

@[instance_reducible]

instance Verb.instBEqAttitude : BEq Attitude

Equations

• Verb.instBEqAttitude = { beq := Verb.instBEqAttitude.beq }

def Verb.instBEqAttitude.beq : Attitude → Attitude → Bool

Equations

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

structure Verbextends Verb.ArgStructure, Verb.Aspect, Verb.Presupposition, Verb.Attitude : Type

The cross-linguistic verb core holds the semantic fields shared across languages.

Composes the Verb.* facets (argument structure, aspect, presupposition, attitude, root) plus the morphs of the citation form, speech-act status, and a polysemy disambiguator. Language-specific fragments extend this with morphological fields appropriate to their inflectional system.

• valency : Valency
• voiceType : Option VoiceType
• passivizable : Bool
• perfectAuxiliaries : Finset PerfectAuxiliary
• vendlerClass : Option Aspect.VendlerClass
• scaleDimension : Option Degree.ScalarDimension
• scalePolarity : Polarity
• direction : Option Spatial.Path.Direction
• incrementality : Option Aspect.Incrementality
• phasal : Option Aspect.Phasal
• factivity : Option Presupposition.Factivity
• implicative : NaturalLogic.ImplicationSignature
• opaqueContext : Bool
• attitude : Option _root_.Attitude
• readings : List Reading
• complementSig : Option NaturalLogic.Signature
• levinClasses : Finset ArgumentStructure.LevinClass

  The [Lev93] classes whose member lists carry the citation form, for the English entries; the classes are Levin's, so entries for other languages carry none. A verb Levin cross-lists carries every class, and a study chooses a sense by membership.

• levinExcluded : Finset ArgumentStructure.LevinClass

  Levin classes that list the citation form in a sense this entry is not, and so are left out of levinClasses.

• root : Semantics.Root

  The verb's lexical root, from which its kind signature and change type are read rather than from its Levin classes. The default {} is the unannotated root.

• morphs : List Morphology.Morph

  The morphs of the citation form, in surface order, are the stem with the affixes and particles it is cited with. A citation form the entry does not analyse is a single root.

• speechActVerb : Bool

  Does the verb denote the performance of an illocutionary act? True for speech-act verbs (say, tell, claim, ask). This is a genuine semantic primitive that cannot be derived from other fields.

• senseTag : SenseTag

  Disambiguates entries that share a citation form. Most verbs use .default; polysemous entries use descriptive tags.

def instBEqVerb.beq : Verb → Verb → Bool

Equations

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

@[instance_reducible]

instance instBEqVerb : BEq Verb

Equations

• instBEqVerb = { beq := instBEqVerb.beq }

def Verb.form (v : Verb) : String

The citation form of a verb is the surface form of its morphs, in boundary notation.

Equations

• v.form = Morphology.Morph.surface v.morphs

def Verb.changeScale (v : Verb) : Option Degree.Boundedness

The scale along which a degree achievement measures change is its dimension's, dualized when the change is towards the negative pole, as the scale of a negative adjective is.

Equations

• v.changeScale = Option.map (fun (x : Degree.ScalarDimension) => v.scalePolarity • x.boundedness) v.scaleDimension

ArgumentFrame accessors

Readers over the frames of Verb.valency and over Verb.readings: the basic diathesis's control type and the alternate frame's, when present, and the entailment profiles of the basic diathesis's subject and object.

def Verb.subjectEntailments (v : Verb) : Option ArgumentStructure.EntailmentProfile

The entailment profile the entry records for the subject of its basic diathesis.

Equations

• v.subjectEntailments = v.valency.basic?.bind fun (x : Diathesis v.valency.arity) => v.valency.profileAt x ArgumentFrame.Slot.external

def Verb.objectEntailments (v : Verb) : Option ArgumentStructure.EntailmentProfile

The entailment profile the entry records for the participant in the object slot of its basic diathesis, its last core complement.

Equations

• v.objectEntailments = v.valency.basic?.bind fun (d : Diathesis v.valency.arity) => d.objectSlot?.bind (v.valency.profileAt d)

def Verb.reading? (v : Verb) (fr : ArgumentFrame) : Option Reading

The reading keyed to frame fr is the first whose frame fr refines.

Equations

• v.reading? fr = List.find? (fun (r : Verb.Reading) => decide (r.frame ≤ fr)) v.readings

def Verb.IsIntransitive (v : Verb) : Prop

Every frame of the verb is intransitive.

Equations

• v.IsIntransitive = ∀ fr ∈ v.valency.frames, fr.IsIntransitive

@[instance_reducible]

instance instDecidableIsIntransitive (v : Verb) : Decidable v.IsIntransitive

Equations

• instDecidableIsIntransitive v = instDecidableIsIntransitive._aux_1 v

def Verb.controlType (v : Verb) : ControlType

The control type of the reading keyed to the basic frame.

Equations

• v.controlType = (v.valency.basic?.bind fun (d : Diathesis v.valency.arity) => (v.reading? d.toArgumentFrame).bind fun (x : Verb.Reading) => x.control).getD ControlType.none

def Verb.altControlType (v : Verb) : ControlType

The control type of the reading keyed to the alternate frame.

Equations

• v.altControlType = (v.valency.frames[1]?.bind fun (fr : ArgumentFrame) => (v.reading? fr).bind fun (x : Verb.Reading) => x.control).getD ControlType.none

def Verb.attitudeOn (v : Verb) (fr : ArgumentFrame) : Option _root_.Attitude

The effective attitude on frame fr is the reading's override, else the lexeme's default.

Equations

• v.attitudeOn fr = ((v.reading? fr).bind fun (x : Verb.Reading) => x.attitude).orElse fun (x : Unit) => v.attitude

def Verb.codings (v : Verb) : List Complement.Coding

All [Noo07] codings across the verb's frames.

Equations

• v.codings = List.flatMap ArgumentFrame.codings v.valency.frames

def Verb.TakesType (v : Verb) (t : Clause.SentenceType) : Prop

Some frame of the verb selects the sentence type t.

Equations

• v.TakesType t = ∃ fr ∈ v.valency.frames, fr.hasType t

@[instance_reducible]

instance instDecidableTakesType (v : Verb) (t : Clause.SentenceType) : Decidable (v.TakesType t)

Equations

• instDecidableTakesType v t = instDecidableTakesType._aux_1 v t

def Verb.TakesQuestion (v : Verb) : Prop

The verb selects some interrogative sentence type, as the responsives and rogatives know, wonder and ask do.

Equations

• v.TakesQuestion = ∃ (t : Clause.SentenceType), t.IsInterrogative ∧ v.TakesType t

@[instance_reducible]

instance instDecidableTakesQuestion (v : Verb) : Decidable v.TakesQuestion

Equations

• instDecidableTakesQuestion v = { decide := decide (∃ a ∈ Finset.univ, (fun (_t : Clause.SentenceType) => _t.IsInterrogative ∧ v.TakesType _t) a), reflects_decide := ⋯ }

def Verb.TakesClausal (v : Verb) : Prop

Some frame of the verb has a clausal position, so the verb selects a CP or reduced clause ([Sch26]'s CP-selecting verbs).

Equations

• v.TakesClausal = ∃ fr ∈ v.valency.frames, fr.HasClausal

@[instance_reducible]

instance instDecidableTakesClausal (v : Verb) : Decidable v.TakesClausal

Equations

• instDecidableTakesClausal v = instDecidableTakesClausal._aux_1 v

def Verb.TakesSpatial (v : Verb) : Prop

Some frame of the verb has a spatial adpositional position, so the verb selects a locative or directional phrase as a complement.

Equations

• v.TakesSpatial = ∃ fr ∈ v.valency.frames, ∃ p ∈ fr.complements, p.relation? = some Case.Kind.spatial

@[instance_reducible]

instance instDecidableTakesSpatial (v : Verb) : Decidable v.TakesSpatial

Equations

• instDecidableTakesSpatial v = instDecidableTakesSpatial._aux_1 v

def Verb.TakesNominal (v : Verb) : Prop

Some frame of the verb has a nominal position, so the verb selects a DP.

Equations

• v.TakesNominal = ∃ fr ∈ v.valency.frames, fr.HasNominal

@[instance_reducible]

instance instDecidableTakesNominal (v : Verb) : Decidable v.TakesNominal

Equations

• instDecidableTakesNominal v = instDecidableTakesNominal._aux_1 v