#  $\omega$PAP Spaces: Reasoning Denotationally About Higher-Order, Recursive
Probabilistic and Differentiable Programs

Mathieu Huot∗, Alexander K. Lew∗, Vikash K. Mansinghka, and Sam Staton

###### Abstract

We introduce a new setting, the category of $\omega$PAP spaces, for reasoning
denotationally about expressive differentiable and probabilistic programming
languages. Our semantics is general enough to assign meanings to most
practical probabilistic and differentiable programs, including those that use
general recursion, higher-order functions, discontinuous primitives, and both
discrete and continuous sampling. But crucially, it is also specific enough to
exclude many pathological denotations, enabling us to establish new results
about both deterministic differentiable programs and probabilistic programs.
In the deterministic setting, we prove very general correctness theorems for
automatic differentiation and its use within gradient descent. In the
probabilistic setting, we establish the almost-everywhere differentiability of
probabilistic programs’ trace density functions, and the existence of
convenient base measures for density computation in Monte Carlo inference. In
some cases these results were previously known, but required detailed proofs
with an operational flavor; by contrast, all our proofs work directly with
programs’ denotations.

11footnotetext:  Equal contribution

##  I Introduction

This paper introduces a new setting, the category of $\omega$PAP spaces, for
reasoning denotationally about expressive probabilistic and differentiable
programs, and demonstrates its utility in several applications. The
$\omega$PAP spaces are built using the same categorical machinery [1] that
underlies the $\omega$-quasi-Borel spaces [2] and the $\omega$-diffeological-
spaces [3, 4], two other recent proposals for understanding higher-order,
recursive probabilistic and differentiable programs. The key difference is
that instead of taking the measurable maps (as in $\omega$Qbs) or the smooth
maps (as in $\omega$Diff) as the primitives in our development, we instead use
the functions that are piecewise analytic under analytic partition, or PAP
[5].

Whereas the smooth functions exclude many primitives used in practice (e.g.,
$<\,:\mathbf{real}\to\mathbf{real}\to\mathbb{B}$), and the measurable
functions admit many pathological examples from analysis (the Cantor function,
the Weierstrass function, space-filling curves), the PAP functions manage to
exhibit very few pathologies while still including nearly all primitives
exposed by today’s differentiable and probabilistic programming languages. As
a result, our semantics can interpret most differentiable and probabilistic
programs that arise in practice, and can be used to provide short denotational
proofs of many interesting properties. As evidence for this claim, we use our
semantics to establish new results (and give new, simplified proofs of old
results) about the correctness of automatic differentiation, the convergence
of automatic-differentiation gradient descent, and the supports and densities
of recursive probabilistic programs.

###  I-A A “Just-Specific-Enough” Semantic Model

In denotational accounts of deterministic and probabilistic programming
languages, deterministic programs typically denote functions and probabilistic
programs typically denote measure kernels. But what kinds of functions and
kernels?

The more specific our answer to that question, the more we can hope to
prove—purely denotationally—about our languages. For example, consider the
question of commutativity: is it the case that, whenever $x$ does not occur
free in $s$,

$\llbracket\mathbf{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}{let}}~{}x=t~{}\mathbf{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}{in}}~{}\mathbf{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}{let}}~{}y=s~{}\mathbf{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}{in}}~{}u\rrbracket=\llbracket\mathbf{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}{let}}~{}y=s~{}\mathbf{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}{in}}~{}\mathbf{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}{let}}~{}x=t~{}\mathbf{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}{in}}~{}u\rrbracket?$

In the probabilistic setting, this amounts to asking whether iterated
integrals can always be reordered. If our semantics interprets programs as
arbitrary measure kernels, then there is no obvious answer, because Fubini’s
theorem, which justifies the interchange of iterated integrals, does not apply
unconditionally. But by interpreting an expressive probabilistic language
using only the s-finite kernels, Staton [6] was able to prove commutativity
denotationally, using the specialization of Fubini’s theorem to the s-finite
case.

Unfortunately, in the quest for semantic models with convenient properties, we
may end up excluding programs that programmers might write in practice. For
example, in [3], all programs are interpreted as smooth functions, enabling an
elegant semantic account of why automatic differentiation algorithms work
(even in the presence of higher-order functions). But to achieve this nice
theory, all non-smooth primitives (including, e.g., the function $\lambda
x.\lambda y.x<y$) were excluded from the language under consideration. As a
result, the theory has little to say about the behavior of automatic
differentiation on non-smooth programs.

In this work, our aim is to find a “just specific enough” semantic model of
expressive probabilistic and differentiable programming languages: specific
enough to establish interesting properties via denotational reasoning, but
general enough to include nearly all programs of practical interest. Like the
recently introduced quasi-Borel predomains [2], our model covers most
probabilistic and differentiable programs that can be expressed in today’s
popular languages: it supports general recursion, higher-order functions,
discrete and continuous sampling, and a broad class of primitive functions
that includes nearly all the mathematical operations exposed by comprehensive
libraries for scientific computing and machine learning (such as numpy and
scipy). But crucially, it also excludes many pathological functions and
kernels that cannot be directly implemented in practice, such as the
characteristic function of the Cantor set (whose construction involves an
infinite limit that programs cannot compute in finite time). As a result, it
is often possible to establish that a desirable property holds of all
$\omega$PAP maps between two spaces, and to then conclude that it holds of all
programs of the appropriate type, without reasoning inductively about their
construction or their operational semantics.

The starting point in our search for a semantic model is Lee et al. [5]’s
notion of piecewise analyticity under analytic partition (or PAP). The PAP
functions are a particularly well-behaved subset of the functions between
Euclidean spaces, and [5] makes a compelling argument that they are “specific
enough” in the sense we describe above. For example, even though they are not
necessarily differentiable, PAP functions admit a generalized notion of
derivative, as well as a generalized chain rule that can be used to give a
denotational justification of automatic differentiation. These nice properties
do not hold for slight generalizations of PAP, e.g. the class of almost-
everywhere differentiable functions.

Nevertheless, a reasonable worry is that PAP functions may be too narrow a
semantic domain: do all programs arising in practice really denote PAP
functions, or does the definition assume properties that not all programs
enjoy? Lee et al. [5] establish that in a first-order language with PAP
primitives and conditionals, all programs denote PAP functions. But real-world
programs use many additional features, such as higher-order functions, general
recursion, and probabilistic effects. In the presence of these features, do
terms of first-order type still denote PAP functions? Consider the program in
Fig. 1, for example: it uses recursion to define a partial function that
diverges on the $\frac{1}{3}$-Cantor set, and halts on its complement. But we
know that the (total) indicator function for the $\frac{1}{3}$-Cantor set is
not PAP. This may seem like reason to doubt that [5]’s proposal can be cleanly
extended to the general-recursive setting.

Figure 1: A program that diverges on the $\frac{1}{3}$-Cantor set, but halts
elsewhere in $(0,1)$. The characteristic function of the $\frac{1}{3}$-Cantor
set is not PAP, so a naively defined interpretation of “partial PAP functions
into $\mathbb{R}$” as PAP functions into $\mathbb{R}+1$ would not suffice to
interpret a language with general recursion. Our definition of partial
$\omega$PAP maps in Section II resolves the issue.

Fortunately, however, it can: in Section II, we extend the definition of PAP
to cover partial and higher-order functions. The resulting class of functions,
the $\omega$PAP maps, suffice to interpret all recursive, higher-order
programs in an expressive call-by-value PCF, with a type of real numbers and
PAP primitives (Theorem II.2). The $\omega$PAP category also supports a strong
monad of measures (Definition IV.5), enabling an interpretation of continuous
sampling and soft conditioning, features common in modern probabilistic
languages.

To be clear, existing semantic frameworks can interpret similarly expressive
languages (e.g., [2]). Our value proposition is that the $\omega$PAP domain
usefully excludes certain pathological denotations that other settings allow.
After defining our semantics in Section II, we devote the remainder of the
paper to presenting evidence for this claim: new results (and new proofs of
old results) that follow cleanly from denotational reasoning about $\omega$PAP
spaces and maps.

###  I-B Differentiable Programming and Automatic Differentiation

Our first application of our semantics is to the study of automatic
differentiation (AD), a family of techniques for mechanically computing
derivatives of user-defined functions. It has found widespread use in machine
learning and related disciplines, where practitioners are often interested in
using gradient-based optimization algorithms, such as gradient descent, to fit
model parameters to data. Languages with support for automatic differentiation
are often called “differentiable programming languages,” even if it may be the
case that some programs do not denote everywhere-differentiable functions.

When applied to straight-line programs built from differentiable primitives
(without
$\mathbf{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}{if}}$
statements, loops, and other control flow), AD has a straightforward
justification using the chain rule. But in the presence of more expressive
programming constructs, AD is harder to reason about: some programs encode
partial or non-differentiable functions, and even when programs are
differentiable, AD can fail to compute their true derivatives at some inputs.

Our $\omega$PAP semantics gives a clean account of the class of partial
functions that recursive, higher-order programs built from “AD-friendly”
primitives can express. In Section III, we use this characterization to
establish guarantees about AD’s behavior when applied to such programs:

  * •

We define a generalized notion of derivative, based on [5]’s intensional
derivatives, and establish that every first-order $\omega$PAP map is
intensionally differentiable.

  * •

We adapt Huot et al. [3]’s denotational correctness proof of AD to prove that
AD correctly computes intensional derivatives of all programs with first-order
type, even if they use recursion and discontinuous primitives (Theorem III.3).
This result is stronger than Mazza and Pagani [7]’s, which follows as a
straightforward corollary. But the main benefit over their development is the
simplicity of our proof, which mirrors Huot et al. [3]’s quite closely despite
the greatly increased complexity of our language.

  * •

Using this characterization of what AD computes, we further prove the novel
result that intensional gradient descent (which optimizes a differentiable
function but using gradients computed by AD) converges with probability 1, if
initialized with a randomized initial location and a randomized learning rate
(Theorem III.7). This implies that gradient descent can be safely applied to
recursive programs with conditionals so long as they denote differentiable
functions, even if AD (which can disagree with the true derivative at some
inputs) is used to compute gradients. Interestingly, if either the initial
location or the learning rate is not randomized, a.s.-convergence is not
guaranteed, and we present counterexamples of PyTorch programs that denote
differentiable functions but cause PyTorch’s gradient descent implementation
to diverge (Propositions III.5 & III.6).

Taken together, these results give a characterization of the behavior of AD in
real systems like PyTorch and Tensorflow, even when they are applied to non-
differentiable or recursive programs.

###  I-C Probabilistic Programming

Probabilistic programming languages extend deterministic languages with
support for random sampling and soft conditioning, making them an expressive
representation both for probability distributions and for general
(unnormalized) measures. Many probabilistic programs are intended to model
some aspect of the world, and many questions of interest can be posed as
questions about the expectations of certain functions under (normalized
versions of) these models. Probabilistic programming languages often come with
tools for automatically running inference algorithms that estimate such
posterior expectations. But the machinery for inference may make assumptions
about the programs the user has written—for example, that the program has a
density with respect to a well-behaved reference measure, or that its density
is differentiable. Our next application of our semantics is to the problem of
verifying that such properties hold for any program in an expressive
probabilistic language.

In Section IV, we extend the core language from Section II to include the
$\mathbf{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}{sample}}$
and
$\mathbf{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}{score}}$
commands. This requires changing our monad of effects, which in Section II
covered only divergence, to also interpret randomness and conditioning. We
consider two different strong monads on $\omega$PAP: one interprets
probabilistic programs as s-finite measures (following [2]), and the other as
weighted sampling procedures (following [8, 9]). In each case, we can prove
interesting properties of all probabilistic programs by working just with the
class of $\omega$PAP maps they denote:

  * •

Interpreting programs as weighted samplers, we prove that almost-surely
terminating probabilistic programs have almost-everywhere differentiable
weight functions (Theorem IV.1). This has been previously shown by Mak et al.
[9], but our proof is substantially simpler, with no need for [9]’s stochastic
symbolic execution technique. Our theorem is also slightly stronger, covering
some programs that do not almost surely halt, and ruling out some pathological
a.e.-differentiable weight functions.

  * •

Interpreting probabilistic programs as $\omega$PAP measures, we prove that all
programs of type $\mathbb{R}^{n}$ denote distributions supported on a
countable union of smooth submanifolds of $\mathbb{R}^{n}$, and thus admit
convenient densities with respect to a particular class of reference measures
(Theorem IV.3).

Besides being interesting in their own right, these results have consequences
for the practical design and implementation of probabilistic programming
systems.

The first result is relevant to the application of gradient-based inference
algorithms, which often require (at least) almost-everywhere differentiability
to be sound.

The second result is relevant for the automatic computation of densities or
Radon-Nikodym derivatives of probabilistic programs, key ingredients in
higher-level algorithms such as importance sampling and MCMC. To see why,
suppose a user has constructed two closed probabilistic programs of type
$\mathbb{R}^{n}$, $p$ and $q$, and wishes to use $q$ as an importance sampling
proposal for $p$. If $\llbracket p\rrbracket$ is absolutely continuous with
respect to $\llbracket q\rrbracket$ ($\llbracket p\rrbracket\ll\llbracket
q\rrbracket$), such an importance sampler does exist, but implementing it
requires computing importance weights: at a point $x\sim\llbracket
q\rrbracket$, we must compute $\frac{d\llbracket p\rrbracket}{d\llbracket
q\rrbracket}(x)$. If $\llbracket p\rrbracket$ and $\llbracket q\rrbracket$
were both absolutely continuous with respect to the Lebesgue measure on
$\mathbb{R}^{n}$, we could compute probability density functions $\rho_{p}$
and $\rho_{q}$ for $\llbracket p\rrbracket$ and $\llbracket q\rrbracket$
respectively, and then compute the importance weight as the ratio of these
densities. But not all programs denote measures that have densities with
respect to the Lebesgue measure.111Consider, e.g., the program that samples
$u\sim\textit{Unif}(0,1)$, and returns $(u,u)\in\mathbb{R}^{2}$. Because it is
supported only on a 1-dimensional line segment within the plane, it has no
density function with respect to the Lebesgue measure in the plane. That is,
there is no nonnegative function $\rho$ such that the probability of an event
$E\subseteq\mathbb{R}^{2}$ is equal to
$\iint_{\mathbb{R}^{2}}1_{E}(x,y)\cdot\rho(x,y)dxdy$. Our result gives us an
alternative to the Lebesgue measure: we can compute the density of $\llbracket
p\rrbracket$ (and $\llbracket q\rrbracket$) with respect to the Hausdorff
measures over the manifolds on which they are supported. (Indeed, computing
densities with respect to Hausdorff measures has previously been proposed by
Radul and Alexeev [10]; our result is that, unlike the Lebesgue base measure,
this choice does not exclude any possible programs a user might write, because
every program is absolutely continuous with respect to such a base measure.)

###  I-D Summary

  * •

We present the category of $\omega$PAP spaces (Section II), a new setting
suitable for a denotational treatment of higher-order, recursive
differentiable or probabilistic programming languages. It supports sound and
adequate semantics of a call-by-value PCF with a type of real numbers and a
very expressive class of primitives.

  * •

To demonstrate that our semantics enables denotational reasoning about a broad
class of interesting program properties, we present new results (and new,
much-simplified proofs of old results) about differentiable (Section III) and
probabilistic (Section IV) programs.

##  II $\omega$PAP Semantics

This section develops the $\omega\text{PAP}{}$ spaces, and shows how to use
them to interpret a higher-order, recursive language with conditionals and
discontinuous primitives. Our starting point is [5]’s definition of piecewise
analyticity under analytic partition (PAP), a property of some functions
defined on Euclidean spaces. The $\omega\text{PAP}{}$ construction
significantly extends Lee et al. [5]’s definition to cover partial and higher-
order functions between Euclidean or other spaces. The $\omega\text{PAP}{}$
setting is general enough to interpret almost all primitives encountered in
practice, but restricted enough to allow precise denotational reasoning.

###  II-A $\omega$PAP Spaces

We first recall a standard definition from analysis:

######  Definition II.1 (analytic function).

If the Taylor series of a smooth function $f:U\to V$ (for
$U\subseteq\mathbb{R}^{n},V\subseteq\mathbb{R}^{m}$) converges pointwise to
$f$ in a neighborhood around $x$, we say $f$ is analytic at $x$. An analytic
function is a function that is analytic at every point in its domain.

When a subset of $\mathbb{R}^{n}$ can be carved out by finitely many analytic
inequalities, we call it an analytic set, following Lee et al. [5]. We call
countable unions of such sets c-analytic.

######  Definition II.2 (analytic set [5]).

We call a set $A\subseteq\mathbb{R}^{n}$ an analytic set if there exists a
finite collection $\\{g_{i}\\}_{i\in I}$ of analytic functions into
$\mathbb{R}$, with open domain $U\subseteq\mathbb{R}^{n}$, such that

$A=\\{x\in U\mid\forall i\in I.g_{i}(x)\leq 0\\}.$

######  Definition II.3 (c-analytic set).

A set $A\subseteq\mathbb{R}^{n}$ is c-analytic if it is a countable union of
analytic subsets of $\mathbb{R}^{n}$.

Lee et al. [5]’s key definition was the class of PAP functions, which are
piecewise analytic:

######  Definition II.4 (PAP function [5]).

For $U\subseteq\mathbb{R}^{n}$ c-analytic and $V$ any subset of
$\mathbb{R}^{m}$, we say $f:U\to V$ is piecewise analytic under analytic
partition (PAP) if there exists a countable family $\\{(A_{i},f_{i})\\}_{i\in
I}$ such that:

  1. 1.

the sets $A_{i}$ are analytic and form a partition of $U$;

  2. 2.

each ${f_{i}:U_{i}\to\mathbb{R}^{m}}$ is an analytic function defined on an
open domain $U_{i}\supseteq A_{i}$;

  3. 3.

when $x\in A_{i}$, $f_{i}(x)=f(x)$.

In our development, PAP functions will play, at first order, the role that
smooth functions play in the construction of diffeological spaces [11], and
that measurable functions play in the construction of quasi-Borel spaces [12].
The change to PAP is essential: many primitives exposed by languages like
TensorFlow and PyTorch fail to be smooth at some inputs, but virtually none
fail to be PAP. And while PAP functions are all measurable, they helpfully
exclude many pathological measurable functions, making it possible to prove
stronger results through denotational reasoning.

The development that follows generalizes PAP functions, so that we can talk
about higher-order and partial PAP functions. To do so, it uses recently
developed categorical techniques [2, 4, 1] (see Appendix B for details).

######  Definition II.5 ($\omega$PAP space).

An $\omega$PAP space is a triple $(|X|,\mathcal{P}_{X},\leq_{X})$, where
$(|X|,\leq)$ is an $\omega cpo{}$ and $\mathcal{P}_{X}$ is a family of sets of
functions, called plots in $X$. For each c-analytic set $A$, we have
$\mathcal{P}_{X}^{A}\subseteq|X|^{A}$. Plots have to satisfy the following
closure conditions:

  * •

Every map from the one point of $\mathbb{R}^{0}$ to $|X|$ is a plot in $X$.

  * •

If $\phi\in|X|^{A}$ is a plot in $X$ and $f:A^{\prime}\to A$ is a PAP function
between c-analytic sets $A^{\prime}$ and $A$, then $\phi\circ f$ is a plot in
$X$.

  * •

Suppose the c-analytic sets $A_{j}\subseteq A$ form a countable partition of
the c-analytic set $A$, with inclusions $i_{j}:A_{j}\to A$. If
$\phi\circ{i_{j}}$ is a plot in $X$ for every $j$, then $\phi$ is a plot in
$X$.

  * •

Whenever $(\alpha_{i})_{i}$ is an $\omega$-chain in $\mathcal{P}^{A}_{X}$
under the pointwise order,
$(\bigvee_{i}\alpha_{i})(x):=\bigvee_{i}(\alpha_{i}(x))$ defines a plot
$\bigvee_{i}\alpha_{i}\in\mathcal{P}_{X}^{A}$.

######  Definition II.6 ($\omega\text{PAP}{}$ map).

An $\omega$PAP map $f:X\to Y$ is a Scott-continuous function between the
underlying $\omega cpo{}$s $(|X|,\leq_{X})$ and $(|Y|,\leq_{Y})$, such that
for every plot $\phi\in\mathcal{P}_{X}^{A}$,
$f\circ\phi\in\mathcal{P}_{Y}^{A}$.

We now look at several examples of $\omega\text{PAP}{}$-spaces. Our first
example establishes that PAP functions between Euclidean spaces are a special
case of $\omega\text{PAP}{}$ maps.

######  Example II.1.

Any c-analytic set $A$ (including, e.g., $\mathbb{R}^{n}$ itself) can be given
the structure of an $\omega$PAP-space $(A,\mathcal{P}_{A},=)$ where for every
c-analytic set $C$, the plots $\mathcal{P}_{A}^{C}$ are given by

$\mathcal{P}_{A}^{C}:=\\{f:C\to A~{}\mid~{}f\text{ is a PAP function}\\}.$

Next, we construct products, coproducts, and exponential $\omega\text{PAP}{}$
spaces, which will be useful for interpreting the tuples, sums, and function
types of our language.

######  Example II.2 (Products).

Given $\omega\text{PAP}$ spaces $X$ and $Y$, define $X\times Y$ to be their
product as $\omega cpo{}$’s, with plots $\langle
f,g\rangle\in\mathcal{P}^{A}_{X\times Y}$ whenever $f\in\mathcal{P}^{A}_{X}$
and $g\in\mathcal{P}^{A}_{Y}$.

More generally, given $\omega\text{PAP}$ spaces $X_{i}$ for $i\in I$, we can
define $\prod_{i\in I}X_{i}$ by their product as $\omega cpo{}$s, with plots
$f\in\mathcal{P}_{\prod_{i\in I}X_{i}}^{A}$ whenever each projection
$\pi_{i}\circ f\in\mathcal{P}_{X_{i}}^{A}$.

######  Example II.3 (Coproducts).

Let $I$ be a countable index set, and $X_{i}$ a $\omega\text{PAP}$ space for
each $i\in I$. Then $\bigsqcup_{i}X_{i}$ is again an $\omega\text{PAP}$ space,
with carrier set $\bigsqcup_{i}|X_{i}|$, and the partial order inherited from
each $X_{i}$ (elements of different spaces $X_{i}$ and $X_{j}$ are not
comparable). A function $f:A\to\bigsqcup_{i}|X_{i}|$ is a plot if there exists
a countable partition $\\{A_{j}\\}_{j}$ of $A$ into c-analytic sets, such that
for each $j$, there is a plot $f_{j}:A_{j}\to X_{k_{j}}$, where $k_{j}\in I$,
such that on $A_{j}$, $f(x)=\mathbf{in}_{k_{j}}f_{j}(x)$, i.e., if the
preimage of each $X_{i}$ under $f$ is a c-analytic set for each $i$.

######  Example II.4 (Exponentials).

Let $X$ and $Y$ be $\omega\text{PAP}$ spaces. Then $X\Rightarrow Y$ is again a
$\omega\text{PAP}{}$ space, with carrier set $\omega\text{PAP}{}(X,Y)$, the
set of $\omega\text{PAP}{}$-morphisms from $X$ to $Y$. $f\leq_{X\Rightarrow
Y}g$ iff for all $x$, $f(x)\leq_{Y}g(x)$. A function $f:A\to|X\Rightarrow Y|$
is a plot if $\mathbf{uncurry}\,f:A\times X\to Y$ is an $\omega\text{PAP}$
morphism.

###  II-B Core Calculus

We present our core calculus in Figure 2. It is a simple call-by-value variant
of PCF (e.g. as in Abramsky and McCusker [13]), with a ground type
$\mathbb{B}$ for Booleans, and a ground type $\mathbf{real}$ for real numbers.
It parametrized by a set of primitives $f$ representing PAP functions. They
typically include analytic functions such as $+,*,\exp,\tan$ and comparison
operators such as $>,=$. The language also includes constants $\underline{c}$
for each real $c$ and
$\mathbf{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}{true}},\mathbf{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}{false}}$
for Booleans. The typing rules and operational semantics are standard, and
given in Appendices A-A and A-B.

$\begin{array}[t]{l@{\quad\\!\\!}*3{l@{}}@{\,}l}{\tau}&::=&&\mspace{-25.0mu}\quad\text{types}\\\
&\mathrel{\lvert}&\mathbf{real}&\quad\text{real numbers}\\\
&\mathrel{\lvert}&\mathbb{B}&\quad\text{booleans}\\\
&\mathrel{\lvert}&{\tau}_{1}\times{\tau}_{2}&\quad\text{product}\\\
&\mathrel{\lvert}&{\tau}_{1}\to{\tau}_{2}&\quad\text{function}\end{array}$
$\begin{array}[t]{l@{\quad\\!\\!}*3{l@{}}@{\,}l}{t}&::=&&\mspace{-25.0mu}\quad\text{terms}\\\
&\mathrel{\lvert}&x&\quad\text{variable}\\\ &\mathrel{\lvert}&\underline{c}\
\mathrel{\lvert}f({t}_{1},\ldots,{t}_{n})&\quad\text{constants/operations}\\\
&\mathrel{\lvert}&\langle{t}_{1},{t}_{2}\rangle&\quad\text{pair
constructor}\\\
&\mathrel{\lvert}&\mathbf{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}{case}}\,{t}_{1}\,\mathbf{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}{of}}\,\langle
x_{1},x_{2}\rangle\to{t}_{2}&\quad\text{pair eliminiation}\\\
&\mathrel{\lvert}&\mathbf{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}{if}}~{}{t}_{1}~{}\mathbf{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}{then}}~{}{t}_{2}~{}\mathbf{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}{else}}~{}{t}_{3}&\quad\text{conditionals}\\\
&\mathrel{\lvert}&\lambda x.{t}\ \mathrel{\lvert}{t}\,{s}&\quad\text{function
abstraction/app.}\\\ &\mathrel{\lvert}&\mu f.\lambda
x.{t}&\quad\text{recursive function}\\\ \end{array}$

Figure 2: Types and terms of our language

###  II-C Denotational semantics

We give a denotational semantics to our language using $\omega\text{PAP}{}$
spaces and maps. A program $\Gamma\vdash{t}:{\tau}$ is interpreted as an
$\omega\text{PAP}{}$ map
$\llbracket{t}\rrbracket:\llbracket\Gamma\rrbracket\to\mathbf{L}\llbracket{\tau}\rrbracket$,
for a suitable partiality monad $\mathbf{L}$ that we now define.

Given an $\omega$PAP space $Y$, we define the $\omega$PAP space $\mathbf{L}Y$
as follows.

  * •

The underlying set is $|\mathbf{L}Y|:=|Y|\sqcup\\{\bot\\}$.

  * •

The order structure is given by $\forall x\in|Y|,\bot\leq_{LY}x$ and $\forall
x,x^{\prime}\in|Y|,x\leq_{LY}x^{\prime}$ iff $x\leq_{Y}x^{\prime}$.

  * •

Plots are given by

$\displaystyle\mathcal{P}_{\mathbf{L}Y}^{A}$
$\displaystyle:=\\{g:|A|\to|Y|\sqcup\\{\bot\\}~{}|~{}\exists B\subseteq
A~{}\text{c-analytic};$ $\displaystyle\qquad\quad
g^{-1}(|Y|)=Im(|B|)~{}and~{}g|_{Im(|B|)}\in\mathcal{P}_{Y}^{B}\\}$

The intuition for $\mathcal{P}_{\mathbf{L}Y}^{A}$ is that the partial
$\omega\text{PAP}{}$ maps from Euclidean space into $Y$ are defined on
c-analytic sets of inputs, but the region on which they are not defined need
not satisfy any special property. This is how we account for the example from
Fig. 1; although it is undefined on the $\frac{1}{3}$-Cantor set (which is not
c-analytic), its domain (the complement of the $\frac{1}{3}$-Cantor set) is
c-analytic.

We also have (natural) $\omega\text{PAP}{}$-morphisms, that we can write using
lambda-calculus notation as

  * •

$\mathbf{return}_{X}:X\to\mathbf{L}X$ given by $\lambda x.\mathbf{inl}~{}x$

  * •

$\mathop{\gg\mkern-10.0mu\scalebox{1.0}[1.0]{=}}_{X,Y}:\mathbf{L}X\times(X\Rightarrow\mathbf{L}Y)\to\mathbf{L}Y$
given by
$\lambda(x,g).\mathbf{match}\,x\,\mathbf{with}\,\mathbf{inr}\,\bot\mapsto\mathbf{inr}\,\bot,\,\mathbf{inl}\,x\mapsto
g(x)$

where $\mathbf{inl},\mathbf{inr}$ are respectively left and right injections
(as set functions, they are not $\omega\text{PAP}{}$-morphisms).

$\mathbf{L}$ extends to $\omega$PAP maps $f:X\to Y$ by setting
$\mathbf{L}f:\mathbf{L}X\to\mathbf{L}Y$ to equal $\mathbf{inl}\circ f$ on all
inputs $\mathbf{inl}~{}x$ and setting
$\mathbf{L}f(\mathbf{inr}~{}\bot)=\mathbf{inr}~{}\bot$. This definition is
inspired by similar constructs present in [2, 4]. Overall,
$(\mathbf{L},\mathbf{return},\mathop{\gg\mkern-10.0mu\scalebox{1.0}[1.0]{=}})$
forms a (commutative) monad.

######  Proposition II.1.

$(\mathbf{L},\mathbf{return},\mathop{\gg\mkern-10.0mu\scalebox{1.0}[1.0]{=}})$
is a (strong, commutative) monad on the category of
$\omega\text{PAP}{}$-spaces and morphisms.

We can now interpret types and terms of our language. The semantics of types
and terms is given in Figure 3. A context
$\Gamma=(x_{1}\colon{\tau}_{1},\dots,x_{n}\colon{\tau}_{n})$ is interpreted as
the product space
$\llbracket\Gamma\rrbracket\stackrel{{\scriptstyle\mathrm{def}}}{{=}}\prod_{i=1}^{n}\llbracket{\tau}_{i}\rrbracket$.
Substitution is given by the usual Kleisli composition of effectful programs,
as is standard for effectful functional languages [14].

$\begin{array}[]{lcl}\llbracket\mathbf{real}\rrbracket&\stackrel{{\scriptstyle\mathrm{def}}}{{=}}&(\mathbb{R},\mathcal{P}_{\mathbb{R}},=)\\\
\llbracket\mathbb{B}\rrbracket&\stackrel{{\scriptstyle\mathrm{def}}}{{=}}&(1+1,\mathcal{P}_{1+1},=)\\\
\llbracket\langle{\tau}_{1},{\tau}_{2}\rangle\rrbracket&\stackrel{{\scriptstyle\mathrm{def}}}{{=}}&\
\llbracket{\tau}_{1}\rrbracket\times\llbracket{\tau}_{2}\rrbracket\\\
\llbracket{\tau}_{1}\to{\tau}_{2}\rrbracket&\stackrel{{\scriptstyle\mathrm{def}}}{{=}}&\llbracket{\tau}_{1}\rrbracket\Rightarrow\mathbf{L}\llbracket{\tau}_{2}\rrbracket\end{array}$
$\begin{array}[]{lcl}\llbracket
x\rrbracket(\rho)&\stackrel{{\scriptstyle\mathrm{def}}}{{=}}&\mathbf{return}~{}\rho(x)\\\
\llbracket\underline{c}\rrbracket(\rho)&\stackrel{{\scriptstyle\mathrm{def}}}{{=}}&\mathbf{return}~{}c\\\
\llbracket
f({{t}_{1}}{\dots}{{t}_{n}})\rrbracket(\rho)&\stackrel{{\scriptstyle\mathrm{def}}}{{=}}&\llbracket{t}_{1}\rrbracket(\rho)\mathop{\gg\mkern-10.0mu\scalebox{1.0}[1.0]{=}}~{}(\lambda
x_{1}.\llbracket{t}_{2}\rrbracket(\rho)\\\
&&\quad\mathop{\gg\mkern-10.0mu\scalebox{1.0}[1.0]{=}}\ldots\mathop{\gg\mkern-10.0mu\scalebox{1.0}[1.0]{=}}~{}(\lambda
x_{n}.\\\ &&\quad f(x_{1},\ldots,x_{n})))\\\
\llbracket\langle{t}_{1},{t}_{2}\rangle\rrbracket(\rho)&\stackrel{{\scriptstyle\mathrm{def}}}{{=}}&\llbracket{t}_{1}\rrbracket(\rho)\mathop{\gg\mkern-10.0mu\scalebox{1.0}[1.0]{=}}~{}(\lambda
x.\llbracket{t}_{2}\rrbracket(\rho)\mathop{\gg\mkern-10.0mu\scalebox{1.0}[1.0]{=}}\\\
&&\quad(\lambda y.\mathbf{return}~{}(x,y)))\\\ \llbracket\lambda
x:{\tau}.{{t}}\rrbracket(\rho)&\stackrel{{\scriptstyle\mathrm{def}}}{{=}}&\mathbf{return}~{}\lambda
v.\llbracket{t}\rrbracket(\rho[x\mapsto v])\\\
\llbracket\mathbf{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}{case}}~{}{t}_{1}\mathbf{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}{of}}~{}\langle
x_{1},x_{2}\rangle&\stackrel{{\scriptstyle\mathrm{def}}}{{=}}&\llbracket{t}_{1}\rrbracket(\rho)\mathop{\gg\mkern-10.0mu\scalebox{1.0}[1.0]{=}}(\lambda
v.\llbracket{t}_{2}\rrbracket(\rho[x\mapsto v]))\\\
\quad\to{t}_{2}\rrbracket&&\\\
\llbracket{t}_{1}\,{t}_{2}\rrbracket(\rho)&\stackrel{{\scriptstyle\mathrm{def}}}{{=}}&\llbracket{t}_{1}\rrbracket(\rho)\mathop{\gg\mkern-10.0mu\scalebox{1.0}[1.0]{=}}(\lambda
f.\llbracket{t}_{2}\rrbracket(\rho)\mathop{\gg\mkern-10.0mu\scalebox{1.0}[1.0]{=}}~{}f)\\\
\llbracket\mathbf{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}{if}}~{}{t}_{1}\mathbf{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}{then}}~{}{t}_{2}&\stackrel{{\scriptstyle\mathrm{def}}}{{=}}&\llbracket{t}_{1}\rrbracket(\rho)\mathop{\gg\mkern-10.0mu\scalebox{1.0}[1.0]{=}}\lambda
b.\mathbf{if}~{}b~{}\mathbf{then}~{}\llbracket{t}_{2}\rrbracket(\rho)\\\
\quad\mathbf{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}{else}}~{}{t}_{3}\rrbracket(\rho)&&\quad\mathbf{else}~{}\llbracket{t}_{3}\rrbracket(\rho)\\\
\llbracket\mu f.\lambda
x.{t}\rrbracket(\rho)&\stackrel{{\scriptstyle\mathrm{def}}}{{=}}&\mathbf{return}~{}\bigvee_{i\in\mathbb{N}}f_{i}\end{array}$
where $f_{0}=\lambda x.\mathbf{inr}~{}\bot,f_{i+1}=\lambda
v.\llbracket{t}\rrbracket(\rho[f\mapsto f_{i},x\mapsto v])$

Figure 3: Denotational semantics of types and terms in $\omega\text{PAP}{}$.
Blue is used for syntax and bold for mathematical functions.

Our denotational semantics in $\omega\text{PAP}{}$ is sound and adequate
w.r.t. our (standard) operational semantics (Appendix A-B).

######  Theorem II.2.

The denotational semantics of our language is sound and adequate.

###### Proof sketch.

We show that $\omega\text{PAP}{}$ spaces and morphisms are a category of
$\omega$-concrete sheaves on a concrete site, as defined in Matache et al.
[1], and use their development. More details are given in Appendix B. ∎

##  III Reasoning about Differentiable Programs

Our first application of our semantics is to the problem of characterizing the
behavior of automatic differentiation on the terms of our language. Automatic
differentiation is a program transformation intended to convert programs
representing real-valued functions into programs representing their
derivatives. When all programs denote smooth functions, this informal
specification can easily be made precise; for example, Figure 4 illustrates
the correctness property that Huot et al. [3] prove for forward-mode AD in a
higher-order language with smooth primitives. Their proof is elegant and
compositional, relying on logical relations defined over the denotations of
open terms.

In our setting, not all programs denote smooth functions, and even when they
do, standard AD algorithms can return incorrect results, in ways that depend
on exactly how the smooth function in question was expressed as a program. For
example, Mazza and Pagani [7] define a program $\texttt{SillyId}=\lambda
x:\mathbb{R}.\mathbf{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}{if}}~{}x=0~{}\mathbf{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}{then}}~{}0~{}\mathbf{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}{else}}~{}x$,
that denotes the identity function (with derivative $\lambda x.1$), but for
which AD incorrectly computes a derivative of 0 when $x=0$. Because two
extensionally equal programs can have different derivatives as computed by AD,
it may seem unclear how any proof strategy based on Figure 4, relating the
syntactic operation of AD to the semantic operation of derivative-taking,
could apply. Indeed, in showing their correctness result for AD, Mazza and
Pagani [7] had to develop new operational techniques for reasoning about
derivatives of traces of recursive, branching programs.

Our $\omega$PAP semantics lets us take a different route, illustrated in
Figure 5. Like Huot et al. [3], we work directly with the denotations of
terms, which in our setting, are $\omega\text{PAP}{}$ maps. But we do not
attempt to assign a unique derivative to each $\omega\text{PAP}{}$ function;
instead, we define a relation on $\omega\text{PAP}{}$ maps that characterizes
when one is an intensional derivative [5] of another. Our correctness proof,
which follows exactly the structure of Huot et al. [3]’s, then establishes
that AD produces a program denoting an (not the) intensional derivative of the
original program’s denotation (Theorem III.3).

All $\omega$PAP maps have intensional derivatives, so there is no need to
restrict the correctness result to only the differentiable functions. But when
an $\omega$PAP map is differentiable in the standard sense, its intensional
derivatives agree almost everywhere with its true derivative. Thus, reasoning
denotationally, we are able to recover Mazza and Pagani [7]’s result: AD is
almost everywhere correct. Interestingly, this almost-everywhere correctness
result is not sufficient to prove the convergence of randomly initialized
gradient descent, even for programs with differentiable denotations
(Proposition III.5).

Program denotational semantics automatic differentiation Program denotational
semantics Smooth function mathematical differentiation Smooth function Figure
4: Common approach to the correctness of AD, e.g. [3].  Program denotational
semantics automatic differentiation Program denotational semantics $\omega$PAP
function intensional differentiation $\omega$PAP function Figure 5: Our
approach to the correctness of AD.

###  III-A Correctness of Automatic Differentiation

Terms in our language denote $\omega\text{PAP}{}$ maps $X\to\mathbf{L}Y$, and
so to speak of correct AD in our language, we need some notion of derivative
that applies to such maps. We begin by recalling Lee et al. [5]’s notion of
intensional derivative, then lift it to our setting:

######  Definition III.1 (intensional derivative [5]).

Let $f:U\to V$ be an $\omega\text{PAP}{}$ map, with c-analytic domain
$U\subseteq\mathbb{R}$ and $V\subseteq\mathbb{R}$ (seen as
$\omega\text{PAP}{}$ spaces). Then an $\omega\text{PAP}{}$ map
$g:U\to\mathbb{R}$ is an intensional derivative of $f$ if there exists a
countable family $\\{(A_{i},f_{i})\\}_{i\in I}$ such that:

  * •

the sets $A_{i}$ are analytic and form a partition of $U$;

  * •

the functions $f_{i}:U_{i}\to\mathbb{R}$ are analytic with open domain
$U_{i}\supseteq A_{i}$; and

  * •

for $x\in A_{i}$, $f(x)=f_{i}(x)$ and $g(x)=\frac{d}{dx}f_{i}(x)$.

######  Definition III.2 (lifted intensional derivative).

Let $f:U\to\mathbf{L}V$ be an $\omega\text{PAP}{}$ map, with c-analytic domain
$U\subseteq\mathbb{R}$ and $V\subseteq\mathbb{R}$ (seen as
$\omega\text{PAP}{}$ spaces). Then an $\omega\text{PAP}{}$ map
$g:U\to\mathbf{L}\mathbb{R}$ is a lifted intensional derivative of $f$ if it
is defined on exactly the inputs that $f$ is, and restricted to this common
domain, $g$ is an intensional derivative of $f$.

(These definitions can be straightforwardly extended to the multivariate case,
where $U\subseteq\mathbb{R}^{n}$ and $V\subseteq\mathbb{R}^{m}$, and our full
correctness theorem does cover such functions. But here we demonstrate the
reasoning principles in the simpler univariate setting. Of course, a program
of type $\mathbf{real}\to\mathbf{real}$ may still be defined in terms of
multivariate primitives.)

We now establish that AD, applied to terms with a free parameter
$\theta:\mathbf{real}\vdash t:\mathbf{real}$, computes these lifted
intensional derivatives. It does so in two steps:

  * •

First, we apply a macro $\mathcal{D}$ (defined in Figure 6) to $t$, yielding a
term
$\theta:\mathbf{real}\times\mathbf{real}\vdash\mathcal{D}({t}):\mathbf{real}\times\mathbf{real}$.
This new term operates not on a single real value, but on a dual number, which
intuitively stores both a value and its (intensional) derivative with respect
to an external parameter.

  * •

Then,
$\theta:\mathbf{real}\vdash\mathbf{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}{let}}~{}\theta=\langle\theta,1\rangle~{}\mathbf{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}{in}}~{}\mathbf{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}{case}}~{}\mathcal{D}(t)~{}\mathbf{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}{of}}$
$\langle x,\frac{dx}{d\theta}\rangle\to\frac{dx}{d\theta}$ is output as the
lifted intensional derivative of $\llbracket t\rrbracket$.

$\begin{array}[]{lcllcl}\mathcal{D}(\mathbf{real})&\stackrel{{\scriptstyle\mathrm{def}}}{{=}}&\mathbf{real}\times\mathbf{real}&\mathcal{D}(\tau_{1}\times\tau_{2})&\stackrel{{\scriptstyle\mathrm{def}}}{{=}}&\mathcal{D}({\tau}_{1})\times\mathcal{D}({\tau}_{2})\\\
\mathcal{D}(\mathbb{B})&\stackrel{{\scriptstyle\mathrm{def}}}{{=}}&\mathbb{B}&\mathcal{D}(\tau_{1}\rightarrow\tau_{2})&\stackrel{{\scriptstyle\mathrm{def}}}{{=}}&\mathcal{D}({\tau}_{1})\to\mathcal{D}({\tau}_{2})\end{array}$
$\begin{array}[]{lcl}\mathcal{D}(x)&\stackrel{{\scriptstyle\mathrm{def}}}{{=}}&x\\\
\mathcal{D}(\underline{c}:\mathbf{real})&\stackrel{{\scriptstyle\mathrm{def}}}{{=}}&\langle\underline{c},0\rangle\\\
\mathcal{D}(\underline{c}:\mathbb{B})&\stackrel{{\scriptstyle\mathrm{def}}}{{=}}&\underline{c}\\\
\mathcal{D}(f({t}_{1},\ldots,{t}_{n}))&\stackrel{{\scriptstyle\mathrm{def}}}{{=}}&f_{\mathcal{D}}(\mathcal{D}({t}_{1}),\ldots,\mathcal{D}({t}_{n}))\\\
\mathcal{D}(\lambda x.{t})&\stackrel{{\scriptstyle\mathrm{def}}}{{=}}&\lambda
x.{\mathcal{D}({t})}\\\
\mathcal{D}({t}\,s)&\stackrel{{\scriptstyle\mathrm{def}}}{{=}}&\mathcal{D}({t})\,\mathcal{D}(s)\\\
\mathcal{D}(\langle{t}_{1},{t}_{2}\rangle)&\stackrel{{\scriptstyle\mathrm{def}}}{{=}}&\langle\mathcal{D}({t}_{1}),\mathcal{D}({t}_{2})\rangle\\\
\mathcal{D}({\mathbf{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}{case}}\,{t}\,\mathbf{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}{of}}\,\langle
x_{1},x_{2}\rangle\to
s})&\stackrel{{\scriptstyle\mathrm{def}}}{{=}}&\mathbf{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}{case}}\,\mathcal{D}({t})\\\
&&\,\mathbf{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}{of}}\,\langle
x_{1},x_{2}\rangle\to\mathcal{D}(s)\\\ \mathcal{D}(\mu
f.{t})&\stackrel{{\scriptstyle\mathrm{def}}}{{=}}&\mu f.\mathcal{D}({t})\\\
\mathcal{D}(\mathbf{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}{if}}~{}{t}_{1}~{}\mathbf{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}{then}}~{}{t}_{2}~{}\mathbf{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}{else}}~{}{t}_{3})&\stackrel{{\scriptstyle\mathrm{def}}}{{=}}&\mathbf{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}{if}}~{}\mathcal{D}({t}_{1})~{}\mathbf{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}{then}}~{}\mathcal{D}({t}_{2})\\\
&&~{}\mathbf{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}{else}}~{}\mathcal{D}({t}_{3})\end{array}$

Figure 6: AD macro for our higher-order recursive language

The key hurdle in showing the correctness of this AD procedure is establishing
that the macro $\mathcal{D}$ is correctly propagating intensional dual
numbers. To show this compositionally, and in a way that exploits our
denotational framework, we first define for each type $\tau$ a relation
$V(\tau)$ between pairs of $\omega$PAP plots in $\llbracket\tau\rrbracket$ and
in $\llbracket\mathcal{D}({\tau})\rrbracket$. It captures more precisely the
properties that the dual numbers flowing through our program should have.

######  Definition III.3 (correct dual-number intensional derivative at
$A\subseteq\mathbb{R}$).

Let $\tau$ be a type and let $f:A\to\llbracket\tau\rrbracket$, for some
c-analytic subset $A\subseteq\mathbb{R}$. Then we say
$f^{\prime}:A\to\llbracket\mathcal{D}(\tau)\rrbracket$ is a correct dual-
number intensional derivative of $f$ if $(f,f^{\prime})\in V_{\tau}(A)$, where
$V_{\tau}(A)$ is defined inductively:

  * •

$V_{\mathbf{real}}(A)=\\{(f,f^{\prime})\mid f^{\prime}(x)=(f(x),g(x))$ for
some intensional derivative $g$ of $f\\}$.

  * •

$V_{\mathbb{B}}(A)=\\{(f,f^{\prime})\mid f=f^{\prime}\\}$.

  * •

$V_{\tau_{1}\times\tau_{2}}(A)=\\{(f,f^{\prime})\mid(\pi_{i}\circ
f,\pi_{i}\circ f^{\prime})\in V_{\tau_{i}}(A)$ for $i=1,2\\}$.

  * •

$V_{\tau_{1}\to\tau_{2}}(A)=\\{(f,f^{\prime})\mid\forall(g,g^{\prime})\in
V_{\tau_{1}}(A),$ $(\lambda x.f(x)(g(x)),\lambda
x.f^{\prime}(x)(g^{\prime}(x)))\in V_{\tau_{2}}(A)\\}$.

Readers may recognize $V$ as defining a (semantic) logical relation; its
definition at product and function types is completely standard, so only at
ground types did we make any real choices. For partial functions, we need to
extend the definition:

######  Definition III.4 (correct lifted dual-number intensional derivative at
$A\subseteq\mathbb{R}$).

Let $\tau$ be a type and let $f:A\to\mathbf{L}\llbracket\tau\rrbracket$, for
some c-analytic subset $A\subseteq\mathbb{R}$. Then we say
$f^{\prime}:A\to\mathbf{L}\llbracket\mathcal{D}(\tau)\rrbracket$ is a correct
lifted dual-number intensional derivative of $f$ if $f$ and $f^{\prime}$ are
defined (i.e., not $\bot$) on the same domain and, restricted to this common
domain, $f^{\prime}$ is a correct dual-number intensional derivative of $f$.

We are now in a position to state more precisely what it would mean for the
$\mathcal{D}$ macro to correctly propagate dual numbers. In particular, the
macro transforms terms $\Gamma\vdash t:\tau$ into their correct dual-number
translations $\mathcal{D}(\Gamma)\vdash\mathcal{D}(t):\mathcal{D}(\tau)$, the
specification for which is given below.

######  Definition III.5 (correct dual-number translation).

Let $\tau_{1}$ and $\tau_{2}$ be types, and let
$f:\llbracket\tau_{1}\rrbracket\to\mathbf{L}\llbracket\tau_{2}\rrbracket$.
Then
$f_{\mathcal{D}}:\llbracket\mathcal{D}(\tau_{1})\rrbracket\to\mathbf{L}\llbracket\mathcal{D}(\tau_{2})\rrbracket$
is a correct dual-number translation of $f$ if, for all c-analytic $A$, and
all pairs $(g,g^{\prime})\in V_{\tau_{1}}(A)$, $f_{D}\circ g^{\prime}$ is a
correct lifted dual-number intensional derivative of $f\circ g$.

We assume that each primitive $f:\tau_{1}\to\tau_{2}$ in our language is
equipped with a built-in correct dual-number translation $f_{\mathcal{D}}$,
which the definition of $\mathcal{D}$ in Figure 6 uses. Because the primitives
are translated correctly, so are whole programs:

######  Lemma III.1 (Correctness of $\mathcal{D}$ macro (limited)).

For any term $\Gamma\vdash t:\tau$,
$\llbracket\mathcal{D}(t)\rrbracket:\llbracket\mathcal{D}(\Gamma)\rrbracket\to\llbracket\mathcal{D}(\tau)\rrbracket$
is a correct dual-number translation of $\llbracket t\rrbracket$.

###### Proof Sketch.

This is the Fundamental Lemma of our logical relations proof, and can be
obtained using general machinery [15], after verifying several properties of
our particular setting:

  * •

$V_{\mathbf{real}}(A)$ is closed under piecewise gluing: if $\\{A_{i}\\}_{i\in
I}$ is a countable partition of $A$, and $(f|_{A_{i}},f^{\prime}|_{A_{i}})\in
V_{\mathbf{real}}(A_{i})$ for each $i\in I$, then $(f,f^{\prime})\in
V_{\mathbf{real}}(A)$. This follows from our definition of intensional
derivative.

  * •

$V_{\mathbf{real}}(A)$ is closed under restriction: if $(f,f^{\prime})\in
V_{\mathbf{real}}(A)$, and $A^{\prime}\subseteq A$ is c-analytic, then
$(f|_{A^{\prime}},f^{\prime}_{A^{\prime}})\in V_{\mathbf{real}}(A^{\prime})$.
This also follows easily from our definition.

  * •

The lifted dual-number intensional derivatives are closed under least upper
bounds: if $\\{(f_{n},f^{\prime}_{n})\\}_{n\in\mathbb{N}}$ is a sequence with
each
$f^{\prime}_{n}:A\to\mathbf{L}\llbracket\mathbb{R}\times\mathbb{R}\rrbracket$
a correct lifted dual-number intensional derivative of
$f:A\to\mathbf{L}\mathbb{R}$, and with $f_{n}\leq f_{n+1}$ and
$f^{\prime}_{n}\leq f^{\prime}_{n+1}$ for each $n\in\mathbb{N}$, then
$\bigvee_{n\in\mathbb{N}}f^{\prime}_{n}$ is a correct lifted dual-number
intensional derivative of $\bigvee_{n\in\mathbb{N}}f_{n}$. This is more
involved, but its proof mirrors the one that establishes
$\mathbf{L}\mathbb{R}$ as an $\omega\text{PAP}{}$ space in the first place: we
explicitly construct representations of the lubs in question as piecewise
functions, satisfying Definition III.2.

∎

The overall correctness theorem follows easily:

######  Theorem III.2 (Correctness of AD Algorithm (limited)).

For any term $\theta:\mathbf{real}\vdash{t}:\mathbf{real}$, the
$\omega\text{PAP}{}$ map
$\lambda\theta.\llbracket\mathbf{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}{case}}~{}\mathcal{D}(t)~{}\mathbf{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}{of}}~{}\langle
x,\frac{dx}{d\theta}\rangle\to\frac{dx}{d\theta}\rrbracket((\theta,1))$ is a
lifted intensional derivative of $\llbracket{t}\rrbracket$.

###### Proof.

We apply Lemma III.1, setting $(g,g^{\prime})$ from Definition III.5 to
$(\lambda\theta.\theta,\lambda\theta.(\theta,1))$. This implies that
$(\llbracket
t\rrbracket,\lambda\theta.\llbracket\mathcal{D}(t)\rrbracket(\theta,1))$ are
defined on the same domain, and on that domain $A$, their restrictions are in
$V_{\mathbf{real}}(A)$. This implies that on that domain,
$\lambda\theta.\pi_{2}(\llbracket\mathcal{D}(t)\rrbracket((\theta,1)))$ is an
intensional derivative of $\llbracket t\rrbracket$, from which the result
follows by unfolding the definition of $\llbracket\cdot\rrbracket$ on
$\mathbf{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}{case}}$
expressions. ∎

This result, which we achieved via denotational reasoning, immediately implies
the result of Mazza and Pagani [7]:

######  Corollary III.2.1.

If $\theta:\mathbf{real}\vdash t:\mathbf{real}$ denotes a total differentiable
function, then the AD algorithm fails at a measure-zero set of inputs.

###### Proof.

Because $\llbracket t\rrbracket$ is total, it is PAP and AD computes an
intensional derivative of $\llbracket t\rrbracket$. Intensional derivatives
are almost everywhere equal to true derivatives [5]. ∎

Using more complex logical predicates, we can prove correctness for
multivariate functions (see Appendix C). In the multivariate setting, forward-
mode AD typically computes Jacobian-vector products; for us, it computes
lifted intensional Jacobian-vector products.

######  Definition III.6 (lifted intensional Jacobian).

Let $f:U\to\mathbf{L}V$ be an $\omega\text{PAP}{}$ map, with
$U\subseteq\mathbb{R}^{n}$ c-analytic and $V\subseteq\mathbb{R}^{m}$. An
$\omega\text{PAP}{}$ map $g:U\to\mathbf{L}\mathbb{R}^{m\times n}$ is an
intensional Jacobian of $f$ if it is defined (i.e., not $\bot$) exactly when
$f$ is, there exists a countable analytic partition $\\{A_{i}\\}_{i\in I}$ of
its domain, and there exist analytic functions $f_{i}:U_{i}\to\mathbb{R}^{m}$
with open domains $U_{i}\supseteq A_{i}$ such that when $x\in A_{i}$,
$f(x)=f_{i}(x)$ and $g(x)=Jf_{i}(x)$, where $J$ is the Jacobian operator.

######  Theorem III.3 (Correctness of AD (full)).

For any term
$x_{1}:\mathbf{real},\dots,x_{n}:\mathbf{real}\vdash{t}:\mathbf{real}\times\dots\times\mathbf{real}$,
and any vector $\mathbf{v}\in\mathbb{R}^{n}$, the $\omega\text{PAP}{}$ map
$\lambda\mathbf{\theta}.\textbf{let
}\mathbf{x}=\llbracket\mathcal{D}({t})\rrbracket((\theta_{1},v_{1}),\dots,(\theta_{n},v_{n}))\textbf{
in }(\pi_{2}x_{1},\dots,\pi_{2}x_{m})$ is equal to
$g(\mathbf{\theta})\cdot\mathbf{v}$ for some intensional Jacobian $g$ of
$\llbracket t\rrbracket$.

###  III-B Optimization of Differentiable Programs with AD-computed
Derivatives

Our characterization of AD’s behavior, proven in the previous section, can be
used to establish the correctness of algorithms that use the results of AD. In
optimization, for example, a very common technique for minimizing a
differentiable function $f:\mathbb{R}^{d}\to\mathbb{R}$ is gradient descent.
Starting at an initial point $x^{0}\in\mathbb{R}^{d}$, for a set step size
$\epsilon>0$, we iterate the following update:

$x^{t+1}:=x^{t}-\epsilon\nabla f(x^{t}).$ (1)

If the step size $\epsilon$ is too large, we cannot hope to converge on an
answer. To ensure that a small-enough step size can be found, we need to know
that $f$’s gradient changes slowly:

######  Definition III.7.

A differentiable function $f:\mathbb{R}^{d}\to\mathbb{R}$ is $L$-smooth if for
all $x,y\in\mathbb{R}^{d}$

$\lVert\nabla f(x)-\nabla f(y)\rVert\leq L\lVert x-y\rVert.$

When $f$ is $L$-smooth, it is well known that $\epsilon$ can be chosen small
enough for gradient descent to converge (albeit not necessarily to a global
minimum):

######  Theorem III.4 (e.g. [16]).

Let $f$ be $L$-smooth, bounded below, and $0<\epsilon<\frac{2}{L}$. Then, for
any initial $x^{0}\in\mathbb{R}^{d}$, following the method from Equation 1,
the gradient of $f$ tends to 0:

$\lim_{t\to\infty}\nabla f(x^{t})=0$

and the function $f$ monotonically decreases on values of the sequence
$\\{x^{t}\\}_{t}$, that is for all $t\in\mathbb{N}$, $f(x^{t+1})\leq
f(x^{t})$.

However, this theorem assumes that the true gradient of $f$ is used to make
each update. When gradients are obtained by AD, this may not be the case, even
if $f$ is differentiable: we proved only that AD computes intensional
derivatives, which may disagree with true derivatives on a measure-zero set of
inputs.

Intuitively, it may seem as though we can avoid the measure-zero set of inputs
on which AD may be incorrect by randomly selecting an initial point $x^{0}$.
Indeed, similar arguments have been made informally in the literature [7]. But
this turns out not to be the case:

######  Proposition III.5.

Let $\epsilon>0$. There exists a program $P$ such that $\llbracket
P\rrbracket:\mathbb{R}\to\mathbb{R}$ satisfies the condition of Theorem III.4,
and yet, for all $x^{0}\in\mathbb{R}$, the gradient descent method diverges to
$-\infty$, when the gradients are computed with AD.

###### Proof sketch.

Let $P$ be the closed program defined by the following code, where $lr$ is our
chosen learning rate $\epsilon$.

⬇

# Recursive helper

def g(x, n):

if x > 0:

return ((x - n)*(x - n))/(lr * 2)

if x == 0:

return x / lr + n*n / (2*lr)

else:

return g(x+1, n+1)

\pardef P(x):

return g(x,0)

One can show that $\llbracket P\rrbracket=x\mapsto\frac{x^{2}}{2\epsilon}$ and
satisfies the conditions of Theorem III.4, yet gradient descent will diverge
to $-\infty$ for all initial points $x^{0}$. The full explanation is given in
Appendix D-A. ∎

The proof applies to an idealized setting where gradient descent is run with
real numbers, rather than floating-point numbers, but in our experiments,
PyTorch did diverge on this program. Similar counterexamples can be
constructed for some variants of the gradient descent algorithm, e.g. when the
learning rate is changing according to a schedule.

Likewise, it is easy to derail the algorithm when the learning rate $\epsilon$
is random but the initial point $x^{0}$ is fixed.

######  Proposition III.6.

Let $x^{0}$ be a fixed initial point. Then there exists a program $P$ such
that $\llbracket P\rrbracket:\mathbb{R}\to\mathbb{R}$ satisfies the conditions
of Theorem III.4, and $\llbracket P\rrbracket^{\prime}(x^{0})\neq 0$, and yet,
for all $\epsilon>0$, the gradient descent method yields $x^{t}=x^{0}$ for all
$t$, when the gradients are computed with AD.

###### Proof.

Simply chose any $x^{0}$ for which the intensional derivative is $0$, but for
which the true derivative is non-zero. ∎

The counterexamples constructed for the proofs above are tied to a specific
learning rate or to a specific initialization. It is therefore reasonable to
think that by randomizing both quantities, one might be able to almost surely
avoid such counter-examples. Thankfully, this is the case.

######  Theorem III.7 (Convergence of GD with intensional derivatives).

Let $f$ be PAP, bounded below, $L$-smooth. Let $(\epsilon,x_{0})$ be drawn
randomly from a continuous probability distribution supported on
$(0,\frac{2}{L})\times\mathbb{R}^{d}$. Then when gradient descent computes
gradients using AD, the true gradient tends to 0 with probability 1:

$\lim_{t\to\infty}\nabla f(x^{t})=0.$

Furthermore, with probability 1, the function $f(x)$ monotonically decreases:
$f(x^{t+1})\leq f(x^{t})$.

The proof is given in Appendix D-B.

##  IV Reasoning about Probabilistic Programs

PAP functions were originally developed in Lee et al. [5] to reason about
automatic differentiation, so perhaps it is not surprising that their
generalization to $\omega\text{PAP}{}$ was useful, in the previous section,
for characterizing AD’s behavior. In this section, we show that the
$\omega$PAP semantics also makes it nice to reason about probabilistic
programs: by excluding pathological deterministic primitives, we also prevent
many pathologies from arising in the probabilistic setting, enabling clean
denotational arguments for several nice properties.

To reason about probabilistic programs, we must extend our core calculus
(Figure 2) with the standard effectful operations exposed by probabilistic
programming languages (PPLs):
$\mathbf{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}{sample}}$
samples a real from the uniform distribution on $(0,1)$, and
$\mathbf{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}{score}}~{}r$
reweights program traces (to implement soft constraints). Their typing rules
are given in Figure 7.

$\Gamma\vdash e:\mathbb{R}$
---
$\Gamma\vdash\mathbf{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}{score}}~{}e:1$

$\Gamma\vdash\mathbf{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}{sample}}:\mathbb{R}$
---

Figure 7: Type system of the probabilistic part of the language

The language needs no new types, but the semantics change: instead of
interpreting our language with the monad $\mathbf{L}$, which models
divergence, we must use a new monad that also tracks probabilistic
computation. In Section IV-A, we introduce a monad of weighted samplers [8],
which can informally be seen as deterministic functions from a source of
randomness to output values. We use this monad to reason about the
deterministic weight functions that some probabilistic programming systems use
during inference, presenting a new (much simplified) proof of Mak et al. [9]’s
result that almost-surely-terminating probabilistic programs have almost-
everywhere differentiable weight functions. In Section IV-B, we introduce a
commutative monad of measures, which can be seen as a smaller version of Vákár
et al. [2]’s monad of measures, excluding those measures which can’t be
defined using $\omega\text{PAP}{}$ deterministic primitives. We use this
smaller monad to prove that all definable measures in our language are
supported on countable unions of smooth manifolds. This implies that they have
densities with respect to a particular well-behaved class of base measures,
and we close by briefly discussing the implications for PPL designers.

###  IV-A Almost-Everywhere Differentiability of Weight Functions

First, we define a monad $\mathbf{S}$ of weighted samplers, that interprets
programs as partial $\omega\text{PAP}{}$ maps from a space $\Omega$ of random
seeds to a space of weighted values. Intuitively, the measure represented (or
“targeted”) by a sampler of weighted pairs $(x,w)$ is the one that assigns
measure $\mathbb{E}[w\cdot 1_{A}(x)]$ to each measurable set $A$. But this
semantics does not validate many important program equivalences, like
commutativity, intuitively because it exposes “implementation details” of
weighted samplers, that can differ even for samplers targeting the same
measure. This is intentional: our first goal is to prove a property of these
“implementation details,” one that inference algorithms automated by PPLs
might rely on.

First, we fix our source of randomness $\Omega$ to be the lists of reals,
$\sqcup_{i\in\mathbb{N}}\mathbb{R}^{i}$ (which is an $\omega\text{PAP}{}$
space, see Example II.3). We then define our monad:

######  Definition IV.1 (monad of weighted samplers).

Let $\mathbf{S}$ be the monad
$(\mathbf{S},\mathbf{return}^{\mathbf{S}},\mathop{\gg\mkern-10.0mu\scalebox{1.0}[1.0]{=}}^{\mathbf{S}})$,
defined as follows:

  * •

$\mathbf{S}X:=\Omega\Rightarrow\mathbf{L}((X+1)\times[0,\infty)\times\Omega)$

  * •

$\mathbf{return}^{\mathbf{S}}_{X}:=\lambda x.\lambda
r.\mathbf{inl}(\mathbf{inl}~{}x,1,r)$

  * •

$\mathop{\gg\mkern-10.0mu\scalebox{1.0}[1.0]{=}}^{\mathbf{S}}_{X,Y}:=\lambda
m.\lambda k.\lambda
r.m(r)\mathop{\gg\mkern-10.0mu\scalebox{1.0}[1.0]{=}}^{\mathbf{L}}(\lambda(x_{?},w,r^{\prime}).\mathbf{match}~{}x_{?}$
$\mathbf{with}~{}\\{\mathbf{inr}~{}\\_\to\mathbf{inl}~{}(x_{?},0.0,r^{\prime})\mid\mathbf{inl}~{}x\to
k(x)(r^{\prime})\mathop{\gg\mkern-10.0mu\scalebox{1.0}[1.0]{=}}^{\mathbf{L}}\lambda(y_{?},v,r^{\prime\prime}).\mathbf{inl}~{}(y_{?},w\cdot
v,r^{\prime\prime})\\}$.

$\begin{array}[]{lcl}\llbracket\mathbf{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}{sample}}\rrbracket(\rho)&\stackrel{{\scriptstyle\mathrm{def}}}{{=}}&\lambda
r.\mathbf{match}~{}r~{}\mathbf{with}\\{\\\
&&\quad()\to\mathbf{inl}~{}(\mathbf{inr}~{}\star,0,r)\\\
&&\quad\mid(r_{1},r_{2:n})\to\mathbf{inl}~{}(\mathbf{inl}~{}r_{1},1,r_{2:n})\\}\\\
\llbracket\mathbf{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}{score}}~{}t\rrbracket(\rho)&\stackrel{{\scriptstyle\mathrm{def}}}{{=}}&\llbracket
t\rrbracket(\rho)\mathop{\gg\mkern-10.0mu\scalebox{1.0}[1.0]{=}}(\lambda
w.\lambda r.\mathbf{inl}(\mathbf{inl}~{}\star,0\vee w,r))\\\ \llbracket\mu
f.\lambda
x.{t}\rrbracket(\rho)&\stackrel{{\scriptstyle\mathrm{def}}}{{=}}&\mathbf{return}~{}\bigvee_{i\in\mathbb{N}}f_{i}\end{array}$
where $f_{0}=\lambda x.\lambda r.\mathbf{inr}~{}\bot,f_{i+1}=\lambda
v.\llbracket{t}\rrbracket(\rho[f\mapsto f_{i},x\mapsto v])$

Figure 8: Updated semantics for new monad $\mathbf{S}$ of effects

This monad interprets a probabilistic program as a partial function mapping
lists of real-valued random samples, called traces, to: (1) the output values
they possibly induce in $X$ (or $\mathbf{inr}~{}\star$ if the input trace does
not contain enough samples to complete execution of the program), (2) a weight
in $[0,\infty)$, and (3) a remainder of the trace, containing any samples not
yet used. The $\mathbf{return}$ of the monad consumes no randomness, and
successfully returns its argument with a weight of $1$. The
$\mathop{\gg\mkern-10.0mu\scalebox{1.0}[1.0]{=}}$ of the monad runs its
continuation on the random numbers remaining in the trace after its first
argument has executed, and multiplies the weights from both parts of the
computation. Figure 8 gives the semantics of
$\mathbf{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}{sample}}$
and
$\mathbf{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}{score}}$,
as well as updated semantics for $\mu f.t$ (the only change is that the bottom
element, from which least fixed points are calculated, is now the bottom
element of $\mathbf{S}X$ rather than $\mathbf{L}X$). The
$\mathbf{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}{sample}}$
command fails to produce a value when given an empty trace, but otherwise
consumes the first value in the trace and returns it. The
$\mathbf{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}{score}}$
command consumes no randomness, and uses its argument (if non-negative) as the
weight.

One way to use a weighted sampler is to run it, continually providing longer
and longer lists of uniform random numbers until a value from $X$ (and an
associated weight) is generated. But many probabilistic programming systems
also expose more sophisticated inference algorithms. Gradient-based methods,
such as Hamiltonian Monte Carlo or Langevin ascent, attempt to find executions
with high weights by performing hill-climbing optimization or MCMC over the
space of traces, guided by a program’s weight function.

######  Definition IV.2 (weight function).

For any $p\in|\mathbf{S}~{}X|$, define its weight function
$w_{p}:\sqcup_{i\in\mathbb{N}}[0,1]^{i}\to[0,\infty)$, as follows:

  * •

When $p(r)=\mathbf{inr}~{}\bot$, $w_{p}(r)=0$.

  * •

When $p(r)=\mathbf{inl}~{}(x,v,r)$ for $r^{\prime}$ non-empty, $w_{p}(r)=0$.

  * •

When $p(r)=\mathbf{inl}~{}(x,v,())$, $w_{p}(r)=v$.

The weight function can be viewed as a density with respect to a particular
base measure on traces; scaling the base measure by this density yields an
unnormalized measure, and the normalized version of this measure, which is a
probability distribution placing high mass on traces that lead to high
weights, is called the posterior over traces. Inference algorithms like HMC
are designed to generate samples approximately distributed according to this
posterior.

Using our definition of the weight function, we can recover Mak et al. [9]’s
result about the almost-everywhere differentiability of weight functions, a
convenient property when reasoning about gradient-based inference:

######  Theorem IV.1.

Probabilistic programs that almost surely halt have almost-everywhere
differentiable weight functions.

###### Proof.

Let $\vdash t:X$ be a program. Almost-sure termination implies that for almost
all inputs $r\in\sqcup_{i\in\mathbb{N}}[0,1]^{i}$, $\llbracket
t\rrbracket(r)\neq\mathbf{inr}~{}\bot$. Restricted to $\llbracket
t\rrbracket$’s domain (which is almost all of
$\sqcup_{i\in\mathbb{N}}[0,1]^{i}$), its weight function $w_{\llbracket
t\rrbracket}$ is $\omega\text{PAP}{}$, and thus almost-everywhere
differentiable. Almost all of almost all of $\sqcup_{i\in\mathbb{N}}[0,1]^{i}$
is almost all of $\sqcup_{i\in\mathbb{N}}[0,1]^{i}$, concluding the proof. ∎

We note that the proof only uses the fact that for almost all
$r\in\sqcup_{i\in\mathbb{N}}[0,1]^{i}$, $\llbracket
t\rrbracket(r)\neq\mathbf{inr}~{}\bot$—which is strictly weaker than almost-
sure termination. Almost-sure termination can fail even though a program halts
on any finite trace of random numbers. Some probabilistic context-free
grammars, for example, do not always surely halt, but as they execute, they
consume an unbounded amount of randomness, so that when provided a finite
trace, they will eventually halt with an error. Our proof shows that such
programs, although they do not almost surely halt, do have almost-everywhere
differentiable weight functions. As such, our result is slightly stronger than
that of Mak et al. [9], and followed immediately from the interpretation of
probabilistic programs in the $\omega\text{PAP}{}$ category.

###  IV-B Existence of Convenient Base Measures for Monte Carlo

We now wish to prove a result not about the intensional properties of
probabilistic programs (like their weight functions), but the extensional
properties of the measures that programs denote. To do so, we construct a
final monad in which to interpret our language: a commutative monad of
measures, similar to that of Vákár et al. [2].

######  Definition IV.3 ($\omega\text{PAP}{}$ space of measure weights).

Define $\mathbb{W}$ to be the $\omega\text{PAP}{}$ space with:

  * •

$|\mathbb{W}|=\mathbb{R}_{\geq 0}\cup\\{\infty\\}$, the extended non-negative
reals;

  * •

$w\leq_{\mathbb{W}}v$ when $v=\infty$ or when $w<v<\infty$.

  * •

$\phi\in\mathcal{P}_{\mathbb{W}}^{A}$ whenever $\phi:A\to\mathbb{W}$ is
measurable.

Note that although many maps into $\mathbb{W}$ exist, very few maps exist out
of $\mathbb{W}$, because its $\omega\text{PAP}{}$ diffeology is so permissive:
any measurable function is a plot.

Following Ścibior et al. [8], measures can be seen as equivalence classes of
samplers that behave the same way as integrators. Given a weighted sampler
$p\in|\mathbf{S}X|$, we can define the integrator it represents:

######  Definition IV.4 (integrator associated to a sampler).

We define $\omega\text{PAP}{}$ maps
$\mathbf{Int}_{X}:\mathbf{S}X\to(X\Rightarrow\mathbb{W})\Rightarrow\mathbb{W}$
sending samplers to their associated integrators:
$\mathbf{Int}_{X}~{}p=\lambda
f.\int_{\text{Dom}(\alpha_{p})}\Lambda_{\Omega}(dr)f(\alpha_{p}(r))$, where

  * •

$\Lambda_{\Omega}$ is a Lebesgue base measure over $|\Omega|$, assigning to
each measurable subset $A\subseteq\Omega$ the value
$\sum_{i\in\mathbb{N}}\Lambda^{i}(\\{\mathbf{x}\mid(i,\mathbf{x})\in A\\})$
(where $\Lambda^{i}$ is the Lebesgue measure on $\mathbb{R}^{i}$).

  * •

$\alpha_{p}:\Omega\to\mathbf{L}X$ is an $\omega\text{PAP}{}$ map that on input
$r$, returns $\mathbf{inr}~{}\bot$ if any of the following hold: $r$ is empty;
$r_{1}<0$; $r_{2:|r|}\not\in[0,1]^{|r|-1}$; $p(r_{2:|r|})$ returns
$\mathbf{inr}\bot$; or $p(r_{2:|r|})$ returns
$\mathbf{inl}~{}(x,v,r^{\prime})$ and either $r^{\prime}$ is non-empty,
$x=\mathbf{inr}~{}\star$, or $v<r_{1}$. Otherwise, $p(r_{2:|r|})$ must return
$(\mathbf{inl}~{}x,\\_,\\_)$, and $\alpha_{p}$ also returns
$\mathbf{inl}~{}x$.

  * •

$\text{Dom}(\alpha_{p})$ is the domain of the partial map $\alpha_{p}$.

Then, following Vákár et al. [2], we take the measures to be those integrators
that lie in the image of $\mathbf{Int}$:

######  Definition IV.5 (monad of measures).

The monad $\mathbf{M}$ of measures is defined by:

  * •

$\mathbf{M}X$ is the image of $\mathbf{S}X$ under $\mathbf{Int}_{X}$. It is a
subobject of $(X\Rightarrow W)\Rightarrow W$ and inherits its order.

  * •

$\mathbf{return}^{\mathbf{M}}_{X}:=\lambda x.\lambda f.f(x)$.

  * •

$\mathop{\gg\mkern-10.0mu\scalebox{1.0}[1.0]{=}}^{\mathbf{M}}_{X,Y}:=\lambda
m.\lambda k.\lambda f.m(\lambda x.k(x)(f))$.

$\begin{array}[]{lcl}\llbracket\mathbf{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}{sample}}\rrbracket(\rho)&\stackrel{{\scriptstyle\mathrm{def}}}{{=}}&\lambda
f.\int_{[0,1]}f(x)dx\\\
\llbracket\mathbf{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}{score}}~{}t\rrbracket(\rho)&\stackrel{{\scriptstyle\mathrm{def}}}{{=}}&\lambda
f.\llbracket t\rrbracket(\rho)(\lambda w.(0\vee w)\cdot f(\star))\\\
\llbracket\mu f.\lambda
x.{t}\rrbracket(\rho)&\stackrel{{\scriptstyle\mathrm{def}}}{{=}}&\mathbf{return}~{}\bigvee_{i\in\mathbb{N}}f_{i}\end{array}$
where $f_{0}=\lambda x.\lambda f.0,f_{i+1}=\lambda
v.\llbracket{t}\rrbracket(\rho[f\mapsto f_{i},x\mapsto v])$

Figure 9: Updated semantics for new monad $\mathbf{M}$ of effects

This monad is a submonad of the continuation monad [2], and so the
$\mathbf{return}$ and $\mathop{\gg\mkern-10.0mu\scalebox{1.0}[1.0]{=}}$ are
inherited. The
$\mathbf{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}{sample}}$
command is interpreted as the uniform measure on $[0,1]$, and the
$\mathbf{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}{score}}~{}t$
command as a measure on a one-point space, with a certain total mass given by
$t$. Our semantics under $\mathbf{M}$ (Fig. 9) is related to the one from the
previous section (Fig. 8) in that for any closed term $\vdash t:X$,
$\mathbf{Int}_{X}(\llbracket t\rrbracket_{\mathbf{S}})=\llbracket
t\rrbracket_{\mathbf{M}}$. Using this, we can establish the following lemma
about the definable measures:

######  Lemma IV.2.

Let $\vdash{t}:\mathbf{real}\times\dots\times\mathbf{real}$. Then, there
exists a partial $\omega$PAP function
$f_{{t}}:\Omega\rightharpoonup\mathbb{R}^{n}$ such that
$\llbracket{t}\rrbracket={f_{{t}}}_{*}\Lambda_{\Omega}$.

That is, any probabilistic program returning reals must arise as a well-
behaved transformation of “input randomness” represented by $\Omega$. This is
not particularly surprising, of course, because a probabilistic program is
defined by specifying an ($\omega\text{PAP}{}$) transformation of input
randomness, but it highlights the way we will use our $\omega\text{PAP}{}$
semantics to establish general properties of the measures denoted by
probabilistic programs.

In particular, we will characterize the definable measures as absolutely
continuous with respect to a particular class of base measures. We first
recall some relevant definitions from differential geometry, starting with the
smooth manifolds, a well-studied generalization of Euclidean spaces; common
examples include lines, spheres, and tori.

######  Definition IV.6.

A smooth manifold $M$ is a second-countable Hausdorff topological space
together with a smooth atlas: an open cover $\mathcal{U}$ together with
homeomorphisms $(\phi_{U}:U\to\mathbb{R}^{n})_{U\in\mathcal{U}}$ called charts
such that $\phi_{V}\circ\phi_{U}^{-1}$ is smooth on its domain of definition
for all $U,V\in\mathcal{U}$. A function $f:M\to N$ between manifolds is smooth
if $\phi_{V}\circ f\circ\phi_{U}^{-1}$ is smooth for all charts
$\phi_{U},\phi_{V}$ of $M$ and $N$. When there’s a global bound $K$ on the
local dimensions $n$ of a smooth manifold, it’s well known by a theorem of
Whitney that the manifold can be embedded as a submanifold of an Euclidean
space, that is its topology is given by restricting the standard one from the
surrounding Euclidean space.

There is a natural measure on smooth manifolds that generalizes the Lebesgue
measure on Euclidean spaces, and matches our intuitive notions of area and
volume on curved spaces.

######  Definition IV.7.

The $k$-Hausdorff measure on a metric space $(X,d)$ is defined as

$H^{k}(S):=\lim_{\delta\to
0}\inf\Big{\\{}\sum_{i}\operatorname{\mathrm{diam}}(U_{i})^{k}\mid
S\subseteq\bigcup_{i}U_{i},\operatorname{\mathrm{diam}}(U_{i})<\delta\Big{\\}}$

where $\operatorname{\mathrm{diam}}(U):=\sup~{}\\{d(x,y)~{}\mid~{}x,y\in U\\}$
and $\operatorname{\mathrm{diam}}(\emptyset):=0$. The Hausdorff dimension is
then defined as $\dim_{\text{Haus}}(S):=\inf\\{k~{}\mid~{}H^{k}(S)=0\\}$.

The Hausdorff measure computes the sizes of sets $S$ in a dimension-dependent
way:

  * •

The $0$-Hausdorff measure counts the points in $S$.

  * •

The $1$-Hausdorff measure sums the lengths of curves within a set. It will be
infinite on surfaces, and 0 on sets of isolated points.

  * •

The $2$-dimentional Hausdorff measure sums the areas of surfaces, and will be
infinite on volumes and 0 on curves. More generally, the $k$-Hausdorff measure
will quantify $k$-dimensional volumes.

For smooth manifolds, the Hausdorff dimension matches the intuitive notion of
dimension, e.g. a sphere in $\mathbb{R}^{3}$ has Hausdorff dimension $2$ , a
path on such a sphere will have Hausdorff dimension $1$, and an open of
$\mathbb{R}^{n}$ has dimension $n$. We now define our class of s-Hausdorff
measures, which measure the sizes of sets by measuring the $d$-dimensional
volumes of their intersections with $d$-dimensional manifolds, for every $d$:

######  Definition IV.8 (s-Hausdorff measure on $\mathbb{R}^{n}$).

An s-Hausdorff measure on $\mathbb{R}^{n}$ is a measure $\mu$ that decomposes
as

$\mu(A)=\sum_{d=0}^{n}H^{d}(A\cap M^{d})$

where each $M^{d}$ is a countable union $\bigcup_{i}M^{d}_{i}$ of
$d$-dimensional smooth manifolds $M^{d}_{i}$.

Our main result in this section is a construction that assigns an s-Hausdorff
measure $B({t})$ to every closed probabilistic program
$\vdash{t}:\mathbf{real}\times\dots\times\mathbf{real}$, such that
$\llbracket{t}\rrbracket$ has a density w.r.t. $B({t})$. We write $\mu\ll\nu$
to mean that $\mu$ is absolutely continuous w.r.t. $\nu$.

######  Theorem IV.3.

Let $\vdash{t}:\mathbf{real}\times\dots\times\mathbf{real}$ be a closed
probabilistic program. There exists an s-Hausdorff measure $B({t})$ on
$\mathbb{R}^{n}$ such that

  * •

$\llbracket{t}\rrbracket$ has a density (possibly infinite) $\rho_{{t}}$ with
respect to $B({t})$;

  * •

if $\mu$ is another s-Hausdorff measure w.r.t. which $\llbracket{t}\rrbracket$
has a density, then that density is $\llbracket{t}\rrbracket$-almost-
everywhere equal to $\rho_{{t}{}}$.

  * •

if $t_{2}$ has the same type and
$\llbracket{t}_{1}\rrbracket\ll\llbracket{t}_{2}\rrbracket$ then
$B({t}_{1})\ll B({t}_{2})$; and

  * •

there is a set $A\subseteq\mathbb{R}^{n}$ such that $\mathbf{1}_{A}$ is a
morphism and is a density of $B({t}_{1})$ with respect to $B({t}_{2})$.

In particular, this means that a sensible design decision for a PPL is to
always compute densities of probabilistic programs $p$ with respect to an
s-Hausdorff base measure $B(p)$. In order to compute Radon-Nikodym derivatives
between multiple programs, the theorem implies we can separately compute their
densities and then take the ratio, so long as we also include a “support
check” (of the sort described by [10]).

Finally, the following result shows that the class of s-Hausdorff measures
seems appropriate to serve as base measures, as for each s-Hausdorff measure,
there is a closed probabilistic program whose posterior distribution has a
strictly positive density w.r.t that measure. This means that we cannot ’carve
out’ any mass from the s-Hausdorff measure, and that the underlying supporting
manifolds faithfully represent the possible supports of posterior
distributions of probabilistic programs.

######  Theorem IV.4.

Assume that the language has all partial PAP functions as primitives. Then,
for every $n\in\mathbb{N}$ and every s-Hausdorff measure $\mu$, there exists a
program $\vdash{t}:\mathbb{R}^{n}$ such that $\llbracket{t}\rrbracket$ and
$\mu$ are mutually absolutely continuous.

The proof is given at the end of Appendix E-B.

##  V Related Work and Discussion

Summary. We introduced the category of $\omega\text{PAP}{}$ spaces and used it
as a denotational model for expressive higher-order recursive effectful
languages. We first looked at a deterministic language with conditionals and
partial PAP functions, which we argued covers almost all differentiable
programs that can be implemented in practice. We showed that AD computes
correct intentional derivatives in such an expressive setting, extending Lee
et al. [5]’s result, and recovering the fact that AD computes derivatives
which are correct almost-everywhere. Next, we showed that gradient descent on
programs implementing differentiable functions can be soundly used with
intentional derivatives, as long as both the learning rate and the
initialization and randomized. We then looked at applications in probabilistic
programming. After introducing a strong monad capturing traces of
probabilistic programs, we gave a denotational proof that the trace density
function of every probabilistic program is almost everywhere differentiable.
Finally, we defined a commutative monad of measures on $\omega\text{PAP}{}$,
and proved that all programs denote measures with densities with respect to
some s-Hausdorff measures. As such, we argued that the s-Hausdorff measures
form a set of convenient base measures for density computations in Monte Carlo
inference, and showed that every closed probabilistic program has a density
w.r.t. some s-Hausdorff measure.

Together, these results demonstrate the value of denotational reasoning with a
“just-specific-enough” model like $\omega\text{PAP}{}$. Results previously
established in the literature by careful operational reasoning, such as
Theorem IV.1, follow almost immediately after setting up the definitions the
right way. And we have also been able to show new theorems, such as Theorem
IV.3, by applying methods from analysis to characterize the restricted class
of denotations in our semantic domain.

Semantics of higher-order differentiable programming. We continue a recent
line of work on giving denotational semantics for higher-order differentiable
programming in functional languages. Our semantics and logical relations proof
builds on insights proposed in the smooth setting in Huot et al. [3], and
takes inspiration from Vákár [4] for the treatment of recursion. In this work,
we considered a simple forward-mode AD translation, but a whole body of work
focused their attention on provably correct and efficient reverse-mode AD
algorithms on higher-order languages [17, 18, 19, 7, 20]. We believe our
correctness result could be adapted to a reverse-mode AD algorithm, perhaps
following the neat ideas developed in Krawiec et al. [20], Radul et al. [21],
or Smeding and Vákár [22], but we leave this for future work. There are also
more synthetic approaches to studying differentiation in a more purely
categorical tradition, sometimes called synthetic differential geometry [23].
Some of these approaches are particularly appealing from a theoretical point
of view [24, 25], but their precise relations with AD and its implementations
remains to be further studied.

Semantics of differentiable programming with non-smooth functions. Our work
directly builds on and extends Lee et al. [5]’s setting to a higher-order
recursive language. As is shown in Lee et al. [26], when moving beyond the
differentiable setting, there are many seemingly reasonable classes of
functions that behave pathologically in subtle ways, usually preventing
compositional reasoning. $\omega$PAP spaces combine the advantage of
restricting to PAP functions at first-order with expressive power provided by
abstract categorical constructions, which conservatively extend the first-
order setting. Bolte and Pauwels [27] investigated a similar problem as Lee et
al. [5] on a more restricted first-order language, but proved a convergence of
gradient descent result in their setting. It would be interesting to see if
some of the ideas developed in Chizat and Bach [28] could be adapted to prove
some convergence of stochastic gradient descent when AD is used on programs
denoting PAP functions, thus going beyond the setting of neural networks.

Semantics of probabilistic programming. Our commutative monad of measures
takes clear inspiration from Staton [6] and Vákár et al. [2], adding an extra
step in the recent search of semantic models for higher-order probabilistic
programming [12, 29]. In particular, our work refines the model of Vákár et
al. [2] by restricting to PAP functions, instead of merely measurable ones,
but keeping its essential good properties for interpreting probabilistic
programs. By doing so, our work is closer in spirit to Freer and Roy [30]’s
study of computable properties for higher-order probabilistic languages. Our
monad for tracking traces of probabilistic programs is similar to what is
presented in Lew et al. [31], giving a denotational version of similar work
that focus on operational semantics, such as Mak et al. [9]. Our result about
densities and s-Hausdorff measures has some of its foundations based on the
careful study of s-finite measures and kernels from Vákár and Ong [32]. It
would be interesting to see if the work of Lew et al. [33] could be extended
to a non-differentiable setting with PAP primitives, proving that an AD
algorithm on a probabilistic language yields unbiased gradient estimates,
perhaps using the estimator derived in Lee et al. [34] for non-smooth
functions.

Disintegration and base measure. Our result on base measures for probabilistic
programs is related to the literature on symbolic disintegration [35, 36, 37],
which has also had to wrestle with the problem of finding base measures with
respect to which expressive programs have densities. Our approach builds on
the idea presented by Radul and Alexeev [10]: we extend the Hausdorff base
measures to s-Hausdorff base measures, and prove that they suffice for
ensuring all programs have densities. We leave open the question of
characterizing exactly the class of densities on s-Hausdorff measures that
arise from probabilistic programs, and the investigation of the closure of
these measures under least upper bounds.

## References

  * Matache et al. [2022] C. Matache, S. Moss, and S. Staton, “Concrete categories and higher-order recursion (with applications including probability, differentiability, and full abstraction),” _arXiv preprint arXiv:2205.15917_ , 2022.
  * Vákár et al. [2019] M. Vákár, O. Kammar, and S. Staton, “A domain theory for statistical probabilistic programming,” _Proceedings of the ACM on Programming Languages_ , vol. 3, no. POPL, p. 36, 2019.
  * Huot et al. [2020] M. Huot, S. Staton, and M. Vákár, “Correctness of automatic differentiation via diffeologies and categorical gluing.” in _FoSSaCS_ , 2020, pp. 319–338.
  * Vákár [2020] M. Vákár, “Denotational correctness of foward-mode automatic differentiation for iteration and recursion,” _arXiv preprint arXiv:2007.05282_ , 2020.
  * Lee et al. [2020] W. Lee, H. Yu, X. Rival, and H. Yang, “On correctness of automatic differentiation for non-differentiable functions,” _Advances in Neural Information Processing Systems_ , vol. 33, pp. 6719–6730, 2020.
  * Staton [2017] S. Staton, “Commutative semantics for probabilistic programming,” in _European Symposium on Programming_. Springer, 2017, pp. 855–879.
  * Mazza and Pagani [2021] D. Mazza and M. Pagani, “Automatic differentiation in pcf,” _Proceedings of the ACM on Programming Languages_ , vol. 5, no. POPL, pp. 1–27, 2021.
  * Ścibior et al. [2017] A. Ścibior, O. Kammar, M. Vákár, S. Staton, H. Yang, Y. Cai, K. Ostermann, S. K. Moss, C. Heunen, and Z. Ghahramani, “Denotational validation of higher-order bayesian inference,” _Proceedings of the ACM on Programming Languages_ , vol. 2, no. POPL, p. 60, 2017.
  * Mak et al. [2021] C. Mak, C.-H. L. Ong, H. Paquet, and D. Wagner, “Densities of almost surely terminating probabilistic programs are differentiable almost everywhere,” _Programming Languages and Systems_ , vol. 12648, p. 432, 2021.
  * Radul and Alexeev [2021] A. Radul and B. Alexeev, “The base measure problem and its solution,” in _International Conference on Artificial Intelligence and Statistics_. PMLR, 2021, pp. 3583–3591.
  * Baez and Hoffnung [2011] J. Baez and A. Hoffnung, “Convenient categories of smooth spaces,” _Transactions of the American Mathematical Society_ , vol. 363, no. 11, pp. 5789–5825, 2011.
  * Heunen et al. [2017] C. Heunen, O. Kammar, S. Staton, and H. Yang, “A convenient category for higher-order probability theory,” in _2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)_. IEEE, 2017, pp. 1–12.
  * Abramsky and McCusker [1998] S. Abramsky and G. McCusker, “Call-by-value games,” in _Computer Science Logic: 11th International Workshop, CSL’97 Annual Conference of the EACSL Aarhus, Denmark, August 23–29, 1997 Selected Papers 11_. Springer, 1998, pp. 1–17.
  * Moggi [1991] E. Moggi, “Notions of computation and monads,” _Information and computation_ , vol. 93, no. 1, pp. 55–92, 1991.
  * Katsumata [2013] S.-y. Katsumata, “Relating computational effects by TT-lifting,” _Information and Computation_ , vol. 222, pp. 228–246, 2013.
  * Polyak [1987] B. T. Polyak, “Introduction to optimization. optimization software,” _Inc., Publications Division, New York_ , vol. 1, p. 32, 1987.
  * Brunel et al. [2019] A. Brunel, D. Mazza, and M. Pagani, “Backpropagation in the simply typed lambda-calculus with linear negation,” _Proceedings of the ACM on Programming Languages_ , vol. 4, no. POPL, pp. 1–27, 2019.
  * Vákár and Smeding [2022] M. Vákár and T. Smeding, “Chad: Combinatory homomorphic automatic differentiation,” _ACM Transactions on Programming Languages and Systems (TOPLAS)_ , vol. 44, no. 3, pp. 1–49, 2022.
  * Huot and Shaikhha [2022] M. Huot and A. Shaikhha, “Denotationally correct, purely functional, efficient reverse-mode automatic differentiation,” 2022. [Online]. Available: https://arxiv.org/abs/2212.09801
  * Krawiec et al. [2022] F. Krawiec, S. P. Jones, N. Krishnaswami, T. Ellis, R. A. Eisenberg, and A. W. Fitzgibbon, “Provably correct, asymptotically efficient, higher-order reverse-mode automatic differentiation.” _Proc. ACM Program. Lang._ , vol. 6, no. POPL, pp. 1–30, 2022.
  * Radul et al. [2022] A. Radul, A. Paszke, R. Frostig, M. Johnson, and D. Maclaurin, “You only linearize once: Tangents transpose to gradients,” _arXiv preprint arXiv:2204.10923_ , 2022.
  * Smeding and Vákár [2023] T. J. Smeding and M. I. Vákár, “Efficient dual-numbers reverse ad via well-known program transformations,” _Proceedings of the ACM on Programming Languages_ , vol. 7, no. POPL, pp. 1573–1600, 2023.
  * Cockett and Cruttwell [2014] J. R. B. Cockett and G. S. Cruttwell, “Differential structure, tangent structure, and sdg,” _Applied Categorical Structures_ , vol. 22, no. 2, pp. 331–417, 2014.
  * Cockett et al. [2019] R. Cockett, G. Cruttwell, J. Gallagher, J.-S. P. Lemay, B. MacAdam, G. Plotkin, and D. Pronk, “Reverse derivative categories,” _arXiv preprint arXiv:1910.07065_ , 2019.
  * Blute et al. [2010] R. Blute, T. Ehrhard, and C. Tasson, “A convenient differential category,” _arXiv preprint arXiv:1006.3140_ , 2010.
  * Lee et al. [2023] W. Lee, X. Rival, and H. Yang, “Smoothness analysis for probabilistic programs with application to optimised variational inference,” _Proceedings of the ACM on Programming Languages_ , vol. 7, no. POPL, pp. 335–366, 2023.
  * Bolte and Pauwels [2020] J. Bolte and E. Pauwels, “A mathematical model for automatic differentiation in machine learning,” _Advances in Neural Information Processing Systems_ , vol. 33, pp. 10 809–10 819, 2020.
  * Chizat and Bach [2018] L. Chizat and F. Bach, “On the global convergence of gradient descent for over-parameterized models using optimal transport,” _Advances in neural information processing systems_ , vol. 31, 2018.
  * Ehrhard et al. [2017] T. Ehrhard, M. Pagani, and C. Tasson, “Measurable cones and stable, measurable functions: a model for probabilistic higher-order programming,” _Proceedings of the ACM on Programming Languages_ , vol. 2, no. POPL, pp. 1–28, 2017.
  * Freer and Roy [2012] C. E. Freer and D. M. Roy, “Computable de finetti measures,” _Annals of Pure and Applied Logic_ , vol. 163, no. 5, pp. 530–546, 2012.
  * Lew et al. [2019] A. K. Lew, M. F. Cusumano-Towner, B. Sherman, M. Carbin, and V. K. Mansinghka, “Trace types and denotational semantics for sound programmable inference in probabilistic languages,” _Proceedings of the ACM on Programming Languages_ , vol. 4, no. POPL, pp. 1–32, 2019.
  * Vákár and Ong [2018] M. Vákár and L. Ong, “On s-finite measures and kernels,” _arXiv preprint arXiv:1810.01837_ , 2018.
  * Lew et al. [2023] A. K. Lew, M. Huot, S. Staton, and V. K. Mansinghka, “Adev: Sound automatic differentiation of expected values of probabilistic programs,” _Proceedings of the ACM on Programming Languages_ , vol. 7, no. POPL, pp. 121–153, 2023.
  * Lee et al. [2018] W. Lee, H. Yu, and H. Yang, “Reparameterization gradient for non-differentiable models,” in _Advances in Neural Information Processing Systems_ , 2018, pp. 5553–5563.
  * Shan and Ramsey [2017] C.-c. Shan and N. Ramsey, “Exact bayesian inference by symbolic disintegration,” in _Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages_ , 2017, pp. 130–144.
  * Cho and Jacobs [2019] K. Cho and B. Jacobs, “Disintegration and bayesian inversion via string diagrams,” _Mathematical Structures in Computer Science_ , vol. 29, no. 7, pp. 938–971, 2019.
  * Narayanan and Shan [2020] P. Narayanan and C.-c. Shan, “Symbolic disintegration with a variety of base measures,” _ACM Transactions on Programming Languages and Systems (TOPLAS)_ , vol. 42, no. 2, pp. 1–60, 2020.
  * Jacobs [1999] B. Jacobs, _Categorical logic and type theory_. Elsevier, 1999.
  * Mitchell and Scedrov [1992] J. C. Mitchell and A. Scedrov, “Notes on sconing and relators,” in _International Workshop on Computer Science Logic_. Springer, 1992, pp. 352–378.
  * Katsumata [2005] S.-y. Katsumata, “A semantic formulation of TT-lifting and logical predicates for computational metalanguage,” in _International Workshop on Computer Science Logic_. Springer, 2005, pp. 87–102.
  * MacLane and Moerdijk [2012] S. MacLane and I. Moerdijk, _Sheaves in geometry and logic: A first introduction to topos theory_. Springer Science & Business Media, 2012.
  * Carboni and Johnstone [1995] A. Carboni and P. Johnstone, “Connected limits, familial representability and artin glueing,” _Mathematical Structures in Computer Science_ , vol. 5, no. 4, pp. 441–459, 1995.
  * Johnstone et al. [2007] P. T. Johnstone, S. Lack, and P. Sobociński, “Quasitoposes, quasiadhesive categories and artin glueing,” in _International Conference on Algebra and Coalgebra in Computer Science_. Springer, 2007, pp. 312–326.
  * Johnstone [2002] P. T. Johnstone, _Sketches of an elephant: A topos theory compendium_. Oxford University Press, 2002, vol. 2.
  * Kammar and McDermott [2018] O. Kammar and D. McDermott, “Factorisation systems for logical relations and monadic lifting in type-and-effect system semantics,” _Electronic notes in theoretical computer science_ , vol. 341, pp. 239–260, 2018.
  * Mityagin [2015] B. Mityagin, “The zero set of a real analytic function,” _arXiv preprint arXiv:1512.07276_ , 2015.

##  Appendix A Language

###  A-A Type System

The type-system for the deterministic language (Section III) is given in
Figure 10.

$\Gamma\vdash x:\tau$
---

$(x:\tau\in\Gamma)$ $\Gamma\vdash c:\tau$ $(c\in\mathcal{C}_{\tau})$
$\Gamma,x:\tau_{1}\vdash{t}:\tau_{2}$ $\Gamma\vdash\lambda
x:\tau_{1}.{t}:\tau_{1}\to\tau_{2}$

$\Gamma\vdash{t}_{1}:\tau_{1}\to\tau_{2}$ $\Gamma\vdash{t}_{2}:\tau_{1}$
---
$\Gamma\vdash{t}_{1}{t}_{2}:\tau_{2}$

$\Gamma\vdash{t}_{1}:\mathbb{B}$ $\Gamma\vdash{t}_{2}:\tau$
$\Gamma\vdash{t}_{3}:\tau$
---
$\Gamma\vdash\mathbf{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}{if}}~{}{t}_{1}~{}\mathbf{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}{then}}~{}{t}_{2}~{}\mathbf{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}{else}}~{}{t}_{3}:\tau$

$\Gamma,f:\tau_{1}\to\tau_{2}\vdash{t}:\tau_{1}\to\tau_{2}$
---
$\Gamma\vdash\mu f:\tau_{1}\to\tau_{2}.{t}:\tau_{1}\to\tau_{2}$

Figure 10: Type system of the deterministic part of the language.
$\mathcal{C}_{\tau}$ denotes the set of primitives of type $\tau$.

###  A-B Operational semantics

Values are given by the following grammar

$v::=x\mid c\mid f\mid\lambda x.{t}\mid\mu f.{t}\mid\langle
v_{1},v_{2}\rangle$

A big step-semantics is given in Figure 11.

$\underline{c}\Downarrow\underline{c}$
---

${t}_{2}\Downarrow\lambda x.{t}$ ${t}_{1}\Downarrow v_{1}$
${t}{}[v_{1}/x{}]\Downarrow v_{2}$
---
${t}_{2}{t}_{1}\Downarrow v_{2}$

$\forall i,{t}_{i}\Downarrow v_{i}$ ${t}\Downarrow f$
---
${t}({t}_{1},\ldots,{t}_{n})\Downarrow\underline{f(v_{1},\ldots,v_{n})}$

${t}_{1}\Downarrow\mathbf{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}{true}}$
${t}_{2}\Downarrow v$
---
$\mathbf{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}{if}}~{}{t}_{1}~{}\mathbf{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}{then}}~{}{t}_{2}~{}\mathbf{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}{else}}~{}{t}_{3}\Downarrow
v$

${t}_{1}\Downarrow\mathbf{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}{false}}$
${t}_{3}\Downarrow v$
---
$\mathbf{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}{if}}~{}{t}_{1}~{}\mathbf{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}{then}}~{}{t}_{2}~{}\mathbf{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}{else}}~{}{t}_{3}\Downarrow
v$

${t}\Downarrow\langle v_{1},v_{2}\rangle$
${t}_{2}[v_{1}/x_{1},v_{2}/x_{2}]\Downarrow v$
---
$\mathbf{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}{case}}\,{t}\,\mathbf{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}{of}}\,\langle
x_{1},x_{2}\rangle\to{t}_{2}\Downarrow v$

${t}{}[\mu f.{t}/f]\Downarrow v$
---
$\mu f.{t}\Downarrow v$

Figure 11: Big step operational semantics of the deterministic part of the
language

##  Appendix B Sound and adequate denotation

####  B-1 Concrete sites and sheaves

Our proof of soundness and adequacy uses reusable machinery developed by
Matache et al. [1]. Their framework requires establishing various properties;
for convenience, in this section, we reproduce the relevant definitions, and
recall the theorem that we will use.

######  Definition B.1 (Reproduced from [1]).

A concrete category is a category $\mathbf{C}$ with a terminal object $1$ such
that the functor $\mathbf{C}(1,-):\mathbf{C}\to\mathbf{Set}$ is faithful.

######  Example B.1.

Let $\mathbf{OpenCont}$ be the category whose objects are open subsets $U$ of
$\mathbb{R}^{n}$ (for all $n\in\mathbb{N}$), and whose morphisms $U\to V$ are
continuous functions. $\mathbb{R}^{0}$ is a terminal object, and
$\mathbf{OpenCont}(\mathbb{R}^{0},-)$ simply sends an open set to its
underlying set, and sends a continuous function to its underlying function.
Therefore, $\mathbf{OpenCont}(\mathbb{R}^{0},-)$ is faithful and
$\mathbf{OpenCont}$ is concrete.

######  Definition B.2 (Reproduced from [1]).

A concrete site $(\mathbf{C},\mathcal{J})$ is a small concrete category
$\mathbf{C}$ with an initial object $0$, together with a coverage
$\mathcal{J}$, which specifies for each object $c$ a set $\mathcal{J}(c)$ of
families of maps with codomain $c$ . We call such a family $\\{f_{i}:c_{i}\to
c\\}_{i\in I}\in\mathcal{J}(c)$ a covering family and say it covers $c$. The
coverage must satisfy the following axioms.

  1. 1.

For every map $h:d\to c$ in $\mathbf{C}$, if $\\{f_{i}:c_{i}\to c\\}_{i\in I}$
covers $c$, then there is a covering family $\\{g_{j}:d_{j}\to d\\}_{j\in
I^{\prime}}$ of $d$ such that every $h\circ g_{j}$ factors through some
$f_{i}$.

  2. 2.

If $\\{f_{i}:c_{i}\to c\\}_{i\in I}$ covers $c$, then $\bigcup_{i\in
I}Im(|f_{i}|)=|c|$.

  3. 3.

the initial object $0$ is covered by the empty set.

  4. 4.

The identity is always covering

  5. 5.

If $\\{f_{i}:c_{i}\to c\\}_{i\in I}\in\mathcal{J}(c)$ and $\\{g_{ij}:c_{ij}\to
c_{i}\\}_{j\in J_{i}}\in\mathcal{J}(c_{i})$ for each $i$, then $\\{f_{i}\circ
g_{ij}:c_{ij}\to c\\}_{i\in I,j\in J_{i}}\in\mathcal{J}(c)$.

######  Example B.2 (Cartesian spaces and smooth maps).

$\mathbf{CartSp}$ is a concrete site, where $\\{f_{i}:U_{i}\to V\\}_{i}$ is a
covering family if $\bigcup_{i}f_{i}(U_{i})=V$, i.e. the images of the $f_{i}$
cover the codomain $V$ in the usual sense.

######  Example B.3.

Similarly to $\mathbf{CartSp}$, $\mathbf{OpenCont}$ is a concrete site, where
$\\{f_{i}:U_{i}\to V\\}_{i}$ is a covering family if
$\bigcup_{i}f_{i}(U_{i})=V$, i.e. the images of the $f_{i}$ cover the codomain
$V$ in the usual sense. Its initial object is the empty set.

######  Example B.4 (Standard Borel spaces).

The category $\mathbf{Sbs}$ has objects the Borel subsets of $\mathbb{R}$ and
morphisms the measurable functions between these objects. It is a concrete
site where the coverage contains the countable sets of inclusions functions
$\\{U_{i}\to U\\}_{i}$ such that $U=\bigcup_{i}U_{i}$ and the $U_{i}$ are
disjoint.

######  Definition B.3 (Reproduced from [1]).

A concrete sheaf $X$ on a concrete site $(\mathbf{C},\mathcal{J})$ is a set
$|X|$, together with, for each object $c\in\mathbf{C}$, a set
$\mathcal{P}_{X}^{c}$ of functions $|c|\to|X|$, such that

  * •

each $\mathcal{P}_{X}^{c}$ contains all the constant functions;

  * •

for any map $h:d\to c\in\mathbf{C}$, and any $g\in\mathcal{P}_{X}^{c}$, the
composite function $g\circ|h|:|d|\to|X|$ is in $\mathcal{P}_{X}^{d}$;

  * •

for each function $g:|c|\to|X|$ and each covering family $\\{f_{i}:c_{i}\to
c\\}_{i\in I}$, if each $g\circ|f_{i}|\in\mathcal{P}_{X}^{c_{i}}$, then
$g:|c|\to|X|\in\mathcal{P}_{X}^{c}$.

A morphism $\alpha:X\to Y$ between concrete sheaves is a function
$\alpha:|X|\to|Y|$ that preserves the structure, namely if
$g\in\mathcal{P}_{X}^{c}$, then $\alpha\circ g\in\mathcal{P}_{Y}^{c}$.

######  Example B.5.

Let $\mathbf{Cont}$ be the category defined as follows. Its objects are pairs
$(X,\mathcal{P}_{X})$ where for each open $U\subseteq\mathbb{R}^{n}$,
$\mathcal{P}_{X}^{U}\subseteq X^{U}$ is closed under the following axioms:

  * •

Constant functions are in $\mathcal{P}_{X}^{U}$

  * •

If $f\in\mathcal{P}_{X}^{U}$ and $g:V\to U$ is continuous, then $f\circ
g\in\mathcal{P}_{X}^{V}$

  * •

If $\\{U_{i}\\}_{i\in\mathbb{N}}$ is an open cover of an open $U$, and for all
$i$, $f_{i}\in\mathcal{P}_{X}^{U_{i}}$, such that for all
$i,j\in\mathbb{N}^{2}$, $f_{i}$ and $f_{j}$ agree on $U_{i}\cap U_{j}$, then
$f:U\to X$ defined by $x\in U_{i}\mapsto f_{i}(x)$, is an element of
$\mathcal{P}_{X}^{U}$.

Its morphisms $X\to Y$ are functions $\alpha:X\to Y$ such that $\alpha\circ
f\in\mathcal{P}_{Y}^{U}$ whenever $f\in\mathcal{P}_{X}^{U}$. Then,
$\mathbf{Cont}$ is a category of concrete sheaves on the concrete site
$\mathbf{OpenCont}$.

######  Example B.6.

Diffeological spaces and Quasi-Borel spaces are examples of categories of
concrete sheaves and morphisms between concrete sheaves. Other examples are
given in Baez and Hoffnung [11].

####  B-2 $\omega$-Concrete sheaves

To interpret recursion, the concrete-sheaf structure will not be sufficient in
general. Instead of evoking what is to my knowledge the yet-to-be-formalised
theory of enriched sheaves over the category of $\omega cpo{}$’s, we continue
with the setting from Matache et al. [1].

######  Definition B.4 (Reproduced from [1]).

An $\omega$-concrete sheaf on a site $(\mathbf{C},\mathcal{J})$ is a concrete
sheaf $X$ together with an ordering $\leq_{X}$ on $|X|$ that equips $X$ with
the structure of$\omega$cpo, such that each $\mathcal{P}_{X}^{c}$ is closed
under pointwise suprema of chains with respect to the pointwise ordering. A
morphism $\alpha:X\to Y$ of $\omega$-concrete sheaves is a continuous function
between $\omega$cpo’s, $\alpha:|X|\to|Y|$, that is also a morphism of concrete
sheaves.

$\omega$-concrete sheaves form a category $\omega
Conc(\mathbf{C},\mathcal{J})$, which is a Cartesian-closed category with
binary coproducts [1].

######  Example B.7.

The category of $\omega$-diffeological spaces [4] and of $\omega$-Quasi-Borel
spaces [2] are examples of categories of $\omega$-concrete sheaves.

####  B-3 Partiality: admissible monos and a partiality monad

To model recursion, we first need to define a (strong) partiality monad
$\mathbf{L}$ on $\omega Conc(\mathbf{C},\mathcal{J})$. There are many choices
for the lifting of the plots, so we parametrize the definition of partiality
monad by a class $\mathcal{M}$ of monomorphisms from the site
$(\mathbf{C},\mathcal{J})$, which we call admissible monos.

Recall that, in any category, monos with the same codomain are preordered. If
$m_{1}:d_{1}\rightarrowtail c,m_{2}:d_{2}\to c$ then $m_{1}\leq m_{2}$ iff
there exists $f:d_{1}\to d_{2}$ such that $m_{2}\circ f=m_{1}$ We write
$Sub(c)$ for the poset quotient of the set of monos with codomain $c$. For any
class $\mathcal{M}$ of monos, we write $Sub_{\mathcal{M}}(c)$ for the full
subposet of $Sub(c)$ whose elements have representatives in $\mathcal{M}$.

######  Definition B.5 (Reproduced from [1]).

A class $\mathcal{M}$ of admissible monos for a concrete site
$(\mathbf{C},\mathcal{J})$ consists of, for each object $c\in\mathbf{C}$, a
set of monos $\mathcal{M}(c)$ with codomain $c$ satisfying the following
conditions

  1. 1.

For all $c\in\mathbf{C},0\to c\in\mathcal{M}(c)$

  2. 2.

$\mathcal{M}$ contains all isomorphisms

  3. 3.

$\mathcal{M}$ is closed under composition

  4. 4.

All pullbacks of $\mathcal{M}$-maps exist and are again in $\mathcal{M}$ (This
makes $Sub_{\mathcal{M}}$ a functor $\mathbf{C}^{op}\to\mathbf{Set}$).

  5. 5.

For each $c$, the function
$Sub_{\mathcal{M}}(c)\to\mathbf{Set}(|c|,\\{0,1\\})$ is componentwise
injective and order-reflecting, and the image of $Sub_{\mathcal{M}}$ is closed
under suprema of $\omega$-chains

  6. 6.

Given an increasing chain in $Sub_{\mathcal{M}}(c)$, $(c_{n}\rightarrowtail
c)_{n\in\mathbb{N}}$, denote its least upper bound by
$c_{\infty}\rightarrowtail c$. Then the closure under precomposition (with any
morphism) of the set $\\{c_{n}\rightarrowtail c_{\infty}\\}_{n\in\mathbb{N}}$
contains a covering family of $c_{\infty}$.

Now, given a class $\mathcal{M}$ of admissible monos, we can define a
partiality monad $L_{\mathcal{M}}$ on the category of $\omega$-concrete
sheaves:

######  Definition B.6 (Reproduced from [1]).

We define the strong partiality monad $\mathbf{L}_{\mathcal{M}}$ associated to
the class of admissible monos $\mathcal{M}$ as

  * •

$|\mathbf{L}_{\mathcal{M}}X|=|X|\sqcup\\{\bot\\}$

  * •

$\forall x\in|X|,\bot\leq_{\mathbf{L}_{\mathcal{M}}X}x$

  * •

$\forall x,x^{\prime}\in|X|,x\leq_{\mathbf{L}_{\mathcal{M}}X}x^{\prime}$ iff
$x\leq_{X}x^{\prime}$

  * •

$\mathcal{P}_{\mathbf{L}_{\mathcal{M}}X}^{c}=\\{g:|c|\to|X|\sqcup\\{\bot\\}~{}|~{}\exists
c^{\prime}\rightarrowtail
c\in\mathcal{M}(c)~{}s.t.~{}g^{-1}(|X|)=Im(|c^{\prime}|)~{}and~{}g|_{Im(|c^{\prime}|)}\in\mathcal{P}_{X}^{c^{\prime}}\\}$

The strong monad structure is exactly the same as the maybe monad on
$\mathbf{Set}$.

######  Proposition B.1 ([1]).

$\mathbf{L}_{\mathcal{M}}:\omega Conc(\mathbf{C},\mathcal{J})\to\omega
Conc(\mathbf{C},\mathcal{J})$ is a strong monad.

####  B-4 Soundness and adequacy

Matache et al. [1] defined a language PCFv, a call-by-value variant of PCF. It
has product, sum types, and a recursion operator similar to ours, and is
presented as a fine-grained call-by-value language. This language is
essentially equivalent to our language, except that we have extra base types
$\mathbf{real}$ and $\mathbb{B}$, and more basic primitives involving these
types. Our conditional is definable using their sum types. They give their
language a standard call-by-value operational semantics, which translates
directly to an operational semantics for our language. In summary, even though
their theorem is stated for PCFv, it directly applies to our language, without
needing further changes or extra proofs, as long as we also interpret our base
types and primitives in the model, as in standard [14].

######  Theorem B.2 ([1]).

A concrete site with a class of admissible monos,
$(\mathbf{C},\mathcal{J},\mathcal{M})$, is a sound and adequate model of PCFv
in $\omega Conc(\mathbf{C},\mathcal{J})$.

Having recalled the general setting of $\omega$-concrete sheaves, we now show
how $\omega$PAP is an instance of this general construction. To do so, we will
show define the category $cPAP$ and show it is a concrete-site (which is the
one for $\omega$PAP) in Section B-6. We will define a set of admissible monos
for $cPAP$ in Section B-7. In order to achieve this, we will need a key
technical proposition (Proposition B.3) and a few other technical lemmas,
proved in Section B-5.

####  B-5 C-analytic sets

The definition of c-analytic sets does not require that the analytic sets that
make up a c-analytic set be disjoint, but it turns out that it is always
possible to partition a c-analytic set into countably many pairwise disjoint
analytic sets.

######  Proposition B.3.

For any c-analytic set $A$, there exists a countable collection of pairwise
disjoint analytic sets $\\{B_{i}\\}_{i\in\mathbb{N}}$ such that
$A=\cup_{i\in\mathbb{N}}B_{i}$.

This is an important property, and most of the rest of this section is devoted
to proving the proposition. The proof is due to Alex Lew.

Let $\\{A_{i}\\}_{i\in\mathbb{N}}$ be a countable set of analytic subsets of
$\mathbb{R}^{n}$.

Each analytic set $A_{i}$ is associated with an open domain $U_{i}$ and a
finite number $J_{i}$ of analytic functions
$\\{f_{ij}\\}_{j\in[1,\dots,J_{i}]}$, so that $A_{i}=\\{x\in U_{i}\mid\forall
j.f_{ij}\leq 0\\}$. Because any open set is a countable union of open balls in
$\mathbb{R}^{n}$, we can assume without loss of generality that the $U_{i}$
are open balls.

######  Definition B.7.

A simple analytic set is a set
$A=\\{x\in\mathcal{B}_{\epsilon}(x_{0})\mid\forall i\leq
I.g_{i}^{+}(x)>0\wedge\forall j\leq J.g_{i}^{-}(x)\leq 0\\}$, for natural
numbers $I$ and $J$ and some $0<\epsilon\leq\infty$ and
$x_{0}\in\mathbb{R}^{n}$.

######  Lemma B.4.

The complement of any simple analytic set is a finite union of pairwise
disjoint simple analytic sets.

###### Proof.

A point $x$ can fail to be in a simple analytic set $A$ for $I+J+1$ mutually
exclusive reasons, each of which applies to a simple analytic set of points:

  1. 1.

If $\epsilon<\infty$, it can fail to lie in $\mathcal{B}_{\epsilon}(x_{0})$.
The set of points outside $\mathcal{B}_{\epsilon}(x_{0})$ is simple analytic:
let $h_{1}^{-}(x)=\epsilon-||x-x_{0}||_{2}$ and consider
$\\{x\in\mathbb{R}^{n}\mid h_{1}^{-}(x)\leq 0\\}$.

  2. 2.

(For each $1\leq i\leq I$.) It can lie within $\mathcal{B}_{\epsilon}(x_{0})$,
and satisfy $g_{n}^{+}(x)>0$ for all $n<i$, but fail to satisfy
$g_{i}^{+}(x)>0$. Let $h_{n}^{+}(x)=g_{n}^{+}(x)$ for $n<i$, and
$h_{1}^{-}(x)=g_{i}^{+}(x)$. Then the set of all such points is
$\\{x\in\mathcal{B}_{\epsilon}(x_{0})\mid\forall n<i.h_{n}^{+}(x)>0\wedge
h_{1}^{-}(x)\leq 0\\}$.

  3. 3.

(For each $1\leq j\leq J$.) It can lie within $\mathcal{B}_{\epsilon}(x_{0})$,
and satisfy $g_{i}^{+}(x)>0$ for all $i\leq I$, and satisfy $g^{-}_{n}(x)\leq
0$ for all $n<j$, but fail to satisfy $g_{j}^{-}(x)\leq 0$. Let
$h^{+}_{i}(x)=g^{+}_{i}(x)$ for all $i\leq I$, $h^{-}_{n}(x)=g^{-}_{n}(x)$ for
all $n<j$, and $h_{I+1}^{+}(x)=g_{j}^{-}(x)$. Then the set of all points to
which *this* reason applies is
$\\{x\in\mathcal{B}_{\epsilon}(x_{0})\mid\forall i\leq
I+1.h^{+}_{i}(x)>0\wedge\forall n<j.h^{-}_{n}(x)\leq 0\\}$.

The union of these simple analytic sets is the complement of $A$. ∎

######  Corollary B.4.1.

If $A_{1},\dots,A_{n}$ are simple analytic sets, then $\overline{\cup_{i\leq
n}A_{i}}$ is a finite union of disjoint analytic sets.

###### Proof.

We have $\overline{\cup A_{i}}=\cap\overline{A_{i}}=\cap(\cup_{m\leq
M_{i}}B_{im})$, where $\\{B_{im}\\}_{m\leq M_{i}}$is a representation of
$A_{i}$’s complement as a disjoint union of finitely many simple analytic
sets. Distributing, this is in turn equal to $\cup_{m_{1}\leq
M_{1}}\dots\cup_{m_{n}\leq M_{n}}(\cap_{i\leq n}B_{im_{i}})$. Each element of
this large union is analytic, because it is the intersection of $n$ analytic
sets. Furthermore, these analytic sets are pairwise disjoint: any pair will
disagree on $m_{i}$ for some $i$, and so the intersection will include
disjoint sets $B_{im_{i}}$ and $B_{im_{i}^{\prime}}$, for $m_{i}\neq
m_{i}^{\prime}$. Because these two sets are disjoint, the overall
intersections will be disjoint. ∎

######  Corollary B.4.2.

If $A_{1},\dots,A_{n}$ are simple analytic sets, then
$A_{n}\setminus\cup_{i<n}A_{i}$ is a finite union of disjoint analytic sets,
each of which is a finite intersection of simple analytic sets.

###### Proof.

$A_{n}\setminus\cup_{i<n}A_{i}=A_{n}\cap(\overline{\cup_{i<n}A_{i}})$, and by
the previous corollary, the right-hand term can be rewritten as a finite union
of disjoint analytic sets $\cup_{i<m}B_{i}$. The intersection is then equal to
$\cup_{i<m}A_{n}\cap B_{i}$. Each element of this finite union is analytic,
because analytic sets are closed under intersection. They are also disjoint,
since the $B_{i}$ are disjoint. ∎

######  Lemma B.5.

Let $A=\cup_{n\in\mathbb{N}}A_{n}$ be a countable union of simple analytic
sets $A_{n}$. Then there are countably many pairwise disjoint analytic sets
$\\{B_{m}\\}_{m\in\mathbb{N}}$ such that $A=\cup_{m\in\mathbb{N}}B_{m}$.

###### Proof.

Consider the countably many disjoint sets
$A^{\prime}_{k}=A_{k}\setminus(\cup_{i<k}A_{i})$. Each $A^{\prime}_{k}$ can
itself be expressed as a countable union of pairwise disjoint sets, by the
previous corollary. ∎

######  Corollary B.5.1.

Every c-analytic set $A$ can be written as a countable disjoint union of
analytic sets.

###### Proof.

Any open domain U can be expressed as a countable union of open balls.
Therefore, in a countable union of arbitrary analytic sets, any analytic set
$A$ with a complicated open domain U can be replaced by countably many
analytic sets with open-ball domains (and the same defining inequalities as
A). We conclude with Lemma B.5, using the fact that a countable family of
countable families is a countable family. ∎

Next, we show a corollary that will be useful in the next section.

######  Corollary B.5.2.

An inclusion $U\subseteq V$ of c-analytic sets $U,V$ is a PAP function $U\to
V$.

###### Proof.

By Corollary B.5.1, we can write $U=\sqcup_{i\in\mathbb{N}}A_{i}$ and
$V=\sqcup_{j\in\mathbb{N}}B_{j}$ where the $A_{i}$ and $B_{j}$ are analytic
sets. Analytic sets are closed under intersection, so $\\{A_{i}\cap
B_{j}\\}_{i\in\mathbb{N},j\in\mathbb{N}}$ is a countable partition of $U$ into
analytic sets. Hence, $\\{(A_{i}\cap
B_{j},id)\\}_{i\in\mathbb{N},j\in\mathbb{N}}$ is a piecewise representation of
the inclusion $U\rightarrowtail V$. ∎

Finally, we show a few closure properties of c-analytic sets.

######  Lemma B.6.

If $f:U\to V$ is analytic and $A\subseteq V$ is analytic, then $f^{-1}(A)$ is
analytic.

###### Proof.

By definition,
$A=\\{x\in(\bigcap_{i}X^{+}_{i})\cap(\bigcap_{j}X^{-}_{j})\mid\forall
i.g^{+}_{i}(x)>0\wedge\forall j.g^{-}_{j}(x)\leq 0\\}$ for some analytic
functions $g^{+}_{i},g^{-}_{j}$. Thus,

$\displaystyle f^{-1}(A)$ $\displaystyle=\\{x\in
f^{-1}\Big{(}(\bigcap_{i}X^{+}_{i})\cap(\bigcap_{j}X^{-}_{j})\Big{)}\mid$
$\displaystyle\qquad\quad\forall i.g^{+}_{i}(f(x))>0\wedge\forall
j.g^{-}_{j}(f(x))\leq 0\\}$
$\displaystyle=\\{x\in(\bigcap_{i}f^{-1}(X^{+}_{i})\cap(\bigcap_{j}f^{-1}(X^{-}_{j}))\mid$
$\displaystyle\qquad\quad\forall i.(g^{+}_{i}\circ f)(x)>0\wedge\forall
j.(g^{-}_{j}\circ f)(x)\leq 0\\}$

As $f$ is analytic, it is continuous and so the sets $f^{-1}(X^{+}_{i})$ and
$f^{-1}(X^{-}_{j})$ are open. And again, as $f$ is analytic, so are the
functions $g^{+}_{i}\circ f$ and $g^{-}_{j}\circ f$. ∎

######  Corollary B.6.1.

If $f:U\to V$ is PAP and $A\subseteq V$ is c-analytic, then $f^{-1}(A)$ is
c-analytic.

###### Proof.

By Corollary B.5.1, we can write $A=\sqcup_{i}A_{i}$ for analytic sets
$A_{i}$. Thus, $f^{-1}(A)=f^{-1}(\sqcup_{i}A_{i})=\sqcup_{i}f^{-1}(A_{i})$ and
it is sufficient to show that each $f^{-1}(A_{i})$ is c-analytic.

$f$ is PAP so there exists a partition $U=\sqcup_{i}B_{i}$ where $B_{i}$ are
analytic sets and analytic functions $f_{i}:U_{i}\to R^{n}$ such that
$f|_{B_{i}}=f_{i}$. Therefore, $f^{-1}(A)=\sqcup_{i}f_{i}^{-1}(A)\cap B_{i}$.
Each $f_{i}^{-1}(A)$ is analytic by Lemma B.6, and so each $f_{i}^{-1}(A)\cap
B_{i}$ is analytic. This means $f^{-1}(A)$ is indeed c-analytic. ∎

####  B-6 Category cPAP

######  Definition B.8 (cPAP).

We call cPAP the category whose objects are c-analytic sets and whose
morphisms are PAP functions between them. Composition is given by the usual
composition of functions.

######  Lemma B.7.

cPAP is a concrete category.

###### Proof.

  * •

cPAP has a terminal object. The analytic set $\mathbb{R}^{0}$ is terminal.

  * •

The functor hom$(1,-):cPAP{}\rightarrow\mathbf{Set}$ is faithful. The functor
is the identity on morphisms.

∎

######  Proposition B.8.

cPAP is a concrete site, where the coverings for a c-analytic set $U$ are
given by countable c-analytic partitions of $U$, i.e.,
$\\{(U_{i})_{i}\mid\cup_{i}U_{i}=U\,\wedge\forall i\neq j,U_{i}\cap
U_{j}=\emptyset\\}$.

###### Proof.

First, note that our definition for the coverings is a well-defined, as
inclusions are PAP functions by Corollary B.5.2.

We now show that the given coverings satisfy the 5 axioms of a concrete site.

  1. 1.

Suppose we have a cPAP morphism $g:C\rightarrow D$, and a c-analytic partition
$\\{D_{i}\\}_{i\in I}$ of $D$. Then we wish to find a partition of $C$ so that
$g$ can be represented as a piecewise gluing of functions with codomains
$D_{i}$. First, note that since they are objects of cPAP, each $D_{i}$ can be
further partitioned into countably many distinct analytic subsets
$\\{D_{ij}\\}_{j\in J_{i}}$, $D_{ij}\subseteq D_{i}$. Furthermore, because $g$
is a morphism, it has a PAP representation $\\{(C_{k},g_{k})\\}_{k\in K}$ for
analytic subsets $C_{k}\subseteq C$ and analytic functions $g_{k}$. For each
$i,j,k$ define $C_{ijk}=\\{c\in C_{k}\mid g_{k}(c)\in D_{ij}\\}$: since
$g_{k}$ is an analytic function and $D_{ij}$ is an analytic set, $C_{ijk}$ is
analytic. Define $g^{*}_{ijk}$ to be the restriction of $g_{k}$ to $C_{ijk}$.
Then $\\{(C_{ijk},g^{*}_{ijk})\\}_{i\in I,j\in J_{i},k\in K}$ is a piecewise
representation of $g$ in which each piece’s codomain is $D_{i}$ for some $i$.

  2. 2.

Let $\\{f_{i}:c_{i}\to c\\}_{i\in I}$ be a covering of $c$. Then
$\bigcup_{i\in I}Im(|f_{i}|)=|c|$. This follows from the definition of
partition.

  3. 3.

The initial object $0$ is covered by the empty set.

  4. 4.

The identity is always covering.

  5. 5.

Let $\\{f_{i}:c_{i}\to c\\}_{i\in I}$ be a covering of $c$ and
$\\{g_{ij}:c_{ij}\to c_{i}\\}_{j\in J_{i}}$ be a cover of $c_{i}$ for each
$i$. Then $\\{f_{i}\circ g_{ij}:c_{ij}\to c\\}_{i\in I,j\in
J_{i}}\in\mathcal{J}(c)$. This also follows from the definition of partition,
and the fact that a countable union of countable sets is countable.

∎

######  Lemma B.9.

cPAP is a subcanonical site.

###### Proof.

Let $X$ be a representable presheaf on cPAP. Then, up to natural isomorphism,
$X$ maps a c-analytic set $A$ to ${\bf cPAP}(A,B)$ for some fixed c-analytic
set $B$. Consider a covering family $\\{(A_{i})\\}_{i\in I}$ for $A$, and a
compatible collection of plots $\phi_{i}\in X(A_{i})$, which can be identified
(via the natural isomorphism) with cPAP morphisms $\phi_{i}:A_{i}\rightarrow
B$. Then we must show that there is a unique $\phi\in X(A)$ whose restriction
to each $A_{i}$ is $\phi_{i}$. To see this, note that each $\phi_{i}$ has a
PAP representation $\\{(A_{ij},\phi_{ij})\\}_{j\in J_{i}}$. By the definition
of a covering family on cPAP, the $A_{i}$ are disjoint, and so
$\\{(A_{ij},\phi_{ij})\\}_{i\in I,j\in J_{i}}$ is a PAP representation; the
$\phi$ we are looking for is the function it represents. ∎

####  B-7 Admissible monos for cPAP

As an admissible set of monos, we choose those given by the monos defined on
an c-analytic subset of their domain of definition. More formally, we define
$\mathcal{M}_{PAP}$ for cPAP as follows:

$\displaystyle\mathcal{M}_{PAP}(B)$ $\displaystyle=\\{m:A\rightarrowtail
B~{}|~{}A\cong A^{\prime},A^{\prime}\text{ is a}$
$\displaystyle\qquad\text{c-analytic subset of }B\\}$

######  Proposition B.10.

$\mathcal{M}_{PAP}$ is an admissible class of monos.

###### Proof.

  1. 1.

For all $c\in\mathbf{C},0\to c\in\mathcal{M}_{PAP}(c)$: the empty-set is
c-analytic.

  2. 2.

$\mathcal{M}_{PAP}$ contains all isomorphisms: clear.

  3. 3.

$\mathcal{M}_{PAP}$ is closed under composition: clear.

  4. 4.

All pullbacks of $\mathcal{M}_{PAP}$-maps exist and are again in
$\mathcal{M}_{PAP}$: this amounts to showing that the preimage $B:=f^{-1}(A)$
for a PAP function $f$ and a c-analytic set $A$ is c-analytic. This is true by
Corollary B.6.1.

  5. 5.

For each $c$, the function
$Sub_{\mathcal{M}}(c)\to\mathbf{Set}(|c|,\\{0,1\\})$ is componentwise
injective and order-reflecting, and the image of $Sub_{\mathcal{M}}$ is closed
under suprema of $\omega$-chains: the function is the identity on sets, and is
thus injective and order-reflecting. Given an omega chain $\\{A_{i}\subseteq
B\\}_{i\in\mathbb{N}}$, we have $i<j\Rightarrow A_{i}\subseteq A_{j}$. Let
$A:=\bigcup_{i\in\mathbb{N}}A_{i}\subseteq B$. It is a countable union of
c-analytic sets and is thus a c-analytic set.

  6. 6.

Given an increasing chain in $Sub_{\mathcal{M}}(c)$, $(c_{n}\rightarrowtail
c)_{n\in\mathbb{N}}$, denote its least upper bound by
$c_{\infty}\rightarrowtail c$. Then the closure under precomposition (with any
morphism) of the set $(c_{n}\rightarrowtail c_{\infty})_{n\in\mathbb{N}}$
contains a covering family of $c_{\infty}$: as shown in the previous point,
$c_{\infty}$ is c-analytic and by Corollary B.5.1, $c_{\infty}=\sqcup A_{i}$
where $A_{i}$ are analytic sets. Thus, $(c_{n}\cap A_{i}\rightarrowtail
c_{\infty})_{n\in\mathbb{N},i\in\mathbb{N}}$ is a covering family of
$c_{\infty}$ that is contained in the closure by precomposition of
$(c_{n}\rightarrowtail c_{\infty})_{n\in\mathbb{N}}$.

∎

###  B-A Soundness and adequacy

We can now prove Theorem II.2:

######  Theorem B.11.

$\omega$PAP has products, coproducts, exponentials and
$\mathbf{L}:\omega\text{PAP}{}\to\omega\text{PAP}{}$ is a strong lifting
monad.

###### Proof.

It follows directly from the fact that we have seen that $\omega\text{PAP}{}$
is a category of $\omega$-concrete sheaves for the concrete site $cPAP{}$
(Proposition B.8), and $\mathbf{L}$ is obtained from an admissible class of
monos on $cPAP{}$ (Propositions B.10 and B.1), by Proposition 7.5 in Matache
et al. [1]. ∎

###### Proof of Theorem II.2.

We apply theorem B.2 to the concrete site
$(PAP,\mathcal{J}_{PAP},\mathcal{M}_{PAP})$ with the admissible class of monos
$\mathcal{M}_{PAP}$. ∎

##  Appendix C Correctness of AD

The main goal of this section is to show Theorem III.2. To do so, we apply the
categorical machinery of fibrations for logical relations developed in [15].
They build on the well-known theory of fibrations [38]. As we follow their
recipe closely, we recall the minimal amount of fibration theory in Section
C-A needed to understand their machinery, which we also reproduce in Section
C-A2 for convenience. We finally use the machinery of fibrations for logical
relations in Section C-B to prove Theorem III.2, our correctness result on AD.

###  C-A Fibrations for logical relations

Roughly, fibrations offer a useful and unifying point of view for reasoning
about generalized predicates on a category. Indeed, the functor
$p:Gl\to\mathbf{C}$ from a glueing/sconing category [39] to the base category
is an example of nice fibration. This justifies to study a categorical version
of logical relations using fibrations. We follow closely this point of view
developed in [15, 40].

####  C-A1 Fibrations

We recall some basic facts from the theory of fibrations [38].

######  Definition C.1 (Reproduced from [38]).

Let $p:\mathbb{E}\to\mathbb{B}$ be a functor. A morphism $f:X\to
Y\in\mathbb{E}$ is Cartesian over $u:I\to J\in\mathbb{B}$ if $pf=u$ and every
$g:Z\to Y\in\mathbb{E}$ for which $pg=u\circ w$ for some $w:pZ\to I$, there is
a unique $h:Z\to X\in\mathbb{E}$ above $w$ with $f\circ h=g$.

######  Definition C.2 (Reproduced from [38]).

A fibration is a functor $p:\mathbb{E}\to\mathbb{B}$ such that for every
$Y\in\mathbb{E}$ and $u:I\to pY\in\mathbb{B}$, there is a Cartesian morphism
$f:X\to Y\in\mathbb{E}$ above $u$. It is also called fibred category or
category (fibred) over $\mathbb{B}$.

######  Example C.1.

Let $\mathbf{Pred}$ be the category whose objects are pairs $(X,S)$ of a set
$X$ and a subset $S\subseteq X$, and morphisms $(X,S)\to(Y,T)$ are functions
$f:X\to Y$ such that $f(S)\subseteq T$. Let $p:\mathbf{Pred}\to\mathbf{Set}$
be the functor that forgets the subsets $S$. It is a fibration.

######  Proposition C.1.

(Change-of-base, [38]) Let $p:\mathbb{\mathbb{B}}\to\mathbb{\mathbb{B}}$ be a
fibration and $K:\mathbb{A}\to\mathbb{B}$ be a functor. Form the pullback in
Cat:

$\textstyle{\mathbb{A}\times_{\mathbb{B}}\mathbb{E}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{K^{*}(p)}$$\textstyle{\mathbb{E}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{p}$$\textstyle{\mathbb{A}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{K}$$\textstyle{\mathbb{B}}$

In this situation, the functor $K^{*}(p)$ is also a fibration.

######  Example C.2.

Consider the functor $K:\mathbf{Set}\times\mathbf{Set}\to\mathbf{Set}$ that
sends a pair of sets to their product. In this case,

$\textstyle{\mathbf{BRel}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{K^{*}(p)}$$\textstyle{\mathbf{Pred}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{p}$$\textstyle{\mathbf{Set}\times\mathbf{Set}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{K}$$\textstyle{\mathbf{Set}}$

$\mathbf{BRel}$ is a category of functions that preserve a binary relation. An
object in $\mathbf{BRel}$ is a binary relation $S\subseteq X\times Y$, and a
morphism $S\subseteq X\times Y\to R\subseteq X_{2}\times Y_{2}$ is a function
$f:X\times Y\to X_{2}\times Y_{2}$ such that for all $(x,y)\in S,f(x,y)\in R$.

######  Proposition C.2.

(Composition, [38]) Let $p:\mathbb{\mathbb{E}}\to\mathbb{\mathbb{B}}$ and
$r:\mathbb{\mathbb{B}}\to\mathbb{\mathbb{A}}$ be fibrations. Then
$rp:\mathbb{\mathbb{E}}\to\mathbb{\mathbb{A}}$ is also a fibration, in which
$f\in\mathbb{E}$ is a Cartesian morphism iff $f$ is a Cartesian morphism for
$p$ and $p(f)$ is is a Cartesian morphism for $r$.

For each $I\in\mathbb{A}$ one obtains a fibration
$p_{I}:\mathbb{E}_{I}=(rp)^{-1}(I)\to\mathbb{B}_{I}=r^{-1}(I)$ by restriction.

######  Definition C.3 (Reproduced from [38]).

Given a fibration $p:\mathbb{\mathbb{E}}\to\mathbb{\mathbb{B}}$, the fibre
category over $I\in\mathbb{B}$ is the subcategory $\mathbb{E}_{I}$ of
$\mathbb{E}$ whose objects are above $I$ and morphisms above $id_{I}$.

######  Definition C.4.

$p:\mathbb{\mathbb{E}}\to\mathbb{\mathbb{B}}$ is an opfibration if
$p^{op}:\mathbb{\mathbb{E}{}^{\text{op}}}\to\mathbb{\mathbb{B}{}^{\text{op}}}$
is a fibration.

######  Example C.3.

$p:\mathbf{Pred}\to\mathbf{Set}$ is an opfibration.

####  C-A2 Fibrations for logical relations for effectful languages

We now recall the setting of fibrations for logical relations from [15].

######  Definition C.5 (Reproduced from [15]).

A partial order bifibration with fibrewise small products is a faithful
functor $p:\mathbb{\mathbb{E}}\to\mathbb{\mathbb{B}}$ such that

  * •

$p$ is a fibration

  * •

$p$ is an opfibration

  * •

each fibre category is a partial order

  * •

each fibre category has small products, and the inverse image functors
(necessarily) preserve them

######  Definition C.6.

A fibration for logical relations over a bi-CCC $\mathbb{B}$ is a partial
order bifibration $p:\mathbb{\mathbb{E}}\to\mathbb{\mathbb{B}}$ with fibrewise
small products such that $\mathbb{E}$ is a bi-CCC and $p$ strictly preserves
the bicartesian-closed structure.