2026-07-30T07:02:10Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:22791 2025-10-02T11:32:08Z ddc:004 open_access

The Lambda Calculus Is Quantifiable Maestracci, Valentin Pistone, Paolo Lambda-calculus Scott semantics Partial metric spaces Böhm trees Taylor expansion 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_∞ 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Valentin Maestracci and Paolo Pistone 2025 Is Part Of LIPIcs, Volume 326, 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CSL.2025.34 urn:nbn:de:0030-drops-227911 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2025.34 eng https://creativecommons.org/licenses/by/4.0/legalcode