A dependently-typed calculus of event telicity and culminativity

TL;DR

This paper introduces a dependently-typed framework for analyzing event telicity and culminativity across languages, formalized in Agda, with applications to English sentence modeling.

Contribution

It develops a novel dependently-typed calculus extending Martin-Löf type theory to model event properties and their linguistic entailments.

Findings

Framework models bounded noun phrases and event culminativity.

Formalization in Agda ensures rigorous proof of properties.

Application to English demonstrates practical utility.

Abstract

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\"of dependent type theory, and the rules and examples in this paper have been formalized in the Agda proof assistant.