Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Canonicity for Cost-Aware Logical Framework via Synthetic Tait Computability

Runming Li, Robert Harper

TL;DR

The paper proves canonicity for cost-aware logical framework via synthetic Tait computability, resolving a prior conjecture by embedding the theory into a glued category and interpreting phases and modalities (including open/closed and strict glue types). It introduces a cost-aware CBPV language with a writer monad-like cost structure, defines a computability structure that models both values and computations, and shows that every closed computation of type $e : ed{ mcp}( ed{ extF}( ed{ at}))$ is equal to a costed canonical form $e = ed{ extstepp}^c( ed{ etp}( ed{ ext{sucp}}^n( ed{ extzero})))$ for some $c$ and $n$. The method leverages Artin gluing and the internal language of the glued category to streamline the proof of canonicity, avoiding much of the traditional heavy lifting of logical relations. The findings advance the meta-theory of cost-aware type theories and set the stage for future work on universes and integrating additional effects.

Abstract

In the original work on the cost-aware logical framework by Niu et al., a dependent variant of the call-by-push-value language for cost analysis, the authors conjectured that the canonicity property of the type theory can be succinctly proved via Sterling's synthetic Tait computability. This work resolves the conjecture affirmatively.

Canonicity for Cost-Aware Logical Framework via Synthetic Tait Computability

TL;DR

The paper proves canonicity for cost-aware logical framework via synthetic Tait computability, resolving a prior conjecture by embedding the theory into a glued category and interpreting phases and modalities (including open/closed and strict glue types). It introduces a cost-aware CBPV language with a writer monad-like cost structure, defines a computability structure that models both values and computations, and shows that every closed computation of type is equal to a costed canonical form for some and . The method leverages Artin gluing and the internal language of the glued category to streamline the proof of canonicity, avoiding much of the traditional heavy lifting of logical relations. The findings advance the meta-theory of cost-aware type theories and set the stage for future work on universes and integrating additional effects.

Abstract

In the original work on the cost-aware logical framework by Niu et al., a dependent variant of the call-by-push-value language for cost analysis, the authors conjectured that the canonicity property of the type theory can be succinctly proved via Sterling's synthetic Tait computability. This work resolves the conjecture affirmatively.

Paper Structure

This paper contains 40 sections, 3 theorems, 27 equations.

Table of Contents

  1. Introduction
  2. Toolbox for synthetic phase distinctions
  3. Propositions
  4. Extension types
  5. Open modality
  6. Closed modality
  7. Strict glue types
  8. Synthetic Tait computability
  9. Call-by-push-value
  10. Synopsis
  11. A refresher on cost-aware logical framework
  12. Category of judgments
  13. Computability structure of
  14. Computability structure of judgments
  15. Value types
  16. ...and 25 more sections

Key Result

theorem 1

For every closed computation $e : \F{\nat}$, there exists $c : \costty$ and $n : \mathbb{N}$ such that $e = \mstep{c}{\ret{n}}$, where $\textsf{suc}^n$ is the $n$-fold successor.

Theorems & Definitions (4)

  • theorem 1: Canonicity
  • remark 1
  • theorem 2: Canonicity
  • theorem 3: Canonicity