Documentation

Linglib.Phenomena.TenseAspect.Studies.AspectualConsistency

Cross-Bridge Consistency Tests #

Verifies that all bridge files agree on fragment verb classifications. Each verb that appears in multiple bridges gets a single theorem here checking that its vendlerClass, verbIncClass, and levinClass fields yield consistent licensing predictions across all classification paths.

What it catches #

If you change a fragment verb annotation (e.g., eat.vendlerClass from .accomplishment to .activity), the per-bridge theorems in each bridge file break individually. But this file additionally verifies that the cross-cutting invariants hold:

vendlerClass and verbIncClass agree on telicity
vendlerClass and levinClass agree on path/telicity
predictsGRAD and predictsSSR are complementary for the same verb
All classification paths (VendlerClass, Telicity, MereoTag, Boundedness) converge at the same licensing prediction

Sinc/inc verbs should be accomplishments (telic with incremental theme). CumOnly verbs should be activities (atelic, no theme-event mapping). Intransitives (no verbIncClass) can be any class.

theorem Phenomena.TenseAspect.Studies.AspectualConsistency.eat_vendler_inc_consistent :

Fragments.English.Predicates.Verbal.eat.vendlerClass = some Semantics.Tense.Aspect.LexicalAspect.VendlerClass.accomplishment ∧ Fragments.English.Predicates.Verbal.eat.verbIncClass = some Semantics.Events.Krifka1998.VerbIncClass.sinc ∧ Semantics.Tense.Aspect.LexicalAspect.VendlerClass.accomplishment.telicity = Semantics.Tense.Aspect.LexicalAspect.Telicity.telic

"eat": accomplishment + sinc → telic VP with incremental theme.

theorem Phenomena.TenseAspect.Studies.AspectualConsistency.build_vendler_inc_consistent :

Fragments.English.Predicates.Verbal.build.vendlerClass = some Semantics.Tense.Aspect.LexicalAspect.VendlerClass.accomplishment ∧ Fragments.English.Predicates.Verbal.build.verbIncClass = some Semantics.Events.Krifka1998.VerbIncClass.sinc ∧ Semantics.Tense.Aspect.LexicalAspect.VendlerClass.accomplishment.telicity = Semantics.Tense.Aspect.LexicalAspect.Telicity.telic

"build": accomplishment + sinc → telic VP with incremental theme.

theorem Phenomena.TenseAspect.Studies.AspectualConsistency.read_vendler_inc_consistent :

Fragments.English.Predicates.Verbal.read.vendlerClass = some Semantics.Tense.Aspect.LexicalAspect.VendlerClass.accomplishment ∧ Fragments.English.Predicates.Verbal.read.verbIncClass = some Semantics.Events.Krifka1998.VerbIncClass.inc ∧ Semantics.Tense.Aspect.LexicalAspect.VendlerClass.accomplishment.telicity = Semantics.Tense.Aspect.LexicalAspect.Telicity.telic

"read": accomplishment + inc → telic VP with incremental (non-strict) theme.

theorem Phenomena.TenseAspect.Studies.AspectualConsistency.push_vendler_inc_consistent :

Fragments.English.Predicates.Verbal.push.vendlerClass = some Semantics.Tense.Aspect.LexicalAspect.VendlerClass.activity ∧ Fragments.English.Predicates.Verbal.push.verbIncClass = some Semantics.Events.Krifka1998.VerbIncClass.cumOnly ∧ Semantics.Tense.Aspect.LexicalAspect.VendlerClass.activity.telicity = Semantics.Tense.Aspect.LexicalAspect.Telicity.atelic

"push": activity + cumOnly → atelic VP, no theme-event mapping.

theorem Phenomena.TenseAspect.Studies.AspectualConsistency.kick_vendler_inc_consistent :

Fragments.English.Predicates.Verbal.kick.vendlerClass = some Semantics.Tense.Aspect.LexicalAspect.VendlerClass.activity ∧ Fragments.English.Predicates.Verbal.kick.verbIncClass = none ∧ Semantics.Tense.Aspect.LexicalAspect.VendlerClass.activity.telicity = Semantics.Tense.Aspect.LexicalAspect.Telicity.atelic

"kick": activity + no verbIncClass → atelic, no incremental theme.

GRAD (gradual change) is predicted for sinc/inc verbs, which are accomplishments (telic). SSR (subinterval reference) is predicted for states/activities (atelic). These should be complementary: a verb should not predict both GRAD and SSR.

theorem Phenomena.TenseAspect.Studies.AspectualConsistency.eat_grad_ssr_complementary :

Krifka1998.predictsGRAD Fragments.English.Predicates.Verbal.eat.verbIncClass = true ∧ Plurals.Studies.Champollion2017.predictsSSR Fragments.English.Predicates.Verbal.eat.vendlerClass = false

"eat": GRAD ✓, SSR ✗ (accomplishment, sinc).

theorem Phenomena.TenseAspect.Studies.AspectualConsistency.build_grad_ssr_complementary :

Krifka1998.predictsGRAD Fragments.English.Predicates.Verbal.build.verbIncClass = true ∧ Plurals.Studies.Champollion2017.predictsSSR Fragments.English.Predicates.Verbal.build.vendlerClass = false

"build": GRAD ✓, SSR ✗ (accomplishment, sinc).

theorem Phenomena.TenseAspect.Studies.AspectualConsistency.read_grad_ssr_complementary :

Krifka1998.predictsGRAD Fragments.English.Predicates.Verbal.read.verbIncClass = true ∧ Plurals.Studies.Champollion2017.predictsSSR Fragments.English.Predicates.Verbal.read.vendlerClass = false

"read": GRAD ✓, SSR ✗ (accomplishment, inc).

theorem Phenomena.TenseAspect.Studies.AspectualConsistency.push_grad_ssr_complementary :

Krifka1998.predictsGRAD Fragments.English.Predicates.Verbal.push.verbIncClass = false ∧ Plurals.Studies.Champollion2017.predictsSSR Fragments.English.Predicates.Verbal.push.vendlerClass = true

"push": GRAD ✗, SSR ✓ (activity, cumOnly).

theorem Phenomena.TenseAspect.Studies.AspectualConsistency.sleep_grad_ssr_complementary :

Krifka1998.predictsGRAD Fragments.English.Predicates.Verbal.sleep.verbIncClass = false ∧ Plurals.Studies.Champollion2017.predictsSSR Fragments.English.Predicates.Verbal.sleep.vendlerClass = true

"sleep": GRAD ✗, SSR ✓ (state, no incremental theme).

theorem Phenomena.TenseAspect.Studies.AspectualConsistency.run_grad_ssr_complementary :

Krifka1998.predictsGRAD Fragments.English.Predicates.Verbal.run.verbIncClass = false ∧ Plurals.Studies.Champollion2017.predictsSSR Fragments.English.Predicates.Verbal.run.vendlerClass = true

"run": GRAD ✗, SSR ✓ (activity, no incremental theme).

For each shared verb, verify the complete chain from fragment annotation through all classification levels to licensing and diagnostic predictions. Changing any fragment field breaks the entire chain for that verb.

"eat": accomplishment → telic → QUA → closed → licensed → "in X" ✓.

"arrive": achievement → telic → QUA → closed → licensed → "in X" ✓.

"leave": achievement → telic → QUA → closed → licensed → "in X" ✓.

"kill": accomplishment → telic → QUA → closed → licensed → "in X" ✓.

"give": accomplishment → telic → QUA → closed → licensed → "in X" ✓.

"cover": accomplishment → telic → QUA → closed → licensed → "in X" ✓.

"buy": accomplishment → telic → QUA → closed → licensed → "in X" ✓.

"sell": accomplishment → telic → QUA → closed → licensed → "in X" ✓.

"break": accomplishment → telic → QUA → closed → licensed → "in X" ✓.

"tear": accomplishment → telic → QUA → closed → licensed → "in X" ✓.

"burn": accomplishment → telic → QUA → closed → licensed → "in X" ✓.

"destroy": accomplishment → telic → QUA → closed → licensed → "in X" ✓.

"melt": accomplishment → telic → QUA → closed → licensed → "in X" ✓.

"put": achievement → telic → QUA → closed → licensed → "in X" ✓.

"meet": achievement → telic → QUA → closed → licensed → "in X" ✓.

Motion verbs have both vendlerClass and levinClass annotations. Verify these are consistent: inherently-directed-motion verbs (achievements) have bounded paths, manner-of-motion verbs (activities) have no inherent path.

theorem Phenomena.TenseAspect.Studies.AspectualConsistency.arrive_motion_consistent :

Fragments.English.Predicates.Verbal.arrive.vendlerClass = some Semantics.Tense.Aspect.LexicalAspect.VendlerClass.achievement ∧ Fragments.English.Predicates.Verbal.arrive.levinClass = some LevinClass.inherentlyDirectedMotion ∧ LevinClass.inherentlyDirectedMotion.pathSpec = some Core.Path.PathShape.bounded

"arrive": achievement + inherentlyDirectedMotion + bounded path.

theorem Phenomena.TenseAspect.Studies.AspectualConsistency.leave_motion_consistent :

Fragments.English.Predicates.Verbal.leave.vendlerClass = some Semantics.Tense.Aspect.LexicalAspect.VendlerClass.achievement ∧ Fragments.English.Predicates.Verbal.leave.levinClass = some LevinClass.leave ∧ LevinClass.leave.pathSpec = some Core.Path.PathShape.source

"leave": achievement + leave class + source path.

theorem Phenomena.TenseAspect.Studies.AspectualConsistency.run_motion_consistent :

Fragments.English.Predicates.Verbal.run.vendlerClass = some Semantics.Tense.Aspect.LexicalAspect.VendlerClass.activity ∧ Fragments.English.Predicates.Verbal.run.levinClass = some LevinClass.mannerOfMotion ∧ LevinClass.mannerOfMotion.pathSpec = none

"run": activity + mannerOfMotion + no inherent path.

These tests loop over allVerbs so adding a new verb to the fragment automatically includes it in the test suite — no per-verb theorem needed. If a new verb has an inconsistent annotation, native_decide fails.

def Phenomena.TenseAspect.Studies.AspectualConsistency.pipelineOK (v : Fragments.English.Predicates.Verbal.VerbEntry) :

Pipeline consistency: for any verb with a vendlerClass annotation, the VendlerClass → Telicity → MereoTag → Boundedness chain must produce a licensing prediction that agrees with the for/in diagnostic. Returns true for verbs without vendlerClass (vacuously OK).

Equations

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

Instances For

theorem Phenomena.TenseAspect.Studies.AspectualConsistency.all_verbs_pipeline_ok :

Fragments.English.Predicates.Verbal.allVerbs.all pipelineOK = true

Every verb in the fragment passes pipeline consistency.

def Phenomena.TenseAspect.Studies.AspectualConsistency.incClassCoherent (v : Fragments.English.Predicates.Verbal.VerbEntry) :

VendlerClass × VerbIncClass coherence: sinc/inc verbs must be accomplishments (telic), cumOnly verbs must be activities (atelic). Returns true for verbs without verbIncClass (vacuously OK).

Equations

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

Instances For

theorem Phenomena.TenseAspect.Studies.AspectualConsistency.all_verbs_inc_coherent :

Fragments.English.Predicates.Verbal.allVerbs.all incClassCoherent = true

Every verb in the fragment has coherent VendlerClass × VerbIncClass.

def Phenomena.TenseAspect.Studies.AspectualConsistency.gradSSRComplementary (v : Fragments.English.Predicates.Verbal.VerbEntry) :

GRAD × SSR complementarity: no verb should predict both gradual change (sinc/inc) and subinterval reference (state/activity). Returns true if the verb doesn't predict both.

Equations

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

Instances For

theorem Phenomena.TenseAspect.Studies.AspectualConsistency.all_verbs_grad_ssr_complementary :

Fragments.English.Predicates.Verbal.allVerbs.all gradSSRComplementary = true

No verb in the fragment predicts both GRAD and SSR.

theorem Phenomena.TenseAspect.Studies.AspectualConsistency.vendler_coverage_count :

(List.filter (fun (v : Fragments.English.Predicates.Verbal.VerbEntry) => v.vendlerClass.isSome) Fragments.English.Predicates.Verbal.allVerbs).length = 237

Count of verbs with vendlerClass annotations (for coverage tracking). Bump this number when adding new vendlerClass annotations.

Every verb with a degreeAchievementScale also has a vendlerClass, and the derived vendlerClass from the scale matches the stipulated one. Adding a new degree achievement verb with inconsistent annotations will cause native_decide to fail.

def Phenomena.TenseAspect.Studies.AspectualConsistency.daVendlerConsistent (v : Fragments.English.Predicates.Verbal.VerbEntry) :

For a verb with degreeAchievementScale, check that vendlerClass is present and matches the derived value from the scale.

Equations

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

Instances For

theorem Phenomena.TenseAspect.Studies.AspectualConsistency.all_verbs_da_vendler_consistent :

Fragments.English.Predicates.Verbal.allVerbs.all daVendlerConsistent = true

Every verb with degreeAchievementScale has vendlerClass matching the derived value.