Cost-Aware Type Theory

TL;DR

The paper introduces CATT, a computational type theory incorporating cost as a primitive, enabling analysis of program complexity and a foundation for feasible proofs.

Contribution

It presents CATT, a novel type theory with a cost-aware dependent function type, bridging complexity analysis and type theory principles.

Findings

CATT includes a new 'funtime' dependent function type with cost semantics.

Proves lemmas and an introduction rule for the funtime type.

Demonstrates CATT's potential for analyzing computational complexity and feasible proofs.

Abstract

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.