A metric model of PCF

First version: 9 March 1998. This version: 7 October 1999.

Martín Hötzel Escardó

Laboratory for Foundations of Computer Science, The University of Edinburgh,

King’s Buildings, JMCB, Mayfield Road, Edinburgh EH9 3JZ, Scotland

      M.Escardo@ed.ac.uk     http://www.dcs.ed.ac.uk/home/mhe/

Abstract We introduce a computationally adequate metric model of PCF, based on the fact that the category of non-expansive maps of complete bounded ultrametric spaces is cartesian closed. The model captures certain temporal aspects of higher-type computation and contains both extensional and intensional functions. We show that Scott’s model arises as its extensional collapse. The intensional aspects of the metric model are illustrated via a Gödel-number-free version of Kleene’s T -predicate.

Keywords: Simply typed lambda-calculus, higher-type recursion theory, metric semantics.

MSC: 03B40, 03D65, 68Q55.

Sections 2, 3, 4 and 9 contain full proofs. Sections 6 and 8 contain enough details. Sections 5 and 7 contain proof sketches only, but no other section depends on them.

1 Introduction

Scott’s model of PCF is based on the introduction of bottom elements in the interpretation of ground types [14]. Conceptually, bottom stands for absence of information. This is made mathematically precise via the information order. Computationally, bottom stands for non-termination. The precise formulation of this statement is referred to as computational adequacy: A PCF program denotes a non-bottom value in Scott’s model if and only if it reduces to that value in finitely many computation steps [11].

Escardó

In practice, a value computed in a very large number of steps gets confused with non-termination. We introduce a metric model of PCF that captures some aspects of this situation. It is based on the fact that the category of non-expansive maps of complete bounded ultrametric spaces is cartesian closed [15]. The ground types are interpreted as metric spaces as follows. A point ∞ stands for non-termination. For each value v, a point v^{(k)} stands for v computed in k steps. The distance between points is defined in such a way that v^{(k)} gets close to ∞ as k increases. The interpretation of constants is defined in such a way that computational adequacy holds in the following form:

Theorem 1.1 A PCF program denotes a point v^{(k)} in the metric model if and only if it reduces to the value v in k computation steps.

If one were going to apply the metric model to develop a semantic approach to complexity theory, a careful analysis of what should count as a computation step in PCF would be needed. For the purposes of this paper, however, the precise way computation steps are counted is completely irrelevant. What is important is that the computation of a convergent program takes finitely many steps, and that the computation of a divergent program takes infinitely many steps.

We first consider a model that counts recursion unfoldings only. This is justified by the fact that the fragment of PCF without the fixed-point combinator is normalizing. Computational adequacy is easily proved via Kripke logical relations in a standard way, but one doesn’t need to consider the interpretation of the fixed-point combinator as a limit of approximations as in usual proofs of adequacy of Scott’s model. We then consider a more realistic interpretation that counts all “atomic reductions”. In this case the proof of computational adequacy is even simpler. Essentially, the denotational and the operational semantics are both fixed points of the same contractive functional on a complete metric space. Therefore, by Banach’s fixed-point theorem, they have to be the same. One can say that soundness implies completeness.

In the metric model one has both intensional and extensional functions. Roughly, a function is extensional if its value doesn’t depend on the time that its argument takes to be computed, and it is intensional if it does. Technically, extensionality is defined via a logical partial equivalence relation. All PCF-denotable functions are extensional. In order to be able to define intensional functions as well, we extend PCF with a Gödel-number-free version of Kleene’s T -predicate that tests whether the computation of a given term of ground type terminates within a given amount of time. Interesting intensional functions, such as fair-merge and McCarthy’s ambiguity operator, become denotable. Moreover, extensional functions that are not PCF-denotable, such as metric versions of Scott’s parallel-or [14] and Plotkin’s existential quantifier [11], become denotable too. Of course, the intensional information of the metric model can be removed by taking subquotients.

Theorem 1.2 Scott’s model is the extensional collapse of the metric model.

One can say that the metric model of PCF is intensional enough so that one can express Kleene’s T -predicate at a semantic level, but extensional enough so that computational mechanisms remain largely invisible. We haven’t investigated the following two natural questions: Is the metric model of PCF+ T fully abstract? Is PCF+ T universal for the metric model, with respect to suitable notions of effectively given ultrametric space and computable nonexpansive map?

Non-termination in PCF is silent. In order to gain a better understanding of the metric model, we also consider a variant of PCF in which nontermination is chattering. The PCF-denotable and chattering-PCF-denotable points coincide, but the operational semantics of chattering PCF explicitly manipulates the intensional information contained in the metric model.

Related work

The ACG (Amsterdam Concurrency Group) and their collaborators have successfully applied metric topology to the denotational semantics of concurrency [1]. In their introduction to the collection of selected ACG papers [3], de Bakker and Rutten say, in page 10,

“A recurring question posed to ACG members concerns the precise mathematical relationship between models based on complete metric spaces and the more familiar models based on complete partial orders.”

An answer to this question is given by de Bakker and Meyer [2]. In our case, a mathematical relationship between the metric and cpo models of PCF is given by Theorem 1.2, whose formulation is made precise by Theorems 7.3 and 7.1. They add that

“Subsidiary to this point, we are often asked what advantages we see in metric spaces as a tool over the—allegedly simpler—cpo’s.”

The main advantage of the metric approach that they mention is the usefulness of Banach’s unique-fixed-point theorem for complete metric spaces over Kleene’s least-fixed-point theorem for cpo’s. This is illustrated by Kok and Rutten [8], who prove that the denotational and operational semantics of certain languages coincide by showing that both are fixed-points of the same contractive functional on a complete metric space. We apply this technique in Section 8 to establish computational adequacy of a metric model of PCF. They continue by saying that

“In a purely functional setting (e.g. when modelling (un)typed lambda calculus), this argument does not apply: We certainly do not claim that the metric machinery has similar advantages over cpo theory to handle lambda models or related constructions.”

The present paper shows that this is an underestimation of the scope of the metric machinery. It is natural to ask whether metric models of the untyped lambda calculus also exist—we haven’t investigated this question. Regarding the generality of Kleene’s fixed-point theorem over Banach’s, they comment, in page 2,

“A simple, but not really convincing, way out is to postulate a silent step of some sort at each entry of a recursive call.”

Implicitly, this refers to the method applied by de Bakker and Zucker in their seminal paper [4, page 87] in order to ensure contractivity of a certain semantic map and hence applicability of Banach’s fixed-point theorem. Our metric interpretation of the fixed-point combinator is based precisely on this simple method, generalized to higher types—see Lemma 3.3. We hope that Theorem 1.1 makes this way out a bit more convincing. Computations do take place in time, and it may be desirable, on occasions, to distinguish short and long computations at a semantic level. Other convincing arguments are given by Theorem 7.1, which relates the metric and cpo interpretations of the fixed-point combinator, and by Theorem 5.3, which shows that our metric interpretation of the fixed-point combinator is extensional (see also Corollary 5.2).

2 Metric lifting

In order to obtain a metric model of PCF, we begin by considering a construction analogous to ordered lifting. For the purposes of this paper, it is enough to consider the metric lifting of a set. The lifting of a metric space is briefly discussed in Section 2.3 from a concrete point of view and in Section 2.4 from a conceptual point of view.

2.1 The metric lifting of a set

Notation 2.1 We denote by r an arbitrary but fixed number with 0 < r < 1, so that lim_{n} r^{n} = 0 in a non-trivial way.

The metric lifting of a set A is the set

L A = (A × ℕ) ∪ {∞}

endowed with the distance function d : L A × L A → [0, ∞) defined by

d(∞, ∞) = d(a^{(k)}, a^{(k)}) = 0, d(a^{(k)}, ∞) = d(∞, a^{(k)}) = r^{k},
d(a^{(k)}, b^{(l)}) = r^{min(k,l)} if a ≠ b or k ≠ l,

where a^{(k)} stands for ⟨a, k⟩. We regard the points of L A as “abstract computations” of elements of A. Specifically, we think of a^{(k)} as computation of a that converges in k steps, and of ∞ as a divergent computation.

Lemma 2.2 L A is a complete bounded ultrametric space.

Recall that a metric space is ultrametric if d(x, z) ≤ max(d(x, y), d(y, z)).

Proof. We give an indirect proof that gives some insight on the nature of the metric—see Section 9. We think of a^{(k)} as the sequence ♭^{k}a^{ω}, and of ∞ as the sequence ♭^{ω}, where ♭ is a “blank symbol”. Define a family =_{n} of equivalence relations on L A by x =_{n} y iff x_{i} = y_{i} for all i < n, where we interpret x, y ∈ L A as sequences as above. It is easy to see that d(x, y) = inf{r^{n}|x =_{n} y}. For x ≠ y, this says that d(x, y) = r^{n} where n is the least integer with x_{n} ≠ y_{n}. It is well-known that this construction via equivalence relations produces a bounded ultrametric space [15, page 703, Example 3(a)]. Essentially, the reason is that the ultrametric property coincides with transitivity of the relation d(x, y) ≤ ϵ, for each fixed ϵ [15, page 717, Proposition 6.4.6]. Moreover, it is easy to see that L A is complete, with all points isolated, except ∞. □

For any isolated point x of any metric space, there is a smallest ϵ > 0 such that the open ball B_{ϵ}(x) is {x}, that is, such that d(x, y) < ϵ implies x = y. For x = v^{(k)}, it is easy to see that the corresponding ϵ is r^{k}. Notice that, as a topological space, L ℕ is not homeomorphic to the one-point compactification of the discrete space of natural numbers. In fact, since d(∞, n^{(0)}) = 1, the open ball B_{1}(∞) is {n^{(k+1)}|n, k ∈ ℕ} ∪ {∞} and has {n^{(0)}|n ∈ ℕ} as its complement. This also shows L ℕ is not compact, as the complement consists of countably many isolated points.

Recall that a map f : X → Y of metric spaces is non-expansive if

d(f(x), f(x′)) ≤ d(x, x′).

If one interprets the assertion that x and x′ are close as saying that it is difficult to distinguish x and x′ by observing their computations, then computable maps have to be non-expansive: distinguishing f(x) from f(x′) is at least as computationally hard as distinguishing x from x′.

Lemma 2.3 For every function f : A → B there is a non-expansive map L f : L A → L B defined by

L f(a^{(k)}) = f(a)^{(k)}, L f(∞) = ∞.

Proof. If x = y then d(L f(x), L f(y)) = 0 = d(x, y). If x = a^{(k)} and y = ∞ then d(L f(x), L f(y)) = d(f(a)^{(k)}, ∞) = r^{k} = d(x, y). Finally, if x = a^{(k)} and y = b^{(l)} with a ≠ b or k ≠ l, then d(L f(x), L f(y)) = d(f(a)^{(k)}, f(b)^{(l)}) ≤ r^{min(k,l)} = d(x, y). □

It follows that L is a functor from the category of sets to the category of non-expansive maps of complete bounded ultrametric spaces.

2.2 Delay operators

For each set A define a “delay operator” δ_{A} : L A → L A and an “inclusion” η_{A} : A → L A by

δ_{A}(a^{(n)}) = a^{(n+1)},  δ_{A}(∞) = ∞,  η_{A}(a) = a^{(0)}.

The idea is that, for a convergent computation x ∈ L A, we have that x and δ(x) compute the same element of A, but the computation δ(x) takes longer than the computation x. This is made precise in Section 7 via the use of partial equivalence relations.

It is clear that every point of L A is either ∞ or else of the form δ^{n}(η(a)) for unique n and a. The following proposition is easily proved:

Proposition 2.4 The metric on L A is uniquely determined by the equations

d(∞, ∞) = d(η(a), η(a)) = 0,  d(η(a), η(b)) = 1  if a ≠ b,
d(η(a), δ(x)) = d(δ(x), η(a)) = 1, d(δ(x), δ(y)) = r · d(x, y).

2.3 The metric lifting of a metric space

In this subsection, which is not needed in the development that follows, we discuss the generalization of metric lifting from sets to metric spaces.

The functor L can be extended to an endofunctor of the category of nonexpansive maps of complete 1-bounded ultrametric spaces by defining

d(∞, ∞) = 0, d(x^{(k)}, ∞) = d(∞, x^{(k)}) = r^{k},
d(x^{(k)}, y^{(k)}) = r^{k}d(x, y), d(x^{(k)}, y^{(l)}) = r^{min(k,l)} for k ≠ l.

Moreover, we then have a monad with unit and multiplication given by

η_{X}(x) = x^{(0)}, μ_{X} ((x^{(n)})^{(m)}) = x^{(m+n)}.

The metric lifting monad is easily seen to be computational in the sense of Moggi [10]. This fact can be used to tackle call-by-value PCF. In this paper we are considering call-by-name PCF as in [11] and we don’t need the monad structure of the metric lifting functor.

2.4 A conceptual account of metric lifting

A conceptual construction of metric lifting is discussed by Daniele Turi and the author in [6]. We have shown that L is the free monad over the endofunctor Δ defined by

ΔX = X,  d_{ΔX}(x, y) = r · d_{X}(x, y),  Δf = f.

Explicitly, L X is the initial algebra of the functor F Y = X + ΔY. From this one concludes that the Eilenberg-Moore algebras of the monad L are in bijection with the algebras of the functor Δ. In order to obtain a concrete description of the bijection, we consider the natural map id_{r} : X → ΔX which is the identity on points. It is easy to see that a map f : X → Y is r-contractive iff it factors through id_{r} : X → ΔX. By a slight abuse of notation, we denote the unique factor by f : ΔX → Y. Thus, the Δ-algebras are essentially the r-contractive endomaps. The bijection takes an algebra α : ΔX → X to the Eilenberg-Moore algebra \overline{α} : L X → X defined by

\overline{α}(x^{(k)}) = α^{k}(x), \overline{α}(∞) = the unique fixed point of α.

Then the delay operator defined above arises from the bijection as the unique map with

μ_{X} = \overline{δ_{X}}.

Thus, structure maps of L-algebras correspond to generalized delay operators.

We remark that, as a set, L X also appears in the work of Rutten [13] on the analysis of while-programs by coinduction, as the final coalgebra of the endofunctor F Y = X + Y of the category of sets.

3 A metric model of PCF

The following folklore result is proved in [15], where some useful full subcategories that don’t arise in this paper are also considered:

Lemma 3.1 The category of non-expansive maps of complete bounded ultrametric spaces is cartesian closed.

For the purposes of this paper it is enough to know that the points of a cartesian product are the pairs of points and that the points of an exponential are the non-expansive maps, with distance defined by

d_{X×Y} (⟨x_{1}, y_{1}⟩, ⟨x_{2}, y_{2}⟩) = max(d_{X}(x_{1}, x_{2}), d_{Y} (y_{1}, y_{2})),
d_{X→Y} (f, g) = sup{d_{Y} (f(x), g(x)) | x ∈ X}.

In later sections we use the fact that limits in function spaces are computed pointwise.

The metric interpretation of PCF is defined as follows. First, the interpretation of types is inductively defined by

X_{o} = L 𝔹,  X_{ι} = L ℕ,  X_{σ→τ} = (X_{σ} → X_{τ}),

where 𝔹 = {true, false} and (X_{σ} → X_{τ}) is the function space constructed in Lemma 3.1. Then constants are interpreted as in Fig. 1, and lambdaabstraction and application are interpreted in the usual way, via the (wellpointed) cartesian-closed structure of our base category using environments. It is easy to check that the interpretation of the conditional is non-expansive and hence well-defined.

⟦v⟧ = η(v)  for every value v = false, true, 0, 1, 2, …, n, …
⟦succ⟧ = L(n ↦ n + 1)
⟦pred⟧ = L(0 ↦ 0, n + 1 ↦ n)
⟦zero⟧ = L(0 ↦ true, n + 1 ↦ false)

⟦if⟧(x)(y)(z) = \{ \begin{matrix}δ^{k}(y) & if x is of the form true^{(k)} \\ δ^{k}(z) & if x is of the form false^{(k)} \\ ∞ & otherwise \end{matrix}

⟦Y_{σ}⟧ = fix_{σ} as constructed in Lemma 3.3

Fig. 1. A metric interpretation of PCF

In order to define a fixed-point operator fix_{σ} : (X_{σ} → X_{σ}) → X_{σ}, we first inductively define δ_{σ} : X_{σ} → X_{σ} by

δ_{o} = δ_{𝔹},  δ_{ι} = δ_{ℕ},  δ_{σ→τ}(f)(x) = δ_{τ}(f(x)).

Recall that a map f of metric spaces is contractive if there is a non-negative constant c < 1, called a contractivity factor of f, with

d(f(x), f(y)) ≤ c · d(x, y).

Lemma 3.2 δ_{σ} : X_{σ} → X_{σ} is a contractive map for each type σ.

Proof. We show by induction on σ that d_{σ}(δ_{σ}(x), δ_{σ}(y)) = r · d_{σ}(x, y). The base case is given by Proposition 2.4. By definition of the metric on function spaces,

d_{σ→τ}(δ_{σ_{→}τ}(f), δ_{σ→τ}(g)) = sup{d_{τ}(δ_{σ_{→}τ}(f)(x), δ_{σ_{→}τ}(g)(x)) | x ∈ X_{σ}}.

By definition of δ_{σ→τ} and by the induction hypothesis, the last term is equal to

sup{d_{τ}(δ_{τ}(f(x)), δ_{τ}(g(x))) | x ∈ X_{σ}} = sup{r · d_{τ}(f(x), g(x)) | x ∈ X_{σ}}.

Finally, the last term is equal to r·sup{d_{τ}(f(x), g(x)) | x ∈ X_{σ}} = r·d_{σ→τ}(f, g) by the fact that multiplication by r preserves suprema and by definition of the metric on function spaces. □

Banach’s fixed-point theorem says that every contractive endomap f : X → X of a non-empty complete metric space X has a unique fixed point, given by lim_{n} f^{n}(x_{0}), where x_{0} is an arbitrary point of X. It is clear that if g : X → X is contractive and f : X → X is non-expansive then the composite map g∘f is contractive. Therefore, for every non-expansive map f : X_{σ} → X_{σ}, the map δ_{σ} ∘f has a unique fixed point.

Lemma 3.3 The map fix_{σ} : (X_{σ} → X_{σ}) → X_{σ} that sends f to the unique fixed point of δ_{σ} ∘f is non-expansive.

Proof. Let Y_{σ} = (X_{σ} → X_{σ}) → X_{σ} and define a functional Φ_{σ} : Y_{σ} → Y_{σ} by Φ(F)(f) = δ_{σ} ∘f(F (f)). Then

d(Φ(F), Φ(G)) = sup{d(δ_{σ}(f(F (f))), δ_{σ}(f(G(f))))|f ∈ (X_{σ} → X_{σ})}

by definition of the metric on function spaces. By Lemma 3.2 and the fact that f is non-expansive, we have that

d(δ_{σ}(f(F (f))), δ_{σ}(f(G(f)))) ≤ c · d(f(F (f)), f(G(f))) ≤ c · d(F (f), G(f)),

where c is a contractivity factor of δ_{σ}. By definition of the metric on function spaces, the fact that taking suprema is a monotone operation, and the fact that multiplication by a non-negative number preserves suprema, we conclude that d(Φ(F), Φ(G)) ≤ c·d(F, G) and hence that Φ is contractive. By Banach’s fixed-point theorem, Φ has a unique fixed point, say F. By construction, for any f ∈ (X_{σ} → X_{σ}), one has that F (f) is a fixed point of δ_{σ} ∘f. This shows that fix_{σ} = F and hence that fix_{σ} ∈ Y_{σ}, which is equivalent to saying that fix_{σ} is non-expansive. □

4 Computational adequacy

The metric interpretation matches the operational semantics in the following way, where M ⇓^{k} v means that the program M evaluates to the value v in finitely many computation steps, k of which are recursion unfoldings:

Theorem 4.1 If M is a PCF program then ⟦M⟧ = v^{(k)} if and only if M ⇓^{k} v.

Recall that a program is a closed term of ground type. Formally, a relation M ⇓^{k} v, where M is a closed term of arbitrary type, can be obtained by decorating the standard inductive definition of the “big-step” evaluation relation of PCF with a superscript as in Fig. 2. It is clear that M ⇓ v if and only if M ⇓^{k} v for some (necessarily unique) k. Therefore, the metric denotation of a program M is of the form v^{(k)} if and only if M ⇓ v.

Here, with or without the superscripts, one has to regard the constants as constructors [7]. For example, “if true” is not a well-formed PCF term, but “λx.λy. if true x y” is. Notice however that, in order to avoid unnecessary syntactical complications, we have defined the metric semantic function by regarding constants as terms. We hope that this causes no confusion.

In order to prove the theorem, we split its statement into two parts, soundness and completeness, generalizing them to higher types in order to obtain

(Val) v ⇓^{0} v  if v is false, true, 0, 1, …, n, …, λα.M,
(Succ) \frac{M ⇓^{k} n}{succ M ⇓^{k} (n + 1)}

(Pred) \frac{M ⇓^{k} 0}{pred M ⇓^{k} 0}  \frac{M ⇓^{k} (n + 1)}{pred M ⇓^{k} n}

(Zero) \frac{M ⇓^{k} 0}{zero M ⇓^{k} true}  \frac{M ⇓^{k} (n + 1)}{zero M ⇓^{k} false}

(Cond) \frac{L ⇓^{k} true M ⇓^{l} v}{if LMN ⇓^{k+l} v}  \frac{L ⇓^{k} false N ⇓^{l} v}{if LMN ⇓^{k+l} v}

(Fix) \frac{M(Y_{σ} M) ⇓^{k} v}{Y_{σ} M ⇓^{k+1} v}

(Appl) \frac{M ⇓^{k} (λx.L) L[N/x] ⇓^{l} v}{MN ⇓^{k+l} v}

Fig. 2. A temporal operational semantics of PCF

suitable induction hypotheses. In the case of soundness, the generalization is easy:

Lemma 4.2 For every closed term M : σ, if M ⇓^{k} v then ⟦M⟧ = δ_{σ}^{k}⟦v⟧.

Proof. By induction on the definition of the evaluation relation. The base case (Val) is trivial. Out of the rules (Succ), (Pred), (Zero) and (Cond), we consider (Cond) as a representative example. Assume that L ⇓^{k} true and M ⇓^{l} v, and hence that if LMN ⇓^{k+l} v by virtue of the left-hand rule (Cond). By the induction hypothesis, ⟦L⟧ = δ^{k}⟦true⟧ and ⟦M⟧ = δ^{l}⟦v⟧. Hence ⟦if LMN⟧ = δ^{k+l}⟦v⟧ by definition of ⟦if⟧. The right-hand rule is handled symmetrically. Now assume that M(Y M) ⇓^{k} v and hence that Y M ⇓^{k+1} v by virtue of rule (Fix). By the induction hypothesis, ⟦M(Y M)⟧ = δ^{k}⟦v⟧. But, by definition of ⟦Y⟧, we have that ⟦Y M⟧ = δ⟦M(Y M)⟧ = δ(δ^{k}⟦v⟧) = δ^{k+1}⟦v⟧, as required. Finally, assume that M ⇓_{σ→τ}^{k} λx.L and L[N/x] ⇓_{τ}^{k} v, and hence that MN ⇓_{τ}^{k+l} v by rule (Appl). By the induction hypothesis, ⟦M⟧ = δ_{σ→τ}^{k}⟦λx.L⟧ and ⟦L[N/x]⟧ = δ_{τ}^{l}⟦v⟧. It follows that ⟦MN⟧ = ⟦M⟧⟦N⟧ = δ_{σ→τ}^{k}⟦λx.L⟧⟦N⟧ = δ_{τ}^{k}(⟦λx.L⟧⟦N⟧) = δ_{τ}^{k}⟦(λx.L)N⟧ = δ_{τ}^{k}⟦L[N/x]⟧ = δ_{τ}^{k}(δ_{τ}^{l}⟦v⟧) = δ_{τ}^{k+l}⟦v⟧, as required. □

In order to establish completeness, we inductively define a reducibility property of closed terms as follows:

• A program M is n-reducible iff for every k ≤ n, ⟦M⟧ = v^{(k)} implies M ⇓^{k} v.

• A closed term M : σ → τ is n-reducible iff for every k ≤ n, the term MN : τ

is k-reducible whenever N : σ is a k-reducible closed term.

• A closed term is reducible iff it is n-reducible for every n.

Notice that if a term is n-reducible then it is k-reducible for every k ≤ n. Thus, reducibility is a Kripke logical property of closed terms. In order to show that the fixed-point combinator is reducible, we need a lemma.

Lemma 4.3 For every type σ = τ_{1} → ⋯ → τ_{m} → γ, every natural number l ≤ m, every term M : σ → σ and all terms N_{i} : τ_{i} with 1 ≤ i ≤ l, the following derived rule holds:

\frac{M(Y_{σ} M)N_{1} … N_{l} ⇓^{k} v}{Y_{σ} MN_{1} … N_{l} ⇓^{k+1} v} .

Proof. By induction on l. The base case is just rule (Fix). For the induction step, assume that the claim holds for l < m and that M(Y_{σ} M)N_{1} … N_{l}N_{l+1} ⇓^{k} v. Since l < m, the term M(Y_{σ} M)N_{1} … N_{l} has a functional type. It follows that the only rule that allows such an evaluation is (Appl). Hence M(Y_{σ} M)N_{1} … N_{l} ⇓^{l} λx.L and L[N_{l+1}/x] ⇓^{m} v with l + m = k. By the induction hypothesis, Y_{σ} MN_{1} … N_{l} ⇓^{l+1} λx.L. Hence, by rule (Appl), we have that Y_{σ} MN_{1} … N_{l}N_{l+1} ⇓^{l+1+m} v, as required. □

Lemma 4.4 Every closed term is reducible.

Proof. By the logical-relations lemma, it suffices to show that every constant is reducible. The first-order constants are trivially reducible. We consider succ as an example. Let n and k ≤ n be natural numbers, let M : ι be a reducible closed term, and assume that ⟦succ M⟧ = v^{(k)}. By the assumption, v > 0 and ⟦M⟧ = (v − 1)^{(k)}. By reducibility of M, we conclude that M ⇓^{k} v − 1. Finally, by rule (Succ), we conclude that succ M ⇓^{k} v, which shows that succ is n-reducible for every n, and hence that it is reducible. We show that Y_{σ} is n-reducible for every n by induction on n. First, recall that every type σ can be uniquely written in the form τ⃗ → γ (a shorthand for the iterated function type τ_{1} → ⋯ → τ_{m} → γ) with γ ground. Also, it is enough to show that, for all k ≤ n, the term Y_{σ}MN⃗ : γ is k-reducible whenever M : σ → σ and N⃗ : τ⃗ are k-reducible terms. The base case of the induction holds vacuously because ⟦Y_{σ}MN⃗⟧ = v^{(0)} is impossible as ⟦Y_{σ}MN⃗⟧ = δ_{γ}⟦M(Y_{σ}M)N⃗⟧. Assume that Y_{σ} is n-reducible. In order to show that it follows that Y_{σ} is (n + 1)- reducible, let M : σ → σ and N⃗ : τ⃗ be k-reducible terms, for k ≤ n + 1, and suppose that ⟦Y_{σ}MN⃗⟧ = v^{(k)}. Since ⟦Y_{σ}MN⃗⟧ = δ_{γ}⟦M(Y_{σ}M)N⃗⟧, it follows that k > 0 and ⟦M(Y_{σ}M)N⃗⟧ = v^{(k−1)}. Since k − 1 ≤ n, and M(Y_{σ}M)N⃗ is (k−1)-reducible, M(Y_{σ}M)N⃗ ⇓^{k−1} v. By Lemma 4.3, it follows that Y_{σ}MN⃗ ⇓^{k} v, and hence that Y_{σ}MN⃗ is k-reducible. Therefore Y_{σ} is (n + 1)-reducible. □

5 Extensional points of the metric model

We endow the metric space X_{γ}, for γ ground, with the least (total) equivalence relation ≈_{γ} such that

v^{(k)} ≈_{γ} v^{(l)},

and the metric space X_{σ→τ} with the “logically” induced partial equivalence relation ≈_{σ→τ}:

f ≈_{σ→τ} g iff f(x) ≈_{τ} g(y) whenever x ≈_{σ} y.

We say that two points x, y ∈ X_{σ} are extensionally equivalent if x ≈_{σ} y, and we say that a point of X_{σ} is extensional if it is extensionally equivalent to itself; otherwise, we say that the point is intensional. Explicitly, all ground points are extensional, and a function f ∈ X_{σ→τ} is extensional iff fx ≈_{τ} fy whenever x ≈_{σ} y. In particular, extensional functions map extensional points to extensional points.

The sets of extensional points of functional types are not closed. For example, consider id_{n} : X_{ι} → X_{ι} defined by

id_{n}(v^{(0)}) = v^{(0)},  id_{n}(v^{(k+1)}) = v^{(k+1+n)},  id_{n}(∞) = ∞.

It is easy to see that this is a Cauchy sequence of non-expansive maps. Moreover, id_{n} ≈ id. Let id_{∞} be the limit of the sequence. Since limits of nonexpansive maps are computed pointwise, one has that v^{(k+1)} ≈ v^{(0)} but that

id_{∞}(v^{(k+1)}) = lim_{n} v^{(k+1+n)} = ∞ ≉ v^{(0)} = id_{∞}(v^{(0)})

so that id_{∞} is intensional.

However, we can show that extensional points are closed under limits of increasing Cauchy sequences, for a suitably (hereditarily) defined partial order, for which extensional non-expansive maps are monotone. Using this one can prove:

Lemma 5.1 The fixed points of two extensionally equivalent contractive endomaps are extensionally equivalent.

In particular, the fixed point of an extensional contractive endomap is extensional.

Corollary 5.2 If f ∈ X_{σ→σ} is an extensional contractive endomap, then its unique fixed point is extensionally equivalent to fix_{σ}(f).

Proof. Since id_{σ} ≈ δ_{σ} and f ≈ f, we have that f ≈ δ_{σ} ∘ f. □

Theorem 5.3 All PCF-denotable points of the metric model are extensional.

(SPZ) \frac{M ⇑^{k}}{succ M ⇑^{k}}  \frac{M ⇑^{k}}{pred M ⇑^{k}}  \frac{M ⇑^{k}}{zero M ⇑^{k}}

(Cond) \frac{L ⇓^{k} true M ⇑^{l}}{if LMN ⇑^{k+l}}  \frac{L ⇓^{k} false N ⇑^{l}}{if LMN ⇑^{k+l}}  \frac{L ⇑^{k}}{if LMN ⇑^{k}}

(Fix) \frac{M(Y_{σ} M) ⇑^{k}}{Y_{σ} M ⇑^{k+1}}  Y_{σ} M ⇑^{0}

(Appl) \frac{M ⇓^{k} (λα.M′) M′[N/α] ⇑^{l}}{MN ⇑^{k+l}}  \frac{M ⇑^{k}}{MN ⇑^{k}}

Fig. 3. Inductive definition of the divergence predicates

Proof. By the logical relations lemma, it suffices to show that the the denotations of constants are extensional. The only non trivial case is the fixed-point combinator. By (the proof of) Lemma 3.3, we know that its interpretation is the unique fixed point of a contractive functional, which is clearly extensional. Hence the result follows from Lemma 5.1. □

6 PCF+T

We now make time visible within PCF by introducing a first-order constant for a Gödel-number-free version of Kleene’s T -predicate. The idea is that one can test how long computations take, and give up if they take too long. We consider extensions of the metric and operational semantics discussed in Sections 3 and 4.

We first define divergence predicates M ⇑^{k} by induction as in Fig. 3.

Proposition 6.1 If M is a PCF program then M ⇑^{k} if and only if M ⇓^{l} v implies l > k.

That is, M is “k-divergent” if and only if the computation of M takes more than k steps. Notice that Theorem 4.1 implies that ⟦M⟧ = ∞ if and only if M ⇑^{k} for every k.

PCF+ T is obtained by extending PCF with a constant T_{γ} : γ → ι → o for each ground type γ and rules

(T) \frac{M ⇓^{k} v N ⇓^{l} n}{T MN ⇓^{k+l} true}(k ≤ n),  \frac{N ⇓^{k} n M ⇑^{n}}{T MN ⇓^{k+n} false} ,  \frac{N ⇑^{k}}{T MN ⇑^{k}} .

Roughly, this says that if the value of N is n, then T MN is true if the computation of M terminates in n or fewer steps, and false otherwise—but one also has to take into account that the computation of T MN itself takes time.

A useful alternative point of view is the following. First, notice that T M has type ι → o. We thus think of T M as a sequence of boolean values. This sequence consists of either infinitely many false’s, if M diverges, or else of finitely many false’s followed by infinitely many true’s, if M converges. Under this interpretation, T M codes the (finite or infinite) number of steps needed to compute M.

Notice that, for PCF, we have defined the divergence predicate from the evaluation relation. For PCF+ T, however, we have defined divergence and evaluation by simultaneous induction. But we still have that M ⇑^{k} if and only if M ⇓^{l} v implies l > k. It is easy to conclude from this that the relations M ⇓^{k} v and M ⇑^{k} are both decidable. In fact, they are primitive recursive. In contrast, M ⇓ v is recursively enumerable but not decidable, of course. Notice also that the relation M ⇓^{k} v is deterministic—but see Proposition 7.2.

The metric interpretation of PCF given in Section 3 is extended to PCF+ T by

⟦T⟧(x)(y) = \{ \begin{matrix}true^{(k+l)} & if y is of the form n^{(k)} and x is of the form v^{(l)} with l ≤ n, \\ false^{(k+n)} & if y is of the form n^{(k)} and x is either ∞ or v^{(l)} with l > n, \\ ∞ & otherwise (that is, if y = ∞). \end{matrix}

As easy extensions of the methods developed in Section 4 show, we still have a good match between the denotational and operational semantics:

Theorem 6.2 If M is a PCF+ T program then ⟦M⟧ = v^{(k)} if and only if M ⇓^{k} v.

An application of T is given in the proof of Lemma 7.2.

7 The extensional collapse of the metric model

In order to relate the metric model with Scott model, let D_{σ} denote the interpretation of type σ in Scott’s model and let ∼_{σ} be the logical relation between X_{σ} and D_{σ} such that ∼_{γ} is the least relation with

∞ ∼_{γ} ⊥, v^{(k)} ∼_{γ} v.

Let X and D denote the metric and Scott interpretation functions respectively.

Theorem 7.1 The relation X ⟦M⟧ ∼_{σ} D⟦M⟧ holds for every closed PCF term M : σ.

Proof. By the logical-relations lemma, it is enough to show that this is the case if M is a constant, the only difficult and interesting case being the fixedpoint combinator. Things are complicated by the fact that it isn’t true that, for a Cauchy sequence x_{k}, if x_{k} ∼ d for every k then lim_{k} x_{k} ∼ d. In fact, this already fails at ground types: one has that v^{(k)} ∼ v, by definition, but that lim_{k} v^{(k)} = ∞ ≁ v. However, under the assumption that the sequence x_{k} is increasing for a suitably (hereditarily) defined order, the conclusion holds, and this is sufficient for the purposes of this proof. At grounds types, such sequences are eventually constant. □

In Section 5 we defined notions of extensional and intensional functions of the metric model. Clearly, T denotes an intensional function. However, it is interesting that one can define, from T, extensional functions that are not PCF-denotable. Let por ∈ D_{o→o→o} be Scott’s parallel-or [14] and E ∈ D_{(ι→o)→o} be Plotkin’s existential quantifier [11].

Lemma 7.2 There are extensional PCF+ T-denotable functions por′ ∈ X_{o→o→o} and E′ ∈ X_{(ι→o)→o} with por′ ∼ por and E′ ∼ E.

Proof. For simplicity, in this sketch we are deliberately informal concerning the distinction between syntax and semantics. We begin by defining a metric version amb : ι → ι → ι of McCarthy’s ambiguity operator. The specification of amb requires that (1) amb xy ≈ x or amb xy ≈ y, (2) if x = ∞ then amb xy ≈ y, and (3) if y = ∞ then amb xy ≈ x. We implement this by returning the argument that terminates first: amb = amb′ 0 where amb′ : ι → ι → ι → ι is recursively defined by

amb′ nxy = if T xn then x else if T yn then y else amb′(n + 1)xy.

In order to define the existential quantifier, we first define a term witness : ι → (ι → o) → ι by

witness np = amb(if pn then n else Ω)(witness(n + 1)p),

where Ω is any divergent program, say Y (λx.x). The idea is that witness np is the first m ≥ n with pm ∼ true, if such an m exists. Here the word first is applied in its temporal sense and not in the ordinal sense. We then define

E′(p) = p(witness 0 p).

The important observation here is that if p is extensional and pΩ ∼ false then p is constant, and, in particular, there is no n with pn ∼ true. Therefore in this case witness 0 p = Ω and E′(p) ∼ false. Parallel-or can be defined similarly. (Notice that this proof doesn’t depend on the particular way computation steps are counted.) □

Theorem 7.3 The relation ∼_{σ} induces a bijection between equivalence classes of extensional points of X_{σ} and elements of D_{σ}.

Proof. The idea of proof sketched here arose after a conversation with John Longley. A technique based on universal domains, which I learned [5] from Thomas Streicher [16], is applied. We first show that the claim holds for σ = u where u = ι → o. Once this is done, we reduce the general case to this particular case as follows.

(1) By the results of Plotkin [12], we know that there are continuous maps E : D_{u→u} ⇆ D_{u} : P with P ∘ E = id_{D_{u→u}}. It follows that there are continuous maps e_{σ} : D_{σ} ⇆ D_{u} : p_{σ} with p_{σ} ∘ e_{σ} = id_{D_{σ}}. For ground types this is clear. We inductively lift them to higher types by e_{σ→τ}(F) = E(e_{τ} ∘ F ∘ p_{σ}) and p_{σ→τ}(f) = p_{τ} ∘ P (f) ∘ e_{σ}.

(2) Since PCF+E+por is universal [11], the maps defined in step (1) are PCF+E+por-definable. By taking the metric interpretation of the corresponding PCF+E′+por′ terms, we conclude, using Theorem 5.3, that there are extensional non-expansive maps S : X_{u→u} ⇆ X_{u} : R with R ∘ S ≈ id_{X_{u→u}} and also S ∼ E and R ∼ P, and that there there are extensional non-expansive maps s_{σ} : X_{σ} ⇆ X_{u} : r_{σ} with r_{σ} ∘ s_{σ} ≈ id_{D_{σ}}. Moreover, by Theorem 7.1, we have that s_{σ} ∼ e_{σ} and r_{σ} ∼ p_{σ}.

(3) We are now ready for the reduction. Suppose that d ∈ D_{σ} is given. Then there is an extensional y ∈ X_{u} with y ∼ e(d). Since r ∼ p, it follows that r(y) ∼ p(e(d)) = d, which establishes existence of an extensional x ∈ X_{σ} with x ∼ d. Now assume that an x ∈ X_{σ} with x ∼ d is given. Then s(x) ∼ e(d) because s ∼ e. But then y ∼ s(x), from which we conclude that r(y) ∼ r(s(x) = x, which establishes uniqueness up to extensional equivalence. Symmetrically, one concludes that for every extensional x ∈ X_{σ} there is a unique d ∈ D_{σ} with x ∼ d (up to equality). □

8 Another metric model of PCF

Perhaps it is more realistic to count one step for each reduction rule (including application, as substitution can be implemented by pointer assignment). In any case, to count steps in this way allows us to prove computational adequacy by an alternative method based on Banach’s fixed-point theorem. Formally, we inductively define an evaluation relation as in Fig. 4.

This operational semantics is matched by the metric semantics inductively defined in Fig. 5, where ρ ranges over environments. In order to prove that this is the case, we show that the denotational and operational semantics can be seen as fixed points of a contractive endomap of a suitable complete metric space. Let P_{σ} be the set of PCF closed terms of type σ and V_{σ} be the metric lifting of set of PCF values of type σ. Then V_{o} = X_{o} and V_{ι} = X_{ι}, the set of functions V_{σ}^{P_{σ}} is a complete metric space with the sup-metric, and so is the product ∏_{σ} V_{σ}^{P_{σ}}, again metrized by the sup-metric. In Fig. 6 we define a functional

Φ : ∏_{σ} V_{σ}^{P_{σ}} → ∏_{σ} V_{σ}^{P_{σ}}

Escardó

(Val) v ⇓^{0} v  if v is false, true, 0, 1, …, n, …, λα.M
(Succ) \frac{M ⇓^{k} n}{succ M ⇓^{k+1} (n + 1)}
(Pred) \frac{M ⇓^{k} 0}{pred M ⇓^{k+1} 0}  \frac{M ⇓^{k} (n + 1)}{pred M ⇓^{k+1} n}
(Zero) \frac{M ⇓^{k} 0}{zero M ⇓^{k+1} true}  \frac{M ⇓^{k} (n + 1)}{zero M ⇓^{k+1} false}
(Cond) \frac{L ⇓^{k} true M ⇓^{l} v}{if LMN ⇓^{k+l+1} v}  \frac{L ⇓^{k} false N ⇓^{l} v}{if LMN ⇓^{k+l+1} v}
(Fix) \frac{M(Y_{σ} M) ⇓^{k} v}{Y_{σ} M ⇓^{k+1} v}
(Appl) \frac{M ⇓^{k} (λx.L) L[N/x] ⇓^{l} v}{MN ⇓^{k+l+1} v}

Fig. 4. Another temporal operational semantics of PCF

⟦α⟧(ρ) = ρ(α)  where α is a formal variable
⟦λα.M⟧(ρ) = (x ↦ ⟦M⟧(ρ[x/α]))
⟦MN⟧(ρ) = δ(⟦M⟧(ρ))(⟦N⟧(ρ))
⟦v⟧(ρ) = η(v)  for every value v = false, true, 0, 1, 2, …, n, …
⟦succ M⟧(ρ) = δ ∘ L(n ↦ n + 1)(⟦M⟧(ρ))
⟦pred M⟧(ρ) = δ ∘ L(0 ↦ 0, n + 1 ↦ n)(⟦M⟧(ρ))
⟦zero M⟧(ρ) = δ ∘ L(0 ↦ true, n + 1 ↦ false)(⟦M⟧(ρ))
⟦if LMN⟧(ρ) = δ \{ \begin{matrix}δ^{k}(⟦M⟧(ρ)) & if ⟦L⟧(ρ) is of the form true^{(k)} \\ δ^{k}(⟦M⟧(ρ)) & if ⟦L⟧(ρ) is of the form false^{(k)} \\ ∞ & otherwise \end{matrix}
⟦Y_{σ} M⟧(ρ) = fix_{σ}(⟦M⟧(ρ))

Fig. 5. Another metric semantics of PCF

Φ(E⃗)(σ)(v) = η(v)
Φ(E⃗)(ι)(succ M) = δ ∘ L(n ↦ n + 1)(E_{ι}(M))
Φ(E⃗)(ι)(pred M) = δ ∘ L(0 ↦ 0, n + 1 ↦ n)(E_{ι}(M))
Φ(E⃗)(o)(zero M) = δ ∘ L(0 ↦ true, n + 1 ↦ false)(E_{o}(M))
Φ(E⃗)(γ)(if LMN) = δ \{ \begin{matrix}δ^{k}(E_{γ}(M)) & if E_{o}(L) is of the form true^{(k)} \\ δ^{k}(E_{γ}(N)) & if E_{o}(L) is of the form false^{(k)} \\ ∞ & otherwise \end{matrix}
Φ(E⃗)(σ)(Y_{σ} M) = δ(E_{σ}(M(Y_{σ} M)))
Φ(E⃗)(τ)(M_{σ→τ} N_{σ}) = δ \begin{cases}v^{(k+l)} & if E_{σ→τ} (M) = (λx.L)^{(k)} and E_{τ} (L[N/x]) = v^{(l)} \\ ∞ & otherwise \end{cases}

Fig. 6. Definition of Φ

by equations of the form

Φ(E⃗)(σ)(M) = v,

where E⃗ ∈ ∏_{σ} V_{σ}^{P_{σ}}, σ is a type, M ∈ P_{σ}, and v ∈ V_{σ}. Lemma 8.1 Φ is a contractive map. Proof. This immediately follows from the fact that each equation, except the base case, is guarded by a delay map. □ Lemma 8.2 Let E⃗val be the unique fixed point of Φ. If M : σ is a closed term then Eval_{σ}(M) = v^{(k)} iff M ⇓^{k} v. Proof. By induction on the definition of M ⇓^{k} v. This is a triviality, as Φ is just a reformulation of the definition of M ⇓^{k} v. □

The following lemma can be regarded as a formulation of soundness: Lemma 8.3 The vector S⃗ ∈ ∏_{σ} V_{σ}^{P_{σ}} defined by S_{γ}(M) = ⟦M⟧ for each ground type γ, and S_{σ} = Eval_{σ} for each functional type σ, is a fixed point of Φ. Proof. Essentially the same as that of Lemma 4.2. □

Completeness is a corollary of soundness: Theorem 8.4 If M is a PCF program then ⟦M⟧ = v^{(k)} iff M ⇓^{k} v. Proof. By Lemma 8.3 and Banach’s fixed-point theorem, we have that S_{γ} = Eval_{γ} for γ ground. Therefore the result follows from Lemma 8.2. □

(PVal) w ⇓ w  if w is false, true, 0, 1, …, n, …, λα.M, δ_{σ}M,

(Succ) \frac{M ⇓ n}{succ M ⇓ (n + 1)}  \frac{M ⇓ δ_{ι}N}{succ M ⇓ δ_{ι}(succ N)}

(Pred) \frac{M ⇓ 0}{pred M ⇓ 0}  \frac{M ⇓ (n + 1)}{pred M ⇓ n}  \frac{M ⇓ δ_{ι}N}{pred M ⇓ δ_{ι}(pred N)}

(Zero) \frac{M ⇓ 0}{zero M ⇓ true}  \frac{M ⇓ (n + 1)}{zero M ⇓ false} \frac{M ⇓ δ_{ι}N}{zero M ⇓ δ_{o}(zero N)}

(Cond) \frac{L ⇓ true M ⇓ w}{if LMN ⇓ w}  \frac{L ⇓ false N ⇓ w}{if LMN ⇓ w} \frac{L ⇓ δ_{o}L′}{if LMN ⇓ δ_{γ}(if L′MN)}

(Fix) Y M ⇓ δ_{σ}(M(Y M))

(Appl) \frac{M ⇓ (λα.M′) M′[N/α] ⇓ w}{MN ⇓ w} \frac{M ⇓ δ_{σ→τ} M′}{MN ⇓ δ_{τ} (M′N)}

Fig. 7. Operational semantics of chattering PCF

9 Chattering PCF

Non-termination in PCF is silent. In order to gain a better understanding of the nature of the metric model, we introduce a variant of PCF in which non-termination is chattering. The terminology was suggested to me by John Longley.

Chattering PCF is PCF extended with a constant δ_{σ} : σ → σ for each type σ. The metric interpretation of chattering PCF is the same as that of PCF, extended by ⟦δ_{σ}⟧ = δ_{σ} . Since ⟦λx. Y_{γ}(λy.x)⟧ = δ_{γ}, we have that the PCF- and chattering-PCF-denotable points coincide. The idea is that the operational semantics of chattering PCF explicitly manipulates the temporal information contained in the metric model.

A pseudo-value (or weak head-normal form) is either a value or a term of the form δM. A relation M ⇓ w between closed terms and pseudo-values is inductively defined in Fig. 7. Notice that the rules in the third column have the role of “propagating delays”. Notice also that there are no reductions under δ—but see Proposition 9.5. Chattering PCF programs are normalizing:

Theorem 9.1 For every program M there is a unique w with M ⇓ w.

Notice that if reductions under δ were allowed, uniqueness would fail. For example, one would have that Y λx.x ⇓ δ^{k}((λx.x)(Y λx.x)) for every k. We prove Theorem 9.1 by induction on types. Uniqueness is clear. In order to prove existence, we define the reducible closed PCF terms are by induction on types as follows:

(i) A program M : γ is reducible if and only if M ⇓ w for some w. (ii) A closed term M : σ → τ is reducible if and only if the term MN : τ is

reducible for every reducible closed term N : σ.

Thus, reducibility is a logical property of closed terms.

Lemma 9.2 Every chattering PCF closed term is reducible.

Proof. By the logical-relations lemma, it suffices to prove that constants are reducible. Every ground constant is reducible, because ground constants are values and values reduce to themselves. In order to show that succ is reducible, we have to show that succ M is reducible whenever M : ι is a reducible closed term. Reducibility of M : ι means that M ⇓ w form some w, which has to be either of the form n or else of the form δN for a unique N. In the first case succ M ⇓ n + 1 and in the second M ⇓ δ(succ N). Similarly, pred, zero, if, and δ are reducible. In order to show that Y_{σ} is reducible, notice that any type σ can be uniquely written as τ_{1} → ⋯ → τ_{k} → γ with γ ground. Hence it is enough to show that Y MN_{1} ⋯ N_{k} is reducible whenever N_{1} : τ_{1}, …, N_{k} : τ_{k} are reducible closed terms. First, by one application of rule (Fix), we have that Y M ⇓ δ_{γ}(M(Y M)). Then, by k applications of rule (Appl), we first have that Y MN_{1} ⇓ δ_{τ_{2}→···→τ_{n}→γ}(M(Y M)N_{1}), then that Y MN_{1}N_{2} ⇓ δ_{τ_{3}→···→τ_{n}→γ}(M(Y M)N_{1}N_{2}), …, and finally that Y MN_{1}N_{2} ⋯ N_{k} ⇓ δ_{γ}(M(Y M)N_{1}N_{2} ⋯ N_{k}). □

This establishes the normalization theorem. Again, we have a good match between the denotational and operational semantics. First, it is straightforward to formulate and prove soundness:

Proposition 9.3 If M ⇓ w then ⟦M⟧ = ⟦w⟧.

Of course, completeness cannot be formulated as the literal converse of soundness, because pseudo-values are week head-normal forms. Recalling that every point of X_{γ} is either of the form η(v) or else of the form δ(x) for a unique x ∈ X_{γ}, completeness can be formulated as follows:

Theorem 9.4 Let M be a chattering PCF program.

(i) If ⟦M⟧ = η(v) then M ⇓ v. (ii) If ⟦M⟧ = δ(x) then M ⇓ δM′ for some M′ with ⟦M′⟧ = x.

This follows from the normalization theorem and soundness. Operationally, PCF and chattering PCF are related as follows:

Proposition 9.5 If M is a PCF program, and hence a chattering PCF program, then the relation M ⇓^{k} v holds in PCF if and only if there are (necessarily unique) chattering PCF programs M_{1}, …, M_{k} such that the following relations hold in chattering PCF:

M ⇓ δM_{1}, M_{1} ⇓ δM_{2}, M_{2} ⇓ δM_{3}, …, M_{k} ⇓ v.

If reductions under δ were allowed, then the proposition could be formulated as: M ⇓^{k} v if and only if M ⇓ δ^{k}v.

In the chattering-style operational semantics, one doesn’t need the divergence predicates in order to define the operational semantics of T:

(T)

\frac{N ⇓ n M ⇓ v}{T MN ⇓ true} ,  \frac{N ⇓ 0 M ⇓ δM′}{T MN ⇓ false} ,

\frac{N ⇓ (n + 1) M ⇓ δM′}{T MN ⇓ δ(T M′n)} ,  \frac{N ⇓ δN′}{T MN ⇓ δ(T MN′)}.

For chattering PCF extended with T in this way, it is easy to see that the above results still hold.

Acknowledgements

I am grateful to John Longley for many stimulating discussions. I have also benefited from discussions with Samson Abramsky, Martin Hofmann, Alex Simpson and Thomas Streicher. Dana Scott found a mistake in the definition of metric lifting in an earlier version of this paper. Jan Rutten helped me with the bibliographic references to metric semantics of concurrency.

References

[1] J.W. de Bakker and E. de Vink. Control Flow Semantics. Foundations of Computing Series. The MIT Press, 1996.

[2] J.W. de Bakker and J.J-. Ch. Meyer. Order and metric in the stream semantics of elemental concurrency. Acta Informatica, 24:491–511, 1987.

[3] J.W. de Bakker and J.J.M.M. Rutten, editors. Ten Years of Concurrency Semantics, Selected Papers of the Amsterdam Concurrency Group. World Scientific, 1992.

[4] J.W. de Bakker and J.I. Zucker. Processes and the denotational semantics of concurrency. Information and Control, 54(1/2):70–120, 1982.

[5] M.H. Escardó. Real PCF extended with ∃ is universal. In A. Edalat, S. Jourdan, and G. McCusker, editors, Advances in Theory and Formal Methods of Computing: Proceedings of the Third Imperial College Workshop, April 1996, pages 13–24, Christ Church, Oxford, 1996. IC Press.

[6] M.H. Escardó and D. Turi. A conceptual account of metric lifting. Laboratory for Foundations of Computer Science, University of Edinburgh. Work in progress, June 1999.

[7] C. A. Gunter. Semantics of Programming Languages—Structures and Techniques. The MIT Press, London, 1992.

[8] J.N. Kok and J.J.M.M. Rutten. Contractions in comparing concurrency semantics. Theoretical Computer Science, 76:179–222, 1990.

[9] J.R. Longley. Matching typed and untyped realizability. Presented at Tutorial Workshop on Realizability Semantics, FLoC’99, Trento, Italy 1999. Available

at http://www.dcs.ed.ac.uk/home/jrl/. To appear in Electronic Notes in

Theoretical Computer Science, Elsevier, 1999.

[10] E. Moggi. Notions of computation and monads. Information and Computation, 93(1):55–92, 1991.

[11] G.D. Plotkin. LCF considered as a programming language. Theoretical Computer Science, 5(1):223–255, 1977.

[12] G.D. Plotkin. 𝕋^{ω} as a universal domain. Journal of Computer and System Sciences, 17:209–236, 1978.

[13] J.J.M.M. Rutten. A note on coinduction and weak bisimilarity for while programs. Technical Report SEN-R9826, ISSN 1386-369X, CWI, Amsterdam, October 1998.

http://www.cwi.nl/static/publications/reports/reports.html.

[14] D.S. Scott. A type-theoretical alternative to CUCH, ISWIM and OWHY. Theoretical Computer Science, 121:411–440, 1993. Reprint of a manuscript produced in 1969.

[15] M.B. Smyth. Topology. In S. Abramsky, D. M. Gabbay, and T.S.E. Maibaum, editors, Handbook of Logic in Computer Science, volume 1, pages 641–761. Clarendon Press, Oxford, 1992.

[16] T. Streicher. A universality theorem for PCF with recursive types, parallel-or and ∃. Mathematical Structures for Computing Science, 4(1):111 – 115, 1994.