# Pseudorandomness of Sato-Tate Distributions for Elliptic Curves

Chung Pang Mok, Huimin Zheng  School of Mathematical Sciences, Soochow
University, 1 Shi-Zi Street, Suzhou 215006, Jiangsu Province, China
<EMAIL_ADDRESS>Department of Mathematics, Nanjing University, 22 Hankou
Road, Nanjing 210093, Jiangsu Province, China  Jiangsu National Center for
Applied Mathematics<EMAIL_ADDRESS>
###### Abstract.

In this paper we propose conjectures that assert that, the sequence of
Frobenius angles of a given elliptic curve over $\mathbf{Q}$ without complex
multiplication is pseudorandom, in other words that the Frobenius angles are
statistically independently distributed with respect to the Sato-Tate measure.
Numerical evidences are presented to support the conjectures.

###### Key words and phrases:

Elliptic Curves, Sato-Tate Distributions, Pseudorandomness, Discrepancy

###### 2010 Mathematics Subject Classification:

11G05, 11Y70

###### Contents

  1. 1 Introduction and Statement of Conjectures
  2. 2 Numerical Evidences for Conjecture 1.1
  3. 3 Numerical Evidences for Conjecture 1.3, part I
  4. 4 Numerical Evidences for Conjecture 1.3, part II
  5. 5 Conclusion and Final Remarks

##  1\. Introduction and Statement of Conjectures

Let $E$ be an elliptic curve defined over the field $\mathbf{Q}$ of rational
numbers. Assume that $E$ does not have complex multiplication. Denote by $N$
the conductor of $E$, so that $E$ has good reduction at primes $p$ not
dividing $N$. Let $\\{p_{k}\\}_{k\geq 1}$ be the set of primes in ascending
order. For $p_{k}$ not dividing $N$, define as usual the quantity
$a_{p_{k}}:=p_{k}+1-\\#E(\mathbf{F}_{p_{k}})$ (here $\mathbf{F}_{p_{k}}$ is
the finite field of cardinality $p_{k}$, and $E(\mathbf{F}_{p_{k}})$ is the
group of points of $E$ over $\mathbf{F}_{p_{k}}$). By the Hasse bound one has
$|a_{p_{k}}|\leq 2p_{k}^{1/2}$. We define $x_{k}\in[0,1]$ for $k\geq 1$,
referred to as the (normalized) Frobenius angle of $E$ at the prime $p_{k}$,
by the condition:

$a_{p_{k}}=2p_{k}^{1/2}\cos(\pi x_{k})$

if $p_{k}$ does not divide $N$, and we simply define $x_{k}=1/2$ if $p_{k}$
divides $N$. The Sato-Tate conjecture, as established by Taylor et. al. [CHT,
T, HSBT, BLGHT], states that the sequence $\\{x_{k}\\}_{k\geq 1}$ is uniformly
distributed with respect to the Sato-Tate measure on $[0,1]$. Specifically
define the Sato-Tate measure $\mu_{ST}$ on $[0,1]$ (which is a probability
measure) by:

$d\mu_{ST}=2\sin^{2}(\pi u)\,du$

(where $du$ is the Lebesgue measure on $[0,1]$) and for $x_{k}$ as above,
denote by $\delta_{x_{k}}$ the Dirac point mass distribution on $[0,1]$
supported at $x_{k}$. For any integer $K\geq 1$ consider the probability
distribution on $[0,1]$ given by:

(1.1) $\displaystyle\frac{1}{K}\sum_{k=1}^{K}\delta_{x_{k}}$

then the Sato-Tate conjecture states that the probability distribution (1.1)
converges weakly to the Sato-Tate measure $\mu_{ST}$ as $K$ tends to infinity.

In this paper we propose the following refinement of the original Sato-Tate
conjecture, that in addition to uniform distribution, we conjecture that the
sequence $\\{x_{k}\\}_{k\geq 1}$ is pseudorandom, in other words the $x_{k}$’s
are in fact statistically independently distributed with respect to the Sato-
Tate measure. Specifically for any integer $s\geq 1$, denote by
$\mu_{ST}^{[s]}$ the probability measure on $[0,1]^{s}$ given by the product
of $s$ (independent) copies of the original one dimensional Sato-Tate measure
$\mu_{ST}$. We consider the joint distributions for $s$ successive terms from
the sequence $\\{x_{k}\\}_{k\geq 1}$. Thus define $X_{k}\in[0,1]^{s}$ for
$k\geq 1$ to be the $s$-dimensional vector given by:

$X_{k}=(x_{k},x_{k+1},\cdots,x_{k+s-1})$

and denote by $\delta_{X_{k}}$ the Dirac point mass distribution on
$[0,1]^{s}$ that is supported at $X_{k}$.

For integer $K\geq 1$ consider similarly the probability distribution on
$[0,1]^{s}$ given by:

(1.2) $\displaystyle\frac{1}{K}\sum_{k=1}^{K}\delta_{X_{k}}$

We propose the following:

######  Conjecture 1.1.

For any integer $s\geq 1$, the sequence $\\{X_{k}\\}_{k\geq 1}$ is uniformly
distributed with respect to $\mu_{ST}^{[s]}$. In other words the probability
distribution on $[0,1]^{s}$ as given by (1.2), converges weakly to
$\mu_{ST}^{[s]}$, as $K$ tends to infinity.

For $s=1$ this is the original Sato-Tate conjecture (which is already proved).
For $s\geq 2$ this asserts the statistical independence of the distribution of
$s$ successive terms from the sequence $\\{x_{k}\\}_{k\geq 1}$ with respect to
Sato-Tate measure. Thus in terms of statistical distribution, Conjecture 1.1
asserts that, with respect to the Sato-Tate measure, the sequence
$\\{x_{k}\\}_{k\geq 1}$ is $\infty$-distributed in the sense of Knuth, c.f.
Definition C on page 151 of [K]. It is in this sense that we say that the
sequence $\\{x_{k}\\}_{k\geq 1}$ is pseudorandom (with respect to the Sato-
Tate measure). We present numerical evidences for Conjecture 1.1 in section 2
below.

######  Remark 1.2.

Let $E$ and $E^{\prime}$ be elliptic curves over $\mathbf{Q}$ without complex
multiplication, and assume that $E$ and $E^{\prime}$ are non-isogenous. Let
$\\{x_{k}\\}_{k\geq 1}$ and $\\{x_{k}^{\prime}\\}_{k\geq 1}$ be the sequences
of Frobenius angles associated to $E$ and $E^{\prime}$ respectively. Consider
the two dimensional vectors $(x_{k},x_{k}^{\prime})\in[0,1]^{2}$ for $k\geq
1$. Harris [H] established that the sequence
$\\{(x_{k},x_{k}^{\prime})\\}_{k\geq 1}$ is uniformly distributed with respect
to $\mu_{ST}^{[2]}$. By contrast, the setting of our Conjecture 1.1 concerns
the statistical independence of the distribution of Frobenius angles for a
single elliptic curve.

Even more optimistically, we propose the following quantitive refinement of
Conjecture 1.1. Firstly define the extreme discrepancy $D^{[s]}_{K}$ (with
respect to the measure $\mu_{ST}^{[s]}$) for integer $K\geq 1$ as follows. For
any rectangular region $\mathcal{R}\subset[0,1]^{s}$ of the form:

$\mathcal{R}=[a_{1},b_{1})\times\cdots\times[a_{s},b_{s})$

define

$A(\mathcal{R};K)=\\#\\{1\leq k\leq K\,\ |\,\ X_{k}\in\mathcal{R}\\}$

Then define

$D^{[s]}_{K}=\sup_{\mathcal{R}}\Big{|}\frac{A(\mathcal{R};K)}{K}-\mu_{ST}^{[s]}(\mathcal{R})\Big{|}$

where $\mathcal{R}$ ranges over all rectangular regions in $[0,1]^{s}$ as
above.

In general for a point $W=(w^{(1)},\cdots,w^{(s)})\in[0,1]^{s}$, we denote by
$\mathcal{R}_{W}\subset[0,1]^{s}$ the rectangular region:

$\mathcal{R}_{W}=[0,w^{(1)})\times\cdots\times[0,w^{(s)})$

We define the star discrepancy $D_{K}^{*,[s]}$ (with respect to the measure
$\mu_{ST}^{[s]}$) as:

$D^{*,[s]}_{K}=\sup_{W\in[0,1]^{s}}\Big{|}\frac{A(\mathcal{R}_{W};K)}{K}-\mu_{ST}^{[s]}(\mathcal{R}_{W})\Big{|}$

We have $0\leq D_{K}^{[s]},D_{K}^{*,[s]}\leq 1$, and the inequalities (c.f. p.
93 of [KN]):

(1.3) $\displaystyle D_{K}^{*,[s]}\leq D_{K}^{[s]}\leq 2^{s}\cdot
D_{K}^{*,[s]}$

(remark that in loc. cit. the notion of discrepancy with respect to the
Lebesgue measure on $[0,1]^{s}$ is considered, but the same considerations
apply verbatim with respect to the measure $\mu_{ST}^{[s]}$ as well).

The discrepancies $D^{[s]}_{K}$ and $D_{K}^{*,[s]}$ quantify the uniformity of
distribution of the finite set $\\{X_{k}\\}_{k=1}^{K}$ with respect to the
measure $\mu_{ST}^{[s]}$ on $[0,1]^{s}$.

######  Conjecture 1.3.

For any integer $s\geq 1$ and $\epsilon>0$, there exists a constant
$C=C(E,s,\epsilon)$ (depending only on the elliptic curve $E$, $s$ and
$\epsilon$), such that:

$D^{[s]}_{K}\leq CK^{\epsilon-\frac{1}{2}}$

for any integer $K\geq 1$.

Of course, Conjecture 1.3 is interesting only when $\epsilon<\frac{1}{2}$; in
addition it can also be stated equivalently in terms of the star discrepancy
$D_{K}^{*,[s]}$ instead of $D_{K}^{[s]}$, by virtue of the inequalities (1.3).

When $s=1$, Conjecture 1.3 was originally formulated by Akiyama-Tanigawa
(Conjecture 1 of [AT]), which refines the original Sato-Tate conjecture. In
general Conjecture 1.3 is a refinement of Conjecture 1.1; namely that by
standard results on uniform distribution (c.f. p. 93 of [KN]), Conjecture 1.1
is equivalent to the assertion:

$\lim_{K\rightarrow\infty}D^{[s]}_{K}=0.$

Conjecture 1.3 is a very strong statement. Indeed Akiyama-Tanigawa showed that
their conjecture (i.e. Conjecture 1.3 in the case $s=1$) implies the validity
of the Riemann Hypothesis for the $L$-function associated to $E$ (that the
$L$-function associated to $E$ has analytic continuation is of course the
consequence of the modularity of $E$); more generally their conjecture implies
the validity of the Riemann Hypothesis for all the higher symmetric power
$L$-functions associated to $E$, c.f. Poposition 3.5 of [M] for the precise
statement (in loc. cit. suitable analytic hypotheses on the higher symmetric
power $L$-functions are assumed, which are in any case consequences of the
Langlands Functoriality Conjecture with respect to the symmetric power
functorial liftings of the modular form associated to $E$. The existence of
the symmetric power functorial liftings of the modular form associated to $E$
is established by Newton-Thorne [NT] under quite general conditions, including
all semistable $E$ for instance).

Conversely Nagoshi showed (see Theorem 2 of [N]) that the conjecture of
Akiyama-Tanigawa holds (at least) for $\epsilon>1/4$, if one supposes the
validity of the Riemann Hypothesis for all the higher symmetric power
$L$-functions associated to $E$ (again assuming suitable analytic hypotheses
on the higher symmetric power $L$-functions); see also [RT] for the explicit
version. At this moment we do not know whether our Conjecture 1.3 for $s\geq
2$ can be approached using the theory of $L$-functions. Nevertheless we
present numerical evidences for Conjecture 1.3 in section 3 below.

In this paper the computations of the orders of the group of points of
elliptic curves over finite fields were performed using the GP/PARI program.
The rest of the computations were then performed using Mathematica 9.0.

##  2\. Numerical Evidences for Conjecture 1.1

With the setting as in Conjecture 1.1, for continuous function $f$ defined on
$[0,1]^{s}$, we would like to test whether:

$\frac{1}{K}\sum_{k=1}^{K}f(X_{k})\stackrel{{\scriptstyle?}}{{\rightarrow}}\int_{[0,1]^{s}}f\,d\mu_{ST}^{[s]}$

as $K$ tends to infinity.

We consider the following six elliptic curves over $\mathbf{Q}$ without
complex multiplication, taken from the $L$-functions and modular forms
database, whose affine Weierstrass equations are given as follows, with
conductor $N$ and Mordell-Weil rank $r$ as indicated:

$E_{1}:y^{2}+y=x^{3}-x^{2},\,\ N=11,\,\ r=0$

$E_{2}:y^{2}+y=x^{3}-x,\,\ N=37,\,\ r=1$

$E_{3}:y^{2}+xy=x^{3}+1,\,\ N=433,\,\ r=2$

$E_{4}:y^{2}+y=x^{3}-7x+6,\,\ N=5077,\,\ r=3$

$E_{5}:y^{2}+y=x^{3}-7x+36,\,\ N=545723,\,\ r=4$

$E_{6}:y^{2}+y=x^{3}-79x+342,\,\ N=19047851,\,\ r=5$

We denote the coordinates on $[0,1]^{s}$ as $u^{(1)},\cdots,u^{(s)}$. For
testing statistical independence, it is good enough to choose test functions
$f$ of the form:

$f(u^{(1)},\cdots,u^{(s)})=\prod_{i=1}^{s}f_{i}(u^{(i)})$

for continuous functions $f_{i}$ on $[0,1]$, in which case we have

(2.1)
$\displaystyle\int_{[0,1]^{s}}f\,d\mu_{ST}^{[s]}=\prod_{i=1}^{s}\int_{[0,1]}f_{i}(u^{(i)})\cdot
2\sin^{2}(\pi u^{(i)})\,du^{(i)}$

We first consider the case $s=10$. Define the function $f^{[10]}$ on
$[0,1]^{10}$:

$\displaystyle f^{[10]}(u^{(1)},\cdots,u^{(10)})$ $\displaystyle=$
$\displaystyle\ln(2+u^{(1)})\cdot\ln(3+u^{(2)})\cdot\exp(-u^{(3)})\cdot(1+u^{(4)})^{2}\cdot(2+u^{(5)})\cdot$
$\displaystyle\sqrt{2+u^{(6)}}\cdot\sqrt{3+u^{(7)}}\cdot(4+u^{(8)})^{\frac{1}{3}}\cdot(8+u^{(9)})^{\frac{1}{4}}\cdot\exp(\sqrt{1+u^{(10)}})$

Using the command NIntegrate of Mathematica, the numerical value of the
integral $\int_{[0,1]^{10}}f^{[10]}\,d\mu_{ST}^{[10]}$ is computed as in (2.1)
to be:

$\int_{[0,1]^{10}}f^{[10]}\,d\mu_{ST}^{[10]}\stackrel{{\scriptstyle.}}{{=}}114.076$

The numerical results for $\frac{1}{K}\sum_{k=1}^{K}f^{[10]}(X_{k})$ for
$K=5000$, $K=10000$, $K=20000$, $K=50000$, and $K=100000$ are tabulated in
Figure 1 below.

| $K=5000$ | $K=10000$ | $K=20000$ | $K=50000$ | $K=100000$
---|---|---|---|---|---
$E_{1}$ | 113.87 | 113.753 | 113.903 | 114.009 | 114.032
$E_{2}$ | 114.196 | 114.08 | 114.074 | 114.128 | 114.181
$E_{3}$ | 114.534 | 114.576 | 114.493 | 114.154 | 114.237
$E_{4}$ | 115.375 | 115.011 | 114.683 | 114.441 | 114.248
$E_{5}$ | 116.127 | 115.137 | 114.499 | 114.62 | 114.474
$E_{6}$ | 116.559 | 115.371 | 115.312 | 114.471 | 114.519
Figure 1. Numerical results for $\frac{1}{K}\sum_{k=1}^{K}f^{[10]}(X_{k})$

We next consider examples with larger values of $s$. For $s\geq 1$ define the
function $g^{[s]}$ on $[0,1]^{s}$ given by:

$\displaystyle
g^{[s]}(u^{(1)},\cdots,u^{(s)})=100\cdot\prod_{i=1}^{s}\exp(-u^{(i)}/i)$

We have:

$\displaystyle\int_{[0,1]^{s}}g^{[s]}\,d\mu_{ST}^{[s]}$ $\displaystyle=$
$\displaystyle 100\cdot\prod_{i=1}^{s}\int_{[0,1]}\exp(-u^{(i)}/i)\cdot
2\sin^{2}(\pi u^{(i)})\,du^{(i)}$ $\displaystyle=$ $\displaystyle
100\cdot\prod_{i=1}^{s}\left(\big{(}1-\exp(-1/i)\big{)}\cdot\frac{4\pi^{2}i^{3}}{1+4\pi^{2}i^{2}}\right)$

The numerical values of $\int_{[0,1]^{s}}g^{[s]}\,d\mu_{ST}^{[s]}$ for
$s=500$, $s=1000$, and $s=2000$, are computed as in (2.2) to be:

$\displaystyle\int_{[0,1]^{500}}g^{[500]}\,d\mu_{ST}^{[500]}\stackrel{{\scriptstyle.}}{{=}}3.44034$
$\displaystyle\int_{[0,1]^{1000}}g^{[1000]}\,d\mu_{ST}^{[1000]}\stackrel{{\scriptstyle.}}{{=}}2.43333$
$\displaystyle\int_{[0,1]^{2000}}g^{[2000]}\,d\mu_{ST}^{[2000]}\stackrel{{\scriptstyle.}}{{=}}1.72086$

While the numerical results for $\frac{1}{K}\sum_{k=1}^{K}g^{[s]}(X_{k})$ for
$K=5000$, $K=10000$, $K=20000$, $K=50000$, and $K=100000$, in the cases
$s=500$, $s=1000$, and $s=2000$ respectively, are tabulated in Figures 2, 3, 4
below.

| $K=5000$ | $K=10000$ | $K=20000$ | $K=50000$ | $K=100000$
---|---|---|---|---|---
$E_{1}$ | 3.4513 | 3.4541 | 3.45074 | 3.4417 | 3.44034
$E_{2}$ | 3.4208 | 3.43017 | 3.43423 | 3.43228 | 3.42744
$E_{3}$ | 3.4013 | 3.38951 | 3.40058 | 3.43055 | 3.42734
$E_{4}$ | 3.33751 | 3.36335 | 3.38431 | 3.40763 | 3.42225
$E_{5}$ | 3.27776 | 3.35011 | 3.40524 | 3.3932 | 3.40618
$E_{6}$ | 3.24535 | 3.33898 | 3.33186 | 3.4024 | 3.39838
Figure 2. Numerical results for $\frac{1}{K}\sum_{k=1}^{K}g^{[500]}(X_{k})$

| $K=5000$ | $K=10000$ | $K=20000$ | $K=50000$ | $K=100000$
---|---|---|---|---|---
$E_{1}$ | 2.4422 | 2.44414 | 2.44149 | 2.43447 | 2.43337
$E_{2}$ | 2.41925 | 2.42568 | 2.42922 | 2.42732 | 2.42337
$E_{3}$ | 2.40409 | 2.39574 | 2.40298 | 2.426 | 2.42349
$E_{4}$ | 2.35616 | 2.37465 | 2.39071 | 2.40813 | 2.4195
$E_{5}$ | 2.31073 | 2.3628 | 2.40653 | 2.39708 | 2.40692
$E_{6}$ | 2.28672 | 2.35609 | 2.3498 | 2.40406 | 2.40116
Figure 3. Numerical results for $\frac{1}{K}\sum_{k=1}^{K}g^{[1000]}(X_{k})$

| $K=5000$ | $K=10000$ | $K=20000$ | $K=50000$ | $K=100000$
---|---|---|---|---|---
$E_{1}$ | 1.72737 | 1.72919 | 1.72717 | 1.72179 | 1.72091
$E_{2}$ | 1.71064 | 1.71501 | 1.71777 | 1.71642 | 1.71329
$E_{3}$ | 1.69752 | 1.6939 | 1.69775 | 1.71531 | 1.71333
$E_{4}$ | 1.66527 | 1.6769 | 1.68915 | 1.70186 | 1.71047
$E_{5}$ | 1.63056 | 1.66685 | 1.70142 | 1.6933 | 1.70075
$E_{6}$ | 1.61208 | 1.66286 | 1.65744 | 1.69837 | 1.69624
Figure 4. Numerical results for $\frac{1}{K}\sum_{k=1}^{K}g^{[2000]}(X_{k})$

In a similar way for $s\geq 1$ define the function $h^{[s]}$ on $[0,1]^{s}$
given by:

$\displaystyle h^{[s]}(u^{(1)},\cdots,u^{(s)})$ $\displaystyle=$
$\displaystyle 100\cdot\prod_{i=1}^{s}\cos\left(\frac{\pi
u^{(i)}}{2i^{1/2}}\right)$

We have:

$\displaystyle\int_{[0,1]^{s}}h^{[s]}\,d\mu_{ST}^{[s]}$ $\displaystyle=$
$\displaystyle 100\cdot\prod_{i=1}^{s}\int_{[0,1]}\cos\left(\frac{\pi
u^{(i)}}{2i^{1/2}}\right)\cdot 2\sin^{2}(\pi u^{(i)})\,du^{(i)}$
$\displaystyle=$ $\displaystyle
100\cdot\prod_{i=1}^{s}\left(\frac{2i^{1/2}}{\pi}\cdot\sin\left(\frac{\pi}{2i^{1/2}}\right)\cdot\frac{16i}{16i-1}\right)$

The numerical values of $\int_{[0,1]^{s}}h^{[s]}\,d\mu_{ST}^{[s]}$ for
$s=500$, $s=1000$, $s=1500$, and $s=2000$, are computed as in (2.3) to be:

$\displaystyle\int_{[0,1]^{500}}h^{[500]}\,d\mu_{ST}^{[500]}\stackrel{{\scriptstyle.}}{{=}}8.814$
$\displaystyle\int_{[0,1]^{1000}}h^{[1000]}\,d\mu_{ST}^{[1000]}\stackrel{{\scriptstyle.}}{{=}}6.92239$
$\displaystyle\int_{[0,1]^{1500}}h^{[1500]}\,d\mu_{ST}^{[1500]}\stackrel{{\scriptstyle.}}{{=}}6.0099$
$\displaystyle\int_{[0,1]^{2000}}h^{[2000]}\,d\mu_{ST}^{[2000]}\stackrel{{\scriptstyle.}}{{=}}5.43635$

While the numerical results for $\frac{1}{K}\sum_{k=1}^{K}h^{[s]}(X_{k})$ for
$K=5000$, $K=10000$, $K=20000$, $K=50000$, and $K=100000$, in the cases
$s=500$, $s=1000$, $s=1500$, and $s=2000$ respectively, are tabulated in
Figures 5, 6, 7, 8 below.

Summing up: the numerical results of this section supply evidences for the
validity of Conjecture 1.1; this conjecture can be described as saying that,
the sequence $\\{x_{k}\\}_{k\geq 1}$ is a pseudorandom sequence in $[0,1]$
with distribution law given by the Sato-Tate measure.

| $K=5000$ | $K=10000$ | $K=20000$ | $K=50000$ | $K=100000$
---|---|---|---|---|---
$E_{1}$ | $8.84564$ | $8.8739$ | $8.85475$ | $8.82749$ | $8.81591$
$E_{2}$ | $8.74331$ | $8.7891$ | $8.80022$ | $8.78814$ | $8.7736$
$E_{3}$ | $8.70232$ | $8.63423$ | $8.67626$ | $8.79667$ | $8.77114$
$E_{4}$ | $8.49599$ | $8.54784$ | $8.62823$ | $8.69612$ | $8.76489$
$E_{5}$ | $8.27357$ | $8.53379$ | $8.69698$ | $8.67127$ | $8.70012$
$E_{6}$ | $8.18894$ | $8.50111$ | $8.45486$ | $8.70109$ | $8.69085$
Figure 5. Numerical results for $\frac{1}{K}\sum_{k=1}^{K}h^{[500]}(X_{k})$

| $K=5000$ | $K=10000$ | $K=20000$ | $K=50000$ | $K=100000$
---|---|---|---|---|---
$E_{1}$ | $6.9513$ | $6.97341$ | $6.95763$ | $6.93425$ | $6.9241$
$E_{2}$ | $6.86542$ | $6.90182$ | $6.91247$ | $6.90096$ | $6.8879$
$E_{3}$ | $6.82891$ | $6.77459$ | $6.80619$ | $6.90821$ | $6.8863$
$E_{4}$ | $6.65655$ | $6.69763$ | $6.76587$ | $6.822$ | $6.88$
$E_{5}$ | $6.47181$ | $6.67989$ | $6.82385$ | $6.80146$ | $6.8251$
$E_{6}$ | $6.40304$ | $6.65958$ | $6.61765$ | $6.82616$ | $6.8182$
Figure 6. Numerical results for $\frac{1}{K}\sum_{k=1}^{K}h^{[1000]}(X_{k})$

| $K=5000$ | $K=10000$ | $K=20000$ | $K=50000$ | $K=100000$
---|---|---|---|---|---
$E_{1}$ | $6.03675$ | $6.0559$ | $6.04206$ | $6.02086$ | $6.01151$
$E_{2}$ | $5.96016$ | $5.99199$ | $6.00129$ | $5.99081$ | $5.97872$
$E_{3}$ | $5.9214$ | $5.87986$ | $5.90473$ | $5.9971$ | $5.97718$
$E_{4}$ | $5.77546$ | $5.80653$ | $5.86934$ | $5.91933$ | $5.97276$
$E_{5}$ | $5.60953$ | $5.7892$ | $5.92279$ | $5.90058$ | $5.92183$
$E_{6}$ | $5.54555$ | $5.77334$ | $5.73411$ | $5.92231$ | $5.91537$
Figure 7. Numerical results for $\frac{1}{K}\sum_{k=1}^{K}h^{[1500]}(X_{k})$

| $K=5000$ | $K=10000$ | $K=20000$ | $K=50000$ | $K=100000$
---|---|---|---|---|---
$E_{1}$ | $5.46061$ | $5.47935$ | $5.46676$ | $5.4467$ | $5.4379$
$E_{2}$ | $5.39035$ | $5.41982$ | $5.42836$ | $5.41881$ | $5.4073$
$E_{3}$ | $5.3513$ | $5.31787$ | $5.33875$ | $5.42458$ | $5.4058$
$E_{4}$ | $5.2241$ | $5.24905$ | $5.30693$ | $5.35259$ | $5.4022$
$E_{5}$ | $5.06843$ | $5.23096$ | $5.35741$ | $5.33487$ | $5.3545$
$E_{6}$ | $5.01111$ | $5.21909$ | $5.18121$ | $5.35458$ | $5.3483$
Figure 8. Numerical results for $\frac{1}{K}\sum_{k=1}^{K}h^{[2000]}(X_{k})$

##  3\. Numerical Evidences for Conjecture 1.3, part I

For numerics related to Conjecture 1.3 in the case $s=1$ (i.e. the original
conjecture of Akiyama-Tanigawa), we refer to [AT] and [St]. To test Conjecture
1.3 directly one would need to evaluate the values the $D_{K}^{[s]}$ or
$D_{K}^{*,[s]}$ for $K$ large. But in higher dimensions $s$ there are serious
combinatorial difficulties in computing (even just numerically) the values of
$D_{K}^{[s]}$ or $D_{K}^{*,[s]}$; this is the well known phenomenon known as
the Curse of Dimensionality.

We first note that, Conjecture 1.3 is obviously equivalent to the statement:

$\liminf_{K\rightarrow\infty}-\frac{\ln D^{[s]}_{K}}{\ln K}\geq\frac{1}{2}$

(and similarly with $D_{K}^{[s]}$ being replaced by $D_{K}^{*,[s]}$).

######  Proposition 3.1.

Let $f$ be a function defined on $[0,1]^{s}$, which is of bounded variation in
the sense of Hardy and Krause. Then Conjecture 1.3 implies:

$\liminf_{K\rightarrow\infty}-\frac{\ln\big{|}\frac{1}{K}\sum_{k=1}^{K}f(X_{k})-\int_{[0,1]^{s}}f\,d\mu_{ST}^{[s]}\big{|}}{\ln
K}\geq\frac{1}{2}$

###### Proof.

This is an immediate consequence of the Koksma-Hlawka inequality (c.f. p. 151
of [KN] and p. 967 of [Ni2]):

$\Big{|}\frac{1}{K}\sum_{k=1}^{K}f(X_{k})-\int_{[0,1]^{s}}f\,d\mu_{ST}^{[s]}\Big{|}\leq
V(f)\cdot D_{K}^{*,[s]}$

where $V(f)$ is the total variation of $f$ in the sense of Hardy and Krause
(the version of the Koksma-Hlawka inequality stated in loc. cit. is with
respect to the Lebesgue measure on $[0,1]^{s}$, but the same proof works
verbatim with respect to the measure $\mu_{ST}^{[s]}$ on $[0,1]^{s}$). ∎

In view of Proposition 3.1. we may then test Conjecture 1.3 indirectly as
follows. With $f$ defined on $[0,1]^{s}$ as above (of bounded variation in the
sense of Hardy and Krause), denote the relative error:

$\operatorname{RelErr}(f,K)=\frac{\frac{1}{K}\sum_{k=1}^{K}f(X_{k})-\int_{[0,1]^{s}}f\,d\mu_{ST}^{[s]}}{\int_{[0,1]^{s}}f\,d\mu_{ST}^{[s]}}$

(assuming that the integral is nonzero).

Then we evaluate:

$-\frac{\ln|\operatorname{RelErr}(f,K)|}{\ln K}$

with $K$ being large. By virtue of Proposition 3.1, Conjecture 1.3 implies
that

$\liminf_{K\rightarrow\infty}\frac{-\ln|\operatorname{RelErr}(f,K)|}{\ln
K}\geq\frac{1}{2}$

In the following numerical examples the dimensions $s$ and the test functions
$f$ on $[0,1]^{s}$ are chosen as in section 2, namely:

$f^{[10]},g^{[500]},g^{[1000]},g^{[2000]},h^{[500]},h^{[1000]},h^{[1500]},h^{[2000]}$

The results are tabulated in Figures 9 -16 below.

| $K=5\times 10^{5}$ | $K=10^{6}$ | $K=2\times 10^{6}$ | $K=5\times 10^{6}$ | $K=10^{7}$
---|---|---|---|---|---
$E_{1}$ | 0.69949 | 0.679386 | 0.630927 | 0.66101 | 0.691336
$E_{2}$ | 0.633969 | 0.581946 | 0.687151 | 0.641671 | 0.670621
$E_{3}$ | 0.573905 | 0.57178 | 0.585748 | 0.576866 | 0.592804
$E_{4}$ | 0.523103 | 0.542605 | 0.531523 | 0.566703 | 0.525969
$E_{5}$ | 0.514324 | 0.516659 | 0.513771 | 0.50841 | 0.504189
$E_{6}$ | 0.494667 | 0.524282 | 0.505647 | 0.490742 | 0.491219
Figure 9. Numerical results for
$-\frac{\ln|\operatorname{RelErr}(f^{[10]},K)|}{\ln K}$

| $K=5\times 10^{5}$ | $K=10^{6}$ | $K=2\times 10^{6}$ | $K=5\times 10^{6}$ | $K=10^{7}$
---|---|---|---|---|---
$E_{1}$ | 0.638723 | 0.648979 | 0.631947 | 0.862372 | 0.808676
$E_{2}$ | 0.575948 | 0.505878 | 0.633176 | 0.552754 | 0.543251
$E_{3}$ | 0.487867 | 0.496663 | 0.514921 | 0.501386 | 0.498532
$E_{4}$ | 0.444677 | 0.462 | 0.462372 | 0.493716 | 0.460063
$E_{5}$ | 0.431359 | 0.436573 | 0.438725 | 0.445434 | 0.44006
$E_{6}$ | 0.404953 | 0.436986 | 0.430817 | 0.421285 | 0.426719
Figure 10. Numerical results for
$-\frac{\ln|\operatorname{RelErr}(g^{[500]},K)|}{\ln K}$

| $K=5\times 10^{5}$ | $K=10^{6}$ | $K=2\times 10^{6}$ | $K=5\times 10^{6}$ | $K=10^{7}$
---|---|---|---|---|---
$E_{1}$ | 0.631169 | 0.645835 | 0.630361 | 0.712336 | 0.706233
$E_{2}$ | 0.567706 | 0.497695 | 0.617072 | 0.544564 | 0.534925
$E_{3}$ | 0.480746 | 0.489362 | 0.507584 | 0.494107 | 0.492241
$E_{4}$ | 0.437471 | 0.455814 | 0.455769 | 0.487224 | 0.453975
$E_{5}$ | 0.424289 | 0.429748 | 0.432216 | 0.439139 | 0.434175
$E_{6}$ | 0.39818 | 0.430663 | 0.424525 | 0.414925 | 0.420545
Figure 11. Numerical results for
$-\frac{\ln|\operatorname{RelErr}(g^{[1000]},K)|}{\ln K}$

| $K=5\times 10^{5}$ | $K=10^{6}$ | $K=2\times 10^{6}$ | $K=5\times 10^{6}$ | $K=10^{7}$
---|---|---|---|---|---
$E_{1}$ | 0.627366 | 0.638355 | 0.622921 | 0.675519 | 0.66696
$E_{2}$ | 0.559385 | 0.490252 | 0.605272 | 0.53634 | 0.526713
$E_{3}$ | 0.473656 | 0.482631 | 0.500549 | 0.487117 | 0.485837
$E_{4}$ | 0.430963 | 0.449776 | 0.449301 | 0.480237 | 0.447863
$E_{5}$ | 0.418162 | 0.423543 | 0.426154 | 0.4331 | 0.428402
$E_{6}$ | 0.391767 | 0.424534 | 0.418375 | 0.408966 | 0.414847
Figure 12. Numerical results for
$-\frac{\ln|\operatorname{RelErr}(g^{[2000]},K)|}{\ln K}$

| $K=5\times 10^{5}$ | $K=10^{6}$ | $K=2\times 10^{6}$ | $K=5\times 10^{6}$ | $K=10^{7}$
---|---|---|---|---|---
$E_{1}$ | 0.606447 | 0.634717 | 0.596622 | 0.769728 | 0.72325
$E_{2}$ | 0.592215 | 0.483297 | 0.643853 | 0.573784 | 0.538485
$E_{3}$ | 0.469397 | 0.46504 | 0.491604 | 0.482104 | 0.506944
$E_{4}$ | 0.428098 | 0.451091 | 0.44635 | 0.467237 | 0.44823
$E_{5}$ | 0.417505 | 0.421578 | 0.424573 | 0.429395 | 0.423905
$E_{6}$ | 0.398343 | 0.426324 | 0.412744 | 0.399427 | 0.40276
Figure 13. Numerical results for
$-\frac{\ln|\operatorname{RelErr}(h^{[500]},K)|}{\ln K}$

| $K=5\times 10^{5}$ | $K=10^{6}$ | $K=2\times 10^{6}$ | $K=5\times 10^{6}$ | $K=10^{7}$
---|---|---|---|---|---
$E_{1}$ | 0.599239 | 0.632049 | 0.594434 | 0.699701 | 0.677617
$E_{2}$ | 0.58362 | 0.4755 | 0.618896 | 0.561171 | 0.528059
$E_{3}$ | 0.462718 | 0.458196 | 0.484627 | 0.474634 | 0.499336
$E_{4}$ | 0.421188 | 0.445555 | 0.440249 | 0.46107 | 0.442045
$E_{5}$ | 0.410704 | 0.414996 | 0.418179 | 0.423116 | 0.41825
$E_{6}$ | 0.391969 | 0.420306 | 0.406692 | 0.393337 | 0.396837
Figure 14. Numerical results for
$-\frac{\ln|\operatorname{RelErr}(h^{[1000]},K)|}{\ln K}$

| $K=5\times 10^{5}$ | $K=10^{6}$ | $K=2\times 10^{6}$ | $K=5\times 10^{6}$ | $K=10^{7}$
---|---|---|---|---|---
$E_{1}$ | 0.596406 | 0.624722 | 0.588404 | 0.675777 | 0.659381
$E_{2}$ | 0.578855 | 0.471502 | 0.612237 | 0.555763 | 0.523419
$E_{3}$ | 0.458443 | 0.454467 | 0.480825 | 0.470964 | 0.495892
$E_{4}$ | 0.41748 | 0.442316 | 0.436737 | 0.457416 | 0.438645
$E_{5}$ | 0.40721 | 0.411428 | 0.414829 | 0.419795 | 0.415218
$E_{6}$ | 0.388235 | 0.416779 | 0.403099 | 0.390014 | 0.393701
Figure 15. Numerical results for
$-\frac{\ln|\operatorname{RelErr}(h^{[1500]},K)|}{\ln K}$

| $K=5\times 10^{5}$ | $K=10^{6}$ | $K=2\times 10^{6}$ | $K=5\times 10^{6}$ | $K=10^{7}$
---|---|---|---|---|---
$E_{1}$ | 0.594196 | 0.620986 | 0.584018 | 0.670973 | 0.654911
$E_{2}$ | 0.574501 | 0.468545 | 0.607293 | 0.55214 | 0.520405
$E_{3}$ | 0.456099 | 0.452267 | 0.478601 | 0.468548 | 0.493642
$E_{4}$ | 0.415082 | 0.440149 | 0.434365 | 0.45504 | 0.436376
$E_{5}$ | 0.404872 | 0.409085 | 0.412494 | 0.417499 | 0.413082
$E_{6}$ | 0.385872 | 0.414499 | 0.40085 | 0.387842 | 0.391689
Figure 16. Numerical results for
$-\frac{\ln|\operatorname{RelErr}(h^{[2000]},K)|}{\ln K}$

##  4\. Numerical Evidences for Conjecture 1.3, part II

Finally we test Conjecture 1.3 directly for the dimensions $s=2$ and $s=3$. We
first recall the following general result of Niederreiter [Ni1] in order to
compute the star discrepancy $D_{K}^{*,[s]}$ of
$\\{X_{k}\\}_{k=1}^{K}\subset[0,1]^{s}$ (with respect to the measure
$\mu_{ST}^{[s]}$).

For $1\leq i\leq s$, denote by
$0=\beta^{(i)}_{1}<\cdots<\beta^{(i)}_{n_{i}}=1$ the set of distinct values of
the set of $i$-th coordinates of the points $\\{X_{k}\\}_{k=1}^{K}$, with the
values $0$ and $1$ being included. Denote by $\mathfrak{q}$ the collection of
rectangular regions $Q\subset[0,1]^{s}$ of the form:

$Q=\prod_{i=1}^{s}(\beta^{(i)}_{j_{i}},\beta^{(i)}_{j_{i}+1}],\,\ 1\leq
j_{i}<n_{i}\mbox{ for }1\leq i\leq s$

which thus forming a partition of $(0,1]^{s}$. For $Q$ as above, denote:

$Y(Q)=(\beta^{(1)}_{j_{1}+1},\cdots,\beta^{(s)}_{j_{s}+1})\in[0,1]^{s}$

the upper end point of $Q$, and

$Z(Q)=(\beta^{(1)}_{j_{1}},\cdots,\beta^{(s)}_{j_{s}})\in[0,1]^{s}$

the lower end point of $Q$.

We then have:

######  Proposition 4.1.

The star discrepancy $D_{K}^{*,[s]}$ is equal to:

$\displaystyle\max_{Q\in\mathfrak{q}}\Big{(}\max\Big{(}\Big{|}\frac{A(\mathcal{R}_{Y(Q)};K)}{K}-\mu_{ST}^{[s]}(\mathcal{R}_{Y(Q)})\Big{|},\Big{|}\frac{A(\mathcal{R}_{Z(Q)};K)}{K}-\mu_{ST}^{[s]}(\mathcal{R}_{Z(Q)})\Big{|}\Big{)}\Big{)}$

###### Proof.

This is Theorem 2 of [Ni1]. In loc. cit. it is stated with respect to the
Lebesgue measure on $[0,1]^{s}$, but the argument works verbatim with respect
to the measure $\mu_{ST}^{[s]}$. ∎

######  Remark 4.2.

To compute $D_{K}^{*,[s]}$ using Proposition 4.1 (i.e. Theorem 2 of [Ni1])
requires the evaluation of $O(K^{s})$ terms. Although there are algorithms
that improve upon that of [Ni1] for computing the star discrepancy (c.f. for
example [DE]), the time complexity of the known algorithms is still
exponential in terms of the dimension $s$; this is an instance of the Curse of
Dimensionality. In fact it is known that the computation of star discrepancy
belongs to the class of NP-hard problems [GSW].

Below we use Proposition 4.1 to compute the numerical values of
$D_{K}^{*,[s]}$ and hence test Conjecture 1.3 (with respect to
$D_{K}^{*,[s]}$), in the cases $s=2$ and $s=3$. The results are tabulated in
Figures 17, 18 below.

Summing up: the numerical results of section 3 and section 4 supply evidences
for the validity of Conjecture 1.3. It is a refinement of Conjecture 1.1, and
can be regarded as a qualitative form, of the Law of Iterated Logarithm for
random numbers (c.f. Chapter 7 of [Ni3]). In particular, Conjecture 1.3
implies that, with respect to the Sato-Tate measure, the sequence of Frobenius
angles of an elliptic curve over $\mathbf{Q}$ without complex multiplication
forms a pseudorandom sequence in $[0,1]$ with strong randomness property, (at
least) as far as statistical distribution is concerned.

| $K=5\times 10^{3}$ | $K=10^{4}$ | $K=2\times 10^{4}$ | $K=5\times 10^{4}$ | $K=10^{5}$
---|---|---|---|---|---
$E_{1}$ | 0.513743 | 0.481735 | 0.493825 | 0.508233 | 0.506597
$E_{2}$ | 0.506241 | 0.511887 | 0.468917 | 0.494157 | 0.492688
$E_{3}$ | 0.484667 | 0.483204 | 0.484577 | 0.526097 | 0.487613
$E_{4}$ | 0.442152 | 0.418237 | 0.434046 | 0.440515 | 0.467903
$E_{5}$ | 0.423393 | 0.443996 | 0.46427 | 0.441762 | 0.42277
$E_{6}$ | 0.413569 | 0.421813 | 0.419844 | 0.458051 | 0.426849
Figure 17. Numerical results for $-\frac{\ln D_{K}^{*,[2]}}{\ln K}$

| $K=5\times 10^{3}$
---|---
$E_{1}$ | 0.495306
$E_{2}$ | 0.479892
$E_{3}$ | 0.472156
$E_{4}$ | 0.413948
$E_{5}$ | 0.405477
$E_{6}$ | 0.39623
Figure 18. Numerical results for $-\frac{\ln D_{K}^{*,[3]}}{\ln K}$

##  5\. Conclusion and Final Remarks

In this paper we propose conjectures that refine the Sato-Tate conjecture,
specifically we conjecture that the Frobenius angles of a given elliptic curve
over $\mathbf{Q}$ without complex multiplication, are statistically
independently distributed with respect to the Sato-Tate measure, including the
more quantitative version involving the discrepancy of joint distributions.
Numerical evidences are presented to support the conjectures.

Taylor et. al. [CHT, T, HSBT, BLGHT] had established the Sato-Tate conjecture
for elliptic curves over totally real fields without complex multiplication,
and more generally [BLGG] established the Sato-Tate conjecture for Hilbert
modular forms over totally real fields (c.f. [ACC+] for the latest results on
the Sato-Tate conjecture for automorphic forms over number fields). Thus it is
natural to expect that our Conjectures 1.1 and 1.3 extend to the more general
setting as well.

It would be intriguing to find possible connections between Conjecture 1.3 in
the case $s\geq 2$ and properties of $L$-functions.

Finally and most interestingly, as observed experimentally from the numerics,
the rate of convergence to the measure $\mu_{ST}^{[s]}$, is slower in the case
of curves with higher Mordell-Weil ranks (in the one dimensional case $s=1$
this was already observed in [St]). Heuristically, in accordance with the
original form of the Birch and Swinnerton-Dyer conjecture, this can be seen as
due to the fact that, for curves of high Mordell-Weil rank, there is a
Chebyshev bias for the quantities $a_{p_{k}}$ towards being negative, c.f.
[M], [S], [KM]. It would be important to understand the rate of convergence to
the measure $\mu_{ST}^{[s]}$ in a more precise form (for example along the
lines suggested in [St] in the case $s=1$).

## References

  * [ACC+] P. Allen, F. Calegari, A. Caraiani, T. Gee, D. Helm, B. Le Hung, J. Newton, P. Scholze, R. Taylor, J. Thorne, Potential automorphy over CM fields. To appear in the Annals of Mathematics.
  * [AT] S. Akiyama, Y. Tanigawa, Calculation of Values of $L$-functions associated to Elliptic Curves. Mathematics of Computation, vol. 68, no. 227 (1999), pp. 1201-1231.
  * [BLGG] T. Barnet-Lamb, T. Gee, D. Geraghty, The Sato-Tate Conjecture for Hilbert Modular Forms. Journal of the American Mathematical Society, vol. 24, no. 2 (2011), pp. 411-469.
  * [BLGHT] T. Barnet-Lamb, D. Geraghty, M. Harris, R. Taylor, A Family of Calabi-Yau Varieties and Potential Automorphy II. Publ. Res. Inst. Math. Sci., vol. 47 (2011), no. 1, pp. 29-98.
  * [CHT] L. Clozel, M. Harris, R. Taylor, Automorphy of some $\ell$-adic lifts of automorphic mod $\ell$ Galois representations. Publ. Math. IHES, vol. 108 (2008), pp. 1-182.
  * [DE] D. Dobkin, E. Eppstein, Computing the discrepancy. Proceedings of the Ninth Annual Symposium on Computational Geometry, pp. 47-52, 1993.
  * [GSW] M. Gnewuch, A. Srivastav, C. Winzen, Finding optimal volume subintervals with $k$ points and calculating the star discrepancy are NP-hard problems. Journal of Complexity, vol. 25, pp. 115-127 (2009).
  * [H] M. Harris, Potential automorphy of odd-dimensional symmetric powers of elliptic curves and applications. Algebra, Arithmetic, and Geometry: in honor of Yu. I. Manin. Vol. II, 1-21, Progr. Math., 270, Birkhäuser Boston, Boston, MA, 2009.
  * [HSBT] M. Harris, N. Shepherd-Barron, R. Taylor, A Family of Calabi-Yau Varieties and Potential Automorphy. Annals of Mathematics, vol. 171, no. 2 (2010), pp. 779-813.
  * [KM] S. Kim, R. Murty, From the Birch and Swinnerton-Dyer conjecture to Nagao’s conjecture (with an appendix by A. Sutherland). Mathematics of Computation, vol. 92 (2023), pp. 385-408.
  * [K] D. Knuth, The Art of Computer Programming. Volume 2: Seminumerical Algorithms. Third Edition. Reading, Massachusetts: Addison-Wesley, 1997.
  * [KN] L. Kuipers, H. Niederreiter, Uniform Distribution of Sequences. Wiley Interscience, Pure and Applied Mathematics, 1974.
  * [M] B. Mazur, Finding Meaning in Error Terms. Bulletin of the American Mathematical Society, vol. 45, no. 2 (2008), pp. 185-228.
  * [N] H. Nagoshi, Joint value-distribution of $L$-functions and discrepancy of Hecke eigenvalues. Lithuanian Mathematical Journal, vol. 56, no. 3 (2016), pp. 325-356.
  * [Ni1] H. Niederreiter, Discrepancy and convex programming. Ann. Mat. Pura Appl. vol. 93 (1972), pp. 89-97.
  * [Ni2] H. Niederreiter, Quasi-Monte Carlo Methods and Pseudo-Random Numbers. Bulletin of the AMS., vol. 84, no. 6 (1978), pp. 957-1041.
  * [Ni3] H. Niederreiter, Random Number Generation and Quasi-Monte Carlo Methods. CBMS-NSF Regional Conference Series in Applied Mathematics, Series No. 63, 1992.
  * [NT] J. Newton, J. Thorne, Symmetric power functoriality for holomorphic modular forms. Publ. Math. IHES, vol. 134 (2021), pp. 1-116.
  * [RT] J. Rouse, J. Thorner, The Explicit Sato-Tate Conjecture and Densities Pertaining to Lehmer-Type Questions. Transactions of the American Mathematical Society, vol. 369 (2017), no. 5, pp. 3575-3604.
  * [S] P. Sarnak, Letter to: Barry Mazur on “Chebyshev’s bias” for $\tau(p)$, 2007. https://publications.ias.edu/sites/default/files/MazurLtrMay08.PDF.
  * [St] W. Stein, Elliptic Curves and Convergence: Sato-Tate, GRH, and BSD. Available online (https://wstein.org/talks/20071016-convergence/talk.pdf), 2007.
  * [T] R. Taylor, Automorphy of some $\ell$-adic lifts of automorphic mod $\ell$ Galois representations, II. Publ. Math. IHES, vol. 108 (2008), pp. 183-239.


# On Pitts’ Relational Properties of Domains

Arthur Azevedo de Amorim

###### Abstract

Andrew Pitts’ framework of _relational properties of domains_ is a powerful
method for defining predicates or relations on domains, with applications
ranging from reasoning principles for program equivalence to proofs of
adequacy connecting denotational and operational semantics. Its main appeal is
handling recursive definitions that are not obviously well-founded: as long as
the corresponding domain is also defined recursively, and its recursion
pattern lines up appropriately with the definition of the relations, the
framework can guarantee their existence.

Pitts’ original development used the Knaster-Tarski fixed-point theorem as a
key ingredient. In these notes, I show how his construction can be seen as an
instance of other key fixed-point theorems: the _inverse limit construction_ ,
the _Banach fixed-point theorem_ and the _Kleene fixed-point theorem_. The
connection underscores how Pitts’ construction is intimately tied to the
methods for constructing the base recursive domains themselves, and also to
techniques based on _guarded recursion_ , or _step-indexing_ , that have
become popular in the last two decades.

##  1 The Original Result

When reasoning about programs, it is common to compare their behaviors. We
might ask if two programs behave equivalently, if their public outputs are
equal, or if one program terminates more often than the other, among other
questions. Many of these issues can be phrased naturally using recursive
relations. For example, to argue that two functions are equivalent, we might
want to check if they produce equivalent outputs when applied to equivalent
inputs, for some notion of equivalence. However, when reasoning about higher-
order or stateful programs, equivalence for inputs and outputs is defined in
terms of equivalence for arbitrary programs. Thus, we end up with a circular
definition of equivalence, which requires care to justify formally without
running into paradoxes.

Andrew Pitts’ framework of _relational properties of domains_ [Pit96] is a
powerful tool for constructing such relations. We can summarize the idea as
follows.

######  Theorem 1.1 ([Pit96]).

Let $D$ be an object of a pointed $\operatorname{\mathsf{CPO}}$-category
$\mathcal{C}$. Suppose that $D$ is equipped with an isomorphism $i:F(D,D)\cong
D$ that satisfies the minimal invariant property, where
$F:\mathcal{C}^{op}\times\mathcal{C}\to\mathcal{C}$ is a
$\operatorname{\mathsf{CPO}}$-functor. Suppose moreover that $\mathcal{C}$ is
equipped with an admissible relational structure $\mathcal{R}$, and that $F$
acts on $\mathcal{R}$. Then there exists $R_{D}\in\mathcal{R}_{D}$ such that
$R_{D}=(i^{-1})^{*}F(R_{D},R_{D})$.

Here is how we can read this result intuitively, before diving into formal
definitions. The object $D$ is a universe where we model the behavior of the
programs. In Pitts’ original result, $D$ was assumed to be a _complete partial
order_ , or CPO, a domain-theoretic notion for modeling general recursion and
nontermination. Here, instead, we assume that $D$ lives in some pointed
$\operatorname{\mathsf{CPO}}$-category $\mathcal{C}$, a generalization allows
us to carry the core of Pitts’ arguments while accounting for variations that
have been explored in the literature, such as families of CPOs [AFJ20],
diagrams of CPOs [Lev02], or CPOs equipped with a metric [Aze+17].

We assume that $D$ is defined recursively as $F(D,D)\cong D$. The equation is
stated using a functor $F$, where each recursive occurrence of $D$ is either
contravariant or covariant; being a $\operatorname{\mathsf{CPO}}$-functor
simply means that $F$ interacts well with the structure of $\mathcal{C}$. In
principle, there could be many solutions to such equations, but Theorem 1.1
only applies to those that satisfy the _minimal invariant property_ , which
roughly means that $D$ is completely characterized by repeatedly unfolding its
definition.

The conclusion of the theorem says that we can construct some “relation”
$R_{D}$ on $D$. In the applications we sketched above, $R_{D}$ could be a
binary relation on a CPO, but the result applies to other settings as well,
such as relations of different arities or families of relations. The
relational structure $\mathcal{R}$ formalizes which properties are required of
the notion of “relation” for the construction to apply. The definition of
$R_{D}$ is given by a recursive equation $R_{D}=(i^{-1})^{*}F(R_{D},R_{D})$,
which is derived from an action of $F$ on $\mathcal{R}$. Different actions and
relational structures yield different definitions, and it is our job to choose
them appropriately depending on the application at hand.

Let us now spell out how this works in detail. A _complete partial order_
(CPO) is a poset $(X,\sqsubseteq)$ such that every increasing chain
$x:\operatorname{\mathbb{N}}\operatorname{\xrightarrow{\mathrm{mono}}}X$ has a
_limit_ , or least upper bound, denoted $\lim_{n}x(n)$. A CPO $X$ is _pointed_
if it has a least element $\bot\in X$. A function $f:X\to Y$ between CPOs is
_continuous_ , denoted $f:X\operatorname{\xrightarrow{\mathrm{cont}}}Y$, if it
is monotone and preserves limits. CPOs and continuous functions between them
form a category $\operatorname{\mathsf{CPO}}$. This category is cartesian
closed; the exponential $Y^{X}$ is given by the set of continuous functions of
type $X\operatorname{\xrightarrow{\mathrm{cont}}}Y$ ordered pointwise.

A $\operatorname{\mathsf{CPO}}$-category is a category $\mathcal{C}$ where the
sets of morphisms $\mathcal{C}(X,Y)$ are CPOs, and such that composition
$(-)\circ(-):\mathcal{C}(Y,Z)\times\mathcal{C}(X,Y)\to\mathcal{C}(X,Z)$ is
continuous. (Product CPOs are ordered component-wise.) The most basic example
of $\operatorname{\mathsf{CPO}}$-category is $\operatorname{\mathsf{CPO}}$
itself, for the order relation on continuous functions defined above. Another
example is given by _functor categories_ of the form $\mathcal{C}^{I}$, where
$\mathcal{C}$ is a $\operatorname{\mathsf{CPO}}$-category and $I$ is a small
category. A morphism in $\mathcal{C}^{I}$ is a family of arrows $(X_{i}\to
Y_{i})_{i\in I}$, and we obtain a $\operatorname{\mathsf{CPO}}$-category by
ordering such families pointwise. Combined with the previous example, this
shows that families or diagrams of CPOs also form
$\operatorname{\mathsf{CPO}}$-categories. If $\mathcal{C}$ is a
$\operatorname{\mathsf{CPO}}$-category, then so is $\mathcal{C}^{op}$, by
inheriting the structure on $\mathcal{C}$. A
$\operatorname{\mathsf{CPO}}$-functor $F:\mathcal{C}\to\mathcal{D}$ is a
functor whose action on morphisms is a continuous function.

Given a $\operatorname{\mathsf{CPO}}$-category, we say that $Y\in\mathcal{C}$
is _pointed_ if $\mathcal{C}(X,Y)$ is pointed for every $X$, and if $\bot\circ
f=\bot$ for every $f$. When $\mathcal{C}=\operatorname{\mathsf{CPO}}$, this
definition of pointedness coincides with the one given above. Every terminal
object 1 is pointed: if $X$ is an object, the unique arrow of type $X\to 1$ is
the least element. We say that $\mathcal{C}$ itself is pointed if every object
is pointed and it has a terminal object 1. In this case, any $\bot:X\to Y$ in
$\mathcal{C}$ factors through 1\. For example, $\operatorname{\mathsf{CPO}}$
is not a pointed $\operatorname{\mathsf{CPO}}$-category (because not every CPO
is pointed according to our definition), but we do obtain a pointed
$\operatorname{\mathsf{CPO}}$-category by restricting ourselves to pointed
CPOs. (More generally, any $\operatorname{\mathsf{CPO}}$-category
$\mathcal{C}$ with a terminal object has a pointed counterpart
$\mathcal{C}_{\bot}$ obtained by restricting $\mathcal{C}$ to pointed
objects.)

Given an isomorphism $i:F(D,D)\cong D$ in $\mathcal{C}$, where $D$ is pointed,
we say that $D$ has the _minimal invariant property_ if the following
condition holds. First, given
$\pi:D\operatorname{\xrightarrow{\mathrm{cont}}}D$, we define
$\Phi(\pi):D\operatorname{\xrightarrow{\mathrm{cont}}}D$ as
$\Phi(\pi)\triangleq i\circ F(\pi,\pi)\circ i^{-1}$, and pose
$\pi_{i}\triangleq\Phi^{i}(\bot)$. Intuitively, each $\pi_{i}$ is a projection
function that truncates $D$ to allow for at most $i$ unfoldings of its
definition; hence, $\lim_{i}\pi_{i}$ is a projection function that allows for
an arbitrary number of unfoldings. Intuitively, we would expect
$\lim_{i}\pi_{i}$ to be the identity on $D$, because leaving the number of
unfoldings unbounded should be tantamount to not truncating $D$ at all.
However, this is not necessarily true; the best we can show in general is
$\lim_{i}\pi_{i}\sqsubseteq 1_{D}$. The minimal invariant property says
precisely that we can strengthen this inequality to $\lim_{i}\pi_{i}=1_{D}$.

Given a category $\mathcal{C}$, a _relational structure_ on $\mathcal{C}$ is
simply a functor
$\mathcal{R}:\mathcal{C}^{op}\to\operatorname{\mathsf{CLat}_{\land}}$, where
$\operatorname{\mathsf{CLat}_{\land}}$ is the category of complete lattices
and functions that preserve greatest lower bounds. We denote the value of
$\mathcal{R}$ at some object $X\in\mathcal{C}$ as $\mathcal{R}_{X}$, and we
use the variables $R$, $S$ and $T$ to range over the elements of
$\mathcal{R}_{X}$. If $f:X\to Y$ is a morphism in $\mathcal{C}$, we write
$\mathcal{R}(f)$ as $f^{*}$ when $\mathcal{R}$ can be understood from the
context.

######  Example 1.2.

Our motivating example of relational structure is the one obtained by choosing
$\mathcal{C}=\operatorname{\mathsf{CPO}}$, and posing $\mathcal{R}_{X}$ to be
the set of binary relations between the elements of $X$ ordered by inclusion.
The greatest lower bound of a family of relations is simply their
_intersection_. And the action of a continuous function
$f:X\operatorname{\xrightarrow{\mathrm{cont}}}Y$ on $\mathcal{R}_{Y}$ takes
the _inverse image_ of a relation by $f$. For intuition, we’ll keep this
vocabulary when discussing other relational structures as well.

To define _admissible_ relational structures, it is convenient to shift our
perspective a bit. Given a relational structure $\mathcal{R}$ on
$\mathcal{C}$, we can build a category, also denoted $\mathcal{R}$, as
follows. The objects of $\mathcal{R}$ are pairs $(X,R)$, where
$X\in\mathcal{C}$ and $R\in\mathcal{R}_{X}$. (By abuse of notation, I’ll often
use $R$ to represent the object $(X,R)\in\mathcal{R}$.) A morphism
$f:(X,R)\to(Y,S)$ is a morphism $f:X\to Y$ in $\mathcal{C}$ such that $R\leq
f^{*}S$. In terms of Example 1.2, this simply means that the function $f$
takes elements related by $R$ to elements related by $S$. We can check that
identities and composition in $\mathcal{C}$ can be lifted to the morphisms of
$\mathcal{R}$. We have a canonical functor $p:\mathcal{R}\to\mathcal{C}$ that
maps the object $(X,R)$ to $X$ and acts as the identity on morphisms.

By unfolding definitions, we can restate some of the properties of the functor
$\mathcal{R}$ in terms of the above construction:

######  Lemma 1.3.

Let $X$, $Y$ and $Z$ be arbitrary objects of $\mathcal{C}$.

  1. 1.

$1_{X}:R\to S\iff R\leq S$, for all $R,S\in\mathcal{R}_{X}$.

  2. 2.

$f:f^{*}S\to S$ for any $S\in\mathcal{R}_{Y}$ and $f:X\to Y$.

  3. 3.

$gf:R\to S\iff f:R\to g^{*}S$, for all $f:X\to Y$, $g:Y\to Z$,
$S\in\mathcal{R}_{Z}$ and $R\in\mathcal{R}_{X}$.

  4. 4.

$f:R\to\bigcap_{i\in I}S_{i}\iff\forall i\in I,f:R\to S_{i}$, for any index
set $I$, $f:X\to Y$, $R\in\mathcal{R}_{X}$ and $S\in\mathcal{R}_{Y}^{I}$.

If $\mathcal{R}$ is a relational structure over a _pointed_
$\operatorname{\mathsf{CPO}}$-category $\mathcal{C}$, we say that a relation
$S\in\mathcal{R}_{Y}$ is _admissible_ if the following conditions hold for all
$R\in\mathcal{R}_{X}$. First, $\bot:R\to S$; second, $\lim_{i}f_{i}:R\to S$
whenever $(f_{i}:R\to S)_{i\in\operatorname{\mathbb{N}}}$ is an increasing
sequence of morphisms. We say that $\mathcal{R}$ itself is admissible if every
relation is admissible. Intuitively, being admissible means that a relation
always holds of diverging programs and is compatible with recursive program
definitions, which are constructed using limits via Kleene’s fixed point
theorem.

######  Example 1.4.

We can adapt Example 1.2 to obtain an admissible relational structure as
follows. First, instead of considering arbitrary CPOs, we just consider
pointed ones; that is, we take
$\mathcal{C}=\operatorname{\mathsf{CPO}}_{\bot}$. Second, instead of
considering arbitrary relations, we consider only those that contain $\bot$
and are closed under taking limits of chains.

The missing piece in the statement of Theorem 1.1 is what it means for a
$\operatorname{\mathsf{CPO}}$-functor
$F:\mathcal{C}^{op}\times\mathcal{C}\to\mathcal{C}$ to act on $\mathcal{R}$.
For each $R\in\mathcal{R}_{X}$ and $S\in\mathcal{R}_{Y}$, we assume that there
is some $F(R,S)\in\mathcal{R}_{F(X,Y)}$; moreover, if $f:R^{\prime}\to R$ and
$g:S\to S^{\prime}$ are morphisms in $\mathcal{R}$, then $F(f,g)$ should be a
morphism of type $F(R,S)\to F(R^{\prime},S^{\prime})$ in $\mathcal{R}$. (Note
the contravariance on first argument).

We can now sketch the main idea of Pitts’ original construction. For the rest
of the paper, we fix some pointed $\operatorname{\mathsf{CPO}}$-category
$\mathcal{C}$ equipped with an admissible relational structure $\mathcal{R}$,
a $\operatorname{\mathsf{CPO}}$-functor
$F:\mathcal{C}^{op}\times\mathcal{C}\to\mathcal{C}$ with an action on
$\mathcal{R}$, and an object $D$ that satisfies the minimal invariant property
for an isomorphism $i:F(D,D)\cong D$.

###### Proof of Theorem 1.1.

The proof relies on the Knaster-Tarski fixed point theorem: every monotone
function on a complete lattice has a least fixed point. Since the mapping
$R\mapsto(i^{-1})^{*}F(R,R)$ is not monotone, we need to modify its definition
a bit. Pitts’ employed the trick of separating covariant and contravariant
arguments: if we pose $L\triangleq\mathcal{R}_{D}^{op}\times\mathcal{R}_{D}$,
then the function

$\displaystyle\Psi$ $\displaystyle:L\to L$ $\displaystyle\Psi(R^{-},R^{+})$
$\displaystyle\triangleq((i^{-1})^{*}F(R^{+},R^{-}),(i^{-1})^{*}F(R^{-},R^{+}))$

_is_ monotone, and we can construct a least fixed point
$(R_{D}^{-},R_{D}^{+})$. Note that $(R_{D}^{+},R_{D}^{-})$ is also a fixed
point, so $(R_{D}^{-},R_{D}^{+})\leq(R_{D}^{+},R_{D}^{-})$ in $L$, and thus
$R_{D}^{+}\leq R_{D}^{-}$. To finish the proof, we just need to show the
reverse inequality. This is where the properties of minimal invariant and the
relational structures come into play. We can show that $\pi_{i}:R_{D}^{-}\to
R_{D}^{+}$ by induction on $i$, which implies, by admissibility, that
$1=\lim_{i}\pi_{i}:R_{D}^{-}\to R_{D}^{+}$. But this is equivalent to
$R_{D}^{-}\leq R_{D}^{+}$ by Lemma 1.3, from which the result follows. ∎

######  Remark 1.5 (Uniformity).

This proof shows that a stronger result holds: for all
$i\in\operatorname{\mathbb{N}}$,

$\displaystyle\pi_{i}$ $\displaystyle:R_{D}\to R_{D}.$ (1)

Intuitively, this means that the constructed relation $R_{D}$ still holds
after we truncate an element of $D$ after $i$ unfoldings. This property, known
as _uniformity_ , will play an important role in Section 3, when constructing
$R_{D}$ by the Banach fixed-point theorem.

######  Remark 1.6.

Pitts’ presentation differs from mine in a few respects [Pit96]. What I call a
relational structure here corresponds to what he calls a relational structure
with inverse images and intersections. More importantly, his notion of action
on a relational structure is different: rather than requiring $\mathcal{R}$ to
be admissible, he requires $F(R,S)$ to be admissible whenever $S$ is. This is
a strengthening of the above notion of action, since it must be defined even
for relations that are not admissible. It allows us to formulate more useful
coinduction principles associated with the relation $R_{D}$, but it does not
change the construction of $R_{D}$ itself, which is why we do not consider it
here.

##  2 Inverse Limit Construction

In practice, minimal invariants such as $D$ are often obtained with Scott’s
_inverse limit construction_. The method can be seen as an adaptation of
Kleene’s fixed-point theorem that accounts for mixed-variance functors, and
can be carried out for many $\operatorname{\mathsf{CPO}}$-categories [Wan79,
SP82]. After reviewing the idea, we will see that Pitts’ result, Theorem 1.1,
is just an instance of it!

We say that two morphisms $f^{e}:X\to Y$ and $f^{p}:Y\to X$ in $\mathcal{C}$
form an _embedding-projection pair_ if $f^{p}f^{e}=1_{X}$ and
$f^{e}f^{p}\sqsubseteq 1_{Y}$. We can show that each half of the pair uniquely
determines the other. Embeddings and projections compose, so we can form a
subcategory $\mathcal{C}^{e}$ consisting of all embeddings, and
$\mathcal{C}^{p}$ consisting of all projections. With embeddings and
projections, we can make mixed-variance functors more symmetric. Since $F$ is
a $\operatorname{\mathsf{CPO}}$-functor, its action on morphisms is monotone,
and we can show that $F(f^{p},f^{e})$ is an embedding, with $F(f^{e},f^{p})$
being the corresponding projection. Thus, $F$ determines a functor
$F^{e}:\mathcal{C}^{e}\to\mathcal{C}^{e}$ by posing $F^{e}(X)\triangleq
F(X,X)$ on objects, and $F^{e}(f^{e})\triangleq F^{e}(f^{p},f^{e})$ on
morphisms.

Much like Kleene’s fixed-point theorem, we’ll see that we can build $D$ by
considering a chain of finite iterations of $F^{e}$ and taking its
colimit—which, in the context of Kleene’s construction, would just correspond
to a limit in a CPO. Since we are dealing with embeddings, colimits behave
particularly symmetrically, a phenomenon known in the literature as the
_limit-colimit coincidence_ :

######  Theorem 2.1 ([SP82]).

Let $X^{e}:(\operatorname{\mathbb{N}},\leq)\to\mathcal{C}^{e}$ be a diagram of
embeddings, which uniquely corresponds to a diagram
$X^{p}:(\operatorname{\mathbb{N}},\geq)\to\mathcal{C}^{p}$ of projections. Let
$A\in\mathcal{C}$. The following conditions are equivalent.

  * •

$A$ is a colimit of $X^{e}$ in $\mathcal{C}$.

  * •

$A$ is a limit of $X^{p}$ in $\mathcal{C}$.

  * •

There is a cocone of embeddings $f^{e}:X^{e}\to\Delta A$ such that
$\lim_{i}f_{i}^{e}\circ f_{i}^{p}=1_{A}$.

  * •

There is a cone of projections $f^{p}:\Delta A\to X^{p}$ such that
$\lim_{i}f_{i}^{e}\circ f_{i}^{p}=1_{A}$.

In this situation, $f^{e}:X^{e}\to\Delta A$ is a colimiting cocone, and
$f^{p}:\Delta A\to X^{p}$ is a limiting cone. We call the pair $(A,f)$ the
_bilimit_ of $X$.

Because of this result, we can show that $F^{e}$ preserves bilimits of chains
of embeddings in $\mathcal{C}$. Then, constructing the fixed point of $F$
becomes simply a matter of adapting the proof of Kleene’s fixed-point theorem.

######  Theorem 2.2 ([SP82]).

Suppose that $\mathcal{C}$ has bilimits of chains of embeddings. Then $F$ has
a minimal invariant $i:F(D,D)\cong D$.

###### Proof.

Let $X_{i}=(F^{e})^{i}(1)$. Since $\mathcal{C}$ is pointed, there is an
embedding $f_{0}^{e}=\bot:1\to X_{1}$. By iterating $F^{e}$ on $f_{0}^{e}$, we
can construct a sequence of embeddings $X_{i}\to X_{i+1}$. By hypothesis, this
chain has a bilimit, which we call $g^{e}:X\to\Delta D$. Since $F^{e}$
preserves bilimits of embeddings, we know that
$F^{e}(g):F^{e}(X)=(X_{i})_{i\geq 1}\to\Delta F^{e}(D)$ is a bilimit. Note
that $1$ is an initial object of $\mathcal{C}^{e}$, so we can extend this
cocone to $h^{e}:X\to\Delta F^{e}(D)$ by posing

$\displaystyle h_{0}^{e}$ $\displaystyle:1\to F^{e}(D)$ $\displaystyle
h_{0}^{e}$ $\displaystyle\triangleq\bot$ $\displaystyle h_{i+1}^{e}$
$\displaystyle:F^{e}(X_{i})\to F^{e}(D)$ $\displaystyle h_{i+1}^{e}$
$\displaystyle\triangleq F^{e}(g_{i}).$

Since both $F(D,D)$ and $D$ satisfy the same universal property, we get an
isomorphism $i:F(D,D)\cong D$. The construction of this isomorphism implies,
for every $j\in\operatorname{\mathbb{N}}$,

$\displaystyle i\circ h_{j+1}^{e}$ $\displaystyle=i\circ
F(g_{j}^{p},g_{j}^{e})=g_{j+1}^{e}.$

Taking projections on both sides, we obtain

$\displaystyle F(g_{j}^{e},g_{j}^{p})\circ i^{-1}$
$\displaystyle=g_{j+1}^{p}.$

Combining the two equations, we find

$\displaystyle g_{j+1}^{e}\circ g_{j+1}^{p}$ $\displaystyle=i\circ
F(g_{j}^{p}g_{j}^{e},g_{j}^{e}g_{j}^{p})\circ i^{-1}.$

Since $g_{0}^{e}=\bot$ and $g_{0}^{p}=\bot$, this implies that
$\pi_{j}\triangleq g_{j}^{e}\circ g_{j}^{p}$ satisfies exactly the same
equations as the projection functions used in the definition of the minimal
invariant property. By Theorem 2.1, the limit of this sequence is the identity
on $D$, so $i:F(D,D)\cong D$ indeed satisfies the minimal invariant property.
∎

To see how this relates to Pitts’ construction, note that $\mathcal{R}$ can
also be seen as a pointed $\operatorname{\mathsf{CPO}}$-category, and the
projection $p:\mathcal{R}\to\mathcal{C}$ preserves this structure. Indeed,
admissibility means that the morphisms of $\mathcal{R}$ have the structure of
a pointed CPO inherited from the morphisms of $\mathcal{C}$. The terminal
object of $\mathcal{R}$ is just the terminal object of $\mathcal{C}$ equipped
with the greatest relation on $\mathcal{R}_{1}$, which exists because
$\mathcal{R}_{1}$ is a complete lattice. Moreover, if we see each relation
$F(R,S)$ as an object of $\mathcal{R}$, then the action of $F$ on
$\mathcal{R}$ can be described equivalently as a
$\operatorname{\mathsf{CPO}}$-functor of type
$\mathcal{R}^{op}\times\mathcal{R}\to\mathcal{R}$ making the following diagram
commute:

${\mathcal{R}^{op}\times\mathcal{R}}$${\mathcal{R}}$${\mathcal{C}^{op}\times\mathcal{C}}$${\mathcal{C}.}$$\scriptstyle{F}$

To apply the inverse limit construction to this lifted functor, we just need
to show that $\mathcal{R}$ has bilimits of chains of embeddings.

######  Lemma 2.3.

Admissible relational structures create bilimits. That is, if $X$ is a chain
of embeddings in $\mathcal{R}$, and $f:pX\to\Delta L$ is a bilimit in
$\mathcal{C}$, then $f:X\to\Delta R$ is a bilimit in $\mathcal{R}$, where
$R\in\mathcal{R}_{L}$ is defined as

$\displaystyle R$ $\displaystyle\triangleq\bigcap_{n}(f_{n}^{p})^{*}X_{n}.$

###### Proof.

By Theorem 2.1, it suffices to show that the corresponding cone of projections
is a limiting cone in $\mathcal{R}$. We’ll show that there is a bijective
correspondence between morphisms of type $T\to R$ and cones of type $\Delta
T\to X$ in $\mathcal{R}$ that is natural in $T$.

In one direction, suppose that $g:T\to\bigcap_{n}(f_{n}^{p})^{*}X_{n}$ is a
morphism in $\mathcal{R}$. This means that $f_{n}^{p}g:T\to X_{n}$ is a
morphism for every $n\in\operatorname{\mathbb{N}}$, and we can check that they
form a cone $\Delta T\to X$. Conversely, suppose that we are given a cone
$g:\Delta T\to X$. By projecting this cone onto $\mathcal{C}$, we obtain
another cone $pg:\Delta pT\to pX$. Since $f^{p}:\Delta L\to pX$ is limiting,
there is a unique mediating morphism $g^{\prime}:pT\to L$. Moreover, for every
$n\in N$, we have $f_{n}^{p}g^{\prime}=g_{n}$. Since $g_{n}:T\to X_{n}$ by
hypothesis, this means that $g^{\prime}:T\to(f_{n}^{p})^{*}X_{n}$ for every
$n\in\operatorname{\mathbb{N}}$. Thus,
$g^{\prime}:T\to\bigcap_{n}(f_{n}^{p})^{*}X_{n}=R$, and the mediating morphism
can be lifted as expected. After checking that this is natural in $T$, we
conclude. ∎

######  Remark 2.4 (A dual characterization).

Since each inverse image function $f^{*}:\mathcal{R}_{Y}\to\mathcal{R}_{X}$
preserves intersections and relations form complete lattices, we can build a
corresponding left adjoint $f_{!}:\mathcal{R}_{X}\to\mathcal{R}_{Y}$, called
the _direct image by $f$_. This allows us to find an alternative
characterization of the bilimit $R$ above, by dualizing the proof.

$R=\bigcup_{n}(f_{n}^{e})_{!}X_{n}.$

Here, $\bigcup$ refers to the supremum of a family of relations, which exists
by completeness.

######  Corollary 2.5.

If $\mathcal{C}$ satisfies the hypotheses of Theorem 2.2, then so does
$\mathcal{R}$.

This leads to an alternative strategy for constructing recursive relations.

###### Proof of Theorem 1.1; inverse limit construction.

Thanks to Corollary 2.5, we can apply Theorem 2.2 to the lifting of $F$ in
$\mathcal{R}$, and build a minimal invariant object $i_{R}:F(R,R)\cong R$ in
$\mathcal{R}$. We can check that $pR$ is just $D$ up to isomorphism, since
both are built as bilimits and those are preserved by $F$. Thus, we might as
well assume that $D=pR$ and $i_{R}=i$. The fact that $i$ is an isomorphism
implies that $R\leq(i^{-1})^{*}F(R,R)$. To conclude, we just need to show the
reverse inequality. We know that $i^{-1}:(i^{-1})^{*}F(R,R)\to F(R,R)$. Since
$i:F(R,R)\to R$, we find by composition that $1:(i^{-1})^{*}F(R,R)\to R$, and
we conclude that $R=(i^{-1})^{*}F(R,R)$. ∎

##  3 Banach Fixed Point

In the last two decades, _guarded recursion_ has emerged as a popular method
for defining recursive relations. While originally developed for reasoning
about denotational semantics [Nak00], it was shortly after adapted to the
operational setting, where it proved to be a convenient interface to _step-
indexed reasoning_ [AM01, App+07].

The basic idea is to work with a family of relations
$(R_{n})_{n\in\operatorname{\mathbb{N}}}$. In the case of step indexing,
$R_{n}$ represents a property that holds of terms of a language within at most
$n$ steps of computation, such as “if the term terminates in at most $n$
steps, then it is a value of type $\mathsf{bool}$”. It is always possible to
define such a family recursively if each $R_{n}$ depends only on the values of
$R_{m}$, for each $m<n$. Manipulating such indices directly quickly becomes
cumbersome, so guarded recursion encapsulates this process in a modality
$\smalltriangleright$, usually known as “later”. Then, any recursive
definition becomes valid, as long as recursive occurrences of the relation
appear under $\smalltriangleright$.

After reviewing the basics of guarded recursion, we will see how it leads to
an alternative proof of Theorem 1.1. First, we need a general, abstract
setting where guarded definitions can be formulated.

######  Definition 3.1.

An _ordered family of equivalences_ (OFE) is a tuple
$(X,(\stackrel{{\scriptstyle n}}{{=}})_{n\in\operatorname{\mathbb{N}}})$,
where $X$ is a set, $(\stackrel{{\scriptstyle
0}}{{=}})\supset(\stackrel{{\scriptstyle 1}}{{=}})\supset\cdots$ is a
decreasing sequence of equivalence relations on $X$, and
$\stackrel{{\scriptstyle 0}}{{=}}$ is the total relation on $X$. The family
should converge to the identity on $X$: $\bigcap_{n}(\stackrel{{\scriptstyle
n}}{{=}})=(=)$ or, equivalently, $(\forall n.x\stackrel{{\scriptstyle
n}}{{=}}y)\Rightarrow x=y$ for any $x,y\in X$.

We will soon see examples of OFEs connected to the denotational models we have
been studying so far. Before we get there, however, let us go back to the
example sketched above: an indexed family of relations on terms $t\in T$. The
set of such indexed families forms an OFE: we say that
$R\stackrel{{\scriptstyle n}}{{=}}S$ if and only if $R_{m}=S_{m}$ for any
$m<n$. Intuitively, this means that the two relations are equivalent if we
restrict ourselves to strictly less than $n$ steps of computation. To define
fixed points in such an abstract setting, we require slightly more structure
of OFEs.

######  Definition 3.2.

Let $X$ be an OFE. A _Cauchy sequence_ on $X$ is a sequence of elements
$x:\operatorname{\mathbb{N}}\to X$ such that, for every
$n\in\operatorname{\mathbb{N}}$, there exists $m\in\operatorname{\mathbb{N}}$
such that, for any $i,j\geq m$, we have $x_{i}\stackrel{{\scriptstyle
n}}{{=}}x_{j}$. We say that $X$ is a _complete OFE_ (COFE) if, for every
Cauchy sequence $x$, there exists some (necessarily unique) $\lim x\in X$ such
that, for every $n\in N$, there exists $m\in\operatorname{\mathbb{N}}$ such
that $x_{i}\stackrel{{\scriptstyle n}}{{=}}\lim x$ for every $i\geq m$.

We can show that the OFE of relations sketched above is complete. Intuitively,
if we look at the $n$th level of the terms of a Cauchy sequence, they will
eventually stabilize at some $R_{n}$, and we can take the family of such
$R_{n}$ to be the limit of the sequence.

######  Theorem 3.3 (Banach Fixed Point).

Suppose that a function $f:X\to X$ on a COFE is _contractive_ ; that is, if
$x\stackrel{{\scriptstyle n}}{{=}}y$, then $f(x)\stackrel{{\scriptstyle
n+1}}{{=}}f(y)$. Suppose, moreover, that there exists some $x_{0}\in X$. The
sequence $x_{i}\triangleq f^{i}(x_{0})$ is a Cauchy sequence, and its limit is
the unique fixed point of $f$; $f(\lim x)=x$.

######  Remark 3.4 (Connection to metric spaces).

Each OFE $X$ gives rise to a metric space as follows: $d(x,y)=2^{-n}$, where
$n$ is the greatest $n$ such that $x\stackrel{{\scriptstyle n}}{{=}}y$ holds
(if there is no such $n$, then $x=y$, and we set $d(x,y)=0$). If $X$ is
complete, then the resulting metric space is also complete. If $f:X\to X$ is
contractive, in the sense of Theorem 3.3, then
$d(f(x),f(y))\leq\frac{1}{2}d(x,y)$, implying that $f$ is contractive in the
traditional sense of metric spaces. This requirements guarantee that the usual
metric formulation of Banach’s fixed point theorem applies.

######  Remark 3.5 (Defining later).

Given a family of relations $(R_{n})_{n\in\operatorname{\mathbb{N}}}$ as
above, we can define another family $\smalltriangleright R$ by shifting $R$ by
1: $(\smalltriangleright R)_{0}=T\times T$, and $(\smalltriangleright
R)_{n+1}=R_{n}$. To define a contractive function on families of relations, it
suffices to consider functions of the form $f(R)=g(\smalltriangleright R)$,
where $g$ is _non-expansive_ , which means that it preserves each relation
$\stackrel{{\scriptstyle n}}{{=}}$. In this case, we say that the definition
of $f$ is _guarded_ , which explains the connection to guarded recursion
alluded to above. Similar definitions of $\smalltriangleright$ can be stated
for other types of relations. Though it will not play a major role in what
follows, guardedness is often a convenient way of checking that a definition
is contractive (e.g. in a type theory).

To apply Theorem 3.3 to construct recursive relations, we need to show that
relations on a minimal invariant $D$ form a COFE. To this end, we restrict
ourselves to _uniform relations_ , which are the $R\in\mathcal{R}_{D}$ such
that $\pi_{i}:R\to R$ for every $i$. As noted in Remark 1.5, the relation that
we aim to build is known to be uniform, so there is no harm in restricting our
search space to require uniformity from the start. We let
$\mathcal{U}\subset\mathcal{R}_{D}$ denote the set of uniform relations.

The reason for focusing on uniform relations is that they are entirely
determined by their inverse images by each of the $\pi_{n}$. Indeed, if
$\pi_{n}^{*}R=\pi_{n}^{*}S$, then $R\leq\pi_{n}^{*}R=\pi_{n}^{*}S$, where the
first inequality holds by uniformity. If this holds for every $n$, by
admissibility, $1=(\lim_{n}\pi_{n}):R\to S$ and $R\leq S$. An analogous
reasoning shows that $S\leq R$, and we conclude that $R=S$. This property, in
turn, helps us define a COFE structure over $\mathcal{U}$.

######  Lemma 3.6.

If $R$ and $S$ are uniform, then the following conditions are equivalent for
every $n\in\operatorname{\mathbb{N}}$:

  * •

$\pi_{n}^{*}R=\pi_{n}^{*}S$

  * •

$\pi_{n}:R\to S$ and $\pi_{n}:S\to R$.

If one of these conditions holds, we say that $R\stackrel{{\scriptstyle
n}}{{=}}S$. This assignment endows the set $\mathcal{U}$ with the structure of
a COFE.

###### Proof.

The equivalence between the two notions follows from the previous discussion.
To show that this indeed defines a COFE, note that we have already seen that
$R=S$ when $R\stackrel{{\scriptstyle n}}{{=}}S$ for every $n$, so we have a
well defined OFE. Thus, we just need to prove completeness. Let $(R_{i})$ be a
Cauchy sequence on $\mathcal{U}$. For every $i\in\operatorname{\mathbb{N}}$,
there exists some $m_{i}\in\operatorname{\mathbb{N}}$ such that
$\pi_{i}^{*}(R_{n})$ is equal to $S_{i}\triangleq\pi_{i}^{*}(R_{m_{i}})$ for
any $n\geq m_{i}$. Without loss of generality, we can assume that $(m_{i})$ is
increasing. We pose

$\displaystyle\lim R$ $\displaystyle\triangleq\bigcap_{i}S_{i}.$

We can show that uniform relations are closed under inverse images by
$\pi_{i}$ and intersections, hence each $S_{i}$ and $\lim R$ are indeed
uniform. Moreover, because $S$ is a subsequence of $R$, it must be a Cauchy
sequence, and it must have the same limit as $R$, if one of them does have a
limit.

To conclude, we just need to show that $\lim R$ is indeed the limit of $S$.
First, note that $(S_{i})$ is decreasing. Indeed, given $i\leq j$, we have

$\displaystyle S_{i}$
$\displaystyle=\pi_{i}^{*}(R_{m_{i}})=\pi_{i}^{*}(R_{m_{j}})=(\pi_{j}\circ\pi_{i})^{*}(R_{m_{j}})=\pi_{i}^{*}(\pi_{j}^{*}(R_{m_{j}}))=\pi_{i}^{*}(S_{j}).$

Thus, $S_{j}\leq S_{i}=\pi_{i}^{*}(S_{j})$ is equivalent to $\pi_{i}:S_{j}\to
S_{j}$, which follows from the uniformity of $S_{j}$.

On the other hand, given $i\in\operatorname{\mathbb{N}}$, we have $\lim
R\stackrel{{\scriptstyle i}}{{=}}S_{i}$. Indeed,

$\displaystyle\pi_{i}^{*}(\lim R)$
$\displaystyle=\pi_{i}^{*}\left(\bigcap_{j}S_{j}\right)$
$\displaystyle=\pi_{i}^{*}\left(\bigcap_{j\geq i}S_{j}\right)$ $S$ is
decreasing $\displaystyle=\bigcap_{j\geq i}\pi_{i}^{*}(S_{j})$ intersections
commute with inverse images $\displaystyle=\bigcap_{j\geq
i}\pi_{i}^{*}(S_{i})$ $\displaystyle=\pi_{i}^{*}(S_{i}),$

which shows that $S$ does converge to $\lim R$. ∎

Now that we have a COFE, we just need a contractive operator on $\mathcal{U}$.

######  Lemma 3.7.

The following defines a contractive operator on $\mathcal{U}$:

$\displaystyle\Psi(R)$ $\displaystyle\triangleq(i^{-1})^{*}(F(R,R)).$

###### Proof.

We begin with the following auxiliary result. If $R\stackrel{{\scriptstyle
n}}{{=}}S$, for $R,S\in\mathcal{U}$, then

$\pi_{n+1}=iF(\pi_{n},\pi_{n})i^{-1}:\Psi(R)\to\Psi(S).$

Indeed, by unfolding definitions, we have $i^{-1}:(i^{-1})^{*}F(R,R)\to
F(R,R)$ and $i:F(S,S)\to(i^{-1})^{*}F(S,S)$. By unfolding $\Psi$, and by
composition, we can prove this statement by showing

$F(\pi_{m},\pi_{m}):F(R,R)\to F(S,S).$

This follows from $R\stackrel{{\scriptstyle n}}{{=}}S$ by Lemma 3.6.

Let us proceed with the main proof. First, note that $\Psi(R)$ is indeed
uniform, so $\Psi:\mathcal{U}\to\mathcal{U}$. Indeed, we need to show that
$\pi_{n}:\Psi(R)\to\Psi(R)$ for any $n$. If $n\neq 0$, we apply the auxiliary
result above. If $n=0$, it suffices to show that $i^{-1}\bot:\Psi(R)\to
F(R,R)$. But $i^{-1}\bot=i^{-1}\bot\bot\leq i^{-1}i\bot=\bot$, so
$i^{-1}\bot=\bot$, and we conclude because $\mathcal{R}\ni F(R,R)$ is pointed.
Second, we need to show that $R\stackrel{{\scriptstyle n}}{{=}}S$ implies
$\Psi(R)\stackrel{{\scriptstyle n+1}}{{=}}\Psi(S)$. This follows by applying
the auxiliary result in both directions, and by using Lemma 3.6. ∎

Combining all these ingredients, we obtain yet another strategy for building
$R_{D}$.

###### Proof of Theorem 1.1; Banach fixed point.

It suffices to apply Theorem 3.3 to the operator
$\Psi:\mathcal{U}\to\mathcal{U}$ of Lemma 3.7. We just need to find an initial
uniform relation to construct the fixed point. Note that $\mathcal{R}_{D}$ has
an element $\top$, defined as the intersection of the empty family of
relations. Moreover, for any $f:X\to D$ in $\mathcal{C}$ and
$R\in\mathcal{R}_{X}$, we have $f:R\to\top$ by Lemma 1.3. In particular,
$\pi_{i}:\top\to\top$ for any $i$, so $\top\in\mathcal{U}$ and we conclude. ∎

##  4 Kleene Fixed Point

As observed earlier, the inverse limit construction can be seen as a
generalization of Kleene’s fixed point theorem:

######  Theorem 4.1 (Kleene).

Let $X$ be a pointed CPO and $f:X\to X$ be a continuous function. Then $f$ has
a least fixed point $x=f(x)$, given by the limit of the chain $\bot\sqsubseteq
f(\bot)\sqsubseteq f^{2}(\bot)\sqsubseteq\cdots$.

As a minor variation on Section 2, let us sketch how we can restate those
results using Kleene’s theorem, by viewing domains and relations as an ordered
structure rather than a category. There are two issues that we need to
address. First, $\mathcal{R}$ contains potentially many morphisms between a
pair of objects, whereas a CPO $X$ seen as a category has at most one. Second,
$\mathcal{R}$ is not a _skeletal category_ : there are objects that are
isomorphic, but not equal. By contrast, a CPO seen as a category is skeletal
because its order is antisymmetric.

To solve the first issue, consider the slice category $\mathcal{C}^{e}/D$.
Objects of $\mathcal{C}^{e}/D$ are embeddings of type $X\to D$, and arrows
from $X\to D$ to $Y\to D$ commuting triangles of embeddings:

${X}$${Y}$${D.}$

Since embeddings are monomorphisms, if there are two arrows of type $X\to Y$
in $\mathcal{C}^{e}/D$, they must be equal. We can apply a similar idea to
$\mathcal{R}$ by considering $\mathcal{R}(\mathcal{C}^{e}/D)$, which is
defined as the following pullback:

${\mathcal{R}(\mathcal{C}^{e}/D)}$${\mathcal{R}^{e}}$${\mathcal{C}^{e}/D}$${\mathcal{C}^{e}}$${\lrcorner}$

Explicitly, objects of $\mathcal{R}(\mathcal{C}^{e}/D)$ are triples
$X=(|X|,e_{X}:|X|\to D,R_{X}:\mathcal{R}_{X})$, where $e_{X}$ is an embedding.
An arrow $f:X\to Y$ is an embedding $f^{e}:|X|\to|Y|$ such that
$e_{Y}f^{e}=e_{X}$ and such that, in $\mathcal{R}$, we have $f^{e}:R_{X}\to
R_{Y}$ and $f^{p}:R_{Y}\to R_{X}$. Once again, there is at most one arrow of
any given type in this category.

To solve the second issue, note that, in many cases of interest, we can
replace $\mathcal{C}^{e}/D$ (and $\mathcal{R}(\mathcal{C}^{e}/D)$) with
equivalent skeletal subcategories, by choosing canonical representatives for
their objects. For instance, if $\mathcal{C}$ is
$\operatorname{\mathsf{CPO}}_{\bot}$, we can replace an embedding $e_{X}:X\to
D$ with its image in $D$, which is isomorphic to $X$. Two objects in
$\mathcal{C}^{e}/D$ are isomorphic if and only if their images in $D$ are
equal. In what follows, I’ll assume that such canonical representatives exist,
and that $D\to D$ is its own representative. By abuse of notation, I’ll
identify the above categories with their skeletal equivalents.

Both $\mathcal{C}^{e}/D$ and $\mathcal{R}(\mathcal{C}^{e}/D)$ are CPOs: to
compute the least upper bound of a chain, we simply project the chain onto
$\mathcal{C}$ (or $\mathcal{R}$), compute its bilimit, and use its canonical
representative in $\mathcal{C}^{e}/D$ (or $\mathcal{R}(\mathcal{C}^{e}/D)$).
Moreover, these CPOs are pointed: their least elements are $(1,\bot:1\to D)$
and $(1,\bot:1\to D,\top)$. This leads to the following alternative proof.

###### Proof of Theorem 1.1; Kleene fixed point.

Let $F:\mathcal{C}^{op}\times\mathcal{C}\to\mathcal{C}$ be a
$\operatorname{\mathsf{CPO}}$-functor. As we have seen in Section 2, we can
view the admissible action of $F$ on $\mathcal{R}$ as a lifting
$F_{\mathcal{R}}:\mathcal{R}^{op}\times\mathcal{R}\to\mathcal{R}$. These
functors give rise to functors $F^{e}:\mathcal{C}^{e}\to\mathcal{C}^{e}$ and
$F^{e}_{\mathcal{R}}:\mathcal{R}^{e}\to\mathcal{R}^{e}$ that preserve colimits
of chains. We have the following commutative diagram:

${\mathcal{R}^{e}}$${\mathcal{R}^{e}}$${\mathcal{C}^{e}}$${\mathcal{C}^{e}.}$$\scriptstyle{F^{e}_{\mathcal{R}}}$$\scriptstyle{F^{e}}$

By working with canonical representatives, we can view these functors as
continuous functions $f:\mathcal{C}^{e}/D\to\mathcal{C}^{e}/D$ and
$f_{\mathcal{R}}:\mathcal{R}(\mathcal{C}^{e}/D)\to\mathcal{R}(\mathcal{C}^{e}/D)$,
and we can take their fixed points by Theorem 4.1. By construction, the fixed
point of $f$ is just $D$, and the above diagram implies that
$p(\mathsf{fix}(f_{\mathcal{R}}))=\mathsf{fix}(f)=D$, where
$p:\mathcal{R}(\mathcal{C}^{e}/D)\to\mathcal{C}^{e}/D$ is the canonical
projection. This means, after some unfolding, that the relation component of
$\mathsf{fix}(f_{\mathcal{R}})$ is a relation on $D$ that satisfies the
recursive equation we are seeking. ∎

######  Remark 4.2.

Most categories used in domain theory have canonical representatives of
embeddings—we can take the image of an embedding, as we have done above, or we
can choose representatives using the axiom of choice. But if images are not
available, there is another option that does not rely on the axiom of choice:
to work with $\bar{\mathcal{C}}$, the _Karoubi envelope_ of $\mathcal{C}$.
This category extends $\mathcal{C}$ by freely splitting all idempotent arrows
in $\mathcal{C}$ (that is, arrows $p:X\to X$ such that $pp=p$). Roughly, this
means that $\bar{\mathcal{C}}$ contains canonical image objects of all
idempotents in $\mathcal{C}$. In particular, we can compute the image of the
idempotent $f^{e}f^{p}$ determined by an embedding $f^{e}:Y\to X$, which
yields a choice of representatives for embeddings. Moreover,
$\bar{\mathcal{C}}$ (and $\bar{\mathcal{R}}$) inherit the properties of the
original categories that we relied on to carry the above constructions, so our
results still apply.

##  5 Conclusion

We have just reviewed Pitts’ framework of relational properties of domains
[Pit96] and seen how it relates to other important fixed-point theorems: the
_inverse limit construction_ [SP82], _Banach’s fixed-point theorem_ , and
_Kleene’s fixed point theorem_. These connections are implicit in some of the
existing literature, and probably already known by experts. For example, the
work of [HJ98] presents a different method for constructing relations on
recursive data types that requires lifting limits and colimits along a
fibration; likewise, the proof of Pitts’ method with the inverse limit
construction uses Lemma 2.3, which lifts bilimits to a relational structure.
As for Banach’s fixed-point theorem, several works for reasoning about
denotational models [BST09a, BST09, Bir+11] employ similar constructions while
sometimes noting that Pitts’ framework could have been used instead [BST09a].
Here, we have seen how this connection goes beyond the construction of a
particular set of logical relations, and lies at the heart of Pitts’ method.
It is worth noting that the connections between these fixed-point theorems go
beyond the setting of relational reasoning—e.g. [Tha10] discusses how we can
view Banach’s fixed-point theorem as an instance of Kleene’s.

Traditionally, _step-indexing_ uses the steps in some operational semantics to
define recursive relations [AM01]. In light of the connections explained
above, Pitts’ construction—as well as other applications of Banach’s fixed-
point theorem for denotational models [Bir+11, BST09, BST09a, MPS86]—use a
similar trick to ensure that the recursion is well-founded, but count the
_number of unfoldings of a recursive type_ instead. In this sense, guarded
recursion is more general, since the notion of counting can be tied to
anything that can be tracked in the execution of a program, not just the
number of unfoldings of the domain equation. On the other hand, relations
constructed with Pitts’ method are often cleaner then their guarded
counterparts, because they do not have to mention step indices or guards
explicitly.

One question that I have not explored is how this connects to variants of
Pitts’ construction used for operational semantics, as developed by [BH99] or
[CH07]. Such works note that the projections $\pi_{i}$ can often be defined as
regular programs in a language, and leverage this fact to adapt Pitts’ ideas
to establish powerful reasoning principles for program equivalence. Like
Pitts’ original construction, these works employ the Knaster-Tarski fixed-
point theorem, but I believe that it might be possible to adapt their
constructions to leverage other results as well. One possible connection lies
in the proof of metric preservation for the Fuzz language [RP10]. Its argument
employed step-indexed logical relations, but the indices of the relations
tracked the number of recursive unfoldings reduced during execution rather
than the number of transitions in a small-step semantics. This idea is similar
to constructions by guarded recursion performed in denotational settings
[BST09, BST09a, Bir+11, MPS86], suggesting that it might be possible to obtain
an alternative, operational proof of metric preservation for Fuzz along the
lines of [BH99, CH07].

## Acknowledgments

I would like to thank Lars Birkedal for useful discussions on this topic.

## References

  * [AFJ20] Arthur Azevedo de Amorim, Matt Fredrikson and Limin Jia  “Reconciling noninterference and gradual typing”  In _LICS ’20: 35th Annual ACM/IEEE Symposium on Logic in Computer Science, Saarbrücken, Germany, July 8-11, 2020_ ACM, 2020, pp. 116–129  DOI: 10.1145/3373718.3394778
  * [AM01] Andrew W. Appel and David A. McAllester  “An indexed model of recursive types for foundational proof-carrying code”  In _ACM Trans. Program. Lang. Syst._ 23.5, 2001, pp. 657–683  DOI: 10.1145/504709.504712
  * [App+07] Andrew W. Appel, Paul-André Melliès, Christopher D. Richards and Jérôme Vouillon  “A very modal model of a modern, major, general type system”  In _Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2007, Nice, France, January 17-19, 2007_ ACM, 2007, pp. 109–122  DOI: 10.1145/1190216.1190235
  * [Aze+17] Arthur Azevedo de Amorim et al.  “A semantic account of metric preservation”  In _Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017_ ACM, 2017, pp. 545–556  DOI: 10.1145/3009837.3009890
  * [BH99] Lars Birkedal and Robert Harper  “Relational Interpretations of Recursive Types in an Operational Setting”  In _Inf. Comput._ 155.1-2, 1999, pp. 3–63  DOI: 10.1006/inco.1999.2828
  * [Bir+11] Lars Birkedal et al.  “Step-indexed kripke models over recursive worlds”  In _Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2011, Austin, TX, USA, January 26-28, 2011_ ACM, 2011, pp. 119–132  DOI: 10.1145/1926385.1926401
  * [BST09] Lars Birkedal, Kristian Støvring and Jacob Thamsborg  “Realizability Semantics of Parametric Polymorphism, General References, and Recursive Types”  In _Foundations of Software Science and Computational Structures, 12th International Conference, FOSSACS 2009, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, York, UK, March 22-29, 2009. Proceedings_ 5504, Lecture Notes in Computer Science  Springer, 2009, pp. 456–470  DOI: 10.1007/978-3-642-00596-1“˙32
  * [BST09a] Lars Birkedal, Kristian Støvring and Jacob Thamsborg  “Relational parametricity for references and recursive types”  In _Proceedings of TLDI’09: 2009 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation, Savannah, GA, USA, January 24, 2009_ ACM, 2009, pp. 91–104  DOI: 10.1145/1481861.1481873
  * [CH07] Karl Crary and Robert Harper  “Syntactic Logical Relations for Polymorphic and Recursive Types”  In _Electron. Notes Theor. Comput. Sci._ 172, 2007, pp. 259–299  DOI: 10.1016/j.entcs.2007.02.010
  * [HJ98] Claudio Hermida and Bart Jacobs  “Structural Induction and Coinduction in a Fibrational Setting”  In _Inf. Comput._ 145.2, 1998, pp. 107–152  DOI: 10.1006/inco.1998.2725
  * [Lev02] Paul Blain Levy  “Possible World Semantics for General Storage in Call-By-Value”  In _Computer Science Logic, 16th International Workshop, CSL 2002, 11th Annual Conference of the EACSL, Edinburgh, Scotland, UK, September 22-25, 2002, Proceedings_ 2471, Lecture Notes in Computer Science  Springer, 2002, pp. 232–246  DOI: 10.1007/3-540-45793-3“˙16
  * [MPS86] David B. MacQueen, Gordon D. Plotkin and Ravi Sethi  “An Ideal Model for Recursive Polymorphic Types”  In _Inf. Control._ 71.1/2, 1986, pp. 95–130  DOI: 10.1016/S0019-9958(86)80019-5
  * [Nak00] Hiroshi Nakano  “A Modality for Recursion”  In _15th Annual IEEE Symposium on Logic in Computer Science, Santa Barbara, California, USA, June 26-29, 2000_ IEEE Computer Society, 2000, pp. 255–266  DOI: 10.1109/LICS.2000.855774
  * [Pit96] Andrew M. Pitts  “Relational Properties of Domains”  In _Inf. Comput._ 127.2, 1996, pp. 66–90  DOI: 10.1006/inco.1996.0052
  * [RP10] Jason Reed and Benjamin C. Pierce  “Distance makes the types grow stronger: a calculus for differential privacy”  In _Proceeding of the 15th ACM SIGPLAN international conference on Functional programming, ICFP 2010, Baltimore, Maryland, USA, September 27-29, 2010_ ACM, 2010, pp. 157–168  DOI: 10.1145/1863543.1863568
  * [SP82] Michael B. Smyth and Gordon D. Plotkin  “The Category-Theoretic Solution of Recursive Domain Equations”  In _SIAM J. Comput._ 11.4, 1982, pp. 761–783  DOI: 10.1137/0211062
  * [Tha10] Jacob Thamsborg  “Denotational World-indexed Logical Relations and Friends”, 2010
  * [Wan79] Mitchell Wand  “Fixed-Point Constructions in Order-Enriched Categories”  In _Theor. Comput. Sci._ 8, 1979, pp. 13–30  DOI: 10.1016/0304-3975(79)90053-7