Documentation

Linglib.Theories.Semantics.Aspect.Incremental

Incrementality (SINC, INC) and Verb-Class Typeclass Hierarchy #

@cite{krifka-1998} @cite{tenny-1994} @cite{dowty-1991}

The incrementality story: a thematic relation θ that establishes a correspondence between an object and an event. K98 distinguishes:

SINC (strictly incremental, eq. 51): bijective sub-object ↔ sub-event correspondence (consumption/creation: eat the apples, draw the circle).
INC (incremental, eq. 59): closure of some SINC θ′ under sum (allows backups: read the article).

Plus the verb-class typeclass hierarchy formed by these properties together with CumTheta (and UP) from ThematicRoleProperties.lean, declared as a mathlib-style extends chain:

IsCumThetaVerb (in ThematicRoleProperties.lean)
    ↑
IsIncVerb extends IsCumThetaVerb
    ↑
IsSincVerb extends IsIncVerb

so that synthesis automatically derives weaker classes from stronger ones. Mathlib analogue: Group extends Monoid extends Semigroup.

Topic-named (not paper-named): SINC originates in @cite{krifka-1998} §3.2 (eq. 51) but the underlying concept is shared by @cite{tenny-1994}'s aspectual roles, @cite{dowty-1991}'s proto-roles, and any modern incremental-theme account.

References #

@cite{krifka-1998} §3.2 (SINC eq. 51), §3.6 (INC eq. 59)
@cite{tenny-1994} (aspectual roles)
@cite{dowty-1991} (proto-roles)

Strict Incrementality (K98 §3.2 eq. 51) #

structure Semantics.Aspect.Incremental.SINC {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] (θ : α → β → Prop) :

Strict Incrementality (SINC): the conjunction of MSO, UO, MSE, UE plus a non-degeneracy condition requiring extended entities. @cite{krifka-1998} eq. 51:

SINC(θ) iff (i) MSO(θ) ∧ UO(θ) ∧ MSE(θ) ∧ UE(θ) (ii) ∃x,y∈U_P ∃e,e'∈U_E [y < x ∧ e' < e ∧ θ(x,e) ∧ θ(y,e')]

Condition (i) guarantees a bijective correspondence between the part structure of the object and the part structure of the event. Condition (ii) ensures θ actually applies to extended entities (ones with proper parts), ruling out degenerate cases where θ only relates atoms. K98 §3.2 page 13-14 worked example: eat the apples, draw the circle.

mso : ArgumentStructure.MSO θ
Proper subevents map to proper object parts.
uo : ArgumentStructure.UO θ
Each event part has a unique object counterpart.
mse : ArgumentStructure.MSE θ
Proper object parts map to proper subevents.
ue : ArgumentStructure.UE θ
Each object part has a unique event counterpart.
extended : ∃ (x : α) (y : α) (e : β) (e' : β), y < x ∧ e' < e ∧ θ x e ∧ θ y e'
Non-degeneracy: θ applies to at least one extended entity pair. eq. (51.ii): the relation must involve entities with proper parts, not just atoms.

Instances For

theorem Semantics.Aspect.Incremental.me_of_mse {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] {θ : α → β → Prop} (h : ArgumentStructure.MSE θ) :

ArgumentStructure.ME θ

MSE implies ME: weaken strict to non-strict. If proper parts map to proper subevents, then parts (including the whole) also map, taking e' = e when y = x.

theorem Semantics.Aspect.Incremental.mo_of_mso {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] {θ : α → β → Prop} (h : ArgumentStructure.MSO θ) :

ArgumentStructure.MO θ

MSO implies MO: weaken strict to non-strict (dual of me_of_mse).

theorem Semantics.Aspect.Incremental.me_of_sinc {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] {θ : α → β → Prop} (h : SINC θ) :

ArgumentStructure.ME θ

SINC implies ME (via MSE).

theorem Semantics.Aspect.Incremental.mo_of_sinc {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] {θ : α → β → Prop} (h : SINC θ) :

ArgumentStructure.MO θ

SINC implies MO (via MSO).

General Incrementality (K98 §3.6 eq. 59) #

@[reducible, inline]

abbrev Semantics.Aspect.Incremental.IncClosure {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] (θ' : α → β → Prop) :

α → β → Prop

General Incrementality (INC): θ is the closure of some strictly incremental θ' under sum formation. @cite{krifka-1998} eq. 59: θ is incremental iff there exists a SINC θ' such that θ(x,e) holds iff (x,e) can be decomposed into θ'-pairs that sum to (x,e). This handles "read the article" (allows re-reading/backups): reading events are built from strictly incremental reading-parts that can overlap in their object coverage.

Specialization of Semantics.Aspect.PrecedenceClosure with the trivial precedence condition: arbitrary sums are admitted.

Equations

Semantics.Aspect.Incremental.IncClosure θ' = Semantics.Aspect.PrecedenceClosure (fun (x x_1 : β) => True) θ'

Instances For

def Semantics.Aspect.Incremental.INC {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] (θ : α → β → Prop) :

General Incrementality: θ is the IncClosure of some SINC θ'.

Equations

Semantics.Aspect.Incremental.INC θ = ∃ (θ' : α → β → Prop), Semantics.Aspect.Incremental.SINC θ' ∧ ∀ (x : α) (e : β), θ x e ↔ Semantics.Aspect.Incremental.IncClosure θ' x e

Instances For

theorem Semantics.Aspect.Incremental.inc_of_sinc {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] {θ : α → β → Prop} (h : SINC θ) (hCum : ArgumentStructure.CumTheta θ) :

INC θ

SINC + CumTheta implies INC: a strictly incremental θ that is cumulative is trivially its own closure. CumTheta ensures the reverse direction: IncClosure θ ⊆ θ.

VerbIncClass — Verb Incrementality Classification (K98 §3.6) #

inductive Semantics.Aspect.Incremental.VerbIncClass :

Incrementality annotations for verbs. @cite{krifka-1998} §3.2-3.7: verbs differ in which thematic role properties their incremental theme satisfies.

sinc : VerbIncClass
Strictly incremental: consumption/creation verbs (K98 §3.2 page 13-14: eat the apples, draw the circle). Per K98 §3.7, build and write a sequence require the necessary-preparatory-event extension to fit cleanly.
inc : VerbIncClass
Incremental: allows backups (read the article, K98 §3.6).
cumOnly : VerbIncClass
Cumulative only: non-incremental (push, pull, carry, K98 §3.2 page 12-13). "cumOnly" is the formaliser's shorthand for "CumTheta-without-incrementality"; K98 doesn't use this literal label.

Instances For

@[implicit_reducible]

instance Semantics.Aspect.Incremental.instDecidableEqVerbIncClass :

DecidableEq VerbIncClass

Equations

Semantics.Aspect.Incremental.instDecidableEqVerbIncClass x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Semantics.Aspect.Incremental.instReprVerbIncClass :

Repr VerbIncClass

Equations

Semantics.Aspect.Incremental.instReprVerbIncClass = { reprPrec := Semantics.Aspect.Incremental.instReprVerbIncClass.repr }

def Semantics.Aspect.Incremental.instReprVerbIncClass.repr :

VerbIncClass → ℕ → Std.Format

Equations

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

Instances For

Verb-Class Typeclass Hierarchy #

Mathlib-style extends chain. The empirical K98 verb classes correspond to partition membership; the typeclass chain encodes structural strength: every property satisfied by a SINC verb is also satisfied by an INC verb, and every property satisfied by an INC verb is also satisfied by a CumTheta verb. So [IsSincVerb θ] → [IsIncVerb θ] → [IsCumThetaVerb θ] via extends.

Linguistic note: this is **not** a claim that *eat* (a SINC verb)
is empirically classified as both SINC and cumOnly. The typeclass
chain only encodes "*eat* satisfies all the properties needed to
apply theorems stated at the IsCumThetaVerb level." Empirical
verb-class membership is captured by `VerbIncClass` (above).

class Semantics.Aspect.Incremental.IsIncVerb {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] (θ : α → β → Prop) extends Semantics.ArgumentStructure.IsCumThetaVerb θ :

Incremental verbs (mathlib-discipline typeclass form bundling INC and inheriting CumTheta from IsCumThetaVerb via extends).

Linguistic exemplar (K98 §3.6 page 18): read (the article) — K98's running case for INC-but-not-SINC. Concretely, read fails UE (a passage can be read at two distinct subevents) and MSO (sub-events e₁ ⊕ e₂' ⊕ e₃ and e₁ ⊕ e₂ ⊕ e₃ relate to the same object), and additionally fails ME on the spine of a book (K98 §3.7 page 19 — the spine, though part of the book, isn't subjected to a reading event). The "allows backups" gloss is correct but partial.

Strictly weaker than IsSincVerb: every SINC verb is INC via the extends chain (witness: inc_of_sinc), but not conversely.

cumTheta : CumTheta θ
inc : INC θ
General incrementality: θ is the IncClosure of some SINC θ' (K98 eq. 59).

Instances

class Semantics.Aspect.Incremental.IsSincVerb {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] (θ : α → β → Prop) extends Semantics.Aspect.Incremental.IsIncVerb θ :

Strictly incremental verbs (mathlib-discipline typeclass form bundling SINC and UP, inheriting INC and CumTheta from IsIncVerb via extends).

Bundles the witnesses that qua_propagation and cum_propagation require for the K89 → K98 propagation chain.

Linguistic exemplars (K98 §3.2 page 13-14): eat (the apples) and draw (the circle) — pure consumption / creation verbs whose object incrementally measures out the event with no backups. K98 §3.6 distinguishes these from INC-only verbs like read. K98 §3.7 explicitly flags build (a house) and write (a sequence of numbers) as needing the "necessary preparatory event" extension to fit the schema — they are NOT clean SINC exemplars and instances should not be declared without addressing K98's §3.7 caveats (scaffold erection, sequence-quantization, surface-only verbs like peel).

Smart constructor IsSincVerb.mk' derives the inherited inc field automatically via inc_of_sinc; consumers usually want mk' rather than the auto-generated mk.

cumTheta : CumTheta θ
inc : INC θ
sinc : SINC θ
Strict incrementality: bijective correspondence between proper object parts and proper event parts (K98 eq. 51).
up : ArgumentStructure.UP θ
Uniqueness of participants: each event has at most one θ-filler (K98 eq. 43).

Instances

@[reducible]

def Semantics.Aspect.Incremental.IsSincVerb.mk' {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] {θ : α → β → Prop} (sinc : SINC θ) (up : ArgumentStructure.UP θ) (cumTheta : ArgumentStructure.CumTheta θ) :

Smart constructor for IsSincVerb: takes the three K98 meaning postulates (SINC, UP, CumTheta) and derives the inherited inc : INC θ field automatically via inc_of_sinc. The auto-generated IsSincVerb.mk requires consumers to provide inc explicitly, which is wasteful since SINC + CumTheta determines INC.

Use this when declaring concrete instances:

instance : IsSincVerb θ := IsSincVerb.mk' sinc up cumTheta

Equations

⋯ = ⋯

Instances For

Bridge: K98 SINC → Beavers Quantized #

K98 SINC and Beavers Quantized are related but DIFFERENT formal commitments: - K98 SINC: bijective sub-event ↔ sub-object correspondence (structural property of θ). - Beavers Quantized: patient ends event with specific final degree g_φ on a scale (scalar result-state property).

K98 SINC does NOT structurally imply Beavers Quantized — a
bijective theme-event correspondence says nothing about a final
state on a scale. The two coincide empirically for consumption /
creation verbs (*eat*, *build*) where the scale is "consumption
progress" with `g_φ = 1` (fully consumed/created), but the
inference requires an explicit `[HasScalarResult]` instance and a
final-degree witness.

This bridge is a SMART CONSTRUCTOR (not an `instance`) because the
final degree is verb-specific lexical content that cannot be
derived from SINC alone.

@[reducible]

def Semantics.Aspect.Incremental.IsQuantizedAffected.ofIsSincVerb {α : Type u_3} {β : Type u_4} {δ : Type u_5} [SemilatticeSup α] [SemilatticeSup β] [ArgumentStructure.Affectedness.HasScalarResult α δ β] [ArgumentStructure.Affectedness.HasLatentScale α β] (θ : α → β → Prop) [_h : IsSincVerb θ] (forget : ∀ (x : α) (e : β), (∃ (g : δ), ArgumentStructure.Affectedness.HasScalarResult.resultAt x g e) → ArgumentStructure.Affectedness.HasLatentScale.latentScale x e) (g_φ : δ) (h_quantized : ArgumentStructure.Affectedness.Quantized θ g_φ) :

ArgumentStructure.Affectedness.Hierarchy.IsQuantizedAffected θ

Bridge: a K98 SINC verb θ with an explicit final-degree witness becomes a Beavers IsQuantizedAffected instance. The forget link is needed to provide the inherited HasLatentScale derivation (any verb with a result state is a fortiori a force-recipient).

Example use:

instance : IsQuantizedAffected eatThemeToy :=
  IsQuantizedAffected.ofIsSincVerb (forget := ...) (g_φ := fullyEaten) (h := ...)

Equations

Semantics.Aspect.Incremental.IsQuantizedAffected.ofIsSincVerb θ forget g_φ h_quantized = Semantics.ArgumentStructure.Affectedness.Hierarchy.IsQuantizedAffected.mk' forget g_φ h_quantized

Instances For