The property tables of the Levin classes

LevinClass.properties is the property table of a class's entry in Part II of Levin's English Verb Classes and Alternations: each line names an alternation of Part One by its section number, or a further property, with the book's asterisk or question mark, its scope and any further qualifier. A class shows an alternation (LevinClass.Participates) when a line names it without a diacritic, lacks it (LevinClass.Stars) when a line stars it or the section grouping it, and tests it (LevinClass.Tests) when it does either.

Implementation notes

• A starred family heading, such as "*Causative Alternations", denies each of the family's subsections, so Stars descends to them. An attested family heading is entered as the subsection whose Part One list carries the class, so Participates reads the lines as they stand.
• A heading phrased as a denial ("not available", "not possible") is the alternation starred.
• A class may list related alternations under different bases: the spray/load class attests the other causative alternations of its locative variant and stars the causative alternations of its with variant, so Participates and Stars are not disjoint, and the qualifiers tell the lines apart.

References

• [Lev93]

def Data.VerbClasses.PropertyLine.alternation? (l : PropertyLine) : Option ArgumentStructure.DiathesisAlternation

The alternation of Part One a property line names, if it names one.

Equations

• l.alternation? = match l.heading with | Data.VerbClasses.Heading.alternation n => ArgumentStructure.DiathesisAlternation.ofNumber? n | Data.VerbClasses.Heading.property p => none

def ArgumentStructure.LevinClass.properties (c : LevinClass) : List Data.VerbClasses.PropertyLine

The property table of the class's entry, in the book's order.

Equations

• c.properties = c.entry.properties

def ArgumentStructure.LevinClass.Lists (c : LevinClass) (a : DiathesisAlternation) (d : Data.VerbClasses.Diacritic) : Prop

The class's table lists the alternation with the given diacritic.

Equations

• c.Lists a d = ∃ l ∈ c.properties, l.heading = Data.VerbClasses.Heading.alternation a.number ∧ l.diacritic = d

@[instance_reducible]

instance ArgumentStructure.LevinClass.instDecidableLists (c : LevinClass) (a : DiathesisAlternation) (d : Data.VerbClasses.Diacritic) : Decidable (c.Lists a d)

Equations

• c.instDecidableLists a d = ArgumentStructure.LevinClass.instDecidableLists._aux_1 c a d

def ArgumentStructure.LevinClass.Participates (c : LevinClass) (a : DiathesisAlternation) : Prop

The class shows the alternation when its table lists it without a diacritic.

Equations

• c.Participates a = c.Lists a Data.VerbClasses.Diacritic.none

@[instance_reducible]

instance ArgumentStructure.LevinClass.instDecidableParticipates (c : LevinClass) (a : DiathesisAlternation) : Decidable (c.Participates a)

Equations

• c.instDecidableParticipates a = ArgumentStructure.LevinClass.instDecidableParticipates._aux_1 c a

def ArgumentStructure.LevinClass.Stars (c : LevinClass) (a : DiathesisAlternation) : Prop

The class lacks the alternation when its table stars it or the section grouping it.

Equations

• c.Stars a = (c.Lists a Data.VerbClasses.Diacritic.star ∨ ∃ p ∈ a.parent?, c.Lists p Data.VerbClasses.Diacritic.star)

@[instance_reducible]

instance ArgumentStructure.LevinClass.instDecidableStars (c : LevinClass) (a : DiathesisAlternation) : Decidable (c.Stars a)

Equations

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

def ArgumentStructure.LevinClass.Tests (c : LevinClass) (a : DiathesisAlternation) : Prop

The class's table tests the alternation, attesting or starring it.

Equations

• c.Tests a = (c.Participates a ∨ c.Stars a)

@[instance_reducible]

instance ArgumentStructure.LevinClass.instDecidableTests (c : LevinClass) (a : DiathesisAlternation) : Decidable (c.Tests a)

Equations

• c.instDecidableTests a = { decide := decide (c.Participates a) || decide (c.Stars a), reflects_decide := ⋯ }