The Lambda Calculus is Quantifiable

TL;DR

This paper develops quantitative methods for the lambda-calculus using partial metrics, enabling a metric-based analysis of lambda terms, their equational theories, and their connections to models like Scott topologies and Taylor expansions.

Contribution

It introduces new quantitative variants of lambda-calculus theories based on partial metrics, including applicative distances and a novel isometric view of Taylor expansion.

Findings

Quantitative variants of lambda calculus based on partial metrics.

Applicative distances capturing higher-order Scott topologies.

Taylor expansion of lambda terms can be represented as an isometric transformation.

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 $\lambda$-calculus, like those arising from B\"ohm 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\"ohm tree of a $\lambda$-term and its Taylor expansion, by showing that the latter can be presented as an isometric transformation.