事件时贫度与完备性的依赖类型计算

我们提出了一个用于分析事件时贫度和完备性的依赖类型跨语言框架，并附带了用于建模英文句子的示例。该框架包含两个部分：在名词域中，我们模型化名词短语的有界性及其与子类型、限定数量和形容词修饰的关系。在动词域中，我们定义一个依赖事件计算，将具有时贫度的事件定义为其承受者受到限制的事件，将完备事件定义为实现其内在终点的时贫度事件，并考虑副词修饰。在两个领域中，我们特别关注相关的蕴涵。该框架定义为intensional Martin-Löf依赖类型论的扩展，本文中的规则和示例已在Agda证明助手中形式化。