Verb entry — lookup and root

The entry-level readers of a verb: lookup by citation form and sense, the root's content, and the argument profiles with their Levin-class fallback, and the predicate a verb forms with a path phrase (Verb.withPath). The semantic classifications of an entry live with their theories, each under the Verb namespace: factivity and trigger status in Semantics/Presupposition/Verb.lean and unaccusativity in Semantics/ArgumentStructure/Unaccusativity.lean. The attitude classification is the entry's attitude field itself.

References

• [SMcN26]
• [Lev93]
• [Dow91]
• [LRH95]
• [Zwa05]

def Verb.subjectProfile? (v : Verb) : Option ArgumentStructure.EntailmentProfile

The subject's entailment profile, the entry's own or else the one its Levin classes agree on ([Lev93], [Dow91]).

Equations

• v.subjectProfile? = (v.subjectEntailments <|> ArgumentStructure.LevinClass.commonProfile ArgumentStructure.LevinClass.subjectProfile v.levinClasses)

def Verb.objectProfile? (v : Verb) : Option ArgumentStructure.EntailmentProfile

The object's entailment profile, the entry's own or else the one its Levin classes agree on.

Equations

• v.objectProfile? = (v.objectEntailments <|> ArgumentStructure.LevinClass.commonProfile ArgumentStructure.LevinClass.objectProfile v.levinClasses)

def Verb.participantProfile? (v : Verb) (i : Fin v.valency.arity) : Option ArgumentStructure.EntailmentProfile

The entailment profile of a participant, the entry's own or else the one its Levin classes agree on for the participant's position in the basic diathesis, subject or object.

Equations

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

def Verb.rootContent (v : Verb) : Semantics.Root.Content

The verb's within-class root content ([SMcN26]).

Equations

• v.rootContent = v.root.content

def Verb.find? (verbs : List Verb) (form : String) (tag : SenseTag := SenseTag.default) : Option Verb

The entry with the given citation form and sense, if the list has one.

Equations

• Verb.find? verbs form tag = List.find? (fun (v : Verb) => v.form == form && v.senseTag == tag) verbs

Path phrases

def Verb.withPath (v : Verb) (p : Adposition.SpatialReading) : Verb

The predicate a verb forms with a path phrase of reading p. A directional phrase that the verb selects as a complement gives the theme's path its direction, the directed motion use of a verb of manner of motion ([LRH95] p. 185), and a bounded one an endpoint, which makes the predicate telic ([Zwa05]). A locative phrase, and a phrase the verb does not select, an adjunct, leave the verb as it is: correre 'run' has a directed motion use in Italian but nuotare 'swim' has none.

Equations

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

@[simp]

theorem Verb.withPath_of_direction_eq_place {v : Verb} {p : Adposition.SpatialReading} (h : p.direction = Spatial.Path.Direction.place) : v.withPath p = v

@[simp]

theorem Verb.withPath_of_not_takesSpatial {v : Verb} {p : Adposition.SpatialReading} (h : ¬v.TakesSpatial) : v.withPath p = v

@[simp]

theorem Verb.direction_withPath {v : Verb} {p : Adposition.SpatialReading} (hv : v.TakesSpatial) (h : p.direction ≠ Spatial.Path.Direction.place) : (v.withPath p).direction = some p.direction

@[simp]

theorem Verb.vendlerClass_withPath {v : Verb} {p : Adposition.SpatialReading} (hv : v.TakesSpatial) (h : p.direction ≠ Spatial.Path.Direction.place) : (v.withPath p).vendlerClass = if p.IsBounded then Option.map (fun (x : Aspect.VendlerClass) => x.telicize) v.vendlerClass else v.vendlerClass