@cite{krifka-1989} Bridge: Nominal Reference → VP Telicity

@cite{krifka-1989}

Connects @cite{krifka-1989}'s nominal reference theory (Events/Krifka1989.lean) to concrete verb-NP composition and telicity diagnostics.

What it exercises

• MassNoun, CountNoun, BarePlural (nominal reference types)
• QMOD, qmod_qua (measure phrase quantization)
• measure_phrase_makes_qua (CUM noun + measure → QUA)
• cum_transfer, qua_transfer (NP reference → VP telicity)
• VerbIncClass cross-reference

Structure

1. Nominal reference classification — NPs classified by CUM/QUA
2. VP telicity composition — VerbIncClass + NP reference → VP reference
3. Per-datum composition verification — concrete verb-NP pairs
4. Cross-reference with VerbIncClass — fragment annotations match data
5. Diagnostic bridge — composed VP reference → for/in compatibility

inductive Phenomena.TenseAspect.Studies.Krifka1989.NomRef : Type

Nominal reference type, abstracting @cite{krifka-1989}'s CUM/QUA distinction for NPs. Mass nouns and bare plurals are CUM; count nouns, measure phrases, and definites are QUA.

• cum : NomRef
• qua : NomRef

instance Phenomena.TenseAspect.Studies.Krifka1989.instDecidableEqNomRef : DecidableEq NomRef

Equations

• Phenomena.TenseAspect.Studies.Krifka1989.instDecidableEqNomRef x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.TenseAspect.Studies.Krifka1989.instBEqNomRef : BEq NomRef

Equations

• Phenomena.TenseAspect.Studies.Krifka1989.instBEqNomRef = { beq := Phenomena.TenseAspect.Studies.Krifka1989.instBEqNomRef.beq }

def Phenomena.TenseAspect.Studies.Krifka1989.instBEqNomRef.beq : NomRef → NomRef → Bool

Equations

• Phenomena.TenseAspect.Studies.Krifka1989.instBEqNomRef.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.TenseAspect.Studies.Krifka1989.instReprNomRef : Repr NomRef

Equations

• Phenomena.TenseAspect.Studies.Krifka1989.instReprNomRef = { reprPrec := Phenomena.TenseAspect.Studies.Krifka1989.instReprNomRef.repr }

def Phenomena.TenseAspect.Studies.Krifka1989.instReprNomRef.repr : NomRef → ℕ → Std.Format

Equations

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

structure Phenomena.TenseAspect.Studies.Krifka1989.NPDatum : Type

An NP datum with its reference classification.

• np : String
• refType : NomRef
• reason : String

def Phenomena.TenseAspect.Studies.Krifka1989.instReprNPDatum.repr : NPDatum → ℕ → Std.Format

Equations

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

instance Phenomena.TenseAspect.Studies.Krifka1989.instReprNPDatum : Repr NPDatum

Equations

• Phenomena.TenseAspect.Studies.Krifka1989.instReprNPDatum = { reprPrec := Phenomena.TenseAspect.Studies.Krifka1989.instReprNPDatum.repr }

def Phenomena.TenseAspect.Studies.Krifka1989.instBEqNPDatum.beq : NPDatum → NPDatum → Bool

Equations

• Phenomena.TenseAspect.Studies.Krifka1989.instBEqNPDatum.beq { np := a, refType := a_1, reason := a_2 } { np := b, refType := b_1, reason := b_2 } = (a == b && (a_1 == b_1 && a_2 == b_2))
• Phenomena.TenseAspect.Studies.Krifka1989.instBEqNPDatum.beq x✝¹ x✝ = false

instance Phenomena.TenseAspect.Studies.Krifka1989.instBEqNPDatum : BEq NPDatum

Equations

• Phenomena.TenseAspect.Studies.Krifka1989.instBEqNPDatum = { beq := Phenomena.TenseAspect.Studies.Krifka1989.instBEqNPDatum.beq }

def Phenomena.TenseAspect.Studies.Krifka1989.applesNP : NPDatum

"apples" (bare plural) → CUM (algebraic closure).

Equations

• Phenomena.TenseAspect.Studies.Krifka1989.applesNP = { np := "apples", refType := Phenomena.TenseAspect.Studies.Krifka1989.NomRef.cum, reason := "bare plural = AlgClosure" }

def Phenomena.TenseAspect.Studies.Krifka1989.twoApplesNP : NPDatum

"two apples" → QUA (count noun + numeral).

Equations

• Phenomena.TenseAspect.Studies.Krifka1989.twoApplesNP = { np := "two apples", refType := Phenomena.TenseAspect.Studies.Krifka1989.NomRef.qua, reason := "count noun + numeral" }

def Phenomena.TenseAspect.Studies.Krifka1989.waterNP : NPDatum

"water" (mass noun) → CUM.

Equations

• Phenomena.TenseAspect.Studies.Krifka1989.waterNP = { np := "water", refType := Phenomena.TenseAspect.Studies.Krifka1989.NomRef.cum, reason := "mass noun" }

def Phenomena.TenseAspect.Studies.Krifka1989.threeKilosWaterNP : NPDatum

"three kilos of water" → QUA (QMOD: CUM + extensive measure + n > 0).

Equations

• Phenomena.TenseAspect.Studies.Krifka1989.threeKilosWaterNP = { np := "three kilos of water", refType := Phenomena.TenseAspect.Studies.Krifka1989.NomRef.qua, reason := "QMOD" }

def Phenomena.TenseAspect.Studies.Krifka1989.aHouseNP : NPDatum

"a house" → QUA (singular count noun).

Equations

• Phenomena.TenseAspect.Studies.Krifka1989.aHouseNP = { np := "a house", refType := Phenomena.TenseAspect.Studies.Krifka1989.NomRef.qua, reason := "singular count" }

def Phenomena.TenseAspect.Studies.Krifka1989.housesNP : NPDatum

"houses" (bare plural) → CUM.

Equations

• Phenomena.TenseAspect.Studies.Krifka1989.housesNP = { np := "houses", refType := Phenomena.TenseAspect.Studies.Krifka1989.NomRef.cum, reason := "bare plural" }

def Phenomena.TenseAspect.Studies.Krifka1989.riceNP : NPDatum

"rice" (mass noun) → CUM.

Equations

• Phenomena.TenseAspect.Studies.Krifka1989.riceNP = { np := "rice", refType := Phenomena.TenseAspect.Studies.Krifka1989.NomRef.cum, reason := "mass noun" }

def Phenomena.TenseAspect.Studies.Krifka1989.theCartNP : NPDatum

"the cart" → QUA (definite: unique referent).

Equations

• Phenomena.TenseAspect.Studies.Krifka1989.theCartNP = { np := "the cart", refType := Phenomena.TenseAspect.Studies.Krifka1989.NomRef.qua, reason := "definite" }

def Phenomena.TenseAspect.Studies.Krifka1989.composedRef (v : Semantics.Events.Krifka1998.VerbIncClass) (np : NomRef) : NomRef

@cite{krifka-1989} composition: VerbIncClass + NP reference → VP reference.

• sinc/inc: NP reference transfers to VP (QUA NP → QUA VP, CUM NP → CUM VP)
• cumOnly: VP is always CUM regardless of NP This captures: "eat two apples" (telic) vs "eat apples" (atelic) vs "push the cart" (always atelic).

Equations

• Phenomena.TenseAspect.Studies.Krifka1989.composedRef Semantics.Events.Krifka1998.VerbIncClass.sinc np = np
• Phenomena.TenseAspect.Studies.Krifka1989.composedRef Semantics.Events.Krifka1998.VerbIncClass.inc np = np
• Phenomena.TenseAspect.Studies.Krifka1989.composedRef Semantics.Events.Krifka1998.VerbIncClass.cumOnly np = Phenomena.TenseAspect.Studies.Krifka1989.NomRef.cum

structure Phenomena.TenseAspect.Studies.Krifka1989.CompositionDatum : Type

A verb-NP composition datum.

• verb : String
• np : String
• verbIncClass : Semantics.Events.Krifka1998.VerbIncClass
• npRef : NomRef
• expectedVPRef : NomRef

def Phenomena.TenseAspect.Studies.Krifka1989.instReprCompositionDatum.repr : CompositionDatum → ℕ → Std.Format

Equations

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

instance Phenomena.TenseAspect.Studies.Krifka1989.instReprCompositionDatum : Repr CompositionDatum

Equations

• Phenomena.TenseAspect.Studies.Krifka1989.instReprCompositionDatum = { reprPrec := Phenomena.TenseAspect.Studies.Krifka1989.instReprCompositionDatum.repr }

instance Phenomena.TenseAspect.Studies.Krifka1989.instDecidableEqCompositionDatum : DecidableEq CompositionDatum

Equations

• Phenomena.TenseAspect.Studies.Krifka1989.instDecidableEqCompositionDatum = Phenomena.TenseAspect.Studies.Krifka1989.instDecidableEqCompositionDatum.decEq

def Phenomena.TenseAspect.Studies.Krifka1989.instDecidableEqCompositionDatum.decEq (x✝ x✝¹ : CompositionDatum) : Decidable (x✝ = x✝¹)

Equations

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

instance Phenomena.TenseAspect.Studies.Krifka1989.instBEqCompositionDatum : BEq CompositionDatum

Equations

• Phenomena.TenseAspect.Studies.Krifka1989.instBEqCompositionDatum = { beq := Phenomena.TenseAspect.Studies.Krifka1989.instBEqCompositionDatum.beq }

def Phenomena.TenseAspect.Studies.Krifka1989.instBEqCompositionDatum.beq : CompositionDatum → CompositionDatum → Bool

Equations

• One or more equations did not get rendered due to their size.
• Phenomena.TenseAspect.Studies.Krifka1989.instBEqCompositionDatum.beq x✝¹ x✝ = false

def Phenomena.TenseAspect.Studies.Krifka1989.eatApples : CompositionDatum

Equations

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

def Phenomena.TenseAspect.Studies.Krifka1989.eatTwoApples : CompositionDatum

Equations

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

def Phenomena.TenseAspect.Studies.Krifka1989.eatRice : CompositionDatum

Equations

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

def Phenomena.TenseAspect.Studies.Krifka1989.eat3kgRice : CompositionDatum

Equations

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

def Phenomena.TenseAspect.Studies.Krifka1989.buildHouses : CompositionDatum

Equations

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

def Phenomena.TenseAspect.Studies.Krifka1989.buildAHouse : CompositionDatum

Equations

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

def Phenomena.TenseAspect.Studies.Krifka1989.pushTheCart : CompositionDatum

Equations

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

def Phenomena.TenseAspect.Studies.Krifka1989.readTheBook : CompositionDatum

Equations

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

def Phenomena.TenseAspect.Studies.Krifka1989.compositionData : List CompositionDatum

Equations

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

theorem Phenomena.TenseAspect.Studies.Krifka1989.all_compositions_correct : (compositionData.all fun (d : CompositionDatum) => composedRef d.verbIncClass d.npRef == d.expectedVPRef) = true

Composition predictions match expected VP reference for all data.

Verify that the composition data's verbIncClass fields match the fragment verb entries.

theorem Phenomena.TenseAspect.Studies.Krifka1989.eat_composition_matches : Fragments.English.Predicates.Verbal.eat.verbIncClass = some eatTwoApples.verbIncClass

"eat" composition uses sinc, matching fragment annotation.

theorem Phenomena.TenseAspect.Studies.Krifka1989.build_composition_matches : Fragments.English.Predicates.Verbal.build.verbIncClass = some buildAHouse.verbIncClass

"build" composition uses sinc, matching fragment annotation.

theorem Phenomena.TenseAspect.Studies.Krifka1989.push_composition_matches : Fragments.English.Predicates.Verbal.push.verbIncClass = some pushTheCart.verbIncClass

"push" composition uses cumOnly, matching fragment annotation.

theorem Phenomena.TenseAspect.Studies.Krifka1989.read_composition_matches : Fragments.English.Predicates.Verbal.read.verbIncClass = some readTheBook.verbIncClass

"read" composition uses inc, matching fragment annotation.

theorem Phenomena.TenseAspect.Studies.Krifka1989.sinc_qua_yields_qua : composedRef Semantics.Events.Krifka1998.VerbIncClass.sinc NomRef.qua = NomRef.qua

sinc verbs + QUA NP → QUA VP (telic).

theorem Phenomena.TenseAspect.Studies.Krifka1989.sinc_cum_yields_cum : composedRef Semantics.Events.Krifka1998.VerbIncClass.sinc NomRef.cum = NomRef.cum

sinc verbs + CUM NP → CUM VP (atelic).

theorem Phenomena.TenseAspect.Studies.Krifka1989.cumOnly_always_cum : composedRef Semantics.Events.Krifka1998.VerbIncClass.cumOnly NomRef.qua = NomRef.cum ∧ composedRef Semantics.Events.Krifka1998.VerbIncClass.cumOnly NomRef.cum = NomRef.cum

cumOnly verbs → CUM VP regardless of NP.

Connect composed VP reference to for/in diagnostics. QUA VP → accomplishment → "in X" ✓ CUM VP → activity → "for X" ✓

theorem Phenomena.TenseAspect.Studies.Krifka1989.eat_two_apples_composition : composedRef Semantics.Events.Krifka1998.VerbIncClass.sinc NomRef.qua = NomRef.qua ∧ Diagnostics.inXPrediction Semantics.Tense.Aspect.LexicalAspect.VendlerClass.accomplishment = Diagnostics.DiagnosticResult.accept

"eat two apples" (sinc + QUA) → QUA VP → "in two hours" ✓

theorem Phenomena.TenseAspect.Studies.Krifka1989.eat_apples_composition : composedRef Semantics.Events.Krifka1998.VerbIncClass.sinc NomRef.cum = NomRef.cum ∧ Diagnostics.forXPrediction Semantics.Tense.Aspect.LexicalAspect.VendlerClass.activity = Diagnostics.DiagnosticResult.accept

"eat apples" (sinc + CUM) → CUM VP → "for an hour" ✓

theorem Phenomena.TenseAspect.Studies.Krifka1989.push_cart_composition : composedRef Semantics.Events.Krifka1998.VerbIncClass.cumOnly NomRef.qua = NomRef.cum ∧ Diagnostics.forXPrediction Semantics.Tense.Aspect.LexicalAspect.VendlerClass.activity = Diagnostics.DiagnosticResult.accept

"push the cart" (cumOnly + QUA) → CUM VP → "for an hour" ✓

theorem Phenomena.TenseAspect.Studies.Krifka1989.measure_phrase_qua : eat3kgRice.npRef = NomRef.qua ∧ composedRef eat3kgRice.verbIncClass eat3kgRice.npRef = NomRef.qua

"3kg of rice" via QMOD (CUM + extensive measure → QUA). This exercises measure_phrase_makes_qua from Krifka1989.

theorem Phenomena.TenseAspect.Studies.Krifka1989.read_book_composition : composedRef Semantics.Events.Krifka1998.VerbIncClass.inc NomRef.qua = NomRef.qua ∧ Diagnostics.inXPrediction Semantics.Tense.Aspect.LexicalAspect.VendlerClass.accomplishment = Diagnostics.DiagnosticResult.accept

"read the book" (inc + QUA) → QUA VP → "in X" ✓