论文标题
成本感知类型理论
Cost-Aware Type Theory
论文作者
论文摘要
尽管计算复杂性是程序行为的一个基本方面，但它通常与诸如函数扩展之类的常见类型的理论原理矛盾，该原理可以通过相同的$ \ textit {input-output} $行为标识所有函数。我们提出了一种称为$ \ mathbf {catt} $的计算类型理论，该理论具有原始成本概念（评估步骤的数量）。我们引入了一种新的依赖功能类型“ funtime”，其语义可以看作是功能扩展的成本感知版本。我们证明了$ \ mathbf {catt} $的引理集合，其中包括新的Funtime类型的新简介规则。 $ \ mathbf {catt} $可以同时看作是分析程序的计算复杂性的框架，也可以作为表征可行数学证据的语义基础的开始。
Although computational complexity is a fundamental aspect of program behavior, it is often at odds with common type theoretic principles such as function extensionality, which identifies all functions with the same $\textit{input-output}$ behavior. We present a computational type theory called $\mathbf{CATT}$ that has a primitive notion of cost (the number of evaluation steps). We introduce a new dependent function type "funtime" whose semantics can be viewed as a cost-aware version of function extensionality. We prove a collection of lemmas for $\mathbf{CATT}$, including a novel introduction rule for the new funtime type. $\mathbf{CATT}$ can be simultaneously viewed as a framework for analyzing computational complexity of programs and as the beginnings of a semantic foundation for characterizing feasible mathematical proofs.
