<commit_before>\newcommand{\Stream}{\mathsf{Stream}}
\newcommand{\Prob}{\mathcal{R}}

\subsection{Introduction}

Suppose we have access to a random bitstream which affords us an ``API'' to access it, $s \leftarrow \mu_R$, where $\mu_R : \Prob(\Stream(\bool))$ is the probability distribution over bitstreams which gives equal probability to all bitstreams, and where we can think of $\Stream$s as being coinductively defined to in some sense ``prefer'' access to the front, but anyway we have the homeomorphism $\Stream(A) \cong \nat \Rightarrow \bool$, where $\Rightarrow : \Type \to \Space \to \Space$ constructs function spaces with discrete domains.

Now, suppose that I have real number in the unit interval with the binary expansion
\[
0. p_0\ p_1\ p_2\ \ldots,
\]
such that we can think of $p : \Stream(\bool)$ as well. I want to sample a Boolean value which is true with probability $p$. We can write the following recursive map which compares streams of Boolean values:
\begin{align*}
\mathsf{cmp} &: \Stream(\bool) \times \Stream(\bool) \to \bool_\bot
\\ \mathsf{cmp}(x, y) &\triangleq \mathsf{cases}(x, y)
\begin{cases}
b_x :: x'\ ,\ b_y :: y'
\quad \Longrightarrow \quad
\mathsf{cases}(b_x, b_y)
  \begin{cases}
  \mathsf{true}\ ,\ \mathsf{false} \quad &\Longrightarrow \quad
    \mathsf{strict}(\mathsf{false})
    \\
    \mathsf{false}\ ,\ \mathsf{true} \quad &\Longrightarrow \quad
    \mathsf{strict}(\mathsf{true})
    \\
    \mathsf{false}\ ,\ \mathsf{false} \quad &\Longrightarrow \quad
    \mathsf{cmp}(x', y')
    \\
    \mathsf{true}\ ,\ \mathsf{true} \quad &\Longrightarrow \quad
    \mathsf{cmp}(x', y')
  \end{cases}
\end{cases}
\end{align*}

Then, to use our random bitstream $s$ to return a Boolean value which is true with probability $p$, we need only compute the comparison $\mathsf{cmp}(p, s) : \bool_\bot$. The issue, which is indicated by the return type of this comparison, is that the comparison doesn't necessarily terminate. What if it happens to be that $p = s$? Then we are in a rut.

Fortunately, this \emph{isn't} the case. While, in our situation, $p : \Stream(\bool)$ is a point of the space, $s \leftarrow \mu_R$ is \emph{not} a point. That's because $\mu_R$ is non-atomic, which means that for any \emph{global point} $p$ of $\Stream(\bool)$,
\[
\mu_R(\cdot \neq p) = \mu_R(\top) = 1.
\]
That is, for any point $p$, $s$ is \emph{not} $p$ (with probability 1).

\cite{simpson2012} defines the ``locale of random sequences'' for a given measure $\mu$, which satisfy all measure-1 properties of that measure. By the previous reasoning, these spaces must not have any points. However, they still have computational structure, and I would like to tentatively argue in this note, that we can avoid dealing with reasoning about termination of functions like $\mathsf{cmp}$ defined on $\Stream(\bool)$ by using that structure. Instead of dealing with $\Stream(\bool)$, we use a subspace of it, called $\Stream(\bool)_{\mu_R}$, which is defined by the nucleus [refer to nLab for definition]
\[
U \mapsto \bigcup \left\{ V \suchthat U \subseteq V, \mu_R(U) = \mu_R(V) \right\},
\]
so that instead we would have for every \emph{global} point $p : \Stream(\bool)$,
\footnote{There are likely predicativity issues here, since there are more and more such global points as you increase the universe level of the ``predicative locale'' which these are points of. This is likely related to the predicativity issues of the double negation sublocale.}
\[
\mathsf{cmp}_p : \Stream(\bool)_{\mu_R} \to \bool.
\]
This in fact defines a valid nucleus. It wasn't clear to me that it preserves meets, so I emailed Antonin, and he provided a very nice explanation why it does in fact preserve meets.
\footnote{Why can't you have 
\[
\mathsf{cmp} :  \Stream(\bool) \times \Stream(\bool)_{\mu_R} \to \bool?
\]
Well, we have the mono $i_{\mu_R} : \Stream(\bool)_{\mu_R} \rightarrowtail \Stream(\bool)$, and imagining $s \leftarrow \mu_R$, we could then compute
\[
\mathsf{cmp}(i_{\mu_R}(s), s),
\]
which we know never terminates. The fact has to be that one input should be a global point, and the other must be random from a regular measure.}

Writing this program seems pointless, because as it turns out, the space $\Stream(\bool)_{\mu_R}$ doesn't have any points: the quotient operation which identifies an open set with the interior of its closure necessarily kills them all. So it seems like we can't ever run $\mathsf{cmp}$. But, recall that $\mu_R$ was a regular measure, so instead we can define $\mu_R : \Prob\left(\Stream(\bool)_{\mu_R} \right)$ which is a stricter requirement; only probability distributions with the same smallest measure-1 subspace as $\mu_R$ can be presented as probability distributions on this space. So the random stream $s \leftarrow \mu_R$, which is perhaps pulling from \texttt{/dev/random}, while certainly not a \emph{point} of $\Stream(\bool)_{\mu_R}$ (after all, this space has no points), implements the (seemingly-impossible) computational \emph{interface} for $\Stream(\bool)_{\mu_R}$.

At least, it does so with probability 1. My point is that using doubly-negated spaces and probability distributions over them, gives a useful formalism for not having to reason about probability 1 termination. All of capacity for non-termination is localized in the ``API'' interface for the random stream $s \leftarrow \mu_R$. In $\Stream(\bool)_{\mu_R}$, we have the cover
\[
\top_{\Stream(\bool)_{\mu_R}} \subseteq
  \bigcup_{n : \nat} [n \mapsto \mathsf{true}],
\]
which in English says that every $\Stream(\bool)$ drawn from $\mu_R$ eventually has a $\mathsf{true}$ somewhere in its sequence. This is of course missing the stream which is always $\mathsf{false}$, but that's all its missing, and because it occurs with probability 0 under $\mu_R$ we can neglect it.

The above cover has an obvious computational interpretation, let's say for our random stream $s \leftarrow \mu_R$. We must be able to \emph{compute} some index $n$ such that the $n$th element is $\mathsf{true}$. This might take a long time, potentially, but with probability 1, it is finite.

There's some philosophical question to be asked: certainly my random stream is \emph{some} stream, so if I happened to write a program that compares the random stream with another stream which happens to be the same exact one. And then it wouldn't terminate. But if we're waiting a long time, it could just be that we're impatient, and we need to wait longer. So even if you did manage to miraculously ``hit some probability 0 event'' in some sense, there's no way to be sure.

\subsection{Reestablishing decidability}

When I tell people that all functions in \contpl{} must be continuous, they get worried. They fret that they can't write a step function, or make a decision over a continuous variable. It may seem particularly worrying when it comes to dealing with probability, where it is only possible to compute the probability of an event if the event is decidable (i.e., clopen). On $\R$, there are no non-trivial open sets, so it seems that computing with probability distributions on $\R$ is a lost cause, if one can't compute the probability of any nontrivial event.

Computing these probabilities is hard for a reason. Suppose we have a distribution $\mu : \Prob(\R)$ and want to compute the probability of the open predicate $\cdot > 0$. The probability $\mu(\cdot > 0)$ is a lower real number, since $\cdot > 0$ is open, which is not useful for computation. It is necessarily hard to upper-bound $\mu(\cdot > 0)$. Suppose that $\mu = \delta(x)$, the Dirac delta distribution which has all its mass at a point $x$. Then $\mu(\cdot > 0) = 1$ if and only if $x > 0$, which is a Sierp\'inski-valued proposition, meaning that it is affirmable, but not refutable. To compute the measure of $\cdot > 0$ as a real number, we'd need to be able to compare $x$ with 0, which is not a computable (continuous) operation.

There are a few things we could do. Rather than attempting to compute the probability of an open set, we can compute the approximate probability of a binary cover of $\R$.\footnote{Binary covers are defined in another note.} Given a binary cover $(P, Q)$ of $\R$, that is, $P, Q : \Open{\R}$ and $\R \subseteq P \cup Q$, we can non-deterministically compute two real numbers, $x_P, x_Q : \R$ such that $x_P + x_Q = 1$ and $x_P \le \mu(P)$ and $x_Q \le \mu(Q)$. That is, we can split up the weight of $\mu$ into $P$ and $Q$, non-deterministically assigning any weight in $P \cap Q$ to either $x_P$ or $x_Q$.

For instance, for our predicate $\cdot > 0$, we might define a binary cover $(\cdot > 0)_\varepsilon : \R \to \mathsf{BCover}$ for any approximation tolerance $\varepsilon : \rat^+$, where
\begin{align*}
\mathsf{Left}^{-1}((\cdot > 0)_\varepsilon) &\triangleq \cdot > 0
\\ \mathsf{Right}^{-1}((\cdot > 0)_\varepsilon) &\triangleq \cdot < \varepsilon.
\end{align*}

Then, when we non-deterministically compute the probability of the $\mathsf{Left}$ and $\mathsf{Right}$ sides, the weight assigned to the $\mathsf{Left}$ side will be at most $\mu(\cdot > 0)$, the ``actual'' probability of the open $\cdot > 0$.

But this still seems unsatisfactory. If one cannot compute, \emph{exactly}, the probability that some normal distribution lies in an open interval (or \emph{any} non-trivial event), when there is clearly no theoretical obstacle to doing so, that would be a problem. There is a substantial difference between probability distributions such as Dirac deltas and normal distributions, and it is beneficial to treat them as two different objects.

Normal distributions are non-atomic, in the sense for any normal distribution $\mu$ and any \emph{global} point $p : \R$, $\mu(\cdot \neq p) = \mu(\top) = 1$. Therefore, normal distributions also give probability distributions over some subspace which has no points, which we'll call $\R_\mathcal{N}$. And while $\R_\mathcal{N}$ has no points, its space of probability distributions $\Prob\left(\R_\mathcal{N}\right)$ certainly does, since there is an obvious map of open sets $j_\mathcal{N} : \Open{\R} \to \Open{\R_\mathcal{N}}$ which is well-behaved and accordingly the map
\begin{align*}
j_\mathcal{N}^* &: \Prob\left(\R_\mathcal{N}\right) \to \Prob(\R)
\\ j_\mathcal{N}^*(\mu)(U) &\triangleq \mu(j_\mathcal{N}(U))
\end{align*}
is well-defined.

In $R_\mathcal{N}$, there is a wealth of decidable propositions (i.e., clopens), meaning that it is easy to compute the probability of many different events of $R_\mathbb{N}$. For instance, our predicate $\cdot > 0$ is now clopen! We have the cover
\[
\R_{\mathcal{N}} \subseteq (\cdot > 0) \cup (\cdot < 0),
\]
since in $\R$, there is the cover
\[
(\cdot \neq 0) \subseteq \neg \neg \left( (\cdot > 0) \cup (\cdot < 0) \right).
\]
Note that the covering for $\R_\mathcal{N}$ is non-trivial, even though $\R_\mathcal{N}$ has no points; even though I am using subset-like notation such as $\subseteq$ and $\cup$, these operations \emph{cannot} be interpreted as operations on subsets. Unlike sets, where all empty sets are isomorphic, two spaces without points are not necessarily homeomorphic to each other.

Since $\cdot > 0$ is clopen, this means that for any probability distribution $\mu : \Prob\left(\R_\mathcal{N}\right)$, we can compute the probabilities $\mu(\cdot > 0)$ and $\mu(\cdot < 0)$, and know that their sum is exactly 1. Many operations impossible on $\R$ are newly possible on $\R_\mathcal{N}$. 

We can compute floors with a pattern match with infinitely many cases:
\begin{align*}
\lfloor \cdot \rfloor &: \R_\mathcal{N} \to \nat
\\ \lfloor x \rfloor &\triangleq \mathsf{cases}(x)
\begin{cases}
[n : \nat] \quad n < \cdot < n + 1
  \qquad \Longrightarrow \qquad
  n
\end{cases}
\end{align*}
This pattern match is well-defined, since there is indeed the cover
\[
\R_\mathcal{N} \subseteq \bigcup_{n : \nat} (n < \cdot < n + 1),
\]
because we have that for any normal distribution $\mu$,
\[
\mu \left( \bigcup_{n : \nat} (n - 1 < \cdot < n + 1) \right) = \mu(\R) = 1.
\]

Continuous maps whose domains are $R_\mathcal{N}$ may not be able to run on points, but they can be useful in other ways: for instance, they can be integrated against certain probability distributions (distributions on $\R_\mathcal{N}$), or computed on samples from such distributions, which are not points but ``lawless sequences'' in some sense. Also, we are able to condition on decidable predicates (whose probability is more than 0): that is, given a space $A$ and probability distribution $\mu : \Prob(A)$, if $U : \Open{A}$ is clopen and satisfies $\mu(U) > 0$, then we can compute a probability distribution $\mu(\cdot \suchthat U) : \Prob(\{A \suchthat U \})$, whose measure is defined by the usual equation
\[
\mu(P \suchthat U) \triangleq \frac{1}{\mu(U)} \mu(P \cap U).
\]
We note that the right-hand side is indeed a lower real number, as it is required to be: since $\mu(U)$ is a real number greater than zero, so is $\frac{1}{\mu(U)}$, and $\mu(P \cap U)$ is a non-negative lower-real number, and multiplying a positive real number by a non-negative lower-real gives a non-negative lower real number.

Therefore, for instance, we could compute a conditional probability distribution of the standard normal distribution, given the observation $\cdot < 0$.

\subsection{Products}

How does producing measure-1 subspaces interact with products? 

Suppose I have have probability distributions $\mu_A : A_{\mu_A}$ and $\mu_B : B_{\mu_B}$. That is, both probability distributions are restricted to their smallest measure-1 subspace. There should be a continuous map, which I believe is mono,
\[f : (A \times B)_{\mu_A \otimes \mu_B} \to A_{\mu_A} \times B_{\mu_B}.\]

Does this map have a continuous inverse? That is, are these spaces homeomorphic, and does the double-negation operation commute with products? My hunch is that the answer is no. Taking $A$ and $B$ to both be $\R$, and $\mu_A$ and $\mu_B$ to be normali distributions, the ``diagonal" relation on $(\R \times \R)_{\mu_A \otimes \mu_B}$ should be clopen (in fact, it is equivalent to $\bot$), but I have a feeling that the diagonal of $\mathbb{R}_{\mu_A} \times \mathbb{R}_{\mu_B}$ shouldn't be open.

If we have probability distributions $\mu_A : \mathcal{R}(A_{\neg\neg})$ and $\mu_B : \mathcal{R}(B_{\neg\neg})$, then the independent product is \[\mu_A \otimes \mu_B : \mathcal{R}(A_{\neg\neg} \times B_{\neg\neg}).\]

I imagine there might be some analogies to be drawn with <NAME>'s discussion of measurable spaces in this MathOverflow answer\footnote{\url{http://mathoverflow.net/a/49542/82487}}.

\subsection{Predicativity worries}
All the statements which I'm making should be valid in an impredicative sense. But I'm worried about how to actually define the smallest measure-1 subspaces in a computational (predicative) way. For doubly-negated spaces, which are somewhat similar, I should cite some references which indicate that doubly-negated spaces \emph{cannot} be inductively generated formal topologies, at least in some cases I think.

The fact that I'm now fairly confident that I want to be able to have these measure-1 subspaces in \contpl{} means that I might need to reconsider using inductively generated formal topologies as \emph{the} main setting for everything.

\subsection{More...}

[[Partial samplers become total since they terminate with probability 1 - this is something that *really* bothers probabilistic semantics people, I should make this a key argument ]]<commit_msg>Some fixes to notes on random subspaces<commit_after>\newcommand{\Stream}{\mathsf{Stream}}
\newcommand{\Prob}{\mathcal{R}}

\subsection{Introduction}

Suppose we have access to a random bitstream which affords us an ``API'' to access it, $s \leftarrow \mu_R$, where $\mu_R : \Prob(\Stream(\bool))$ is the probability distribution over bitstreams which gives equal probability to all bitstreams, and where we can think of $\Stream$s as being coinductively defined to in some sense ``prefer'' access to the front, but anyway we have the homeomorphism $\Stream(A) \cong \nat \Rightarrow A$, where $\Rightarrow : \Type \to \Space \to \Space$ constructs function spaces with discrete domains.

Now, suppose that I have real number in the unit interval with the binary expansion
\[
0. p_0\ p_1\ p_2\ \ldots,
\]
such that we can think of $p : \Stream(\bool)$ as well. I want to sample a Boolean value which is true with probability $p$. We can write the following recursive map which compares streams of Boolean values:
\begin{align*}
\mathsf{cmp} &: \Stream(\bool) \times \Stream(\bool) \to \bool_\bot
\\ \mathsf{cmp}(x, y) &\triangleq \mathsf{cases}(x, y)
\begin{cases}
b_x :: x'\ ,\ b_y :: y'
\quad \Longrightarrow \quad
\mathsf{cases}(b_x, b_y)
  \begin{cases}
  \mathsf{true}\ ,\ \mathsf{false} \quad &\Longrightarrow \quad
    \mathsf{strict}(\mathsf{false})
    \\
    \mathsf{false}\ ,\ \mathsf{true} \quad &\Longrightarrow \quad
    \mathsf{strict}(\mathsf{true})
    \\
    \mathsf{false}\ ,\ \mathsf{false} \quad &\Longrightarrow \quad
    \mathsf{cmp}(x', y')
    \\
    \mathsf{true}\ ,\ \mathsf{true} \quad &\Longrightarrow \quad
    \mathsf{cmp}(x', y')
  \end{cases}
\end{cases}
\end{align*}

Then, to use our random bitstream $s$ to return a Boolean value which is true with probability $p$, we need only compute the comparison $\mathsf{cmp}(p, s) : \bool_\bot$. The issue, which is indicated by the return type of this comparison, is that the comparison doesn't necessarily terminate. What if it happens to be that $p = s$? Then we are in a rut.

Fortunately, this \emph{isn't} the case. While, in our situation, $p : \Stream(\bool)$ is a point of the space, $s \leftarrow \mu_R$ is \emph{not} a point. That's because $\mu_R$ is non-atomic, which means that for any \emph{global point} $p$ of $\Stream(\bool)$,
\[
\mu_R(\cdot \neq p) = \mu_R(\top) = 1.
\]
That is, for any point $p$, $s$ is \emph{not} $p$ (with probability 1).

\cite{simpson2012} defines the ``locale of random sequences'' for a given measure $\mu$, which satisfy all measure-1 properties of that measure. By the previous reasoning, these spaces must not have any points. However, they still have computational structure, and I would like to tentatively argue in this note, that we can avoid dealing with reasoning about termination of functions like $\mathsf{cmp}$ defined on $\Stream(\bool)$ by using that structure. Instead of dealing with $\Stream(\bool)$, we use a subspace of it, called $\Stream(\bool)_{\mu_R}$, which is defined by the nucleus [refer to nLab for definition]
\[
U \mapsto \bigcup \left\{ V \suchthat U \subseteq V, \mu_R(U) = \mu_R(V) \right\},
\]
so that instead we would have for every \emph{global} point $p : \Stream(\bool)$,
\footnote{There are likely predicativity issues here, since there are more and more such global points as you increase the universe level of the ``predicative locale'' which these are points of. This is likely related to the predicativity issues of the double negation sublocale.}
\[
\mathsf{cmp}_p : \Stream(\bool)_{\mu_R} \to \bool.
\]
This in fact defines a valid nucleus. It wasn't clear to me that it preserves meets, so I emailed Antonin, and he provided a very nice explanation why it does in fact preserve meets.
\footnote{Why can't you have 
\[
\mathsf{cmp} :  \Stream(\bool) \times \Stream(\bool)_{\mu_R} \to \bool?
\]
Well, we have the mono $i_{\mu_R} : \Stream(\bool)_{\mu_R} \rightarrowtail \Stream(\bool)$, and imagining $s \leftarrow \mu_R$, we could then compute
\[
\mathsf{cmp}(i_{\mu_R}(s), s),
\]
which we know never terminates. The fact has to be that one input should be a global point, and the other must be random from a non-atomic probability distribution.}

Writing this program seems pointless, because as it turns out, the space $\Stream(\bool)_{\mu_R}$ doesn't have any points, since $\mu_R$ is non-atomic. So it seems like we can't ever run $\mathsf{cmp}$. But this isn't really the case: the random stream $s \leftarrow \mu_R$, which is perhaps pulling from \texttt{/dev/random}, while certainly not a \emph{point} of $\Stream(\bool)_{\mu_R}$ (after all, this space has no points), implements the (seemingly-impossible) computational \emph{interface} for $\Stream(\bool)_{\mu_R}$.

At least, it does so with probability 1. My point is that using doubly-negated spaces and probability distributions over them, gives a useful formalism for not having to reason about probability 1 termination. All of capacity for non-termination is localized in the ``API'' interface for the random stream $s \leftarrow \mu_R$. In $\Stream(\bool)_{\mu_R}$, we have the cover
\[
\top_{\Stream(\bool)_{\mu_R}} \subseteq
  \bigcup_{n : \nat} [n \mapsto \mathsf{true}],
\]
which in English says that every $\Stream(\bool)$ drawn from $\mu_R$ eventually has a $\mathsf{true}$ somewhere in its sequence. This is of course missing the stream which is always $\mathsf{false}$, but that's all its missing, and because it occurs with probability 0 under $\mu_R$ we can neglect it.

The above cover has an obvious computational interpretation, let's say for our random stream $s \leftarrow \mu_R$. We must be able to \emph{compute} some index $n$ such that the $n$th element is $\mathsf{true}$. This might take a long time, potentially, but with probability 1, it is finite.

There's some philosophical question to be asked: certainly my random stream is \emph{some} stream, so if I happened to write a program that compares the random stream with another stream which happens to be the same exact one. And then it wouldn't terminate. But if we're waiting a long time, it could just be that we're impatient, and we need to wait longer. So even if you did manage to miraculously ``hit some probability 0 event'' in some sense, there's no way to be sure.

\subsection{Reestablishing decidability}

When I tell people that all functions in \contpl{} must be continuous, they get worried. They fret that they can't write a step function, or make a decision over a continuous variable. It may seem particularly worrying when it comes to dealing with probability, where it is only possible to compute the probability of an event if the event is decidable (i.e., clopen). On $\R$, there are no non-trivial open sets, so it seems that computing with probability distributions on $\R$ is a lost cause, if one can't compute the probability of any nontrivial event.

Computing these probabilities is hard for a reason. Suppose we have a distribution $\mu : \Prob(\R)$ and want to compute the probability of the open predicate $\cdot > 0$. The probability $\mu(\cdot > 0)$ is a lower real number, since $\cdot > 0$ is open, which is not useful for computation. It is necessarily hard to upper-bound $\mu(\cdot > 0)$. Suppose that $\mu = \delta(x)$, the Dirac delta distribution which has all its mass at a point $x$. Then $\mu(\cdot > 0) = 1$ if and only if $x > 0$, which is a Sierp\'inski-valued proposition, meaning that it is affirmable, but not refutable. To compute the measure of $\cdot > 0$ as a real number, we'd need to be able to compare $x$ with 0, which is not a computable (continuous) operation.

There are a few things we could do. Rather than attempting to compute the probability of an open set, we can compute the approximate probability of a binary cover of $\R$.\footnote{Binary covers are defined in another note.} Given a binary cover $(P, Q)$ of $\R$, that is, $P, Q : \Open{\R}$ and $\R \subseteq P \cup Q$, we can non-deterministically compute two real numbers, $x_P, x_Q : \R$ such that $x_P + x_Q = 1$ and $x_P \le \mu(P)$ and $x_Q \le \mu(Q)$. That is, we can split up the weight of $\mu$ into $P$ and $Q$, non-deterministically assigning any weight in $P \cap Q$ to either $x_P$ or $x_Q$.

For instance, for our predicate $\cdot > 0$, we might define a binary cover $(\cdot > 0)_\varepsilon : \R \to \mathsf{BCover}$ for any approximation tolerance $\varepsilon : \rat^+$, where
\begin{align*}
\mathsf{Left}^{-1}((\cdot > 0)_\varepsilon) &\triangleq \cdot > 0
\\ \mathsf{Right}^{-1}((\cdot > 0)_\varepsilon) &\triangleq \cdot < \varepsilon.
\end{align*}

Then, when we non-deterministically compute the probability of the $\mathsf{Left}$ and $\mathsf{Right}$ sides, the weight assigned to the $\mathsf{Left}$ side will be at most $\mu(\cdot > 0)$, the ``actual'' probability of the open $\cdot > 0$.

But this still seems unsatisfactory. If one cannot compute, \emph{exactly}, the probability that some normal distribution lies in an open interval (or \emph{any} non-trivial event), when there is clearly no theoretical obstacle to doing so, that would be a problem. There is a substantial difference between probability distributions such as Dirac deltas and normal distributions, and it is beneficial to treat them as two different objects.

Normal distributions are non-atomic, in the sense for any normal distribution $\mu$ and any \emph{global} point $p : \R$, $\mu(\cdot \neq p) = \mu(\top) = 1$. Therefore, normal distributions also give probability distributions over some subspace which has no points, which we'll call $\R_\mathcal{N}$. And while $\R_\mathcal{N}$ has no points, its space of probability distributions $\Prob\left(\R_\mathcal{N}\right)$ certainly does, since there is an obvious map of open sets $j_\mathcal{N} : \Open{\R} \to \Open{\R_\mathcal{N}}$ which is well-behaved and accordingly the map
\begin{align*}
j_\mathcal{N}^* &: \Prob\left(\R_\mathcal{N}\right) \to \Prob(\R)
\\ j_\mathcal{N}^*(\mu)(U) &\triangleq \mu(j_\mathcal{N}(U))
\end{align*}
is well-defined.

In $R_\mathcal{N}$, there is a wealth of decidable propositions (i.e., clopens), meaning that it is easy to compute the probability of many different events of $R_\mathbb{N}$. For instance, our predicate $\cdot > 0$ is now clopen! We have the cover
\[
\R_{\mathcal{N}} \subseteq (\cdot > 0) \cup (\cdot < 0),
\]
since for any normal distribution $\mu$,
\[
\mu\left((\cdot > 0) \cup (\cdot < 0)\right) = \mu(\R) = 1.
\]
Note that the covering for $\R_\mathcal{N}$ is non-trivial, even though $\R_\mathcal{N}$ has no points; even though I am using subset-like notation such as $\subseteq$ and $\cup$, these operations \emph{cannot} be interpreted as operations on subsets. Unlike sets, where all empty sets are isomorphic, two spaces without points are not necessarily homeomorphic to each other.

Since $\cdot > 0$ is clopen, this means that for any probability distribution $\mu : \Prob\left(\R_\mathcal{N}\right)$, we can compute the probabilities $\mu(\cdot > 0)$ and $\mu(\cdot < 0)$, and know that their sum is exactly 1. Many operations impossible on $\R$ are newly possible on $\R_\mathcal{N}$. 

We can compute floors with a pattern match with infinitely many cases:
\begin{align*}
\lfloor \cdot \rfloor &: \R_\mathcal{N} \to \nat
\\ \lfloor x \rfloor &\triangleq \mathsf{cases}(x)
\begin{cases}
[n : \nat] \quad n < \cdot < n + 1
  \qquad \Longrightarrow \qquad
  n
\end{cases}
\end{align*}
This pattern match is well-defined, since there is indeed the cover
\[
\R_\mathcal{N} \subseteq \bigcup_{n : \nat} (n < \cdot < n + 1),
\]
because we have that for any normal distribution $\mu$,
\[
\mu \left( \bigcup_{n : \nat} (n - 1 < \cdot < n + 1) \right) = \mu(\R) = 1.
\]

Continuous maps whose domains are $R_\mathcal{N}$ may not be able to run on points, but they can be useful in other ways: for instance, they can be integrated against certain probability distributions (distributions on $\R_\mathcal{N}$), or computed on samples from such distributions, which are not points but ``lawless sequences'' in some sense. Also, we are able to condition on decidable predicates (whose probability is more than 0): that is, given a space $A$ and probability distribution $\mu : \Prob(A)$, if $U : \Open{A}$ is clopen and satisfies $\mu(U) > 0$, then we can compute a probability distribution $\mu(\cdot \suchthat U) : \Prob(\{A \suchthat U \})$, whose measure is defined by the usual equation
\[
\mu(P \suchthat U) \triangleq \frac{1}{\mu(U)} \mu(P \cap U).
\]
We note that the right-hand side is indeed a lower real number, as it is required to be: since $\mu(U)$ is a real number greater than zero, so is $\frac{1}{\mu(U)}$, and $\mu(P \cap U)$ is a non-negative lower-real number, and multiplying a positive real number by a non-negative lower-real gives a non-negative lower real number.

Therefore, for instance, we could compute a conditional probability distribution of the standard normal distribution, given the observation $\cdot < 0$.

\subsection{Products}

How does producing measure-1 subspaces interact with products? Suppose I have have probability distributions $\mu_A : A_{\mu_A}$ and $\mu_B : B_{\mu_B}$. That is, both probability distributions are restricted to their smallest measure-1 subspace. There should be a continuous map, which I believe is mono,
\[f : (A \times B)_{\mu_A \otimes \mu_B} \to A_{\mu_A} \times B_{\mu_B}.\]
Does this map have a continuous inverse? That is, are these spaces homeomorphic?

\subsection{Predicativity worries}
All the statements which I'm making should be valid in an impredicative sense. But I'm worried about how to actually define the smallest measure-1 subspaces in a computational (predicative) way. For doubly-negated spaces, which are somewhat similar, I should cite some references which indicate that doubly-negated spaces \emph{cannot} be inductively generated formal topologies, at least in some cases I think.

The fact that I'm now fairly confident that I want to be able to have these measure-1 subspaces in \contpl{} means that I might need to reconsider using inductively generated formal topologies as \emph{the} main setting for everything.

\subsection{More...}

[[Partial samplers become total since they terminate with probability 1 - this is something that *really* bothers probabilistic semantics people, I should make this a key argument ]]
{'fraction_non_alphanumeric': 0.115527451570812, 'fraction_numerical': 0.004449797584395597, 'mean_word_length': 4.0721194637705755, 'pattern_counts': {'":': 0, '<': 26, '<?xml version=': 0, '>': 44, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '947423', 'n_tokens_mistral': 8613, 'n_tokens_neox': 8183, 'n_words': 4253}