Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

The Lambda Calculus is Quantifiable

Valentin Maestracci, Paolo Pistone

TL;DR

This paper introduces several quantitative methods for the lambda-calculus based on partial metrics, a well-studied variant of standard metric spaces that have been used to metrize non-Hausdorff topologies, like those arising from Scott domains.

Abstract

In this paper we introduce several quantitative methods for the lambda-calculus based on partial metrics, a well-studied variant of standard metric spaces that have been used to metrize non-Hausdorff topologies, like those arising from Scott domains. First, we study quantitative variants, based on program distances, of sensible equational theories for the $λ$-calculus, like those arising from Böhm trees and from the contextual preorder. Then, we introduce applicative distances capturing higher-order Scott topologies, including reflexive objects like the $D_\infty$ model. Finally, we provide a quantitative insight on the well-known connection between the Böhm tree of a $λ$-term and its Taylor expansion, by showing that the latter can be presented as an isometric transformation.

The Lambda Calculus is Quantifiable

TL;DR

This paper introduces several quantitative methods for the lambda-calculus based on partial metrics, a well-studied variant of standard metric spaces that have been used to metrize non-Hausdorff topologies, like those arising from Scott domains.

Abstract

In this paper we introduce several quantitative methods for the lambda-calculus based on partial metrics, a well-studied variant of standard metric spaces that have been used to metrize non-Hausdorff topologies, like those arising from Scott domains. First, we study quantitative variants, based on program distances, of sensible equational theories for the -calculus, like those arising from Böhm trees and from the contextual preorder. Then, we introduce applicative distances capturing higher-order Scott topologies, including reflexive objects like the model. Finally, we provide a quantitative insight on the well-known connection between the Böhm tree of a -term and its Taylor expansion, by showing that the latter can be presented as an isometric transformation.

Paper Structure

This paper contains 24 sections, 22 theorems, 8 equations.

Table of Contents

  1. Introduction
  2. Two notions of program approximation
  3. Quantifying $\lambda$-theories via partial metrics
  4. Contributions
  5. Outline
  6. Partial Metric Spaces
  7. Quantifying $\lambda$-Theories
  8. $\lambda$-PPMs
  9. Böhm Trees
  10. Contextual equivalence
  11. Quantifying Scott Domains
  12. Scott Domains via Partial Metrics
  13. Applicative distances and the function space
  14. Quantifying a Reflexive Object
  15. Quantifying Scott's $D_\infty$
  16. ...and 9 more sections

Key Result

Lemma 3.1

$x$ is generic in the topology $\mathcal{O}_p(X)$ iff $x\leq_p y$ holds for all $y\in X$.

Theorems & Definitions (57)

  • Definition 2.1
  • Definition 2.2: open balls, topology
  • Definition 2.3
  • Example 2.1: Sierpinski space
  • Example 2.2: Intervals
  • Example 2.3: Labeled trees
  • Definition 3.1
  • Lemma 3.1
  • proof
  • Remark 3.1
  • ...and 47 more