arXiv:1702.00374v2 [cs.PL] 11 Jul 2017

A Semantic Account of Metric Preservation
Arthur Azevedo de Amorim

Marco Gaboardi

Justin Hsu

University of Pennsylvania, USA

University at Buffalo,
The State University of New York, USA

University of Pennsylvania, USA

Shin-ya Katsumata

Ikram Cherigui

Research Institute for Mathematical Sciences,
Kyoto University, Japan

École Normale Supérieure Paris, France

Abstract
Program sensitivity measures how robust a program is to small
changes in its input, and is a fundamental notion in domains ranging
from differential privacy to cyber-physical systems. A natural way
to formalize program sensitivity is in terms of metrics on the input
and output spaces, requiring that an r-sensitive function map inputs
that are at distance d to outputs that are at distance at most r · d.
Program sensitivity is thus an analogue of Lipschitz continuity for
programs.
Reed and Pierce introduced Fuzz, a functional language with
a linear type system that can express program sensitivity. They
show soundness operationally, in the form of a metric preservation
property. Inspired by their work, we study program sensitivity and
metric preservation from a denotational point of view. In particular,
we introduce metric CPOs, a novel semantic structure for reasoning
about computation on metric spaces, by endowing CPOs with a
compatible notion of distance. This structure is useful for reasoning
about metric properties of programs, and specifically about program
sensitivity. We demonstrate metric CPOs by giving a model for the
deterministic fragment of Fuzz.
Categories and Subject Descriptors F.3.2 [Logics and Meaning
of Programs]: Semantics of Programming Languages
Keywords domain theory, program sensitivity, metric spaces, Lipschitz continuity

1.

Introduction

In many applications, programs should not be too sensitive to small
variations in their inputs. For example, cyber-physical systems must
cope with measurement errors from the outside world, whereas
differential privacy [22] tries to protect the privacy of individuals
in a database by bounding the influence that the presence of each
individual has on the result of database queries. Program sensitivity
(or Lipschitz continuity) has recently emerged as a useful tool for

reasoning about such requirements. Roughly speaking, sensitivity is
a measure of how much the results of the program may vary when
the program is run on nearby inputs. More formally, a function
f : X → Y is r-sensitive if dX (f (x), f (y)) ≤ r · dY (x, y) for
every pair of inputs x, y ∈ X, where dS is a function assigning a
non-negative distance to pairs of elements of a set S.
Motivated by its useful applications, many techniques have been
proposed for reasoning about program sensitivity formally, including
static analyses for imperative programs [14], relational program
logics [9], and relational refinement types [8]. In this work, we
focus on the approach proposed by Reed and Pierce [38] in the
Fuzz programming language.1 Fuzz is a purely functional PCF-like
language that provides a clean, compositional sensitivity analysis
for higher-order programs. This analysis is implemented as a linear
indexed type system: every Fuzz type τ is endowed with a notion
of distance, and function types !r τ ( σ carry a numeric index r
describing their sensitivity.
Establishing soundness for Fuzz is challenging due to the presence of general recursive functions and types. The central technical
result, metric preservation [38], relied on the definition of intricate,
syntactic logical relations that mixed step-indexing and metric information. The logical relations were used for two purposes: to define
distances, and to prove soundness. This mixed approach obscures
the connection between Fuzz programs and the theory of metric
spaces.
In this paper, we propose an alternative, domain-theoretic treatment of sensitivity and metric preservation in the presence of general
recursion. Our main contribution is a new notion of metric CPO,
which is a complete partial order endowed with a compatible metric,
in the sense that every open ball is stable under limits of ω-chains.
While simple, this notion of compatibility provides a natural extension of the notion of sensitivity to partial functions and has received
little attention in the literature. We use metric CPOs to build a model
of Fuzz that validates metric preservation.2 This model helps clarify
some aspects of the analysis of Fuzz; for instance, a result on least
fixed points on metric CPOs gave us a much more precise encoding
of recursive functions in Fuzz (cf. Lemma 4.9 and Section 5.3).

1 The

language did not have a name at first; “Fuzz” was only introduced later
(e.g. [26, 27]).
2 While Fuzz allows probabilistic sampling to model algorithms from
differential privacy, the probabilistic features of Fuzz are largely orthogonal
to the sensitivity analysis. We keep the discussion focused on sensitivity
analysis, leaving modeling of the probabilistic features for future work.

By grounding our work on well-established domain-theoretic
notions, we can leverage a vast array of tools to model recursive
functions and types. Technically, we first show that metric CPOs
have the appropriate structure for solving recursive domain equations, following the approach laid out by Freyd [25], Smyth and
Plotkin [40], and others. Then, we prove the adequacy of the denotational semantics of Fuzz with respect to its operational semantics
by adapting a method due to Pitts [36] for constructing a family of
type-indexed logical relations. We use fibrational category theory as
a key technical ingredient, for smoothly lifting colimits of CPOs to
the metric setting and for defining relations on metric CPOs.
While our work is primarily motivated by Fuzz, we believe
that metric CPOs can provide useful guidance for studying metric
aspects of programs. For instance, differential privacy is a form of
non-expansiveness [38, Proposition 4.1], but that result applies to
total functions, and it is not clear what it means to partial ones.
Another intriguing question is evaluating what constructs from
the theory of metric spaces could be incorporated in the design
of languages and libraries. For instance, the Banach fixed-point
theorem, a central tool in analysis, has a constructive interpretation
that permits approximating a fixed point up to arbitrary precision,
but it requires reasoning about the sensitivity of programs. We plan
to investigate these and other directions in future work.
Outline. We will begin with a simplified setting that highlights
the core features of sensitivity analysis without general recursion,
reviewing basic notions of metric spaces (Section 2) and showing
how they yield a model of a terminating fragment of Fuzz (Section 3).
Then, we introduce metric CPOs in Section 4 and demonstrate how
the constructions in the terminating fragment can be naturally lifted
to this setting, and how we can use these structures to interpret
recursive definitions of functions and data types. We use these tools
to extend our model of Fuzz with recursive types and to prove metric
preservation in Section 5. We conclude with a discussion of related
work and some promising directions for future work (Sections 6
and 7).

2.

Metric Spaces

We begin by studying the essence of sensitivity analysis in the
simplest setting, with metric spaces and total functions. Most
results here are standard, and covered in more detail in other works
(e.g. [28]).
Let R∞
≥0 , {r ∈ R | r ≥ 0} ∪ {∞} be the set of extended
non-negative reals. We extend addition and the order relation on R
to R∞
≥0 by setting
∞ + r = r + ∞ = ∞,

r ≤ ∞,

for every r ∈ R≥0 .

An extended pseudo-metric space is a tuple (X, dX ), where X
is a set and dX : X 2 → R∞
≥0 is a metric: a function satisfying
(i) dX (x, x) = 0
(ii) dX (x, y) = dX (y, x); and
(iii) the triangle inequality dX (x, z) ≤ dX (x, y) + dX (y, z).
An extended pseudo-metric space differs from the classic notion
of metric space in two respects. First, two points can be at distance
0 from each other without being equal; we don’t impose the axiom
d(x, y) = 0 ⇒ x = y. Second, since distances range over R∞
≥0 ,
pairs of points can be infinitely apart. We simplify the exposition
by henceforth referring to extended pseudo-metric spaces simply as
metric spaces. In additional to standard metric spaces, such as the
real numbers R under the Euclidean metric, we will consider metrics
defined on products, sums, and functions; Figure 1 summarizes these
constructions.

Space (Carrier)

d(a, b)

R

|a − b|

1

0

r · X (X)

r · dX (a, b)

X & Y (X × Y )

max(dX (a1 , b1 ), dY (a2 , b2 ))

X ⊗ Y (X × Y )

dX (a1 , b1 ) + dY (a2 , b2 )

X +Y

dX (a, b) if a, b ∈ X
dY (a, b) if a, b ∈ Y
∞ otherwise

X→Y

supx∈X dY (a(x), b(x))

Figure 1. Basic metric spaces

The essence of sensitivity analysis lies in the notion of nonexpansiveness. A function f : X → Y between metric spaces is
non-expansive if dY (f (x1 ), f (x2 )) ≤ dX (x1 , x2 ) for all x1 , x2 ∈
X. Metric spaces and non-expansive functions form a category
Met with rich structure, which we develop in the remainder of
this section. Non-expansiveness subsumes the notion of function
sensitivity, thanks to the metric scaling operation (cf. Figure 1).
Unpacking definitions, an r-sensitive function X → Y is exactly a
non-expansive function from the r-scaled space r · X to Y .
To define scaling by r, we extend multiplication to R∞
≥0 :
(
0
if r = 0
r·∞,∞
∞·r ,
∞ otherwise.
It is important to point out that multiplication on R∞
≥0 is noncommutative since 0 · ∞ = ∞ and ∞ · 0 = 0. Otherwise, it is
well-behaved: it is associative, monotone in both arguments, and
it distributes over addition. We will later see that this treatment of
∞ is crucial for scaling to distribute over sums, and for modeling
function sensitivity in the presence of non-termination.
If f ∈ Met(X, Y ), then f ∈ Met(r · X, s · Y ) for any r and
s such that r ≥ s. In categorical language, this means that scaling
∞
extends to a bifunctor R∞
≥0 × Met → Met, where R≥0 is regarded
as the category arising from the order ≥ .
Now that we have pinned down the basic definitions for metric
spaces, we turn our attention to simple constructions for building
spaces. These operations will be used to interpret more complex
types, as usual. The first observation is that there are two natural
metrics on a product space X × Y , denoted X & Y and X ⊗ Y .
The first one combines distances by taking the maximum, while
the second one adds them up. These two metrics correspond to
different sensitivity analyses. For instance, addition on real numbers
is a non-expansive function R ⊗ R → R, but not for the signature
R & R → R.
Categorically speaking, there are other differences between the
metrics. The first, X & Y yields the usual notion of Cartesian
product on Met: given two non-expansive functions f : Z → X
and g : Z → Y , the function hf, gi : Z → X × Y defined by
hf, gi(z) , (f (z), g(z))
is non-expansive for X & Y . Furthermore, note that the projections
π1 : X × Y → X

π2 : X × Y → Y

are trivially non-expansive for this metric.
The second, product X ⊗ Y also supports the non-expansive
projections π i , but not pairing. Instead, it allows us to split the metric
of a space: the diagonal function δ(x) = (x, x) is a non-expansive

function
(r + s) · X → (r · X) ⊗ (s · X).
Furthermore, currying and function application are non-expansive
under this metric. More precisely, (Met, ⊗, 1) is a symmetric monoidal category, and there is an adjunction (−) ⊗ X a
Met(X, −) making this structure closed. Here, non-expansive functions are endowed with the supremum metric on functions defined
on Figure 1.
We can also define a metric on the disjoint union of two spaces,
placing elements from different components infinitely far apart.
Note that this metric yields a coproduct on Met: if f : X → Z and
g : Y → Z, then the case-analysis function [f, g] : X + Y → Z
defined as
[f, g](ι1 (x)) , f (x)

[f, g](ι2 (y)) , g(y),

is non-expansive, where ι1 : X → X + Y and ι2 : Y → X + Y
are the (trivially non-expansive) canonical injections.
We conclude with several useful identities that relate scaling to
the above constructions:
r · (X & Y ) = r · X & r · Y
r · (X ⊗ Y ) = r · X ⊗ r · Y
r · (X + Y ) = r · X + r · Y
r · (s · X) = (rs) · X.
The case for sums relies crucially on the fact that 0 · ∞ = ∞, which
guarantees that the copies of X and Y in X + Y remain infinitely
apart after scaling. This point was overlooked in the original Fuzz
work [38], where 0 · ∞ is defined as 0. In that case, the identity only
holds for r > 0 strictly.

3.

Core Fuzz

We now show how to model a fragment of Fuzz without general
recursion. The syntax, summarized in Figure 2, is based on a λcalculus with products and sums, with a few modifications. First,
Fuzz has two pair constructors, (e1 , e2 ) and he1 , e2 i, corresponding
to the two products. The first one is eliminated using case analysis
(let(x, y) = e in e0 ), whereas the second one is eliminated using the
projections π i . The ! constructor boxes its argument, which can later
be unboxed with the form let !x = e in e0 . This constructor marks
where we need to scale the metric of a space. For concreteness we
will include real numbers k and a unit () value, and addition on real
numbers.
e ∈ E ::= x | k ∈ R | e1 + e2 | ()
| λx. e | e1 e2
| (e1 , e2 ) | let(x, y) = e in e0
| he1 , e2 i | πi e
| !e | let !x = e in e0
| inl e | inr e | (case e of inl x ⇒ el | inr y ⇒ er )
v ∈ V ::= k ∈ R | () | λx.e
| (v1 , v2 ) | hv1 , v2 i | !v | inl v | inr v
Figure 2. Syntax of Core Fuzz
Fuzz programs run under a standard call-by-value big-step
semantics. We write e ,→ v to say that term e evaluates to value v
(also a term). We omit the definition of this relation, which can be
found in the original paper [38].
The type system is more interesting. Terms are typed with
judgments of the form Γ ` e : σ, where Γ is a typing environment

and σ is a type. The complete definition is given in Figure 3. The type
system is inspired by bounded linear logic, with a few idiosyncratic
points. First, judgments track the sensitivity of each variable used in
a term. More precisely, a binding x :r σ in an environment Γ means
that the variable x has type σ under Γ and that terms typed under Γ
are r-sensitive with respect to x. Most rules use environment scaling
(rΓ) and addition (Γ + ∆) to track sensitivities. Note that the latter
operation is only defined when Γ and ∆ agree on the types of all
variable bindings.3 Second, an abstraction λx.e can only be typed if
e is 1-sensitive on x (cf. (( I)). Functions of different sensitivities
must take arguments in a scaled type !r σ and unwrap them using let
(cf. (!E)).
The Fuzz type system essentially corresponds to the constructions of last section, and can be interpreted in metric spaces in a
straightforward manner. Given a type σ, we define a metric space
JσK with the rules
JRK , R

Jσ ( τ K , Met(JσK, Jτ K)
Jσ & τ K , JσK & Jτ K

J1K , 1

Jσ ⊗ τ K , JσK ⊗ Jτ K
J!r σK , r · JσK.

Each environment Γ is interpreted as a tensor product, scaled by
the corresponding sensitivities:
J∅K , 1

JΓ, x :r σK , JΓK ⊗ (r · JσK)

We sometimes treat elements of JΓK as maps from variables in
Γ to elements of the denotations of their types. We can show by
a straightforward induction how this interpretation interacts with
scaling and addition.
Lemma 3.1. For every r and Γ, JrΓK = r · JΓK. For every Γ and
∆, if Γ + ∆ is defined, then the diagonal function δ(x) = (x, x) is
a non-expansive function JΓ + ∆K → JΓK ⊗ J∆K.

Finally, each typing derivation Γ ` e : σ yields a non-expansive
function JeK : JΓK → JσK by structural induction:
(Var) JxK(a) , a(x).
(Const) JkK , k.

(Plus) Je1 + e2 K , (+) ◦ (Je1 K ⊗ Je2 K) ◦ δ.

(1I) J()K , ? , where ? is the unique element of the singleton 1.
(( I) Jλx.eK , λJeK, where λ denotes currying.

(( E) Je1 e2 K ,  ◦ (Je1 K ⊗ Je2 K) ◦ δ, where  denotes function
application.

(⊗I) J(e1 , e2 )K , (Je1 K ⊗ Je2 K) ◦ δ.

(⊗E) Jlet(x, y) = e1 in e2 K , Je2 K ◦ (id ⊗ (r · Je1 K)) ◦ δ, where
r is the sensitivity of x and y in e2 .
(&I) Jhe1 , e2 iK , hJe1 K, Je2 Ki.
(&E) Jπ i eK , π i JeK.

(!I) J!eK , r · JeK, where r is the corresponding scaling factor.
(!E) Jlet !x = e1 in e2 K , Je2 K ◦ (id ⊗ (r · Je1 K)) ◦ δ.
(+Il ) Jinl eK , ι1 ◦ JeK.

(+Ir ) Jinr eK , ι2 ◦ JeK.

(+E) Jcase e of inl x ⇒ el | inr y ⇒ er K , [Jel K, Jer K]◦(r ·JeK),
where r is the sensitivity of x and y.
3 In the original paper [38], two environments Γ, ∆ can be added also when a
variable appears either only in Γ or only in ∆. For simplicity, here we require
instead all the variables to appear both in Γ and ∆. These are essentially
equivalent, since we can always assume that the sensitivity of a variable is 0.

r, s ∈ R∞
≥0

σ, τ ::= R | 1 | σ ( τ | σ ⊗ τ | σ & τ | σ + τ | !r σ

∆ = x1 :s1 σ 1 , . . . , xn :sn σ n
Γ = x1 :r1 σ 1 , . . . , xn :rn σ n
Γ + ∆ = x1 :r1 +s1 σ 1 , . . . , xn :rn +sn σ n

Γ = x1 :r1 σ 1 , . . . , xn :rn σ n
rΓ = x1 :r·r1 σ 1 , . . . , xn :r·rn σ n
(x :r σ) ∈ Γ
r≥1
Γ`x:σ
Γ, x :1 σ ` e : τ
Γ ` λx. e : σ ( τ

k∈R
Γ`k:R

(Var)

Γ ` e : σ1 ⊗ σ2
∆, x :r σ 1 , y :r σ 2 ` e0 : τ
rΓ + ∆ ` let(x, y) = e in e0 : τ
Γ`e:σ
rΓ ` !e : !r σ
Γ`e:σ
Γ ` inl e : σ + τ

(+Il )

(Const)

Γ ` e1 : R
∆ ` e2 : R
Γ + ∆ ` e1 + e2 : R

Γ ` e1 : σ ( τ
∆ ` e2 : σ
Γ + ∆ ` e1 e2 : τ

(( I)

(Plus)

(&I)

Γ ` e1 : ! s σ
∆, x :rs σ ` e2 : τ
rΓ + ∆ ` let !x = e1 in e2 : τ
(+Ir )

(1I)

Γ ` () : 1

Γ ` e1 : σ
∆ ` e2 : τ
Γ + ∆ ` (e1 , e2 ) : σ ⊗ τ

(( E)

Γ ` e1 : σ
Γ ` e2 : τ
Γ ` he1 , e2 i : σ & τ

(⊗E)

(!I)

Γ`e:τ
Γ ` inr e : σ + τ

Γ, ∆ ::= ∅ | Γ, x :r σ

(⊗I)

Γ ` e : σ1 & σ2
Γ ` πi e : σi

(&E)

(!E)

Γ ` e : σ1 + σ2
∆, x :r σ 1 ` el : τ
∆, y :r σ 2 ` er : τ
rΓ + ∆ ` case e of inl x ⇒ el | inr y ⇒ er : τ

(+E)

Figure 3. Core Fuzz Typing Rules
We will tacitly identify the denotation of typed closed terms
` e : σ with elements JeK ∈ JσK in what follows. We begin with the
following standard lemma, showing that the denotational semantics
behaves well with respect to weakening. As usual, the proof follows
by simple induction on the typing derivation.
Lemma 3.2 (Weakening). Let e be a typed term such that
Γ1 , Γ2 ` e : σ. For any other environment ∆, we have a derivation
Γ1 , ∆, Γ2 ` e : σ whose semantics is equal to JeK ◦ π Γ , where
π Γ : JΓ1 , ∆, Γ2 K → JΓ1 , Γ2 K discards all components corresponding to ∆.
To state a substitution lemma, we introduce some terminology
and notation. We define a substitution as a finite partial map from
variables to values,4 and use ~v to range over them. We write e[~v ] for
the simultaneous substitution of the values ~v (x) for the variables
x in e. We say that a substitution ~v is well-typed under Γ, written
~v : Γ, if for all types σ, ` ~v (x) : σ if and only if there exists r such
that (x :r σ) ∈ Γ. We can readily lift the semantics of terms to
substitutions by assigning well-typed substitutions to denotations
J~v K ∈ JΓK in the obvious way. Then:
Lemma 3.3 (Substitution). Let e be a well-typed term
Γ, ∆ ` e : σ,
and ~v : Γ be a well-typed substitution. Then, there is a derivation of
∆ ` e[~v ] : σ,
Furthermore, this derivation has semantics
Je[~v ]K = JeK(J~v K, −).

With this lemma, we can show:

Lemma 3.4 (Preservation). If ` e : σ and e ,→ v, then ` v : σ and
the semantics of both typing judgments are equal.
Together, the lemmas provide a short proof of metric preservation
for our simple fragment of Fuzz.
4A

similar result holds for the substitution of arbitrary expressions, but we
will not need this generality.

Theorem 3.5 (Metric Preservation). Suppose that we have a welltyped program
Γ ` e : σ,
and well-typed substitutions ~v : Γ and ~v 0 : Γ. Then, there are
well-typed values v and v 0 such that
e[~v ] ,→ v

and

e[~v 0 ] ,→ v 0 .

Furthermore,
dJσK (JvK, Jv 0 K) ≤ dJΓK (J~v K, J~v 0 K).

Proof. By Lemma 3.3, both e[~v ] and e[~v 0 ] have type σ under the
empty environment, and their denotations are equal to JeK(J~v K) and
JeK(J~v 0 K). By non-expansiveness of JeK,
dJσK (JeK(J~v K), JeK(J~v 0 K)) ≤ dJΓK (J~v K, J~v 0 K).

(1)

We can show by standard techniques that well-typed terms normalize, and thus we find values v and v 0 such that e[~v ] ,→ v and
e[~v 0 ] ,→ v 0 . By Lemma 3.4, both v and v 0 have type σ under the
empty environment, and their denotations are equal to those of e[~v ]
and e[~v 0 ]. Thus, (1) yields the desired result.

4.

Metric CPOs

While metric spaces suffice for the core fragment of Fuzz studied
so far, they lack the structure needed to model the full language
with non-terminating expressions and recursive types. To handle
these features, we will use the domain-theoretic notion of complete
partial order. We first review the basic theory of these structures,
and then show how to refine them into metric CPOs, which enable
sensitivity analysis in the presence of general recursion.
4.1

Preliminaries

Let (X, v ) be a poset (i.e., a set with a reflexive, transitive, and
anti-symmetric relation). We say that X is complete (or a CPO, for
short) if every ω-chain of elements of X
x0 v x1 v x2 v · · ·
F
has a least upper bound, denoted i xi . If X possesses a least
element ⊥ , we say that X is pointed.

A function f : X → Y between CPOs is monotone if x v x0
implies f (x) v f (x0 ); in particular, f maps ω-chains toFω-chains.

It is continuous if it preserves least upper bounds: f
i xi =
F
i f (xi ). Continuous functions between CPOs are the morphisms
of a category, CPO. Note that continuous functions also form a CPO
under the point-wise order f v g ⇔ ∀x.f (x) v g(x), with least
upper bounds of chains given by
!
G
G
fi (x) =
fi (x).
i

i

If the codomain is pointed, then the CPO is pointed as well, with
the constant function that returns ⊥ as the least element.
Continuous functions are useful because they allow us to interpret recursive definitions as fixed points.

4.2

Adding Metrics

In order to extend the sensitivity analysis of Section 2 on CPOs, we
seek to define a category of CPOs with metrics that is similar to Met
in structure. In particular, we would like non-expansive functions to
correspond to objects in this category, and to be closed under least
upper bounds so that they can form a CPO.
Let’s think about how this might hold. Suppose that we have an
ω-chain (fi )i∈N of non-expansive continuous functions X → Y ,
where both
F X and Y are CPOs endowed with metrics. To show that
the limit i fi is non-expansive, we must show that for any pair of
inputs x and x0 ,
!
G
G
d
fi (x), fi (x0 ) ≤ d(x, x0 ),
i

i
0

Theorem 4.1 (Kleene). Let X be a pointed CPO. Every continuous
function f : X → X has a least fixed point, given by
G i
fix(f ) =
f (⊥ ).
i

That is, fix(f ) = f (fix(f )), and fix(f ) v x for every x such that
x = f (x). The mapping f 7→ fix(f ) defines a continuous function
fix : CPO(X, X) → X.
We use CPOs to represent outcomes of a computation. Any
set X can be regarded as a CPO under the trivial discrete order
x v x0 ⇔ x = x0 . We use this order for sets of first-order values,
such as R or B. If X and Y are CPOs then so is X × Y , with
ordering
(x, y) v (x0 , y 0 ) ⇔ x v x0 ∧ y v y 0 ,
and the disjoint union X + Y , with ordering

assuming that d(fi (x), fi (x )) ≤ d(x, x0 ) for every i ∈ N. Unfortunately, this does not hold in general. For instance, let N∞ be
the CPO of natural numbers with the usual linear (not flat) order,
extended with a greatest element ∞. We can define a metric on the
disjoint union X = N∞ + N∞ by setting
(
1 if n = ∞
d(ι1 (n), ι2 (n)) =
0 otherwise,
and by stipulating that all other pairs of distinct points are infinitely
apart. Then, the functions fn : X → X (n ∈ N), defined by
fn (ιk (m)) , ιk (n),
are non-expansive and form an ω-chain, but do not satisfy the above
properties since at the limit we have
!
G
G
d
fn (ι1 (0)), fn (ι2 (0)) = d(ι1 (∞), ι2 (∞))
n

n

ιi (x) v ιj (x0 ) ⇔ i = j ∧ x v x0 .
These constructions, with the obvious projections and injections,
yield categorical products and sums in CPO. The singleton set 1 is a
terminal object in this category. Currying and uncurrying continuous
functions makes CPO a cartesian-closed category.
As it is typical, we represent computations that may run forever
with pointed CPOs of the form X⊥ , constructed by adjoining a
distinguished least element ⊥ to a CPO X. The copy of X in
X⊥ models computations that terminate successfully, whereas ⊥
models divergence. This construction extends to a functor on CPO
in the obvious way. This functor has the structure of a monad, where
the unit η : X → X⊥ injects X into X⊥ , and the multiplication
X⊥⊥ → X⊥ collapses the two bottom elements into a single
one. We write CPO⊥ for the Kleisli category of this monad. Its
morphisms are continuous functions X → Y⊥ , and composition of
two arrows g : Y → Z⊥ and f : X → Y⊥ is given by g † f , where
g † : Y⊥ → Z⊥ is the Kleisli lifting of g:
g † (⊥ ) =⊥
g † (y) = g(y)

if y 6= ⊥ .

Note that there is a natural transformation t : X⊥ × Y⊥ →
(X × Y )⊥ , corresponding to forcing a pair of computations:
(
(x, y) if x 6= ⊥ and y 6= ⊥
t(x, y) =
(2)
⊥
otherwise.
This, along with the unit η 1 : 1 → 1⊥ , makes (−)⊥ into a lax
symmetric monoidal functor. We use arrows in CPO⊥ to model
programs in a call-by-value discipline, which take fully computed
values as inputs and may either terminate or run forever.

= 1 6≤ d(ι1 (0), ι2 (0)).
So, we impose additional restrictions on the metrics we consider.
Definition 4.2. A pre-metric CPO is a CPO X endowed with a
metric. We say that X is a metric CPO if its metric is compatible
with the underlying partial order, in the following sense. Let r ∈
0
R∞
≥0 , and (xi )i∈N and (xi )i∈N be two ω-chains on X, such that
0
d(xi , xi ) ≤ r for all i. Then
!
G
G 0
d
xi , xi ≤ r.
i

i

Metric CPOs and continuous, non-expansive functions between
them form a category, which we call MetCPO.
All CPO constructions from the last section can be lifted to
metric CPOs.5 For instance, any discrete CPO with a metric is a
metric CPO. Another simple case is sums.
Lemma 4.3. If X and Y are metric CPOs, then so are X + Y and
X⊥ , under the sum metric of Section 2. Furthermore, X + Y and
the canonical injections give a coproduct on MetCPO.
Since ⊥ is infinitely apart from every other point, any morphism f : X → Y⊥ has the same termination behavior for any
pair of inputs that are at finite distance. Just as in the previous
section, we can extend (−)⊥ to a monad on MetCPO, yielding a
corresponding Kleisli category MetCPO⊥ representing potentially
non-terminating computations.
We can also lift the cartesian product on Met to MetCPO.
5 We will later see in Section 4.3 how to lift much of the structure of CPO
to MetCPO in a principled way, via a general fibrational construction.

Lemma 4.4. Let X and Y be metric CPOs. The product metric
X & Y , with the standard CPO structure over X × Y , is a metric
CPO. The projections π 1 : X & Y → X and π 2 : X & Y → Y are
non-expansive continuous functions, and make X & Y a cartesian
product in MetCPO.

of (2) is compatible with this metric, as well as the metric from
Lemma 4.4:

Dealing with the tensor product and its additive metric requires
more care. The following characterization of metric CPOs comes in
handy.

Morphisms of metric CPOs form a metric CPO, as shown in the
next result. As expected, currying and function application have a
similar than in Met.

Lemma 4.5. A pre-metric CPO X is a metric CPO if and only if
for every pair of ω-chains on X, (xi )i∈N and (x0i )i∈N , we have
!
G
G 0
d
xi , xi ≤ lim inf d(xi , x0i ).

Lemma 4.7. Let X and Y be metric CPOs. The set of morphisms
MetCPO(X, Y ) forms a metric CPO, inheriting its partial order from CPO(X, Y ) and its metric structure from Met(X, Y ).
The cartesian-closed structure of CPO induces an adjunction in
MetCPO:
(−) ⊗ X a MetCPO(X, −),
making it a symmetric monoidal closed category.

i

i

i

Proof. (⇒ ) Consider an arbitrary r > lim inf i d(xi , x0i ). There
exists an infinite set I ⊆ N such that
∀i ∈ I.d(xi , x0i ) ≤ r.
Since I is infinite, we get ω-chains (xi )i∈I and (x0i )i∈I , and because
X is a metric CPO, we find
!
!
G
G 0
G
G 0
d
xi ,
xi = d
xi ,
xi ≤ r.
i∈N

i∈I

i∈N

i∈I

Since r can be arbitrarily close to lim inf i d(xi , x0i ), we conclude
!
G
G 0
d
xi ,
xi ≤ lim inf d(xi , x0i ).
i∈N

i∈N

i∈N

(⇐ ) Suppose that
d

Proof. First, we must show that MetCPO(X, Y ) is a pre-metric
CPO, for which it suffices to show that it is closed under least
upper bounds. We can then conclude by showing that this structure
satisfies the metric CPO axiom. Showing that the monoidal structure
is closed is standard.
We prove both properties with the following auxiliary result.
Consider two chains (fi )i∈N and (gi )i∈N inFMetCPO(X, Y ),
Fand
two elements x1 , x2 ∈ X. Pose f = i fi and g = i gi .
Suppose that there exists r such that d(fi , gi ) ≤ r for every i ∈ N.
Since each fi and gi is non-expansive, we get d(fi (x1 ), gi (x2 )) ≤
r + d(x1 , x2 ) for every i ∈ N. We then conclude
!
G
G
d(f (x1 ), g(x2 )) = d
fi (x1 ), gi (x2 ) ≤ r + d(x1 , x2 ).
i

!
G

t : X⊥ ⊗ Y⊥ → (X ⊗ Y )⊥
t : X⊥ & Y⊥ → (X & Y )⊥ .

xi ,

i∈N

G
i∈N

x0i

≤ lim inf
i∈N

d(xi , x0i ).

Suppose furthermore that there exists r such that ∀i.d(xi , x0i ) ≤ r.
This implies lim inf i d(xi , x0i ) ≤ r, from which we conclude.
Lemma 4.6. Let X and Y be metric CPOs. The space X ⊗ Y is a
metric CPO over the standard product CPO.
Proof. We have to show that the above metric is compatible with the
order on X × Y . By Lemma 4.5, it suffices to show that for every
pair of ω-chains (pi )i∈N and (p0i )i∈N ,
!
G G 0
d
pi , pi ≤ lim inf d(pi , p0i ).
i

i

i

By definition, this is equivalent to
!
!
G
G 0
G G 0
d
xi , xi + d
yi , yi
i

i

i

i


≤ lim inf d(xi , x0i ) + d(yi , yi0 ) ,
i

where pi = (xi , yi ) and p0i = (x0i , yi0 ). Since X and Y are metric
CPOs, it suffices to show that
lim inf d(xi , x0i ) + lim inf d(yi , yi0 )
i
i

≤ lim inf d(xi , x0i ) + d(yi , yi0 ) ,
i

which always holds.
As before, this metric yields a symmetric monoidal category
(MetCPO, ⊗, 1) whose tensor unit is the terminal object. Note that
the forcing natural transformation t : X⊥ × Y⊥ → (X × Y )⊥

i

Now, we can see that MetCPO(X, Y ) is closed under least upper bounds by taking gi = fi and r = 0, since then d(f (x1 ), f (x2 )) ≤
d(x1 , x2 ). Furthermore, by setting x1 and x2 to the same value,
we find d(f (x1 ), g(x1 )) ≤ r + 0 and, since x1 is arbitrary, we
conclude d(f, g) ≤ r and that MetCPO(X, Y ) is indeed a metric
CPO.
Metric CPOs also support scaling.
Lemma 4.8. Let X be a metric CPO and r ∈ R∞
≥0 . Then r · X is
also a metric CPO, under the same order as X.
Proof. We just need to show that the new metric is compatible with
the CPO order. Suppose that we are given two chains on X, (xi ) and
(x0i ), and that there is r0 ∈ R∞
such that r·d(xi , x0i ) ≤ r0 for every
F≥0 F 0 
i; we must show that r · d i xi , i xi ≤ r0 . If r = 0 or r0 = ∞,
the inequality becomes trivial and we’reF
done. If
Fr 6∈{0, ∞}, then
d(xi , x0i ) ≤ r0 /r for every i, hence d i xi , i x0i ≤ r0 /r and
0
we’re done. The remaining case is when r = ∞ and
F r <F∞. Itmust
be the case that d(xi , x0i ) = 0 for every i, so d i xi , i x0i = 0
and we are done.
All the scaling identities of Section 2 remain valid, with the
addition of
r · X⊥ = (r · X)⊥ .
Similarly to Section 2, we have inclusions
MetCPO(X, Y ) ⊆ MetCPO(r · X, s · Y )
MetCPO⊥ (X, Y ) ⊆ MetCPO⊥ (r · X, s · Y )
whenever r ≥ s. Thus, scaling extends once again to a functor on
both categories.
Finally, we can interpret recursion by adding sensitivity information to the Kleene fixed-point combinator of Theorem 4.1:

Lemma 4.9. Let X be a pointed metric CPO, and r ∈ R∞
≥0 . The
fix combinator is a morphism s · MetCPO(r · X, X) → X, where
(
1
if r < 1
s = 1−r
∞
otherwise.
Proof. Let f and g be two morphisms r · X → X. We can show by
induction that
X

j
d(f i (⊥ ), g i (⊥ )) ≤
· d(f, g).
(3)
j<i r
Furthermore, when r < 1, we have
X
1 − ri
j
.
j<i r =
1−r
Therefore, the right-hand side of (3) is bounded by s · d(f, g) for
every i. Since X is a metric CPO, we find that d(fix(f ), fix(g)) ≤
s · d(f, g) and conclude.
4.3

Second, algebraic compactness also provides solutions to domain
equations given in terms of mixed-variance CPO-functors. More
precisely, suppose C is algebraically compact, and F : C ? → C is a
CPO-functor, where C ? , C op × C. Then we can find µF ∈ C and
an isomorphism
i : F (µF, µF ) ∼
(6)
= µF.
Such domain equations allow us to consider type operators involving exponentials C(−, −), which cannot be modeled directly as
covariant functors as was done for (4).
The following classic result provides useful sufficient conditions
for showing that MetCPO⊥ is algebraically compact.
Theorem 4.10 (Smyth and Plotkin [40]). Let C be a CPO-category
with a terminal object. Suppose that C(X, Y ) is pointed for every
X and Y , and that f ◦ ⊥ =⊥ for every f . Suppose furthermore
that C has colimits of ω-chains of embeddings; that is, of diagrams
of the form
X0

Domain Equations

Fuzz allows users to define data types recursively. To give a semantics to these types, we must solve the following problem: given
an operator F that maps types to types, find a type µF such that
F (µF ) ∼
= µF . The theory of algebraic compactness [24, 25, 40]
provides an elegant framework for studying these so called domain
equations. After a short review of this framework, we show how it
applies to MetCPO⊥ , preparing the way to model recursive types
in Fuzz in the next section.
Solutions to domain equations usually exploit existing CPO
structure on the arrows of a category. A CPO-category is a category
whose hom sets are CPOs and whose composition is continuous.
There are many examples of such categories, including CPO and
CPO⊥ , but also MetCPO and MetCPO⊥ by Lemma 4.7. Additionally, CPO-categories are closed under products and opposites:
in the first case, the order on arrows is just the product order, while
in the second one it is the same as in the original category.
We are interested in solving domain equations for type operators
F that can be extended to CPO-functors: these are functors between
CPO-categories whose action on morphisms is continuous. This
includes identity functors, constant functors, and the composition
of CPO-functors, as well as all the type operators that we have
considered in this section (&, ⊗, etc.). Thus, CPO-functors can
describe many recursive data types. For instance, the functor F :
MetCPO⊥ → MetCPO⊥ defined as
F (X) , 1 + R ⊗ X

(4)

is a CPO-functor, and the solution of the corresponding domain
equation is a metric CPO of lists of real numbers. By construction,
the distance between two lists of same length is the sum of the
distances of corresponding pairs of numbers, and lists of different
length are infinitely apart.
We say that a CPO-category C is algebraically compact if, for
every CPO-functor F : C → C, there exists an object µF and an
isomorphism
i : F (µF ) ∼
(5)
= µF
such that i is an initial algebra and i−1 is a final coalgebra. As usual,
this universal property of i translates into powerful induction and
coinduction principles [36] that characterize the solution µF up to
isomorphism. However, it does not play a major role in our analysis,
so we will not worry about it in what follows.
Two basic facts about algebraic compactness will be useful later
on. First, if C is algebraically compact and T is a finite set, then the
product C T is also algebraically compact. This allows us to describe
mutually recursive types as solutions to domain equations of the
form F (X1 , . . . , Xn ) ∼
= (X1 , . . . , Xn ).

X1

X2

···,

where every arrow e has an arrow e# such that e# e = id and
ee# v id. Then, C is algebraically compact.
Most of these conditions can be easily checked. (The terminal
object in MetCPO⊥ is the empty metric CPO 0.) The most difficult
one is showing that MetCPO⊥ has colimits of ω-chains of embeddings. For this purpose, we introduce a fibrational construction
that will let us lift colimits in CPO to MetCPO, where they can be
easily transferred to MetCPO⊥ . Later (Section 5), we will reuse
this machinery to show that the denotational semantics of Fuzz is
adequate.
Let F : E → D be a functor. The fiber category over an
object X ∈ D is the subcategory EX of E consisting of objects
and morphisms that are mapped to X and idX by F , respectively.
If A, B ∈ E, we write f : A ⊃ B to mean that there exists
f 0 : A → B such that f = F f 0 . We say that F is a CLat∧ fibration6 over D if it is a posetal fibration with fibered limits, or,
more explicitly, if it satisfies the following properties.
1. For each X ∈ D, the fiber category EX
T is a poset, and every
subset S ⊆ EX has a meet, denoted by S.
2. For each arrow f : X → Y in D and B ∈ EY , there is a element
f ∗ B ∈ EX (called the inverse image of B by f ) such that
g : A ⊃ f ∗B ⇔ f g : A ⊃ B
(7)
T ∗
∗ T
for all arrows g. Furthermore, f ( S) = {f B | B ∈ S}
for any set S ⊆ EX .
Intuitively, we use elements of EX to represent abstract predicates or relations over X, with the partial order of EX corresponding
to logical implication. We think of an arrow f : A ⊃ B as taking
elements related by A to elements related by B. Note that the above
properties imply that F is a faithful functor, and that each inverse
image f ∗ B is the unique element satisfying (7).
One example of CLat∧ -fibration is the canonical forgetful functor p : Met → Set. Each fiber MetX corresponds to the poset of
metrics on X, ordered by
d ≤ d0 ⇔ ∀x, x0 ∈ X.d(x, x0 ) ≥ d0 (x, x0 ).
Thus, the intersection of a family of metrics {di }i∈I on a set is
just their point-wise supremum (supi di )(x, y) = supi di (x, y),
and the inverse image of a metric d by a function f is given by
6 The

name CLat∧ -fibration stems from the fact that these structures
correspond uniquely (via the Grothendieck construction) to a functor Dop →
CLat∧ , where the codomain is the category of complete lattices and meetpreserving functions.

f ∗ d(x, y) = d(f (x), f (y)). In terms of the relational intuition
above, each metric d on X yields a family of relations {Rr }r∈ R∞
,
≥0
defined by (x, x0 ) ∈ Rr ⇔ d(x, x0 ) ≤ r. Non-expansiveness then
simply means that elements related at distance r are mapped to
elements related at distance r.
If D is also a CPO-category, it is useful to require more structure
of F . An object B ∈ E is called admissible [36, Definition 4.3] if
the image of E(A, B) under F is closed under limits of ω-chains
for every A. We say that F itself is admissible if every object in E
is admissible; this gives E a canonical structure of CPO-category.7
Alternatively, F is admissible if both E and D are CPO-categories
and F is a CPO-functor.
The following summarizes useful facts about CLat∧ -fibrations.

σ, τ ::= · · · | α ∈ T
Φ ::= (α 7→ Φ(α))α∈T
Γ ` e : Φ(α)
Γ ` fold e : α

(µI)

e ::= · · · | fold e | unfold e
v ::= · · · | fold v
Γ`e:α
Γ ` unfold e : Φ(α)

(µE)

Figure 4. Fuzz Recursive Types
MetCPO(X, Y ) such that e† = (m)⊥ . By composing the unit η
of the lifting monad, we conclude e = η Y ◦ m = Jm.
Theorem 4.15. The category MetCPO⊥ has colimits of ω-chains
of embeddings.

Lemma 4.11.
1. CLat∧ -fibrations preserve and create limits and colimits.
2. CLat∧ -fibrations are closed under products, opposites, and
pullbacks along any functor. The same conclusions hold for
admissible CLat∧ -fibrations over CPO-categories, restricting
pullbacks along CPO-functors.
3. Let D be a CPO-category, and F : E → D a CLat∧ -fibration.
Admissible objects of F are closed under inverse images and
intersections [36, Lemma 4.14]. In particular, restricting F to
the full subcategory Eadm of admissible objects of E yields an
admissible CLat∧ -fibration.
We want to use this result to compute colimits in MetCPO. To do
this, we characterize MetCPO as the full subcategory of admissible
objects of CPO ×Set Met, the category of pre-metric CPOs and nonexpansive, continuous functions. The latter arises as the following
pullback of functors, and r below is a CLat∧ -fibration:
CPO ×Set Met

Met
p

r

CPO

U

Set

Proposition 4.12. (CPO ×Set Met)adm = MetCPO.
Proof. Every metric CPO is admissible, by an argument analogous
to Lemma 4.7. To see the converse, we can observe that a pre-metric
CPO is a metric CPO if and only if the set of continuous, nonexpansive functions Br → X is closed under least upper bounds for
every r ∈ R∞
≥0 , where Br is the discrete metric CPO consisting of
two points at distance r.
Corollary 4.13. The forgetful functor q : MetCPO → CPO is an
admissible CLat∧ -fibration, and MetCPO is cocomplete.
Proof. By Lemma 4.11.
To conclude, we just need to show that ω-colimits of embeddings
in MetCPO⊥ can be transferred from MetCPO. The key observation is that every embedding is the image of a morphism by the
left adjoint J : MetCPO → MetCPO⊥ associated to the Kleisli
category.
Lemma 4.14. For any embedding e ∈ MetCPO⊥ (X, Y ), there
exists a unique morphism m ∈ MetCPO(X, Y ) such that e = Jm.
Proof. We write K for a right adjoint of J. Let e be an embedding in MetCPO⊥ (X, Y ). Since it is a split monomorphism,
Ke = e† ∈ MetCPO(X⊥ , Y⊥ ) is also a (split) monomorphism.
Moreover, Ke(⊥ ) =⊥ ; therefore, there exists a unique m ∈

Proof. From Lemma 4.14, every ω-chain (Xi , ei ) of embeddings
in MetCPO⊥ is the J-image of an ω-chain (Xi , mi ) in MetCPO.
Moreover, J preserves any colimit. Therefore the J-image of a
colimiting cone over (Xi , mi ), which exists by Corollary 4.13,
gives a colimiting cone over (Xi , ei ).
Having checked this result, we can apply Theorem 4.10 to show
that MetCPO⊥ is algebraically compact.

5.

Full Fuzz

Now, we are ready to model full Fuzz with recursive types (Figure 4).
We will extend the basic setup of Section 3 and prove a metric
preservation property analogous to Theorem 3.5.
The full Fuzz language is parameterized by a finite set T of type
identifiers, and a definition environment Φ mapping identifiers α to
type expressions Φ(α), which may themselves contain identifiers.8
Identifiers behave as iso-recursive types: programs can freely cast
between α and Φ(α) with the fold and unfold operators (cf. (µE)
and (µI)).
5.1

Adapting the Model

Ideally, we would like to extend the interpretation of types in
Section 3 by setting
JαK , JΦ(α)K.
(8)
Since Φ(α) is not smaller than α, this definition is not well-founded.
However, we can still give it a formal meaning by appealing to
algebraic compactness.
The first step, following Section 4.3, is to express the interpretation of recursive types as the solution of a system of domain
equations
∼ µFΦ ,
i : FΦ (µFΦ , µFΦ ) =
(9)
where FΦ : (MetCPO⊥ T )? → MetCPO⊥ T , and µFΦ ∈
MetCPO⊥ T maps each recursive type α to its interpretation
µFΦ (α). To define FΦ , we assign to each σ a mixed-variance
CPO-functor Fσ : (MetCPO⊥ T )? → MetCPO⊥ defined by
recursion on σ:
Fα (X, Y ) , Y (α)
Fσ(τ (X, Y ) , MetCPO⊥ (Fσ (Y, X), Fτ (X, Y ))
The other cases essentially follow the definition of J−K in Section 3,
and are omitted for brevity. We can now define
FΦ (X, Y )(α) , FΦ(α) (X, Y ).

7 The

terminology is reminiscent of Pitts’ work on relational properties of
domains [36]. In fact, CLat∧ -fibrations are closely related to his notion of
normal relational structure with inverse images and intersections.

8 This

is slightly different from the original presentation of Fuzz, which has
anonymous recursive types µα.σ instead of globally defined ones.

Since MetCPO⊥ is algebraically compact, so is MetCPO⊥ T ,
implying that a solution to (9) exists. With this solution in hand, we
can finally interpret types as
JσK , Fσ (µFΦ , µFΦ ).

All the equations describing the interpretation of types for Core
Fuzz carry over to this definition. Additionally, the isomorphism i
of (9) corresponds to a family of isomorphims
iα : JΦ(α)K ∼
= JαK,

which give recursive types their intended semantics.
Now that we know how to interpret types, we can proceed
with the rest of the semantics. The interpretation of environments
Γ remains the same: an iterated tensor product of scaled metric
CPOs. As before, we scale and split environments with an analog of
Lemma 3.1:
JrΓK = r · JΓK

Γ ` he1 , e2 i : σ & τ ,
given interpretations for both subterms, Je1 K : JΓK → JσK⊥ and
Je2 K : JΓK → Jτ K⊥ . We define Jhe1 , e2 iK as the composite
hJe1 K,Je2 Ki

JσK⊥ & Jτ K⊥

t

(JσK & Jτ K)⊥ ,

where t is the forcing morphism from (2). The interpretation of
other term constructors of Core Fuzz is adapted to this new setting
analogously. To conclude, we interpret fold and unfold using the
isomorphisms provided by algebraic compactness:
(µI) Jfold eK = iα ◦ JeK

(µE) Junfold eK = iα −1 ◦ JeK
5.2

k∈R

(a, v) ∈ F̂σ (A, B)

(k, k) ∈ F̂R (A, B)

(ι1 (a), inl v) ∈ F̂σ+τ (A, B)

(?, ()) ∈ F̂1 (A, B)

(ι2 (b), inr v) ∈ F̂σ+τ (A, B)

(b, v) ∈ F̂τ (A, B)

ffl ∈ {⊗, ×}

Metatheory

The basic properties of Core Fuzz (Lemmas 3.2 to 3.4) generalize
without difficulty to this new setting. As in other call-by-value
languages, we also obtain:
Lemma 5.1. Let ` v : σ be a value. Then JvK = η(x) for some
x ∈ JσK.

Thanks to this result, we can treat the denotation of a value
` v : σ as an element JvK ∈ JσK. These properties lead to our main
soundness result:
Theorem 5.2 (Metric Preservation). Suppose that we have a welltyped program
Γ ` e : σ,
and well-typed substitutions ~v : Γ and ~v 0 : Γ. Then
0

0

dJσK⊥ (Je[~v ]K, Je[~v ]K) ≤ dJΓK (J~v K, J~v K).

Unlike the previous statement of metric preservation, this result
doesn’t allow us to conclude anything about the termination behavior
of the programs e[~v ] and e[~v 0 ]. For that we need the following
property, which connects the domain-theoretic and operational views
of termination:
Lemma 5.3 (Adequacy). Let ` e : σ be a well-typed term. If
JeK 6= ⊥ , there exists a value ` v : σ such that e ,→ v.

Adequacy implies that programs e[~v ] and e[~v 0 ] in the statement
of Theorem 5.2 have the same termination behavior if dJΓK (~v , ~v 0 ) <

(a, va ) ∈ F̂σ (A, B)

(b, vb ) ∈ F̂τ (A, B)

((a, b), (va , vb )) ∈ F̂σfflτ (A, B)
∀(a, v) ∈ F̂σ (B, A).(f (a), e[x 7→ v]) ∈ F̂τ (A, B)⊥ (as in (12))
(f, λx.e) ∈ F̂σ(τ (A, B)

δ : JΓ + ∆K → JΓK ⊗ J∆K.

The biggest difference with respect to Core Fuzz is that the new
semantics is monadic, in order to accommodate the presence of
non-termination in a call-by-value discipline. Judgments Γ ` e : σ
now correspond to Kleisli arrows JeK : JΓK → JσK⊥ in MetCPO,
defined recursively by adapting the semantics of Section 3. For
instance, consider the rule (&I): we want to interpret a typed term

JΓK

F̂σ : (RelTV )? → RelV

(a, v) ∈ F̂σ (A, B)

(a, v) ∈ B(α)

(a, !v) ∈ F̂!σ (A, B)

(a, fold v) ∈ F̂α (A, B)

Figure 5. Relational lifting of the Fσ functors. We implicitly use
an object (X, P ) ∈ RelV to denote the relation P ⊆ X × V , so
that F̂σ (A, B) stands for a relation between Fσ (RT A, RT B) and
V.

∞. Indeed, supposing that the inputs are at finite distance, metric
preservation yields
dJσK⊥ (Je[~v ]K, Je[~v 0 ]K) < ∞.
Now, imagine that e[~v ] terminates in a value v. By preservation,
Je[~v ]K = JvK 6= ⊥ . This implies Je[~v 0 ]K 6= ⊥ , because
d(JvK, ⊥ ) = ∞. Finally, by adequacy, we find v 0 such that
e[~v 0 ] ,→ v 0 . The symmetric case follows similarly.
Following Plotkin [37], we prove Lemma 5.3 by constructing, for
each type σ, a logical relation Sσ ⊆ JσK × V such that if Γ ` e : σ,
~a ∈ JΓK, and ~v : Γ, then
(~a, ~v ) ∈ SΓ ⇒ (JeK(~a), e[~v ]) ∈ Sσ ⊥ ,

(10)

where
(~a, ~v ) ∈ SΓ ⇔ (∀(x :r τ ) ∈ Γ.(~a(x), ~v (x)) ∈ Sτ )
(a, e) ∈ Sσ

⊥

(11)

⇔ (a 6= ⊥ ⇒ ∃v.e ,→ v ∧ (a, v) ∈ Sσ ). (12)

Adequacy follows from (10) by instantiating Γ with the empty
environment. Our goal is to define Sσ so that (10) is strong enough
to be established by a simple induction on the typing derivation.
This almost completely determines how Sσ should be defined; it
must satisfy equations including
SR = {(k, k) | k ∈ R}
Sσ&τ = {((a, b), hva , vb i) | (a, va ) ∈ Sσ , (b, vb ) ∈ Sτ }
Sα = {(iα (a), fold v) | (a, v) ∈ SΦ(α) }.

(13)
(14)
(15)

Once again, we cannot define S by structural recursion, since (15)
expresses Sα in terms of SΦ(α) . To overcome this circularity, we use
a method due to Pitts [36, Theorem 4.16], originally stated in terms
of his relational structures and adapted here to CLat∧ -fibrations.
Theorem 5.4. Let D be algebraically compact, F : D? → D be a
CPO-functor, and G : E → D be an admissible CLat∧ -fibration.
Suppose we can lift F to E, in the sense that there exists a functor
F̂ : E ? → E such that the following diagram commutes:

F̂

E?
G?

D

?

showed how to type the call-by-value Y combinator in Fuzz as
follows:

E
G

F

Y : !∞ (!∞ (τ ( σ) ( τ ( σ) ( τ ( σ

D

Suppose furthermore that the hom sets of E and D are pointed, and
that G preserves these least elements. Then, we can construct µF̂ ∈
EµF such that µF̂ = (i−1 )∗ F̂ (µF̂ , µF̂ ), where i : F (µF, µF ) ∼
=
µF is the isomorphism given by algebraic compactness, as in (6).
Analogously to our interpretation of types, we will use F̂ to
express the logical relations Sα as the solution of fixed-point
equations, and then define the other logical relations Sσ in terms
of these solutions. To apply Theorem 5.4, we use the following
category RelV .
1. Objects are pairs (X, P ), where X is a metric CPO, and
P ⊆ X × V is a relation such that
!
G
(∀i.(xi , v) ∈ P ) ⇒
xi , v ∈ P,
(16)
i

for all ω-chains (xi ) in X and v ∈ V .
2. Arrows (X, P ) → (Y, Q) are continuous, non-expansive functions f : X → Y⊥ such that, whenever (x, v) ∈ P and
f (x) 6= ⊥ , we have (f (x), v) ∈ Q.
We let R denote the forgetful functor RelV → MetCPO⊥ ; this
results in an admissible CLat∧ -fibration. Intersections are given by
intersections of relations, and the inverse image of (X, P ) ∈ RelV
along f ∈ MetCPO⊥ (Y, X) is given by
f ∗ (X, P ) , (Y, {(x, v) | (f (x), v) ∈ P ∨ f (x) =⊥ }).
Furthermore, both MetCPO⊥ and RelV have pointed hom sets, and
R preserves least elements.
We build the logical relations (Sα ⊆ µFΦ (α) × V )α∈T by
building an object (µFΦ , Sα )α∈T in the fiber of RT over µFΦ ∈
MetCPO⊥ T . Since RT is also an admissible CLat∧ -fibration, we
just need to lift FΦ across RT and apply Theorem 5.4. It suffices to
find, for each type σ, a functor F̂σ : (RelTV )? → RelV such that
R ◦ F̂σ = Fσ ◦ RT ,

(17)

and then set F̂Φ (A, B)(α) , F̂Φ(α) (A, B); the complete definition
is in Figure 5. With the fixed point µF̂Φ , we can finally define the
logical relations Sσ as (the relation component of) F̂σ (µF̂Φ , µF̂Φ ).
With the definition in Figure 5, and the characterization of µF̂Φ in
Theorem 5.4, we can validate all the properties needed for proving
(10) (and thus Lemma 5.3) by induction, including (13) to (15).
Remark 5.5. Alternatively, we could have characterized RelV
reusing the machinery of Lemma 4.11, specifically by pulling back
SubCPO⊥ , the category of admissible subobjects of CPO⊥ , as
depicted below.
RelV
q⊥

CPO⊥

(−)×V

CPO⊥

In this diagram, by I × V we mean the coproduct of V -many
copies of I in CPO⊥ , which is inherited from CPO via the Kleisli
adjunction.
5.3

where α is a recursive type defined as !∞ α ( τ ( σ. (To
improve readability, we have elided the wrapping and unwrapping
of recursive and scaled types, and we use a derived let form.)
With this combinator, we can construct the fixed-point expression
fix f.e , Y (λf.e), and derive a corresponding typing rule.
Γ, f :∞ τ ( σ ` e : τ ( σ
∞Γ ` fix f.e : τ ( σ
This rule makes it possible to define functions of finite sensitivity
by recursion. It places little restrictions on how the recursive function
calls itself, since it allows the body e to be infinitely sensitive on f ;
however, it also requires scaling the typing environment by infinity.
Reed and Pierce [38] justified this by arguing that “we can’t [...]
establish any bound on how sensitive the overall function is from
just one call to it”.
Somewhat surprisingly, Lemma 4.9 allows us to define fixed
points directly on metric CPOs with a more precise sensitivity than
the one above. This suggests that we might be able to improve the
encoding of Y if we assume that its argument F is a finitely sensitive
function (i.e., if the body e is finitely sensitive on f ). After some
thought, we obtain
Yr : !1/(1−r) (!r (τ ( σ) ( τ ( σ) ( τ ( σ
Yr , λF. let f : αr = λf x.F (f f )x in f f,
where r < 1, and αr is now defined as !r/(1−r) αr ( τ ( σ. This
leads to the following typing rule:
Γ, f :r τ ( σ ` e : τ ( σ
r<1
1
Γ ` fixr f.e : τ ( σ
1−r
where fixr f.e , Yr (λf.e). We see that the scaling factor 1/(1 − r)
is unbounded as r approaches 1, when we recover the original rule.
One situation where this fixed point can be useful is for typing
functions where recursive calls are guarded by a scaling factor
smaller than 1. For instance, suppose that we define a type of lists
with exponentially decaying distances:
list τ , () + τ ⊗ !r list τ
If r < 1, we can type the map function with a finite sensitivity on
its function argument:
map : !1/(1−r) (τ ( σ) ( list τ ( list σ
map = λf.fixr m.λl.
case l of
| inl() ⇒ inl()

SubCPO⊥

R

MetCPO⊥

Y , λF. let f : α = λf x.F (f f )x in f f,

A Remark on Recursive Functions

Now that we have interpreted the full version of Fuzz, we show how
our semantics gives a different perspective on fixed points. Using a
standard encoding based on recursive types, Reed and Pierce [38]

| inr(x, l0 ) ⇒ inr(f x, ml0 )
This stands in contrast to the typical map function, which has
infinite sensitivity on its function argument. Exploring applications
of this new, more precise type for the fixed point is an intriguing
direction for future work.

6.

Related Work

Since the seminal works of Arnold and Nivat [5], and de Bakker and
Zucker [18], several authors have used metric spaces as a foundation
for denotational semantics. The technical motivations are often
similar to those for order-based structures, such as CPOs, since

the Banach fixed-point theorem yields a natural interpretation of
recursive functions and types.
A theme in many of these approaches is the use of ultrametric
spaces, where the triangle inequality is replaced with the stronger
variant
d(x, z) ≤ max(d(x, y), d(y, z)).
Typically, ultrametrics express that two objects (e.g., execution
traces, sets of terms, etc.) are equal up to a finite approximation:
the bigger the approximation, the closer the two objects are. For
instance, we can define an ultrametric on the set of sequences of
program states by posing d(~s1 , ~s2 ) = 2−c(~s1 ,~s2 ) , where c(~s1 , ~s2 )
is the length of the largest common prefix of ~s1 and ~s2 .
Ultrametrics on traces and trees appear in much of the earlier
work on the subject, where they can model language features such
as non-determinism and concurrency [4, 18, 32, 33]. (See van
Breugel [41] for a good introduction to the subject, and Baier
and Majster-Cederbaum [7], Majster-Cederbaum and Zetzsche [34]
for a comparison between the metric approaches and their orderbased counterparts.) A similar use of ultrametric spaces appears in a
denotational model of PCF given by Escardó [23], where the metric
structure describes intensional temporal aspects of PCF programs,
and its extensional collapse recovers the standard Scott model. Such
intensional uses contrast with our metric CPOs, where the metrics
describe mostly extensional aspects of programs.
A different use of ultrametrics emerged for modeling recursive
types in functional languages, starting with MacQueen et al. [31],
and continuing with Abadi and Plotkin [1], Abadi et al. [2], Amadio
[3]; see also Chroboczek [16] for a similar approach based on game
semantics. An interesting aspect of these models is that the metric
structure is often used in conjunction with the CPO structure. These
approaches have been extended recently to model more advanced
language features (e.g. references), providing a semantic framework
for investigating guardedness, step-indexing and Kripke possibleworld semantics. Works in this direction include those by Birkedal
et al. [10, 11, 12], Schwinghammer et al. [39]. In these works,
the metric structure expresses convergence properties that underlie
syntactic structures used in languages with guarded definitions, e.g.
Nakano’s recursion modality [35]. A similar approach has also been
used by Krishnaswami and Benton [30] in the context of reactive
and event-based programming, which models interactive programs
as operating on streams; stream functions are contractive maps in
their model. Our model differs from these works, e.g. contractivity
plays a different role and our requirement on the domain structure
is a sort of compatibility. However we plan to explore whether our
model can be used for similar goals in future work.
In a separate line of work, unrelated to ultrametrics, Kozen [29]
uses Banach lattices—a special kind of metric space—and nonexpansive linear operators between them to model probabilistic
programs. Spaces of subprobability distributions over a set of
values are modeled as Banach lattices. Although this is similar
in spirit to our use of metrics, there is still a crucial conceptual
difference: Kozen uses non-expansiveness to model the loss of mass
of a distribution as a program executes, due to the possibility of
non-termination. Indeed, he shows how non-expansiveness in this
setting corresponds to the usual monotonicity of domain-theoretic
functions.

7.

Conclusion

In this work we have introduced a domain-theoretic structure for
studying program sensitivity in higher-order languages with recursive types and non-termination. We have shown the effectiveness of
our approach by interpreting the deterministic fragment of Fuzz [38].
As future work, we plan to extend our approach to cover the probability monad of Fuzz. While metric interpretations of probabilities

are widespread in the programming-languages literature, e.g. [6, 19–
21, 29], we are not aware of any similar work that models the metric
of Reed and Pierce [38], used for reasoning about differential privacy. Interpreting this metric could also hint at how to interpret a
larger class of metric-like functions called f -divergences [17]. An
orthogonal direction is to study an interpretation of DFuzz [26], a
dependently typed version of Fuzz for proving differential privacy
for programs whose privacy depends on values provided at runtime.
This may require an extension of our framework to accommodate
their use of sized types.
Metric CPOs could also give meaning to the program analysis
studied by Chaudhuri et al. [14, 15]. Their notion of robustness
is analogous to the notion of sensitivity we consider in this paper.
However, their program analysis is based on previous work by the
same authors for analyzing program continuity [13]. Considering
restrictions or relaxations of metric CPOs for describing these
notions of continuity and robustness is also an interesting avenue
for future work.

Acknowledgments
We thank the anonymous reviewers for their detailed comments,
which improved earlier versions of this work. This work was partially supported by NSF grants TC-1065060, TWC-1513694, TWC1565365 and TWC-1513854, a grant from the Simons Foundation
(#360368 to Justin Hsu), and JSPS KAKENHI Grant Number
JP15K00014 (to Shin-ya Katsumata).

References
[1] M. Abadi and G. D. Plotkin. A PER model of polymorphism and
recursive types. In IEEE Symposium on Logic in Computer Science
(LICS), Philadelphia, Pennsylvania, pages 355–365, 1990.
[2] M. Abadi, B. C. Pierce, and G. D. Plotkin. Faithful ideal models
for recursive polymorphic types. In IEEE Symposium on Logic in
Computer Science (LICS), Asilomar, California, pages 216–225, 1989.
[3] R. M. Amadio. Recursion over realizability structures. Information
and Computation, 91(1):55–85, 1991.
[4] P. America and J. J. M. M. Rutten. Solving reflexive domain equations
in a category of complete metric spaces. In Workshop on the Mathematical Foundations of Programming Semantics (MFPS), New Orleans,
Louisiana, volume 298 of Lecture Notes in Computer Science, pages
254–288. Springer-Verlag, 1987.
[5] A. Arnold and M. Nivat. Metric interpretations of infinite trees
and semantics of non-deterministic recursive programs. Theoretical
Computer Science, 11(2):181–205, 1980.
[6] C. Baier and M. Z. Kwiatkowska. Domain equations for probabilistic
processes. Electronic Notes in Theoretical Computer Science, 7:34–54,
1997.
[7] C. Baier and M. E. Majster-Cederbaum. Denotational semantics in
the CPO and metric approach. Theoretical Computer Science, 135(2):
171–220, 1994.
[8] G. Barthe, B. Köpf, F. Olmedo, and S. Zanella Béguelin. Probabilistic
relational reasoning for differential privacy. In ACM SIGPLAN–
SIGACT Symposium on Principles of Programming Languages (POPL),
Philadelphia, Pennsylvania, pages 97–110, 2012.
[9] G. Barthe, M. Gaboardi, E. J. Gallego Arias, J. Hsu, A. Roth, and
P.-Y. Strub. Higher-order approximate relational refinement types
for mechanism design and differential privacy. In ACM SIGPLAN–
SIGACT Symposium on Principles of Programming Languages (POPL),
Mumbai, India, pages 55–68, 2015.
[10] L. Birkedal, K. Støvring, and J. Thamsborg. Realizability semantics
of parametric polymorphism, general references, and recursive types.
In International Conference on Foundations of Software Science and
Computation Structures (FoSSaCS), York, England, volume 5504 of
Lecture Notes in Computer Science, pages 456–470. Springer-Verlag,
2009.

[11] L. Birkedal, K. Støvring, and J. Thamsborg. The category-theoretic
solution of recursive metric-space equations. Theoretical Computer
Science, 411(47):4102–4122, 2010.
[12] L. Birkedal, R. E. Møgelberg, J. Schwinghammer, and K. Støvring.
First steps in synthetic guarded domain theory: Step-indexing in the
topos of trees. In IEEE Symposium on Logic in Computer Science
(LICS), Toronto, Ontario, pages 55–64, 2011.
[13] S. Chaudhuri, S. Gulwani, and R. Lublinerman. Continuity analysis
of programs. In ACM SIGPLAN–SIGACT Symposium on Principles of
Programming Languages (POPL), Madrid, Spain, pages 57–70, 2010.
[14] S. Chaudhuri, S. Gulwani, R. Lublinerman, and S. NavidPour. Proving
programs robust. In Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations
of Software Engineering (ESEC/FSE), Szeged, Hungary, pages 102–
112, 2011.
[15] S. Chaudhuri, S. Gulwani, and R. Lublinerman. Continuity and
robustness of programs. Communications of the ACM, 55(8):107–115,
2012.
[16] J. Chroboczek. Subtyping recursive games. In International Conference
on Typed Lambda Calculi and Applications (TLCA), Kraków, Poland,
volume 2044 of Lecture Notes in Computer Science, pages 61–75.
Springer-Verlag, 2001.
[17] I. Csiszr and P. C. Shields. Information theory and statistics: A tutorial.
Foundations and Trends in Communications and Information Theory, 1
(4):417–528, 2004.
[18] J. W. de Bakker and J. I. Zucker. Denotational semantics of concurrency.
In ACM SIGACT Symposium on Theory of Computing (STOC), San
Francisco, California, pages 153–158, 1982.
[19] E. P. de Vink and J. J. M. M. Rutten. Bisimulation for probabilistic
transition systems: A coalgebraic approach. Theoretical Computer
Science, 221(1–2):271–293, 1999.
[20] J. den Hartog, E. P. de Vink, and J. W. de Bakker. Metric semantics
and full abstractness for action refinement and probabilistic choice.
Electronic Notes in Theoretical Computer Science, 40:72–99, 2000.
[21] J. Desharnais, R. Jagadeesan, V. Gupta, and P. Panangaden. The
metric analogue of weak bisimulation for probabilistic processes. In
IEEE Symposium on Logic in Computer Science (LICS), Copenhagen,
Denmark, pages 413–422, 2002.
[22] C. Dwork, F. McSherry, K. Nissim, and A. D. Smith. Calibrating noise
to sensitivity in private data analysis. In IACR Theory of Cryptography
Conference (TCC), New York, New York, volume 3876 of Lecture Notes
in Computer Science, pages 265–284. Springer-Verlag, 2006.
[23] M. H. Escardó. A metric model of PCF, 1999. Workshop on
Realizability Semantics and Applications, Trento, Italy.
[24] M. P. Fiore and G. D. Plotkin. An axiomatization of computationally
adequate domain theoretic models of FPC. In IEEE Symposium on
Logic in Computer Science (LICS), Paris, France, pages 92–102, 1994.
[25] P. Freyd. Algebraically complete categories. In International Category
Theory Conference (CT), Como, Italy, volume 1488 of Lecture Notes
in Mathematics, pages 95–104. Springer-Verlag, 1990. ISBN 978-3540-46435-8.

[26] M. Gaboardi, A. Haeberlen, J. Hsu, A. Narayan, and B. C. Pierce.
Linear dependent types for differential privacy. In ACM SIGPLAN–
SIGACT Symposium on Principles of Programming Languages (POPL),
Rome, Italy, pages 357–370, 2013.
[27] A. Haeberlen, B. C. Pierce, and A. Narayan. Differential privacy under
fire. In USENIX Security Symposium, San Francisco, USA, 2011.
[28] D. Hofmann, G. J. Seal, and W. Tholen, editors. Monoidal Topology.
Cambridge University Press, 2014.
[29] D. Kozen. Semantics of probabilistic programs. Journal of Computer
and System Sciences, 22(3):328–350, 1981.
[30] N. R. Krishnaswami and N. Benton. Ultrametric semantics of reactive
programs. In IEEE Symposium on Logic in Computer Science (LICS),
Toronto, Ontario, pages 257–266, 2011.
[31] D. B. MacQueen, G. D. Plotkin, and R. Sethi. An ideal model for
recursive polymorphic types. In ACM Symposium on Principles of
Programming Languages (POPL), Salt Lake City, Utah, pages 165–
174, 1984.
[32] M. E. Majster-Cederbaum. On the uniqueness of fixed points of
endofunctors in a category of complete metric spaces. Information
Processing Letters, 29(6):277–281, 1988.
[33] M. E. Majster-Cederbaum and F. Zetzsche. Towards a foundation for
semantics in complete metric spaces. Information and Computation,
90(2):217–243, 1991.
[34] M. E. Majster-Cederbaum and F. Zetzsche. The comparison of a CPObased semantics with a CMS-based semantics for CSP. Theoretical
Computer Science, 124(1):1–40, 1994.
[35] H. Nakano. A modality for recursion. In IEEE Symposium on Logic in
Computer Science (LICS), Santa Barbara, California, pages 255–266,
2000.
[36] A. M. Pitts. Relational properties of domains. Information and
Computation, 127(2):66–90, 1996.
[37] G. Plotkin. Lectures on predomains and partial functions. Notes for a
course given at the Center for the Study of Language and Information,
Stanford, 1985.
[38] J. Reed and B. C. Pierce. Distance makes the types grow stronger:
A calculus for differential privacy. In ACM SIGPLAN International
Conference on Functional Programming (ICFP), Baltimore, Maryland,
pages 157–168, 2010. ISBN 978-1-60558-794-3.
[39] J. Schwinghammer, L. Birkedal, and K. Støvring. A step-indexed
Kripke model of hidden state via recursive properties on recursively
defined metric spaces. In International Conference on Foundations of
Software Science and Computation Structures (FoSSaCS), Saarbrücken,
Germany, volume 6604 of Lecture Notes in Computer Science, pages
305–319. Springer-Verlag, 2011.
[40] M. B. Smyth and G. D. Plotkin. The category-theoretic solution of
recursive domain equations. SIAM Journal on Computing, 11(4):761–
783, 1982.
[41] F. van Breugel. An introduction to metric semantics: operational and
denotational models for programming and specification languages.
Theoretical Computer Science, 258(1–2):1–98, 2001.

