Interpreting Lambda Calculus in Domain-Valued Random Variables

Furber, Robert; Mardare, Radu; Panangaden, Prakash; Scott, Dana

doi:10.4230/LIPIcs.CSL.2026.48

Interpreting Lambda Calculus in Domain-Valued Random Variables

Robert Furber

Heriot-Watt University, Edinburgh, UK Radu Mardare

Heriot-Watt University, Edinburgh, UK Prakash Panangaden

McGill University, Montreal, Canada Dana Scott Carnegie Mellon University, Pittsburgh, PA, USA

Abstract

We develop Boolean-valued domain theory and show how the lambda-calculus can be interpreted using domain-valued random variables. We focus on the reflexive domain construction rather than the language and its semantics. We develop the Boolean-valued set theory needed from scratch and then develop Boolean-valued domain theory on top of that. The notions of equality and partial order have to be given Boolean-valued interpretations; when we say that an equation is valid in the model we mean that its interpretation is the top element of the Boolean algebra.

Keywords and phrases:

lambda calculus, domain theory, random variables

Copyright and License:

2012 ACM Subject Classification:

Theory of computation ; Theory of computation

\rightarrow

Probabilistic computation ; Theory of computation

\rightarrow

Lambda calculus ; Theory of computation

\rightarrow

Denotational semantics

Editors:

Stefano Guerrini and Barbara König

Series and Publisher:

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

1 Introduction

There has been burgeoning interest in probabilistic programming languages in the last decade. The main motivation is building compositional models of probabilistic processes and performing inference on them [25, 16, 33]. For machine learning applications the notion of conditioning is fundamental and the striking results of [1, 2] show that this is a subtle issue.

The combination of probability and higher type programming has been both technically challenging and important for the development of semantics for such languages. There are a variety of approaches based on probabilistic coherence spaces [10] or cones [9], quasi-Borel spaces [31, 17, 32] and Boolean-valued models [3] which was based on Dana Scott’s vision [28]. Stochastic lambda-calculi have appeared [6, 7, 8] with important contributions to the understanding of probability theory at higher type. The work on quasi-Borel spaces gives a cartesian closed category that can serve as the foundation for a typed higher-order probabilistic programming language [17].

In [3] a Boolean-valued domain theory was developed. The idea is to use one of the standard set-theoretic models of the $\lambda$ -calculus but interpreted in a suitable Boolean-valued universe of sets. However, the basic domain theoretic definitions of directed set, supremum, reflexive dcpo and continuity were interpreted as usual. The theory presented there is rather complicated and had artificial restrictions on the way randomness was handled. In the present paper a completely Boolean-valued point of view is adopted and even basic concepts, like equality and order, are all interpreted in a Boolean-valued logic. This leads to a much simpler theory but still in line with the vision of [28]. The version of Boolean-valued domain theory used in the current paper supersedes [3] by working “internally”, by transferring theorems from ordinary logic to Boolean-valued logic as much as possible, rather than the “bare handed” approach of [3].

We show that untyped $\lambda$ -calculus can be interpreted in domain-valued random variables. In order to employ the theory of Boolean-valued sets, for most of the article we actually use the Boolean-valued power set rather than random variables, and then show that there is an isomorphism between the two at the end. We focus on the reflexive domain construction rather than the language and its semantics.

The main contribution of this paper is the completely Boolean-valued reconstruction of domain theory. The notion of equality has to be interpreted in the Boolean algebra and when we say that an equation is valid in the model we mean that its interpretation is the top element of the domain.

What makes the theory of Boolean-valued sets necessary is that domain-valued random variables do not form a continuous dcpo. However, when “continuous dcpo” is given its interpretation in Boolean-valued sets, they are. The version of Boolean-valued sets we have used is the original version in terms of a cumulative hierarchy. If the reader prefers, they may rephrase the arguments results in terms of topos theory in a Boolean topos, and we outline the connection of the two in Section 3, though the only part of this theory that we use is the ability to define functions. As an example of how to apply Boolean-valued domain theory, we show that there exist two sets of integers, neither of which can be mapped to the other by a $\lambda$ -definable function. The reason for choosing this example is that it shows that $\lambda$ -calculus and its model based on domain-valued random variables are powerful enough to prove a fact that does not mention probability in its statement, and such that the proof is pure $\lambda$ -calculus and probability and doesn’t need to pass via the equivalence between $\lambda$ -definability and general recursion and applying the Kleene-Post theorem [20] that there are incomparable many-one degrees. The proof, however, is inspired by Spector’s probabilistic proof [30].

For reasons of space, the complete proofs of some results are omitted, even from the appendix. However, they can be found in the “related version” on the arxiv, linked above.

2 Background on Boolean-Valued Set Theory

In this section we describe how statements and proofs in ordinary set theory can be re-interpreted in a Boolean-valued sense. This interpretation is originally due to Scott and Solovay [26, 19, 5].

Throughout this section we let $A$ be an arbitrary complete Boolean algebra. It will play the role that the two-element Boolean algebra $2$ plays in ordinary logic. We can build up the class of $A$ -valued sets, $V^{A}$ , by considering an $A$ -valued set $X$ to be a partial function that assigns to each element $x$ of its domain the amount, valued in $A$ , that $x$ is an element of $X$ . We build up $V^{A}$ by the following generalization of von Neumann’s construction:

V^{A}_{0}=\emptyset,\nobreak\ \nobreak\ \nobreak\ V^{A}_{\alpha+1}=\{f:V^{A}_{% \alpha}\rightharpoonup A\},\nobreak\ \nobreak\ \nobreak\ V^{A}_{\alpha}=% \bigcup_{\beta<\alpha}V^{A}_{\beta}\nobreak\ \nobreak\ \text{for }\alpha\text{% a limit ordinal.}

Then either informally, or using proper classes, $V^{A}=\bigcup\limits_{\alpha\in\mathbf{Ord}}V^{A}_{\alpha}$ .

We use the term $A$ -valued set for the elements of $V^{A}$ , but we also will use the shorter term $A$ -set, and this helps to avoid certain confusions arising from the term “valued”.

We can then interpret $\in$ , $\subseteq$ and $=$ by the following mutually recursive formulas:

	$\displaystyle\\|x\in X\\|=\bigvee_{t\in\mathrm{dom}X}\\|x=t\\|\land X(t)$	$\displaystyle\\|X\subseteq Y\\|=\bigwedge_{t\in\mathrm{dom}X}X(t)\Rightarrow\\|t% \in Y\\|$
	$\displaystyle\\|x=y\\|=\\|x\subseteq y\\|\land\\|y\subseteq x\\|.$

In the above, and all that follows, we use an operator precedence convention for $\bigvee$ and $\bigwedge$ that agrees with operator precedence for $\exists$ and $\forall$ , so there is an implicit bracket around everything to the right of such a join or meet.

Recall that the first-order language of set theory, which we write as $\mathfrak{L}_{\mathbf{Set}}$ , is the usual first-order language for a signature with equality and one two-place relation symbol, namely $\in$ . We write $\mathfrak{L}_{\mathbf{Set}}(V^{A})$ for this language extended with constants from $V^{A}$ .

In any Boolean algebra, we can interpret the connectives of propositional logic. Using the completeness of $A$ , we can interpret the universal quantifier as a meet and the existential quantifier as a join. All together, this gives us an interpretation of $\mathfrak{L}_{\mathbf{Set}}(V^{A})$ in $V^{A}$ .

Theorem 1 ( $V^{A}$ as a model).

(i)

If $\phi\in\mathfrak{L}_{\mathbf{Set}}(V^{A})$ is a theorem of ZFC set theory, then $\|\phi\|=1$ in $V^{A}$ .
(ii)

The inference rules of first-order logic can be applied to theorems of ZFC set theory and statements about elements of $V^{A}$ in $\mathfrak{L}_{\mathbf{Set}}(V^{A})$ .
(iii)

If $\|\exists x.\Phi(x,X_{1},\cdots,X_{n})\|=a$ , where $X_{1},\ldots,X_{n}\in V^{A}$ (and we allow $n=0$ ), then there exists $X_{0}\in V^{A}$ such that $\|\Phi(X_{0},X_{1},\cdots,X_{n})\|=a$ .

The constructions of singletons $\{x\}^{A}$ , unordered pairs $\{x,y\}^{A}$ and ordered pairs $(x,y)^{A}$ are done as usual in set theory, but interpreted in $V^{A}$ . Details can be found in the arxiv version. For $X,Y\in V^{A}$ we define $X\mathrel{\times_{\!A}}Y$ as follows.

$X\mathrel{\times_{\!A}}Y:\{(x,y)^{A}\mid x\in\mathrm{dom}(X),y\in\mathrm{dom}(% Y)\}\rightarrow A$

$(X\mathrel{\times_{\!A}}Y)(x,y)^{A}=\|x\in X\|\land\|y\in Y\|.$
For each $A$ -set $X$ , the $A$ -valued power set $\mathcal{P}^{A}(X)$ is defined by

$\mathrm{dom}(\mathcal{P}^{A}(X))=\{u\in V^{A}\mid\mathrm{dom}(u)=\mathrm{dom}(% X)\text{ and }\forall t\in\mathrm{dom}(u).u(t)\leq X(t)\}$

$\mathcal{P}^{A}(X)(u)=1$
For all $S,X\in V^{A}$ we have $\|S\in\mathcal{P}^{A}(X)\|=\|S\subseteq X\|,$ which is how the power set axiom is proved for $V^{A}$ .
If $\Phi$ is a set-theoretic formula we can define the $A$ -set

\{x\in X\mid\Phi(x)\}^{A}:\mathrm{dom}(X)\rightarrow A\nobreak\ \nobreak\ % \text{ by}

\{x\in X\mid\Phi(x)\}^{A}(t)=X(t)\land\|\Phi(t)\|,

which proves the axiom of separation for $V^{A}$ .

If we now consider von Neumann’s universe $V$ of classic set theory constructed inductively on ordinals $\alpha\in\mathbf{Ord}$ , then for each set $S\in V_{\alpha}$ , there is a corresponding element $\check{S}\in V^{A}_{\alpha}$ defined recursively. The domain of $\check{S}$ is $\{\check{x}\mid x\in S\}$ , and it is defined by:

\check{\emptyset}=\emptyset,\nobreak\ \nobreak\ \nobreak\ \text{and }\nobreak% \ \check{S}(\check{x})=1\nobreak\ \text{for all }x\in S.

To describe how a statement in set theory about an ordinary set in $X\in V$ translates to a statement about $\check{X}\in V^{A}$ , we need the notion of a $\Delta_{0}$ statement. Bounded quantifiers are those of the form $\forall x\in X.\Phi(x)$ and $\exists x\in X.\Psi(x)$ , i.e. in the language of set theory $\forall x.x\in X\Rightarrow\Phi(x)$ and $\exists x.x\in X\land\Psi(x)$ . A $\Delta_{0}$ formula $\Phi\in\mathfrak{L}_{\mathbf{Set}}(V^{A})$ is one containing only bounded quantifiers. We have $\Delta_{0}$ invariance¹¹1Note that Bell uses the alternative terminology “restricted” for $\Delta_{0}$ . [19, Lemma 14.21] or [5, Theorem 1.23 (v)].

Theorem 2 ( $\Delta_{0}$ invariance).

Let $\Phi(x_{1},\ldots,x_{n})$ be a $\Delta_{0}$ -formula, whose free variables are $x_{1},\ldots,x_{n}$ . Let $X_{1},\cdots,X_{n}\in V$ . Then, $\Phi(X_{1},\ldots,X_{n})\Leftrightarrow\|\Phi(\check{X}_{1},\ldots,\check{X}_{% n})\|=1.$

We point out some useful consequences of Theorem 2. The statements “ $S$ is a singleton whose only element is $x$ ”, “ $S$ is an unordered pair of $x$ and $y$ ” and “ $S$ is an ordered pair, first element $x$ , second element $y$ ” are all $\Delta_{0}$ statements, and so the following all hold

\displaystyle\widecheck{\{x\}}

\displaystyle=\{\check{x}\}^{A}

\displaystyle\widecheck{\{x,y\}}

\displaystyle=\{\check{x},\check{y}\}^{A}

\displaystyle\widecheck{(x,y)}

\displaystyle=(\check{x},\check{y})^{A}.

Another important consequence of Theorem 2 is that $\check{\omega}$ is the smallest inductive²²2In the sense used to formulate the axiom of infinity in ZF. $A$ -set in $V^{A}$ , so that $\check{\omega}$ is the $\omega$ of $V^{A}$ . Given any set $X$ , we say a subset $S\subseteq X$ is finite if there exists $n\in\omega$ and $f:n\rightarrow X$ such that $S=\mathrm{im}(f)$ . We write $\mathcal{P}_{\mathrm{fin}}(X)$ for the set of all finite subsets of $X$ . If we interpret this with $A$ -sets, for each $X\in V^{A}$ we can define $\mathcal{P}^{A}_{\mathrm{fin}}(X)$ to be the set of finite $A$ -subsets of $X$ , using the axiom of separation. The following proposition is a consequence of the distributive law – see [21, 3.1.11].

Proposition 3.

For all sets $X$ , $\nobreak\ \nobreak\ \nobreak\ \|\mathcal{P}^{A}_{\mathrm{fin}}(\check{X})=% \widecheck{\mathcal{P}_{\mathrm{fin}}(X)}\|=1.$

We can define the category $\mathbf{Set}_{A}$ from $V^{A}$ as follows. The class of objects is $V^{A}$ , and for each $X,Y\in V^{A}$ , the set of functions $\{X\overset{A}{\rightarrow}Y\}\in V^{A}$ can be defined using products, power set, and the axiom of separation. We define:

\displaystyle\mathbf{Set}_{A}(X,Y)

\displaystyle=\{f\in\mathrm{dom}(\{X\overset{A}{\rightarrow}Y\})\mid\|f\in\{X% \overset{A}{\rightarrow}Y\}\|=1\}/\sim,

where $\sim$ is the equivalence relation defined by $f\sim g$ iff $\|f=g\|=1$ . Identity elements are defined as identity relations, and composition by composition of relations, which is well-defined with respect to $\sim$ .

3 Boolean-Valued Setoids

We now discuss the kind of “Boolean-valued sets” that are essentially $A$ -valued models of the theory of $=$ . These can be considered an alternative description of either sheaves or separated presheaves on $A$ , and are usually discussed in the more general case where $A$ is a Heyting algebra, such as in [12, 15, 24]. Although we will use only one definition of $A$ -valued sets, the distinction between $A$ -valued relations that satisfy the definition of a function internally and functions that do so gives us two distinct categories.

In order to distinguish the $A$ -valued sets we will be discussing from elements of $V^{A}$ , we call them $A$ -valued setoids³³3Setoid is a long-established term for a set equipped with an equivalence relation., or simply $A$ -setoids. An $A$ -setoid is a pair $(X,\|\mbox{$=$}\|_{X})$ where $X$ is a set, $\|\mbox{$=$}\|_{X}:X\times X\rightarrow A$ . The two axioms of $\|\mbox{$=$}\|_{X}$ are symmetry and transitivity, i.e.

	$\displaystyle\forall x,y\in X.\\|x=y\\|_{X}$	$\displaystyle=\\|y=x\\|_{X}$
	$\displaystyle\forall x,y,z\in X.\\|x=y\\|_{X}\land\\|y=z\\|_{X}$	$\displaystyle\leq\\|x=z\\|_{X}.$

so $A$ -valued setoids are “ $A$ -valued partial equivalence relations”.

Since reflexivity is not assumed, the statement $\|x=x\|_{X}$ does not represent a tautology, but its intended interpretation is, in some sense, the degree to which $x\in X$ , or the place where $x\in X$ . So we define the notation $\varepsilon_{X}(x)=\|x=x\|_{X}$ .

We say $(X,\|\mbox{$=$}\|_{X})$ is total if $\|x=x\|_{X}=1$ for all $x\in X$ , i.e. if reflexivity holds; it is strict if $\|x=y\|_{X}=1$ implies $x=y$ .

Definition 4.

Let $(X,\|\mbox{$=$}\|_{X})$ be an $A$ -setoid. We say it is complete⁴⁴4This definition is slightly different from that used in [12, 4.10,4.11] and elsewhere, which would not suit us because under that definition $\mathcal{P}^{A}(X)$ is not complete, when considered as an $A$ -setoid in the sense we will define in Definition 14. if either, hence both, of the following equivalent properties holds:

(i)

For any family of elements $(a_{i})_{i\in I}$ in $A$ and corresponding family $(x_{i})_{i\in I}$ in $X$ such that for all $i,j\in I$ , $a_{i}\land a_{j}\leq\|x_{i}=x_{j}\|_{X}$ , there exists $x\in X$ such that for all $i\in I$ , $a_{i}\leq\|x_{i}=x\|_{X}$ .
(ii)

For any pairwise disjoint family of elements $(a_{i})_{i\in I}$ in $A$ and corresponding family $(x_{i})_{i\in I}$ in $X$ such that for all $i\in I$ , $a_{i}\leq\|x_{i}=x_{i}\|_{X}$ , there exists $x\in X$ such that for all $i\in I$ , $a_{i}\leq\|x_{i}=x\|_{X}$ .

Definition 5.

If $(X,\|\mbox{$=$}\|_{X})$ is an $A$ -setoid and $(Y,\|\mbox{$=$}\|_{Y})$ is a set and a function $\|\mbox{$=$}\|_{Y}:Y\times Y\rightarrow A$ , and $f:X\rightarrow Y$ is a bijection such that for all $x_{1},x_{2}\in X$ :

\|f(x_{1})=f(x_{2})\|_{Y}=\|x_{1}=x_{2}\|_{X},

then we say $f$ is a strict isomorphism, and it follows that $(Y,\|\mbox{$=$}\|_{Y})$ is an $A$ -setoid, and is total, strict or complete iff $(X,\|\mbox{$=$}\|_{X})$ is.

Definition 6.

The product $(X,\|\mbox{$=$}\|_{X})\times(Y,\|\mbox{$=$}\|_{Y})$ is defined to have

\|(x,y)=(x^{\prime},y^{\prime})\|_{X\times Y}=\|x=x^{\prime}\|_{X}\land\|y=y^{% \prime}\|_{Y}.

Definition 7.

A predicate on $(X,\|\mbox{$=$}\|_{X})$ is a function $S:X\rightarrow A$ such that:

(i)

For all $x_{1},x_{2}\in X$ , $\|x_{1}=x_{2}\|_{X}\leq S(x_{1})\Leftrightarrow S(x_{2})$ .
(ii)

For all $x\in X$ , $S(x)\leq\varepsilon_{X}(x)$ .

A binary relation $X\rightarrow Y$ is simply a predicate on $X\times Y$ .

This allows us to define a category of setoids with relations that satisfy the internal definition of a function (“relational functions”) as morphisms.

Definition 8.

The category $\mathbf{SetoidR}_{A}$ has $A$ -setoids as objects and a morphism is a relation $f:X\rightarrow Y$ such that (additionally to (i) and (ii) from Definition 7):

(iii)

For all $x\in X$ , $y_{1},y_{2}\in Y$ , $f(x,y_{1})\land f(x,y_{2})\leq\|y_{1}=y_{2}\|_{Y}$ .
(iv)

For all $x\in X$ , $\varepsilon_{X}(x)\leq\bigvee_{y\in Y}f(x,y)$ .

The identity function $\mathrm{id}_{X}:X\rightarrow X$ is defined by: $\mathrm{id}_{X}(x_{1},x_{2})=\|x_{1}=x_{2}\|_{X}.$
Composition of functions $f:X\rightarrow Y$ and $g:Y\rightarrow Z$ is defined by

(g\circ f)(x,z)=\bigvee_{y\in Y}f(x,y)\land g(y,z).\qquad

We define the category of $A$ -setoids and “functional functions”, $\mathbf{SetoidF}_{A}$ , as follows.

Definition 9.

The category $\mathbf{SetoidF}_{A}$ has $A$ -setoids as objects. The morphisms are defined starting with an $A$ -setoid:

	$\displaystyle X\multimap Y$	$\displaystyle=\{f:X\rightarrow Y\mid\forall x_{1},x_{2}\in X.\\|x_{1}=x_{2}\\|_{% X}\leq\\|f(x_{1})=f(x_{2})\\|_{Y}\}$
	$\displaystyle\\|f_{1}=f_{2}\\|_{X\multimap Y}$	$\displaystyle=\bigwedge_{x\in X}\varepsilon_{X}(x)\Rightarrow\\|f_{1}(x)=f_{2}(% x)\\|_{Y}.$

Then the hom set $\mathbf{SetoidF}_{A}(X,Y)$ is the quotient set of this,⁵⁵5Monro calls these admissible functions in [24, Definition 5.2]. i.e. $X\multimap Y$ modulo the equivalence relation:

f_{1}\sim f_{2}\text{ iff }\forall x\in X.\varepsilon_{X}(x)\leq\|f_{1}(x)=f_{% 2}(x)\|_{Y}.

Identity maps and composition are defined as for functions.

The category $\mathbf{SetoidF}_{A}$ is called $\mathbf{Mod}_{0}(A)$ in [24, Definition 5.2], where it is proved to be a quasi-topos. The full subcategory on non-empty⁶⁶6We mean not having $\emptyset$ as an underlying set. It is still allowed, and necessary, to have sets that do not assign any value other than $0$ to any element, which are “empty” in terms of Boolean-valued logic. complete $A$ -setoids is a topos [24, Proposition 5.6 (ii)] equivalent to the category of sheaves on the canonical topology on $A$ .

Mapping a functional function to its graph defines a faithful functor from $\mathbf{SetoidF}_{A}\rightarrow\mathbf{SetoidR}_{A}$ .

Definition 10.

The following defines a faithful functor $\boldsymbol{\gamma}:\mathbf{SetoidF}_{A}\rightarrow\mathbf{SetoidR}_{A}$ . On objects, $\boldsymbol{\gamma}(X,\|\mbox{$=$}\|_{X})=(X,\|\mbox{$=$}\|_{X})$ . For $f\in\mathbf{SetoidF}_{A}(X,Y)$ , we define

\boldsymbol{\gamma}(f)(x,y)=\varepsilon_{X}(x)\land\|f(x)=y\|_{Y}.

We can formulate a notion of poset that does not require us to define $\|\mbox{$=$}\|_{X}$ but can instead be defined in terms of it. It turns out to be useful in the general theory, as well as for dealing with posets that are $A$ -setoids or $A$ -sets.

Definition 11.

An $A$ -poset is a pair $(X,\|\mbox{$\leq$}\|_{X})$ , where $X$ is a set and $\|\mbox{$\leq$}\|_{X}:X\times X\rightarrow A$ is such that for all $x_{1},x_{2},x_{3}\in X$ :

(i)

$\|x_{1}\leq x_{2}\|_{X}\land\|x_{2}\leq x_{3}\|_{X}\leq\|x_{1}\leq x_{3}\|_{X}.$
(ii)

$\|x_{1}\leq x_{2}\|_{X}\leq\|x_{1}\leq x_{1}\|_{X}\land\|x_{2}\leq x_{2}\|_{X}.$

We then define $\|\mbox{$=$}\|_{X}$ by

\|x_{1}=x_{2}\|_{X}=\|x_{1}\leq x_{2}\|_{X}\land\|x_{2}\leq x_{1}\|_{X}.

(1)

Then $(X,\|\mbox{$=$}\|_{X})$ is an $A$ -setoid, and $\|\mbox{$\leq$}\|_{X}$ is a reflexive, antisymmetric, transitive relation when these statements are interpreted in the $A$ -valued sense. If $(X,\|\mbox{$=$}\|_{X})$ is an $A$ -setoid and $\|\mbox{$\leq$}\|_{X}$ is a relation that is reflexive, antisymmetric and transitive, in the $A$ -valued sense, then $(X,\|\mbox{$\leq$}\|_{X})$ is an $A$ -poset in the above sense, and $\|\mbox{$=$}\|_{X}$ satisfies (1).

Since $\|\mbox{$=$}\|_{X}$ is defined in terms of $\|\mbox{$\leq$}\|_{X}$ , the following fact is convenient for proving that a function on underlying sets $f:X\rightarrow Y$ not only defines an element of $\mathbf{SetoidF}_{A}(X,Y)$ but also a monotone function in the $A$ -valued sense.

Lemma 12.

Let $(X,\|\mbox{$\leq$}\|_{X}),(Y,\|\mbox{$\leq$}\|_{Y})$ be $A$ -posets, and suppose that $f:X\rightarrow Y$ is $A$ -monotone in the sense⁷⁷7This is monotonicity using the interpretation of logic in Section 2. that for all $x_{1},x_{2}\in X$ , $\|x_{1}\leq x_{2}\|_{X}\leq\|f(x_{1})\leq f(x_{2})\|_{Y}.$
Then $f\in X\multimap Y$ . Every $f\in\mathbf{SetoidF}_{A}(X,Y)$ that is monotone in the $A$ -valued interpretation of the term is of this form.

The following definition and theorem are based on [23, Proposition 3.3].

Definition 13.

Let $(X,\|\mbox{$=$}\|_{X}),(Y,\|\mbox{$=$}\|_{X})$ be $A$ -setoids such that $Y$ is complete, and let $f\in\mathbf{SetoidR}_{A}(X,Y)$ . For each $x\in X$ , there exists $\boldsymbol{\mathcal{F}}(f)(x)\in Y$ such that

f(x,y)\leq\|\boldsymbol{\mathcal{F}}(f)(x)=y\|_{Y}.

(2)

Any choice of $\boldsymbol{\mathcal{F}}(f)(x)$ for all $x\in X$ defines an element $\boldsymbol{\mathcal{F}}(f)\in\mathbf{SetoidF}_{A}(X,Y)$ such that $\boldsymbol{\gamma}(\boldsymbol{\mathcal{F}}(f))=f$ , and in fact this establishes a $\mathbf{SetoidF}_{A}$ isomorphism $\mathbf{SetoidR}_{A}(X,Y)\cong\mathbf{SetoidF}_{A}(X,Y)$ .

Every $A$ -set defines an $A$ -setoid as follows.

Definition 14.

Let $X\in V^{A}$ . Define $\|\mbox{$=$}\|_{X}:\mathrm{dom}(X)\times\mathrm{dom}(X)\rightarrow A$ by

\|x=y\|_{X}=\|x\in X\|\land\|y\in X\|\land\|x=y\|

(3)

Then $(\mathrm{dom}(X),\|\mbox{$=$}\|_{X})$ is an $A$ -setoid, which we write $\mathrm{Oid}(X)$ when we need to be unambiguous. When we speak of elements of $\mathrm{Oid}(X)$ , we mean elements of the underlying set of $\mathrm{Oid}(X)$ , i.e. elements of $\mathrm{dom}(X)$ , following the usual convention for sets with structure.

Definition 15.

Let $X\in V^{A}$ . For each $S\in V^{A}$ such that $\|S\subseteq X\|=1$ , then $e(S)$ , defined as follows, is a predicate on $\mathrm{Oid}(X)$ :

e(S)(x)=\|x\in S\|,

where $x\in\mathrm{Oid}(X)$ . In particular, this holds if $S\in\mathrm{dom}(\mathcal{P}^{A}(X))$ .

Definition 16.

The following defines $\mathrm{Oid}:\mathbf{Set}_{A}\rightarrow\mathbf{SetoidR}_{A}$ a functors, where $f:X\rightarrow Y$ is in $\mathbf{Set}_{A}$ :

\mathrm{Oid}(f)(x,y)=\|(x,y)^{A}\in f\|

This functors is full, faithful and essentially surjective, so $\mathbf{Set}_{A}\simeq\mathbf{SetoidR}_{A}$ .

Theorem 17.

For each $X\in V^{A}$ , $\mathrm{Oid}(\mathcal{P}^{A}(X))$ is complete. Moreover, if $\Phi$ is a formula of $\mathfrak{L}_{\mathbf{Set}}(V^{A})$ and $\|\exists S\in\mathcal{P}^{A}(X).\Phi(S,\ldots)\|=a\in A$ , then there exists $S\in\mathrm{Oid}(\mathcal{P}^{A}(X))$ such that $\|\Phi(S,\ldots)\|=a$ .

Corollary 18.

For each $X,Y\in V^{A}$ , $\mathrm{Oid}(\mathcal{P}^{A}(X\mathrel{\times_{\!A}}Y))$ and $\mathrm{Oid}(\{X\overset{A}{\rightarrow}Y\})$ are complete, and if we prove a relation or a function exists in the Boolean-valued sense, satisfying some formula $\Phi\in\mathfrak{L}_{\mathbf{Set}}(V^{A})$ , then there exists a corresponding element of $\mathrm{Oid}(\mathcal{P}^{A}(X\mathrel{\times_{\!A}}Y))$ or $\mathrm{Oid}(\{X\overset{A}{\rightarrow}Y\})$ satisfying $\Phi$ .

4 Models of Untyped Lambda-calculus in Boolean-valued sets

In this section we show how to model untyped $\lambda$ -calculus in $A$ -valued sets. We use the Engeler model [11] as the main example. We will repeatedly use Theorem 1 to prove statements in $V^{A}$ by proving them in set theory first. The reader who would prefer to use a topos formulation might prefer to use the categorical formulation of the Engeler model from [18].

4.1 Background on Domain Theory

A dcpo $(D,\leq)$ is a poset that is directed complete, i.e. such that every directed set has a supremum. Every complete lattice is a dcpo. The least element of a dcpo $(D,\leq)$ , if it exists, is called the bottom element and is written $\bot$ . In a dcpo $D$ , where $d,e\in D$ , we say that $d$ is way below $e$ , written $d\ll e$ , if for each directed set $(e_{i})_{i\in I}$ such that $e\leq\bigvee_{i\in I}e_{i}$ , there exists some $j\in I$ such that $d\leq e_{j}$ . The relation $\ll$ is transitive and antisymmetric, but in general is neither reflexive nor irreflexive. We write $\rotatebox[origin={c}]{-90.0}{$\twoheadrightarrow$}d=\{e\in D\mid e\ll d\}$ . A dcpo $D$ is called continuous if for all $d\in D$ , the set $\rotatebox[origin={c}]{-90.0}{$\twoheadrightarrow$}d$ is directed and $d=\bigvee\rotatebox[origin={c}]{-90.0}{$\twoheadrightarrow$}d$ . A continuous dcpo is called a domain. A complete lattice that is continuous as a dcpo is called a continuous lattice. A basis or base for a domain $D$ is a subset $B\subseteq D$ such that for all $d\in D$ , $\rotatebox[origin={c}]{-90.0}{$\twoheadrightarrow$}d\cap B$ is directed, and $d=\bigvee(\rotatebox[origin={c}]{-90.0}{$\twoheadrightarrow$}d\cap B)$ . It follows that if $D$ is continuous, then $D$ is a base for $D$ . If $D$ has a countable base, we say it is a countably-based domain. See [14] for more related concepts.

If $D$ and $E$ are dcpos, a function $f:D\rightarrow E$ is said to be Scott continuous if it is monotone and preserves directed suprema. We write ${[D\rightarrow E]}$ for the set of Scott-continuous maps $D\rightarrow E$ . This is a dcpo when given the pointwise ordering, and directed suprema are calculated pointwise. When we refer to this as a dcpo, we always use this structure. The Scott topology on a dcpo $D$ is the topology whose open sets are the sets $U\subseteq D$ such that $U$ is an up set and for all directed sets $(d_{i})_{i\in I}$ such that $\bigvee_{i\in I}d_{i}\in U$ there exists $i\in I$ such that $d_{i}\in U$ . If $D$ and $E$ are dcpos, a function $f:D\rightarrow E$ is Scott continuous iff it is a continuous map from $D$ to $E$ equipped with their respective Scott topologies.

Definition 19.

A reflexive dcpo is a triple $(D,\mathbf{fun},\mathbf{lam})$ , where $D$ is a dcpo with bottom⁸⁸8This is what is meant by a cpo in [4, Definition 1.2.1 (ii)]., and $\mathbf{fun}:D\rightarrow{[D\rightarrow D]}$ and $\mathbf{lam}:{[D\rightarrow D]}\rightarrow D$ are Scott-continuous maps making ${[D\rightarrow D]}$ a retract of $D$ , i.e. $\mathbf{fun}\circ\mathbf{lam}=\mathrm{id}_{{[D\rightarrow D]}}$ . A reflexive dcpo is extensional iff $\mathbf{fun}$ , or equivalently $\mathbf{lam}$ is an isomorphism, i.e. iff additionally $\mathbf{lam}\circ\mathbf{fun}=\mathrm{id}_{D}$ .

It is often convenient to formulate this notion using the uncurried form of $\mathbf{fun}$ , which is to say, we can equivalently define a reflexive dcpo to be a triple $(D,\cdot,\mathbf{lam})$ where $D$ is a dcpo with bottom, and $\cdot:D\times D\rightarrow D$ and $\mathbf{lam}:{[D\rightarrow D]}\rightarrow D$ are Scott-continuous maps such that for each $f\in{[D\rightarrow D]}$ and $d\in D$ we have $\mathbf{lam}(f)\cdot d=f(d)$ .

The language of untyped $\lambda$ -calculus can be interpreted in a reflexive dcpo as follows. Given a reflexive dcpo $(D,\cdot,\mathbf{lam})$ , and a set of variables $\mathrm{Var}$ , a valuation is a partial function $\rho:\mathrm{Var}\rightarrow D$ . We also choose a set of constants $\mathfrak{K}\subseteq D$ , which is allowed to be any subset, including $\emptyset$ and $D$ itself. We then define the language of $\lambda$ -calculus $\Lambda(D,\mathrm{Var},\mathfrak{K})$ as follows.

Definition 20.

The language $\Lambda(D,\mathrm{Var},\mathfrak{K})$ is defined inductively by the rules

We write $\Lambda(\mathrm{Var})$ for $\Lambda(D,\mathrm{Var},\emptyset)$ , since this does not depend on $D$ . The elements of $\Lambda(\mathrm{Var})$ are called pure $\lambda$ -terms. We write $\mathrm{fv}(M)$ for the set of free variables of $M$ , defined as usual.

We make the following observation about how the above definition is formulated in set theory⁹⁹9This is needed to make the proof of Proposition 22 and later results that deal with viewing the syntax of $\lambda$ -calculus from inside $V^{A}$ more comprehensible. .

Example 21.

There exist $\Delta_{0}$ formulas ${\Lambda(D,\mathrm{Var},\mathfrak{K})}\text{-}\mathrm{inductive}$ and ${\Lambda(\mathrm{Var})}\text{-}\mathrm{inductive}$ , such that the sets $\Lambda(D,\mathrm{Var},\mathfrak{K})$ and $\Lambda(\mathrm{Var})$ are respectively definable as the smallest sets satisfying their corresponding formula.

Indeed, to define ${\Lambda(\mathrm{Var})}\text{-}\mathrm{inductive}$ and ${\Lambda(D,\mathrm{Var},\mathfrak{K})}\text{-}\mathrm{inductive}$ , we need a way to represent the syntax of $\lambda$ -calculus. For example, we could take the ordinals $0$ to mean a variable, $1$ a $\lambda$ -abstraction, $2$ an application and $3$ a constant, so that a variable appears as $(0,x)$ for $x\in\mathrm{Var}$ , a $\lambda$ -abstraction as $(1,(x,M))$ where $x\in\mathrm{Var}$ and $M$ is a $\lambda$ -term, an application as $(2,(M,N))$ where $M, N$ are $\lambda$ -terms, and a constant as $(4,d)$ where $d\in\mathfrak{K}$ .

Then we can define:

	$\displaystyle{\Lambda(\mathrm{Var})}\text{-}\mathrm{inductive}(X)$	$\displaystyle=(\forall x\in\mathrm{Var}.\exists p\in X.p=(0,x))$
		$\displaystyle\land(\forall x\in\mathrm{Var}.\forall M\in X.\exists p\in X.p=(1% ,(x,M)))$
		$\displaystyle\land(\forall M\in X.\forall N\in X.\exists p\in X.p=(2,(M,N))).$

Strictly speaking this is not quite a $\Delta_{0}$ formula, but it is not difficult to see that the statements $p=(0,x)$ , $p=(1,(x,M))$ and $p=(2,(M,N))$ are expressible as $\Delta_{0}$ formulas (with the usual set-theoretic representations of ordered pairs). Then, we define:

{\Lambda(D,\mathrm{Var},\mathfrak{K})}\text{-}\mathrm{inductive}(X)={\Lambda(% \mathrm{Var})}\text{-}\mathrm{inductive}(X)\land(\forall d\in\mathfrak{K}.% \exists p\in X.p=(3,d))

Then, $\Lambda(\mathrm{Var})$ and $\Lambda(D,\mathrm{Var},\mathfrak{K})$ are the least sets satisfying their respective formulas.

Proposition 22.

Let $\mathrm{Var}$ be a set¹⁰¹⁰10Not Boolean-valued, just the usual kind of set.. For any complete Boolean algebra $A$ , there exists¹¹¹¹11By Theorem 1 (i) and (iii). $\Lambda(\widecheck{\mathrm{Var}})^{A}$ that satisfies the definition of $\Lambda(\widecheck{\mathrm{Var}})$ in the Boolean-valued sense, i.e.

\|{(\Lambda(\widecheck{\mathrm{Var}})}\text{-}\mathrm{inductive}(\Lambda(% \widecheck{\mathrm{Var}})^{A})\|=1

and for all $X\in V^{A}$ such that $\|{\Lambda(\widecheck{\mathrm{Var}})}\text{-}\mathrm{inductive}(X)\|=1$ , we have $\|\Lambda(\widecheck{\mathrm{Var}})^{A}\subseteq X\|=1$ .
Then $\|\widecheck{\Lambda(\mathrm{Var})}=\Lambda(\widecheck{\mathrm{Var}})^{A}\|=1$ .

The equational theory of $\lambda$ -calculus, called $\boldsymbol{\lambda}$ is described following [4]:

Definition 23.

Sentences of $\boldsymbol{\lambda}$ are of the form $M=N$ , where $M,N\in\Lambda(\mathrm{Var})$ . The theory $\boldsymbol{\lambda}$ is generated by the following rules, under modus ponens and $\alpha$ -conversion.

(i)

$(\lambda x.M)N=M[x:=N]$ , where $M[x:=N]$ is capture-avoiding substitution of $N$ for $x$ .
(ii)

$M=M$ .
(iii)

$M=N\Rightarrow N=M$ .
(iv)

$M=N,N=L\Rightarrow M=L$ .
(v)

$M=N\Rightarrow MZ=NZ$ .
(vi)

$M=N\Rightarrow ZM=ZN$ .
(vii)

$M=N\Rightarrow\lambda x.M=\lambda x.N$ .

We write $\boldsymbol{\lambda}\vdash M=N$ to say that the equation $M=N$ is derivable in the theory $\boldsymbol{\lambda}$ .

Example 24.

Here is a brief description of the set-theoretic formulation of $\boldsymbol{\lambda}$ . We can simply consider it to be a subset of $\Lambda(\mathrm{Var})\times\Lambda(\mathrm{Var})$ , and interpret $\boldsymbol{\lambda}\vdash M=N$ as $(M,N)\in\boldsymbol{\lambda}$ . We can define a formula ${\boldsymbol{\lambda}}\text{-}\mathrm{inductive}(S)$ , which we no longer require to be $\Delta_{0}$ , that encodes the rules of forming $\boldsymbol{\lambda}$ from Definition 23, and then $\boldsymbol{\lambda}$ can be characterized as the least set (with respect to $\subseteq$ ) such that ${\boldsymbol{\lambda}}\text{-}\mathrm{inductive}(\boldsymbol{\lambda})$ . This allows us to define $\boldsymbol{\lambda}^{A}$ in $V^{A}$ .

We can then prove that $\|\check{\boldsymbol{\lambda}}\subseteq\boldsymbol{\lambda}^{A}\|=1$ by induction on the structure of an element of $\boldsymbol{\lambda}$ .

Definition 25.

Following [4, Definition 5.4.2], we define the interpretation of $\lambda$ -terms from $M\in\Lambda(D,\mathrm{Var},\mathfrak{K})$ in $D$ , using a valuation $\rho$ such that $\mathrm{fv}(M)\subseteq\mathrm{dom}(\rho)$ , by

$\displaystyle\llbracket{x}\rrbracket_{\rho}$	$\displaystyle=\rho(x)$	$\displaystyle x\in\mathrm{Var}$
$\displaystyle\llbracket{k}\rrbracket_{\rho}$	$\displaystyle=k$	$\displaystyle k\in\mathfrak{K}$
$\displaystyle\llbracket{MN}\rrbracket_{\rho}$	$\displaystyle=\llbracket{M}\rrbracket_{\rho}\cdot\llbracket{N}\rrbracket_{\rho}$
$\displaystyle\llbracket{\lambda x.M}\rrbracket_{\rho}$	$\displaystyle=\mathbf{lam}(\bblambda d.\llbracket{M}\rrbracket_{\rho(x:=d)}),$

where $\bblambda$ is the “meta-lambda”, and $\rho(x:=d)$ is the partial function where $\mathrm{dom}(\rho(x:=d))=\mathrm{dom}(\rho)\cup\{x\}$ and

\rho(x:=d)(y)=\begin{cases}\rho(y)&\text{if }y\in\mathrm{dom}(\rho)\setminus\{% x\}\\ d&\text{if }y=x\end{cases}

This is proved to define a model of $\lambda$ -calculus in [4, Theorem 5.4.4], which is to say, that for all $M,N\in\Lambda(D,\mathrm{Var})$ , if $\boldsymbol{\lambda}\vdash M=N$ , then for all valuations $\rho$ , $\llbracket{M}\rrbracket_{\rho}=\llbracket{N}\rrbracket_{\rho}$ . For closed terms $M\in\Lambda(D,\mathrm{Var},\mathfrak{K})$ , we write $\llbracket{M}\rrbracket$ for $\llbracket{M}\rrbracket_{\emptyset}$ .

We now give the Boolean-valued version.

Theorem 26.

Let $D\in V^{A}$ such that the $A$ -setoid of $D$ is strict, total and complete, and let there be $\mathbf{lam}$ and $\cdot$ in $V^{A}$ such that $\|(D,\mathbf{lam},\cdot)\text{ is a reflexive dcpo}\|=1$ . And take $\mathrm{Var}$ to be a set of variables and $\mathfrak{K}\in V^{A}$ such that $\|\mathfrak{K}\subseteq D\|=1$ an $A$ -set of constants. Then for each $\rho$ that defines a partial function from $\widecheck{\mathrm{Var}}$ to $D$ , there are functions $\llbracket{{\mbox{-}}}\rrbracket^{A}_{\rho}\in\mathbf{SetoidF}_{A}(\Lambda(D,% \widecheck{\mathrm{Var}},\mathfrak{K})^{A},D)$ and $\llbracket{{\mbox{-}}}\rrbracket^{A}_{\rho}\in\mathbf{SetoidF}_{A}(\widecheck{% \Lambda(\mathrm{Var})},D)$ satisfying Definition 25 in the $A$ -valued sense.

Furthermore, for all $M,N\in\Lambda(\mathrm{Var})$ , if $\boldsymbol{\lambda}\vdash M=N$ , then for all $\rho$ we have $\llbracket{\check{M}}\rrbracket_{\rho}=\llbracket{\check{N}}\rrbracket_{\rho}$ .

4.2 The Engeler Model

We start with a basic result about the power set.

Proposition 27.

For any set $X$ , the power set $\mathcal{P}(X)$ , when ordered using the subset relation $\subseteq$ , is a dcpo (in fact, a complete lattice). If $S,T\in\mathcal{P}(X)$ , $S\ll T$ iff $S$ is finite and $S\subseteq T$ . The set of finite sets $\mathcal{P}_{\mathrm{fin}}(X)$ is a base, and if $X$ is countable, it is a countable base.

We can then apply this in $V^{A}$ as follows.

Proposition 28.

For any $X\in V^{A}$ , the $A$ -set $\mathcal{P}^{A}(X)$ , ordered with the subset relation, is a continuous lattice with base $\mathcal{P}^{A}_{\mathrm{fin}}(X)$ , interpreted in the $A$ -valued sense. As an $A$ -setoid, $\mathcal{P}^{A}(X)$ is complete and total. If $X=\check{Y}$ , then $\widecheck{\mathcal{P}_{\mathrm{fin}}(Y)}$ is a base, and $\mathcal{P}^{A}(\check{Y})$ is strict.

We define the Engeler model [11, 4], an adaptation of the Scott-Plotkin graph model that uses set-theoretic operations instead of Gödel numbering, as follows¹²¹²12What we really need of $E$ is for it to be countable, non-empty, and an algebra of the functor $\mathcal{P}_{\mathrm{fin}}\times\mathrm{Id}$ , such that the structure map $\mathcal{P}_{\mathrm{fin}}(E)\times E\rightarrow E$ is injective, which implies $E$ must be infinite. We cannot use the initial algebra of $\mathcal{P}_{\mathrm{fin}}\times\mathrm{Id}$ , because it is $\emptyset$ ..

Let $E_{0}=\{\emptyset\}$ . We define $E_{n+1}=(\mathcal{P}_{\mathrm{fin}}(E_{n})\times E_{n})\uplus E_{n}$ and $E=\bigcup_{n=0}^{\infty}E_{n}$ . Then we have a map $({\mbox{-}},{\mbox{-}}):\mathcal{P}_{\mathrm{fin}}(E)\times E\rightarrow E$ defined by pairing, since for each $S\in\mathcal{P}_{\mathrm{fin}}(E)$ we have $S\subseteq E_{n}$ for some $n\in\mathbb{N}$ . For reasons that will become clear later, we express the existence of the Engeler model in the following manner.

Proposition 29.

Let $E$ be a set equipped with an injective mapping $({\mbox{-}},{\mbox{-}}):\mathcal{P}_{\mathrm{fin}}(E)\times E\rightarrow E$ . Define $\mathbf{lam}:{[\mathcal{P}(E)\rightarrow\mathcal{P}(E)]}\rightarrow\mathcal{P}% (E)$ and ${\mbox{-}}\cdot{\mbox{-}}:\mathcal{P}(E)\times\mathcal{P}(E)\rightarrow% \mathcal{P}(E)$ by

	$\displaystyle\mathbf{lam}(f)$	$\displaystyle=\{(K,q)\mid q\in f(K)\}=\{x\in E\mid\exists K\in\mathcal{P}_{% \mathrm{fin}}(E),q\in f(K).x=(K,q)\}$
	$\displaystyle F\cdot X$	$\displaystyle=\{q\in E\mid\exists K\in\mathcal{P}_{\mathrm{fin}}(E).K\subseteq X% \text{ and }(K,q)\in F\},$

where $f\in{[\mathcal{P}(E)\rightarrow\mathcal{P}(E)]}$ , and $F,X\in\mathcal{P}(E)$ . Then $(\mathcal{P}(E),\cdot,\mathbf{lam})$ is a reflexive dcpo.

We can now build the Engeler model in $V^{A}$ , as follows.

Theorem 30.

Let $E$ be the set defined before Proposition 29. $(\mathcal{P}^{A}(\check{E}),\|\subseteq\|,\cdot,\mathbf{lam})$ is an $A$ -valued reflexive dcpo, where $\cdot$ and $\mathbf{lam}$ are defined by the $A$ -valued interpretation of the definitions given in Proposition 29.

By combining Theorem 30 with Proposition 28 and Theorem 26, we obtain a function $\llbracket{{\mbox{-}}}\rrbracket^{A}$ that interprets $\lambda$ -terms in a manner that respects provable equations between them.

The following lemma shows that if we only use pure $\lambda$ -terms we do not get anything new by using $\mathcal{P}^{A}(\check{E})$ instead of $\mathcal{P}(E)$ as a model of $\lambda$ -calculus.

Lemma 31.

Let $M\in\Lambda(\mathrm{Var})$ and $\rho$ a valuation such that $\mathrm{fv}(M)\subseteq\mathrm{dom}(\rho)$ , and consider $\llbracket{{\mbox{-}}}\rrbracket^{A}$ and $\llbracket{{\mbox{-}}}\rrbracket$ as defined for $\mathcal{P}^{A}(\check{E})$ and $\mathcal{P}(E)$ respectively. Then $\|\llbracket{\check{M}}\rrbracket^{A}_{\check{\rho}}=\widecheck{\llbracket{M}% \rrbracket_{\rho}}\|=1.$
In particular, since $\emptyset=\check{\emptyset}$ , if $M$ is closed we have $\|\llbracket{\check{M}}\rrbracket^{A}=\widecheck{\llbracket{M}\rrbracket}\|=1.$

4.3 Injective Spaces and Oracles

We can encode the Booleans $\{\bot,\top\}$ , and natural numbers $\mathbb{N}$ in $\lambda$ -calculus in several ways, e.g. with the Church numerals. The details of the encoding do not matter, only the following.

Definition 32.

Let $(D,\mathbf{fun},\mathbf{lam})$ be a reflexive dcpo, and let $\bot,\top$ be closed $\lambda$ -terms and $(c_{n})_{n\in\mathbb{N}}$ a family of closed $\lambda$ -terms. We say $(D,\mathbf{fun},\mathbf{lam},\bot,\top,(c_{n})_{n\in\mathbb{N}})$ is a reflexive dcpo with numerals if

(i)

$\llbracket{\bot}\rrbracket$ and $\llbracket{\top}\rrbracket$ are distinct elements of $D$ .
(ii)

There exists a closed $\lambda$ -term $\mathbf{if}$ such that for all $\lambda$ -terms $M, N$ , $\boldsymbol{\lambda}\vdash\mathbf{if}\top MN=M$ and $\boldsymbol{\lambda}\vdash\mathbf{if}\bot MN=N$ .
(iii)

There exist closed $\lambda$ -terms $\mathbf{succ}$ and $\mathbf{pred}$ representing the successor and predecessor operations on $(c_{n})_{n\in\mathbb{N}}$ , i.e. for all $n\in\mathbb{N}$ , $\boldsymbol{\lambda}\vdash\mathbf{succ}c_{n}=c_{n+1}$ and $\boldsymbol{\lambda}\vdash\mathbf{pred}c_{n+1}=c_{n}$ and $\boldsymbol{\lambda}\vdash\mathbf{pred}c_{0}=c_{0}$ .
(iv)

There exists a closed $\lambda$ -term $\mathbf{0}^{?}$ such that $\boldsymbol{\lambda}\vdash\mathbf{0}^{?}c_{0}=\top$ and for all $n>0$ , $\boldsymbol{\lambda}\vdash\mathbf{0}^{?}c_{n}=\bot$ .

Proposition 33.

The Church Booleans and Church numerals make the Engeler model into a reflexive continuous lattice with numerals.

Corollary 34.

The Engeler model in $V^{A}$ , as described in Theorem 30, is a reflexive continuous lattice with numerals, when given ( $\check{{\mbox{-}}}$ of) the Church Booleans and Church numerals, with this whole statement being interpreted in $V^{A}$ .

In the following, for a set $A\subseteq\mathbb{N}$ , we write $\chi_{A}$ for the function $A\rightarrow 2$ such that $\chi_{A}(x)=\begin{cases}1&\text{if }x\in A\\ 0&\text{if }x\not\in A\end{cases},$
while if $\{\bot,\top\}$ are part of the structure of a reflexive dcpo with numerals $D$ , we write $\chi_{A}^{D}$ for the function $\mathbb{N}\rightarrow\{\llbracket{\bot}\rrbracket,\llbracket{\top}\rrbracket\}$ such that:
$\chi_{A}^{D}(x)=\begin{cases}\llbracket{\top}\rrbracket&\text{if }x\in A\\ \llbracket{\bot}\rrbracket&\text{if }x\not\in A\end{cases}.$

Every dcpo is a $T_{0}$ topological space when equipped with its Scott topology [14]. And a $T_{0}$ topological space $X$ is injective for subspace embeddings in the category of $T_{0}$ -spaces iff $X$ is a continuous lattice equipped with the Scott topology [27]. This has useful consequences for representations of the natural numbers in reflexive dcpos that are continuous lattices.

Lemma 35.

Let $(D,\mathbf{fun},\mathbf{lam},\bot,\top,(c_{n})_{n\in\mathbb{N}})$ be a reflexive dcpo with numerals. Then:

(i)

$\{\llbracket{\bot}\rrbracket,\llbracket{\top}\rrbracket\}$ and $\{\llbracket{c_{n}}\rrbracket\}_{n\in\mathbb{N}}$ are discrete in the Scott topology of $D$ , and also are distinct elements, i.e. $\llbracket{c_{m}}\rrbracket=\llbracket{c_{n}}\rrbracket$ implies $m=n$ .

If $D$ is additionally a continuous lattice, then:

(ii)

For every set $A\subseteq\mathbb{N}$ , there is a $d_{g}\in D$ such that for all $n\in\mathbb{N}$ , $d_{g}\cdot\llbracket{c_{n}}\rrbracket=\chi^{D}_{A}(n)$ .

We can now define a pre-order on sets of integers to be used in the example (Theorem 43). Readers familiar with recursion theory will see that it is the $\lambda$ -calculus version of comparability of many-one degrees [29, Definition 4.8 (i), (iii)].

Proposition 36.

Let $D$ be a reflexive continuous lattice with numerals. The following are equivalent for $S_{1},S_{2}\subseteq\mathbb{N}$ , in which case we write $S_{1}\leq_{m}S_{2}$ :

(i)

There exists a closed $\lambda$ -term $M\in\Lambda(D,\mathrm{Var})$ such that for all $n\in\mathbb{N}$ , there exists $m\in\mathbb{N}$ such that $\boldsymbol{\lambda}\vdash Mc_{n}=c_{m}$ , and there exist $d_{S_{1}},d_{S_{2}}\in D$ such that for all $n\in\mathbb{N}$ , $\llbracket{d_{S_{1}}c_{n}}\rrbracket=\chi_{S_{1}}^{D}(n)$ , $\llbracket{d_{S_{2}}c_{n}}\rrbracket=\chi_{S_{2}}^{D}(n)$ and $\llbracket{d_{S_{2}}(Mc_{n})}\rrbracket=\llbracket{d_{S_{1}}c_{n}}\rrbracket$ .
(ii)

There exists a closed $\lambda$ -term $M\in\Lambda(D,\mathrm{Var})$ such that for all $n\in\mathbb{N}$ , there exists $m\in\mathbb{N}$ such that $\boldsymbol{\lambda}\vdash Mc_{n}=c_{m}$ , and for all $d_{S_{1}},d_{S_{2}}\in D$ such that for all $n\in\mathbb{N}$ , $\llbracket{d_{S_{1}}c_{n}}\rrbracket=\chi_{S_{1}}^{D}(n)$ and $\llbracket{d_{S_{2}}c_{n}}\rrbracket=\chi_{S_{2}}^{D}(n)$ , we have that for all $n\in\mathbb{N}$ , $\llbracket{d_{S_{2}}(Mc_{n})}\rrbracket=\llbracket{d_{S_{1}}c_{n}}\rrbracket$ .

5 Random Variables

In this section we relate the Boolean-valued Engeler model in $V^{A}$ from Corollary 34 to the random-variable-based Boolean-valued models of $\lambda$ -calculus from [3], and give the example application (Theorem 43).

We start with some terminology. A negligibility space $(X,\Sigma,\mathcal{N})$ is a measurable space $(X,\Sigma)$ equipped with a $\sigma$ -ideal $\mathcal{N}$ such that $\Sigma/\mathcal{N}$ is a complete Boolean algebra, not just $\sigma$ -complete. We use $A(X)$ to denote $\Sigma/\mathcal{N}$ , as it is the complete Boolean algebra associated to $X$ or simply the algebra associated to $X$ .

For a probability space $(X,\Sigma,\mu)$ , the null ideal $\mathcal{N}(\mu)$ is the $\sigma$ -ideal of sets $N\in\Sigma$ with $\mu(N)=0$ , and $\Sigma/\mathcal{N}(\mu)$ is a complete Boolean algebra [13, 322B,322C], so $(X,\Sigma,\mathcal{N}(\mu))$ is a negligibility space, and $\Sigma/\mathcal{N}(\mu)$ is known as the measure algebra of $(X,\Sigma,\mu)$ .

Let $Y$ be a countable set. For each $y\in Y$ , let $B_{y}=\{S\subseteq Y\mid y\in S\}$ , which form a subbasis of open sets for the positive topology¹³¹³13The positive topology equals the Scott topology. on $\mathcal{P}(Y)$ . All notions of measurability for $\mathcal{P}(Y)$ will be with respect to the Borel $\sigma$ -algebra defined by this topology, and since this is a second countable topology, $(B_{y})_{y\in Y}$ is also a countable generating set for this $\sigma$ -algebra.

Definition 37.

Let $X=(X,\Sigma_{X})$ be a measurable space and $Y$ a countable set. We define $\mathcal{L}^{0}(X;\mathcal{P}(Y))$ to be the set of measurable functions $X\rightarrow\mathcal{P}(Y)$ , using the Borel $\sigma$ -algebra of the Scott topology of $\mathcal{P}(Y)$ . We define a $\Sigma_{X}$ -valued order as follows:

\|a\leq b\|_{\mathcal{L}^{0}}=\{x\in X\mid a(x)\subseteq b(x)\}.

The corresponding notion of equality is

\|a=b\|_{\mathcal{L}^{0}}=\{x\in X\mid a(x)=b(x)\}.

Lemma 38.

If $X=(X,\Sigma_{X},\mathcal{N}_{X})$ is a negligibility space, define $L^{0}(X;\mathcal{P}(Y))$ to be $\mathcal{L}^{0}(X;\mathcal{P}(Y))$ modulo the relation $\sim$ defined by: $a\sim b\text{ iff }X\setminus\|a=b\|_{\mathcal{L}^{0}}\in\mathcal{N}_{X},$ which is the usual “almost everywhere” equivalence. Then $\|\mbox{$\leq$}\|_{L^{0}}$ and $\|\mbox{$=$}\|_{L^{0}}$ , defined by composing the corresponding notions for $\mathcal{L}^{0}(X;\mathcal{P}(Y))$ with $[{\mbox{-}}]:\Sigma\rightarrow A(X)$ , are well-defined and make $L^{0}(X;\mathcal{P}(Y))$ into an $A(X)$ -poset.

We define $G_{X}:L^{0}(X;\mathcal{P}(Y))\rightarrow\mathcal{P}^{A(X)}(\check{Y})$ as follows, where $a\in\mathcal{L}^{0}(X;\mathcal{P}(Y))$ and $y\in Y$ :

G_{X}([a])(\check{y})=[a^{-1}(B_{y})]=[\{x\in X\mid y\in a(x)\}]

(4)

The measurability of $a$ guarantees that $a^{-1}(B_{y})\in\Sigma$ .

Proposition 39.

For any negligibility space $(X,\Sigma,\mathcal{N})$ and any countable set $Y$ , the map $G_{X}$ is a strict isomorphism of $A(X)$ -posets $L^{0}(X;\mathcal{P}(Y))\rightarrow\mathcal{P}^{A(X)}(\check{Y})$ .

Since $\mathcal{P}(E)$ is a reflexive dcpo and has a binary operation $\cdot$ for application, for any measurable space $X$ we can extend this pointwise to $\mathcal{L}^{0}(X;\mathcal{P}(E))$ by defining for $a,b\in\mathcal{L}^{0}(X;\mathcal{P}(E))$ and $x\in X$ : $(a\cdot b)(x)=a(x)\cdot b(x).$
For a negligibility space $X$ we can then extend this to $L^{0}(X;\mathcal{P}(E))$ by defining $[a]\cdot[b]=[a\cdot b].$

Proposition 40.

Let $(X,\Sigma,\mathcal{N})$ be a negligibility space. Then the above definition of $\cdot:L^{0}(X;\mathcal{P}(E))\times L^{0}(X;\mathcal{P}(E))\rightarrow L^{0}(X% ;\mathcal{P}(E))$ is well-defined, and $G_{X}:L^{0}(X;\mathcal{P}(E))\rightarrow\mathcal{P}^{A(X)}(\check{E})$ is an “application homomorphism”, i.e. for all $[a],[b]\in L^{0}(X;\mathcal{P}(E))$ ,

G_{X}([a]\cdot[b])=G_{X}([a])\cdot G_{X}([b]).

We now introduce the following notation. If $S\subseteq E$ , define $K_{S}\in\mathcal{L}^{0}(X;\mathcal{P}(E))$ to be the function taking the constant value $S$ . This relates to $\check{{\mbox{-}}}$ in the following way.

Lemma 41.

Let $Y$ be an arbitrary countable set. For all $S\subseteq Y$ we have

\|G_{X}([K_{S}])=\check{S}\|=1

Recall that a subbase of clopens for the product topology of $2^{\omega}$ is given by the sets $(C_{n,b})_{n\in\omega,b\in 2}$ , where $C_{n,b}=\{f\in 2^{\omega}\mid f(n)=b\}.$
These sets also generate the Borel $\sigma$ -algebra of $2^{\omega}$ .

In the following, we will also have to consider the (isomorphic) product space $2^{\omega}\times 2^{\omega}$ , but for which we will need to describe the subsets in more detail. So for $i\in\{1,2\}$ , $n\in\omega$ and $b\in 2$ we write $D_{i,n,b}=\{(f_{1},f_{2})\in 2^{\omega}\times 2^{\omega}\mid f_{i}(n)=b\}.$
Then for all $i\in\{1,2\}$ , $n\in\omega$ and $b\in 2$ we have $D_{i,n,b}=\pi_{i}^{-1}(C_{n,b})$ .

Let $X=2^{\omega}\times 2^{\omega}$ equipped with its Borel $\sigma$ -algebra as a measurable space. We define $\mu_{X}$ to be the usual independent fair coin measure, which is to say, it is the unique measure such that for all finitely-supported partial functions $f_{1},f_{2}:\omega\rightarrow 2$

\mu\left(\bigcap_{n\in\mathrm{dom}(f_{1})}D_{1,n,f_{1}(n)}\cap\bigcap_{n\in% \mathrm{dom}(f_{2})}D_{2,n,f_{2}(n)}\right)=2^{-(|\mathrm{dom}(f_{1})|+|% \mathrm{dom}(f_{2})|)}.

We take the null ideal of this measure as the negligible sets of $X$ . Then $\pi_{1},\pi_{2}$ are random variables in $\mathcal{L}^{0}(X;2^{\omega})$ . They define $S_{1},S_{2}\in\mathcal{P}^{A(X)}(\check{\omega})$ as follows, taking $i\in\{1,2\}$ :

S_{i}(\check{n})=[\pi_{i}^{-1}(C_{n,1})]=[D_{i,n,1}].

(5)

We remind the reader at this point that $\|\check{n}\in S_{i}\|=S_{i}(\check{n})$ because of the way Boolean-valued equality behaves for elements of $\check{\omega}$ .

Proposition 42.

For all $f:\omega\rightarrow\omega$ , neither $S_{1}$ nor $S_{2}$ is the preimage of a finite $A(X)$ -subset of $\check{\omega}$ , i.e. $\|\exists K\in\mathcal{P}^{A(X)}_{\mathrm{fin}}(\check{\omega}).\forall n\in% \check{\omega}.n\in S_{1}\Leftrightarrow\check{f}(n)\in K\|=0$ , and likewise for $S_{2}$ .
Moreover, $\|S_{1}=\check{f}^{-1}(S_{2})\|=0$ and $\|S_{2}=\check{f}^{-1}(S_{1})\|=0$ , i.e. these sets cannot be mapped to each other by any classical function.

Theorem 43.

There exist sets $T_{1},T_{2}\subseteq\mathbb{N}$ such that neither can be mapped to the other by a $\lambda$ -definable function, i.e. we neither have $T_{1}\leq_{m}T_{2}$ nor $T_{2}\leq_{m}T_{1}$ (recall Proposition 36).

Proof.

We start by doing Boolean-valued reasoning about $S_{1}$ and $S_{2}$ , taking $A=A(2^{\omega}\times 2^{\omega})$ , and use the fact that the Engeler model $\mathcal{P}^{A}(\check{E})$ is ( $A$ -valuedly) a reflexive continuous lattice with numerals (Corollary 34) and Proposition 36.

First, by Theorem 1 applied to Lemma 35 (ii), there exist $d_{1},d_{2}\in\mathcal{P}^{A}(\check{E})$ such that for all $n\in\omega$ and $i\in\{1,2\}$ we have $\|d_{i}\cdot\check{c_{n}}=\check{\top}\|=\|\check{n}\in S_{i}\|$ and $\|d_{i}\cdot\check{c_{n}}=\check{\bot}\|=\lnot\|\check{n}\in S_{i}\|$ .

Suppose $M\in\Lambda(\mathrm{Var})$ such that for all $n\in\omega$ , there exists $m\in\omega$ such that $\boldsymbol{\lambda}\vdash Mc_{n}=c_{m}$ . In particular, there exists some function $f:\omega\rightarrow\omega$ such that for all $m\in\omega$ , $\boldsymbol{\lambda}\vdash Mc_{n}=c_{f(n)}$ .

Now we consider $\llbracket{d_{2}(\check{M}\check{c}_{n})}\rrbracket^{A}$ and $\llbracket{d_{1}\check{c}_{n}}\rrbracket^{A}$ . In the following, for ease of notation, we write an equals sign to mean the corresponding $A$ -valued equality being equal to $1$ :
$\llbracket{d_{2}(\widecheck{Mc_{n}})}\rrbracket^{A}=d_{2}\cdot\llbracket{% \widecheck{Mc_{n}}}\rrbracket^{A}=d_{2}\cdot\llbracket{\widecheck{c_{f(n)}}}% \rrbracket^{A}$ by Theorem 26. Therefore,
$\|\llbracket{d_{2}(\widecheck{Mc_{n}})}\rrbracket^{A}=\llbracket{\check{\top}}% \rrbracket^{A}\|=\|d_{2}\cdot\llbracket{\widecheck{c_{f(n)}}}\rrbracket^{A}=% \llbracket{\check{\top}}\rrbracket^{A}\|=\|\widecheck{f(n)}\in S_{2}\|,$ and the corresponding negative statement for $\bot$ . Likewise, $\|\llbracket{d_{1}\check{c}_{n}}\rrbracket^{A}=\llbracket{\check{\top}}% \rrbracket\|=\|\check{n}\in S_{1}\|,$ and the corresponding statement for $\bot$ . So all together, $\|d_{2}\cdot\llbracket{\widecheck{Mc_{n}}}\rrbracket^{A}=d_{1}\cdot\llbracket{% \check{c}_{n}}\rrbracket^{A}\|=\|\widecheck{f(n)}\in S_{2}\Leftrightarrow% \check{n}\in S_{1}\|.$
It is proved in Proposition 42 that $\|\forall n\in\check{\omega}.\check{f}(n)\in S_{2}\Leftrightarrow n\in S_{1}\|=0$ , so we can conclude that $\bigwedge_{n\in\omega}\|d_{2}\cdot\llbracket{\widecheck{Mc_{n}}}\rrbracket^{A}% =d_{1}\cdot\llbracket{\check{c}_{n}}\rrbracket^{A}\|=0$ for all $M\in\Lambda(\widecheck{\mathrm{Var}})$ that map numerals to numerals.

Let $a_{1},a_{2}\in\mathcal{L}^{0}(X;\mathcal{P}(E))$ s.t. for $i\in\{1,2\}$ we have $[a_{i}]=G_{X}^{-1}(d_{i})$ . Then, using Proposition 39, Proposition 40, Lemma 31 and Lemma 41, we get:
$0=\bigwedge_{n\in\omega}\|G_{X}^{-1}(d_{2}\cdot\llbracket{\widecheck{Mc_{n}}}% \rrbracket^{A})=G_{X}^{-1}(d_{1}\cdot\llbracket{\check{c}_{n}}\rrbracket^{A})% \|_{L^{0}}$
$=\bigwedge_{n\in\omega}\|G_{X}^{-1}(d_{2})\cdot G_{X}^{-1}(\llbracket{% \widecheck{Mc_{n}}}\rrbracket^{A})=G_{X}^{-1}(d_{1})\cdot G_{X}^{-1}(% \llbracket{\check{c}_{n}}\rrbracket^{A})\|_{L^{0}}$
$=\bigwedge_{n\in\omega}\|[a_{2}]\cdot G_{X}^{-1}(\widecheck{\llbracket{Mc_{n}}% \rrbracket})=[a_{1}]\cdot G_{X}^{-1}(\widecheck{\llbracket{c_{n}}\rrbracket})% \|_{L^{0}}=\bigwedge_{n\in\omega}\|[a_{2}]\cdot[K_{\llbracket{Mc_{n}}% \rrbracket}]=[a_{1}]\cdot[K_{\llbracket{c_{n}}\rrbracket}]\|_{L^{0}}$
$=\left[\bigcap_{n\in\omega}\{x\in X\mid a_{2}(x)\cdot K_{\llbracket{Mc_{n}}% \rrbracket}(x)=a_{1}(x)\cdot K_{\llbracket{c_{n}}\rrbracket}(x)\}\right]$
$=[\{x\in X\mid\forall n\in\omega.a_{2}(x)\cdot\llbracket{Mc_{n}}\rrbracket=a_{% 1}(x)\cdot\llbracket{c_{n}}\rrbracket\}]$ ,
so the set inside the square brackets has measure zero.

Since the set of $M\in\Lambda(\mathrm{Var})$ that map numerals to numerals is countable (because $\mathrm{Var}$ is countable), the set of $x\in X$ such that for all $M\in\Lambda(\mathrm{Var})$ mapping numerals to numerals we have $a_{2}(x)\cdot\llbracket{Mc_{n}}\rrbracket\neq a_{1}(x)\cdot\llbracket{c_{n}}\rrbracket$ has measure $1$ .

For all $i\in\{1,2\}$ , we have, by the definition of $d_{i}$ , for all $n\in\omega$ the statement $\|d_{i}\cdot\llbracket{c_{n}}\rrbracket^{A}=\llbracket{\top}\rrbracket^{A}\|% \lor\|d_{i}\cdot\llbracket{c_{n}}\rrbracket^{A}=\llbracket{\bot}\rrbracket^{A}% \|=1$ . By a similar argument to that used above, this means that the set of $x\in X$ such that $a_{i}(x)\cdot\llbracket{c_{n}}\rrbracket\in\{\llbracket{\top}\rrbracket,% \llbracket{\bot}\rrbracket\}$ has measure $1$ , and by the countability of $\omega$ the set where this is true for both $i\in\{1,2\}$ and all $n\in\omega$ is also of measure $1$ .

Therefore the intersection of the sets defined in the previous two paragraphs has measure $1$ , and so is non-empty and so there exists a point $x$ in it. We can then define $T_{i}=\{n\in\omega\mid a_{i}(x)\cdot\llbracket{c_{n}}\rrbracket=\llbracket{% \top}\rrbracket\}$ , and we have proved, by Proposition 36, that $T_{1}\not\leq_{m}T_{2}$ . $\hfill\blacktriangleleft$

We could not have done this proof by using the “fact” that $L^{0}(X;\mathcal{P}(E))$ is a continuous dcpo, because this is not true, as stated in our last proposition.

Proposition 44.

Let $X=(X,\Sigma,\mathcal{N})$ be a negligibility space such that $A(X)$ is not atomic, and let $Y$ be a non-empty countable set. Then $L^{0}(X;\mathcal{P}(Y))$ is not a continuous dcpo.

6 Conclusions

We have developed domain theory in a Boolean-valued universe of sets. Using the measure algebra as the Boolean algebra we obtained a domain of random variables which can be see to be a reflexive domain in the internal language of the Boolean-valued set theory. We have focused on the pure $\lambda$ -calculus here but it should be straightforward to extend this to a $\lambda$ -calculus with probabilistic choice as an explicit primitive.

There are a number of directions for future work. First, one can use this construction to give semantics to a $\lambda$ -calculus extended with probabilistic choice as was done in [3]. In this model it will be interesting to see which equations involving the interplay of choice and the standard $\lambda$ -calculus constructions are valid. One could then relate it to an operational semantics as, for example, in [8] but one would need a Boolean-valued notion of operational semantics. More interestingly one could define conditioning as a primitive and explore its semantics. A second line of research is the notion of approximation. A notion of “approximate equality” has been developed recently [22]; the connection to the notion of equality used in the present paper is unclear but there is a similarity in that in both cases equality may only hold partially.

References

[1] Nathanael L. Ackerman, Cameron E. Freer, and Daniel M. Roy. Noncomputable conditional distributions. In Logic in Computer Science (LICS), 2011 26th Annual IEEE Symposium on, pages 107–116. IEEE, 2011. doi:10.1109/LICS.2011.49.
[2] Nathanael L. Ackerman, Cameron E. Freer, and Daniel M. Roy. On the computability of conditional probability. J. ACM, 66(3):23:1–23:40, 2019. doi:10.1145/3321699.
[3] Giorgio Bacci, Robert Furber, Dexter Kozen, Radu Mardare, Prakash Panangaden, and Dana Scott. Boolean-valued semantics for the stochastic $\lambda$ -calculus. In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, pages 669–678. ACM, 2018. doi:10.1145/3209108.3209175.
[4] Henk P. Barendregt. The Lambda Calculus: Its Syntax and Semantics. North-Holland, Amsterdam, 1984.
[5] John L. Bell. Set Theory: Boolean-Valued Models and Independence Proofs, volume 47 of Oxford Logic Guides. Oxford University Press, third edition, 2005.
[6] Johannes Borgström, Ugo Dal Lago, Andrew D. Gordon, and Marcin Szymczak. A lambda-calculus foundation for universal probabilistic programming. In Jacques Garrigue, Gabriele Keller, and Eijiro Sumii, editors, Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, ICFP 2016, Nara, Japan, September 18-22, 2016, pages 33–46. ACM, 2016. doi:10.1145/2951913.2951942.
[7] Fredrik Dahlqvist and Dexter Kozen. Semantics of higher-order probabilistic programs with conditioning. Proc. ACM Program. Lang., 4(POPL):57:1–57:29, 2020. doi:10.1145/3371125.
[8] Pedro H. Azevedo de Amorim, Dexter Kozen, Radu Mardare, Prakash Panangaden, and Michael Roberts. Universal semantics for the stochastic $\lambda$ -calculus. In Proceedings of the ACM-IEEE Symposium on Logic in Computer Science, 2021. arXiv preprint:2011.13171.
[9] Thomas Ehrhard, Michele Pagani, and Christine Tasson. Measurable cones and stable, measurable functions: a model for probabilistic higher-order programming. Proceedings of the ACM Symposium on Principles of Programming Languages, 2(POPL):1–28, 2017. doi:10.1145/3158147.
[10] Thomas Ehrhard, Christine Tasson, and Michele Pagani. Probabilistic coherence spaces are fully abstract for probabilistic pcf. In Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 309–320, 2014. doi:10.1145/2535838.2535865.
[11] Erwin Engeler. Algebras and Combinators. Algebra Universalis, 13(1):389–392, December 1981. doi:10.1007/BF02483849.
[12] Michael P. Fourman and Dana S. Scott. Sheaves and Logic. In Michael Fourman, Christopher Mulvey, and Dana Scott, editors, Applications of Sheaves: Proceedings of the Research Symposium on Applications of Sheaf Theory to Logic, Algebra, and Analysis, Durham, July 9–21, 1977, pages 302–401. Springer Berlin Heidelberg, 1979. doi:10.1007/BFb0061824.
[13] David H. Fremlin. Measure Theory, Volume 3. https://www.essex.ac.uk/maths/people/fremlin/mt.htm, 2002.
[14] Gerhard Gierz, Karl H. Hofmann, Klaus Keimel, Jimmie D. Lawson, Michael W. Mislove, and Dana S. Scott. Continuous Lattices and Domains, volume 93 of Encyclopedia of Mathematics and its Applications. Cambridge University Press, 2003.
[15] Robert Goldblatt. Topoi: The Categorial Analysis of Logic. Dover, 2006.
[16] Noah Goodman, Vikash Mansingkha, Daniel Roy, Keith Bonawitz, and Joshua Tenenbaum. Church: a language for generative models. In Proceedings of the 24th Conference on Uncertainty in Artificial Intelligence, pages 220–229, 2008.
[17] Chris Heunen, Ohad Kammar, Sam Staton, and Hongseok Yang. A convenient category for higher-order probability theory. In Proceedings of the Thirty-second Annual ACM-IEEE Symposium on Logic in Computer Science, pages 1–12, 2017. doi:10.1109/LICS.2017.8005137.
[18] Martin Hyland, Misao Nagayama, John Power, and Giuseppe Rosolini. A Category Theoretic Formulation for Engeler-style Models of the Untyped $\lambda$ -Calculus. Electronic Notes in Theoretical Computer Science, 161:43–57, 2006. Proceedings of the Third Irish Conference on the Mathematical Foundations of Computer Science and Information Technology (MFCSIT 2004). doi:10.1016/j.entcs.2006.04.024.
[19] Thomas J. Jech. Set Theory. Springer, 3rd Millennium edition, 2003.
[20] Stephen C. Kleene and Emil L. Post. The Upper Semi-Lattice of Degrees of Recursive Unsolvability. Annals of Mathematics, 59(3):379–407, 1954. doi:10.2307/1969708.
[21] Anatoly G. Kusraev and Semën S. Kutateladze. Boolean Valued Analysis, volume 494 of Mathematics and Its Applications. Springer, 1999. doi:10.1007/978-94-011-4443-8.
[22] Radu Mardare, Prakash Panangaden, and Gordon Plotkin. Quantitative algebraic reasoning. In Proceedings of the 31st Annual ACM-IEEE Symposium on Logic in Computer Science, pages 700–709, 2016. doi:10.1145/2933575.2934518.
[23] Gordon P. Monro. A Category-theoretic Approach to Boolean-valued Models of Set Theory. Journal of Pure and Applied Algebra, 42(3):245–274, 1986. doi:10.1016/0022-4049(86)90010-1.
[24] Gordon P. Monro. Quasitopoi, Logic and Heyting-valued Models. Journal of Pure and Applied Algebra, 42(2):141–164, 1986. doi:10.1016/0022-4049(86)90077-0.
[25] Dan Roy. Computability, inference and modeling in probabilistic programming. PhD thesis, MIT, June 2011.
[26] Dana Scott. A proof of the independence of the continuum hypothesis. Mathematical Systems Theory, 1(2):89–111, 1967. doi:10.1007/BF01705520.
[27] Dana Scott. Continuous Lattices. In F. William Lawvere, editor, Toposes, Algebraic Geometry and Logic, pages 97–136. Springer Berlin Heidelberg, 1972. doi:10.1007/BFb0073967.
[28] Dana Scott. Stochastic $\lambda$ -calculi. Journal of Applied Logic, 12(3):369–376, 2014.
[29] Robert I. Soare. Recursively Enumerable Sets and Degrees. Perspectives in Mathematical Logic. Springer, 1987.
[30] Clifford Spector. Measure-Theoretic Construction of Incomparable Hyperdegrees. Journal of Symbolic Logic, 23(3):280–288, September 1958. doi:10.2307/2964288.
[31] Sam Staton, Hongseok Yang, Frank Wood, Chris Heunen, and Ohad Kammar. Semantics for probabilistic programming: higher-order functions, continuous distributions, and soft constraints. In Proceedings of the 31st Annual ACM-IEEE Symposium On Logic In Computer Science, pages 525–534, 2017.
[32] Matthijs Vákár, Ohad Kammar, and Sam Staton. A domain theory for statistical probabilistic programming. Proceedings of the ACM Conference on Principles of Programming Languages, 3(POPL):1–29, 2019. doi:10.1145/3290349.
[33] Frank Wood, Jan Willem van de Meent, and Vikash Mansinghka. A new approach to probabilistic programming inference. In Proceedings of the 17th International conference on Artificial Intelligence and Statistics, pages 1024–1032, 2014. URL: http://proceedings.mlr.press/v33/wood14.html.

Appendix A Appendix

Proof of Theorem 1.

For (i) and (ii), see [5, Theorem 1.17]; (iii) is a particular instance of what we shall later call the “completeness” of $V^{A}$ – see [19, Lemma 14.19] or [5, Lemma 1.27]. $\hfill\blacktriangleleft$

Proof of Theorem 26.

It follows from Theorem 1 applied to Definition 25 that there exist some elements of $V^{A}$ representing functions $\llbracket{{\mbox{-}}}\rrbracket^{A}_{\rho}$ with the required properties holding with Boolean value $1$ . So by Corollary 18 we can take $\llbracket{{\mbox{-}}}\rrbracket^{A}_{\rho}\in\mathbf{Set}_{A}(\Lambda(D,% \widecheck{\mathrm{Var}},\mathfrak{K})^{A},D)$ and also $\llbracket{{\mbox{-}}}\rrbracket^{A}_{\rho}\in\mathbf{Set}_{A}(\widecheck{% \Lambda(\mathrm{Var})},D)$ for pure terms (using Proposition 22). So by Definition 16, these define maps in $\mathbf{SetoidR}_{A}(\Lambda(D,\widecheck{\mathrm{Var}},\mathfrak{K})^{A},D)$ and $\mathbf{SetoidR}_{A}(\widecheck{\Lambda(\mathrm{Var})},D)$ . So by completeness of $D$ , we can apply Definition 13 to get maps in $\mathbf{SetoidF}_{A}(\Lambda(D,\widecheck{\mathrm{Var}},\mathfrak{K})^{A},D)$ and $\mathbf{SetoidF}_{A}(\widecheck{\Lambda(\mathrm{Var})},D)$ .

From this, we get that if $\boldsymbol{\lambda}\vdash M=N$ , then $\|\widecheck{(M,N)}\in\boldsymbol{\lambda}^{A}\|=1$ , and therefore for all $\rho$ , $\|\llbracket{\check{M}}\rrbracket_{\rho}=\llbracket{\check{N}}\rrbracket_{\rho% }\|=1$ . Since $D$ is strict, this implies that actually $\llbracket{\check{M}}\rrbracket_{\rho}=\llbracket{\check{N}}\rrbracket_{\rho}$ in the usual sense as well. $\hfill\blacktriangleleft$

Proof of Proposition 28.

We get the first part by applying Theorem 1 to Proposition 27. By Theorem 17, $\mathcal{P}^{A}(X)$ is complete, and it is clear from its definition that it is total. Now, if $X=\check{Y}$ , we use the fact that $\|\widecheck{\mathcal{P}_{\mathrm{fin}}(Y)}=\mathcal{P}^{A}_{\mathrm{fin}}(% \check{Y})\|=1$ (Proposition 3), so $\widecheck{\mathcal{P}_{\mathrm{fin}}(Y)}$ is also a base for $\mathcal{P}^{A}(\check{Y})$ with Boolean value 1.

Finally, to show that $\mathcal{P}^{A}(\check{Y})$ is strict, let $S,T\in\mathcal{P}^{A}(\check{Y})$ such that $\|S=T\|_{\mathcal{P}^{A}(\check{Y})}=1$ , which is equivalent to $\|S=T\|=1$ . First observe that $\mathrm{dom}(S)=\mathrm{dom}(\check{Y})=\mathrm{dom}(T)$ , and then that for all $\check{y}\in\mathrm{dom}(\check{Y})$ , we have $\|\check{y}\in S\|=S(\check{y})$ and likewise for $T$ . Since $\|S=T\|=1$ , for all $y\in Y$ we have

S(\check{y})=\|\check{y}\in S\|=\|\check{y}\in T\|=T(\check{y}),

so $S=T$ . $\hfill\blacktriangleleft$

Proof of Theorem 30.

By Theorem 2, $\widecheck{({\mbox{-}},{\mbox{-}})}$ defines an injective function $\widecheck{\mathcal{P}_{\mathrm{fin}}(E)}\mathrel{\times_{\!A}}\check{E}=% \widecheck{\mathcal{P}_{\mathrm{fin}}(E)\times E}\rightarrow\check{E}$ . Since $\|\widecheck{\mathcal{P}_{\mathrm{fin}}(E)}=\mathcal{P}^{A}_{\mathrm{fin}}(% \check{E})\|=1$ by Prop. 3, it also defines an injective function $\mathcal{P}^{A}_{\mathrm{fin}}(\check{E})\mathrel{\times_{\!A}}\check{E}% \rightarrow\check{E}$ . We apply Theorem 1 (i) to Prop. 29 to conclude that $\mathcal{P}^{A}(\check{E})$ is a reflexive dcpo. $\hfill\blacktriangleleft$

Proof of Corollary 34.

By Lemma 31, $\|\llbracket{\check{\bot}}\rrbracket^{A}=\widecheck{\llbracket{\bot}\rrbracket% }\|=1$ , and likewise for $\top$ and the Church numerals.

Then part (i) of Definition 32 is a $\Delta_{0}$ statement, so it follows by applying Theorem 2 to Proposition 33. Parts (ii) - (iv) then follow by Example 24. $\hfill\blacktriangleleft$

Proof of Lemma 35.

(i)

As Scott topologies are $T_{0}$ , part (i) of Definition 32 implies that there is a Scott-open set $U\subseteq D$ containing one of $\{\llbracket{\top}\rrbracket,\llbracket{\bot}\rrbracket\}$ but not the other. We start under the assumption that $\llbracket{\top}\rrbracket\in U$ and $\llbracket{\bot}\rrbracket\not\in U$ . This implies that $\{\llbracket{\top}\rrbracket\}$ is an open subset of the subspace $\{\llbracket{\top}\rrbracket,\llbracket{\bot}\rrbracket\}$ .

The map $\mathbf{fun}(\llbracket{\lnot}\rrbracket):D\rightarrow D$ is Scott continuous, and $\mathbf{fun}(\llbracket{\lnot}\rrbracket)(\llbracket{\bot}\rrbracket)=% \llbracket{\top}\rrbracket$ and vice-versa. So $\mathbf{fun}(\llbracket{\lnot}\rrbracket)^{-1}(U)$ is an open set containing $\llbracket{\bot}\rrbracket$ , but not $\llbracket{\top}\rrbracket$ , proving that $\{\llbracket{\bot}\rrbracket\}$ is an open subset of the subspace $\{\llbracket{\top}\rrbracket,\llbracket{\bot}\rrbracket\}$ . This proves that $\{\llbracket{\top}\rrbracket,\llbracket{\bot}\rrbracket\}$ is a discrete subspace of $D$ , and the proof starting with $\llbracket{\bot}\rrbracket\in U$ is similar.

To prove the discreteness and distinctness of $\{\llbracket{c_{n}}\rrbracket\}_{n\in\mathbb{N}}$ , we will need the fact that there exist closed $\lambda$ -terms $\mathbf{m}^{?}$ such that $\boldsymbol{\lambda}\vdash\mathbf{m}^{?}c_{n}=\top$ if $m=n$ and $\boldsymbol{\lambda}\vdash\mathbf{m}^{?}c_{n}=\bot$ otherwise. It is not difficult to prove directly that we can take $\mathbf{1}^{?}=\lambda m.\mathbf{if}(\mathbf{0}^{?}m)\bot(\mathbf{0}^{?}(% \mathbf{pred}m))$ , and $\mathbf{n}^{?}=\lambda m.\mathbf{n-1}^{?}(\mathbf{pred}m)$ . It follows that $\mathbf{fun}(\llbracket{\mathbf{n}^{?}}\rrbracket)(\llbracket{c_{m}}\rrbracket% )=\llbracket{\top}\rrbracket$ if $n=m$ and $\llbracket{\bot}\rrbracket$ otherwise.

Now, if $m\neq n$ are elements of $\mathbb{N}$ , we have $\boldsymbol{\lambda}\vdash\mathbf{m}^{?}c_{m}=\top$ , and $\boldsymbol{\lambda}\vdash\mathbf{m}^{?}c_{n}=\bot$ , so $\mathbf{fun}(\llbracket{\mathbf{m}^{?}}\rrbracket)(\llbracket{c_{m}}\rrbracket% )=\llbracket{\top}\rrbracket\neq\llbracket{\bot}\rrbracket=\mathbf{fun}(% \llbracket{\mathbf{m}^{?}}\rrbracket)(\llbracket{c_{n}}\rrbracket)$ . As $\mathbf{fun}(\llbracket{\mathbf{m}^{?}}\rrbracket$ is a function, it follows that $\llbracket{c_{m}}\rrbracket\neq\llbracket{c_{n}}\rrbracket$ .

To prove the discreteness of $\{\llbracket{c_{n}}\rrbracket\}_{n\in\mathbb{N}}$ , we show that for all $m\in\mathbb{N}$ , the singleton $\{\llbracket{c_{m}}\rrbracket\}$ is relatively open in $\{\llbracket{c_{n}}\rrbracket\}_{n\in\mathbb{N}}$ . Let $U\subseteq D$ be a Scott-open set such that $\llbracket{\top}\rrbracket\in U$ , but $\llbracket{\bot}\rrbracket\not\in U$ . Then $V=\mathbf{fun}(\llbracket{\mathbf{m}^{?}}\rrbracket)^{-1}(U)$ is a Scott-open set such that $\llbracket{m}\rrbracket\in V$ but $\llbracket{n}\rrbracket\not\in V$ for all $n\in\mathbb{N}$ such that $n\neq m$ .
(ii)

Given $A\subseteq\mathbb{N}$ , define $g:\{\llbracket{c_{n}}\rrbracket\}_{n\in\mathbb{N}}\rightarrow D$ by $g(\llbracket{c_{n}}\rrbracket)=\chi^{D}_{A}(n)$ . By the discreteness of $\{\llbracket{c_{n}}\rrbracket\}_{n\in\mathbb{N}}$ , proved in the previous part, this is continuous. Since $D$ is a continuous lattice, and therefore injective [27, Theorem 2.12], $g$ extends to a Scott-continuous map $\overline{g}:D\rightarrow D$ , and since $(D,\mathbf{lam},\mathbf{fun})$ is a reflexive dcpo we can define $d_{g}=\mathbf{lam}\overline{g}$ , and then for all $n\in\mathbb{N}$ :

$d_{g}\cdot\llbracket{c_{n}}\rrbracket=\overline{g}(\llbracket{c_{n}}\rrbracket% )=\chi^{D}_{A}(n).\$

$\hfill\blacktriangleleft$

Proof of Lemma 38.

We prove that $\|a\leq b\|_{\mathcal{L}^{0}}$ is measurable as follows. First, define $\gamma\subseteq\mathcal{P}(Y)\times\mathcal{P}(Y)$ to be the graph of the $\subseteq$ relation, i.e. $\nobreak\ \nobreak\ \gamma=\{(S,T)\in\mathcal{P}(Y)\times\mathcal{P}(Y)\mid S% \subseteq T\}$ .

$\|a\leq b\|_{\mathcal{L}^{0}}=\langle a,b\rangle^{-1}(\gamma)$ , so since $\langle a,b\rangle:X\rightarrow\mathcal{P}(Y)\times\mathcal{P}(Y)$ is measurable, we only need to show that $\gamma$ is measurable with respect to the product measurable space structure. We have

	$\displaystyle\gamma$	$\displaystyle=\{(S,T)\in\mathcal{P}(Y)\times\mathcal{P}(Y)\mid\forall y\in Y.y% \in S\Rightarrow y\in T\}$
		$\displaystyle=\bigcap_{y\in Y}\{(S,T)\in\mathcal{P}(Y)\times\mathcal{P}(Y)\mid y% \not\in S\text{ or }y\in T\}$
		$\displaystyle=\bigcap_{y\in Y}\{(S,T)\in\mathcal{P}(Y)\times\mathcal{P}(Y)\mid y% \not\in S\}\cup\{(S,T)\in\mathcal{P}(Y)\times\mathcal{P}(Y)\mid y\in T\}$
		$\displaystyle=\bigcap_{y\in Y}((\mathcal{P}(Y)\setminus B_{y})\times\mathcal{P% }(Y))\cup(\mathcal{P}(Y)\times B_{y}).$

Measurability then follows from the countability of $Y$ .

For the well-definedness of $\|\mbox{$\leq$}\|_{L^{0}}$ , it is clear that if $a\sim a^{\prime}$ and $b\sim b^{\prime}$ , then $\|a\leq b\|_{\mathcal{L}^{0}}$ and $\|a^{\prime}\leq b^{\prime}\|_{\mathcal{L}^{0}}$ can only differ where $a$ differs from $a^{\prime}$ or $b$ differs from $b^{\prime}$ , and the set of all such points is in $\mathcal{N}_{X}$ . It is easy to deduce the transitivity (in the sense of Definition 11 (i)) from transitivity of $\subseteq$ , and part (ii) of the definition of an $A(X)$ -poset follows because $\|a\leq a\|_{L^{0}}=1$ for all $a\in L^{0}(X;\mathcal{P}(Y))$ . $\hfill\blacktriangleleft$

Proof of Proposition 39.

We show that for all $a,b\in\mathcal{L}^{0}(X;\mathcal{P}(Y))$ , $\|G_{X}([a])\leq G_{X}([b])\|_{\mathcal{P}^{A(X)}(\check{Y})}=\|[a]\leq[b]\|_{% L^{0}}$ . This shows, in one go, that $G_{X}$ is an $A(X)$ -monotone function and also injective (using the fact that $L^{0}(X;\mathcal{P}(Y))$ is total, i.e. $\varepsilon_{L^{0}(X;\mathcal{P}(Y))}([a])=[X]$ for all $a\in\mathcal{L}^{0}(X;\mathcal{P}(Y))$ ).

We start by expanding the definitions:

		$\displaystyle\\|G_{X}([a])\leq G_{X}([b])\\|_{\mathcal{P}^{A(X)}(\check{Y})}=\\|G% _{X}([a])\subseteq G_{X}([b])\\|$
	$\displaystyle={}$	$\displaystyle\bigwedge_{t\in\mathrm{dom}(G_{X}([a]))}\\|t\in G_{X}([a])\\|% \Rightarrow\\|t\in G_{X}([b])\\|=\bigwedge_{y\in Y}G_{X}([a])(\check{y})% \Rightarrow G_{X}([b])(\check{y})$
	$\displaystyle={}$	$\displaystyle\bigwedge_{y\in Y}[\{x\in X\mid y\in a(x)\}]\Rightarrow[\{x\in X% \mid y\in b(x)\}]$
	$\displaystyle={}$	$\displaystyle\left[\bigcap_{y\in Y}\{x\in X\mid y\in a(x)\text{ implies }y\in b% (x)\}\right]$
	$\displaystyle={}$	$\displaystyle[\{x\in X\mid\forall y\in Y.y\in a(x)\text{ implies }y\in b(x)\}]$
	$\displaystyle={}$	$\displaystyle[\{x\in X\mid a(x)\subseteq b(x)\}]=\\|[a]\leq[b]\\|_{L^{0}}.$

Since $L^{0}(X;\mathcal{P}(Y))$ is a strict $A(X)$ -setoid, and $\mathcal{P}^{A(X)}(\check{Y})$ is total, implying that $G_{X}$ is an injective function. So to prove that $G_{X}$ is a strict isomorphism, we only need to show that $G_{X}$ is surjective.

Let $b\in\mathcal{P}^{A(X)}(\check{Y})$ . For each $y\in Y$ , pick $S_{y}\in\Sigma$ such that $[S_{y}]=b(\check{y})$ . Define a function
$a:X\rightarrow\mathcal{P}(Y)$ by $a(x)=\{y\in Y\mid x\in S_{y}\}$ . For each $y\in Y$ , we have

a^{-1}(B_{y})=\{x\in X\mid a(x)\in B_{y}\}=\{x\in X\mid y\in a(x)\}=\{x\in X% \mid x\in S_{y}\}=S_{y}\in\Sigma.

Since $(B_{y})_{y\in Y}$ generates the Borel $\sigma$ -algebra of $\mathcal{P}(Y)$ , this implies that $a$ is measurable. For all $y\in Y$ , we then have

G_{X}([a])(\check{y})=[a^{-1}(B_{y})]=[S_{y}]=b(\check{y}),

and therefore $G_{X}([a])=b$ , as required to prove $G_{X}$ surjective. $\hfill\blacktriangleleft$

Proof of Proposition 40.

In fact, we will prove the first part by deducing it from the second part. So let $a,b\in\mathcal{L}^{0}(X;\mathcal{P}(E))$ . Then for all $q\in E$ we have

	$\displaystyle(G_{X}([a])\cdot G_{X}([b]))(\check{q})$
$\displaystyle={}$	$\displaystyle\\|\exists K\in\mathcal{P}^{A(X)}_{\mathrm{fin}}(\check{E}).K% \subseteq G_{X}([b])\text{ and }(K,\check{q})^{A(X)}\in G_{X}([a])\\|$
$\displaystyle={}$	$\displaystyle\\|\exists K\in\widecheck{\mathcal{P}_{\mathrm{fin}}(E)}.K% \subseteq G_{X}([b])\text{ and }(K,\check{q})^{A(X)}\in G_{X}([a])\\|$	Proposition 3
$\displaystyle={}$	$\displaystyle\bigvee_{K\in\mathcal{P}_{\mathrm{fin}}(E)}\\|\check{K}\subseteq G% _{X}([b])\\|\land\\|\widecheck{(K,q)}\in G_{X}([a])\\|$
$\displaystyle={}$	$\displaystyle\bigvee_{K\in\mathcal{P}_{\mathrm{fin}}(E)}G_{X}([a])(\widecheck{% (K,q)})\land\bigwedge_{k\in K}G_{X}([b])(\check{k})$
$\displaystyle={}$	$\displaystyle\bigvee_{K\in\mathcal{P}_{\mathrm{fin}}(E)}[\{x\in X\mid(K,q)\in a% (x)\}]\land\bigwedge_{k\in K}[\{x\in X\mid k\in b(x)\}]$
$\displaystyle={}$	$\displaystyle\bigvee_{K\in\mathcal{P}_{\mathrm{fin}}(E)}[\{x\in X\mid(K,q)\in a% (x)\}]\land[\{x\in X\mid K\subseteq b(x)\}]$
$\displaystyle={}$	$\displaystyle[\{x\in X\mid\exists K\in\mathcal{P}_{\mathrm{fin}}(E).K\subseteq b% (x)\text{ and }(K,q)\in a(x)\}]$	as $\mathcal{P}_{\mathrm{fin}}(E)$ countable
$\displaystyle={}$	$\displaystyle[\{x\in X\mid q\in a(x)\cdot b(x)\}]$
$\displaystyle={}$	$\displaystyle G_{X}([a\cdot b])(\check{q}),$

so all together we have proved that $G_{X}([a])\cdot G_{X}([b])=G_{X}([a\cdot b])$ . In passing, we have proved that for all $q\in E$ , $(a\cdot b)^{-1}(B_{q})$ is measurable, and therefore that $a\cdot b\in\mathcal{L}^{0}(X;\mathcal{P}(E))$ .

If $a^{\prime},b^{\prime}\in\mathcal{L}^{0}(X;\mathcal{P}(E))$ such that $[a^{\prime}]=[a]$ and $[b^{\prime}]=[b]$ , then by Proposition 39 and the fact that $\mathcal{P}^{A(X)}(\check{E})$ is a strict $A(X)$ -setoid:

G_{X}([a\cdot b])=G_{X}([a])\cdot G_{X}([b])=G_{X}([a^{\prime}])\cdot G_{X}([b% ^{\prime}])=G_{X}([a^{\prime}\cdot b^{\prime}]),

and therefore $[a\cdot b]=[a^{\prime}\cdot b^{\prime}]$ , so the definition $[a]\cdot[b]=[a\cdot b]$ genuinely defines a function $L^{0}(X;\mathcal{P}(E))\times L^{0}(X;\mathcal{P}(E))\rightarrow L^{0}(X;% \mathcal{P}(E))$ . Putting this together with what we proved above gives us $G_{X}([a])\cdot G_{X}([b])=G_{X}([a]\cdot[b])$ . $\hfill\blacktriangleleft$

Proof of Lemma 41.

It suffices to show that for all $y\in Y$ , $\|\check{y}\in G_{X}([K_{S}])\|=\|\check{y}\in\check{S}\|$ . We have

\|\check{y}\in G_{X}([K_{S}])\|=G_{X}([K_{S}])(\check{y})=[\{x\in X\mid y\in K% _{S}(x)\}]=[\{x\in X\mid y\in S\}]=\|\check{y}\in\check{S}\|.

$\hfill\blacktriangleleft$

Proof of Proposition 44.

First, let $p=\bigvee\{a\in A(X)\mid a\text{ an atom}\}$ . As $A(X)$ is not atomic, $\lnot p\neq 0$ , so there is a set $S\in\Sigma$ such that $S\not\in\mathcal{N}$ and $[S]=\lnot p$ . By definition there are no atoms below $[S]$ . Define

b(x)=\begin{cases}Y&\text{if }x\in S\\ \emptyset&\text{otherwise,}\end{cases}

where $x\in X$ . This defines a measurable function $X\rightarrow\mathcal{P}(Y)$ . As $S\not\in\mathcal{N}$ , $[b]\neq[K_{\emptyset}]$ . We show that $L^{0}(X;\mathcal{P}(Y))$ is not continuous by showing that $[b]$ is not the supremum of elements way below it, which will follow from the fact that the only element of $L^{0}(X;\mathcal{P}(Y))$ that is way below $[b]$ is $[K_{\emptyset}]$ .

If the only element below $[b]$ is $[K_{\emptyset}]$ , then we are finished, so we reduce to the case that there is at least one $[a]\in L^{0}(X;\mathcal{P}(Y))$ such that $[K_{\emptyset}]<[a]<[b]$ . Define $T=a^{-1}(\mathcal{P}(Y)\setminus\{\emptyset\})$ , which is in $\Sigma$ because $a$ is measurable and $\mathcal{P}(Y)\setminus\{\emptyset\}=\bigcup_{y\in Y}B_{y}$ and is therefore a Borel set. We have $T\setminus S\in\mathcal{N}$ , so we redefine $T$ to be $T\cap S$ if necessary to make $T\subseteq S$ .

Since there are no atoms below $[S]$ , there are none below $[T]$ either, so there exists a non-zero element $a_{1}\in A(X)$ such that $a_{1}\leq[T]$ and $a_{1}$ has no atoms below it. We can repeat this argument to form a strictly descending sequence $(a_{i})_{i\in\mathbb{N}}$ where for all $i\in\mathbb{N}$ , $a_{i}$ has no atoms below it and $a_{i}\leq[T]$ . We can define $b_{i}=a_{i}\setminus\bigwedge_{i=1}^{\infty}a_{i}$ , to get such a strictly decreasing sequence $(b_{i})_{i\in\mathbb{N}}$ , now with $\bigwedge_{i=1}^{\infty}b_{i}=0$ . Since $A(X)=\Sigma/\mathcal{N}$ , we can find a sequence $(V_{i})_{i\in\mathbb{N}}$ of elements of $\Sigma$ such that for all $i\in\mathbb{N}$ , $[V_{i}]=b_{i}$ , and by adjusting negligible sets it can be arranged that $(V_{i})_{i\in\mathbb{N}}$ is also strictly descending. Defining $T_{i}=T\setminus U_{i}$ , then $(T_{i})_{i\in\mathbb{N}}$ is strictly increasing with respect to $\subseteq$ , maps to a strictly increasing sequence under $[{\mbox{-}}]$ , and $T\setminus\bigcup_{i=1}^{\infty}T_{i}\in\mathcal{N}$ . Define, for each $i\in\mathbb{N}$ , $c_{i}:X\rightarrow\mathcal{P}(Y)$ as follows:

c_{i}(x)=\begin{cases}Y&\text{if }x\in T_{i}\cup S\setminus T\\ \emptyset&\text{if }x\in T\setminus T_{i}\cup X\setminus S,\end{cases}

where $x\in X$ . Each $c_{i}$ is measurable for the same reasons that $b$ is, and $([c_{i}])_{i\in\mathbb{N}}$ is a strictly increasing sequence in $L^{0}(X;\mathcal{P}(Y))$ . Since for all $i\in\mathbb{N}$ , $c_{i}(x)=\emptyset$ for all $x\in T\setminus T_{i}$ and $T\setminus T_{i}\not\in\mathcal{N}$ , while $a(x)\neq\emptyset$ for all $x\in T\supseteq T\setminus T_{i}$ , we have $[a]\not\leq[c_{i}]$ . But $\bigvee_{i=1}^{\infty}[c_{i}]=\left[\bigvee_{i=1}^{\infty}c_{i}\right]=[b]$ because $T\setminus\bigcup_{i=1}^{\infty}T_{i}\in\mathcal{N}$ . Therefore $a$ is not way below $b$ . $\hfill\blacktriangleleft$

[bib.bib1] [1] Nathanael L. Ackerman, Cameron E. Freer, and Daniel M. Roy. Noncomputable conditional distributions. In Logic in Computer Science (LICS), 2011 26th Annual IEEE Symposium on, pages 107–116. IEEE, 2011. doi:10.1109/LICS.2011.49.

[bib.bib2] [2] Nathanael L. Ackerman, Cameron E. Freer, and Daniel M. Roy. On the computability of conditional probability. J. ACM, 66(3):23:1–23:40, 2019. doi:10.1145/3321699.

[bib.bib3] [3] Giorgio Bacci, Robert Furber, Dexter Kozen, Radu Mardare, Prakash Panangaden, and Dana Scott. Boolean-valued semantics for the stochastic $\lambda$ -calculus. In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, pages 669–678. ACM, 2018. doi:10.1145/3209108.3209175.

[bib.bib4] [4] Henk P. Barendregt. The Lambda Calculus: Its Syntax and Semantics. North-Holland, Amsterdam, 1984.

[bib.bib5] [5] John L. Bell. Set Theory: Boolean-Valued Models and Independence Proofs, volume 47 of Oxford Logic Guides. Oxford University Press, third edition, 2005.

[bib.bib6] [6] Johannes Borgström, Ugo Dal Lago, Andrew D. Gordon, and Marcin Szymczak. A lambda-calculus foundation for universal probabilistic programming. In Jacques Garrigue, Gabriele Keller, and Eijiro Sumii, editors, Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, ICFP 2016, Nara, Japan, September 18-22, 2016, pages 33–46. ACM, 2016. doi:10.1145/2951913.2951942.

[bib.bib7] [7] Fredrik Dahlqvist and Dexter Kozen. Semantics of higher-order probabilistic programs with conditioning. Proc. ACM Program. Lang., 4(POPL):57:1–57:29, 2020. doi:10.1145/3371125.

[bib.bib8] [8] Pedro H. Azevedo de Amorim, Dexter Kozen, Radu Mardare, Prakash Panangaden, and Michael Roberts. Universal semantics for the stochastic $\lambda$ -calculus. In Proceedings of the ACM-IEEE Symposium on Logic in Computer Science, 2021. arXiv preprint:2011.13171.

[bib.bib9] [9] Thomas Ehrhard, Michele Pagani, and Christine Tasson. Measurable cones and stable, measurable functions: a model for probabilistic higher-order programming. Proceedings of the ACM Symposium on Principles of Programming Languages, 2(POPL):1–28, 2017. doi:10.1145/3158147.

[bib.bib10] [10] Thomas Ehrhard, Christine Tasson, and Michele Pagani. Probabilistic coherence spaces are fully abstract for probabilistic pcf. In Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 309–320, 2014. doi:10.1145/2535838.2535865.

[bib.bib11] [11] Erwin Engeler. Algebras and Combinators. Algebra Universalis, 13(1):389–392, December 1981. doi:10.1007/BF02483849.

[bib.bib12] [12] Michael P. Fourman and Dana S. Scott. Sheaves and Logic. In Michael Fourman, Christopher Mulvey, and Dana Scott, editors, Applications of Sheaves: Proceedings of the Research Symposium on Applications of Sheaf Theory to Logic, Algebra, and Analysis, Durham, July 9–21, 1977, pages 302–401. Springer Berlin Heidelberg, 1979. doi:10.1007/BFb0061824.

[bib.bib13] [13] David H. Fremlin. Measure Theory, Volume 3. https://www.essex.ac.uk/maths/people/fremlin/mt.htm, 2002.

[bib.bib14] [14] Gerhard Gierz, Karl H. Hofmann, Klaus Keimel, Jimmie D. Lawson, Michael W. Mislove, and Dana S. Scott. Continuous Lattices and Domains, volume 93 of Encyclopedia of Mathematics and its Applications. Cambridge University Press, 2003.

[bib.bib15] [15] Robert Goldblatt. Topoi: The Categorial Analysis of Logic. Dover, 2006.

[bib.bib16] [16] Noah Goodman, Vikash Mansingkha, Daniel Roy, Keith Bonawitz, and Joshua Tenenbaum. Church: a language for generative models. In Proceedings of the 24th Conference on Uncertainty in Artificial Intelligence, pages 220–229, 2008.

[bib.bib17] [17] Chris Heunen, Ohad Kammar, Sam Staton, and Hongseok Yang. A convenient category for higher-order probability theory. In Proceedings of the Thirty-second Annual ACM-IEEE Symposium on Logic in Computer Science, pages 1–12, 2017. doi:10.1109/LICS.2017.8005137.

[bib.bib18] [18] Martin Hyland, Misao Nagayama, John Power, and Giuseppe Rosolini. A Category Theoretic Formulation for Engeler-style Models of the Untyped $\lambda$ -Calculus. Electronic Notes in Theoretical Computer Science, 161:43–57, 2006. Proceedings of the Third Irish Conference on the Mathematical Foundations of Computer Science and Information Technology (MFCSIT 2004). doi:10.1016/j.entcs.2006.04.024.

[bib.bib19] [19] Thomas J. Jech. Set Theory. Springer, 3rd Millennium edition, 2003.

[bib.bib20] [20] Stephen C. Kleene and Emil L. Post. The Upper Semi-Lattice of Degrees of Recursive Unsolvability. Annals of Mathematics, 59(3):379–407, 1954. doi:10.2307/1969708.

[bib.bib21] [21] Anatoly G. Kusraev and Semën S. Kutateladze. Boolean Valued Analysis, volume 494 of Mathematics and Its Applications. Springer, 1999. doi:10.1007/978-94-011-4443-8.

[bib.bib22] [22] Radu Mardare, Prakash Panangaden, and Gordon Plotkin. Quantitative algebraic reasoning. In Proceedings of the 31st Annual ACM-IEEE Symposium on Logic in Computer Science, pages 700–709, 2016. doi:10.1145/2933575.2934518.

[bib.bib23] [23] Gordon P. Monro. A Category-theoretic Approach to Boolean-valued Models of Set Theory. Journal of Pure and Applied Algebra, 42(3):245–274, 1986. doi:10.1016/0022-4049(86)90010-1.

[bib.bib24] [24] Gordon P. Monro. Quasitopoi, Logic and Heyting-valued Models. Journal of Pure and Applied Algebra, 42(2):141–164, 1986. doi:10.1016/0022-4049(86)90077-0.

[bib.bib25] [25] Dan Roy. Computability, inference and modeling in probabilistic programming. PhD thesis, MIT, June 2011.

[bib.bib26] [26] Dana Scott. A proof of the independence of the continuum hypothesis. Mathematical Systems Theory, 1(2):89–111, 1967. doi:10.1007/BF01705520.

[bib.bib27] [27] Dana Scott. Continuous Lattices. In F. William Lawvere, editor, Toposes, Algebraic Geometry and Logic, pages 97–136. Springer Berlin Heidelberg, 1972. doi:10.1007/BFb0073967.

[bib.bib28] [28] Dana Scott. Stochastic $\lambda$ -calculi. Journal of Applied Logic, 12(3):369–376, 2014.

[bib.bib29] [29] Robert I. Soare. Recursively Enumerable Sets and Degrees. Perspectives in Mathematical Logic. Springer, 1987.

[bib.bib30] [30] Clifford Spector. Measure-Theoretic Construction of Incomparable Hyperdegrees. Journal of Symbolic Logic, 23(3):280–288, September 1958. doi:10.2307/2964288.

[bib.bib31] [31] Sam Staton, Hongseok Yang, Frank Wood, Chris Heunen, and Ohad Kammar. Semantics for probabilistic programming: higher-order functions, continuous distributions, and soft constraints. In Proceedings of the 31st Annual ACM-IEEE Symposium On Logic In Computer Science, pages 525–534, 2017.

[bib.bib32] [32] Matthijs Vákár, Ohad Kammar, and Sam Staton. A domain theory for statistical probabilistic programming. Proceedings of the ACM Conference on Principles of Programming Languages, 3(POPL):1–29, 2019. doi:10.1145/3290349.

[bib.bib33] [33] Frank Wood, Jan Willem van de Meent, and Vikash Mansinghka. A new approach to probabilistic programming inference. In Proceedings of the 17th International conference on Artificial Intelligence and Statistics, pages 1024–1032, 2014. URL: http://proceedings.mlr.press/v33/wood14.html.

	$\displaystyle\forall x,y\in X.\\|x=y\\|_{X}$	$\displaystyle=\\|y=x\\|_{X}$
	$\displaystyle\forall x,y,z\in X.\\|x=y\\|_{X}\land\\|y=z\\|_{X}$	$\displaystyle\leq\\|x=z\\|_{X}.$

	$\displaystyle X\multimap Y$	$\displaystyle=\{f:X\rightarrow Y\mid\forall x_{1},x_{2}\in X.\\|x_{1}=x_{2}\\|_{% X}\leq\\|f(x_{1})=f(x_{2})\\|_{Y}\}$
	$\displaystyle\\|f_{1}=f_{2}\\|_{X\multimap Y}$	$\displaystyle=\bigwedge_{x\in X}\varepsilon_{X}(x)\Rightarrow\\|f_{1}(x)=f_{2}(% x)\\|_{Y}.$

Interpreting Lambda Calculus in Domain-Valued Random Variables

Abstract

Keywords and phrases:

Copyright and License:

2012 ACM Subject Classification:

Related Version:

DOI:

Event:

Editors:

Series and Publisher:

1 Introduction

2 Background on Boolean-Valued Set Theory

Theorem 1 (VA as a model).

Theorem 2 (Δ0 invariance).

Proposition 3.

3 Boolean-Valued Setoids

Definition 4.

Definition 5.

Definition 6.

Definition 7.

Definition 8.

Definition 9.

Definition 10.

Definition 11.

Lemma 12.

Definition 13.

Definition 14.

Definition 15.

Definition 16.

Theorem 17.

Corollary 18.

4 Models of Untyped Lambda-calculus in Boolean-valued sets

4.1 Background on Domain Theory

Definition 19.

Definition 20.

Example 21.

Proposition 22.

Definition 23.

Example 24.

Definition 25.

Theorem 26.

4.2 The Engeler Model

Proposition 27.

Proposition 28.

Proposition 29.

Theorem 30.

Lemma 31.

4.3 Injective Spaces and Oracles

Definition 32.

Proposition 33.

Corollary 34.

Lemma 35.

Proposition 36.

5 Random Variables

Definition 37.

Lemma 38.

Proposition 39.

Proposition 40.

Lemma 41.

Proposition 42.

Theorem 43.

Proof.

Proposition 44.

6 Conclusions

References

Appendix A Appendix

Proof of Theorem 1.

Proof of Theorem 26.

Proof of Proposition 28.

Proof of Theorem 30.

Proof of Corollary 34.

Proof of Lemma 35.

Proof of Lemma 38.

Proof of Proposition 39.

Proof of Proposition 40.

Proof of Lemma 41.

Proof of Proposition 44.

Theorem 1 ( $V^{A}$ as a model).

Theorem 2 ( $\Delta_{0}$ invariance).