Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

The syntactic side of autonomous categories enriched over generalised metric spaces

Fredrik Dahlqvist, Renato Neves

TL;DR

The idea of equivalence taking values in a quantale V is explored, which covers the cases of (in)equations and (ultra)metric equations among others, and a V-equational deductive system for linear {\lambda}-calculus is introduced together with a proof that it is sound and complete.

Abstract

Programs with a continuous state space or that interact with physical processes often require notions of equivalence going beyond the standard binary setting in which equivalence either holds or does not hold. In this paper we explore the idea of equivalence taking values in a quantale V, which covers the cases of (in)equations and (ultra)metric equations among others. Our main result is the introduction of a V-equational deductive system for linear λ-calculus together with a proof that it is sound and complete. In fact we go further than this, by showing that linear λ-theories based on this V-equational system form a category that is equivalent to a category of autonomous categories enriched over 'generalised metric spaces'. If we instantiate this result to inequations, we get an equivalence with autonomous categories enriched over partial orders. In the case of (ultra)metric equations, we get an equivalence with autonomous categories enriched over (ultra)metric spaces. We additionally show that this syntax-semantics correspondence extends to the affine setting. We use our results to develop examples of inequational and metric equational systems for higher-order programming in the setting of real-time, probabilistic, and quantum computing.

The syntactic side of autonomous categories enriched over generalised metric spaces

TL;DR

The idea of equivalence taking values in a quantale V is explored, which covers the cases of (in)equations and (ultra)metric equations among others, and a V-equational deductive system for linear {\lambda}-calculus is introduced together with a proof that it is sound and complete.

Abstract

Programs with a continuous state space or that interact with physical processes often require notions of equivalence going beyond the standard binary setting in which equivalence either holds or does not hold. In this paper we explore the idea of equivalence taking values in a quantale V, which covers the cases of (in)equations and (ultra)metric equations among others. Our main result is the introduction of a V-equational deductive system for linear λ-calculus together with a proof that it is sound and complete. In fact we go further than this, by showing that linear λ-theories based on this V-equational system form a category that is equivalent to a category of autonomous categories enriched over 'generalised metric spaces'. If we instantiate this result to inequations, we get an equivalence with autonomous categories enriched over partial orders. In the case of (ultra)metric equations, we get an equivalence with autonomous categories enriched over (ultra)metric spaces. We additionally show that this syntax-semantics correspondence extends to the affine setting. We use our results to develop examples of inequational and metric equational systems for higher-order programming in the setting of real-time, probabilistic, and quantum computing.
Paper Structure (18 sections, 27 theorems, 83 equations, 5 figures)

This paper contains 18 sections, 27 theorems, 83 equations, 5 figures.

Table of Contents

  1. Introduction
  2. Background: linear $\lambda$-theories and autonomous categories
  3. Linear $\lambda$-calculus, soundness and completeness
  4. Equivalence theorem between linear $\lambda$-theories and autonomous categories
  5. From equations to $\mathcal{V}$-equations
  6. Preliminaries
  7. A $\mathcal{V}$-equational deductive system
  8. Semantics of $\mathcal{V}$-equations
  9. $\mathcal{V}\lambda$-calculus, soundness, and completeness
  10. Equivalence theorem between linear $\mathcal{V}\lambda$-theories and $\mathcal{V}\text{-}\mathsf{Cat}_{\mathsf{sep}}$-autonomous categories
  11. Examples of linear $\mathcal{V} \lambda$-theories and their models
  12. Real-time computation
  13. Probabilistic computation
  14. Quantum computation
  15. Concluding notes
  16. ...and 3 more sections

Key Result

Theorem 2.1

The calculus defined by the rules of fig:lang enjoys the following properties:

Figures (5)

  • Figure 1: Term formation rules of linear $\lambda$-calculus.
  • Figure 2: Judgement interpretation on an autonomous category $\mathsf{C}$.
  • Figure 3: Equations corresponding to the axiomatics of autonomous categories.
  • Figure 4: $\mathcal{V}$-congruence rules.
  • Figure 5: Additional data for affine $\lambda$-calculus.

Theorems & Definitions (64)

  • Theorem 2.1
  • Lemma 2.2: Exchange and Substitution
  • Theorem 2.3
  • proof : Proof sketch
  • Definition 2.4: Linear $\lambda$-theories
  • Definition 2.5: Models of linear $\lambda$-theories
  • Theorem 2.6: Soundness & Completeness
  • proof : Proof sketch
  • Definition 2.7
  • Lemma 2.8
  • ...and 54 more