Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

A Complete V-Equational System for Graded lambda-Calculus

Fredrik Dahlqvist, Renato Neves

TL;DR

This paper drops the (often too strict) linearity constraint by adding graded modal types which allow multiple uses of a resource in a controlled manner and shows that such a control, whilst providing more expressivity to the programmer, also interacts more richly with V-equations than the linear or Cartesian cases.

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.

A Complete V-Equational System for Graded lambda-Calculus

TL;DR

This paper drops the (often too strict) linearity constraint by adding graded modal types which allow multiple uses of a resource in a controlled manner and shows that such a control, whilst providing more expressivity to the programmer, also interacts more richly with V-equations than the linear or Cartesian cases.

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.
Paper Structure (12 sections, 15 theorems, 25 equations, 4 figures)

This paper contains 12 sections, 15 theorems, 25 equations, 4 figures.

Table of Contents

  1. Introduction
  2. A graded $\lambda$-calculus and its interpretation
  3. The calculus
  4. The interpretation
  5. A complete $\mathcal{V}$-equational system for graded $\lambda$-calculus
  6. The $\mathcal{V}$-equational system
  7. Interpretation of $\mathcal{V}$-equations, soundness, and completeness
  8. A canonical construction of Lipschitz exponential comonads
  9. Applications to timed and probabilistic computation
  10. Timed computation and dilations
  11. Probabilistic computation
  12. Conclusions and future work

Key Result

proposition 1

Let us consider two lists of contexts $\Gamma_1,\dots, \Gamma_n$ and $\Gamma'_1,\dots,\Gamma'_n$, contexts $E$ and $E'$, and suppose that $E \in \mathrm{Sf}(\Gamma_1;\dots;\Gamma_n)$, $E' \in \mathrm{Sf}(\Gamma'_1;\dots;\Gamma'_n)$. Then the following clauses hold:

Figures (4)

  • Figure 1: Term formation rules of graded $\lambda$-calculus.
  • Figure 2: Equational schema of graded $\lambda$-calculus.
  • Figure 3: Judgement interpretation.
  • Figure 4: $\mathcal{V}$-congruence rules.

Theorems & Definitions (35)

  • remark 1
  • proposition 1
  • theorem 1
  • proof
  • lemma 1: Exchange and Substitution
  • proof
  • remark 2
  • remark 3
  • definition 1
  • definition 2
  • ...and 25 more