A Complete V-Equational System for Graded lambda-Calculus

TL;DR

This paper develops a comprehensive V-equational system for graded lambda-calculus, enabling nuanced program equivalence reasoning with metrics, including timed and probabilistic behaviors, by introducing graded modal types and Lipschitz exponential comonads.

Contribution

It introduces a sound and complete V-equational system for graded lambda-calculus with modal types, extending previous linear systems to more expressive, non-linear contexts.

Findings

Established a V-equational system for graded lambda-calculus.

Constructed Lipschitz exponential comonads via a universal method.

Derived models for timed and probabilistic programming behaviors.

Abstract

Modern programming frequently requires generalised notions of program equivalence based on a metric or a similar structure. Previous work addressed this challenge by introducing the notion of a V-equation, i.e. an equation labelled by an element of a quantale V, which covers inter alia (ultra-)metric, classical, and fuzzy (in)equations. It also introduced a V-equational system for the linear variant of lambda-calculus where any given resource must be used exactly once. In this paper we drop the (often too strict) linearity constraint by adding graded modal types which allow multiple uses of a resource in a controlled manner. We show that such a control, whilst providing more expressivity to the programmer, also interacts more richly with V-equations than the linear or Cartesian cases. Our main result is the introduction of a sound and complete V-equational system for a lambda-calculus with graded modal types interpreted by what we call a Lipschitz exponential comonad. We also show how to build such comonads canonically via a universal construction, and use our results to derive graded metric equational systems (and corresponding models) for programs with timed and probabilistic behaviour.