A Probabilistic and Non-Deterministic Call-by-Push-Value Language
Jean Goubault-Larrecq
TL;DR
This paper introduces a probabilistic, non-deterministic call-by-push-value language with a domain-theoretic semantics, enabling rigorous mathematical treatment of higher-order probabilistic programs.
Contribution
It presents a novel language design combining probabilistic choice and non-determinism within the call-by-push-value framework, with sound, adequate, and fully abstract semantics.
Findings
Semantic models are sound and adequate.
Language achieves full abstraction with additional primitives.
Framework handles higher-order probabilistic languages mathematically.
Abstract
There is no known way of giving a domain-theoretic semantics to higher-order probabilistic languages, in such a way that the involved domains are continuous or quasi-continuous - the latter is required to do any serious mathematics. We argue that the problem naturally disappears for languages with two kinds of types, where one kind is interpreted in a Cartesian-closed category of continuous dcpos, and the other is interpreted in a category that is closed under the probabilistic powerdomain functor. Such a setting is provided by Paul B. Levy's call-by-push-value paradigm. Following this insight, we define a call-by-push-value language, with probabilistic choice sitting inside the value types, and where conversion from a value type to a computation type involves demonic non-determinism. We give both a domain-theoretic semantics and an operational semantics for the resulting language, and…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
A Probabilistic and Non-Deterministic Call-by-Push-Value
Language††thanks: This research was partially supported by Labex DigiCosme (project ANR-11-LABEX-0045-DIGICOSME) operated by ANR as part of the program “Investissement d’Avenir” Idex Paris-Saclay (ANR-11-IDEX-0003-02).
Jean Goubault-Larrecq LSV, ENS Paris-Saclay, CNRS, Université Paris-Saclay. Address: ENS Paris-Saclay, 61 avenue du président Wilson, 94230 Cachan, France. Email: [email protected]
Abstract
There is no known way of giving a domain-theoretic semantics to higher-order probabilistic languages, in such a way that the involved domains are continuous or quasi-continuous—the latter is required to do any serious mathematics. We argue that the problem naturally disappears for languages with two kinds of types, where one kind is interpreted in a Cartesian-closed category of continuous dcpos, and the other is interpreted in a category that is closed under the probabilistic powerdomain functor. Such a setting is provided by Paul B. Levy’s call-by-push-value paradigm. Following this insight, we define a call-by-push-value language, with probabilistic choice sitting inside the value types, and where conversion from a value type to a computation type involves demonic non-determinism. We give both a domain-theoretic semantics and an operational semantics for the resulting language, and we show that they are sound and adequate. With the addition of statistical termination testers and parallel if, we show that the language is even fully abstract—and those two primitives are required for that.
Keywords: domain theory; PCF; call-by-push-value; probabilistic choice; non-deterministic choice; full abstraction.
1 Introduction
A central problem of domain theory is the following: is there any full Cartesian-closed subcategory of the category of continuous dcpos that is closed under the probabilistic powerdomain functor [14]? Solving the question in the positive would allow for a simple semantics of probabilistic higher-order languages, where types are interpreted as certain continuous dcpos.
However, we have a conundrum here. The category itself is closed under [13], but is not Cartesian-closed [2, Exercise 3.3.12(11)]. Among the Cartesian-closed categories of continuous domains, none is known to be closed under , and most, such as the category of bc-domains or the category of continuous complete lattices, definitely are not [14].
Instead of solving this problem, one may wonder whether there are other kinds of domain-theoretic semantics that would be free of the issue. Typically, can we imagine having two classes of types? One would be interpreted in a category of continuous dcpos that is closed under — for example, although we will prefer the category of pointed coherent continuous dcpos (see below). The other would be interpreted in a Cartesian-closed category of continuous dcpos, and we will use . Such a division in two classes of types is already present in Paul B. Levy’s call-by-push-value [17] (a.k.a. CBPV), and although the division is justified there as to be between value types and computation types, the formal structure will be entirely similar.
Outline
We briefly review some related work in Section 2, and give a few basic working definitions in Section 3. We define our probabilistic call-by-push-value languages in Section 4, explaining the design decisions we had to make in the process—notably the extra need for demonic non-determinism. We give domain-theoretic and operational semantics there, too. We establish soundness in Section 5 and adequacy in Section 6, to the effect that for every ground term of the specific type , the probability that must terminate, as defined from the operational semantics, coincides with a similar notion of probability defined from the denotational semantics. In Section 7, we review a few useful consequences of adequacy, among which the coincidence between the applicative preorder and the contextual preorder (both will be defined there), a fact sometimes called Milner’s Context Lemma in the context of PCF (see [20, Theorem 8.1]). We show that, among the languages we have defined, CBPV is not (inequationally) fully abstract in Section 8, and that adding a parallel if operator does not make it fully abstract, but that adding both and a statistical termination tester operator (as in [11]) results in an (inequationally) fully abstract language. The latter is proved in Section 9. We conclude and list a few remaining open questions in Section 10.
Acknowledgments
I wish to thank Zhenchao Lyu and Xiaodong Jia, who participated in many discussions on the theme of this paper; Ohad Kammar, who kindly pointed me to [23]; and the anonymous referees of the LICS’19 conference.
2 Related Work
Call-by-push-value (CBPV) is the creation of Paul B. Levy [17] (see also the book [18]), and is a typed higher-order pure functional language. It was originally meant as a subsuming paradigm, embodying both call-by-value and call-by-name disciplines.
The first probabilistic extension of CBPV was proposed recently by Ehrhard and Tasson [4], and its denotational semantics rests on probabilistic coherence spaces. Their typing discipline is inspired by linear logic, and they also include a treatment of general recursive types, which we will not. In contrast, our extension of CBPV will have first-class types of subprobability distributions , and will also include a type former for demonic non-determinism (a.k.a., must-non-determinism).
Statistical probabilistic programming has attracted quite some attention recently, and quasi-Borel spaces and predomains have recently been used to give adequate semantics to typed and untyped probabilistic programming languages, see [23]. The latter describes another way of circumventing the problem we stated in the introduction. One important point that Vákár, Kammar and Staton achieve is the commutativity of the probabilistic choice monad, at all, even higher-order, types. In standard domain theory, the monad is known to be commutative in full subcategories of only. That would be enough motivation to attempt to solve the problem stated in the introduction, of finding a Cartesian-closed category, closed under [14]. We also implement a commutative monad in a higher-order setting; our way of circumventing the problem is merely different.
There is a large body of literature concerned with the question of full abstraction for PCF-like languages. The first paper on the subject is due to G. Plotkin [19], who defined the language PCF, asked all the important questions (soundness, adequacy, full abstraction, definability), and answered all of them, except for the question of finding a fully abstract denotational model of PCF without parallel if, a question that was solved later, through game semantics notably [12, 1]. Th. Streicher’s book [20] is an excellent reference on the subject.
Probabilistic coherence spaces provide a fully abstract semantics for a version of PCF with probabilistic choice, as shown by Ehrhard, Tasson, and Pagani [5]. The already cited paper of Ehrhard and Tasson [4] gives an analogous result for their probabilistic version of CBPV. Our work is concerned with languages with domain-theoretic semantics instead, and our former work [11] gives soundness, adequacy and full abstraction results for PCF plus angelic non-determinism, and for PCF plus probabilistic choice and angelic non-determinism plus so-called statistical termination testers. We will see that CBPV naturally calls for a form of demonic, rather than angelic, non-determinism.
3 Preliminaries
We refer to [8, 2, 10] for material on domain theory and topology. A dcpo is pointed if and only if it has a least element . Dcpos are always equipped with their Scott topology. and are dcpos, with the usual ordering. The way-below relation is written : if and only if for every directed family such that , there is an such that . A dcpo is continuous if and only if every element is the supremum of a directed family of elements way-below it. In that case, the sets \hbox to0.0pt{\uparrow\hss}\raise 2.15277pt\hbox{\uparrow}x=\{y\in X\mid x\ll y\} form a base of open sets of the Scott topology. We recall that a base of a topology is a family of open sets such that every open set is a union of sets from . A subbase is a family such that the finite intersections of elements of form a base.
A basis of a dcpo (not to be confused with a base) is a set of elements of such that, for every , is directed and has as supremum. A dcpo is continuous if and only if it has a basis. Then the sets \hbox to0.0pt{\uparrow\hss}\raise 2.15277pt\hbox{\uparrow}b, , also form a base of the Scott topology.
We write for the specialization ordering of a topological space. For a dcpo , that is the original ordering on . A subset of a topological space is saturated if and only if it is upwards-closed in , if and only if it is the intersection of its open neighborhoods. A topological space is locally compact if and only if for every , for every open neighborhood of , there is a compact saturated set such that . ( denotes the interior of .) In that case, for every compact saturated subset and every open neighborhood of , there is a compact saturated set such that . A topological space is coherent if and only if the intersection of any two compact saturated subsets is compact. It is well-filtered if and only if for every filtered family of compact saturated sets (filtered meaning directed for reverse inclusion), every open neighborhood of already contains some . In a well-filtered space, the intersection of such a filtered family is compact saturated. A stably compact space is a , well-filtered, locally compact, coherent and compact space . Then the complements of compact saturated sets form another topology on , the cocompact topology, and with the cocompact topology is the de Groot dual of . For every stably compact space, . Every pointed, coherent, continuous dcpo is stably compact.
Given two dcpos and , denotes the dcpo of all Scott-continuous maps from to , ordered pointwise. Directed suprema are also pointwise, namely for every directed family in .
4 The Languages CBPV and CBPV
The first language we introduce is called CBPV: it is a call-by-push-value language with emonic non-determinism and robabilistic choice. We will explain below why we do not consider just probabilistic choice, but also demonic non-determinism.
4.1 Types and their Semantics
We consider the following grammar of types:
[TABLE]
The types , , …, are the value types, and the types , , …, are the computation types, following Levy [17]. Our types differ from Levy’s: we do not have countable sums in value types or countable products in computation types, we write instead of , and we have a primitive type of integers; the main difference is the construction, denoting the type of subprobability valuations on the space of elements of type .
We write , for types when it is not important whether they are value types or computation types.
We have already said in the introduction that computation types will be interpreted in the category of continuous complete lattices. Value types will give rise to pointed, coherent, continuous dcpos \left\llbracket{\tau}\right\rrbracket:
- •
for every computation type , we will define \left\llbracket{\boldsymbol{\mathtt{U}}\underline{\tau}}\right\rrbracket as \left\llbracket{\underline{\tau}}\right\rrbracket: being a continuous complete lattice, it is in particular pointed, coherent, and a continuous dcpo;
- •
\left\llbracket{\boldsymbol{\mathtt{unit}}}\right\rrbracket will be Sierpiński space with ;
- •
\left\llbracket{\boldsymbol{\mathtt{int}}}\right\rrbracket will be , with the ordering that makes least and all integers be pairwise incomparable;
- •
\left\llbracket{\boldsymbol{\mathtt{V}}\tau}\right\rrbracket will be \mathbf{V}_{\leq 1}(\left\llbracket{\tau}\right\rrbracket), where denotes the dcpo of all subprobability valuations on the space .
A subprobability valuation on is a map from the lattice of open subsets of to which is strict (), Scott-continuous, and modular (). When is a continuous dcpo, so is [13, Corollary 5.4]. It is pointed, since the zero valuation is least in . If is also coherent, then is stably compact, see below. Hence \left\llbracket{\boldsymbol{\mathtt{V}}\tau}\right\rrbracket is indeed a pointed, coherent continuous dcpo.
The fact that is stably compact for every coherent continuous dcpo is folklore. We argue as follows. The lift of , obtained by adding a fresh bottom element to , is stably compact. Then the space of all probability valuations , i.e., such that , is stably compact in the weak upwards topology [3, Theorem 39]. The latter has a subbase of open sets of the form , for every open subset of and . The restriction map is a homeomorphism from onto , both with their weak upwards topology, with inverse . Hence is stably compact in its weak upwards topology. Since is continuous, the latter coincides with the Scott topology, as shown by [16, Satz 8.6], see also [22, Satz 4.10].
It might seem curious that probabilistic non-determinism arises, as , among the value types. I have no philosophical backing for that, but this is somehow forced upon us by the mathematics.
Similarly, computation types will give rise to continuous complete lattices \left\llbracket{\underline{\tau}}\right\rrbracket—notably \left\llbracket{\sigma\to\underline{\tau}}\right\rrbracket will be the continuous complete lattice [\left\llbracket{\sigma}\right\rrbracket\to\left\llbracket{\underline{\tau}}\right\rrbracket] of all Scott-continuous maps [\left\llbracket{\sigma}\right\rrbracket\to\left\llbracket{\underline{\tau}}\right\rrbracket] from \left\llbracket{\sigma}\right\rrbracket to \left\llbracket{\underline{\tau}}\right\rrbracket—, but we have to decide on an interpretation of types of the form .
If we had decided to interpret computation types as bc-domains instead of continuous complete lattices, then a natural choice would be to define \left\llbracket{\boldsymbol{\mathtt{F}}{}\tau}\right\rrbracket as Ershov’s bc-hull of \left\llbracket{\tau}\right\rrbracket [7]. (Bc-domains are, roughly speaking, continuous complete lattices that may lack a top element.) As Ershov notices, “the construction of a bc-hull in the general case is highly nonconstructive (using a Zorn’s lemma)” (ibid., page 13). Fortunately, the bc-hull of a space is a natural subspace of the Smyth powerdomain of , at least when is a coherent algebraic dcpo (ibid., Corollary B), and is easier to work with. Explicitly, is the poset of all non-empty compact saturated subsets of , ordered by reverse inclusion, and is used to interpret demonic non-determinism in denotational semantics. When is well-filtered and locally compact, is also a continuous dcpo, and it is a bc-domain provided is also compact and coherent. We shall see below that , the poset of all (possibly empty) compact saturated subsets of —alternatively, plus an additional top element —, is a continuous complete lattice whenever is a stably compact space, and that would make \mathcal{Q}^{\top}(\left\llbracket{\tau}\right\rrbracket) a good candidate for \left\llbracket{\boldsymbol{\mathtt{F}}{}\tau}\right\rrbracket.
For technical reasons related to adequacy, we will need a certain map below to be strict, i.e., to map to . (Technically, this is needed so that the denotational semantics of the construction , to be introduced below, be strict in that of , in order to validate the fact that loops forever if does.) This will be obtained by defining \left\llbracket{\boldsymbol{\mathtt{F}}{}\tau}\right\rrbracket as \mathcal{Q}^{\top}_{\bot}(\left\llbracket{\tau}\right\rrbracket) instead, where is the lift of , obtained by adding a fresh element below all others.
We recapitulate:
- •
\left\llbracket{\sigma\to\underline{\tau}}\right\rrbracket=[\left\llbracket{\sigma}\right\rrbracket\to\left\llbracket{\underline{\tau}}\right\rrbracket];
- •
\left\llbracket{\boldsymbol{\mathtt{F}}{}\sigma}\right\rrbracket=\mathcal{Q}^{\top}_{\bot}(\left\llbracket{\sigma}\right\rrbracket).
Let us check that \mathcal{Q}^{\top}_{\bot}(\left\llbracket{\sigma}\right\rrbracket) has the required property of being a continuous complete lattice, and let us prove some additional properties that we will need later. We start with the similar properties of \mathcal{Q}^{\top}(\left\llbracket{\sigma}\right\rrbracket). We let map every to .
Proposition 4.1
Let be a stably compact space. Then:
* is a continuous complete lattice, and is way-below if and only if ;* 2. 2.
For every continuous complete lattice , for every continuous map , there is a Scott-continuous map such that , and it is defined by . 3. 3.
*, . *
Proof.
- This is well-known, but here is a brief argument. The elements of are exactly the closed subsets in the de Groot dual of , and the closed sets of any topological space always form a complete lattice. Note that the supremum of an arbitrary family in is .
Given any compact saturated subset of , the family of compact saturated neighborhoods of is filtered, and has as intersection. Indeed, since is saturated, it is the intersection of its open neighborhoods; for every open neighborhood of , local compactness implies that there is a compact saturated set such that ; applying this to shows that is non-empty, and given , applying it to , shows that contains an element included in both and .
It follows that, if , then contains an element of , hence in particular an open neighborhood of . Conversely, if where is open, then for every directed family in such that , contains some by well-filteredness, hence . Therefore .
Finally, since every in is the filtered intersection of the elements of , it is the supremum of the directed family , and we have just argued that every element of is way-below , showing that is continuous.
-
We define as . This satisfies , and is monotonic. Note that this is defined even when is empty, in which case is the top element of . In order to show that is Scott-continuous, let be a directed family in , and . We wish to show that ; the converse inclusion is by monotonicity. To this end, we let be an element of way-below . Since for every , every element of is in the open set f^{-1}(\hbox to0.0pt{\uparrow\hss}\raise 2.15277pt\hbox{\uparrow}y). Then is included in f^{-1}(\hbox to0.0pt{\uparrow\hss}\raise 2.15277pt\hbox{\uparrow}y), so by well-filteredness some is also included in f^{-1}(\hbox to0.0pt{\uparrow\hss}\raise 2.15277pt\hbox{\uparrow}y). Then for every , so . Since that holds for every , the desired inequality follows.
-
Easy check. Note that item 2 does not state that is unique; we have just chosen the largest one. A similar construction is well-known for . Proposition 4.1 establishes the essential properties needed to show that defines a monad on the category of stably compact spaces, and that is not only well-known, but we will not require as much.
We turn to \mathcal{Q}^{\top}_{\bot}(\left\llbracket{\tau}\right\rrbracket). We again write for the function that maps to , this time from to \mathcal{Q}^{\top}_{\bot}(\left\llbracket{X}\right\rrbracket). Below, we again write for the extension of to . This should not cause any confusion with the map of Proposition 4.1, since the two maps coincide on . Note that is now strict.
Proposition 4.2
Let be a stably compact space. Then:
* is a continuous complete lattice, and is way-below if and only if , or and ;* 2. 2.
For every continuous complete lattice , for every continuous map , there is a strict Scott-continuous map such that . This is defined by , and for every , . 3. 3.
, . 4. 4.
*For every stably compact space , for every Scott-continuous map , and for every Scott-continuous map from to a continuous complete lattice , . *
Proof.
-
The lift of a continuous complete lattice is a continuous complete lattice, and is always way-below every element.
-
Easy.
-
We check the second inequality. That follows from Proposition 4.1, item 3 if . If , then and . Similarly if .
-
Fix . If , then by strictness. Henceforth, we assume that .
If for some , then , so , and , since is strict. Henceforth, we assume that for every .
We claim that is compact. Let be a directed family of open subsets of whose union contains . For every , is compact and included in , so for some . Hence . Since is compact, for some , whence .
is also saturated in , hence an element of , and therefore also of . It follows that this is the infimum of the elements , , hence is equal to . Therefore . Item 4 above is part of the properties needed to check that defines a monad on . We will not expand on that.
4.2 Syntax
We define the syntax of our language CBPV together with its typing discipline, inductively, as in Figure 1, using the notation to say “ is a term of type ”. There are countably infinitely many variables , , …of each value type .
We extend the notation to the case where has an arbitrary computation type by: for every , , where is fresh. Similarly, we extend to all computation types by letting .
The variable is binding in , in , and in , and its scope is in all three cases. We omit the standard definition of -renaming and of capture-avoiding substitution.
Using recursion at value types may seem strange, but this allows us to define some interesting values. For example, we can define the uniform distribution on by the term , which operates via a form of rejection sampling.
We will also consider an extension of CBPV called CBPV, obtained by admitting the following additional clauses:
[TABLE]
is the statistical termination tester, and is parallel if. We extend the notation to the case where and have an arbitrary computation type by letting denote when , have type , where is a fresh variable.
The language CBPV is obtained by admitting only the second one as extra clause, while CBPV only admits the first one as extra clause.
4.3 Denotational Semantics
Let , the dcpo of environments, be the product of the dcpos \left\llbracket{\sigma}\right\rrbracket over all variables . Its elements are maps from variables to values . The denotational semantics is given by a family of Scott-continuous maps \left\llbracket{M}\right\rrbracket, one for each , from to \left\llbracket{\overline{\tau}}\right\rrbracket: see Figure 2, where the bottom two clauses are specific to CBPV, resp. to CBPV, and the two of them together are specific to CBPV. We use the notation to denote the function that maps each to . For every , and every V\in\left\llbracket{\sigma}\right\rrbracket, we write for the environment that maps to and every variable to . The operator maps every Scott-continuous map from a pointed dcpo to itself, to its least fixed point . The Dirac mass at is the probability valuation such that if , [math] otherwise. For every continuous map , is the continuous map from to defined by for every open subset of . For future reference, we note that , and that, for every continuous map ,
[TABLE]
Implicit here is the fact that the map is itself continuous. Also, integration is linear in both the integrated function and the continuous valuation , and Scott-continuous in each. These facts can be found in Jones’ PhD thesis [13].
The fact that the semantics \left\llbracket{M}\right\rrbracket\rho is well-defined and continuous in is standard. Note the use of binary infimum () in the semantics of and of , for which we use the following lemma.
Lemma 4.3
Let be a continuous complete lattice.
The infimum map is Scott-continuous. 2. 2.
For any two continuous maps , where is a any topological space, the infimum is computed pointwise: .
Proof. Item 1 is well-known. Explicitly, one must show that for every directed family with supremum in , for every , : for every , is below and below some , hence below for some .
As for item 2, the composition of with is continuous by item 1, is below and , and is clearly above any lower bound of and .
4.4 Operational Semantics
We choose an operational semantics in the style of [11]. It operates on configurations, which are pairs of an evaluation context and a term . The deterministic part of the calculus will be defined by rewrite rules between configurations. For the probabilistic and non-deterministic part of the calculus, we will rely on judgments , which state, roughly, that the probability that computation terminates, starting from , is larger than .
The elementary contexts, together with their types (where , are value or computation types) are defined by:
- •
, for every and every computation type ;
- •
for every ;
- •
, for every computation type ;
- •
;
- •
for all ;
- •
for every ;
- •
and , for all value types and ;
- •
, for every .
The initial contexts are , and . For every elementary or initial context and every , we write for the result of replacing the unique occurrence of the hole in (after removing the outer square brackets) by . E.g, .
A context (of type ) is a finite list () where is an initial context, , …, are elementary contexts, and , , and . We then write for .
Note that the contexts are defined in exactly the same way for CBPV and for CBPV, CBPV, and CBPV.
The configurations of the operational semantics are pairs where and . The rules of the operational semantics are given in Figure 3. The last row is specific to CBPV, CBPV, or to CBPV. The first rewrite rule—the redex discovery rule —applies provided is an elementary context. The notation denotes capture-avoiding substitution of for in .
The judgments are defined for all terms , contexts , and , and mean that is way-below the probability of termination of (i.e., either or is strictly less than the probability that terminates). Since induces non-deterministic choice, we really mean the probability of *must-*termination, namely that, in whichever way the non-determinism involved in the use of the operator is resolved (evaluating left, or right), the final probability is larger than .
We write for , where sups are taken in . This leads to the following central notion, which we only state for ground terms. A term is ground if and only if it has no free variable. (We define ground contexts similarly.) The case of non-ground terms can be dealt with using appropriate quantifications over substitutions, but will not be needed.
Definition 4.4
*The contextual preorder between ground CBPV terms of type is defined by if and only if for every ground evaluation context , . *
We will freely reuse the notations , for the similarly defined notions on the related languages CBPV, CBPV, and CBPV. If there is any need to make the language precise, we will mention it explicitly.
We end this section with a few elementary lemmata, which will come in handy later on, and which should help the reader train with the way the operational semantics works.
Lemma 4.5
If is derivable and is such that , then is also derivable, whether in CBPV, CBPV, CBPV, or CBPV.
Proof. Easy induction on the rules of Figure 3. In the case of a derivation of the form , where , from and , we write as where and are rational and between [math] and , resp. . (E.g., we let and .) By induction hypothesis we can derive and , so we can derive .
Lemma 4.6
If , then .
Proof. Whenever we can derive , we can derive by the leftmost rule of the next-to-last row of Figure 3.
Lemma 4.7
Let be a sequence of elementary contexts, of type . For every context , for every term , .
Proof. By the redex discovery rule, , so by Lemma 4.6. Conversely, if is derivable, then we show that is derivable by induction on . If , this is clear. Otherwise, there are only two rules that allow us to derive . In the case of the first of these rules (the middle rule of the first of the three rows of rules), , and we can derive by the same rule. In the case of the other rule, was derived from a shorter derivation of , where , using the redex discovery rule . By induction hypothesis, is derivable, namely is derivable.
Lemma 4.8
Let be a sequence of elementary contexts. If then .
Proof. , by Lemma 4.6 and Lemma 4.7.
For short, let us write for .
Lemma 4.9
Let be any context of type . For every term , .
Proof. Let us write as where is an initial context and is a sequence of elementary contexts. We first show that . Once this is done, Lemma 4.7 states that , and that will finish the proof.
We assume , otherwise the claim is trivial. Then . Indeed, if , and if . By Lemma 4.6, .
In the converse direction, assume that is derivable. If , then is also derivable. Otherwise, if , then the only remaining possible derivation is obtained from a smaller derivation of , so is again derivable. If and , then we can only have derived from a smaller derivation of , and then from another derivation of , namely . Since that holds for every , .
5 Soundness
We let the rank of a type be [math] for a value type that is not of the form , for types of the form , and for computation types. This will play a key role in our soundness proof, for the following reason: for every elementary or initial context , the rank of is less than or equal to the rank of . Hence if is of type , and is of type , then every has rank between those of and .
Beyond its role as a technical aide, the concept of rank is profitably interpreted from the point of view of the type and effect discipline [21]. While the separation between value types and computation types exhibits two kinds of effects, ranks refine this further by distinguishing between rank [math] value types, where the only effect is recursion, from rank value types, where probabilistic choice is also allowed. Rank types further allow for non-deterministic choice effects. With that viewpoint, one might be puzzled by the fact that the rank [math] types are able to encapsulate arbitrary rank types. However, the typical inhabitants of types are thunks , which do not execute, hence do not produce any side effect, unless being forced to, using the operation, yielding again a value of the rank type .
We will also need to define the semantics of contexts so that \left\llbracket{C[M]}\right\rrbracket\rho=\left\llbracket{C}\right\rrbracket\rho(\left\llbracket{M}\right\rrbracket\rho) for every and for every environment . \left\llbracket{E_{0}E_{1}E_{2}\cdots E_{n}}\right\rrbracket\rho is the composition of \left\llbracket{E_{0}}\right\rrbracket\rho, \left\llbracket{E_{1}}\right\rrbracket\rho, \left\llbracket{E_{2}}\right\rrbracket\rho, …, \left\llbracket{E_{n}}\right\rrbracket\rho, where:
- •
\left\llbracket{[\_N]}\right\rrbracket\rho maps to f(\left\llbracket{N}\right\rrbracket\rho),
- •
\left\llbracket{[{\_}\mathrel{\boldsymbol{\mathtt{to}}}{x_{\sigma}}\mathrel{\boldsymbol{\mathtt{in}}}{N}]}\right\rrbracket\rho={(V\in\left\llbracket{\sigma}\right\rrbracket\mapsto\left\llbracket{N}\right\rrbracket\rho[x_{\sigma}\mapsto V])}^{*},
- •
\left\llbracket{[\mathop{\boldsymbol{\mathtt{force}}}\_]}\right\rrbracket\rho is the identity map,
- •
\left\llbracket{[\mathop{\boldsymbol{\mathtt{succ}}}\_]}\right\rrbracket\rho maps to and otherwise adds one,
- •
\left\llbracket{[\mathop{\boldsymbol{\mathtt{pred}}}\_]}\right\rrbracket\rho maps to and otherwise subtracts one,
- •
\left\llbracket{[\boldsymbol{\mathtt{ifz}}\;\_\;N\;P]}\right\rrbracket\rho maps [math] to \left\llbracket{N}\right\rrbracket\rho, every non-zero number to \left\llbracket{P}\right\rrbracket\rho and to ,
- •
\left\llbracket{[\_;N]}\right\rrbracket\rho maps to \left\llbracket{N}\right\rrbracket\rho, and to ,
- •
\left\llbracket{[\pi_{1}\_]}\right\rrbracket\rho is first projection,
- •
\left\llbracket{[\pi_{2}\_]}\right\rrbracket\rho is second projection,
- •
\left\llbracket{[\mathop{\boldsymbol{\mathtt{do}}}\nolimits{x_{\sigma}\leftarrow\_};N]}\right\rrbracket\rho={(V\in\left\llbracket{\sigma}\right\rrbracket\mapsto\left\llbracket{N}\right\rrbracket\rho[x_{\sigma}\mapsto V])}^{\dagger},
- •
\left\llbracket{[\mathop{\boldsymbol{\mathtt{produce}}}\_]}\right\rrbracket\rho=\eta^{\mathcal{Q}}, and
- •
\left\llbracket{[\mathop{\boldsymbol{\mathtt{produce}}}\mathop{\boldsymbol{\mathtt{ret}}}\nolimits\_]}\right\rrbracket\rho maps to .
Proposition 5.1** (Soundness)**
Let , , where is a value or computation type, and let . In CBPV, in CBPV, in CBPV, and in CBPV:
For every , if is derivable, then either \left\llbracket{C[M]}\right\rrbracket\rho=\bot and , or \left\llbracket{C[M]}\right\rrbracket\rho\neq\bot and for every \nu\in\left\llbracket{C[M]}\right\rrbracket\rho, . 2. 2.
If \left\llbracket{C[M]}\right\rrbracket\rho=\bot then , otherwise for every \nu\in\left\llbracket{C[M]}\right\rrbracket\rho, .
Proof. Item 2 is an easy consequence of item 1, which we prove by induction on the derivation.
In the case of the first rule (), , and \left\llbracket{C[M]}\right\rrbracket\neq\bot. For every \nu\in\left\llbracket{C[M]}\right\rrbracket\rho=\eta^{\mathcal{Q}}(\delta_{\top}), we have , so , and certainly for every .
The case of the second rule is obvious.
The case of the leftmost rule of the next row follows from the observation that if , then \left\llbracket{C[M]}\right\rrbracket\rho=\left\llbracket{C^{\prime}[M^{\prime}]}\right\rrbracket\rho. We use the standard substitution lemma \left\llbracket{M}\right\rrbracket(\rho[x_{\sigma}\mapsto\left\llbracket{N}\right\rrbracket\rho])=\left\llbracket{M[x_{\sigma}:=N]}\right\rrbracket\rho in the case of -reduction (): the value of the left-hand side is \left\llbracket{C}\right\rrbracket\rho(\left\llbracket{M}\right\rrbracket(\rho[x_{\sigma}\mapsto\left\llbracket{N}\right\rrbracket\rho])), and the value of the right-hand side is \left\llbracket{C}\right\rrbracket\rho(\left\llbracket{M[x_{\sigma}:=N]}\right\rrbracket\rho)). In the case of , we also use the fact that {(V\in\left\llbracket{\sigma}\right\rrbracket\mapsto\left\llbracket{N}\right\rrbracket\rho[x_{\sigma}:=V])}^{*}(\eta^{\mathcal{Q}}(\left\llbracket{M}\right\rrbracket\rho))=\left\llbracket{N}\right\rrbracket\rho[x_{\sigma}\mapsto\left\llbracket{M}\right\rrbracket\rho] (Proposition 4.2, item 2). In the case of , we use the equality and the substitution lemma.
By our observation on ranks, if , where and for each , then all the types are computation types (rank ). In that case, can only be of one of the two forms , . (Further inspection would reveal that the first case is impossible, but we will not need that yet.) We now observe that in each case, \left\llbracket{E_{i}}\right\rrbracket\rho maps top to top: in the case of , this is by Proposition 4.2, item 3. It follows that \left\llbracket{C}\right\rrbracket\rho also maps top to top, whence \left\llbracket{C[\mathop{\boldsymbol{\mathtt{abort}}}\nolimits_{\boldsymbol{\mathtt{F}}{}\sigma}]}\right\rrbracket\rho=\left\llbracket{C}\right\rrbracket\rho(\left\llbracket{\mathop{\boldsymbol{\mathtt{abort}}}\nolimits_{\boldsymbol{\mathtt{F}}{}\sigma}}\right\rrbracket\rho)=\left\llbracket{C}\right\rrbracket\rho(\emptyset)=\emptyset. As a consequence, \left\llbracket{C[\mathop{\boldsymbol{\mathtt{abort}}}\nolimits_{\boldsymbol{\mathtt{F}}{}\sigma}]}\right\rrbracket\rho\neq\bot, and the claim that for every \nu\in\left\llbracket{C[\mathop{\boldsymbol{\mathtt{abort}}}\nolimits_{\boldsymbol{\mathtt{F}}{}\sigma}]}\right\rrbracket\rho, is vacuously true: the rule that derives for every is sound.
Similarly, and still assuming , for each , \left\llbracket{E_{i}}\right\rrbracket\rho preserves binary infima. When , this is because the function {(V\in\left\llbracket{\sigma}\right\rrbracket\mapsto\left\llbracket{N}\right\rrbracket\rho[x_{\sigma}\mapsto V])}^{*} maps binary infima to binary infima by Proposition 4.2, item 3. When , \left\llbracket{[\_N]}\right\rrbracket\rho maps every to f(\left\llbracket{N}\right\rrbracket\rho), and therefore preserves binary infima by Lemma 4.3, item 2. It follows that \left\llbracket{C}\right\rrbracket\rho preserves binary infima. We apply this to the rightmost rule of the middle row (if and then ). We have \left\llbracket{C[M\owedge N]}\right\rrbracket\rho=\left\llbracket{C}\right\rrbracket\rho(\left\llbracket{M}\right\rrbracket\rho\wedge\left\llbracket{N}\right\rrbracket\rho)=\left\llbracket{C}\right\rrbracket\rho(\left\llbracket{M}\right\rrbracket\rho)\wedge\left\llbracket{C}\right\rrbracket\rho(\left\llbracket{N}\right\rrbracket\rho)=\left\llbracket{C[M]}\right\rrbracket\rho\wedge\left\llbracket{C[N]}\right\rrbracket\rho.
In particular, if \left\llbracket{C[M\owedge N]}\right\rrbracket\rho=\bot, and since implies or in any space of the form , then \left\llbracket{C[M]}\right\rrbracket\rho or \left\llbracket{C[N]}\right\rrbracket\rho is equal to . By symmetry, let us assume that \left\llbracket{C[M]}\right\rrbracket\rho=\bot. By induction hypothesis, the only value of such that is derivable is . There are only two rules that can end a derivation of , and they both require .
If \left\llbracket{C[M\owedge N]}\right\rrbracket\rho\neq\bot, then \left\llbracket{C[M]}\right\rrbracket\rho\neq\bot and \left\llbracket{C[N]}\right\rrbracket\rho\neq\bot, so by induction hypothesis, for every in \left\llbracket{C[M]}\right\rrbracket\rho, and for every in \left\llbracket{C[N]}\right\rrbracket\rho, . Hence this holds for every \nu\in\left\llbracket{C[M\owedge N]}\right\rrbracket\rho=\left\llbracket{C[M]}\right\rrbracket\rho\wedge\left\llbracket{C[N]}\right\rrbracket\rho=\left\llbracket{C[M]}\right\rrbracket\rho\cup\left\llbracket{C[N]}\right\rrbracket\rho.
Let us deal with the last of the CBPV rules (middle rule, middle row of Figure 3): we have deduced from and , hence by induction hypothesis: either \left\llbracket{C[M]}\right\rrbracket\rho=\bot and , or for every \nu\in\left\llbracket{C[M]}\right\rrbracket\rho, ; and either \left\llbracket{C[N]}\right\rrbracket\rho=\bot and , or for every \nu\in\left\llbracket{C[N]}\right\rrbracket\rho, . In that case has type for some value type , and every intermediate type must therefore have rank or . The only eligible elementary contexts () are of the form , , or . In each case, the rank of is equal to that of . Since has rank and has rank , cannot be . It cannot be either since has rank [math]. Hence is equal to , and every () is of the form . We note that \left\llbracket{[\mathop{\boldsymbol{\mathtt{do}}}\nolimits{x_{\sigma}\leftarrow\_};N]}\right\rrbracket\rho={(V\in\left\llbracket{\sigma}\right\rrbracket\mapsto\left\llbracket{N}\right\rrbracket\rho[x_{\sigma}\mapsto V])}^{\dagger} is a linear map, i.e., preserves sums and scalar multiplication. Indeed the formula is linear in . It follows that \left\llbracket{E_{1}E_{2}\cdots E_{n}}\right\rrbracket\rho is also linear, so \left\llbracket{E_{1}E_{2}\cdots E_{n}[M\oplus N]}\right\rrbracket\rho=\left\llbracket{E_{1}E_{2}\cdots E_{n}}\right\rrbracket\rho(\frac{1}{2}(\left\llbracket{M}\right\rrbracket\rho+\left\llbracket{N}\right\rrbracket\rho))=\frac{1}{2}(\nu_{1}+\nu_{2}), where \nu_{1}=\left\llbracket{E_{1}E_{2}\cdots E_{n}[M]}\right\rrbracket\rho and \nu_{2}=\left\llbracket{E_{1}E_{2}\cdots E_{n}[N]}\right\rrbracket\rho. Note that \left\llbracket{C[M]}\right\rrbracket\rho=\eta^{\mathcal{Q}}(\nu_{1})=\mathop{\uparrow}\nolimits\nu_{1}, and similarly \left\llbracket{C[N]}\right\rrbracket\rho=\mathop{\uparrow}\nolimits\nu_{2}, and that those values are different from . Similarly, \left\llbracket{C[M\oplus N]}\right\rrbracket\rho=\mathop{\uparrow}\nolimits(\frac{1}{2}(\nu_{1}+\nu_{2})) is different from . Since \nu_{1}\in\left\llbracket{C[M]}\right\rrbracket\rho, we obtain that by . Similarly, . Using the fact that, for all , if and only if or , . For every \nu\in\left\llbracket{C[M\oplus N]}\right\rrbracket\rho=\mathop{\uparrow}\nolimits(\frac{1}{2}(\nu_{1}+\nu_{2})), and we therefore obtain that .
We turn to the rules of the bottom row, which are specific to the extensions of CBPV with , or , or both. For the first one, by induction hypothesis either \left\llbracket{M}\right\rrbracket\rho=\bot and then , or else for every \mu\in\left\llbracket{M}\right\rrbracket\rho. The first case is impossible since it is a requirement of the syntax of that be non-zero. This implies that \left\llbracket{\bigcirc_{>b}M}\right\rrbracket\rho=\top. It follows that \left\llbracket{C[\bigcirc_{>b}M]}\right\rrbracket\rho=\left\llbracket{C}\right\rrbracket\rho(\left\llbracket{\bigcirc_{>b}M}\right\rrbracket\rho)=\left\llbracket{C}\right\rrbracket\rho(\top)=\left\llbracket{C[\underline{*}]}\right\rrbracket\rho. By induction hypothesis again, either \left\llbracket{C[\underline{*}]}\right\rrbracket\rho=\bot and , or for every in \left\llbracket{C[\underline{*}]}\right\rrbracket\rho. Hence either \left\llbracket{C[\bigcirc_{>b}M]}\right\rrbracket\rho=\bot and , or for every in \left\llbracket{C[\bigcirc_{>b}M]}\right\rrbracket\rho.
For the last two, we note that, in all three cases on \left\llbracket{M}\right\rrbracket\rho (equal to , to [math], or other), \left\llbracket{C[\boldsymbol{\mathtt{pifz}}\;M\;N\;P]}\right\rrbracket\rho is equal to one of the terms \left\llbracket{C[\boldsymbol{\mathtt{ifz}}\;M\;N\;P]}\right\rrbracket\rho or \left\llbracket{C[N\owedge P]}\right\rrbracket\rho, and is larger than or equal to the other one. In other words, \left\llbracket{C[\boldsymbol{\mathtt{pifz}}\;M\;N\;P]}\right\rrbracket\rho=\max(\left\llbracket{C[\boldsymbol{\mathtt{ifz}}\;M\;N\;P]}\right\rrbracket\rho,\left\llbracket{C[N\owedge P]}\right\rrbracket\rho). If that is equal to , then both terms \left\llbracket{C[\boldsymbol{\mathtt{ifz}}\;M\;N\;P]}\right\rrbracket\rho and \left\llbracket{C[N\owedge P]}\right\rrbracket\rho are equal to , so by induction hypothesis the only derivations of and are such that . Hence the only derivations of are such that , using any of the three possible rules. If \left\llbracket{C[\boldsymbol{\mathtt{pifz}}\;M\;N\;P]}\right\rrbracket\rho\neq\bot, then let us assume that by any of the last two rules. If , then certainly for every \nu\in\left\llbracket{C[\boldsymbol{\mathtt{pifz}}\;M\;N\;P]}\right\rrbracket\rho. Otherwise, by induction hypothesis we have \left\llbracket{C[\boldsymbol{\mathtt{ifz}}\;M\;N\;P]}\right\rrbracket\rho\neq\bot and for every \nu\in\left\llbracket{C[\boldsymbol{\mathtt{ifz}}\;M\;N\;P]}\right\rrbracket\rho, or \left\llbracket{C[N\owedge P]}\right\rrbracket\rho\neq\bot and for every \nu\in\left\llbracket{C[N\owedge P]}\right\rrbracket\rho. Since \left\llbracket{C[\boldsymbol{\mathtt{pifz}}\;M\;N\;P]}\right\rrbracket\rho=\max(\left\llbracket{C[\boldsymbol{\mathtt{ifz}}\;M\;N\;P]}\right\rrbracket\rho,\left\llbracket{C[N\owedge P]}\right\rrbracket\rho), and means smallest with respect to inclusion (for non-bottom elements), in particular for every \nu\in\left\llbracket{C[\boldsymbol{\mathtt{pifz}}\;M\;N\;P]}\right\rrbracket\rho.
6 Adequacy
Adequacy is proved through the use of a suitable logical relation , where relates ground terms of type with elements of \left\llbracket{{\overline{\sigma}}}\right\rrbracket. (A term is ground if and only if it has no free variable. We define ground contexts similarly.) Again we work in CBPV or any of its extensions with or or both, without further mention.
Defining necessitates that we also define auxiliary relations between ground contexts (resp., between ground contexts ) and continuous maps h\colon\left\llbracket{\sigma}\right\rrbracket\to[0,1]. This pattern is similar to the technique of -lifting, and particularly to Katsumata’s -logical predicates [15]. We write “for all ” instead of “for every ground context and for every continuous map h\colon\left\llbracket{\sigma}\right\rrbracket\to[0,1] such that ”, instead of “for every ground context and for every continuous map h\colon\left\llbracket{\sigma}\right\rrbracket\to[0,1] such that ”, and instead of “for every ground term and for every a\in\left\llbracket{\sigma}\right\rrbracket such that ”. We define:
- •
iff ;
- •
if , and always;
- •
if , and always;
- •
if and only if and ;
- •
if and only if \mathop{\text{Pr}}(C\cdot M\mathbin{\downarrow})\geq\int_{x\in\left\llbracket{\sigma}\right\rrbracket}h(x)d\nu for all ;
- •
if and only if for all ;
- •
if and only if for all , ; here is any continuous map from \left\llbracket{\sigma}\right\rrbracket to the continuous complete lattice , so makes sense: , and if , then —which is equal to if ;
- •
if and only if for all ;
- •
if and only if for all .
Lemma 6.1
For all ground terms , if and then .
Proof. By induction on . If , then means that . For every ground context , and by Lemma 4.7. Since , , so . It follows that . By induction hypothesis, , whence .
If , then means that , or that and . In the first case, holds vacuously. In the second case, , so again. The case is dealt with similarly—in the second case, and has to be replaced by .
If , then means that and , where . We note that for every ground context , by Lemma 4.7. In turn, since and using Lemma 4.7 again. Therefore . By induction hypothesis, . Similarly, , so .
If , then means that for some \nu\in\mathbf{V}_{\leq 1}(\left\llbracket{\sigma}\right\rrbracket), and that \mathop{\text{Pr}}(C\cdot M\mathbin{\downarrow})\geq\int_{x\in\left\llbracket{\sigma}\right\rrbracket}h(x)d\nu for all . For all such and , is even larger, so .
If , then means that for all , . Then is even larger, so .
If , then means that is some function f\in[\left\llbracket{\sigma}\right\rrbracket\to\left\llbracket{\underline{\tau}}\right\rrbracket], and that for all , . For every ground context , , by Lemma 4.7, the assumption , and Lemma 4.7 again. Hence . By induction hypothesis, . It follows that .
For each type , and every ground term , let us write for the set of values a\in\left\llbracket{{\overline{\sigma}}}\right\rrbracket such that .
Lemma 6.2
For every type , for every ground term , is Scott-closed and contains .
Proof. This is an easy induction on types. Only the cases and need some care. In the case , is Scott-closed because integration is Scott-continuous in the valuation. Explicitly, it is upwards-closed, and for every directed family in , with supremum , for all , \mathop{\text{Pr}}(C\cdot M\mathbin{\downarrow})\geq\int_{x\in\left\llbracket{\sigma}\right\rrbracket}h(x)d\nu_{i} for every , so \mathop{\text{Pr}}(C\cdot M\mathbin{\downarrow})\geq\sup_{i\in I}\int_{x\in\left\llbracket{\sigma}\right\rrbracket}h(x)d\nu_{i}=\int_{x\in\left\llbracket{\sigma}\right\rrbracket}h(x)d\nu. In order to show that contains (the zero valuation), we must show that \mathop{\text{Pr}}(C\cdot M\mathbin{\downarrow})\geq\int_{x\in\left\llbracket{\sigma}\right\rrbracket}h(x)d0=0 for all , and that is trivial.
In the case , let us fix and so that . Since is continuous by Proposition 4.2, item 2, \{Q\in\mathcal{Q}^{\top}_{\bot}(\left\llbracket{\sigma}\right\rrbracket)\mid{h}^{*}(Q)>r\}={({h}^{*})}^{-1}((r,\infty]) is open for every . By taking complements, the set F_{C,h}=\{Q\in\mathcal{Q}^{\top}_{\bot}(\left\llbracket{\sigma}\right\rrbracket)\mid{h}^{*}(Q)\leq\mathop{\text{Pr}}(C\cdot M\mathbin{\downarrow})\} is closed. Hence is closed in \mathcal{Q}^{\top}_{\bot}(\left\llbracket{\sigma}\right\rrbracket). Finally, contains because is strict, hence .
Let us say that a term has as sole free variable if and only if the set of free variables of is included in , namely if is ground or if the only free variable of is . In that case, for every ground term , is ground.
Corollary 6.3
Let have as sole free variable, let be a Scott-continuous map from \left\llbracket{\sigma}\right\rrbracket to \left\llbracket{\sigma}\right\rrbracket, and assume that for all , . Then .
Proof. We show that for every . Since contains by Lemma 6.2, this is true when . If , then by assumption. We now use the fact that for every ground context , , hence , by Lemma 4.6. Using Lemma 6.1, we obtain that .
Since for every and since is Scott-closed (Lemma 6.2), .
Lemma 6.4
Let be a value type. For all , .
Proof. Let be a ground context of type , be a continuous map from \left\llbracket{\sigma}\right\rrbracket to , and assume that . By definition of , and since , , and h(V)=\int_{x\in\left\llbracket{\sigma}\right\rrbracket}h(x)d\delta_{V}.
Lemma 6.5
Let and be two value types. Let be a term with as sole free variable, f\in[\left\llbracket{\sigma}\right\rrbracket\to\left\llbracket{\boldsymbol{\mathtt{V}}\tau}\right\rrbracket], and assume that for all , . For all , .
Proof. Let be a ground context, and be a Scott-continuous map from \left\llbracket{\tau}\right\rrbracket to such that . We wish to show that \mathop{\text{Pr}}(C\cdot\mathop{\boldsymbol{\mathtt{do}}}\nolimits{x_{\sigma}\leftarrow M};N\mathbin{\downarrow})\geq\int_{y\in\left\llbracket{\tau}\right\rrbracket}h(y)df^{\dagger}(\nu), namely that \mathop{\text{Pr}}(C\cdot\mathop{\boldsymbol{\mathtt{do}}}\nolimits{x_{\sigma}\leftarrow M};N\mathbin{\downarrow})\geq\int_{x\in\left\llbracket{\sigma}\right\rrbracket}\allowbreak(\int_{y\in\left\llbracket{\tau}\right\rrbracket}h(y)df(x))d\nu, using (1).
We first show that , where g(x)=\int_{y\in\left\llbracket{\tau}\right\rrbracket}h(y)df(x) for every x\in\left\llbracket{\sigma}\right\rrbracket. That reduces to showing that for all . Now , so , by Lemma 4.6, and \mathop{\text{Pr}}(C\cdot N[x_{\sigma}:=P]\mathbin{\downarrow})\geq g(x)=\int_{y\in\left\llbracket{\tau}\right\rrbracket}h(y)df(x) because and for all .
Using this together with the fact that , \mathop{\text{Pr}}(C[\mathop{\boldsymbol{\mathtt{do}}}\nolimits{x_{\sigma}\leftarrow\_};N]\cdot M\mathbin{\downarrow})\geq\int_{x\in\left\llbracket{\sigma}\right\rrbracket}g(x)d\nu. Since , by Lemma 4.6, \mathop{\text{Pr}}(C\cdot\mathop{\boldsymbol{\mathtt{do}}}\nolimits{x_{\sigma}\leftarrow M};N\mathbin{\downarrow})\geq\int_{x\in\left\llbracket{\sigma}\right\rrbracket}g(x)d\nu.
Lemma 6.6
Let be a value type. For all , .
Proof. Let . Let be a ground context of type , be a continuous map from \left\llbracket{\sigma}\right\rrbracket to , and assume that . By definition of , . Since , , so .
Lemma 6.7
Let , be two value types. Let be a term with as sole free variable, f\in[\left\llbracket{\sigma}\right\rrbracket\to\left\llbracket{\boldsymbol{\mathtt{F}}{}\tau}\right\rrbracket], and assume that for all , . For all , .
Proof. Let be a ground context, and be a Scott-continuous map from \left\llbracket{\tau}\right\rrbracket to such that . We wish to show that . Using Proposition 4.2, we will show the equivalent claim that .
We first show that . For all , we aim to show that . Since and , . Since , by Lemma 4.6 , as desired.
Knowing that , and using , we obtain that . Since , by Lemma 4.6 .
We write for the characteristic map of an open subset of a space .
Lemma 6.8
; 2. 2.
.
Proof.
-
Let . It suffices to show that . If , then the right-hand side is [math], and the inequality is clear. Otherwise, we claim that the left-hand side is (greater than or) equal to . We have , so by Lemma 4.6. Since , , and since we can deduce for every .
-
Let . It suffices to show that . Since by item 1, \mathop{\text{Pr}}([\mathop{\boldsymbol{\mathtt{produce}}}\_]\cdot M\mathbin{\downarrow})\geq\int_{x\in\left\llbracket{\boldsymbol{\mathtt{unit}}}\right\rrbracket}\chi_{\{\top\}}(x)\allowbreak d\nu=\nu(\{\top\}). We use Lemma 4.6 together with and we obtain the desired inequality.
A substitution is a map of finite domain from pairwise distinct variables to ground terms of the same type as . We omit the definition of (parallel) substitution application . The case is the special case . We note that when is distinct from , …, , and not free in , …, . Also, if contains all the free variables of , then is ground.
We define the relation between substitutions and environments by if and only if for every , .
Proposition 6.9
For every type , for every term of CBPV or any of its extensions with or or both, for every substitution whose domain contains all the free variables of , for every environment , if then M\theta\mathrel{R}_{\overline{\sigma}}\left\llbracket{M}\right\rrbracket\rho.
Proof. By induction on . This is the assumption when is a variable.
In the case of -abstractions , let us write as , and assume by -renaming that is different from every and free in no . For all , we define as and we observe that , so by induction hypothesis M\theta^{\prime}\mathrel{R}_{\underline{\tau}}\left\llbracket{M}\right\rrbracket\rho[x_{\sigma}\mapsto V]. Hence M\theta[x_{\sigma}:=N]\mathrel{R}_{\underline{\tau}}\left\llbracket{M}\right\rrbracket\rho[x_{\sigma}\mapsto V]. By Lemma 4.6 and Lemma 6.1, using the fact that for all ground contexts , we obtain that (\lambda x_{\sigma}.M\theta)N\mathrel{R}_{\underline{\tau}}\left\llbracket{M}\right\rrbracket\rho[x_{\sigma}\mapsto V]. Since that holds for all , (\lambda x_{\sigma}.M)\theta=\lambda x_{\sigma}.M\theta\mathrel{R}_{\sigma\to\underline{\tau}}\left\llbracket{\lambda x_{\sigma}.M}\right\rrbracket\rho.
The case of applications is by definition of .
For terms of the form , by assumption M\theta\mathrel{R}_{\sigma}\left\llbracket{M}\right\rrbracket\rho. By Lemma 6.6, \mathop{\boldsymbol{\mathtt{produce}}}M\theta\mathrel{R}_{\boldsymbol{\mathtt{F}}{}\sigma}\eta^{\mathcal{Q}}(\left\llbracket{M}\right\rrbracket\rho)=\left\llbracket{\mathop{\boldsymbol{\mathtt{produce}}}M}\right\rrbracket\rho.
For terms of the form where and , as for -abstractions we write as , and we assume by that is different from every and free in no . By induction hypothesis M\theta\mathrel{R}_{\boldsymbol{\mathtt{F}}{}\sigma}\left\llbracket{M}\right\rrbracket\rho, and for all , N\theta^{\prime}\mathrel{R}_{\boldsymbol{\mathtt{F}}{}\tau}\left\llbracket{N}\right\rrbracket\rho[x_{\sigma}:=V] where . As for -abstractions, the latter means that N\theta[x_{\sigma}:=P]\mathrel{R}_{\boldsymbol{\mathtt{F}}{}\tau}\left\llbracket{N}\right\rrbracket\rho[x_{\sigma}:=V]. Letting be the map V\in\left\llbracket{\sigma}\right\rrbracket\mapsto\left\llbracket{N}\right\rrbracket\rho[x_{\sigma}:=V], therefore, for all . By Lemma 6.7, ({M}\mathrel{\boldsymbol{\mathtt{to}}}{x_{\sigma}}\mathrel{\boldsymbol{\mathtt{in}}}{N})\theta={M\theta}\mathrel{\boldsymbol{\mathtt{to}}}{x_{\sigma}}\mathrel{\boldsymbol{\mathtt{in}}}{N\theta}\mathrel{R}_{\boldsymbol{\mathtt{F}}{}\tau}{f}^{*}(\left\llbracket{M}\right\rrbracket\rho)=\left\llbracket{{M}\mathrel{\boldsymbol{\mathtt{to}}}{x_{\sigma}}\mathrel{\boldsymbol{\mathtt{in}}}{N}}\right\rrbracket\rho.
For terms , by induction hypothesis M\theta\mathrel{R}_{\underline{\tau}}\left\llbracket{M}\right\rrbracket\rho. For every ground context , , so by Lemma 4.6 and Lemma 6.1, \mathop{\boldsymbol{\mathtt{force}}}\mathop{\boldsymbol{\mathtt{thunk}}}M\mathrel{R}_{\underline{\tau}}\left\llbracket{M}\right\rrbracket\rho. By definition of , \mathop{\boldsymbol{\mathtt{thunk}}}M\theta\mathrel{R}_{\boldsymbol{\mathtt{U}}\underline{\tau}}\left\llbracket{M}\right\rrbracket\rho=\left\llbracket{\mathop{\boldsymbol{\mathtt{thunk}}}M}\right\rrbracket\rho.
The case of terms of the form is by definition of .
In the case of , we have by definition. Similarly, .
For terms with , by induction hypothesis M\theta\mathrel{R}_{\boldsymbol{\mathtt{int}}}\left\llbracket{M}\right\rrbracket\rho. If \left\llbracket{M}\right\rrbracket\rho=\bot, then \mathop{\boldsymbol{\mathtt{succ}}}M\theta\mathrel{R}_{\boldsymbol{\mathtt{int}}}\bot=\left\llbracket{\mathop{\boldsymbol{\mathtt{succ}}}M}\right\rrbracket\rho. Otherwise, let n=\left\llbracket{M}\right\rrbracket\rho\in\mathbb{Z}. By definition, for every ground context . Replacing by , . Since and since , using Lemma 4.6 we obtain . This shows that \mathop{\boldsymbol{\mathtt{succ}}}M\theta\mathrel{R}_{\boldsymbol{\mathtt{int}}}\underline{n+1}=\left\llbracket{\mathop{\boldsymbol{\mathtt{succ}}}M}\right\rrbracket\rho. The case of terms is similar.
For terms , by induction hypothesis M\theta\mathrel{R}_{\boldsymbol{\mathtt{int}}}\left\llbracket{M}\right\rrbracket\rho, N\theta\mathrel{R}_{\overline{\sigma}}\left\llbracket{N}\right\rrbracket\rho, and P\theta\mathrel{R}_{\overline{\sigma}}\left\llbracket{P}\right\rrbracket\rho. If \left\llbracket{M}\right\rrbracket\rho=\bot, then (\boldsymbol{\mathtt{ifz}}\;M\;N\;P)\theta\mathrel{R}_{\overline{\sigma}}\bot=\left\llbracket{\boldsymbol{\mathtt{ifz}}\;M\;N\;P}\right\rrbracket\rho, by Lemma 6.2. Otherwise, let n=\left\llbracket{M}\right\rrbracket\rho\in\mathbb{Z}. Since M\theta\mathrel{R}_{\boldsymbol{\mathtt{int}}}\left\llbracket{M}\right\rrbracket\rho, for every ground context . In particular, for every ground context , . Using Lemma 4.7, it follows that . Since reduces to if , and to if , by Lemma 4.6, is larger than or equal to if , and to otherwise. By Lemma 6.1, \boldsymbol{\mathtt{ifz}}\;M\theta\;N\theta\;P\theta\mathrel{R}_{\overline{\sigma}}\left\llbracket{N}\right\rrbracket\rho if , and \boldsymbol{\mathtt{ifz}}\;M\theta\;N\theta\;P\theta\mathrel{R}_{\overline{\sigma}}\left\llbracket{P}\right\rrbracket\rho if . In any case, (\boldsymbol{\mathtt{ifz}}\;M\;N\;P)\theta=\boldsymbol{\mathtt{ifz}}\;M\theta\;N\theta\;P\theta\mathrel{R}_{\overline{\sigma}}\left\llbracket{\boldsymbol{\mathtt{ifz}}\;M\;N\;P}\right\rrbracket\rho.
The case of terms is similar. By induction hypothesis, M\theta\mathrel{R}_{\boldsymbol{\mathtt{unit}}}\left\llbracket{M}\right\rrbracket\rho and N\theta\mathrel{R}_{\overline{\sigma}}\left\llbracket{N}\right\rrbracket\rho. If \left\llbracket{M}\right\rrbracket\rho=\bot, then \left\llbracket{M;N}\right\rrbracket\rho=\bot, so (M;N)\theta\mathrel{R}_{\overline{\sigma}}\left\llbracket{M;N}\right\rrbracket\rho by Lemma 6.2. Otherwise, \left\llbracket{M}\right\rrbracket\rho=\top, so , meaning that for every ground context . In particular, for every ground context , . By Lemma 4.7, , and by Lemma 4.6, , using the rule . Hence . By Lemma 6.1, (M;N)\theta=M\theta;N\theta\mathrel{R}_{\overline{\sigma}}\left\llbracket{N}\right\rrbracket\rho=\left\llbracket{M;N}\right\rrbracket\rho.
The case of terms and follows from the definition of .
For terms , by induction hypothesis M\theta\mathrel{R}_{\sigma}\left\llbracket{M}\right\rrbracket\rho and N\theta\mathrel{R}_{\tau}\left\llbracket{N}\right\rrbracket\rho. For every ground context , , so by Lemma 4.6 and Lemma 6.1, \pi_{1}\langle M,N\rangle\theta=\pi_{1}\langle M\theta,\allowbreak N\theta\rangle\mathrel{R}_{\sigma}\left\llbracket{M}\right\rrbracket\rho. Similarly, \pi_{2}\langle M,N\rangle\theta\mathrel{R}_{\tau}\left\llbracket{N}\right\rrbracket\rho. By definition of , it follows that \langle M,N\rangle\theta\mathrel{R}_{\sigma\times\tau}\left\llbracket{\langle M,N\rangle}\right\rrbracket\rho.
For terms , by induction hypothesis M\theta\mathrel{R}_{\tau}\left\llbracket{M}\right\rrbracket\rho, so \mathop{\boldsymbol{\mathtt{ret}}}\nolimits M\theta\mathrel{R}_{\boldsymbol{\mathtt{V}}{}\tau}\delta_{\left\llbracket{M}\right\rrbracket\rho}=\left\llbracket{\mathop{\boldsymbol{\mathtt{ret}}}\nolimits M}\right\rrbracket\rho by Lemma 6.4.
For terms where and , as for -abstractions we write as , and we assume that is different from every and free in no . By induction hypothesis M\theta\mathrel{R}_{\boldsymbol{\mathtt{V}}{}\sigma}\left\llbracket{M}\right\rrbracket\rho, and for all , N\theta^{\prime}\mathrel{R}_{\boldsymbol{\mathtt{V}}{}\tau}\left\llbracket{N}\right\rrbracket\rho[x_{\sigma}:=V] where . As for -abstractions, the latter means that N\theta[x_{\sigma}:=P]\mathrel{R}_{\boldsymbol{\mathtt{V}}{}\tau}\left\llbracket{N}\right\rrbracket\rho[x_{\sigma}:=V]. Letting be the map V\in\left\llbracket{\sigma}\right\rrbracket\mapsto\left\llbracket{N}\right\rrbracket\rho[x_{\sigma}:=V], therefore, for all . By Lemma 6.5, (\mathop{\boldsymbol{\mathtt{do}}}\nolimits{x_{\sigma}\leftarrow M};N)\theta=\mathop{\boldsymbol{\mathtt{do}}}\nolimits{x_{\sigma}\leftarrow M\theta};(N\theta)\mathrel{R}_{\boldsymbol{\mathtt{V}}{}\tau}f^{\dagger}(\left\llbracket{M}\right\rrbracket\rho)=\left\llbracket{\mathop{\boldsymbol{\mathtt{do}}}\nolimits{x_{\sigma}\leftarrow M};N}\right\rrbracket\rho.
For terms , by induction hypothesis M\theta\mathrel{R}_{\tau}\left\llbracket{M}\right\rrbracket\rho and N\theta\mathrel{R}_{\tau}\left\llbracket{N}\right\rrbracket\rho. For all , \mathop{\text{Pr}}(C\cdot M\theta\mathbin{\downarrow})\geq\int_{x\in\left\llbracket{\tau}\right\rrbracket}h(x)d\left\llbracket{M}\right\rrbracket\rho, and \mathop{\text{Pr}}(C\cdot N\theta\mathbin{\downarrow})\geq\int_{x\in\left\llbracket{\tau}\right\rrbracket}h(x)d\left\llbracket{N}\right\rrbracket\rho. For all and , if we can deduce and , then we can deduce . Therefore \mathop{\text{Pr}}(C\cdot(M\oplus N)\theta\mathbin{\downarrow})\geq\frac{1}{2}(\mathop{\text{Pr}}(C\cdot M\theta\mathbin{\downarrow})+\mathop{\text{Pr}}(C\cdot N\theta\mathbin{\downarrow}))\geq\frac{1}{2}(\int_{x\in\left\llbracket{\tau}\right\rrbracket}h(x)d\left\llbracket{M}\right\rrbracket\rho+\int_{x\in\left\llbracket{\tau}\right\rrbracket}h(x)d\left\llbracket{N}\right\rrbracket\rho)=\int_{x\in\left\llbracket{\tau}\right\rrbracket}h(x)d\left\llbracket{M\oplus N}\right\rrbracket\rho. Hence (M\oplus N)\theta\mathrel{R}_{\tau}\left\llbracket{M\oplus N}\right\rrbracket\rho.
The case of terms is similar, using the fact that instead. The latter follows from the fact that if we can deduce both and , then we can deduce . By induction hypothesis, M\theta\mathrel{R}_{\boldsymbol{\mathtt{F}}{}\tau}\left\llbracket{M}\right\rrbracket\rho and N\theta\mathrel{R}_{\boldsymbol{\mathtt{F}}{}\tau}\left\llbracket{N}\right\rrbracket\rho. For all , \mathop{\text{Pr}}(C\cdot M\theta\mathbin{\downarrow})\geq{h}^{*}(\left\llbracket{M}\right\rrbracket\rho) and \mathop{\text{Pr}}(C\cdot N\theta\mathbin{\downarrow})\geq{h}^{*}(\left\llbracket{N}\right\rrbracket\rho), so \mathop{\text{Pr}}(C\cdot(M\owedge N)\theta\mathbin{\downarrow})\geq\min({h}^{*}(\left\llbracket{M}\right\rrbracket\rho),{h}^{*}(\left\llbracket{N}\right\rrbracket\rho))={h}^{*}(\left\llbracket{M}\right\rrbracket\rho)\wedge{h}^{*}(\left\llbracket{N}\right\rrbracket\rho)={h}^{*}(\left\llbracket{M}\right\rrbracket\rho\wedge\left\llbracket{N}\right\rrbracket\rho) (because preserves binary infima, see Proposition 4.2, item 3) ={h}^{*}(\left\llbracket{M\owedge N}\right\rrbracket\rho). Hence (M\owedge N)\theta\mathrel{R}_{\boldsymbol{\mathtt{F}}{}\tau}\left\llbracket{M\owedge N}\right\rrbracket\rho.
For , we show that \mathop{\boldsymbol{\mathtt{abort}}}\nolimits_{\boldsymbol{\mathtt{F}}{}\tau}\mathrel{R}_{\boldsymbol{\mathtt{F}}{}\tau}\left\llbracket{\mathop{\boldsymbol{\mathtt{abort}}}\nolimits_{\boldsymbol{\mathtt{F}}{}\tau}}\right\rrbracket\rho=\emptyset () by showing that for all , . Indeed, by the rule (), .
For where , as for -abstractions, let us write as , and assume by -renaming that is different from every and free in no . For all , we define as and we observe that , so by induction hypothesis M\theta^{\prime}\mathrel{R}_{\sigma}\left\llbracket{M}\right\rrbracket\rho[x_{\sigma}\mapsto V]. Let f(V)=\left\llbracket{M}\right\rrbracket\rho[x_{\sigma}\mapsto V]. We have just shown that for all . By Corollary 6.3, (\mathop{\boldsymbol{\mathtt{rec}}}x_{\sigma}.M)\theta=\mathop{\boldsymbol{\mathtt{rec}}}x_{\sigma}.(M\theta)\mathrel{R}_{\sigma}\mathop{\mathrm{lfp}}(f)=\left\llbracket{\mathop{\boldsymbol{\mathtt{rec}}}x_{\sigma}.M}\right\rrbracket\rho.
We finish with the constructions involving or . For where , by induction hypothesis M\theta\mathrel{R}_{\boldsymbol{\mathtt{F}}\boldsymbol{\mathtt{V}}\boldsymbol{\mathtt{unit}}}\left\llbracket{M}\right\rrbracket\rho. Using Lemma 6.8, item 2, we obtain that \mathop{\text{Pr}}([\_]\cdot M\theta\mathbin{\downarrow})\geq{(\nu\in\mathbf{V}_{\leq 1}\mathbb{S}\mapsto\nu(\{\top\}))}^{*}(\left\llbracket{M}\right\rrbracket\rho). If \left\llbracket{M}\right\rrbracket\rho=\bot, then \left\llbracket{\bigcirc_{>b}M}\right\rrbracket\rho=\bot, so \bigcirc_{>b}M\theta\mathrel{R}_{\boldsymbol{\mathtt{unit}}}\left\llbracket{\bigcirc_{>b}M}\right\rrbracket\rho, trivially. Otherwise, \left\llbracket{M}\right\rrbracket\rho is a compact saturated subset of . If for some \nu\in\left\llbracket{M}\right\rrbracket\rho, then again \left\llbracket{\bigcirc_{>b}M}\right\rrbracket\rho=\bot, so \bigcirc_{>b}M\theta\mathrel{R}_{\boldsymbol{\mathtt{unit}}}\left\llbracket{\bigcirc_{>b}M}\right\rrbracket\rho is again trivial. Finally, if for every \nu\in\left\llbracket{M}\right\rrbracket\rho, then we verify that b\ll{(\nu\in\mathbf{V}_{\leq 1}\mathbb{S}\mapsto\nu(\{\top\}))}^{*}(\left\llbracket{M}\right\rrbracket\rho): if \left\llbracket{M}\right\rrbracket\rho\neq\emptyset, {(\nu\in\mathbf{V}_{\leq 1}\mathbb{S}\mapsto\nu(\{\top\}))}^{*}(\left\llbracket{M}\right\rrbracket\rho)=\min_{\nu\in\left\llbracket{M}\right\rrbracket\rho}\nu(\{\top\}), so is way-below that value; while if \left\llbracket{M}\right\rrbracket\rho=\emptyset, then {(\nu\in\mathbf{V}_{\leq 1}\mathbb{S}\mapsto\nu(\{\top\}))}^{*}(\left\llbracket{M}\right\rrbracket\rho)=1, and because the operator requires . It follows that , so there is a number such that and is derivable. By Lemma 4.5, is derivable. For every ground context , for every such that is derivable, the leftmost rule of the bottom row of Figure 3 allows us to derive , so . It follows that \bigcirc_{>b}M\mathrel{R}_{\boldsymbol{\mathtt{unit}}}\top=\left\llbracket{\bigcirc_{>b}M}\right\rrbracket\rho.
Finally, for terms of the form , where and , we wish to show that (\boldsymbol{\mathtt{pifz}}\;M\;N\;P)\theta\mathrel{R}_{\boldsymbol{\mathtt{F}}{}\tau}\left\llbracket{\boldsymbol{\mathtt{pifz}}\;M\;N\;P}\right\rrbracket\rho. This means showing that, for all , \mathop{\text{Pr}}(C\cdot\boldsymbol{\mathtt{pifz}}\;M\theta\;N\theta\;P\theta\mathbin{\downarrow})\geq{h}^{*}(\left\llbracket{\boldsymbol{\mathtt{pifz}}\;M\;N\;P}\right\rrbracket\rho).
If \left\llbracket{M}\right\rrbracket\rho=\bot, then \left\llbracket{\boldsymbol{\mathtt{pifz}}\;M\;N\;P}\right\rrbracket\rho=\left\llbracket{N}\right\rrbracket\rho\wedge\left\llbracket{P}\right\rrbracket\rho. In that case, we note that is larger than or equal to : for every way-below , we can derive for some , and for some ; then, by Lemma 4.5, we can derive and , hence . By induction hypothesis, N\theta\mathrel{R}_{\boldsymbol{\mathtt{F}}{}\tau}\left\llbracket{N}\right\rrbracket\rho, so \mathop{\text{Pr}}(C\cdot N\theta\mathbin{\downarrow})\geq{h}^{*}(\left\llbracket{N}\right\rrbracket\rho), and similarly \mathop{\text{Pr}}(C\cdot P\theta\mathbin{\downarrow})\geq{h}^{*}(\left\llbracket{P}\right\rrbracket\rho). Therefore \mathop{\text{Pr}}(C\cdot\boldsymbol{\mathtt{pifz}}\;M\theta\;N\theta\;P\theta\mathbin{\downarrow})\geq\min({h}^{*}(\left\llbracket{N}\right\rrbracket\rho),{h}^{*}(\left\llbracket{P}\right\rrbracket\rho))={h}^{*}(\left\llbracket{N}\right\rrbracket\rho\wedge\left\llbracket{P}\right\rrbracket\rho)={h}^{*}(\left\llbracket{\boldsymbol{\mathtt{pifz}}\;M\;N\;P}\right\rrbracket\rho), since preserves binary infima (Proposition 4.2, item 3).
If \left\llbracket{M}\right\rrbracket\rho\neq\bot, then \left\llbracket{\boldsymbol{\mathtt{pifz}}\;M\;N\;P}\right\rrbracket\rho=\left\llbracket{\boldsymbol{\mathtt{ifz}}\;M\;N\;P}\right\rrbracket\rho. We have already seen that \boldsymbol{\mathtt{ifz}}\;M\theta\;N\theta\;P\theta\mathrel{R}_{\boldsymbol{\mathtt{F}}{}\tau}\left\llbracket{\boldsymbol{\mathtt{ifz}}\;M\;N\;P}\right\rrbracket\rho, so \mathop{\text{Pr}}(C\cdot\boldsymbol{\mathtt{ifz}}\;M\theta\;N\theta\;P\theta\mathbin{\downarrow})\geq{h}^{*}(\left\llbracket{\boldsymbol{\mathtt{ifz}}\;M\;N\;P}\right\rrbracket\rho)={h}^{*}(\left\llbracket{\boldsymbol{\mathtt{pifz}}\;M\;N\;P}\right\rrbracket\rho). For every , if we can derive , then we can also derive , so , and that is larger than or equal to {h}^{*}(\left\llbracket{\boldsymbol{\mathtt{pifz}}\;M\;N\;P}\right\rrbracket\rho).
Given a ground term (or context) , \left\llbracket{M}\right\rrbracket\rho does not depend on , and we will simply write \left\llbracket{M}\right\rrbracket in this case.
Proposition 6.10** (Adequacy)**
In any of the languages CBPV, CBPV, CBPV, and CBPV, for every ground term ,
[TABLE]
where is the map .
Explicitly: either \left\llbracket{M}\right\rrbracket=\bot and , or \left\llbracket{M}\right\rrbracket=\emptyset and , or \left\llbracket{M}\right\rrbracket\neq\bot,\emptyset and \mathop{\text{Pr}}(M\mathbin{\downarrow})=\min_{\nu\in\left\llbracket{M}\right\rrbracket}\nu(\{\top\}).
Proof. By Proposition 6.9 applied to , M\mathrel{R}_{\boldsymbol{\mathtt{F}}\boldsymbol{\mathtt{V}}\boldsymbol{\mathtt{unit}}}\left\llbracket{M}\right\rrbracket. By Lemma 6.8, item 2, , so \mathop{\text{Pr}}([\_]\cdot M\mathbin{\downarrow})\geq{h}^{*}(\left\llbracket{M}\right\rrbracket). The converse inequality is by soundness (Proposition 5.1, item 2).
7 Consequences of Adequacy
Definition 7.1
The applicative preorder between ground CBPV terms of value type is defined by if and only if for every ground term , .
While the applicative preorder is only defined at value types, one can extend it fairly trivially to computation types by letting if and only if .
As for (Definition 4.4), we will freely reuse the notations for all the variants of CBPV considered in this paper, with or without and . Any result that does not mention the language considered holds for all four: this will notably be the case in the current section.
Lemma 7.2
For all ground terms such that , for every ground term , .
Proof. We must show that for every ground evaluation context , . By Lemma 4.7, . Similarly, . Since , , and we conclude.
We reuse the logical relation of Section 6.
The following is sometimes called Milner’s Context Lemma in the setting of PCF, and we will prove it by using a variant of an argument due to A. Jung [20, Theorem 8.1].
Theorem 7.3** (Contextual=applicative)**
For every value type , the contextual preorder and the applicative preorder on ground CBPV terms of type are the same relation.
Proof. Let , be two ground terms of type . If , then consider a ground evaluation context . By Lemma 4.9, , which is equal to by definition, is equal to . By adequacy (Proposition 6.10), \mathop{\text{Pr}}(C[M]\mathbin{\downarrow})={h}^{*}(\left\llbracket{C[M]}\right\rrbracket) where is the map . Let , where is a fresh variable of type . Then \left\llbracket{C[M]}\right\rrbracket=\left\llbracket{QM}\right\rrbracket. By adequacy again, \mathop{\text{Pr}}(QM\mathbin{\downarrow})={h}^{*}(\left\llbracket{QM}\right\rrbracket), so . Similarly, . Since , the former is less than or equal to the latter, so .
Conversely, let us assume . Consider a ground term . By Proposition 6.9 with , M\mathrel{R}_{\tau}\left\llbracket{M}\right\rrbracket. By Lemma 6.1, since , we also have N\mathrel{R}_{\tau}\left\llbracket{M}\right\rrbracket. By Proposition 6.9 again, Q\mathrel{R}_{\tau\to\boldsymbol{\mathtt{F}}\boldsymbol{\mathtt{V}}\boldsymbol{\mathtt{unit}}}\left\llbracket{Q}\right\rrbracket. Hence QN\mathrel{R}_{\boldsymbol{\mathtt{F}}\boldsymbol{\mathtt{V}}\boldsymbol{\mathtt{unit}}}\left\llbracket{QM}\right\rrbracket. By Lemma 6.8, , where is as above. Using the definition of , \mathop{\text{Pr}}(QN\mathbin{\downarrow})=\mathop{\text{Pr}}([\_]\cdot QN\mathbin{\downarrow})\geq{h}^{*}(\left\llbracket{QM}\right\rrbracket). The latter is equal to by adequacy (Proposition 6.10). We have shown , where is arbitrary, hence .
Corollary 7.4
*For every computation type , the contextual preorder and the applicative preorder on ground CBPV terms of type are the same relation. *
Proof. We claim that if and only if . The result will then follow from Theorem 7.3, since is equivalent to , hence to , by definition.
If , let be any ground evaluation context of type . Let us write as , where , and . Since is not , , or , must be at least . The only elementary context of type is . Let . Then (by Lemma 4.9) ={h}^{*}(\left\llbracket{C^{\prime}[\mathop{\boldsymbol{\mathtt{force}}}\mathop{\boldsymbol{\mathtt{thunk}}}M]}\right\rrbracket) (by adequacy, where is given in Proposition 6.10) ={h}^{*}(\left\llbracket{C^{\prime}[M]}\right\rrbracket) (because and are both interpreted as identity maps) . Similarly, . Since , the former is less than or equal to the latter. This allows us to conclude that .
Conversely, we assume that , and we consider an arbitrary ground evaluation context . Then is a ground evaluation context of type , so . As above, we have \mathop{\text{Pr}}(C[\mathop{\boldsymbol{\mathtt{force}}}\_]\cdot\mathop{\boldsymbol{\mathtt{thunk}}}M\mathbin{\downarrow})={h}^{*}(\left\llbracket{C[\mathop{\boldsymbol{\mathtt{force}}}\mathop{\boldsymbol{\mathtt{thunk}}}M]}\right\rrbracket)={h}^{*}(\left\llbracket{C[M]}\right\rrbracket)=\mathop{\text{Pr}}(C\cdot M\mathbin{\downarrow}), and , and the former is less than or equal to the latter.
The following proposition is a form of extensionality: two abstractions are related by if and only if applying them to the same ground terms yield related results.
Proposition 7.5
Let be two terms with as sole free variable. Then if and only if for every ground term , .
Proof. If , then for every ground term , by Lemma 7.2. Hence for every ground evaluation context , . Using Lemma 4.9, we obtain . By adequacy (Proposition 6.10), \mathop{\text{Pr}}(C[(\lambda x_{\sigma}.M)P]\mathbin{\downarrow})={h}^{*}(\left\llbracket{C[(\lambda x_{\sigma}.M)P]}\right\rrbracket), where . That is equal to {h}^{*}(\left\llbracket{C[M[x_{\sigma}:=P]]}\right\rrbracket), hence to . Similarly, , so . Since is arbitrary, .
Conversely, assume that for every ground term . We wish to show that for every ground evaluation context , . Let us write as , where each is of type , and . We cannot have , since is none of the types , , . By inspection of the possible shape of the elementary context , we see that it must be of the form for some (ground) term . Let . Using Lemma 4.9 and adequacy as above, , and similarly with instead of . We have since , so .
A final, expected, consequence of adequacy is the following.
Proposition 7.6
*For every value type , for every two ground terms , if \left\llbracket{M}\right\rrbracket\leq\left\llbracket{N}\right\rrbracket then . *
Proof. For every ground term , \left\llbracket{QM}\right\rrbracket=\left\llbracket{Q}\right\rrbracket(\left\llbracket{M}\right\rrbracket)\leq\left\llbracket{Q}\right\rrbracket(\left\llbracket{N}\right\rrbracket), hence {h}^{*}(\left\llbracket{QM}\right\rrbracket)\leq{h}^{*}(\left\llbracket{QN}\right\rrbracket) for every continuous map . By adequacy (Proposition 6.10), \mathop{\text{Pr}}(QM\mathbin{\downarrow})={h}^{*}(\left\llbracket{QM}\right\rrbracket), and \mathop{\text{Pr}}(QN\mathbin{\downarrow})={h}^{*}(\left\llbracket{QN}\right\rrbracket) where is the map . Therefore . The converse implication, if it holds, is full abstraction.
8 The Failure of Full Abstraction
We will show that CBPV is not fully abstract, for two reasons. One is the expected lack of a parallel if operator, just as in PCF [19]. The other is the lack of a statistical termination tester, as in [11].
Our main tool is a variant on our previous logical relations . This time, will be an -ary relation, for some non-empty set , between semantical values—namely, \mathrel{S}_{\overline{\sigma}}\subseteq\left\llbracket{{\overline{\sigma}}}\right\rrbracket^{I}. The construction is parameterized by a finite family of subsets of , and two -ary relations . Again we will also define auxiliary relations , and , which are certain sets of -tuples of Scott-continuous maps from \left\llbracket{\sigma}\right\rrbracket to . We write for , and similarly with , , etc. For every and every subset of , we write for the vector obtained from by replacing every element , , by [math]; namely, is equal to [math] if , to otherwise. We require the following:
- •
, is closed under binary unions, and is well-founded: every filtered family in has a least element , .
- •
is non-empty, closed under directed suprema, convex (notably, if and are in then so is ), and is -lower, meaning that for every , for every , is in ;
- •
is closed under directed suprema, under pairwise minima (if and are in then so is ), contains the all one vector , and is -lower.
We define the following.
- •
iff ;
- •
(resp., ) iff: the set is in and the components , , are all equal;
- •
, where for every , iff and ;
- •
iff for all , {(\int_{x\in\left\llbracket{\sigma}\right\rrbracket}h_{i}(x)d\nu_{i})}_{i\in I}\in{\triangleright};
- •
iff for all , ;
- •
iff for all , ;
- •
iff for all , ;
- •
iff for all , .
For every -indexed tuple of environments, finally, if and only if for every variable , .
Lemma 8.1
For every , for every CBPV* term , {(\left\llbracket{M}\right\rrbracket\rho_{i})}_{i\in I} is in .* 2. 2.
The same remains true for all CBPV* terms if . *
Proof. We first show: is closed under directed suprema taken in \left\llbracket{{\overline{\sigma}}}\right\rrbracket^{I}, and contains . This is by induction on the type . Most cases are trivial. We deal with the remaining ones:
- •
When or , is in , because . We must show that the supremum of every directed family in is in . Let for each , and . Define if and only if . Then implies , so is a filtered family. Since is well-founded, there is an index such that for every . Then, for every , is equal to if , and is different from otherwise. In particular, . Letting be the common value of the terms , , for each , we have for every , and all these values are equal. Therefore is in .
- •
When , is the tuple consisting of zero valuations only, and for every , {(\int_{x\in\left\llbracket{\sigma}\right\rrbracket}h_{i}(x)d0)}_{i\in I}=\vec{0} is in (since is -lower and ), so . In order to show closure under directed suprema, let be a directed family in , with . Its supremum is where . For every , {(\int_{x\in\left\llbracket{\sigma}\right\rrbracket}h_{i}(x)d\nu_{i})}_{i\in I}={(\sup_{j}\int_{x\in\left\llbracket{\sigma}\right\rrbracket}h_{i}(x)d\nu_{ji})}_{i\in I}, since integration is Scott-continuous in the valuation. That is a directed supremum of values in , hence is in . It follows that is in .
- •
When , is in because, for every , is equal to (since is strict), and that is in : , which is in because is -lower and . As far as closure under directed suprema is concerned, let be a directed family in , where . Let us write its supremum as . For every , is the supremum of the family of tuples , , since is Scott-continuous (Proposition 4.2, item 2), and all those tuples are in . Since the latter is closed under directed suprema, is in , so is in .
Next, we claim that: for every and for every , is in . To this end, let . Our goal is to show that {(\int_{y\in\left\llbracket{\tau}\right\rrbracket}h_{i}(y)df_{i}^{\dagger}(\nu_{i}))}_{i\in I} is in . Using (1), this boils down to showing that {(\int_{x\in\left\llbracket{\sigma}\right\rrbracket}h^{\prime}_{i}(x)d\nu_{i})}_{i\in I} is in , where is the map x\mapsto\int_{y\in\left\llbracket{\tau}\right\rrbracket}h_{i}(y)df_{i}(x). We note that is in : for every , is in (by definition of ); by the definition of , and using the fact that , {(\int_{y\in\left\llbracket{\tau}\right\rrbracket}h_{i}(y)df_{i}(a_{i}))}_{i\in I} is in , in other words is in . Since and , the claim follows.
We also claim that: for every and for every , is in . Let . We wish to show that is in . Using Proposition 4.2, item 4, this amounts to showing that is in . We note that is in : for every , is in , and is in , so is in . Since , and using the definition of , is in .
Finally, for every vector in \left\llbracket{{\overline{\sigma}}}\right\rrbracket^{I}, and for every subset of , we define as the vector obtained from by replacing each component with by . We claim that: for every , for every , is in . This is by induction on . For types of the form , , and , we simply call the induction hypothesis. When is or , let , and . We have , and by induction hypothesis. Since is closed under binary unions, is in . Moreover, all the components with are equal to , and they are all equal. Therefore is in . When , let . For every , \vec{b}={(\int_{x\in\left\llbracket{\sigma}\right\rrbracket}h_{i}(x)d\nu_{i})}_{i\in I} is in . The vector {(\int_{x\in\left\llbracket{\sigma}\right\rrbracket}h_{i}(x)d\nu_{|J\;i})}_{i\in I} is equal to , hence is in as well, since is -lower. When , let . For every , is in . Since each function is strict, for every , . For every , . Therefore is equal to where , and that is in by assumption and the fact that is -lower. Hence is in .
- We now prove the lemma by induction on . For variables, this follows from the assumption that . The case of constants and is clear. The case of -abstractions and of applications is immediate from the definition of . Similarly, the case of terms , and are immediate from the definition of . For terms of the form , with , or terms of the form , with , the claim is trivial.
For terms of the form , with , by induction hypothesis {(\left\llbracket{M}\right\rrbracket\rho_{i})}_{i\in I} is in . In order to show that {(\left\llbracket{\mathop{\boldsymbol{\mathtt{produce}}}M}\right\rrbracket\rho_{i})}_{i\in I}={(\eta^{\mathcal{Q}}(\left\llbracket{M}\right\rrbracket\rho_{i}))}_{i\in I} is in , we fix , and we check that {({h_{i}}^{*}(\eta^{\mathcal{Q}}(\left\llbracket{M}\right\rrbracket\rho_{i})))}_{i\in I} is in . Since {h_{i}}^{*}(\eta^{\mathcal{Q}}(\left\llbracket{M}\right\rrbracket\rho_{i}))=h_{i}(\left\llbracket{M}\right\rrbracket\rho_{i}) (Proposition 4.2, item 2), this follows from the definition of .
For terms of the form , with and , we must show that {(\left\llbracket{{M}\mathrel{\boldsymbol{\mathtt{to}}}{x_{\sigma}}\mathrel{\boldsymbol{\mathtt{in}}}{N}}\right\rrbracket\rho_{i})}_{i\in I} is in \left\llbracket{\boldsymbol{\mathtt{F}}{}\tau}\right\rrbracket. Since \left\llbracket{{M}\mathrel{\boldsymbol{\mathtt{to}}}{x_{\sigma}}\mathrel{\boldsymbol{\mathtt{in}}}{N}}\right\rrbracket\rho_{i}={f_{i}}^{*}(\left\llbracket{M}\right\rrbracket\rho_{i}), where f_{i}(V)=\left\llbracket{N}\right\rrbracket\rho_{i}[x_{\sigma}\mapsto V], we will obtain this as a consequence of if we can show that is in . For every , is in , so {(f_{i}(a_{i}))}_{i\in I}={(\left\llbracket{N}\right\rrbracket\rho_{i}[x_{\sigma}\mapsto a_{i}])}_{i\in I} is indeed in .
For terms of the form , where , we must show that for every , {(\int_{x\in\left\llbracket{\tau}\right\rrbracket}h_{i}(x)d\left\llbracket{\mathop{\boldsymbol{\mathtt{ret}}}\nolimits M}\right\rrbracket\rho_{i})}_{i\in I} is in . Since \int_{x\in\left\llbracket{\tau}\right\rrbracket}h_{i}(x)d\left\llbracket{\mathop{\boldsymbol{\mathtt{ret}}}\nolimits M}\right\rrbracket\rho_{i}=\int_{x\in\left\llbracket{\tau}\right\rrbracket}h_{i}(x)d\delta_{\left\llbracket{M}\right\rrbracket\rho_{i}}=h_{i}(\left\llbracket{M}\right\rrbracket\rho_{i}), this follows from the fact that and the definition of .
For terms of the form , with and , we wish to show that {(\left\llbracket{\mathop{\boldsymbol{\mathtt{do}}}\nolimits{x_{\sigma}\leftarrow M};N}\right\rrbracket\rho_{i})}_{i\in I} is in , namely that {(f_{i}^{\dagger}(\left\llbracket{N}\right\rrbracket\rho_{i}))}_{i\in I} is in , where f_{i}(V)=\left\llbracket{N}\right\rrbracket\rho_{i}[x_{\sigma}\mapsto V]. As in the case of terms, is in , and {(\left\llbracket{N}\right\rrbracket\rho_{i})}_{i\in I} is in , so the claim is proved by applying .
For terms of the form , with , by induction hypothesis {(\left\llbracket{M}\right\rrbracket\rho_{i})}_{i\in I} is in . Let J=\{i\in I\mid\left\llbracket{M}\right\rrbracket\rho_{i}=\bot\}, and be the common value of \left\llbracket{M}\right\rrbracket\rho_{i}, (or an arbitrary element of if ). Then is also equal to \{i\in I\mid\left\llbracket{\mathop{\boldsymbol{\mathtt{succ}}}M}\right\rrbracket\rho_{i}=\bot\}, which is therefore in . Moreover, is the common value of \left\llbracket{\mathop{\boldsymbol{\mathtt{succ}}}M}\right\rrbracket\rho_{i}, . We reason similarly for terms of the form .
For terms of the form , where and , by hypothesis, in particular, {(\left\llbracket{M}\right\rrbracket\rho_{i})}_{i\in I} is in . Let J=\{i\in I\mid\left\llbracket{M}\right\rrbracket\rho_{i}=\bot\}, and be the common value of \left\llbracket{M}\right\rrbracket\rho_{i}, (or any element of if ). {(\left\llbracket{\boldsymbol{\mathtt{ifz}}\;M\;N\;P}\right\rrbracket\rho_{i})}_{i\in I} is equal to , where \vec{a}={(\left\llbracket{N}\right\rrbracket\rho_{i})}_{i\in I} if and \vec{a}={(\left\llbracket{P}\right\rrbracket\rho_{i})}_{i\in I} if . The latter is in by induction hypothesis, so the former is in , too, by .
For terms of the form , with and , {(\left\llbracket{M}\right\rrbracket\rho_{i})}_{i\in I} is in by induction hypothesis. Let J=\{i\in I\mid\left\llbracket{M}\right\rrbracket\rho_{i}=\bot\}. {(\left\llbracket{M;N}\right\rrbracket)}_{i\in I} is equal to where \vec{a}={(\left\llbracket{N}\right\rrbracket\rho_{i})}_{i\in I}, which is in by induction hypothesis and .
For terms of the form , with , we wish to show that the tuple {(\left\llbracket{M\oplus N}\right\rrbracket\rho_{i})}_{i\in I} is in . Let . By induction hypothesis, the tuples {(\int_{x\in\left\llbracket{\tau}\right\rrbracket}h_{i}(x)d\left\llbracket{M}\right\rrbracket\rho_{i})}_{i\in I} and {(\int_{x\in\left\llbracket{\tau}\right\rrbracket}h_{i}(x)d\left\llbracket{N}\right\rrbracket\rho_{i})}_{i\in I} are in . Since is convex, {(\frac{1}{2}(\int_{x\in\left\llbracket{\tau}\right\rrbracket}h_{i}(x)d\left\llbracket{M}\right\rrbracket\rho_{i}+\int_{x\in\left\llbracket{\tau}\right\rrbracket}h_{i}(x)d\left\llbracket{N}\right\rrbracket\rho_{i}))}_{i\in I} is also in , and that is just {(\int_{x\in\left\llbracket{\tau}\right\rrbracket}h_{i}(x)d\left\llbracket{M\oplus N}\right\rrbracket\rho_{i})}_{i\in I}.
For terms of the form , with , we wish to show that the tuple {(\left\llbracket{M\owedge N}\right\rrbracket\rho_{i})}_{i\in I} is in . Let . By induction hypothesis, {({h_{i}}^{*}(\left\llbracket{M}\right\rrbracket\rho_{i}))}_{i\in I} and {({h_{i}}^{*}(\left\llbracket{N}\right\rrbracket\rho_{i}))}_{i\in I} are in . Since is closed under pairwise minima, and commutes with pairwise infima (Proposition 4.2, item 3), {({h_{i}}^{*}(\left\llbracket{M\owedge N}\right\rrbracket\rho_{i}))}_{i\in I} is also in , showing the claim.
For , we consider an arbitrary vector , and we must show that is in . By Proposition 4.2, item 3, is the top element, , of , and the claim follows from the fact that .
For terms of the form , let be the map defined by f_{i}(V)=\left\llbracket{M}\right\rrbracket\rho_{i}[x_{\sigma}\mapsto V]. For every , is in , hence by induction hypothesis is in . Let us write as . By , is in , and therefore , , …, are all in . By the other part of , in in as well. That tuple is just , namely {(\left\llbracket{\mathop{\boldsymbol{\mathtt{rec}}}x_{\sigma}.M}\right\rrbracket\rho_{i})}_{i\in I}.
- In the case of terms of the form , of type , and assuming , the induction hypothesis {(\left\llbracket{M}\right\rrbracket\rho_{i})}_{i\in I}\in\mathrel{S}_{\boldsymbol{\mathtt{int}}} implies that all the values \left\llbracket{M}\right\rrbracket\rho_{i} are the same: letting J=\{i\in I\mid\left\llbracket{M}\right\rrbracket\rho_{i}=\bot\}, either and they are all equal to , or and they are all equal by definition of . Hence {(\left\llbracket{\boldsymbol{\mathtt{pifz}}\;M\;N\;P}\right\rrbracket\rho_{i})}_{i\in I} is equal to {(\left\llbracket{N}\right\rrbracket\rho_{i})}_{i\in I}, to {(\left\llbracket{P}\right\rrbracket\rho_{i})}_{i\in I}, or to {(\left\llbracket{M\owedge N}\right\rrbracket\rho_{i})}_{i\in I}, and they are all in .
8.1 The Need for Parallel If
In this section, we let , , be arbitrary (e.g., the whole of ), and . The latter is the smallest possible set that satisfies the constraints required of , and is the graph of the infimum function .
A triple in is in if and only if is empty, equal to or , or to , and all the non-bottom components are equal. Those are the triples , , and (with ).
Lemma 8.2
The triples in are the triples of characteristic maps of open subsets , , of of one of the following forms:
*; * 2. 2.
* for some ;* 3. 3.
, arbitrary; 4. 4.
, arbitrary.
Proof. A triple of Scott-continuous maps is in if and only if for all , . We claim that this is equivalent to: , , take their values in and for all such that , . In one direction, if , then since for every , is in for every , in particular , , take their values in . Also, for all such that , . Indeed, the triples such that are of the form , or , or , or , with , hence are exactly the triples in . Then is in , hence since is the graph of on . In the other direction, let us assume . For all , we have just seen that , so is in the graph of on . It follows that is in .
Equivalently, means that , , are the characteristic maps , , of open subsets , , of such that: for all such that , if and only if and . Clearly, any of the cases 1–4 implies .
Let us assume that holds. By taking , we obtain that . If is empty, then is empty and we are in case 3. If is empty, then is empty and we are in case 4. Henceforth, let us assume that and are non-empty. If , then pick any : we can then take , so is in by ; this implies that , hence also , since ; hence we are in case 1. We reason similarly if is in . It remains to examine the cases where and are non-empty subsets of . If there are two distinct elements and , then is equal to and must be in by , so , and again , meaning that we are in case 1. Otherwise, for some , then as well, and we are in case 2.
Lemma 8.3
*For every ground CBPV term such that \left\llbracket{P}\right\rrbracket(\bot)(0)=\left\llbracket{P}\right\rrbracket(0)(\bot)=\{0\}, the equality \left\llbracket{P}\right\rrbracket(\bot)(\bot)=\{0\} holds. *
Proof. Let Q\in\left\llbracket{\boldsymbol{\mathtt{F}}{}\boldsymbol{\mathtt{int}}}\right\rrbracket be such that is in . Consider any triple , as given in Lemma 8.2. By definition, and recalling that is the graph of the infimum map, . If were empty, then would be equal to , so and would be equal to , and that is contradicted by the case 1 triple for example. By considering the case 2 triple , we obtain that , namely that . Therefore the only Q\in\left\llbracket{\boldsymbol{\mathtt{F}}{}\boldsymbol{\mathtt{int}}}\right\rrbracket such that is . (One can also check that is indeed in , but that will not be needed.)
By Lemma 8.1, item 1, for all and , the triple (\left\llbracket{P}\right\rrbracket(m_{1})(n_{1}),\left\llbracket{P}\right\rrbracket(m_{2})(n_{2}),\left\llbracket{P}\right\rrbracket(m_{3})(n_{3})) is in . The triples and are in . Hence (\left\llbracket{P}\right\rrbracket(0)(\bot),\left\llbracket{P}\right\rrbracket(\bot)(0),\left\llbracket{P}\right\rrbracket(\bot)(\bot)) is in . Explicitly, (\{0\},\{0\},\left\llbracket{P}\right\rrbracket(\bot)(\bot)) is in . We have just seen that this implies \left\llbracket{P}\right\rrbracket(\bot)(\bot)=\{0\}.
We introduce the following abbreviations.
- •
denotes for every value type . We have \left\llbracket{\Omega_{\sigma}}\right\rrbracket=\bot.
- •
denotes , for every computation type . We have \left\llbracket{\Omega_{\underline{\tau}}}\right\rrbracket=\bot.
- •
For all and , abbreviates , where is not free in . \left\llbracket{M\mathbin{==}\underline{0}\mathbin{\&}N}\right\rrbracket\rho is equal to \left\llbracket{N}\right\rrbracket\rho if \left\llbracket{M}\right\rrbracket\rho=\{0\}, to if \left\llbracket{M}\right\rrbracket\rho=\emptyset, and to in all other cases.
- •
Similarly, abbreviates , so that \left\llbracket{M\mathbin{==}\underline{1}\mathbin{\&}N}\right\rrbracket\rho is equal to \left\llbracket{N}\right\rrbracket\rho if \left\llbracket{M}\right\rrbracket\rho=\{1\}, to if \left\llbracket{M}\right\rrbracket\rho=\emptyset, and to in all other cases.
- •
Finally, for all , let abbreviate , where is not free in , so that \left\llbracket{M\mathbin{\&}N}\right\rrbracket\rho is equal to \left\llbracket{N}\right\rrbracket\rho if \left\llbracket{M}\right\rrbracket\rho=\{\top\} or if \left\llbracket{M}\right\rrbracket\rho=\mathbb{S}, to if \left\llbracket{M}\right\rrbracket\rho=\emptyset and to if \left\llbracket{M}\right\rrbracket\rho=\bot.
We let associate to the right, so means .
Proposition 8.4
For every term , let:
[TABLE]
We also define as , and as , where has type .
In CBPV, , but \left\llbracket{M}\right\rrbracket\not\leq\left\llbracket{N}\right\rrbracket.
Proof. \left\llbracket{M}\right\rrbracket applied to any Scott-continuous map returns:
- •
if ;
- •
if or if and ;
- •
and in all other cases.
Then \left\llbracket{N}\right\rrbracket applied to returns:
- •
if \left\llbracket{M}\right\rrbracket(G)=\{\top\} and ;
- •
if \left\llbracket{M}\right\rrbracket(G)=\{\top\} and ;
- •
if \left\llbracket{M}\right\rrbracket(G)=\emptyset;
- •
in all other cases.
In particular, \left\llbracket{M}\right\rrbracket\not\leq\left\llbracket{N}\right\rrbracket: defining to be the parallel or map ( for every , , for all such that ), \left\llbracket{M}\right\rrbracket(G)=\{\top\}, but \left\llbracket{N}\right\rrbracket(G)=\bot. Note, by the way, that the argument would also work with other choices of map , for example for every , and in all other cases.
For every ground CBPV term , \left\llbracket{M(P)}\right\rrbracket=\{\top\} if and only if \left\llbracket{P}\right\rrbracket(\bot)(0)=\left\llbracket{P}\right\rrbracket(0)(\bot)=\{0\}, and if so, \left\llbracket{P}\right\rrbracket(\bot)(\bot)=\{0\} by Lemma 8.3. Taking G=\left\llbracket{P}\right\rrbracket, it follows that the second case of the definition of \left\llbracket{N}\right\rrbracket(G) does not occur, so \left\llbracket{N(P)}\right\rrbracket=\left\llbracket{N}\right\rrbracket(G) is equal to if \left\llbracket{M(P)}\right\rrbracket=\{\top\} (and then is automatic), to if \left\llbracket{M(P)}\right\rrbracket=\emptyset, and to in all other cases. Hence \left\llbracket{N(P)}\right\rrbracket=\left\llbracket{M(P)}\right\rrbracket. Since in particular \left\llbracket{M(P)}\right\rrbracket\leq\left\llbracket{N(P)}\right\rrbracket, by Proposition 7.6, . Since is arbitrary, by Proposition 7.5.
8.2 The Need for Statistical Termination Testers
We turn to justify the need for a operator, following similar ideas as in [11, Proposition 8.5].
Here we let , , , and .
In that case, if and only if for every , . Letting and , , if and only if:
[TABLE]
This defines a (bounded) polytope of , and we claim that its vertices are:
[TABLE]
We check that those points satisfy all the given inequalities. Conversely, let satisfy (2)–(5). Because it satisfies (4), is a linear convex combination , where and , and the remaining inequalities become , , , whose solutions in are the convex combinations of , , , and (as a two-dimensional picture will show), say , with and . Since the latter is affine in , and , it follows that the solutions of (2)–(5) are all of the form times , plus times , plus times (where . denotes concatenation of tuples, i.e., ), hence a a convex combination of the 10 tuples of the above table.
Lemma 8.5
For all , if and only if .
Proof. We have if and only if for all , . Writing and as above, the domain of variation of is the convex hull of the 10 points in (6), and we must check that for all those -tuples. The domain of variation of the pairs alone is the convex hull of , , , (and , which is already a convex combination of the others). By linearity, it is equivalent to check for just those four values of . Therefore if and only if , , , and . Since the first three are always true, only the last one remains.
Lemma 8.6
Let \nu_{1},\nu_{2}\in\left\llbracket{\boldsymbol{\mathtt{V}}{}\boldsymbol{\mathtt{unit}}}\right\rrbracket. If then .
Proof. For every , . Considering the case where and are given by the data of the 5th row of (6), we obtain . Considering the last row instead, we obtain . The inequality is obvious.
Lemma 8.7
Let be any Scott-continuous map from to . Then .
Proof. It suffices to verify that for all , is in , namely that . By Lemma 8.6, , and we conclude since , being Scott-continuous, is monotonic.
Proposition 8.8
Let:
[TABLE]
where has type .
In CBPV and also in CBPV, , but \left\llbracket{M}\right\rrbracket\not\leq\left\llbracket{N}\right\rrbracket.
Proof. Let be any ground CBPV or CBPV term of type , and:
[TABLE]
We have:
[TABLE]
where . By Lemma 8.5, is in . By Lemma 8.1 (item 2), (\left\llbracket{P}\right\rrbracket,\left\llbracket{P}\right\rrbracket) is in , so (\left\llbracket{P}\right\rrbracket(0),\left\llbracket{P}\right\rrbracket(\frac{1}{2}\delta_{\top})) is in . Using Lemma 8.7, for every Scott-continuous map k\colon\left\llbracket{\boldsymbol{\mathtt{V}}\boldsymbol{\mathtt{unit}}}\right\rrbracket\to[0,1], , so ({(k(\frac{1}{2}\_+\frac{1}{2}\delta_{\top}))}^{*}(\left\llbracket{P}\right\rrbracket(0)),{k}^{*}(\left\llbracket{P}\right\rrbracket(\frac{1}{2}\delta_{\top}))) is in . In other words, {(k(\frac{1}{2}\_+\frac{1}{2}\delta_{\top}))}^{*}(\left\llbracket{P}\right\rrbracket(0))\geq{k}^{*}(\left\llbracket{P}\right\rrbracket(\frac{1}{2}\delta_{\top})).
Since , and using Proposition 4.2, item 2, . It follows that (using Proposition 4.2, item 4) . Hence our previous equality can be read, alternatively, as {k}^{*}({g}^{*}(\left\llbracket{P}\right\rrbracket(0)))\geq{k}^{*}(\left\llbracket{P}\right\rrbracket(\frac{1}{2}\delta_{\top})). In other words,
[TABLE]
for every Scott-continuous map k\colon\left\llbracket{\boldsymbol{\mathtt{V}}\boldsymbol{\mathtt{unit}}}\right\rrbracket\to[0,1].
We claim that . To this end, we let be any ground evaluation context of type , and we aim to show that . By adequacy (Proposition 6.10) and Lemma 4.9, this means showing that {h}^{*}(\left\llbracket{C}\right\rrbracket(\left\llbracket{M(P)}\right\rrbracket))\leq{h}^{*}(\left\llbracket{C}\right\rrbracket(\left\llbracket{N(P)}\right\rrbracket)), where .
Let us write as , where , . All the types have rank , namely, are computation types. It follows that , and that the elementary contexts , are of the form or . However, is an -type (i.e., of the form for some value type ), and that implies that must be of the form and must be an -type again. Then must again be of the form and must be an -type, and so on: the elementary contexts , , are all of the form , and for some value type , with . In particular, \left\llbracket{E_{i}}\right\rrbracket={f_{i}}^{*} for some Scott-continuous map f_{i}\colon\left\llbracket{\boldsymbol{\mathtt{V}}{}\tau_{i+1}}\right\rrbracket\to\left\llbracket{\boldsymbol{\mathtt{V}}{}\tau_{i}}\right\rrbracket. It follows that \left\llbracket{C}\right\rrbracket={f_{1}}^{*}\circ{f_{2}}^{*}\circ\cdots\circ{f_{n}}^{*}. If , then applying Proposition 4.2, item 4, repeatedly, we obtain that \left\llbracket{C}\right\rrbracket={f}^{*} for some Scott-continuous map f\colon\left\llbracket{\boldsymbol{\mathtt{V}}\boldsymbol{\mathtt{unit}}}\right\rrbracket\to\left\llbracket{\boldsymbol{\mathtt{F}}\boldsymbol{\mathtt{V}}\boldsymbol{\mathtt{unit}}}\right\rrbracket; applying it one more time, {h}^{*}\circ\left\llbracket{C}\right\rrbracket={({h}^{*}\circ f)}^{*}. If , then {h}^{*}\circ\left\llbracket{C}\right\rrbracket={h}^{*}. In both cases, {h}^{*}\circ\left\llbracket{C}\right\rrbracket is equal to for some Scott-continuous map k\colon\left\llbracket{\boldsymbol{\mathtt{V}}{}\boldsymbol{\mathtt{unit}}}\right\rrbracket\to[0,1].
By (7), {h}^{*}(\left\llbracket{C}\right\rrbracket(\left\llbracket{N(P)}\right\rrbracket))\geq{h}^{*}(\left\llbracket{C}\right\rrbracket(\left\llbracket{M(P)}\right\rrbracket)), and this is what we needed to show to establish .
Since is arbitrary, by Proposition 7.5, .
For every , let be the map that sends every \nu\in\left\llbracket{\boldsymbol{\mathtt{V}}\boldsymbol{\mathtt{unit}}}\right\rrbracket to if , and to otherwise. This is is easily seen to be Scott-continuous. For (e.g., ),
[TABLE]
In particular, \left\llbracket{M}\right\rrbracket([>b])\not\leq\left\llbracket{N}\right\rrbracket([>b]), so \left\llbracket{M}\right\rrbracket\not\leq\left\llbracket{N}\right\rrbracket. The function is, of course, the semantics of . As a consequence, it is not definable in PCBV and even CBPV, at least for . A similar argument would show that it is not definable for any , replacing the definition of by , for any dyadic number .
9 Full Abstraction
Full abstraction for CBPV will follow from a series of auxiliary results that show that the Scott topology on various dcpos coincides with some other, simpler topologies. Before we make that precise, let us say that our goal is that every type should be describable, in the following sense. For a Scott-open subset of \left\llbracket{{\overline{\sigma}}}\right\rrbracket, where is a type, recall that \chi_{U}\in[\left\llbracket{{\overline{\sigma}}}\right\rrbracket\to\mathbb{S}] is its characteristic map. We write for the map \left\llbracket{[\mathop{\boldsymbol{\mathtt{produce}}}\mathop{\boldsymbol{\mathtt{ret}}}\nolimits\_]}\right\rrbracket\circ\chi_{U}, which maps every x\in\left\llbracket{{\overline{\sigma}}}\right\rrbracket to if , to otherwise.
Definition 9.1
An element of \left\llbracket{{\overline{\sigma}}}\right\rrbracket, for a type , is definable if and only if it is equal to \left\llbracket{M}\right\rrbracket for some ground CBPV term .
A Scott-open subset of \left\llbracket{\tau}\right\rrbracket, for a value type , is definable if and only if \tilde{\chi}_{U}=\left\llbracket{M}\right\rrbracket for some ground CBPV term .
For a computation type , a Scott-open subset of \left\llbracket{\underline{\tau}}\right\rrbracket is definable if and only if \tilde{\chi}_{U}=\left\llbracket{M}\right\rrbracket for some ground CBPV term .
*A type is describable if and only if \left\llbracket{{\overline{\sigma}}}\right\rrbracket has a basis of definable elements and the Scott topology on \left\llbracket{{\overline{\sigma}}}\right\rrbracket has a subbase of definable open subsets. *
As a first, easy example of a describable type, we have:
Lemma 9.2
* is describable.*
Proof. All the elements of \left\llbracket{\boldsymbol{\mathtt{unit}}}\right\rrbracket=\mathbb{S} are definable, since \left\llbracket{\Omega_{\boldsymbol{\mathtt{unit}}}}\right\rrbracket=\bot and \left\llbracket{\underline{*}}\right\rrbracket=\top. The function defines the open subset , which is by itself a subbase of the Scott topology.
Lemma 9.3
* is describable.*
Proof. All the elements of \left\llbracket{\boldsymbol{\mathtt{int}}}\right\rrbracket=\mathbb{Z}_{\bot} are definable: \left\llbracket{\Omega_{\boldsymbol{\mathtt{int}}}}\right\rrbracket=\bot, \left\llbracket{\underline{n}}\right\rrbracket=n. A subbase of the Scott topology consists of the sets , , and they are definable by if , and by otherwise.
We now consider more complex types. It will be useful to realize that every describable type has a base, not just a subbase, of definable open subsets. Moreover this base, which is obtained as the collection of finite intersections of subbasic open sets, is closed under finite intersections. We call strong base any base that is closed under finite intersections.
Lemma 9.4
For every describable type , the Scott topology on \left\llbracket{{\overline{\sigma}}}\right\rrbracket has a strong base of definable open subsets.
Proof. For any two terms , let be the term , where is a fresh variable. For every environment , \left\llbracket{M\wedge N}\right\rrbracket\rho={h}^{*}(\left\llbracket{M}\right\rrbracket\rho) where h(\nu)=\left\llbracket{N}\right\rrbracket\rho[x_{\boldsymbol{\mathtt{V}}\boldsymbol{\mathtt{unit}}}\mapsto\nu]=\left\llbracket{N}\right\rrbracket\rho (since is not free in ). Since is strict, if \left\llbracket{M}\right\rrbracket\rho=\bot, then \left\llbracket{M\wedge N}\right\rrbracket\rho=\bot. Otherwise, by Proposition 4.2, item 2, {h}^{*}(\left\llbracket{M}\right\rrbracket\rho)=\bigwedge_{\nu\in\left\llbracket{M}\right\rrbracket\rho}h(\nu). If \left\llbracket{M}\right\rrbracket\rho\neq\emptyset, in particular if \left\llbracket{M}\right\rrbracket=\{\delta_{\top}\}, this is equal to \left\llbracket{N}\right\rrbracket\rho.
We write for . This implements logical and, in the sense that if \left\llbracket{M_{i}}\right\rrbracket\rho is either equal to or to for every , its denotation in any environment is if \left\llbracket{M_{i}}\right\rrbracket\rho=\{\delta_{\top}\} for every , and is if \left\llbracket{M_{i}}\right\rrbracket\rho=\bot for some .
Given finitely many open subsets , …, defined by terms respectively (where if is a value type, if is a computation type), the term then defines the intersection .
9.1 Product types
Lemma 9.5
Let , be two continuous dcpos. Let be a basis of , be a basis of , be a subbase of the Scott topology on , be a subbase of the Scott topology on . Then:
- •
The set is a basis of .
- •
The set is a subbase of the Scott topology on .
Proof. The second part follows from the fact that the Scott topology on a product of continuous dcpos is the product topology, because it is generated by sets of the form \hbox to0.0pt{\uparrow\hss}\raise 2.15277pt\hbox{\uparrow}(x,y)=\hbox to0.0pt{\uparrow\hss}\raise 2.15277pt\hbox{\uparrow}x\times\hbox to0.0pt{\uparrow\hss}\raise 2.15277pt\hbox{\uparrow}y. (This is not true of non-continuous dcpos.)
Proposition 9.6
For any two describable value types and , is describable.
Proof. We use Lemma 9.5 with X=\left\llbracket{\sigma}\right\rrbracket, Y=\left\llbracket{\tau}\right\rrbracket. (resp., ) is the basis of definable elements of \left\llbracket{\sigma}\right\rrbracket (resp., \left\llbracket{\tau}\right\rrbracket). is the base of definable open subsets at type , obtained by Lemma 9.4, and similarly for . The elements of are definable as , where \left\llbracket{M}\right\rrbracket\in B_{X}, \left\llbracket{N}\right\rrbracket\in B_{Y}, and the elements of are definable as , where is defined by and is defined by , and where was defined in the course of the proof of Lemma 9.4.
9.2 Function types
Semantically, at function types, the key result will be the following Proposition 9.10, which in particular says that the Scott topology on coincides with the topology of pointwise convergence, under certain assumptions.
A standard basis of is given by the step functions , where each is open in , each is in , and denotes the map that maps every element of to , and all others to . We show that this can be refined by requiring to be taken from some given strong base of the topology on , and to be taken from some basis of . We note that maps each point to , where . In general, will not be in . To avoid this problem, we require our step functions to be of a special form.
Definition 9.7
Let be a topological space, be a strong base of the topology of , be a continuous dcpo, and be a basis of . A -step function is any step function of the form where:
each is in ; 2. 2.
each is in ; 3. 3.
* and for all ;* 4. 4.
for all , .
We make a preliminary remark.
Lemma 9.8
Given a continuous dcpo , and a family , in order to show that is a basis of it is enough to show that for every , every Scott-open neighborhood of contains a such that .
Proof. If so, then the family is non-empty (take ) and directed (for any two , take W=\hbox to0.0pt{\uparrow\hss}\raise 2.15277pt\hbox{\uparrow}d_{1}\cap\hbox to0.0pt{\uparrow\hss}\raise 2.15277pt\hbox{\uparrow}d_{2}), and (for every open neighborhood of , some element of is in so , and the converse inequality is obvious).
A core-compact topological space is one whose lattice of open subsets is a continuous dcpo. We write for the way-below relation on that lattice. Every locally compact space is core-compact, with if and only if for some compact saturated set .
Lemma 9.9
Let be a core-compact space, be a strong base of the topology of , be a a continuous complete lattice, and be a basis of . Then is a continuous complete lattice, with a basis of -step functions.
Note: one could replace “continuous complete lattice” by “bc-domain” here, and the proof would only be slightly more complicated.
Proof. We apply Lemma 9.8 to . By Proposition 2 of [6], is a bounded complete continuous dcpo with a basis of step functions, and since it has a top, it is a continuous complete lattice. Let be the family of step functions of the form where each is in . For every , and every Scott-open neighborhood of , there is an element of , way-below , and in . Let us write as a union of elements of . The family of maps , where ranges over the finite subsets of for each , is directed (since an upper bound of and of is ), and has as supremum (because for every , letting , there are indices for each such that , hence where ). Hence is in for some finite subsets of , . Now is equal to , showing that it is in . Moreover, . We can therefore apply our preliminary remark and conclude that is a basis of .
Given any element of , we can write it as , where for each , and . (In case were a bc-domain, the same argument would apply provided we only considered the subsets such that is non-empty.) Note that: for all , implies . Also: , for all , , and each is in (because is a strong base).
Let be the family of maps , where and satisfy conditions and and, additionally, each is in . For every , and every Scott-open neighborhood of , contains an element of satisfying conditions and and way-below .
Here is the idea of the rest of the proof. Enumerating the subsets of so that the cardinality of never goes down, starting from the empty set, we replace by an element such that and ; at each step, we also replace by for all strict supersets of , so that still holds. Since is a basis, for large enough, the resulting function will be in . We can also require that for all , since all those elements have been chosen in previous steps so that . At the end of the enumeration, we obtain a function of satisfying conditions and , in , below hence way-below , and such that and for every . In particular, that element is in . Let us now prove that formally.
We claim that: for every downwards-closed family of (downwards-closed with respect to inclusion), there is an element of the form in satisfying conditions and , lying in , such that for every (in particular, ), and such that and for every . This is proved by induction on the cardinality of . This is vacuous if is empty. Hence consider a non-empty downwards-closed family of , let be a maximal element of , and let . Notice that is again downwards-closed. Hence, by induction hypothesis, there an element of satisfying conditions and , in , such that for every , and such that and for every . Since is a basis, we can write as the supremum of a directed family of elements of . For each , let . One checks easily that is a directed family whose supremum is above . Hence is in for some . For every , (using ), so there is a such that . By directedness, we can assume without loss of generality that and all the indices , , are equal. (Otherwise replace them by some such that and for every .) For every , we define as if does not contain , as if , and as if contains strictly. We have:
- •
For all , . The key case is when , which follows from the fact that was chosen larger than or equal to every , , and that in this case. When instead, (by ). The cases where , are both different from are easy verifications.
- •
Hence the function satisfies , and trivially as well.
- •
For every , . When , this is because . When , , using .
- •
We have built so that it is in .
- •
For every , is in : when , this is because is in ; otherwise, since is maximal in , cannot contain , so , which is in because , using the induction hypothesis.
- •
For every , : when , this is because ; otherwise, because , using the induction hypothesis.
This finishes to prove claim . Applying this claim to the case where is the whole of , we obtain an element of satisfying conditions and , in , below hence way-below , and such that and for every . In particular, that element is in . By our preliminary remark, is a basis of .
Proposition 9.10
Let be a continuous dcpo and be a bc-domain. Let be a basis of , be a base of the Scott topology on . Let be a basis of , and be a subbase of the Scott topology on . Then:
- •
The set of all -step functions is a basis of .
- •
The set of all opens , , , is a subbase of the Scott topology on . We write for the open subset .
Proof. The first part is Lemma 9.9. The second part is based on Lemma 5.16 of [9], which states that the subsets , , open in , form a subbase of the topology of , as soon as is a continuous poset and is a bc-domain.
We introduce the following abbreviations.
- •
For all , , and for every , denotes .
- •
Given terms and , …, of type , abbreviates:
[TABLE]
In particular, if , this is equal to .
- •
Given terms and , is the term defined as .
- •
Given a term , and such that , is the term of type defined as .
- •
Given terms , …, of type and , …, of type , abbreviates:
[TABLE]
Lemma 9.11
\left\llbracket{\boldsymbol{\mathtt{pif}}\;(M\mathbin{==}\underline{n})\;N\;P}\right\rrbracket\rho* is equal to \left\llbracket{N}\right\rrbracket\rho if \left\llbracket{M}\right\rrbracket\rho=n, to \left\llbracket{P}\right\rrbracket\rho if \left\llbracket{M}\right\rrbracket\rho\neq n,\bot and to \left\llbracket{N}\right\rrbracket\rho\wedge\left\llbracket{P}\right\rrbracket\rho if \left\llbracket{M}\right\rrbracket\rho=\bot;* 2. 2.
\left\llbracket{\boldsymbol{\mathtt{pswitch}}\;M\colon\underline{1}\mapsto N_{1}\mid\cdots\mid\underline{n}\mapsto N_{n}}\right\rrbracket\rho* is equal to \left\llbracket{N_{m}}\right\rrbracket\rho if \left\llbracket{M}\right\rrbracket\rho is an element of , to \bigwedge_{i\in\{1,\cdots,n\}}\left\llbracket{N_{i}}\right\rrbracket\rho if \left\llbracket{M}\right\rrbracket\rho=\bot, and to otherwise. * 3. 3.
\left\llbracket{M\vee N}\right\rrbracket\rho=\sup(\left\llbracket{M}\right\rrbracket\rho,\left\llbracket{N}\right\rrbracket\rho). 4. 4.
\left\llbracket{[{M}\colon{i}]}\right\rrbracket\rho* is equal to if \left\llbracket{M}\right\rrbracket\rho=\top, to if \left\llbracket{M}\right\rrbracket\rho=\bot.*
Proof. 1, 3 and 4 are clear. We prove item 2 by induction on . If , then \left\llbracket{\boldsymbol{\mathtt{pswitch}}\;M\colon\underline{1}\mapsto N_{1}\mid\cdots\mid\underline{n}\mapsto N_{n}}\right\rrbracket\rho=\left\llbracket{\mathop{\boldsymbol{\mathtt{abort}}}\nolimits_{\underline{\tau}}}\right\rrbracket\rho, which is the top element of \left\llbracket{\underline{\tau}}\right\rrbracket, as an easy induction on shows. Note that, in case \left\llbracket{M}\right\rrbracket\rho=\bot, this is also equal to \bigwedge_{i\in\{1,\cdots,n\}}\left\llbracket{N_{i}}\right\rrbracket\rho since . If , then by item 1, \left\llbracket{\boldsymbol{\mathtt{pswitch}}\;M\colon\underline{1}\mapsto N_{1}\mid\cdots\mid\underline{n}\mapsto N_{n}}\right\rrbracket\rho is equal to \left\llbracket{N_{n}}\right\rrbracket\rho if \left\llbracket{M}\right\rrbracket\rho=n, to \left\llbracket{\boldsymbol{\mathtt{pswitch}}\;M\colon\underline{1}\mapsto N_{1}\mid\cdots\mid\underline{n-1}\mapsto N_{n-1}}\right\rrbracket\rho if \left\llbracket{M}\right\rrbracket\rho\in\mathbb{Z}\smallsetminus\{n\}, and to their infimum if \left\llbracket{M}\right\rrbracket\rho=\bot. We then use the induction hypothesis to conclude.
Lemma 9.12
Let and . Assume that \left\llbracket{M}\right\rrbracket\rho is of the form . Then \left\llbracket{{M}\mathrel{\boldsymbol{\mathtt{to}}}{x_{\sigma}}\mathrel{\boldsymbol{\mathtt{in}}}{N}}\right\rrbracket\rho=\bigwedge_{i=1}^{k}\left\llbracket{N}\right\rrbracket\rho[x_{\sigma}\mapsto V_{i}].
Proof. By structural induction on . Let be the map V\in\left\llbracket{\sigma}\right\rrbracket\mapsto\left\llbracket{N}\right\rrbracket\rho[x_{\sigma}\mapsto V]. If is of the form , then:
[TABLE]
by Proposition 4.2, item 2.
If is of the form , then:
[TABLE]
The last equality follows from the fact that finite infima of continuous functions are computed pointwise, by Lemma 4.3, item 2.
Lemma 9.13
\left\llbracket{\boldsymbol{\mathtt{pcase}}\;M_{1}\mapsto N_{1}\mid\cdots\mid M_{n}\mapsto N_{n}}\right\rrbracket\rho* is equal to \bigwedge_{i\in I}\left\llbracket{N_{i}}\right\rrbracket\rho, where I=\{i\in\{1,\cdots,n\}\mid\left\llbracket{M_{i}}\right\rrbracket\rho\neq\top\}.*
Proof. By Lemma 9.11, item 4, \left\llbracket{[{M_{1}}\colon{1}]\owedge\cdots\owedge[{M_{n}}\colon{n}]}\right\rrbracket\rho=\bigwedge_{i=1}^{n}\left\llbracket{[{M_{i}}\colon{i}]}\right\rrbracket\rho=\bigcup_{i=1}^{n}\left\llbracket{[{M_{i}}\colon{i}]}\right\rrbracket\rho=\bigcup_{i\in I}\{i\}=I=\mathop{\uparrow}\nolimits I. By Lemma 9.12, it then follows that \left\llbracket{\boldsymbol{\mathtt{pcase}}\;M_{1}\mapsto N_{1}\mid\cdots\mid M_{n}\mapsto N_{n}}\right\rrbracket\rho is equal to \bigwedge_{i\in I}\left\llbracket{P}\right\rrbracket\rho[y_{\boldsymbol{\mathtt{int}}}\mapsto i] where , and by Lemma 9.11, item 2, this is equal to \bigwedge_{i\in I}\left\llbracket{N_{i}}\right\rrbracket\rho.
It follows:
Proposition 9.14
For every describable value type , for every describable computation type , the type is describable.
Proof. We use Proposition 9.10, with X=\left\llbracket{\sigma}\right\rrbracket, Y=\left\llbracket{\underline{\tau}}\right\rrbracket. (resp., ) is the basis of definable elements of \left\llbracket{\sigma}\right\rrbracket (resp., \left\llbracket{\underline{\tau}}\right\rrbracket). is the base of definable open subsets at type , obtained thanks to Lemma 9.4, and is the subbase of definable open subsets at type .
We first show that all the elements of are definable. This will imply that the definable elements at type form a basis of \left\llbracket{\sigma\to\underline{\tau}}\right\rrbracket. We recall that such an element is a -step function .
Let be defined by ground terms , i.e., \tilde{\chi}_{U_{I}}=\left\llbracket{M_{I}}\right\rrbracket, and let be defined by ground terms . Let us pick a variable . For every subset of , let . (If , the empty disjunction is .) For every environment , and letting , by Lemma 9.13, \left\llbracket{\boldsymbol{\mathtt{pcase}}\;\{M_{I}^{\perp}(x_{\sigma})\mapsto N_{I}\mid I\subseteq\{1,\cdots,m\}\}}\right\rrbracket\rho is equal to the infimum of the values \left\llbracket{N_{I}}\right\rrbracket=y_{I} over the subsets of such that \left\llbracket{M_{I}^{\perp}(x_{\sigma})}\right\rrbracket\rho\neq\top, i.e., such that .
Let be the set of indices between and such that . For every , if and only if for every , is in , if and only if . For every , if and only if for every , , if and only if for every , implies (by contraposition), if and only if for every , implies , if and only if . Therefore \left\llbracket{\boldsymbol{\mathtt{pcase}}\;\{M_{I}^{\perp}(x_{\sigma})\mapsto N_{I}\mid I\subseteq\{1,\cdots,m\}\}}\right\rrbracket\rho is equal to . It follows that is definable as .
Second, we show that all the elements of are definable as ground terms of type . Such an element is of the form , where x=\left\llbracket{M}\right\rrbracket for some ground term , and V=\left\llbracket{P}\right\rrbracket for some ground term . Then is definable as the ground term .
9.3 Valuation Types
We have already mentioned in Section 4 that, for every continuous dcpo, is a pointed continuous dcpo, and that its Scott topology coincides with the weak upwards topology [3]. The latter has a subbase of open sets of the form , for every open subset of and , where . We can restrict further so that , since otherwise is empty. Call a number dyadic if and only if it is of the form , with .
Proposition 9.15
Let be a pointed continuous dcpo. Let be a basis of , be a base of the Scott topology on . Then:
- •
The set of all simple probability valuations , where each is a dyadic number in , , and each is a point in , is a basis of .
- •
The set of all opens , where is an element of , and is a dyadic number in , is a subbase of the Scott topology on .
Proof. By a theorem of Jones [13, Theorem 5.2], the simple subprobability valuations form a basis of . For every simple subprobability valuation , one easily checks that the collection of simple subprobability valuations with dyadic and way-below in , and way-below , is directed, and .
We check that every element of , as written above, is way-below . For convenience, we let . Let be a directed family in with a supremum above . We wish to show that there is a such that for every open subset of , . In order to do so, we show that for every subset of , there is an index such that for every open subset of such that , . By directedness, there is a such that for every such , and this will show the claim.
Henceforth, let us fix . We have (because for each , and recalling that iff or ) \leq\nu(\bigcup_{i\in J}\hbox to0.0pt{\uparrow\hss}\raise 2.15277pt\hbox{\uparrow}y_{i}) (because for each ), so there is a such that \sum_{i\in J}b_{i}\leq\nu_{k}(\bigcup_{i\in J}\hbox to0.0pt{\uparrow\hss}\raise 2.15277pt\hbox{\uparrow}y_{i}). For every open subset with , \mu(U)=\sum_{i\in J}b_{i}\leq\nu_{k}(\bigcup_{i\in J}\hbox to0.0pt{\uparrow\hss}\raise 2.15277pt\hbox{\uparrow}y_{i})\leq\nu_{k}(U), which finishes the proof.
It is standard domain theory that given a dcpo , a point that is the supremum of a directed family , where is itself the supremum of a directed family of points way-below , then is directed and has as supremum. In our case is included in , showing that every continuous probability valuation is the supremum of a directed family of elements of .
In order to show the second part of the proposition, we consider an arbitrary subbasic open set of the weak upwards (=Scott) topology, open in , . We write as , where each is in , and as the infimum of the numbers . Since , is in for large enough. For every , if and only if for some large enough , if and only if for some large enough and some finite subset of , . Hence , showing that is a subbase of the weak upwards (=Scott) topology.
Corollary 9.16
For every describable value type , the type is describable.
Proof. Let X=\left\llbracket{\sigma}\right\rrbracket, be the basis of definable elements of \left\llbracket{\sigma}\right\rrbracket, be a strong base of definable open subsets at type guaranteed by Lemma 9.4, and let us use Proposition 9.15.
Although is not associative, we can make sense of sums of terms of type : when , this is just , otherwise this is . This way, \left\llbracket{M_{1}\oplus M_{2}\oplus\cdots\oplus M_{2^{n}}}\right\rrbracket\rho is simply equal to \frac{1}{2^{n}}\sum_{i=1}^{2^{n}}\left\llbracket{M_{i}}\right\rrbracket\rho.
For every element in , we can write each () as , where and with the same for all values of . Hence, and letting , can be written as a sum , where each is in . Since is describable, for each () is equal to \left\llbracket{M_{i}}\right\rrbracket for some ground term ( is equal to \left\llbracket{\Omega_{\sigma}}\right\rrbracket). Also, [math] is equal to \left\llbracket{\Omega_{\boldsymbol{\mathtt{V}}\sigma}}\right\rrbracket, so is definable as the sum of the terms , plus terms .
Let be an element of , where , , and is a dyadic number in . Each is definable, that is, \tilde{\chi}_{U_{i}}=\left\llbracket{M_{i}}\right\rrbracket for some ground term . Let us fix a variable . For each , let : \left\llbracket{M^{\prime}(x_{\sigma})}\right\rrbracket\rho=\top if , otherwise. Then is definable by the term . Indeed, letting ,
[TABLE]
so \left\llbracket{\bigcirc_{>r}(\mathop{\boldsymbol{\mathtt{produce}}}(\mathop{\boldsymbol{\mathtt{do}}}\nolimits{x_{\sigma}\leftarrow y_{\boldsymbol{\mathtt{V}}\sigma}};{\mathop{\boldsymbol{\mathtt{ret}}}\nolimits M^{\prime}}))}\right\rrbracket\rho is equal to if , otherwise.
9.4 Types
The upper Vietoris topology on (resp., ) has basic open sets , where ranges over the open subsets of . The operator commutes with finite intersections and with directed suprema. Moreover, is Scott-open if is well-filtered.
Proposition 9.17
Let be a pointed, coherent, continuous dcpo. Let be a basis of , be a subbase of the Scott topology on . Then:
- •
The set consisting of plus the compact saturated sets of the form , , where each is in , is a basis of .
- •
The set of all opens , where ranges over non-empty finite unions of elements of , plus the whole space itself, is a base of the Scott topology on .
Proof. By Proposition 4.2, item 1, if and only if or . Now can be written as \bigcup_{x\in Q\cap B_{X}}\hbox to0.0pt{\uparrow\hss}\raise 2.15277pt\hbox{\uparrow}x, and since is compact, if then there are finitely many elements , …, of such that Q^{\prime}\subseteq\bigcup_{i=1}^{n}\hbox to0.0pt{\uparrow\hss}\raise 2.15277pt\hbox{\uparrow}x_{i}=\text{int}({\mathop{\uparrow}\nolimits\{x_{1},\cdots,x_{n}\}}). By Lemma 9.8, this shows the first part.
Let be a Scott-open subset of . If , then is the whole space, which is in . Otherwise, is a Scott-open subset of . By Proposition 4.1, item 1, is a continuous complete lattice, so is a union of sets of the form \hbox to0.0pt{\uparrow\hss}\raise 2.15277pt\hbox{\uparrow}Q, where ranges over the elements of belonging to any given basis, and \uparrow$$\uparrow is understood in . Using the first part, we can take those elements of the form , and then \hbox to0.0pt{\uparrow\hss}\raise 2.15277pt\hbox{\uparrow}Q=\{Q\in\mathcal{Q}^{\top}(X)\mid Q^{\prime}\subseteq\text{int}({\mathop{\uparrow}\nolimits\{x_{1},\cdots,x_{n}\}})\}=\Box\text{int}({\mathop{\uparrow}\nolimits\{x_{1},\cdots,x_{n}\}}).
We can therefore write as a union of sets , open in , and then we can write as a union of finite intersections (taken in ) of elements of , hence as a directed union of finite unions of finite intersections of elements of , hence (by distributivity) as a directed union of finite intersections of finite unions of elements of . In (not ), commutes with directed unions and finite intersections (this would not hold for the empty intersection in ). The result follows.
Corollary 9.18
For every describable value type , is a describable computation type.
Proof. Let X=\left\llbracket{\sigma}\right\rrbracket, be the basis of definable elements of \left\llbracket{\sigma}\right\rrbracket, and be the subbase of definable open subsets at type , and let us use Proposition 9.17.
For every element of , where each is in , hence x_{i}=\left\llbracket{M_{i}}\right\rrbracket for some ground term , the term ( if ) defines , in the sense that Q=\left\llbracket{M}\right\rrbracket. The term defines .
We deal with the second part. The whole space \left\llbracket{\boldsymbol{\mathtt{F}}{}\sigma}\right\rrbracket is definable as an open set by the term . We consider the other elements of . Let us write as a finite union of elements of , where is defined by in the sense that \tilde{\chi}_{U_{i}}=\left\llbracket{M_{i}}\right\rrbracket. Then is defined by , where . Indeed, for every environment , letting , if then \left\llbracket{\lambda x_{\boldsymbol{\mathtt{F}}{}\sigma}.{x_{\boldsymbol{\mathtt{F}}{}\sigma}}\mathrel{\boldsymbol{\mathtt{to}}}{y_{\sigma}}\mathrel{\boldsymbol{\mathtt{in}}}{M(y_{\sigma})}}\right\rrbracket(\bot)=\bot, matching the fact that is not in . Otherwise, using the fact that \left\llbracket{\bigcirc_{>1/2}(M_{1}y_{\sigma})\vee\cdots\vee\bigcirc_{>1/2}(M_{m}y_{\sigma})}\right\rrbracket\rho^{\prime} is equal to if and to otherwise, for every environment , we obtain:
[TABLE]
by Proposition 4.2, item 2, and that is equal to if , and to otherwise.
9.5 Full Abstraction
By induction on types, using Lemma 9.2 (), Lemma 9.3 (), Proposition 9.6 (product types), Proposition 9.14 (function types), Corollary 9.16 ( types), and Corollary 9.18 ( types), every type is describable (the case of types is trivial).
Theorem 9.19** (Full abstraction)**
CBPV is inequationally fully abstract. For every value type , for every two ground CBPV terms , the following are equivalent:
; 2. 2.
; 3. 3.
\left\llbracket{M}\right\rrbracket\leq\left\llbracket{N}\right\rrbracket.
Proof. The equivalence between 1 and 2 is Theorem 7.3. Item 3 implies item 1 by Proposition 7.6. In the converse direction, we assume that \left\llbracket{M}\right\rrbracket\not\leq\left\llbracket{N}\right\rrbracket and we claim that there is a ground term such that . Since is the specialization ordering of the Scott topology on \left\llbracket{\tau}\right\rrbracket, and the latter has a subbase of definable elements, there is a ground term such that \left\llbracket{M}\right\rrbracket\in U and \left\llbracket{N}\right\rrbracket\not\in U, where \tilde{\chi}_{U}=\left\llbracket{Q}\right\rrbracket. Hence \left\llbracket{QM}\right\rrbracket=\tilde{\chi}_{U}(\left\llbracket{M}\right\rrbracket)=\{\delta_{\top}\}, while \left\llbracket{QN}\right\rrbracket=\bot. By adequacy (Proposition 6.10), and letting , \mathop{\text{Pr}}(QM\mathbin{\downarrow})={h}^{*}(\left\llbracket{QM}\right\rrbracket)=1, while .
10 Conclusion and Open Problems
We started from the question of using call-by-push-value as a way of getting around our ignorance of the existence of a Cartesian-closed category of continuous dcpos that would be closed under the probabilistic powerdomain functor. This led us to define a pretty expressive call-by-push-value language with probabilistic choice and demonic non-determinism. We have gone so far as to show that it is inequationally fully abstract, once extended with parallel if and statistical termination testers —and those are required for that.
One should note that both are implementable: by standard dovetailing techniques, or more concretely by using threads, and by guessing and checking a derivation of , or more concretely by simulating all the execution traces of and counting their probabilities. The latter can be done, concretely, by running under a hypervisor that forks the process it emulates at each random binary choice : each subprocess that terminates after having gone through random binary choices contributes to a global counter, and the hypervisor itself terminates when that counter exceeds .
A few questions remain:
Is definable in CBPV? Is CBPV fully abstract? The results of Section 8.1 fail to answer those questions. 2. 2.
We have defined languages with an operator, and where computation types are interpreted as continuous lattices. Would bc-domains be enough, namely, can we do without an operator and still obtain a full abstraction result? Note that does not just estimate probabilities of termination, but also catches the exception raised by , hence serves more than one purpose. 3. 3.
Since the type is describable in CBPV for every value type , the binary supremum map on \left\llbracket{\boldsymbol{\mathtt{F}}{}\tau}\right\rrbracket is obtainable as a directed supremum of definable values. Whereas implements demonic non-determinism, binary suprema implement angelic non-determinism. Is binary supremum itself definable?
The reference list from the paper itself. Each links out to its DOI / PubMed record.
- 1[1] Samson Abramsky, Radha Jagadeesan, and Pasquale Malacaria. Full abstraction for PCF. Information and Computation , 163(2):409–470, 2000.
- 2[2] Samson Abramsky and Achim Jung. Domain theory. In S. Abramsky, D. M. Gabbay, and T. S. E. Maibaum, editors, Handbook of Logic in Computer Science , volume 3, pages 1–168. Oxford University Press, 1994.
- 3[3] Mauricio Alvarez-Manilla, Achim Jung, and Klaus Keimel. The probabilistic powerdomain for stably compact spaces. Theoretical Computer Science , 328(3):221–244, 2004.
- 4[4] Thomas Ehrhard and Christine Tasson. Probabilistic call by push value. Logical Methods in Computer Science , 15(1), 2019. Also ar Xiv:1607.04690 v 4 [cs.LO], Aug. 2018.
- 5[5] Thomas Ehrhard, Christine Tasson, and Michele Pagani. Probabilistic coherence spaces are fully abstract for probabilistic PCF. In Suresh Jagannathan and Peter Sewell, editors, Proc. 41st Ann. ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’14) , pages 309–320, 2014.
- 6[6] Thomas Erker, Martín Hötzel Escardó, and Klaus Keimel. The way-below relation of function spaces over semantic domains. Topology and Its Applications , 89(1–2):61–74, 1998.
- 7[7] Yuri L. Ershov. The bounded-complete hull of an α 𝛼 \alpha -space. Theoretical Computer Science , 175:3–13, 1997.
- 8[8] Gerhard Gierz, Karl Heinrich Hofmann, Klaus Keimel, Jimmie D. Lawson, Michael Mislove, and Dana S. Scott. Continuous Lattices and Domains , volume 93 of Encyclopedia of Mathematics and its Applications . Cambridge University Press, 2003.