A dependently-typed calculus of event telicity and culminativity
This work addresses a foundational issue in computational linguistics for researchers studying event semantics, but it is incremental as it builds on existing type theory.
The paper tackles the problem of analyzing event telicity and culminativity across languages by presenting a dependently-typed framework, formalized in Agda, to model boundedness in noun phrases and events with associated entailments.
We present a dependently-typed cross-linguistic framework for analyzing the telicity and culminativity of events, accompanied by examples of using our framework to model English sentences. Our framework consists of two parts. In the nominal domain, we model the boundedness of noun phrases and its relationship to subtyping, delimited quantities, and adjectival modification. In the verbal domain we define a dependent event calculus, modeling telic events as those whose undergoer is bounded, culminating events as telic events that achieve their inherent endpoint, and consider adverbial modification. In both domains we pay particular attention to associated entailments. Our framework is defined as an extension of intensional Martin-Löf dependent type theory, and the rules and examples in this paper have been formalized in the Agda proof assistant.