The Lambda Calculus Is Quantifiable

Maestracci, Valentin; Pistone, Paolo

doi:10.4230/LIPIcs.CSL.2025.34

The Lambda Calculus Is Quantifiable

Valentin Maestracci

I2M, Université d’Aix-Marseille, France Paolo Pistone

LIP, Université Claude Bernard Lyon 1, France

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ö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 $\lambda$ -term and its Taylor expansion, by showing that the latter can be presented as an isometric transformation.

Keywords and phrases:

Lambda-calculus, Scott semantics, Partial metric spaces, Böhm trees, Taylor expansion

Funding:

Paolo Pistone: Research has been funded by the French project ANR-23-CPJ1-0054-01.

Copyright and License:

2012 ACM Subject Classification:

Theory of computation

\rightarrow

Lambda calculus ; Theory of computation

\rightarrow

Program semantics

Editors:

Jörg Endrullis and Sylvain Schmitz

Series and Publisher:

Leibniz International Proceedings in Informatics, Schloss Dagstuhl – Leibniz-Zentrum für Informatik

1 Introduction

Two notions of program approximation.

One of the fundamental goals of program semantics is to understand when two different programs compute the same function. This is why, since its origins, the semantics of the $\lambda$ -calculus, the mathematical foundation for higher-order programming languages, has been focused on the problem of program equivalence. Indeed, $\lambda$ -theories, the equational theories of the $\lambda$ -calculus, constitute one of the pillars of the mathematical theory behind this much studied language, ranging from more operational theories, like $\beta$ -equivalence, to more observational ones, like contextual equivalence.

Actually, several well-known denotational models of the $\lambda$ -calculus are not just the source for some $\lambda$ -theory, but they also provide a topological point of view on them: the interpretations of the $\lambda$ -calculus via Böhm trees, Scott domains or the Taylor expansion, involve spaces whose objects can be seen as limits of “finite” approximants, as well as continuous functions between such spaces, that is, functions commuting with such limits. In this way, the $\lambda$ -theory induced by a topological model is associated with a notion of approximation, in the sense that a program is equivalent to another program whenever the net of finite approximants of the first converges to the second.

However, in general computer science, the approximation of a program is more commonly thought as the fact of computing values which are close (possibly up to some probability) to those produced by the program itself. By the way, the replacement of computationally expensive algorithms by more efficient, but somehow inaccurate, ones, is pervasive in all domains involving probabilistic or numerical methods. This has motivated, in the last few years, a rise of interest towards semantic approaches to functional languages focused, rather than on program equivalence, on notions of program similarity [37, 17, 11, 14, 16]. In these approaches, each type is endowed with a pseudo-metric, measuring the amount to which two programs behave in a similar, although non necessarily equivalent, way, and thus providing ways to estimate the errors produced by approximated optimization methods. At the same time, since any pseudo-metric induces an equational theory over programs, namely the one formed by all the pairs of programs which are at no distance the one from the other, this approach can be seen as a way to enrich, or “topologize”, well-established notions of program equivalence.

Quantifying $\lambda$ -theories via partial metrics.

In a sense, the overall goal of this paper is to reconcile these two, apparently different, ways to look at program approximations, by developing metric counterparts to well-established methods for the $\lambda$ -calculus, thus providing ways to enrich $\lambda$ -theories with notions of program similarity.

One reason why one could wish to approximate $\lambda$ -theories by metrics is computational: while equational theories are generally undecidable, equivalences and, as we’ll see, distances of finite approximants can often be computed effectively. Could one thus express the equivalence between two terms as the fact that the distance between their respective approximants gets closer and closer to zero? This amounts to requiring that the limits in the topology $T_{1}$ generating the $\lambda$ -theory are also limits in the topology $T_{2}$ generated by some program pseudo-metric. In other words, that $T_{1}$ is finer than $T_{2}$ .

At the same time, since program metrics are generally undecidable as well, could the distances between two programs be themselves approximated by looking at the (computable) distances between their approximants? This amounts to requiring, conversely, that the metric limits, that is, the limits in $T_{2}$ , are also limits in the topology $T_{1}$ inducing the $\lambda$ -theory. In other words, that $T_{2}$ is finer than $T_{1}$ .

All this sums up to the following question: can we make the topology arising from the semantics and the topology arising from the metric coincide? At first, one would tend to answer no: for instance, while the topology of a metric space is always Hausdorff, the topologies arising from the semantics of the $\lambda$ -calculus (e.g. Scott domains) are not. Nevertheless, there is a well-known reply to this answer, namely partial metrics [8, 9, 28, 42, 40, 38], a well-studied variant of standard metrics developed in connection with ideas from program semantics. A partial metric differs from a standard metric in that the self-distances $p(x,x)$ need not be zero; correspondingly, one has a stronger triangular law of the form $p(x,y)\leq p(x,z)+p(z,y)-p(z,z)$ , taking into account the self-distance of the middle point $z$ . As a consequence, distinct points will not have disjoint neighborhoods, as soon as the self-distance of one makes it “too thick”, so to say, to separate it from the other.

In fact, any continuous domain with a countable basis is quantifiable (a term we borrow from [40]) by a partial metric. This means that its Scott topology does coincide with the topology induced by the metric [9, 35, 42, 40, 41], so that the limits in the Scott topology agree with the metric limits and viceversa.

While the quantification of domains via partial metrics has been well-known for a while, the application of such results to the study of higher-order languages has not been much explored so far. We do it in this paper: we introduce quantitative variants for well-known methods like Böhm trees, Scott domains and the Taylor expansion, based on partial metrics, at the same time providing ways to approximate their associated $\lambda$ -theories.

Contributions.

In this paper we show that several well-known approaches to the study of the $\lambda$ -calculus can be quantified, that is, enriched with metric reasoning on program similarity. Our contributions can be summarized as follows:

$\blacksquare$

We introduce a partial metric variant of the notion of sensible $\lambda$ -theory [5] and we explore quantitative versions of well-known theories like those arising from Böhm trees and the contextual preorder.
$\blacksquare$

We introduce applicative partial metrics, and we illustrate their use to quantify higher-order Scott domains as well as reflexive objects, like Scott’s model $D_{\infty}$ . This opens the way to apply metric techniques to typed or non-typed higher-order languages.
$\blacksquare$

Finally, we study the Taylor expansion of $\lambda$ -terms [18, 19, 4], a powerful technique inspired by ideas from linear logic, and show that it can be presented as an isometric transformation from Böhm trees to sets of resource $\lambda$ -terms, thus refining the well-known commutation theorem [20], that relates the corresponding $\lambda$ -theories.

Outline.

In Section 2 we recall basic notions about partial metric spaces. In Section 3 we introduce quantitative variants of sensible $\lambda$ -theories. In Section 4 we investigate the quantification of higher-order Scott domains via applicative distances, and in Section 5 we apply these ideas to the quantification of reflexive objects. In Section 6 we discuss the Taylor expansion. Finally, in Section 7 we indicate related work as well as a few future directions.

2 Partial Metric Spaces

In this section we introduce partial metric spaces and we illustrate a few examples.

Definition 1.

A function $p:X\times X\to[0,+\infty]$ is called a partial metric (PM) when it satisfies the following axioms:

(P1)

$p(x,x)\leq p(x,y)$ ,
(P2)

If $p(x,x)=p(x,y)=p(y,y)$ then $x=y$ ,
(P3)

$p(x,y)=p(y,x)$ ,
(P4)

$p(x,y)\leq p(x,z)+p(z,y)-p(z,z)$ .

$p$ is called a partial pseudo-metric (PPM) when it satisfies P1, P3 and P4, and a partial ultra-metric (PUM) when it satisfies P1, P3 and

(P4U): $p(x,y)\leq\max\{p(x,z),p(z,y)\}$ .

While in a standard (pseudo-)metric space each point is at distance $0$ from itself, condition P1 states that the distance of a point from itself is only required to be smaller than its distance from any other point. Condition P2 adapts the usual separation condition $d(x,y)=0\Rightarrow x=y$ to non-zero self-distances, and distinguishes PMs from PPMs. Condition P3 is the usual symmetry, while P4 is a strengthening of the triangular law of metric spaces, that also takes into account the possibly non-zero self-distance of the middle point $z$ . P4U is as for standard ultra-metric spaces. Notice that P4U implies P4, so PUMs are indeed PPMs. Notice that a PPM (resp. a PUM, a PM) $p$ always induces a pseudo-metric (resp. a ultra-metric, a metric) by the formula $d_{p}(x,y):=2p(x,y)-p(x,x)-p(y,y)$ .

A PPM $p$ induces a preorder on $X$ defined by $x\leq_{p}y$ iff $p(x,y)\leq p(x,x)$ . Notice that this implies by P1 that $p(x,y)=p(x,x)$ . When $p$ is a PM the preorder $\leq_{p}$ is indeed an order. With respect to this preorder, $p$ is antimonotonic in the sense that $x\leq_{p}x^{\prime}$ implies $p(x^{\prime},y)\leq p(x,y)$ . Intuitively, the higher points are those with smaller self-distance.

The symmetrization of the preorder $\leq_{p}$ yields an equivalence relation $\simeq_{p}$ . In the next section we will indeed explore the use of partial metrics as ways of approximating preorders or equivalence relations on $\lambda$ -terms. We will say that a PPM $p$ quantifies an order (resp. an equivalence) relation over $X$ when this relation coincides with $\leq_{p}$ (resp. $\simeq_{p}$ ).

Let us now talk about the topology induced by a PPM.

Definition 2 (open balls, topology).

Let $p$ be a PPM on $X$ . For any $x\in X$ and $\epsilon\in(0,+\infty)$ , the open ball of center $x$ and radius $\epsilon$ is the set $B_{\epsilon}^{p}(x)=\{y\in X\mid p(y,x)<p(x,x)+\epsilon\}$ . The topology of $p$ , noted $\mathcal{O}_{p}(X)$ , is formed by all subsets $U\subseteq X$ which are unions of open balls.

Recall that, by P1, the distance between two points $x, y$ is always greater or equal than the self-distances $p(x,x),p(y,y)$ . We could equivalently define open balls as for standard metric spaces, i.e. $B_{\epsilon}^{p}(x)=\{y\in X\mid p(y,x)<\epsilon\}$ , but this would make $B_{\epsilon}^{p}(x)$ empty whenever $\epsilon\leq p(x,x)$ . Open balls are upper: if $y\in B_{\epsilon}^{p}(x)$ and $y\leq_{p}y^{\prime}$ , by antimonotonicity we deduce $p(y^{\prime},x)\leq p(y,x)<p(x,x)+\epsilon$ , whence $y^{\prime}\in B_{\epsilon}^{p}(x)$ . As a consequence, all open sets $U\in\mathcal{O}_{p}(X)$ are upper.

Contrarily to standard metric spaces, the topology $\mathcal{O}_{p}(X)$ is not in general Hausdorff: suppose $x, y$ are distinct points such that $x\leq_{p}y$ ; since any open set containing $x$ must also contain $y$ , there can be no disjoint open sets $U, V$ such that $x\in U$ and $y\in V$ . In some cases, as we’ll see, $\mathcal{O}_{p}(X)$ may coincide with the Scott topology induced by the order $\leq_{p}$ .

In Sections 4 and 5 we will explore the use of partial metrics as ways of approximating (Scott) topologies on $\lambda$ -terms. We will say that a PPM $p$ quantifies a topology $\mathcal{O}(X)$ over $X$ when $\mathcal{O}(X)=\mathcal{O}_{p}(X)$ .

Continuous functions between PPMs can be defined in the usual topological sense: given PPMs $p,p^{\prime}$ , respectively on $X$ and $X^{\prime}$ , a function $f:X\to X^{\prime}$ is $p,p^{\prime}$ -continuous when $f^{-1}$ sends open sets in $\mathcal{O}_{p^{\prime}}(X^{\prime})$ onto open sets in $\mathcal{O}_{p}(X)$ . There is an equivalent $\epsilon/\delta$ -definition: $f$ is $p,p^{\prime}$ -continuous if for all $x\in X$ and $\epsilon>0$ , there exists $\delta>0$ such that $f(B_{\delta}^{p}(x))\subseteq B_{\epsilon}^{p^{\prime}}(f(x))$ .

We compare different PPMs on a set $X$ by relating the associated topologies:

Definition 3.

Given two PPMs $p,p^{\prime}$ on $X$ , we say that $p$ is finer than $p^{\prime}$ (noted $p\sqsubseteq p^{\prime}$ ) when $\mathcal{O}_{p^{\prime}}(X)\subseteq\mathcal{O}_{p}(X)$ .

Equivalently, $p\sqsubseteq p^{\prime}$ when the identity map $\mathrm{id}_{X}:X\to X$ is $p,p^{\prime}$ -continuous, i.e. every open $p^{\prime}$ -ball contains an open $p$ -ball around any of its points.

We conclude this short presentation with a few examples.

Example 4 (Sierpinski space).

The simplest example of a non-Hausdorff topology that is quantified by a partial metric is the Sierpinski space $S=\{0,1\}$ , with the Scott topology $\mathcal{O}_{\sigma}(S)=\{\emptyset,\{1\},\{0,1\}\}$ induced by the order $0\leq 1$ . Define the PM $s$ on $S$ by $s(0,0)=s(0,1)=1$ and $s(1,1)=0$ . Notice how this implies $0\leq_{s}1$ . Since $0$ has self-distance $1$ , the unique open balls are indeed $\emptyset$ , $\{1\}$ and $\{0,1\}$ , that is, $\mathcal{O}_{\sigma}(S)=\mathcal{O}_{s}(S)$ .

Example 5 (Intervals).

The closed intervals of $\mathbb{R}$ , noted $\mathbf{I}(\mathbb{R})$ , admit the PM $p_{\mathrm{int}}(I_{1},I_{2}):=\inf\{|b-a|\mid I_{1}\cup I_{2}\subseteq[a,b]\}$ , which is the size of the smallest interval containing $I_{1}$ and $I_{2}$ . The order defined by the metric here is intuitive, it is reverse inclusion/the Scott information order: $I\leq_{p_{int}}J$ iff $p_{\mathrm{int}}(I,J)\leq p_{\mathrm{int}}(I,I)$ iff $J\subseteq I$ . The more information one has, the higher. This example explains the choice of the word “partial”: an interval, in term of Scott topology, represents an information on a partial execution: we have yet to discover the precise real number that we are computing. By contrast, the total elements will be those with self distance $0$ (the ones where $p$ behaves like a regular metric), i.e. of the form $\{r\}$ , a complete information, of a terminated execution.

Example 6 (Labeled trees).

Let $\Sigma\mathrm{Tree}_{\leq\infty}$ be the set of (non necessarily finite) finitely branching $\Sigma$ -labeled trees, where $\Sigma$ is a countable set of labels. For any $\alpha\in\Sigma\mathrm{Tree}_{\leq\infty}$ , let $|\alpha|\in\mathbb{N}\cup\{\infty\}$ indicate the height of $\alpha$ . For any $n\in\mathbb{N}$ , let $\alpha_{n}$ be the finite tree obtained by truncating all paths of $\alpha$ at length $n$ , if $|\alpha|\geq n$ , and be undefined otherwise. We write $\alpha_{n}\triangleq\beta_{n}$ to indicate that $\alpha_{n}$ and $\beta_{n}$ are both definite and equal, and $\alpha_{n}\not\triangleq\beta_{n}$ for its negation. For any $\alpha,\beta\in\Sigma\mathrm{Tree}_{\leq\infty}$ , define $\mathrm{div}(\alpha,\beta):=\inf\{n\mid\alpha_{n}\triangleq\beta_{n}\text{ and% }\alpha_{n+1}\not\triangleq\beta_{n+1}\}$ .

The standard tree (ultra-)metric $d_{\mathrm{tree}}$ is defined by $d(\alpha,\beta)=0$ if $\alpha=\beta$ and $2^{-\mathrm{div}(\alpha,\beta)}$ otherwise. We obtain instead a PUM by simply letting $p_{\mathrm{tree}}(\alpha,\beta):=2^{-\mathrm{div}(\alpha,\beta)}$ (where it is intended that $2^{-\infty}=0$ ). For a finite tree $\alpha$ , its self-distance is $p_{\mathrm{tree}}(\alpha,\alpha)=2^{-|\alpha|}$ , while $p_{\mathrm{tree}}(\alpha,\alpha)=0$ holds iff $\alpha$ has infinite height. Also this case suggests that finite trees are seen as “partial” objects, while the infinite trees are the “total” ones. Indeed, $p_{\mathrm{tree}}$ , unlike $d_{\mathrm{tree}}$ , quantifies the Scott topology on $\Sigma\mathrm{Tree}_{\leq\infty}$ (see Section 4).

3 Quantifying $\lambda$ -Theories

In this section we introduce quantitative variants, based on partial metrics, of sensible $\lambda$ -theories that arise from well-studied models of the untyped lambda-calculus, that is, the theory of Böhm trees and the theory of contextual equivalence. Moreover, we lift several properties of such equational theories to the corresponding notion of program similarity.

$\lambda$ -PPMs.

Let us first recall the standard notion of $\lambda$ -theory [5].

Definition 7.

A $\lambda$ -theory $T$ is an equivalence relation $\simeq_{T}$ on the set $\Lambda$ of all $\lambda$ -terms satisfying the rules below:

(congr1): $M\simeq_{T}N\Rightarrow MP\simeq_{T}NP$ ,
(congr2): $M\simeq_{T}N\Rightarrow PM\simeq_{T}PN$ ,
( $\xi$ ): $M\simeq_{T}N\Rightarrow\lambda x.M\simeq_{T}\lambda x.N$ ,
( $\beta$ ): $(\lambda x.M)N\simeq_{T}M[N/x]$ .

A $\lambda$ -theory $T$ is said extensional when it satisfies the rule $(\eta)$ :

( $\eta$ ): $M\simeq_{T}\lambda x.Mx$ .

and sensible when it equates all unsolvable terms and does not equate a solvable and an unsolvable term.

Notice that a sensible theory $T$ must be consistent: it cannot equate all terms.

A $\lambda$ -theory may either arise from an operational theory (e.g. $\beta$ - and $\beta\eta$ -reduction) or be induced by a model (as the theory formed by all equations between terms that are interpreted by the same entity in the model). While there exists a continuum of different $\lambda$ -theories, beyond the theories of $\beta$ and $\beta\eta$ -equivalence (respectively, the smallest $\lambda$ -theory and the smallest extensional $\lambda$ -theory), very few theories have been studied in depth. Indeed, all most common denotational models of the untyped $\lambda$ -calculus induce one of the two sensible theories $\mathcal{B}$ , and $\mathcal{H}^{*}$ , that we consider below.

We now introduce a quantitative variant of $\lambda$ -theories. Let us first recall that a point $x$ in a topological space $X$ is said generic when its closure is $X$ or, equivalently, all its neighborhoods are dense in $X$ . For instance, $0$ is generic in the Sierpinski space $S$ . In the case of PPM we have the following:

Lemma 8.

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

Proof.

Call $x$ generic for $p$ if $x\leq_{p}y$ (that is, $p(y,x)=p(x,x)$ ) holds for all $y\in X$ . $x$ is generic for $p$ iff the only open ball centered at $x$ is $X$ : from $p(y,x)=p(x,x)$ it follows that for any $\epsilon>0$ , $y\in B_{\epsilon}(x)$ , that is, $B_{\epsilon}(x)=X$ ; conversely, if any open ball centered at $x$ is equal to $X$ , then, for all $\epsilon>0$ , $p(y,x)<p(x,x)+\epsilon$ , which implies $p(y,x)\leq p(x,x)$ and thus $p(y,x)=p(x,x)$ by P1.

Now, if $x$ is generic for $p$ , then any open set $U$ containing $x$ must contain some open ball $B_{\epsilon}(x)$ , which forces $U=X$ since $B_{\epsilon}(x)=X$ , so $x$ is generic in $\mathcal{O}_{p}(X)$ . Conversely, if $x$ is generic in $\mathcal{O}_{p}(X)$ , then for any $\epsilon>0$ , the closure of $B_{\epsilon}(x)$ is $X$ . This implies that for all $\epsilon>0$ , $p(y,x)\leq p(x,x)+\epsilon$ , and thus that $p(y,x)=p(x,x)$ , so $x$ is generic for $p$ . $\hfill\blacktriangleleft$

$\blacktriangleright$ Remark 9.

Generic points are indistinguishable: if $x$ and $y$ are both generic for $p$ , then from $p(y,y)=p(x,y)=p(x,x)$ it follows that $x\simeq_{p}y$ . Conversely, if $x$ is generic and $y$ is not, then, $x\not\simeq_{p}y$ : if $x\simeq_{p}y$ , then, since $p(y,x)=p(y,y)$ , for all $z$ , $p(y,z)\leq p(y,x)+p(x,z)-p(x,x)=p(y,x)+p(x,x)-p(x,x)=p(y,x)=p(y,y)$ , so $y$ would be generic as well.

Definition 10 ( $\lambda$ -PPM).

A pseudo-partial metric $p$ over $\Lambda$ is called a $\lambda$ -PPM (resp. an extensional $\lambda$ -PPM) if the following hold:

$\blacksquare$

$\simeq_{p}$ is a $\lambda$ -theory (resp. an extensional $\lambda$ -theory);
$\blacksquare$

all contexts $\mathtt{C}[-]$ correspond to $p$ -continuous maps $\Lambda\to\Lambda$ .

$p$ is called sensible if all unsolvable terms are generic while no solvable term is.

Observe that we do not require contexts to be non-expansive (or $1$ -Lipschitz), as in other standard metric approaches [37, 17, 15], but just continuous. Also notice that, by Remark 9, a sensible PPM $p$ must satisfy $M\simeq_{p}N$ for all unsolvable terms $M, N$ , and $M\not\simeq_{p}N$ for $M$ unsolvable and $N$ solvable: the associated $\lambda$ -theory $\simeq_{p}$ is thus sensible.

In the rest of this section we introduce $\lambda$ -PPMs quantifying the $\lambda$ -theories $\mathcal{B}$ and $\mathcal{H}^{*}$ .

Böhm Trees.

The interpretation of $\lambda$ -terms as Böhm trees is one of the fundamental tools in the $\lambda$ -calculus. The Böhm tree $\mathcal{B}(M)$ of a $\lambda$ -term $M$ is a $(\Lambda\cup\{\bot\})$ -labeled tree defined co-inductively as follows:

$\blacksquare$

if $M$ reduces to $\lambda x_{1}.\dots.\lambda x_{m}.xM_{1}\dots M_{n}$ , then $\mathcal{B}(M)$ has a root with label $\lambda x_{1}.\dots.\lambda x_{m}.x$ and $n$ subtrees $\mathcal{B}(M_{1}),\dots,\mathcal{B}(M_{n})$ ;
$\blacksquare$

otherwise, $\mathcal{B}(M)$ only consists of the root, with label $\bot$ .

An alternative presentation of $\mathcal{B}(M)$ is via partial terms, which are $\lambda$ -terms in normal form, enriched with the constant $\bot$ and rules $\lambda x.\bot\to\bot$ , $\bot M\to\bot$ . We note these partial terms $A,B,\dots$ . The set $\mathcal{A}$ of partial terms is ordered by the contextual closure $\preceq$ of the relation generated by $\bot\preceq A$ , for all $A\in\mathcal{A}$ . Partial terms correspond straightforwardly to finite Böhm trees.

For any $\lambda$ -term $M$ , let the partial term $M_{\mathcal{A}}$ be defined inductively as follows: $M_{\mathcal{A}}=\lambda\vec{x}.y(M_{1})_{\mathcal{A}}\dots(M_{n})_{\mathcal{A}}$ if $M=\lambda\vec{x}.yM_{1}\dots M_{n}$ , and $M_{\mathcal{A}}=\bot$ if $M=\lambda\vec{x}.(\lambda y.P)M_{1}\dots M_{n+1}$ . Let $A\leq M$ whenever $M$ $\beta$ -reduces to $M^{\prime}$ with $A\preceq M^{\prime}_{\mathcal{A}}$ . We then let $\mathcal{B}(M)=\{A\mid A\leq M\}$ . Observe that $\mathcal{B}(M)$ can be seen at the same time as a tree under the relation $\leq$ , and the standard tree ordering $\mathcal{B}(M)\preceq\mathcal{B}(N)$ holds precisely when $\mathcal{B}(M)$ is included in $\mathcal{B}(N)$ .

The $\lambda$ -theory $\mathcal{B}$ contains all equations $M\simeq_{\mathcal{B}}N$ , where $\mathcal{B}(M)=\mathcal{B}(N)$ . $\mathcal{B}$ is sensible but non-extensional (as e.g. $\mathcal{B}(\lambda x.x)\neq\mathcal{B}(\lambda x.\lambda y.xy)$ ).

We now introduce the corresponding $\lambda$ -PPM: we measure the distance between $\lambda$ -terms by comparing their Böhm trees via the tree partial metric.

Definition 11 (Böhm partial metric).

For any two $\lambda$ -terms $M, N$ , let

\displaystyle p_{\mathrm{B\"{o}hm}}(M,N)

\displaystyle:=p_{\mathrm{tree}}(\mathcal{B}(M),\mathcal{B}(N)).

Observe that $p_{\mathrm{B\"{o}hm}}(M,M)=0$ iff $\mathcal{B}(M)$ is infinite. It is not difficult to check that $p_{\mathrm{B\"{o}hm}}$ captures the theory $\mathcal{B}$ :

Proposition 12.

$M\leq_{p_{\mathrm{B\"{o}hm}}}N$ iff $\mathcal{B}(M)\leq\mathcal{B}(N)$ , and thus $M\simeq_{p_{\mathrm{B\"{o}hm}}}N$ iff $M\simeq_{\mathcal{B}}N$ .

As discussed in Section 4, $p_{\mathrm{B\"{o}hm}}$ captures the Scott topology of Böhm trees. This proves that contexts are continuous, and thus that $p_{\mathrm{B\"{o}hm}}$ is a $\lambda$ -PPM. Moreover, since $p_{\mathrm{tree}}(\bot,\alpha)=1$ , the unsolvable terms are generic, while, for any solvable term $M$ , $p_{\mathrm{B\"{o}hm}}(M,M)<1$ and thus, for any $\epsilon<1-p_{\mathrm{B\"{o}hm}}(M,M)$ , the open ball $B_{\epsilon}^{p_{\text{B\"{o}hm}}}(M)$ does not contain the term $\lambda x.M$ (since $p_{\mathrm{B\"{o}hm}}(M,\lambda x.M)=1>p_{\mathrm{B\"{o}hm}}(M,M)+\epsilon$ ).

$\blacktriangleright$ Remark 13.

While the theory $\mathcal{B}$ is $\Pi^{0}_{2}$ -complete, the distances $p_{\mathrm{tree}}(A,B)$ are effectively computable whenever $A, B$ are finite trees (equivalently, partial terms). Moreover, to check that $p_{\mathrm{B\"{o}hm}}(M,N)<\epsilon$ , it is necessary and sufficient to find approximants $A\leq M$ and $B\leq N$ such that $p_{\mathrm{tree}}(A,B)<\epsilon$ .

Contextual equivalence.

We now consider the theory arising from contextual equivalence. Let $M\sqsubseteq_{\mathrm{ctx}}N$ if for all context $\mathtt{C}[-]$ , if $\mathtt{C}[M]$ is solvable, then $\mathtt{C}[N]$ is solvable. The theory $\mathcal{H}^{*}$ contains all equations $M\simeq_{H^{*}}N$ where $M\sqsubseteq_{\mathrm{ctx}}N$ and $N\sqsubseteq_{\mathrm{ctx}}M$ both hold. It is extensional and sensible, and is indeed the maximum sensible theory.

To quantify $\mathcal{H}^{*}$ we define the following distance:

Definition 14 (contextual partial metric).

For all terms $M, N$ , we define

p_{\mathrm{ctx}}(M,N)=\sum_{n=0}^{\infty}\left\{\frac{1}{2^{n}}\ \Big{|}\ % \mathtt{C}_{n}[M]\text{ is unsolvable or }\mathtt{C}_{n}[N]\text{ is % unsolvable}\right\},

where $(\mathtt{C}_{n}[-])_{n\in\mathbb{N}}$ is an enumeration of all contexts.

The distance $p_{\mathrm{ctx}}(M,N)$ intuitively counts all contexts $\mathtt{C}_{n}[-]$ that fail on either $M$ or $N$ . In particular, the self-distance $p_{\mathrm{ctx}}(M,M)$ counts the contexts that fail on $M$ .

The following result shows that $p_{\mathrm{ctx}}$ captures the contextual preorder:

Proposition 15.

$M\leq_{p_{\mathrm{ctx}}}N$ iff $M \sqsubseteq_{\mathrm{ctx}}N$ , and thus $M\simeq_{p_{\mathrm{ctx}}}N$ iff $M \simeq_{\mathcal{H}^{*}}N$ .

For the result above, the choice of the enumeration is irrelevant, as is the choice of the weights $\frac{1}{2^{n}}$ , which could be replaced by arbitrary weights $\theta_{n}$ summing up to $1$ .

$\blacktriangleright$ Remark 16.

Contrarily to contextual equivalence, which is $\Pi^{0}_{2}$ -complete as well, to check that $N\in B_{\epsilon}^{p_{\mathrm{ctx}}}(M)$ one does not need to look at the behavior of $M$ and $N$ under all contexts. Intuitively, $B_{\epsilon}^{p_{\mathrm{ctx}}}(M)$ contains all those programs that behave like $M$ on certain finitely many contexts. Indeed, $p_{\mathrm{ctx}}(M,N)<p_{\mathrm{ctx}}(M,M)+\epsilon$ means that the contexts on which $M$ does converge and $N$ does not sum up to some value strictly smaller than $\epsilon$ . This is true iff $N$ converges on those finitely many contexts $\mathtt{C}_{i}[-]$ , where $2^{-(i+1)}\leq\epsilon$ , on which $M$ converges.

Proposition 17.

$p_{\mathrm{ctx}}$ is a sensible extensional $\lambda$ -PPM.

Proof.

Let us show that contexts yield continuous maps. Take a term $M$ , $\epsilon>0$ and a context $\mathtt{C}$ . We need to find some $\delta>0$ such that for all $P\in B_{\delta}^{p_{\mathrm{ctx}}}(M)$ , $\mathtt{C}[P]\in B_{\epsilon}^{p_{\mathrm{ctx}}}(\mathtt{C}[M])$ . By Remark 16 there exists a finite number of contexts $\mathtt{C}_{1},\dots,\mathtt{C}_{k}$ such that $\mathtt{C}_{i}[\mathtt{C}[M]]$ is solvable and $N\in B_{\epsilon}^{p_{\mathrm{ctx}}}(\mathtt{C}[M])$ iff $\mathtt{C}_{i}[N]$ is solvable for $i=1,\dots,k$ . Take $m$ such that for all $i=1,\dots,k$ , the context $\mathtt{C}_{i}[\mathtt{C}[-]]$ has an index smaller than $m$ , and let $\delta=2^{-m}$ . Notice that $\mathtt{C}_{i}[\mathtt{C}[M]]$ is solvable. Moreover, for any term $P$ , if $P\in B_{\delta}^{p_{\mathrm{ctx}}}(M)$ , then $\mathtt{C}_{i}[\mathtt{C}[P]]$ must be solvable for all $i=1,\dots,m$ . This implies then that $\mathtt{C}[P]\in B_{\epsilon}^{p_{\mathrm{ctx}}}(\mathtt{C}[M])$ , as desired.

The sensibility of $p_{\mathrm{ctx}}$ essentially follows from the well-known genericity lemma [5, 2]: if $\mathtt{C}[M]$ is solvable, where $M$ is unsolvable, then $\mathtt{C}[N]$ must be solvable for all $N$ ; this implies that for any unsolvable $M$ , and for any term $N$ , $p_{\mathrm{ctx}}(M,N)=p_{\mathrm{ctx}}(M,M)$ , so $M$ is generic in $p_{\mathrm{ctx}}$ . Conversely, if $M$ is solvable, then, for any unsolvable term $N$ , one can easily construct a context $\mathtt{C}$ such that $\mathtt{C}[M]$ reduces to $\lambda x.x$ and $\mathtt{C}[N]$ diverges. This allows us to conclude that $p_{\mathrm{ctx}}(M,N)>p_{\mathrm{ctx}}(M,M)$ , and thus that $M$ is not generic in $p$ . $\hfill\blacktriangleleft$

Similarly to the $\lambda$ -theory $\mathcal{H}^{*}$ , the $\lambda$ -PPM $p_{\mathrm{ctx}}$ is maximum among sensible $\lambda$ -PPMs.

Proposition 18.

For any sensible $\lambda$ -PPM $p$ , $p\sqsubseteq p_{\mathrm{ctx}}$ .

Proof.

Let $p$ be a sensible $\lambda$ -ppm. Consider a term $M$ and $\epsilon>0$ . We must find $\delta>0$ such that $B_{\delta}^{p}(M)\subseteq B_{\epsilon}^{p_{\mathrm{ctx}}}(M)$ . By Remark 16 there exists a finite number of contexts $\mathtt{C}_{1},\dots,\mathtt{C}_{k}$ such that $\mathtt{C}_{i}[M]$ is solvable and $N\in B_{\epsilon}^{p_{\mathrm{ctx}}}(M)$ iff $\mathtt{C}_{i}[N]$ is solvable for $i=1,\dots,k$ .

Fix an $i\leq k$ and let $Q_{i}=\mathtt{C}_{i}[M]$ . Since $Q_{i}$ is solvable and $p$ is sensible, we can find an open set $U_{i}$ containing $Q_{i}$ and not containing any unsolvable term. Since $p$ is a $\lambda$ -PPM, $\mathtt{C}_{i}$ corresponds to a continuous function, and thus $\mathtt{C}_{i}^{-1}(U_{i})$ contains some open ball $B^{p}_{\delta_{i}}(M)$ . Let $\delta=\min_{i}\delta_{i}$ : if $P\in B^{p}_{\delta}(M)$ , then for all $i=1,\dots,k$ , $\mathtt{C}_{i}[P]\in U_{i}$ , so it must be solvable. We conclude then that $P\in B_{\epsilon}^{p_{\mathrm{ctx}}}(M)$ . $\hfill\blacktriangleleft$

$\blacktriangleright$ Remark 19.

That $p_{\mathrm{B\"{o}hm}}\sqsubset p_{\mathrm{ctx}}$ can be easily seen directly: the elements of $B^{p_{\mathrm{ctx}}}_{\epsilon}(M)$ are those which converge on a finite number of contexts $\mathtt{C}_{1},\dots,\mathtt{C}_{k}$ on which $M$ converges too (cf. Remark 16). For any such context $\mathtt{C}_{i}$ , the convergence of $\mathtt{C}_{i}[M]$ to a head normal form only depends on the exploration of a finite portion of $\mathcal{B}(M)$ , say up to height $m_{i}$ . Letting $m=\max_{i}\{m_{i}\}$ and $\delta=2^{-m}$ , we have then that $B^{p_{\mathrm{B\"{o}hm}}}_{\delta}(M)\subseteq B^{p_{\mathrm{ctx}}}_{\epsilon}% (M)$ . The converse inclusion $p_{\mathrm{ctx}}\sqsubseteq p_{\mathrm{B\"{o}hm}}$ cannot hold: any open ball $B^{p_{\mathrm{B\"{o}hm}}}_{\epsilon}(I)$ around $I=\lambda x.x$ that does not contain its $\eta$ -expansion $\lambda x.\lambda y.xy$ contains no open $p_{\mathrm{ctx}}$ -ball around $I$ .

Other well-known characterizations of $\mathcal{H}^{*}$ exist, which suggest different ways to quantify this theory. One is in terms of the so-called Nakajima trees (cf. [5], Ex. 19.4.4, p. 511): these are a variant of Böhm trees that are invariant under the $\eta$ -rule. By adapting the tree partial metric one could then obtain another partial metric $p_{\mathrm{Nakajima}}$ that quantifies $\mathcal{H}^{*}$ .

Moreover, the theory $\mathcal{H}^{*}$ is induced by a large class of denotational models of the $\lambda$ -calculus (cf. [31]), including in particular the models based on Scott domains, that we discuss in Sections 4 and 5, or the relational model from [6], to which the techniques illustrated in those sections can be easily adapted.

4 Quantifying Scott Domains

As discussed in the introduction, the $\lambda$ -theories like $\mathcal{B}$ or $\mathcal{H}^{*}$ are induced by topological models, based on Scott domains, which provide notions of approximant for $\lambda$ -terms. In this section, after discussing the connection between partial metrics and Scott domains, we introduce applicative PPMs as a means to capture domains of Scott-continuous functions, and we illustrate how this leads to quantify topological models of typed $\lambda$ -calculi.

Scott Domains via Partial Metrics.

Let us recall some basic terminology about dcpos and Scott domains.

A partially ordered set $(X,\leq)$ is a dcpo (directed complete partial order) if all directed subsets of $X$ admit a least upper bound. The way below relation $\ll$ on a dcpo is defined by $x\ll y$ iff for all directed subset $\Delta\subseteq X$ , $y\leq\bigvee\Delta$ implies $x\leq d$ , for some $d\in\Delta$ . A point $x\in X$ is said compact if $x\ll x$ . A basis for a dcpo $X$ is a subset $B\subseteq X$ such that for any $x\in X$ , the set $\Delta=\{y\in B\mid y\ll x\}$ is directed and $x=\bigvee\Delta$ . A dcpo is said continuous if it has a basis and algebraic if it has a basis formed of compact elements. A domain is a continuous dcpo with a countable basis. A domain $X$ is bounded complete if for any finite set $Y\subseteq_{\mathrm{fin}}X$ , if an upper bound of $Y$ exists in $X$ , then $\bigvee Y$ exists in $X$ . A bounded complete and algebraic domain is called a Scott domain.

The Scott topology $\mathcal{O}_{\sigma}(X)$ on a partially ordered set $(X,\leq)$ has open sets being upper subsets $U\subseteq X$ which are finitely accessible: $x\in U$ implies $y\in U$ for some $y\ll x$ . A function $f:X\to Y$ between dcpos is said continuous iff $f$ is monotone and commutes with the lubs of directed subsets, that is, for all directed $\Delta\subseteq X$ , $f(\bigvee\Delta)=\bigvee f(\Delta)$ . This is equivalent to asking $f$ to be continuous, in the usual sense, with respect to the Scott topology. The category of bounded complete domains and continuous functions is cartesian closed (cf. [1]).

Let us specify what it means for a dcpo to be quantified by a partial metric.

Definition 20.

A dcpo $(X,\leq)$ is quantified by a PM $p$ when its associated Scott topology is quantified by $p$ , that is, when $\mathcal{O}_{p}(X)=\mathcal{O}_{\sigma}(X)$ .

Beyond the Sierpinski space $S$ , also the other two dcpos from Section 2 are quantified by the associated PMs (proofs are in the long version):

Proposition 21.

The interval dcpo $\mathbf{I}(\mathbb{R})$ is quantified by $p_{\mathrm{int}}$ (cf. Example 5). The domain $\Sigma\mathrm{Tree}_{\leq\infty}$ of $\Sigma$ -trees is quantified by $p_{\mathrm{tree}}$ (cf. Example 6).

When $p$ quantifies a dcpo $(X,\leq)$ , the order $\leq_{p}$ coincides with the order $\leq$ of the dcpo.

Lemma 22.

Suppose the dcpo $(X,\leq)$ is quantified by $p$ . Then $\leq$ coincides with $\leq_{p}$ .

Proof.

$\leq$ coincides with the specialization order $x\leq^{\mathcal{O}_{\sigma}(X)}y\Leftrightarrow\forall U\in\mathcal{O}_{\sigma% }(X)(x\in U\Rightarrow y\in U)$ ; similarly, $\leq_{p}$ coincides with the specialization order $x\leq^{\mathcal{O}_{p}(X)}y\Leftrightarrow\forall U\in\mathcal{O}_{p}(X)(x\in U% \Rightarrow y\in U)$ . From $\mathcal{O}_{\sigma}(X)=\mathcal{O}_{p}(X)$ we deduce that the two specialization orders coincide, and thus $\leq$ and $\leq_{p}$ as well. $\hfill\blacktriangleleft$

However, checking that a partial metric $p$ captures the order of the dcpo is not in general enough to deduce that $p$ quantifies the dcpo, as shown by Example 24 below. The following proposition provides necessary (but not sufficient) conditions.

Proposition 23.

Let $(X,\leq)$ be a continuous dcpo and $p$ a partial metric on $X$ such that $\leq$ coincides with $\leq_{p}$ .Then the following conditions are equivalent:

1.

$\mathcal{O}_{p}(X)\subseteq\mathcal{O}_{\sigma}(X)$ ;
2.

open $p$ -balls are finitely accessible;
3.

$p$ is Scott-continuous (as a map towards the dcpo $([0,+\infty],\geq)$ ).

Proof.

( $1\Leftrightarrow 2$ ): Since the open balls are upper sets, these are Scott open iff they are finitely accessible.
( $3\Rightarrow 2$ ): $p$ is Scott continuous when for all $x\in X$ and directed subset $\Delta\subseteq X$ one has $p(x,\bigvee\delta)=\inf_{d\in\delta}p(x,d)$ . Suppose $p$ is continuous and let $y\in B_{\epsilon}(x)$ . We need to show that there exists $y^{\prime}\ll y$ such that $y^{\prime}\in B_{\epsilon}(x)$ . This implies that for some $\epsilon^{\prime}<\epsilon$ , $p(y,x)<p(x,x)+\epsilon^{\prime}$ . Since $p$ is continuous and $y=\bigvee\{z\mid z\ll y\}$ we have then $\inf\{p(z,x)\mid z\ll y\}=p(y,x)<p(x,x)+\epsilon^{\prime}.$ This implies in turn that for some $y^{\prime}\ll y$ , $p(y^{\prime},x)\leq p(x,x)+\epsilon^{\prime}<p(x,x)+\epsilon$ , that is, $y^{\prime}\in B_{\epsilon}(x)$ .
( $2\Rightarrow 3$ ): Suppose that open $p$ -balls are finitely accessible, hence Scott open. Let $\Delta\subseteq X$ be a directed set and $x\in X$ . We need to prove that $p(x,\bigvee\Delta)=\inf_{d\in\Delta}p(x,d)$ . Observe that the “ $\leq$ ” direction directly follows from $d\leq\bigvee\Delta$ . To prove the “ $\geq$ ” direction we argue as follows: let $p(x,\bigvee\Delta)=p(x,x)+\delta$ , with $\delta\in\mathbb{R}_{\geq 0}$ . Let $\delta^{\prime}>\delta$ , so that we have $\bigvee\Delta\in B_{\delta^{\prime}}(x)$ . Since $B_{\delta^{\prime}}(x)$ is Scott-open, there exists $w\ll\bigvee\Delta$ such that $w\in B_{\delta^{\prime}}(x)$ . From $w\ll\bigvee\Delta$ it follows that, for some $d\in D$ , $w\leq d$ holds, whence $p(d,x)\leq p(w,x)<p(x,x)+\delta^{\prime}$ . We have thus proved that for all $\delta^{\prime}>\delta$ there exists $d\in\Delta$ such that $p(d,x)<p(x,x)+\delta^{\prime}$ , which implies then $\inf_{d\in\Delta}p(d,x)\leq p(x,x)+\delta=p(x,\bigvee\Delta).$

$\hfill\blacktriangleleft$

To check the converse condition $\mathcal{O}_{\sigma}(X)\subseteq\mathcal{O}_{p}(X)$ , one must show that, given $x\ll y$ , one can form open balls around $y$ whose elements all lie way above $x$ . This corresponds to showing that the basic open sets $\mathrel{\rotatebox{90.0}{$\twoheadrightarrow$}}x=\{y\mid x\ll y\}$ for the Scott topology are metric open.

Example 24.

We construct a PM on $\Sigma\mathrm{Tree}_{\leq\infty}$ that captures the tree order but fails to quantify its Scott topology. Define a variant $q$ of the tree partial metric as $q(\alpha,\beta)=\frac{1}{2}p_{\mathrm{tree}}(\alpha,\beta)+\frac{1}{4}$ if $\alpha\neq\beta$ or $\alpha=\beta$ is finite, and as $p_{\mathrm{tree}}(\alpha,\beta)$ if $\alpha=\beta$ is infinite. $q$ is still a partial metric and furthermore the order $\leq_{q}$ coincides with the tree order (and thus with $\leq_{p}$ as well); now, letting $\alpha_{n}$ be a directed sequence of finite trees converging to an infinite tree $\alpha$ , we have $\lim_{n}q(\alpha_{n},\alpha)=\frac{1}{4}>0=q(\bigvee_{n}\alpha_{n},\alpha)$ . Hence $q$ is not Scott-continuous, and by Proposition 23 we have that $\mathcal{O}_{q}(\Sigma\mathrm{Tree}_{\leq\infty})\not\subseteq\mathcal{O}_{% \sigma}(\Sigma\mathrm{Tree}_{\leq\infty})$ .

$\blacktriangleright$ Remark 25 (computability of $p(x,y)<\epsilon$ ).

An immediate and useful consequence of the fact that open balls are Scott open is that $p(x,y)<\epsilon$ holds precisely when $p(x^{\prime},y^{\prime})<\epsilon$ holds for some approximants $x^{\prime}\ll x$ and $y^{\prime}\ll y$ . In other words, to verify that $y$ is close enough to $x$ it is enough to check that the approximants of $y$ get close enough to the approximants of $x$ . When distances between approximants, as well as the relation $b\ll x$ between a point and an approximant, are computable, the property $p(x,y)<\epsilon$ may be (semi-)decidable, even though the exact values $p(x,y)$ are as hard as computing the $\lambda$ -theory (usually, $\Pi^{0}_{2}$ or worse). For instance, in the case of Böhm trees, to check that $p_{\mathrm{B\"{o}hm}}(M,N)<2^{-n}$ , it is enough to check that $\mathcal{B}(M)$ and $\mathcal{B}(N)$ coincide up to height $n$ , a property which can be semi-decided.

Example 26 ( $\epsilon/\delta$ -continuity of contexts).

As $p_{\mathrm{tree}}$ quantifies the Scott topology of trees (cf. Proposition 21), it quantifies the Scott topology of Böhm trees. From the continuity theorem for Böhm trees (cf. [5]) we deduce then the following: for all context $\mathtt{C}[-]$ and $\lambda$ -term $M$ and for all $\epsilon>0$ , there exists $\delta>0$ such that, for all terms $P$ , $p_{\mathrm{B\"{o}hm}}(P,M)\leq\delta$ implies $p_{\mathrm{B\"{o}hm}}(\mathtt{C}[P],\mathtt{C}[M])\leq\epsilon$ . Another way of stating this is that for all $\mathtt{C}[-]$ and $M$ , for all $n\in\mathbb{N}$ there exists $m\in\mathbb{N}$ such that, if $\mathcal{B}(P)$ and $\mathcal{B}(M)$ are the same up to depth $m$ , then $\mathcal{B}(\mathtt{C}[P])$ and $\mathcal{B}(\mathtt{C}[M])$ are the same up to depth $n$ .

Let us conclude this paragraph by recalling a very general result on the quantifiability of domains, already mentioned in the Introduction:

Theorem 27 (cf. [40]).

Let $(X,\leq)$ be a domain with a countable basis $(b_{n})_{n\in\mathbb{N}}$ , and let $\theta_{n}\in(0,1]$ be a sequence of weights such that $\sum_{n}^{\infty}\theta_{n}\leq 1$ . Then $X$ is quantified by the partial metric $p^{X}_{b_{n},\theta_{n}}(x,y)=\sum_{n\in N}\theta_{n}$ , where $N:=\left\{n\ |\ b_{n}\not\ll x\ \text{or}\ b_{n}\not\ll y\right\}$ .

While Theorem 27 provides a general positive answer to the quantifiability problem for domains, the practical usability of metrics like $p^{X}_{b_{n},\theta_{n}}$ depends on whether the relation $b_{n}\ll x$ between a point and an approximant, and its negation, are computable.

Applicative distances and the function space.

The categories of Scott domains (resp. bounded complete domains) and continuous functions are sub-categories of $\mathrm{Top}$ that are, as is well-known, cartesian closed. Using Theorem 27 it is possible to define, on each object of such categories, a partial metric that quantifies its topology. However, in common approaches to higher-order languages (e.g. [17, 25, 16]), one requires distances to be defined in a compositional way.

For example, given metric spaces $(X,d_{X})$ and $(Y,d_{Y})$ , a standard way to define a metric on their cartesian product is by letting $d_{X\times Y}(\langle x,y\rangle,\langle x^{\prime},y^{\prime}\rangle)=d_{X}(x% ,x^{\prime})+d_{Y}(y,y^{\prime})$ . Indeed, a similar construction also works for PMs:

Proposition 28.

Let $X, Y$ be two Scott domains, quantified, respectively, by the partial metrics $p_{X},p_{Y}$ . Their cartesian product $X\times Y$ is then quantified by the partial metric $p_{X\times Y}:=\frac{1}{2}(p_{X}+p_{Y})$ .

We omit the proof of Proposition 28 as it is similar to that of Proposition 30 below (still, the proof can be found in the extended version).

$\blacktriangleright$ Remark 29.

In the following discussion we restrict attention to partial metrics valued in $[0,1]$ , rather than on $[0,+\infty]$ . This is not a limitation, since for any partial metric $p$ with values in $[0,+\infty]$ , the partial metric $p^{\leq 1}:X\times X\to[0,1]$ defined by $p^{\leq 1}(x,y):=\frac{p(x,y)}{1+p(x,y)}$ induces the same topology (cf. [34]).

Let us now consider the function space. Given metric spaces $(X,d)$ and $(X^{\prime},d^{\prime})$ , a standard compositional way to define a metric on the space $\mathcal{C}(X,X^{\prime})$ of continuous functions from $X$ to $X^{\prime}$ is via the $\sup$ -condition $d_{\sup}(f,g)=\sup_{x\in X}d^{\prime}(f(x),f(x^{\prime}))$ . Notably, when $X$ is compact, $d_{\sup}$ metrizes the compact-open topology on $\mathcal{C}(X,X^{\prime})$ . Other compositional metrics on the space of non-expansive functions $\mathrm{NExp}(X,X^{\prime})$ , depending on both $d$ and $d^{\prime}$ , can be found in the literature [10, 15]. Similar compositional definitions are also found in more operational approaches like e.g. [37, 25].

A common intuition in all these definitions is that two functions are close when their application to close (or even identical) points produces points that are still close. We will call functional distances respecting this idea applicative distances.

However, to define an applicative PM on the space of continuous functions, we cannot directly adapt a definition like $d_{\sup}$ : unlike for standard (pseudo-)metrics, the $\sup$ s of a family of PPMs does not define a PPMs. This is due to condition P4, which relies in a contravariant way on the medium self-distance $p(z,z)$ .

Instead, we will rely on the remark that a continuous function $f:X\to Y$ is uniquely determined by its action on the (countably many) elements of a basis of $X$ . This suggests indeed the definition from the Proposition below:

Proposition 30.

Let $X, Y$ be two bounded complete domains, quantified, respectively, by the PMs $p_{X},p_{Y}$ , and let $(a_{n})_{n\in\mathbb{N}}$ be an enumeration of a basis of $X$ . Then, for all $0<\theta\leq\frac{1}{2}$ , their exponential $X\Rightarrow Y$ is quantified by the PM

p^{\theta}_{X\Rightarrow Y}(f,g)=\sum_{n=1}^{\infty}\theta^{n}p_{Y}(f(a_{n}),g% (a_{n})).

(1)

Before proving the result above, let us first discuss the PM $p^{\theta}_{X\Rightarrow Y}$ . The distances $p^{\theta}_{X\Rightarrow Y}(f,g)$ are defined by infinite series, which are convergent by our assumption that $p_{X},p_{Y}$ are bounded by 1. However, for any $\epsilon>0$ , the verification that $p^{\theta}_{X\Rightarrow Y}(f,g)<\epsilon$ can be reduced to a finitary test:

Lemma 31.

For all continuous functions $f,g:X\to Y$ , for all $n>0$ , there exists $N\in\mathcal{O}(n)$ such that, if $p_{Y}(f(a_{i}),g(a_{i}))<2^{-(n+1)}$ holds for all $i=1,\dots,N$ , then $p^{\theta}_{X\Rightarrow Y}(f,g)<2^{-n}$ .

Proof.

Let $\epsilon=2^{-n}$ . We must choose $N$ so that $\sum_{i>N}^{\infty}\theta^{i}<\frac{\epsilon}{2}$ . Since $\sum_{n=1}^{\infty}\theta^{n}\leq 1$ , this corresponds to requiring $\sum_{n=1}^{N}\theta^{n}>1-\frac{\epsilon}{2}$ , or, equivalently, $\frac{1-\theta^{N+1}}{1-\theta}-1>1-\frac{\epsilon}{2}.$ A few computations yield then the condition $N+1>\log\left(3\theta+\theta^{2}\epsilon+\epsilon\right)\in\mathcal{O}(\log\epsilon)$ .

Let us show that under this condition the claim holds. Suppose $p^{\theta}(f(a_{i}),g(a_{i}))\leq\frac{\epsilon}{2}$ holds for $i=1,\dots,N$ . Then we have

\displaystyle p^{\theta}(f,g)

\displaystyle=\left(\sum_{k=1}^{N}\theta^{n}q(f(a_{k}),g(a_{k}))\right)+\left(% \sum_{k>N}^{\infty}\theta^{n}q(f(a_{k}),g(a_{k}))\right)\leq\left(\sum_{k=1}^{% N}\theta^{n}\frac{\epsilon}{2}\right)+\frac{\epsilon}{2}\leq\epsilon

$\hfill\blacktriangleleft$

The intuition behind the test above is that for $N$ high enough, the infinite sum $\sum_{n\geq N}^{\infty}\theta^{n}$ gets too small to actually matter in checking that $p^{\theta}_{X\Rightarrow Y}(f,g)$ is smaller than $\epsilon$ , and one is thus reduced to the finite sum $\sum_{n=1}^{N}\theta^{n}p_{Y}(f(a_{n}),g(a_{n}))$ . This is indeed a key ingredient in showing that open balls of functions are finitely accessible, and in particular, that if $g\in B_{\epsilon}(f)$ , this only depends on finitely many values of $g$ .

Conversely, from $p^{\theta}_{X\Rightarrow Y}(f,g)<\epsilon$ , one can deduce bounds $p_{Y}(f(a_{n}),g(a_{n}))<\theta^{-n}\epsilon$ for all $n\in\mathbb{N}$ , although such bounds become more and more loose as $n$ increases, due to the exponential scaling factor $\theta^{-n}$ .

Let us now turn to the proof of Proposition 30. First, let us recall that, given bounded complete domains $X, Y$ , with countable bases $B(X),B(Y)$ , the domain $\mathcal{C}(X,Y)$ admits a countable basis formed by all functions of the form $(\mathrel{\rotatebox{90.0}{$\twoheadrightarrow$}}a\searrow b)$ , where $a\in B(X),b\in B(Y)$ , and $(\mathrel{\rotatebox{90.0}{$\twoheadrightarrow$}}a\searrow b)(x)=b$ in case $a\ll x$ , while $(\mathrel{\rotatebox{90.0}{$\twoheadrightarrow$}}a\searrow b)(x)=\bot$ otherwise.

Importantly, while it is always the case that $f\ll g$ implies $f(x)\ll g(x)$ for all $x\in X$ , the converse need not hold. Rather, the way below relation can be characterized as follows.

Lemma 32 (cf. [21]).

For all $f,g\in\mathcal{C}(X,Y)$ , $f\ll g$ iff there exists basis elements $a_{1},\dots,a_{n}\in B(X)$ and $b_{1},\dots,b_{n}\in B(Y)$ such that

$\blacksquare$

$b_{i}\ll g(a_{i})$ ,
$\blacksquare$

$\mathrel{\rotatebox{90.0}{$\twoheadrightarrow$}}a_{i}\ll g^{-1}(\mathrel{% \rotatebox{90.0}{$\twoheadrightarrow$}}b_{i})$ ¹¹1 Recall that $\mathcal{O}(X)$ is a continuous domain. For two open sets $U,V\in\mathcal{O}(X)$ , $U\ll V$ holds when any open cover of $V$ has a finite subset which covers $U$ . , for all $i=1,\dots,n$ ,
$\blacksquare$

$f\leq\bigvee_{i=1}^{n}(\mathrel{\rotatebox{90.0}{$\twoheadrightarrow$}}a_{i}% \searrow b_{i})$ .

We now have all ingredients to prove Proposition 30.

Proof of Proposition 30.

$\mathcal{O}_{\sigma}(X\Rightarrow Y)\supseteq\mathcal{O}_{p_{X\Rightarrow Y}}(% X\Rightarrow Y)$ :

We have to show that open balls are Scott-open. First observe that open balls are upper sets. We thus only need to show that they are finitely accessible: for all $g\in B_{\epsilon}(f)$ we must find some $h\ll g$ such that $h\in B_{\epsilon}(f)$ . Let then $g\in B_{\epsilon}(f)$ , so that $p^{\lambda}_{X\Rightarrow Y}(f,g)<p^{\lambda}_{X\Rightarrow Y}(f,f)+\epsilon$ . Observe that this implies that we can find positive reals $\theta,\delta>0$ such that $\theta+\delta\leq\epsilon$ and $p^{\lambda}_{X\Rightarrow Y}(f,g)<p^{\lambda}_{X\Rightarrow Y}(f,f)+\delta$ . Let $N$ be such that $\sum_{n>N}^{\infty}\lambda^{n}\leq\frac{\theta}{2}$ . For all $n\leq N$ , fix some $b_{n}\in B_{\frac{\theta}{2}}(g(a_{n}))$ such that $b_{n}\ll g(a_{n})$ , and some basis element $c_{n}\ll a_{n}$ .

Let now $h=\bigvee_{i=1}^{N}(\mathrel{\rotatebox{90.0}{$\twoheadrightarrow$}}c_{i}% \searrow b_{i})$ . From $b_{i}\ll g(a_{i})$ it follows that $a_{i}\in g^{-1}(\mathrel{\rotatebox{90.0}{$\twoheadrightarrow$}}b_{i})$ , and thus that $\mathrel{\rotatebox{90.0}{$\twoheadrightarrow$}}c_{i}\ll g^{-1}(\mathrel{% \rotatebox{90.0}{$\twoheadrightarrow$}}b_{i})$ . By Lemma 32 this implies that $h\ll g$ . Let us show that $h\in B_{\epsilon}(f)$ . For all $n<N$ , we have $p_{Y}(h(a_{n}),g(a_{n}))\leq p_{Y}(b_{n},g(a_{n}))<p_{Y}(g(a_{n}),g(a_{n}))+% \frac{\theta}{2}$ , whence, for all $n\leq N$ , $p_{Y}(h(a_{n}),g(a_{n}))-p_{Y}(g(a_{n}),g(a_{n}))<\frac{\theta}{2}$ . Let’s check that $h\in B_{\epsilon}(f)$ :

	$\displaystyle p^{\lambda}_{X\Rightarrow Y}(h,f)$	$\displaystyle=\sum_{n=1}^{\infty}\lambda^{n}p_{Y}(h(a_{n}),f(a_{n}))$
		$\displaystyle\leq\sum_{n=1}^{\infty}\lambda^{n}\Big{(}p_{Y}(h(a_{n}),g(a_{n}))% +p_{Y}(g(a_{n}),f(a_{n}))-p_{Y}(g(a_{n}),g(a_{n}))\Big{)}$
		$\displaystyle\leq\sum_{n=1}^{N}\lambda^{n}\Big{(}p_{Y}(h(a_{n}),g(a_{n}))-p_{Y% }(g(a_{n}),g(a_{n}))\Big{)}$
		$\displaystyle\qquad\qquad +\sum_{n>N}^{\infty}\lambda^{n}p_{Y}(h(a_{n}),g(a_{n% }))+p^{\lambda}_{X\Rightarrow Y}(g,f)$
		$\displaystyle<\sum_{n=1}^{N}\lambda^{n}\frac{\theta}{2}+\sum_{n>N}^{\infty}% \lambda^{n}+p^{\lambda}_{X\Rightarrow Y}(f,f)+\delta$
		$\displaystyle\leq\frac{\theta}{2}+\frac{\theta}{2}+p^{\lambda}_{X\Rightarrow Y% }(f,f)+\delta\leq p^{\lambda}_{X\Rightarrow Y}(f,f)+\epsilon.$

$\mathcal{O}_{\sigma}(X\Rightarrow Y)\subseteq\mathcal{O}_{p_{X\Rightarrow Y}}(% X\Rightarrow Y)$ :

It suffices to show that the basic Scott open sets $\mathrel{\rotatebox{90.0}{$\twoheadrightarrow$}}f$ contain an open p-ball $B_{\epsilon}(g)$ around any of its points $g\in\ \mathrel{\rotatebox{90.0}{$\twoheadrightarrow$}}f$ . So, suppose $f\ll g$ : by Lemma 32 there exists $c_{1},\dots,c_{n}\in X$ , $b_{1},\dots,b_{n}\in Y$ such that $b_{i}\ll g(c_{i})$ , $\mathrel{\rotatebox{90.0}{$\twoheadrightarrow$}}c_{i}\ll g^{-1}(\mathrel{% \rotatebox{90.0}{$\twoheadrightarrow$}}b_{i})$ and $f\leq\bigvee_{i}(\mathrel{\rotatebox{90.0}{$\twoheadrightarrow$}}c_{i}\searrow b% _{i})$ . From $b_{i}\ll g(c_{i})$ it follows that there exists $\epsilon_{i}>0$ such that $B_{\epsilon_{i}}(g(c_{i}))\subseteq\ \mathrel{\rotatebox{90.0}{$% \twoheadrightarrow$}}b_{i}$ . Let $N$ be such that for all $i=1,\dots,n$ , $c_{i}$ has an index $\leq N$ in the enumeration $a_{n}$ of $\mathcal{B}(X)$ . Let $\epsilon=\lambda^{N}\min\{\epsilon_{1},\dots,\epsilon_{n}\}$ .

We claim that $B_{\epsilon}(g)\subseteq\ \mathrel{\rotatebox{90.0}{$\twoheadrightarrow$}}f$ : let $h\in B_{\epsilon}(g)$ , then, from $\sum_{n}\lambda^{n}\big{(}p_{Y}(h(a_{n}),g(a_{n}))-p_{Y}(g(a_{n}),g(a_{n}))% \big{)}<\epsilon$ , we deduce, for $i=1,\dots,n$ , $p_{Y}(h(c_{i}),g(c_{i}))<p_{Y}(g(c_{i}),g(c_{i}))+\lambda^{-i}\epsilon\leq p_{% Y}(g(c_{i}),g(c_{i}))+\epsilon_{i}$ , that is, $h(c_{i})\in B_{\epsilon_{i}}(g(c_{i}))$ . We deduce that $b_{i}\ll h(c_{i})$ , and thus that $f\leq\bigvee_{i}(\mathrel{\rotatebox{90.0}{$\twoheadrightarrow$}}c_{i}\searrow b% _{i})\ll h$ . We can thus conclude that $f\ll h$ .

$\hfill\blacktriangleleft$

We conclude this section with a few examples.

Example 33 (RealPCF).

The language RealPCF [22] is an extension of PCF with a type $\mathbf{I}$ for partial real numbers (i.e. finite approximations of real numbers or, equivalently, computable closed intervals) and primitives for computable analysis, with a canonical Scott semantics in which $\mathbf{I}$ is interpreted via the domain $\mathbf{I}(\mathbb{R})$ . This is perfectly in line with the quantification of $\mathbf{I}(\mathbb{R})$ we presented in Example 5, which sees smaller and smaller intervals as providing more and more information. Via the applicative distances just presented, we obtain then a quantification of the Scott semantics of full RealPCF.

Example 34 (Scott topologies of open and closed sets).

Given a topological space $X$ , one can endow the space $\mathcal{O}(X)$ of its open sets with the Scott topology induced by the inclusion order, as well as the (homeomorphic) space $\mathcal{C}(X)$ of its closed sets under the Scott topology induced by the reversed inclusion order.

Whenever $X$ is exponentiable in $\mathrm{Top}$ (which is the case, in particular, whenever $X$ is a Scott domain), the bijection $h:\mathcal{O}(X)\simeq\mathrm{Top}(X,S)$ , where $S$ is the Sierpinski space and $h(U)$ is the characteristic function of $U$ , is a homeomorphism [24]. Given a countable basis $(x_{n})_{n}$ of $X$ , and weights $\theta_{n}$ with $\sum_{n}\theta_{n}\leq 1$ , we can then quantify $\mathcal{O}(X)$ and $\mathcal{C}(X)$ via

	$\displaystyle p^{\mathcal{O}}_{x_{n},\theta_{n}}(U,V)$	$\displaystyle=\sum_{n=1}^{\infty}\theta_{n}\cdot s(h(U)(x_{n}),h(V)(x_{n}))=% \sum\left\{\theta_{n}\ \|\ x_{n}\notin U\lor x_{n}\notin V\right\},$
	$\displaystyle p^{\mathcal{C}}_{x_{n},\theta_{n}}(C,D)$	$\displaystyle=p^{\mathcal{O}}(\overline{C},\overline{D})=\sum\left\{\theta_{n}% \ \|\ x_{n}\in C\lor x_{n}\in D\right\}.$

Example 35 (Böhm trees as closed sets).

Consider the poset $\mathcal{A}$ of partial terms. Let $\mathrm{Ide}(\mathcal{A})$ be the dcpo of ideals of $\mathcal{A}$ , that is, of lower directed subsets of $\mathcal{A}$ . Observe that any Böhm tree $\mathcal{B}(M)\subseteq\mathcal{A}$ is an element of $\mathrm{Ide}(\mathcal{A})$ , and the set $\downarrow\mathcal{B}(M)=\{U\mid U\subseteq\mathcal{B}(M)\}\subseteq\mathrm{% Ide}(\mathcal{A})$ is a closed set under the Scott topology of $\mathrm{Ide}(\mathcal{A})$ . Given an enumeration $A_{n}$ of partial terms and weights $\theta_{n}$ , we can then define an alternative $\lambda$ -PPM by letting $p^{\mathcal{B}}_{A_{n},\theta_{n}}(M,N)=p^{\mathcal{C}}_{\downarrow A_{n},% \theta_{n}}(\downarrow\mathcal{B}(M),\downarrow\mathcal{B}(N))=\sum_{n}\{% \theta_{n}\ |\ A_{n}\not\leq M\ \text{or}\ A_{n}\not\leq N\}$ . While they produce different distances, $p^{\mathcal{B}}_{A_{n},\theta_{n}}$ and $p_{\mathrm{B\"{o}hm}}$ quantify the same topology, i.e. $p_{\mathrm{B\"{o}hm}}\sqsupseteq\sqsubseteq p^{\mathcal{B}}$ .

Example 36 (Scott topology of the power set).

A countable set $X$ is (trivially) a domain for the order given by equality, and its Scott topology coincides with the indiscrete topology, i.e. $\mathcal{O}(X)=\mathcal{P}(X)$ . Given an enumeration $x_{n}$ of $X$ , the Scott topology on $\mathcal{P}(X)$ is thus quantified by $p^{\mathcal{P}}_{x_{n},\theta_{n}}(A,B)=\sum\left\{\theta_{n}\ |\ x_{n}\notin A% \lor x_{n}\notin B\right\},$ for $A,B\subseteq X$ .

5 Quantifying a Reflexive Object

The denotational models for the untyped $\lambda$ -calculus correspond to the reflexive objects within some cartesian closed category, that is, the objects $X$ satisfying the isomorphism $X\simeq X\to X$ . Within cpo-enriched categories, reflexive objects can be obtained by a direct limit construction, whose paradigmatic example is Scott’s $D_{\infty}$ model. In this section we show how to quantify this model via applicative distances, at the same time illustrating a technique that could be adapted to other similar constructions, like e.g. the reflexive object within the relational model [6].

Quantifying Scott’s $D_{\infty}$ .

Let us recall the idea of the direct limit construction of a reflexive object. One starts from some bounded complete domain $D$ , and constructs a sequence of spaces $D_{0}:=D$ , $D_{n+1}:D_{n}\to D_{n}$ , together with maps $i_{n}:D_{n}\to D_{n+1}$ and $j_{n}:D_{n+1}\to D_{n}$ forming a pair $(i_{n},j_{n})$ called an injection/retraction pair, that is, satisfying $j_{n}\circ i_{n}=\mathrm{id}_{D_{n+1}}$ and $i_{n}\circ j_{n}\leq\mathrm{id}_{D_{n}}$ . One obtains then a reflexive object $D_{\infty}\simeq D_{\infty}\to D_{\infty}$ as the direct limit of the sequence $D_{n}\stackrel{{\scriptstyle i_{n}}}{{\to}}D_{n+1}$ , as well as injection-retraction pairs $i_{n\infty}:D_{n}\to D_{\infty}$ , $j_{\infty n}:D_{\infty}\to D_{n}$ .

Notice that an element $x$ of $D_{\infty}$ yields, for any $n$ , a function $x_{n}:=j_{\infty n}(x)\in D_{n}=D_{n-1}\to D_{n-2}\to\dots\to D_{0}$ ; conversely, any compact element $x\in D_{n}$ yields a compact element $i_{n\infty}(x)\in D_{\infty}$ , and such elements form indeed a basis of $D_{\infty}$ .

Suppose now that the starting space $D$ is quantified by some PM $p$ . Using the applicative metrics from the previous section we can quantify all the $D_{n}$ by letting $p_{0}:=p$ and $p_{n+1}(x,y)=\sum_{i=1}^{\infty}\frac{1}{2^{i}}p_{n}(x(a^{n}_{i}),y(a^{n}_{i}))$ , where $(a^{n}_{i})_{i}$ is an enumeration of the basis elements of $D_{n}$ . We obtain then a PM quantifying $D_{\infty}$ by letting

\begin{split}p_{\infty}(x,y)&=\sum_{n=1}^{\infty}\frac{1}{2^{n}}p_{n}(x_{n},y_% {n})\\ &=\sum_{n,k_{n-1},\dots,k_{0}=1}^{\infty}\left(\frac{1}{2^{n+k_{n-1}+\dots+k_{% 0}}}\right)\cdot p\left(x_{n}(a^{n-1}_{k_{n-1}})\dots(a^{0}_{k_{0}}),y_{n}(a^{% n-1}_{k_{n-1}})\dots(a^{0}_{k_{0}})\right).\end{split}

Intuitively, the distance $p_{\infty}$ compares $x$ and $y$ by considering all possible ways of evaluating the functions $x_{n},y_{n}\in D_{n}$ on $n$ basis elements of the corresponding spaces $D_{n-1},\dots,D_{0}$ . As for the applicative metrics from the previous section, while the distances $p_{\infty}(x,y)$ are defined via infinite series, one can check that $x\in B_{\epsilon}^{p_{\infty}}(y)$ by a finitary criterion.

Lemma 37.

For all $x\in D_{\infty}$ and $n>0$ , there exists $N\in\mathcal{O}(n)$ such that for all $y\in D_{\infty}$ , if, for all $i,k_{0},\dots,k_{i-1}\leq N$ , $p(x_{i}a_{i-1}^{k_{i-1}}\dots a_{0}^{k_{0}},y_{i}a_{i-1}^{k_{i-1}}\dots a_{0}^% {k_{0}})<2^{-(n+1)}$ , then $p_{\infty}(x,y)<2^{-n}$ .

Proof.

We must find $N$ satisfying $\sum_{n,k_{n-1},\dots,k_{0}>N}^{\infty}\frac{1}{2^{n+k_{n-1}+\dots+k_{0}}}<% \frac{\epsilon}{2}$ . Notice that if $N$ satisfies $\sum_{n>N}^{\infty}\frac{1}{2^{n}}<\frac{\epsilon}{2}$ , then it also satisfies the other condition, so we can argue as for Lemma 31. $\hfill\blacktriangleleft$

The following result is proved in detail in the long version.

Theorem 38.

The partial metric $p_{\infty}$ quantifies the Scott topology of $D_{\infty}$ .

Proof.

We will exploit a few properties of the maps $i_{nm}$ , proved in the extended version:

i.

For all $n\in\mathbb{N}$ , $x\in X_{n}$ and $y\in X_{\infty}$ , $x\ll y_{n}$ $\Rightarrow$ $i_{n\infty}(x)\ll y$ .
ii.

For all $x,y\in X_{\infty}$ , $x\ll y$ iff there exists $N\in\mathbb{N}$ and $w_{1},\dots,w_{k}\in X_{N}$ such that $w_{1},\dots,w_{k}\ll y_{N}$ and $x\leq i_{N\infty}(w_{1}\vee\dots\vee w_{k})$ .
iii.

For all $n\in\mathbb{N}$ , $x\in X_{n}$ and $y\in X_{\infty}$ , $i_{n\infty}(x)\ll y$ $\Rightarrow$ $\exists N\forall k\geq N,i_{n(n+k)}(x)\ll y_{n+k}$ .

$\mathcal{O}_{\sigma}(D_{\infty})\supseteq\mathcal{O}_{p_{\infty}}(D_{\infty})$ :

Let $y\in B_{\epsilon}(x)$ . We need to find $y^{\prime}\in D_{\infty}$ such that $y^{\prime}\in B_{\epsilon}(x)$ and $y^{\prime}\ll y$ . From $p_{\infty}(y,x)<p_{\infty}(x,x)+\epsilon$ it follows that we can find $\theta,\delta>0$ such that $p_{\infty}(y,x)<p_{\infty}(x,x)+\delta$ and $\delta+\theta\leq\epsilon$ . Let $N$ be such that $\sum_{n>N}^{\infty}\frac{1}{2^{n}}<\frac{\theta}{2}$ . Since the $p_{n}$ -balls are Scott open, for all $n\leq N$ , we can find some $z_{n}\in B_{\frac{\theta}{2}}(y_{n})$ such that $z_{n}\ll y_{n}$ . Observe that by (i.) we have $i_{n\infty}(z_{n})\ll y$ . This implies in particular that the join $\bigvee_{n=1}^{N}i_{n\infty}(z_{n})$ exists in $D_{\infty}$ . Define $y^{\prime}:=\bigvee_{n=1}^{N}i_{n\infty}(z_{n})$ . Notice that $y^{\prime}\ll y$ holds so we just have to check that $y^{\prime}\in B_{\epsilon}(x)$ .

First recall that, by antimonotonicity of $p_{n}$ , $p_{n}(a\vee a^{\prime},b)\leq\min\{p_{n}(a,b),p_{n}(a^{\prime},b)\}$ . Now, for all $n\leq N$ , we have that $y^{\prime}_{n}=j_{\infty n}(y^{\prime})=\left(\bigvee_{k<N}i_{k,n}(z_{k})% \right)\vee z_{n}\vee\left(\bigvee_{n<k\leq N}j_{k,n}(z_{k})\right)$ . Then we deduce $p_{n}(y^{\prime}_{n},y_{n})\leq p_{n}(z_{n},y_{n})<p_{n}(y_{n},y_{n})+\frac{% \theta}{2}$ . We can now compute

	$\displaystyle p_{\infty}(y^{\prime},x)$	$\displaystyle=\sum_{n=1}^{\infty}\frac{1}{2^{n}}p_{n}(y^{\prime}_{n},x_{n})$
		$\displaystyle\leq\sum_{n=1}^{\infty}\frac{1}{2^{n}}\Big{(}p_{n}(y^{\prime}_{n}% ,y_{n})+p_{n}(y_{n},x_{n})-p(y_{n},y_{n})\Big{)}$
		$\displaystyle\leq\left(\sum_{n=1}^{\infty}\frac{1}{2^{n}}p_{n}(y^{\prime}_{n},% y_{n})-p_{n}(y_{n},y_{n})\right)+p_{\infty}(y,x)$
		$\displaystyle=\left(\sum_{n=1}^{N}\frac{1}{2^{n}}(p_{n}(y^{\prime}_{n},y_{n})-% p_{n}(y_{n},y_{n}))\right)$
		$\displaystyle\qquad\qquad+\left(\sum_{n>N}^{\infty}\frac{1}{2^{n}}(p_{n}(y^{% \prime}_{n},y_{n})-p_{n}(y_{n},y_{n}))\right)+p_{\infty}(y,x)$
		$\displaystyle<\left(\sum_{n=1}^{N}\frac{1}{2^{n}}\frac{\theta}{2}\right)+\frac% {\theta}{2}+p_{\infty}(x,x)+\delta\leq p_{\infty}(x,x)+\theta+\delta\leq p_{% \infty}(x,x)+\epsilon.$

$\mathcal{O}_{\sigma}(X_{\infty})\subseteq\mathcal{O}_{p_{\infty}}(X_{\infty})$ :

Suppose $x\ll y$ . We need to find $\epsilon>0$ such that $B_{\epsilon}(y)\subseteq\ \mathrel{\rotatebox{90.0}{$\twoheadrightarrow$}}x$ . By (ii.) there exists $N$ and $w_{1},\dots,w_{k}\in X_{N}$ such that $x\leq i_{N\infty}(w_{1}\vee\dots\vee w_{k})\ll y$ . By (iii.) there exists $N^{\prime}\geq N$ such that $i_{NN^{\prime}}(w_{j})\ll y_{N^{\prime}}$ . Observe that $i_{N^{\prime}\infty}(i_{NN^{\prime}}(u))=i_{N\infty}(u)$ , which implies that $x\leq\bigvee_{j}i_{N^{\prime}\infty}(i_{NN^{\prime}}(w_{j}))$ .

For each $j=1,\dots,k$ we can find then $\epsilon_{j}>0$ such that $B_{\epsilon_{j}}(y_{N^{\prime}})\subseteq\ \mathrel{\rotatebox{90.0}{$% \twoheadrightarrow$}}i_{NN^{\prime}}(w_{j})$ . Let $\epsilon:=2^{-(N^{\prime}+1)}\min\{\epsilon_{j}\mid j=1,\dots,k\}$ . Suppose $z\in B_{\epsilon}(y)$ : for all $j=1,\dots,k$ , from $p_{\infty}(z,y)\leq\epsilon$ we deduce $p_{N^{\prime}}(z_{N^{\prime}},y_{N^{\prime}})\leq 2^{N^{\prime}}\epsilon<% \epsilon_{j}$ , whence $z_{N^{\prime}}\in B_{\epsilon_{j}}(y_{N^{\prime}})$ , which forces $i_{NN^{\prime}}(w_{j})\ll z_{N^{\prime}}$ . By (i.) the last inequality implies $i_{N^{\prime}\infty}(w_{j})=i_{N^{\prime}\infty}(i_{NN^{\prime}}(w_{j}))\ll z$ , and we thus obtain $x\leq\bigvee_{j}i_{N^{\prime}\infty}(i_{NN^{\prime})}(w_{j}))\ll z$ , that is, $x\ll z$ .

$\hfill\blacktriangleleft$

The Scott $\lambda$ -PPM.

The interpretation of closed $\lambda$ -terms in the Scott model $D_{\infty}$ , for $D$ an arbitrary algebraic domain quantified by a PM $p$ , yields a PPM $p_{\mathrm{Scott}}(M,N):=p_{\infty}(\llbracket M\rrbracket,\llbracket N\rrbracket)$ , where $\llbracket M\rrbracket\in D_{\infty}$ indicates the interpretation of $M$ inside $D_{\infty}$ . When $D$ is non-trivial (i.e. $D\neq\{\bot\}$ ), using well-known properties of the Scott model, $p_{\mathrm{Scott}}(M,N)$ yields an extensional and sensible $\lambda$ -PPM.

The result below relates $p_{\mathrm{Scott}}$ to the other $\lambda$ -PPMs discussed in Section 3.

Proposition 39.

$p_{\mathrm{B\"{o}hm}}\sqsubset p_{\mathrm{Scott}}\sqsubset p_{\mathrm{ctx}}$ .

Proof sketch.

( $p_{\mathrm{B\"{o}hm}}\sqsubset p_{\mathrm{Scott}}$ ): We exploit the approximation theorem for $D_{\infty}$ [5] which says that, for any closed $\lambda$ -term $M$ , letting $\Lambda_{\bot}^{o}$ be the set of closed partial terms and $\llbracket-\rrbracket:\Lambda^{o}_{\bot}\to D_{\infty}$ the interpretation function, $\llbracket M\rrbracket=\bigvee\{\llbracket A\rrbracket\mid A\leq M\}$ . Since $D$ is algebraic, any open ball $B_{\epsilon}^{p_{0}}(\llbracket M\rrbracket(\vec{a}))$ contains some compact element $c\ll\llbracket M\rrbracket(\vec{a})$ . By the approximation theorem, then, we deduce that there exists a partial term $A\leq M$ such that $c\ll\llbracket A\rrbracket(\vec{a})$ .

Consider the open ball $B_{\epsilon}^{p_{\mathrm{Scott}}}(M)$ . Thanks to Lemma 37 one can find a finite number of sequences of basis elements $\vec{a}_{1},\dots,\vec{a}_{n}$ and positive reals $\delta_{1},\dots,\delta_{n}>0$ such that for all term $P$ , if $\llbracket P\rrbracket(\vec{a}_{i})\in B_{\delta_{i}}^{p_{0}}(\llbracket M% \rrbracket(\vec{a}_{i})$ holds for all $i=1,\dots,n$ , then $P\in B_{\epsilon}^{p_{\mathrm{Scott}}}(M)$ .

By reasoning as above via the approximation theorem, we obtain partial terms $A_{1},\dots,A_{n}\leq M$ such that $A_{i}\in B_{\delta_{i}}^{p_{0}}(\llbracket M\rrbracket(\vec{a}_{i})$ , and we deduce then $A=\bigvee_{i}A_{i}\in B_{\epsilon}^{p_{\mathrm{Scott}}}(M)$ . Letting now $k$ be the height $A$ and $\theta=2^{-k}$ , we thus conclude that $B_{\theta}^{\mathrm{B\"{o}hm}}(M)\subseteq B_{\epsilon}^{p_{\mathrm{Scott}}}(M)$ .

The strictness follows from the fact that the associated $\lambda$ -theories $\mathcal{B}$ and $\mathcal{H}^{*}$ are strictly included, as argued at the end of Remark 19 for the case of $p_{\mathrm{ctx}}$ .
( $p_{\mathrm{Scott}}\sqsubset p_{\mathrm{ctx}}$ ): By Proposition 18, we only need to prove strictness. Let $I:=\lambda x.x$ and consider the terms $P_{k}:=\lambda y_{1}.\dots.\lambda y_{k}.I$ . It can be easily checked that, for any context $\mathtt{C}$ , if $\mathtt{C}[I]$ is solvable, then $\mathtt{C}[P_{k}]$ must be solvable as well. This implies then that, for any $\epsilon>0$ , the open ball $B_{\epsilon}^{\mathrm{ctx}}(I)$ contains all the terms $P_{k}$ .

Now, one can construct a compact basis element $c\in D_{\infty}$ such that, for all $k>2$ , $\llbracket P_{k}\rrbracket\not\ll c\ll\llbracket I\rrbracket$ (see the extended version for the details). Since $\mathcal{O}_{p_{\infty}}(D_{\infty})$ coincides with the Scott topology, which is generated by the sets $\mathrel{\rotatebox{90.0}{$\twoheadrightarrow$}}b$ , for $b$ a basis element, from $c\ll\llbracket I\rrbracket$ we deduce that there exists $\epsilon>0$ such that $B_{\epsilon}^{p_{\infty}}(\llbracket I\rrbracket)\subseteq\ \mathrel{% \rotatebox{90.0}{$\twoheadrightarrow$}}c$ . From $\llbracket P_{2}\rrbracket\not\ll c$ we deduce then $\llbracket P_{2}\rrbracket\notin B_{\epsilon}^{p_{\infty}}(\llbracket I\rrbracket)$ , we conclude that the open $p_{\infty}$ -ball $B_{\epsilon}^{p_{\infty}}(\llbracket I\rrbracket)$ contains no open $p_{\mathrm{ctx}}$ -ball.

$\hfill\blacktriangleleft$

Recalling that $D_{\infty}$ induces the theory $\mathcal{H}^{*}$ , the relation $p_{\mathrm{B\"{o}hm}}\sqsubset p_{\mathrm{Scott}}$ is in accordance with what happens with the corresponding $\lambda$ -theories. By contrast, while $D_{\infty}$ and the contextual preorder both induce the $\lambda$ -theory $\mathcal{H}^{*}$ , the first induces a $\lambda$ -PPM which is finer than the contextual partial metric. As can be seen in the proof in the Appendix, the reason behind this is that, given terms $M\sqsubseteq_{\mathrm{ctx}}P$ , there exists open $p_{\mathrm{Scott}}$ -balls $B_{\epsilon}(P)$ whose elements all lie above $M$ , while $p_{\mathrm{ctx}}$ cannot define any such ball, since whether $M\leq Q$ cannot be tested by applying only finitely many contexts to $Q$ (cf. Remark 16).

6 Quantifying the Taylor Expansion

In this section we discuss the Taylor expansion of $\lambda$ -terms [18, 19, 20], a well-studied method that refines methods based on Böhm trees and Scott domains, by decomposing the non-linear behavior of a term into the linear behavior of a set of simpler terms, called resource $\lambda$ -terms. Notably, several well-known properties of $\lambda$ -terms (like e.g. continuity and stability), which were originally established by topological and semantic methods, can be proved in a simpler, combinatorial way, via the Taylor expansion [4].

The famous commutation theorem [20] says that the Taylor expansion commutes with the construction of the Böhm tree, and shows that the associated $\lambda$ -theories coincide. By presenting the Taylor expansion as an isometric transformation, we add a quantitative flavor to this result, showing that also the corresponding notions of program similarity coincide.

All proofs of the results contained in this section can be found in the extended version.

Resource terms and the Taylor expansion.

As we said, the Taylor expansion associates a $\lambda$ -term with a set of terms, called resource terms, with a linear operational semantics. The set $\Lambda^{r}$ of resource terms is defined by the grammar $t:=x\mid\lambda x.t\mid t\langle t,\dots,t\rangle$ , where $\langle t,\dots,t\rangle$ indicates a finite multiset of terms. We define an order $\prec$ over resource $\lambda$ -terms as the context closure of the relation $\emptyset\prec\langle t_{1},\dots,t_{n}\rangle$ . The operational semantics of resource terms replaces the standard $\beta$ -rule with a linear monadic rule $\to_{r}$ that relates a redex $(\lambda x.t)\langle u_{1},\dots,u_{n}\rangle$ with the set of terms $t[u_{\sigma(1)}/x_{1},\dots,u_{\sigma(n)}/n]$ , obtained by replacing each occurrence $x_{i}$ of $x$ in $t$ by the term $u_{\sigma(i)}$ , whenever $t$ contains exactly $n$ occurrences of $x$ and where $\sigma$ is any permutation in $\mathfrak{S}_{n}$ . For example, the resource term $(\lambda x.x\langle x\rangle)\langle y,z\rangle$ reduces to the set of terms $\{y\langle z\rangle,z\langle y\rangle\}$ corresponding to the two possible ways of distributing $y, z$ across the two occurrences of $x$ in $x\langle x\rangle$ . Instead, the resource term $(\lambda x.x\langle x\rangle)\langle y\rangle$ reduces to the empty set: as the single occurrence of $y$ cannot be duplicated, it does not suffice to replace all occurrences of $x$ in $x\langle x\rangle$ . More generally, if $t$ contains a number of occurrences of $x$ different from $n$ , then $(\lambda x.t)\langle u_{1},\dots,u_{n}\rangle\to_{r}\emptyset$ . Thanks to the impossibility of duplicating terms, linear reduction $\to_{r}^{*}$ is not only confluent, but also strongly normalizing (in linear time).

The Taylor expansion of a $\lambda$ -term $M$ is a set $\mathcal{T}(M)\subseteq\Lambda^{r}$ defined inductively as $\mathcal{T}(x)=\{x\}$ , $\mathcal{T}(\lambda x.M)=\{\lambda x.t\mid t\in\mathcal{T}(M)\}$ and $\mathcal{T}(MN)=\{t\langle t_{1},\dots,t_{n}\rangle\mid t\in\mathcal{T}(M),x_{% n}\in\mathbb{N},t_{1},\dots,t_{n}\in\mathcal{T}(N)\}$ . For example, the Taylor expansion of $\lambda x.\lambda y.yx$ is composed of all resource terms of the form $\lambda x.\lambda y.y\langle x,\dots,x\rangle$ . Since reduction is confluent and strongly normalizing, we can define the set $\mathrm{nf}(\mathcal{T}(M))$ containing the normal forms of the resource terms in $\mathcal{T}(M)$ .

The Taylor expansion extends to partial $\lambda$ -terms by letting $\mathcal{T}(\bot)=\emptyset$ . In this way, we can define the Taylor expansion of a Böhm tree $\alpha\in\mathrm{Ide}(\mathcal{A})$ by $\mathcal{T}(\alpha)=\bigcup\{\mathcal{T}(A)\mid A\in\alpha\},$ . The aforementioned commutation theorem says then that $\mathcal{T}(\mathcal{B}(M))=\mathrm{nf}(\mathcal{T}(M))$ ; together with the injectivity of $\mathcal{T}$ over Böhm trees (which is easily proved), this shows the equivalence of the $\lambda$ -theory $\mathcal{B}$ and the $\lambda$ -theory generated by equating all closed terms whose Taylor expansions have the same normal form.

We provide an alternative, topological, presentation of the Taylor expansion of Böhm trees. A natural choice would be to take the Scott topology induced by the resource term order $\preceq$ . However, under this order, $\Lambda^{r}$ is not a dcpo: limits of directed sequences need not exist (as they would correspond, just like Böhm trees, to infinite terms). This leads then to consider, just like for partial terms, the completion $\mathrm{Ide}(\Lambda^{r})$ of $\Lambda^{r}$ , which forms an algebraic dcpo. The elements of $\mathrm{Ide}(\Lambda^{r})$ can be seen as possibly infinite resource terms, and the compact elements correspond to the finite ones, that is, to ordinary resource terms.

Recall that $\mathrm{Ide}(\mathcal{A})$ can be identified with the set of Böhm trees; the Taylor expansion can be presented in this setting as a map $\mathcal{T}^{*}:\mathrm{Ide}(\mathcal{A})\to\mathcal{P}(\mathrm{Ide}(\Lambda^{% r}))$ defined by $\mathcal{T}^{*}(\alpha)=\mathrm{Ide}(\mathcal{T}(\alpha)).$ To see that it is well-defined, let us observe that $\mathcal{T}(\alpha)\subseteq\Lambda^{r}$ , so $\mathrm{Ide}(\mathcal{T}(\alpha))\subseteq\mathrm{Ide}(\Lambda^{r})$ is a set of ideals. Notice that the set $\mathcal{T}^{*}(\alpha)$ is closed with respect to the Scott topology of $\mathrm{Ide}(\Lambda^{r})$ .

Defining a metric on $\Lambda^{r}$ .

We introduce a PUM on $\Lambda^{r}$ quantifying the order $\preceq$ , which is essentially an adaptation of the tree partial metric. A normal resource term is of the form $t=\lambda x_{1}.\dots.\lambda x_{n}.xb_{1}\dots b_{m}$ , where each $b_{i}$ is a finite multiset $b_{i}=\langle t_{i}^{1},\dots,t_{i}^{m_{i}}\rangle$ . The height of a resource term $h(t)$ is defined recursively as $h(t)=\max_{ij}h(t_{i}^{j})+1$ , where $t$ is as above. For any variable occurrence $z$ in $t$ , we define its height in $t$ $h_{t}(z)$ as $h_{t}(z)=1$ if $z$ is as $x$ above, and as $h_{t}(z)=h_{t_{i}^{j}}(z)+1$ if the occurrence is in $t_{i}^{j}$ .

For any normal resource term $t$ and $n\leq h(t)$ , we define the resource term $t|_{n}$ , corresponding to the “truncation” of $t$ at height $n$ : if $h(t)\leq n$ , then $t|_{n}=t$ , and if $h(t)>n$ , then we replace any subterm of $t$ of the form $xb_{1}\dots b_{m}$ , where $x$ is at height $n$ , by $x\emptyset\dots\emptyset$ . Observe that $h(t|_{n})\leq n$ and $h(t|_{n})=n$ holds whenever $h(t)\geq n$ .

Definition 40 (resource partial metric).

For any two resource terms $t,u\in\Lambda^{r}$ , we define

r(t,u):=\inf\{2^{-n}\mid h(t),h(u)\geq n\text{ and }t|_{n}\ =\ u|_{n}\}.

By arguing similarly to the case of trees, it can be shown that $r$ is a PUM, and that the order $\leq_{r}$ coincides with $\preceq$ . Notice that $r(t,t)=2^{-h(t)}$ .

Lifting the metric to $\mathcal{P}(\Lambda^{r})$ .

We now discuss how to lift the metric $r$ to subsets of $\Lambda^{r}$ . A standard way to lift a metric $d$ from a set $X$ to its powerset $\mathcal{P}(X)$ is via the Hausdorff lifting $H_{d}(A,B)=\max\{\sup\limits_{a\in A}\inf\limits_{b\in B}d(a,b),\sup\limits_{b% \in B}\inf\limits_{a\in A}d(a,b)\}.$ Intuitively, $H_{d}(A,B)$ looks, for each element of one set, for its closest element in the other set, and then measures the distance that is obtained by this operation in the worst case. The same construction, when applied to a partial metric $p$ , yields the partial Hausdorff metric $H_{p}$ (see [3, 28]) which, in spite of its name, is in fact not a partial metric, as it satisfies a weaker triangular law $H_{p}(A,B)\leq H_{p}(A,C)+H_{p}(C,B)-\inf_{c\in C}p(c,c)$ .

In any case, the Hausdorff lifting $H_{r}$ of the resource partial metric is not the right choice for us: suppose $\alpha$ is an infinite Böhm tree, so that its self-distance is $0$ ; then $\mathcal{T}(\alpha)$ is a set of finite terms of arbitrary depth, so that $H_{r}(\mathcal{T}(\alpha),\mathcal{T}(\alpha))=\sup_{t\in\mathcal{T}(\alpha)}r% (t,t)=\sup\{2^{-|t|}\mid t\in\mathcal{T}(\alpha)\}=\frac{1}{2}>0=p_{\mathrm{% tree}}(\alpha,\alpha)$ . Beyond making the Taylor expansion non-isometric, from this we deduce that $H_{r}$ is constantly $\frac{1}{2}$ over all non-empty Taylor expansions!

Instead, we introduce the following variant of the Hausdorff lifting:

Definition 41.

For any PM $p:X\times X\to[0,1]$ , let $H_{p}^{*}:\mathcal{P}(X)\times\mathcal{P}(X)\to[0,1]$ be:

H^{*}_{p}(A,B)=\max\left\{\sup\limits_{a\in A}\inf\limits_{a^{\prime}\geq_{p}a% \in A,b\in B}p(a^{\prime},b),\sup\limits_{b\in B}\inf\limits_{b^{\prime}\geq_{% p}b\in B,a\in A}p(a,b^{\prime})\right\}.

Intuitively, on two sets $A, B$ , $H^{*}_{p}(A,B)$ measures how close the elements of $A$ get to the elements of $B$ as soon as one is allowed to freely move higher within $A$ and $B$ following the order $\leq_{p}$ . Notice that, for $\alpha$ an infinite Böhm tree, we now have $H_{r}^{*}(\mathcal{T}(\alpha),\mathcal{T}(\alpha))=0$ , as desired. Similarly to the partial Hausdorff metric $H_{p}$ , for a partial metric $p$ , $H_{p}^{*}$ is not in general a partial metric. Indeed, it only satisfies the following properties:

Proposition 42.

For any partial metric space $(X,p)$ , the distance $H^{*}_{p}$ satisfies:

1.

$H^{*}_{p}(A,A)\leq H^{*}_{p}(A,B)$ ;
2.

$H^{*}_{p}(A,B)=H_{p}^{*}(B,A)$ ;
3.

$H^{*}_{p}(A,B)\leq H^{*}_{p}(A,C)+H^{*}_{p}(C,B)-\inf_{c\in C}p(c,c)$ .

However, $H_{p}^{*}$ is in fact a PM when restricted to $\mathrm{Ide}_{p}(X)$ , the dcpo of ideals with respect to the order $\leq_{p}$ .

Proposition 43.

For any PM $p$ on $X$ , $H^{*}_{p}$ is a PM on $\mathrm{Ide}_{p}(X)$ quantifying the order $\subseteq$ .

When $p=r$ , the resource partial metric, $H_{r}^{*}$ indeed quantifies the Scott topology:

Proposition 44.

The PM $H_{r}^{*}$ quantifies the Scott topology on $\mathrm{Ide}_{r}(\Lambda^{r})$ .

Taylor is an isometry.

The Taylor expansion can be presented either as a map $\mathcal{T}:\Lambda\to\mathcal{P}(\Lambda^{r})$ turning a $\lambda$ -term into a set of resource terms, or as a map $\mathcal{T}^{*}:\mathrm{Ide}(\mathcal{A})\to\mathcal{P}(\mathrm{Ide}(\Lambda^{% r}))$ turning a Böhm tree (i.e. an infinitary normal $\lambda$ -term) into a set of infinitary resource terms.

We will show that both maps are isometries, when considering $\Lambda$ with the Böhm PM and $\mathrm{Ide}(\mathcal{A})$ with the tree PM, and measuring sets of (finite/infinite) resource terms via the lifting $H_{r}^{*}$ of the resource partial metric.

Let the $\lambda$ -PPM $p_{\mathrm{Taylor}}$ be defined by $p_{\mathrm{Taylor}}(M,N)=H_{r}^{*}(\mathrm{nf}(\mathcal{T}(M)),\mathrm{nf}(% \mathcal{T}(N)))$ . As we observed, the $\lambda$ -theory generated by equating all terms $M, N$ such that $\mathrm{nf}(\mathcal{T}(M))=\mathrm{nf}(\mathcal{T}(N))$ coincides the theory $\mathcal{B}$ . Our result will extend this to the corresponding quantitative theories.

Let us first consider the Taylor expansion of $\lambda$ -terms.

Theorem 45.

$\mathcal{T}:(\Lambda,p_{\mathrm{B\"{o}hm}})\longrightarrow(\mathcal{P}(\Lambda% ^{r}),H_{r}^{*})$ is an isometry. Thus, $p_{\mathrm{Taylor}}=p_{\mathrm{B\"{o}hm}}$ .

The results above states that, whenever the Böhm trees of two terms $M, N$ differ at height $n$ , then, by moving higher and higher in their normalized Taylor expansions $\mathcal{T}(M)$ and $\mathcal{T}(N)$ , one can find resource terms that differ precisely at height $n$ , and can do no better.

Let us now consider the map $\mathcal{T}^{*}$ . Since $\mathrm{Ide}(\Lambda^{r})$ is quantified by $H_{r}^{*}$ , we can consider its lifting $H^{*}_{H_{r}^{*}}$ to $\mathcal{P}(\mathrm{Ide}_{p}(\Lambda^{r}))$ . In fact, the computation of $H^{*}_{H_{r}^{*}}$ leads us back to $H_{r}^{*}$ :

Lemma 46.

For all $\lambda$ -terms $M, N$ , $H^{*}_{r}(\mathcal{T}(M),\mathcal{T}(N))=H^{*}_{H_{r}^{*}}(\mathcal{T}^{*}(M),% \mathcal{T}^{*}(N)).$

Thanks to Proposition 45, this immediately produces:

Theorem 47.

$\mathcal{T}^{*}:(\mathrm{Ide}(\mathcal{A}),p_{\mathrm{tree}})\longrightarrow(% \mathcal{P}(\mathrm{Ide}(\Lambda_{r})),H^{*}_{H^{*}_{r}})$ is an isometry.

$\blacktriangleright$ Remark 48.

As shown in detail in the long version, we can obtain an isometry also if we choose to measure Böhm trees and Taylor expansions using the PMs from Examples 35 and 36. Indeed, for any enumeration $(A_{n})_{n}$ of partial terms, one can define an enumeration $(r_{n})_{n}$ of resource terms and weights $\theta_{n}$ such that $\mathcal{T}:(\mathcal{B},p^{\mathcal{B}}_{(A_{n})_{n},\frac{1}{2^{n}}})% \longrightarrow(\mathcal{P}(\Lambda_{r}),p^{\mathcal{P}}_{(r_{n})_{n},\theta_{% n}})$ is an isometry.

7 Conclusions

Related Work.

Since their introduction in [8], the literature on partial metrics has grown vast, and comprises both theoretical investigations [39, 34, 3, 29] and connections with theoretical computer science [38], notably domain theory [9, 35, 40, 41]. Recently, an elegant categorical description of partial metric spaces as quantaloid-enriched categories has been proposed [28], as well as a characterization of the partial metric spaces that are exponentiable (in a category whose morphisms are the non-expansive - or 1-Lipschitz - functions and not, as in this paper, all continuous functions). While, as we have said, the metrizability of Scott domains via partial metrics has been well known since [9, 35], not much is found in this vast literature about the specific use of partial metrics for studying the topological semantics of the $\lambda$ -calculus or, more generally, of higher-order programming languages.

Beyond partial metrics, the literature on higher-order program metrics has been growing vast as well. As the category Met of metric spaces and non-expansive functions is not cartesian closed, the literature has focused on two complementary directions: on the one hand, restrict to cartesian closed sub-categories of Met, like ultra-metric spaces [23], or injective metric spaces [10]; [15] adapts Mardare’s et al.’s quantitative equational theories [32] to higher-order languages, introducing a notion of quantitative $\lambda$ -theory (which, contrarily to $\lambda$ -PPMs, require contexts to be non-expansive). On the other hand, restrict attention to linear [12, 16] or graded [37, 17] $\lambda$ -calculi, which can be modeled in Met. Notably, [17] introduces metric CPOs, that is CPOs endowed with sub-continuous metrics (i.e. satisfying $d(\lim_{n}x_{n},\lim_{n}y_{n})\leq\epsilon$ whenever $d(x_{n},y_{n})\leq\epsilon$ holds for all $n$ ). This is a weaker condition than quantifiability, since the limits in the metric need not coincide with the CPO limits.

Differential logical relations [14, 13] have been recently introduced as a generalized approach to program metrics, relaxing usual Lipschitz, and even continuity, conditions. Notably, related models based on generalized partial metric spaces are studied in [27, 36]. In such models distances need not be positive reals but are computed on an arbitrary quantale.

Finally, several works have investigated infinitary $\lambda$ -calculi defined via a metric completion of ordinary terms [30, 33]. These approaches are based on ultrametrics akin to the tree metric considered in this paper for Böhm trees. Recall that ordinary metric spaces are topologically Hausdorff, contrarily to the spaces considered in this paper. The metric completion of partial metric spaces is discussed in [26, 28].

Future Work.

While this paper focuses on metric counterparts for well-known techniques, our results suggest several potential developments.

The metrizability of Scott domains suggests to study models based on Lipschitz-continuous, rather than just continuous, functions, as is standard in the literature on linear $\lambda$ -calculi. For instance, considering the Böhm metric, a non-expansive context should respect depth: if two terms $M, N$ coincide up to depth $n$ , then $\mathtt{C}[M]$ and $\mathtt{C}[N]$ must also coincide up to depth $n$ . This suggests connections with recent work on stratified notions of program equivalence [2].

Sections 4 and 6 introduced several methods to lift a partial metric to the powerset; using such liftings, as we suggest at several places, our results based on Scott domains could be adapted to the relational model, in which $\lambda$ -terms are interpreted via relations $R\in\mathcal{P}(A\times B)$ .

While we here just considered the untyped $\lambda$ -calculus and basic cartesian closed structure (i.e. finite products and exponentials), the applicative distances introduced in this paper should adapt well also to languages with coproducts and dependent types; moreover, our results on the Hausdorff lifting suggests that other monadic liftings (e.g. the probability monad) could be considered. At the same time, the metric account of RealPCF suggested at in Example 33 could be explored in more depth, for instance considering the behavior of operators like the parallel if or even program derivatives.

Finally, the fact that several partial metrics considered in this paper produce computable distances between finite approximants suggests to explore potential connections with quantitative type systems related to the relational and topological semantics, like those based on non-idempotent intersection types [7].

References

[1] Roberto M. Amadio and Pierre-Louis Curien. Domains and Lambda-Calculi. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1998.
[2] Victor Arrial, Giulio Guerrieri, and Delia Kesner. Genericity through stratification. In Proceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS ’24, New York, NY, USA, 2024. Association for Computing Machinery. doi:10.1145/3661814.3662113.
[3] Hassen Aydi, Mujahid Abbas, and Calogero Vetro. Partial Hausdorff metric and Nadler’s fixed point theorem on partial metric spaces. Topology and its Applications, 159(14):3234–3242, 2012. doi:10.1016/j.topol.2012.06.012.
[4] Davide Barbarossa and Giulio Manzonetto. Taylor subsumes Scott, Berry, Kahn and Plotkin. Proc. ACM Program. Lang., 4(POPL), December 2019. doi:10.1145/3371069.
[5] Hendrik Pieter Barendregt. The lambda calculus - its syntax and semantics, volume 103 of Studies in logic and the foundations of mathematics. North-Holland, 1985.
[6] Antonio Bucciarelli, Thomas Ehrhard, and Giulio Manzonetto. Not enough points is enough. In Jacques Duparc and Thomas A. Henzinger, editors, Computer Science Logic, pages 298–312, Berlin, Heidelberg, 2007. Springer Berlin Heidelberg. doi:10.1007/978-3-540-74915-8_24.
[7] Antonio Bucciarelli, Delia Kesner, and Daniel Ventura. Non-idempotent intersection types for the lambda-calculus. Logic Journal of the IGPL, 25(4):431–464, 2017. doi:10.1093/jigpal/jzx018.
[8] Michael Bukatin, Ralph Kopperman, Steve Matthews, and Homeira Pajoohesh. Partial metric spaces. American Mathematical Monthly, 116:708–718, October 2009. URL: http://www.jstor.org/stable/40391197, doi:10.4169/193009709X460831.
[9] Michael A. Bukatin and Joshua S. Scott. Towards computing distances between programs via Scott domains. In Sergei Adian and Anil Nerode, editors, Logical Foundations of Computer Science, pages 33–43, Berlin, Heidelberg, 1997. Springer Berlin Heidelberg. doi:10.1007/3-540-63045-7_4.
[10] Maria Manuel Clementino and Dirk Hofmann. Exponentiation in V-categories. Topology and its Applications, 153(16):3113–3128, 2006. Special Issue: Aspects of Contemporary Topology. doi:10.1016/j.topol.2005.01.038.
[11] Raphaëlle Crubillé and Ugo Dal Lago. Metric Reasoning About Lambda-Terms: The General Case. In Hongseok Yang, editor, Programming Languages and Systems - 26th European Symposium on Programming, ESOP 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, volume 10201 of Lecture Notes in Computer Science, pages 341–367, Berlin, Heidelberg, 2017. Springer. doi:10.1007/978-3-662-54434-1_13.
[12] Fredrik Dahlqvist and Renato Neves. An Internal Language for Categories Enriched over Generalised Metric Spaces. In Florin Manea and Alex Simpson, editors, 30th EACSL Annual Conference on Computer Science Logic (CSL 2022), volume 216 of Leibniz International Proceedings in Informatics (LIPIcs), pages 16:1–16:18, Dagstuhl, Germany, 2022. Schloss Dagstuhl – Leibniz-Zentrum für Informatik. doi:10.4230/LIPIcs.CSL.2022.16.
[13] Ugo Dal Lago and Francesco Gavazzo. Differential logical relations part II: increments and derivatives. In Gennaro Cordasco, Luisa Gargano, and Adele A. Rescigno, editors, Proceedings of the 21st Italian Conference on Theoretical Computer Science, Ischia, Italy, September 14-16, 2020, volume 2756 of CEUR Workshop Proceedings, pages 101–114. CEUR-WS.org, 2020. URL: http://ceur-ws.org/Vol-2756/paper_10.pdf.
[14] Ugo Dal Lago, Francesco Gavazzo, and Akira Yoshimizu. Differential logical relations, part I: the simply-typed case. In 46th International Colloquium on Automata, Languages, and Programming, ICALP 2019, July 9-12, 2019, Patras, Greece, pages 111:1–111:14, 2019. doi:10.4230/LIPIcs.ICALP.2019.111.
[15] Ugo Dal Lago, Furio Honsell, Marina Lenisa, and Paolo Pistone. On Quantitative Algebraic Higher-Order Theories. In Amy P. Felty, editor, 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022), volume 228 of Leibniz International Proceedings in Informatics (LIPIcs), pages 4:1–4:18, Dagstuhl, Germany, 2022. Schloss Dagstuhl – Leibniz-Zentrum für Informatik. doi:10.4230/LIPIcs.FSCD.2022.4.
[16] Ugo Dal Lago, Naohiko Hoshino, and Paolo Pistone. On the Lattice of Program Metrics. In Marco Gaboardi and Femke van Raamsdonk, editors, 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023), volume 260 of Leibniz International Proceedings in Informatics (LIPIcs), pages 20:1–20:19, Dagstuhl, Germany, 2023. Schloss Dagstuhl – Leibniz-Zentrum für Informatik. doi:10.4230/LIPIcs.FSCD.2023.20.
[17] Arthur Azevedo de Amorim, Marco Gaboardi, Justin Hsu, Shin-ya Katsumata, and Ikram Cherigui. A semantic account of metric preservation. In Giuseppe Castagna and Andrew D. Gordon, editors, Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017, POPL 2017, pages 545–556, New York, NY, USA, 2017. ACM. doi:10.1145/3009837.3009890.
[18] Thomas Ehrhard and Laurent Regnier. The differential lambda-calculus. Theoretical Computer Science, 309:1–41, 2003. doi:10.1016/S0304-3975(03)00392-X.
[19] Thomas Ehrhard and Laurent Regnier. Böhm Trees, Krivine’s Machine and the Taylor Expansion of Lambda-Terms. In Arnold Beckmann, Ulrich Berger, Benedikt Löwe, and John V. Tucker, editors, Logical Approaches to Computational Barriers, pages 186–197, Berlin, Heidelberg, 2006. Springer Berlin Heidelberg. doi:10.1007/11780342_20.
[20] Thomas Ehrhard and Laurent Regnier. Uniformity and the Taylor expansion of ordinary lambda-terms. Theor. Comput. Sci., 403(2-3):347–372, 2008. doi:10.1016/j.tcs.2008.06.001.
[21] Thomas Erker, Martín Hötzel Escardó, and Klaus Keimel. The way-below relation of function spaces over semantic domains. Topology and its Applications, 89(1):61–74, 1998. Domain Theory. doi:10.1016/S0166-8641(97)00226-5.
[22] Martín Hötzel Escardó. PCF extended with real numbers. Theor. Comput. Sci., 162(1):79–115, 1996. doi:10.1016/0304-3975(95)00250-2.
[23] Martín Hötzen Escardó. A metric model of PCF. Unpublished note presented at the Workshop on Realizability Semantics and Applications, June 1999. Available at the author’s webpage., 1999.
[24] M.H. Escardo and R. Heckmann. Topologies on spaces of continuous functions. Topology Proceedings, 26(2):545–564, 2001-2002.
[25] Francesco Gavazzo. Quantitative behavioural reasoning for higher-order effectful programs: Applicative distances. In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS ’18, pages 452–461, New York, NY, USA, 2018. doi:10.1145/3209108.3209149.
[26] Xun Ge and Shou Lin. Completions of partial metric spaces. Topology and its Applications, 182:16–23, 2015. doi:10.1016/j.topol.2014.12.013.
[27] Guillaume Geoffroy and Paolo Pistone. A partial metric semantics of higher-order types and approximate program transformations. In Computer Science Logic 2021 (CSL 2021), volume 183 of LIPIcs–Leibniz International Proceedings in Informatics, pages 35:1–35:18, 2021. doi:10.4230/LIPIcs.CSL.2021.23.
[28] Dirk Hofmann and Isar Stubbe. Topology from enrichment: the curious case of partial metrics. Cahiers de Topologie et Géométrie DIfférentielle Catégorique, LIX, 4:307–353, 2018.
[29] Gunther Jäger and T. M. G. Ahsanullah. Characterization of quantale-valued metric spaces and quantale-valued partial metric spaces by convergence. Applied General Topology, 19(1):129–144, 2018.
[30] Richard Kennaway, Jan Willem Klop, M. Ronan Sleep, and Fer-Jan de Vries. Infinitary lambda calculus. Theor. Comput. Sci., 175(1):93–125, 1997. doi:10.1016/S0304-3975(96)00171-5.
[31] Giulio Manzonetto. Models and theories of lambda calculus. PhD thesis, Paris Diderot University, France, 2008. URL: https://tel.archives-ouvertes.fr/tel-00715207.
[32] Radu Mardare, Prakash Panangaden, and Gordon Plotkin. Quantitative algebraic reasoning. In Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2016). IEEE Computer Society, 2016.
[33] Damiano Mazza. Non-linearity as the metric completion of linearity. In Masahito Hasegawa, editor, Typed Lambda Calculi and Applications, pages 3–14, Berlin, Heidelberg, 2013. Springer Berlin Heidelberg. doi:10.1007/978-3-642-38946-7_3.
[34] Volodymyr Mykhaylyuk and Vadym Myronyk. Metrizability of partial metric spaces. Topology and its Applications, 308:107949, 2022. doi:10.1016/j.topol.2021.107949.
[35] S.J. O’Neill. Partial metrics, valuations and domain theory. Annals of the New York Academy of Sciences, 806:304–315, 1996.
[36] Paolo Pistone. On generalized metric spaces for the simply typed lambda-calculus. In 36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021, Rome, Italy, June 29 - July 2, 2021, pages 1–14. IEEE, 2021. doi:10.1109/LICS52264.2021.9470696.
[37] Jason Reed and Benjamin C. Pierce. Distance makes the types grow stronger: a calculus for differential privacy. In Paul Hudak and Stephanie Weirich, editors, Proceeding of the 15th ACM SIGPLAN international conference on Functional programming, ICFP 2010, Baltimore, Maryland, USA, September 27-29, 2010, pages 157–168. ACM, 2010. doi:10.1145/1863543.1863568.
[38] Salvador Romaguera, Pedro Tirado, and Óscar Valero. Complete partial metric spaces have partially metrizable computational models. Int. J. Comput. Math., 89(3):284–290, 2012. doi:10.1080/00207160.2011.559229.
[39] M. P. Schellekens. The correspondence between partial metrics and semivaluations. Theoretical Computer Science, 315(1):135–149, May 2004. doi:10.1016/j.tcs.2003.11.016.
[40] Michel P. Schellekens. A characterization of partial metrizability: domains are quantifiable. Theor. Comput. Sci., 305(1-3):409–432, 2003. Topology in Computer Science. doi:10.1016/S0304-3975(02)00705-3.
[41] Michael B. Smyth. The constructive maximal point space and partial metrizability. Ann. Pure Appl. Log., 137(1-3):360–379, 2006. doi:10.1016/j.apal.2005.05.032.
[42] Pawel Waszkiewicz. Distance and measurement in domain theory. Electronic Notes in Theoretical Computer Science, 45, 2001. doi:10.1016/S1571-0661(04)80975-7.

[bib.bib1] [1] Roberto M. Amadio and Pierre-Louis Curien. Domains and Lambda-Calculi. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1998.

[bib.bib2] [2] Victor Arrial, Giulio Guerrieri, and Delia Kesner. Genericity through stratification. In Proceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS ’24, New York, NY, USA, 2024. Association for Computing Machinery. doi:10.1145/3661814.3662113.

[bib.bib3] [3] Hassen Aydi, Mujahid Abbas, and Calogero Vetro. Partial Hausdorff metric and Nadler’s fixed point theorem on partial metric spaces. Topology and its Applications, 159(14):3234–3242, 2012. doi:10.1016/j.topol.2012.06.012.

[bib.bib4] [4] Davide Barbarossa and Giulio Manzonetto. Taylor subsumes Scott, Berry, Kahn and Plotkin. Proc. ACM Program. Lang., 4(POPL), December 2019. doi:10.1145/3371069.

[bib.bib5] [5] Hendrik Pieter Barendregt. The lambda calculus - its syntax and semantics, volume 103 of Studies in logic and the foundations of mathematics. North-Holland, 1985.

[bib.bib6] [6] Antonio Bucciarelli, Thomas Ehrhard, and Giulio Manzonetto. Not enough points is enough. In Jacques Duparc and Thomas A. Henzinger, editors, Computer Science Logic, pages 298–312, Berlin, Heidelberg, 2007. Springer Berlin Heidelberg. doi:10.1007/978-3-540-74915-8_24.

[bib.bib7] [7] Antonio Bucciarelli, Delia Kesner, and Daniel Ventura. Non-idempotent intersection types for the lambda-calculus. Logic Journal of the IGPL, 25(4):431–464, 2017. doi:10.1093/jigpal/jzx018.

[bib.bib8] [8] Michael Bukatin, Ralph Kopperman, Steve Matthews, and Homeira Pajoohesh. Partial metric spaces. American Mathematical Monthly, 116:708–718, October 2009. URL: http://www.jstor.org/stable/40391197, doi:10.4169/193009709X460831.

[bib.bib9] [9] Michael A. Bukatin and Joshua S. Scott. Towards computing distances between programs via Scott domains. In Sergei Adian and Anil Nerode, editors, Logical Foundations of Computer Science, pages 33–43, Berlin, Heidelberg, 1997. Springer Berlin Heidelberg. doi:10.1007/3-540-63045-7_4.

[bib.bib10] [10] Maria Manuel Clementino and Dirk Hofmann. Exponentiation in V-categories. Topology and its Applications, 153(16):3113–3128, 2006. Special Issue: Aspects of Contemporary Topology. doi:10.1016/j.topol.2005.01.038.

[bib.bib11] [11] Raphaëlle Crubillé and Ugo Dal Lago. Metric Reasoning About Lambda-Terms: The General Case. In Hongseok Yang, editor, Programming Languages and Systems - 26th European Symposium on Programming, ESOP 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, volume 10201 of Lecture Notes in Computer Science, pages 341–367, Berlin, Heidelberg, 2017. Springer. doi:10.1007/978-3-662-54434-1_13.

[bib.bib12] [12] Fredrik Dahlqvist and Renato Neves. An Internal Language for Categories Enriched over Generalised Metric Spaces. In Florin Manea and Alex Simpson, editors, 30th EACSL Annual Conference on Computer Science Logic (CSL 2022), volume 216 of Leibniz International Proceedings in Informatics (LIPIcs), pages 16:1–16:18, Dagstuhl, Germany, 2022. Schloss Dagstuhl – Leibniz-Zentrum für Informatik. doi:10.4230/LIPIcs.CSL.2022.16.

[bib.bib13] [13] Ugo Dal Lago and Francesco Gavazzo. Differential logical relations part II: increments and derivatives. In Gennaro Cordasco, Luisa Gargano, and Adele A. Rescigno, editors, Proceedings of the 21st Italian Conference on Theoretical Computer Science, Ischia, Italy, September 14-16, 2020, volume 2756 of CEUR Workshop Proceedings, pages 101–114. CEUR-WS.org, 2020. URL: http://ceur-ws.org/Vol-2756/paper_10.pdf.

[bib.bib14] [14] Ugo Dal Lago, Francesco Gavazzo, and Akira Yoshimizu. Differential logical relations, part I: the simply-typed case. In 46th International Colloquium on Automata, Languages, and Programming, ICALP 2019, July 9-12, 2019, Patras, Greece, pages 111:1–111:14, 2019. doi:10.4230/LIPIcs.ICALP.2019.111.

[bib.bib15] [15] Ugo Dal Lago, Furio Honsell, Marina Lenisa, and Paolo Pistone. On Quantitative Algebraic Higher-Order Theories. In Amy P. Felty, editor, 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022), volume 228 of Leibniz International Proceedings in Informatics (LIPIcs), pages 4:1–4:18, Dagstuhl, Germany, 2022. Schloss Dagstuhl – Leibniz-Zentrum für Informatik. doi:10.4230/LIPIcs.FSCD.2022.4.

[bib.bib16] [16] Ugo Dal Lago, Naohiko Hoshino, and Paolo Pistone. On the Lattice of Program Metrics. In Marco Gaboardi and Femke van Raamsdonk, editors, 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023), volume 260 of Leibniz International Proceedings in Informatics (LIPIcs), pages 20:1–20:19, Dagstuhl, Germany, 2023. Schloss Dagstuhl – Leibniz-Zentrum für Informatik. doi:10.4230/LIPIcs.FSCD.2023.20.

[bib.bib17] [17] Arthur Azevedo de Amorim, Marco Gaboardi, Justin Hsu, Shin-ya Katsumata, and Ikram Cherigui. A semantic account of metric preservation. In Giuseppe Castagna and Andrew D. Gordon, editors, Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017, POPL 2017, pages 545–556, New York, NY, USA, 2017. ACM. doi:10.1145/3009837.3009890.

[bib.bib18] [18] Thomas Ehrhard and Laurent Regnier. The differential lambda-calculus. Theoretical Computer Science, 309:1–41, 2003. doi:10.1016/S0304-3975(03)00392-X.

[bib.bib19] [19] Thomas Ehrhard and Laurent Regnier. Böhm Trees, Krivine’s Machine and the Taylor Expansion of Lambda-Terms. In Arnold Beckmann, Ulrich Berger, Benedikt Löwe, and John V. Tucker, editors, Logical Approaches to Computational Barriers, pages 186–197, Berlin, Heidelberg, 2006. Springer Berlin Heidelberg. doi:10.1007/11780342_20.

[bib.bib20] [20] Thomas Ehrhard and Laurent Regnier. Uniformity and the Taylor expansion of ordinary lambda-terms. Theor. Comput. Sci., 403(2-3):347–372, 2008. doi:10.1016/j.tcs.2008.06.001.

[bib.bib21] [21] Thomas Erker, Martín Hötzel Escardó, and Klaus Keimel. The way-below relation of function spaces over semantic domains. Topology and its Applications, 89(1):61–74, 1998. Domain Theory. doi:10.1016/S0166-8641(97)00226-5.

[bib.bib22] [22] Martín Hötzel Escardó. PCF extended with real numbers. Theor. Comput. Sci., 162(1):79–115, 1996. doi:10.1016/0304-3975(95)00250-2.

[bib.bib23] [23] Martín Hötzen Escardó. A metric model of PCF. Unpublished note presented at the Workshop on Realizability Semantics and Applications, June 1999. Available at the author’s webpage., 1999.

[bib.bib24] [24] M.H. Escardo and R. Heckmann. Topologies on spaces of continuous functions. Topology Proceedings, 26(2):545–564, 2001-2002.

[bib.bib25] [25] Francesco Gavazzo. Quantitative behavioural reasoning for higher-order effectful programs: Applicative distances. In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS ’18, pages 452–461, New York, NY, USA, 2018. doi:10.1145/3209108.3209149.

[bib.bib26] [26] Xun Ge and Shou Lin. Completions of partial metric spaces. Topology and its Applications, 182:16–23, 2015. doi:10.1016/j.topol.2014.12.013.

[bib.bib27] [27] Guillaume Geoffroy and Paolo Pistone. A partial metric semantics of higher-order types and approximate program transformations. In Computer Science Logic 2021 (CSL 2021), volume 183 of LIPIcs–Leibniz International Proceedings in Informatics, pages 35:1–35:18, 2021. doi:10.4230/LIPIcs.CSL.2021.23.

[bib.bib28] [28] Dirk Hofmann and Isar Stubbe. Topology from enrichment: the curious case of partial metrics. Cahiers de Topologie et Géométrie DIfférentielle Catégorique, LIX, 4:307–353, 2018.

[bib.bib29] [29] Gunther Jäger and T. M. G. Ahsanullah. Characterization of quantale-valued metric spaces and quantale-valued partial metric spaces by convergence. Applied General Topology, 19(1):129–144, 2018.

[bib.bib30] [30] Richard Kennaway, Jan Willem Klop, M. Ronan Sleep, and Fer-Jan de Vries. Infinitary lambda calculus. Theor. Comput. Sci., 175(1):93–125, 1997. doi:10.1016/S0304-3975(96)00171-5.

[bib.bib31] [31] Giulio Manzonetto. Models and theories of lambda calculus. PhD thesis, Paris Diderot University, France, 2008. URL: https://tel.archives-ouvertes.fr/tel-00715207.

[bib.bib32] [32] Radu Mardare, Prakash Panangaden, and Gordon Plotkin. Quantitative algebraic reasoning. In Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2016). IEEE Computer Society, 2016.

[bib.bib33] [33] Damiano Mazza. Non-linearity as the metric completion of linearity. In Masahito Hasegawa, editor, Typed Lambda Calculi and Applications, pages 3–14, Berlin, Heidelberg, 2013. Springer Berlin Heidelberg. doi:10.1007/978-3-642-38946-7_3.

[bib.bib34] [34] Volodymyr Mykhaylyuk and Vadym Myronyk. Metrizability of partial metric spaces. Topology and its Applications, 308:107949, 2022. doi:10.1016/j.topol.2021.107949.

[bib.bib35] [35] S.J. O’Neill. Partial metrics, valuations and domain theory. Annals of the New York Academy of Sciences, 806:304–315, 1996.

[bib.bib36] [36] Paolo Pistone. On generalized metric spaces for the simply typed lambda-calculus. In 36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021, Rome, Italy, June 29 - July 2, 2021, pages 1–14. IEEE, 2021. doi:10.1109/LICS52264.2021.9470696.

[bib.bib37] [37] Jason Reed and Benjamin C. Pierce. Distance makes the types grow stronger: a calculus for differential privacy. In Paul Hudak and Stephanie Weirich, editors, Proceeding of the 15th ACM SIGPLAN international conference on Functional programming, ICFP 2010, Baltimore, Maryland, USA, September 27-29, 2010, pages 157–168. ACM, 2010. doi:10.1145/1863543.1863568.

[bib.bib38] [38] Salvador Romaguera, Pedro Tirado, and Óscar Valero. Complete partial metric spaces have partially metrizable computational models. Int. J. Comput. Math., 89(3):284–290, 2012. doi:10.1080/00207160.2011.559229.

[bib.bib39] [39] M. P. Schellekens. The correspondence between partial metrics and semivaluations. Theoretical Computer Science, 315(1):135–149, May 2004. doi:10.1016/j.tcs.2003.11.016.

[bib.bib40] [40] Michel P. Schellekens. A characterization of partial metrizability: domains are quantifiable. Theor. Comput. Sci., 305(1-3):409–432, 2003. Topology in Computer Science. doi:10.1016/S0304-3975(02)00705-3.

[bib.bib41] [41] Michael B. Smyth. The constructive maximal point space and partial metrizability. Ann. Pure Appl. Log., 137(1-3):360–379, 2006. doi:10.1016/j.apal.2005.05.032.

[bib.bib42] [42] Pawel Waszkiewicz. Distance and measurement in domain theory. Electronic Notes in Theoretical Computer Science, 45, 2001. doi:10.1016/S1571-0661(04)80975-7.

The Lambda Calculus Is Quantifiable

Abstract

Keywords and phrases:

Funding:

Copyright and License:

2012 ACM Subject Classification:

Related Version:

DOI:

Event:

Editors:

Series and Publisher:

1 Introduction

Two notions of program approximation.

Quantifying 𝝀-theories via partial metrics.

Contributions.

Outline.

2 Partial Metric Spaces

Definition 1.

Definition 2 (open balls, topology).

Definition 3.

Example 4 (Sierpinski space).

Example 5 (Intervals).

Example 6 (Labeled trees).

3 Quantifying 𝝀-Theories

𝝀-PPMs.

Definition 7.

Lemma 8.

Proof.

▶ Remark 9.

Definition 10 (λ-PPM).

Böhm Trees.

Definition 11 (Böhm partial metric).

Proposition 12.

▶ Remark 13.

Contextual equivalence.

Definition 14 (contextual partial metric).

Proposition 15.

▶ Remark 16.

Proposition 17.

Proof.

Proposition 18.

Proof.

▶ Remark 19.

4 Quantifying Scott Domains

Scott Domains via Partial Metrics.

Definition 20.

Proposition 21.

Lemma 22.

Proof.

Proposition 23.

Proof.

Example 24.

▶ Remark 25 (computability of p⁢(x,y)<ϵ).

Example 26 (ϵ/δ-continuity of contexts).

Theorem 27 (cf. [40]).

Applicative distances and the function space.

Proposition 28.

▶ Remark 29.

Proposition 30.

Lemma 31.

Proof.

Lemma 32 (cf. [21]).

Proof of Proposition 30.

Example 33 (RealPCF).

Example 34 (Scott topologies of open and closed sets).

Example 35 (Böhm trees as closed sets).

Example 36 (Scott topology of the power set).

5 Quantifying a Reflexive Object

Quantifying Scott’s 𝑫∞.

Lemma 37.

Proof.

Theorem 38.

Proof.

The Scott 𝝀-PPM.

Proposition 39.

Proof sketch.

6 Quantifying the Taylor Expansion

Resource terms and the Taylor expansion.

Defining a metric on 𝚲𝒓.

Definition 40 (resource partial metric).

Quantifying $\lambda$ -theories via partial metrics.

3 Quantifying $\lambda$ -Theories

$\lambda$ -PPMs.

$\blacktriangleright$ Remark 9.

Definition 10 ( $\lambda$ -PPM).

$\blacktriangleright$ Remark 13.

$\blacktriangleright$ Remark 16.

$\blacktriangleright$ Remark 19.

$\blacktriangleright$ Remark 25 (computability of $p(x,y)<\epsilon$ ).

Example 26 ( $\epsilon/\delta$ -continuity of contexts).

$\blacktriangleright$ Remark 29.

Quantifying Scott’s $D_{\infty}$ .

The Scott $\lambda$ -PPM.

Defining a metric on $\Lambda^{r}$ .

Lifting the metric to $\mathcal{P}(\Lambda^{r})$ .

$\blacktriangleright$ Remark 48.