# Path Sums for Propagators in Causal Sets

Samuel Shuman<EMAIL_ADDRESS>Department of Physics, Oregon State
University.

###### Abstract

A major challenge in Causal Set research is that theories need only to match
general relativity and quantum field theory in the appropriate limits. This
means that there should be many different ways to calculate a scalar field
propagator in a causal set that match the known limits, but may give
significantly different results on the small scale. In this work, we explore
under what conditions a path sum will correspond to a scalar field propagator
in such a way that it matches the known value in the continuum limit. A family
of solutions for the path sum is found and is verified numerically in a few
specific cases.

††preprint: APS/123-QED

##  I  Introduction

###  I.1 Background: Causal Sets

Causal Set Theory (CST) is a candidate theory of quantum gravity. Like many
such theories, it focuses on describing the Planck scale structure of
spacetime in a way that is mostly consistent with general relativity and
quantum field theory. As one might expect, there are many ways to approximate
these theories on the Planck scale, so to make progress, we must decide which
classical properties should be fundamental aspects of the new theory and which
should be emergent on the large scale. CST is based on the idea that spacetime
is fundamentally discrete, and has a fundamental causal structure, but
Lorentzian geometry is emergent.

The central idea of CST, that causal structure and discreteness are enough to
recover Lorentzian geometry on the large scale, has its foundation in a series
of papers in the 1970s. These papers showed that for all past and future
distinguishing spacetimes the causal structure is enough to determine the
conformal geometry [1, 2]. This means that if you know the causal structure of
a spacetime and the volume of every region, that is enough to recover the
entire geometry. As summarized by Rafael Sorkin in [3]:

$\text{Causal Structure}+\text{Volume}=\text{Geometry}$

As we will see, discreteness, when treated in the ways we will describe, can
tell you about the spacetime volume of any region, with the number of points
in a region corresponding to the volume. This correspondence depends on a
parameter called the density, $\rho$, of the causal set. Thus we get:

$\text{Causality}+\text{Discreteness}\approx\text{Geometry}$

Therefore, a discrete set of events with a causal ordering should be enough to
recover the geometry of a Lorentzian manifold. This idea was first laid out by
Bombelli, Lee, Meyer, and Sorkin in 1987 [4].

####  I.1.1 Definitions

What follows are some important definitions in CST. A Causal Set is a set of
events, $C$, paired with a parameter, $\rho$, called the density, and an
ordering relation (the causal order), $\prec$, satisfying the following
properties:

  * •

Transitivity $x\prec y$, $y\prec z$ $\Rightarrow x\prec z$

  * •

Anti-symmetry $x\prec y$ $\Rightarrow y\not\prec x$

  * •

Local-finiteness

Local-finiteness requires that the interval

$[x,y]=\\{z\|x\prec z\prec y\\}$

is finite for all $x,y\in C$. Note that in the context of general relativity,
the interval is often referred to as a causal diamond. To summarize what these
requirements correspond to physically, transitivity tells us that this
relation orders the causal set and can be interpreted as a casual structure,
antisymmetry tells us that there are no closed causal loops $x\prec y\prec x$,
and local-finiteness tells us that regions of a causal set that correspond to
finite regions in a manifold description should have finitely many elements.
This last requirement guarantees that our causal set is discrete and that
there can exist a number-volume correspondence as mentioned above.

We must also consider a few types of trajectories in causal sets. A trajectory
is a sequence of events in $C$. Note that no requirement is made here
regarding causal structure. A chain is a sequence of events $(x_{n})$ in $C$
such that $x_{i}\prec x_{i+1}$ for all $i$. We say $x$ is linked to $y$,
denoted $x\prec*y$, if $x\prec y$ and the interval $[x,y]$ is empty. We can
then define a path as a sequence $(x_{n})$ in $C$ such that
$x_{i}\prec*x_{i+1}$ for all $i$. To state this a different way, paths are
chains that are as close to continuous as possible. The length of a trajectory
$\\{x_{0},\dots,x_{n}\\}$ is defined to be $n$. Finally, we will define a jump
between two events in a spacetime to be a trajectory of length 1. In
particular, this means the jump from $x$ to $y$ for some $x,y\in C$ is the
sequence $\\{x,y\\}$ with no intermediate points.

####  I.1.2 Sprinklings

The dynamics of CST have not been fully determined, so we cannot yet solve for
the causal order corresponding to physical conditions from first principles.
In this paper, we will need to generate causal sets that correspond to a flat
spacetime. To do this we will use a method called sprinkling. Sprinkling is a
strategy to generate a causal set corresponding to a given manifold by taking
a random set of points in that manifold as our events and using the causal
structure of the manifold to define the causal relation.

One might expect a regular lattice to be a more appropriate sprinkling
procedure than randomly selecting events. However, a random sprinkling is
necessary to preserve Lorentz symmetry. To make sense of this, note that a
regular lattice in a spacetime defines a preferred reference frame (see figure
1). We will see that a Poisson process is a natural choice for this random
distribution.

Figure 1: From [5], a lattice spacetime in two dimensions. The number-volume
correspondence only holds in a specific frame and fails to hold in a Lorentz
boosted frame.

A Poisson process in a 4-dimensional spacetime is defined analogously to a
1-dimensional Poisson distribution. It is defined by a single parameter that
tells you the density at which events are selected. In general, a Poisson
process must satisfy two properties. One is that the probability of finding
exactly $n$ points in a region of volume $V$ is:

$P\\{N=n\\}=\frac{(\rho V)^{n}}{n!}e^{-\rho V}$ (1)

Here, $\rho$ is the average number density of points in the spacetime. The
other required property is that the number of points in disjoint, bounded
regions is independent.

Figure 2: A Poisson sprinkling in a flat 2-dimensional spacetime shown in both
the original reference frame and one that is Lorentz boosted. This was
calculated with $\rho=600$ and a relative velocity of $v=0.6c$. Unlike the
lattice sprinkling shown in figure 1, the Poisson random sprinkling has no
preferred reference frame.

This is what is called a homogeneous Poisson process, meaning that the rate at
which events occur, $\rho$, is constant and does not depend on the location in
spacetime. Homogeneous Poisson processes are particularly easy to simulate in
finite regions. First, use the Poisson distribution and the volume of the
region to randomly determine the number of points that will be sprinkled. Then
each point is placed in the region with a uniform random distribution. For
rectangular regions, this can be done by selecting each coordinate from a one
dimensional uniform distribution [6].

####  I.1.3 Correspondences

If CST is correct, then the underlying structure of the universe is a causal
set and any manifold representation of spacetime is just an approximation.
That being said, the manifold approximation for spacetime must be very good
when we “zoom out” from the discreteness scale.

This leads to the “Fundamental Conjecture of CST” or the “Hauptvermutung” [5].
In short, if a causal set that is generated by a Poisson sprinkling into a
manifold $M$ can also be achieved as a Poisson sprinkling into a manifold
$M^{\prime}$ at the same density, then the two manifolds $M$ and $M^{\prime}$
must have almost identical geometries. There have been some suggestions, such
as in [7], to make this statement more rigorous but there is not yet a clear
consensus. If this conjecture was not true, then CST would need additional
structure to recover general relativity on the large-scale.

One way this problem has been approached is to establish correspondences
between properties of a causal set and properties of any manifold it can be
faithfully embedded in. A manifold faithfully embeds a causal set if the
causal set can be generated as a Poisson sprinkling on that manifold. The idea
is to say that any manifold that faithfully embeds a particular causal set
must approximate certain geometric properties on the large-scale. The most
basic example is the number-volume correspondence we have already discussed.
Since our points are sprinkled by a Poisson process, the fractional variance
in the number of points in a region is:

$\frac{\delta n}{n}=\frac{\sqrt{n}}{n}=\frac{1}{\sqrt{n}}$ (2)

Thus, regions of the causal set containing a large number of events, $n$, can
be known within a very small uncertainty to have volume $V=n/\rho$ in any
manifold that faithfully embeds it.

Another correspondence is for the geodesic proper time separating two causally
connected events. In 2 dimensions [8], this proper time can be estimated as:

$\tau^{6}=\frac{1}{8\rho^{3}}(J_{1}-2J_{2}+J_{3})$ (3)

with $J_{k}$ defined by

$J_{k}=(2k+2)(2k+4)(2^{3})\left(kC_{k}\right)^{3/k}$ (4)

and $C_{k}$ defined as the number of chains of length $k$ connecting the
events. These formulas vary slightly depending on the dimension of the
spacetime.

It should be noted that many such correspondences have been investigated.
There are correspondences to estimate the curvature, dimension, volume, proper
time, etc of the regions of any manifold that can be represented by that
causal set. See [5] for further discussion of these correspondences.

###  I.2 Background: Path Integrals and Propagators

In general, a propagator describes how a quantum system transitions from one
state to another. A common special case is a propagator that describes how a
system transitions from one event to another. This will be proportional to the
probability amplitude associated with transitioning between these events. For
events $x,y$ in spacetime, we will denote this propagator $K(x,y)$. The
functional form of the propagator depends on the quantum system being
described.

The path integral formulation developed by Richard Feynman shows that some
propagators between events in spacetime can be calculated by integrating over
trajectories connecting the two events [9]. Different propagators can be found
by including different types of trajectories in this integral, but not all
propagators can be defined this way [10]. To find the total probability
amplitude of transitioning between two events, we can assign a probability
amplitude to each path and add up each of those contributions:

$K(x,y)=\int_{x}^{y}\delta q\hskip 4.0pte^{iS[q]}$ (5)

The integral must be taken over paths, $q$, connecting $x$ and $y$. The
probability amplitude associated with each path is $e^{iS[q]}$ where $S[q]$ is
the action of that path, which will depend on the quantum system being
described.

###  I.3  Previous Work

There has been past work considering scalar field propagators in causal sets.
For example, in [11, 12] the author considered a model that assigned an
amplitude to each jump along a path (called the hop amplitude $a$), and
another to each intermediate event along the path (called the stop amplitude
$b$). They were able to show that there are values of these constants that
recover the free scalar field retarded propagator when averaged over
sprinklings and considered in the appropriate continuum limit. The main idea
is to create a matrix representation of the propagator that approximately
matches the value of the propagator in the continuum.

Now let us consider an illustrative example for how the average values of such
propagators were calculated. In [11, 12], when summing over paths and
averaging over sprinklings, the propagator becomes:

$K(x,y)=\sum_{n}a^{n}b^{n-1}P_{n}(x,y)$ (6)

where $P_{n}(x,y)$ is the average number of paths of length $n$ from $x$ to
$y$. This expression comes from the fact that every path of length $n$ has $n$
hops and $(n-1)$ stops. The author then set up an integral for $P_{n}(x,y)$
and used that to get an integral relationship for the propagator

$\displaystyle P_{n}(x,y)=\rho^{n-1}\int dz_{1}\int dz_{2}\mathellipsis\int
dz_{n-1}$
$\displaystyle\mu(x,z_{1})\mu(z_{1},z_{2})\mathellipsis\mu(z_{n-1},y)$ (7)

Here $\mu(x,y)$ is the probability that events $x$ and $y$ are linked. This
leads to the integral relation:

$K(y-x)=a\mu(y-x)+\rho ab\int dz\mu(z-x)K(y-z)$ (8)

Since the integral is a convolution, this equation can be solved with a
Fourier transform.

$\tilde{K}(p)=\frac{a\tilde{\mu}(p)}{1-\rho ab\tilde{\mu}(p)}$ (9)

Then one only has to Fourier transform back to get an expression for the
average over sprinklings of the scalar field propagator associated with these
hop and stop amplitudes.

While this work was able to suggest a method to construct a propagator on a
causal set, there is an important consideration. Since the only restrictions
are that the path sum matches the continuum propagator on average and does not
vary too much over sprinklings, we should expect many different formulas for
the propagator to match these conditions. For that reason, it is useful to
solve this problem in a more general way, so that we might categorize a
greater variety of possible path sums that are consistent with the continuum
calculation.

A similar approach was taken in [13], but in that paper the authors allowed
for non-constant hop amplitudes and did not include stop amplitudes. While
they solved for a matrix relationship between these hop amplitudes and the
propagator in a way that is similar to what we will see in the next section,
they did not discuss how this relationship would average over sprinklings.

##  II  Path Sums for Propagators

In this section, we will develop a general method for analyzing the
relationship between a scalar field propagator in a causal set and the jump
amplitude matrix $T$ (which serves the same role as the matrix $A$ in [13]).
By looking at this relationship after averaging over sprinklings into
Minkowski space, we will require that we recover the same propagator as the
continuum calculation. In [11], there is discussion for how such a propagator
could be used to define a scalar field theory on a causal set.

###  II.1  Propagators and Jump Amplitudes
on Causal Sets

First, since the causal set is discrete we can label events in the causal set
by non-negative integer indices. Let us assume the causal set is finite. Then
define the matrix $T$, by

$\displaystyle T_{ij}\equiv\text{The probability amplitude associated with}$
$\displaystyle\text{jumping from event }i\text{ to event }j$

We will also define

$\displaystyle\sigma_{ij}\equiv\text{The total probability amplitude of all}$
$\displaystyle\text{trajectories from event }i\text{ to event }j$

The propagator will be proportional to the matrix $\sigma$, but we must
include a constant that incorporates the units of the propagator in the same
way that $\delta q$ incorporates the units of the propagator in equation 5. In
particular, we will define $K_{xy}=a\sigma_{xy}$.

Since all trajectories can be broken down into a sequence of jumps, we should
expect a relationship between $T$ and $\sigma$. Consider organizing
trajectories from $x$ to $y$ by the first jump taken. Every trajectory from
$x$ to $y$ is either a direct jump to $y$, or a jump to some element $z$
followed by a trajectory from $z$ to $y$. Therefore we have

$\sigma_{xy}=T_{xy}+\sum_{z}T_{xz}\sigma_{zy}$ (10)

Since $K_{xy}=a\sigma_{xy}$, we get the composition relation

$K_{xy}=aT_{xy}+\sum_{z}T_{xz}K_{zy}$ (11)

Or, written in matrix form

$K=aT+TK$ (12) $K=aT(I-T)^{-1}$ (13)

This derivation allows us to define the propagator whenever $(I-T)$ is
invertible. If $(I-T)$ is not invertible, then there is not a clear way to
define a propagator in terms of the jump amplitude matrix, $T$. Note that when
the allowed jumps are all causal, $(I-T)$ is guaranteed to be invertible and
so the propagator is well-defined [11, 12].

•$x$•$z$•••$y$•••$T_{xy}$$T_{xz}$$K_{zy}$ Figure 3: Every trajectory from $x$
to $y$ is either a direct jump to $y$, or a jump to some event $z$ followed by
a trajectory from $z$ to $y$. This is reflected in the composition law
$K=aT+TK$.

###  II.2  Averaging Over Sprinklings

The next step taken in previous attempts at deriving path sums in causal sets
is equivalent to postulating a model $T$ matrix (such as the hop and stop
amplitudes considered in [11, 12]) and then carefully considering what
integral relations may hold for this model. In this work, we will take a more
general approach by defining an average value of the matrix $T$ and of the
propagator.

First, let $x$ and $y$ be two elements in the background manifold $M$.
Consider the space of all possible causal sets faithfully embedded in $M$ that
include $x$ and $y$. If we label these two events with the indices 0 and 1 in
these causal sets, then we will define

$T(x,y)\equiv\text{average over sprinklings of }T_{01}$ (14)
$K(x,y)\equiv\text{average over sprinklings of }K_{01}$ (15)

We will assume these averages lead to functions that are sufficiently smooth
and continuous. This seems reasonable since the $K$ and $T$ matrices will be
defined in terms of the causal structure of a sprinkling into a smooth
manifold. Importantly, since we are doing this calculation in Minkowski
spacetime, we will also assume translational invariance:

$T(x,y)=T(y-x)$ $K(x,y)=K(y-x)$

Next we will consider how these average functions follow the composition law
in equation 11. For the $K_{01}$ matrix element we have

$K_{01}=aT_{01}+\sum_{i}T_{0i}K_{i1}$ (16)

When we average over sprinklings, $K_{01}$ becomes $K(y-x)$ and $T_{01}$
becomes $T(y-x)$. The sum will include all points in the causal set, so when
averaged over all possible sprinklings we will need to include every point in
the manifold. To make the next step more clear, consider the discreteness
scale volume $V_{0}=1/\rho$, which can be thought of as the average volume
associated with each event in a sprinkling. We can write the sum as

$\sum_{i}T_{0i}K_{i1}=\rho\sum_{i}T_{0i}K_{i1}V_{0}$ (17)

The sum now evaluates $T_{0i}K_{i1}$ at each event in the spacetime and
multiplies by a volume associated with that event. Now we can see that this is
a type of Riemann sum that will become an integral when we average over all
sprinklings. Thus we get the average composition relation:

$K(y-x)=aT(y-x)+\rho\int dzT(z-x)K(y-z)$ (18)

Since the integral is a convolution, this relationship can be solved by
Fourier transforming the equation.

$\tilde{K}(p)=a\tilde{T}(p)+\rho\tilde{T}(p)\tilde{K}(p)$ (19)
$\tilde{K}(p)=\frac{a\tilde{T}(p)}{1-\rho\tilde{T}(p)}$ (20)

Then all that remains is to Fourier transform back to find the average
propagator $K(y-x)$.

While this is similar to what was done in [11, 12], since we have not
specified the jump amplitude function, we can solve for that instead.

$\tilde{T}(p)=\frac{\tilde{K}(p)}{a+\rho\tilde{K}(p)}$ (21)

Then Fourier transforming back would tell us what jump amplitudes would be
needed on average to recreate a given propagator as a path sum in a causal
set.

###  II.3  Solving for Jump Amplitudes

The Feynman, retarded, and advanced propagators for scalar fields all have
Fourier transforms of the form

$\tilde{K}(p)=\frac{1}{f(p)+m^{2}}$ (22)

For example, for the Feynman propagator we would set
$f(p)=p^{2}-i\varepsilon$. Plugging this into equation 21 yields:

$\tilde{T}(p)=\frac{1}{a}\cdot\frac{1}{f(p)+m^{2}+\rho/a}$ (23)

This has the same form as the Fourier transform of the propagator but with the
constant $(m^{2}+\rho/a)$ taking the place of $m^{2}$. To simplify this
expression, define the factor $\beta=\sqrt{1+\frac{\rho}{m^{2}a}}$. Then
$m^{2}\mapsto(m^{2}+\rho/a)$ may instead be written as $m\mapsto(\pm\beta m)$.
This gives a final result for the average value of the jump amplitudes for
propagators of this form:

$T(y-x)=\frac{1}{a}K(y-x)\text{ , }m\mapsto\pm\beta m$ (24)

###  II.4  Units of $a$

So far in this paper, we have used natural units with $\hbar=c=1$. In this
section we will reintroduce $\hbar$ in order to better understand how $a$
should depend on $\rho$ and $m$. The constant $a$ that appears in these
expressions is included so that the propagator is not unitless. To determine
what units we should expect for $a$, note that $a$ has the same units as the
propagator, $K$. Consider the Feynman propagator. This has the Fourier
transform:

$\tilde{K}=\frac{1}{p^{2}+m^{2}}$ (25)

This is a Green’s function for the Klein-Gordon equation, which is a statement
of the relativistic energy relation $E^{2}=p^{2}+m^{2}$. Therefore we should
expect $\tilde{K}$ to have the same units as $1/m^{2}$. Now consider the
Fourier transform for $K$.

$\tilde{K}=\int dxe^{ipx}K$ (26)

Since $\tilde{K}$ has units of $1/m^{2}$ and $dx$ has units of spacetime
volume, $K$ must have units of $\frac{1}{Vm^{2}}$. In order for these units to
come directly from the constants $m$ and $\rho$, we must have a normalization
of the form $a=\alpha\frac{\rho}{m^{2}}$, where $\alpha$ is a unitless
parameter. This yields a $\beta$ factor of the form

$\beta=\sqrt{1+\frac{1}{\alpha}}$ (27)

Since fundamental constants like $\hbar$ and $G$ may also contribute to the
units of $a$, we cannot rule out that $\alpha$ may depend on $\rho$ and
$m^{2}$. As we will discuss in section III.1.4, the only clear restriction on
$\alpha$ is that it is non-zero.

##  III  Applications

In this section, we will apply the formulas derived in section II to construct
path sums for the retarded propagator and the Feynman propagator. First, we
will show that this formulation is consistent with past work. Then we will use
numerical simulations to show that these results are consistent with the
continuum values for the retarded propagator. In this section it will be
useful to define:

$\nu(y-x)\equiv\Theta(y^{0}-x^{0})\Theta\Big{(}\tau(y-x)^{2}\Big{)}$ (28)

Note that this is 1 if $x\prec y$ and 0 otherwise.

###  III.1  Results for the Retarded Propagator

####  III.1.1 Comparison to Previous Results

In order to compare the following results, which are in terms of jump
amplitudes, to the results in [11, 12], we must first consider how hop and
stop amplitudes can be expressed in terms of jump amplitudes. All but the last
jump along a trajectory consists of a hop and a stop (since only intermediate
events count as stops). This means that if we multiply the hop and stop
amplitudes from [11, 12] we should get something that matches the jump
amplitudes in the following calculations. Furthermore, since the last jump
includes only a hop we must divide the trajectory’s probability amplitude by
the stop amplitude to get its contribution to the propagator. This means our
unit constant $a$ should be the inverse of the stop amplitude. Note that the
unit constant $a$ introduced in the previous section is not the same as the
hop amplitude $a$ from [11, 12].

####  III.1.2 Results in 2 Dimensions

In 2 dimensions, the retarded propagator takes the form:

$K(y-x)=\nu(y-x)\frac{1}{2}J_{0}\Big{(}m\tau(y-x)\Big{)}$ (29)

Using equation 24, in order for the path sum to match this on average, the
average jump amplitudes must be:

$T(y-x)=\frac{1}{a}\nu(y-x)\frac{1}{2}J_{0}\Big{(}\pm\beta m\tau(y-x)\Big{)}$
(30)

The derivation discussed in [11] is equivalent to setting
$a=-\frac{\rho}{m^{2}}$. When this choice is made we get:

$\beta=\sqrt{1+\frac{\rho}{m^{2}a}}=0$ (31)
$T(y-x)=-\frac{m^{2}}{\rho}\frac{1}{2}\nu(y-x)$ (32)

The $\Theta$-functions ensure that jumps are only allowed from $x$ to $y$ if
$x\prec y$. This result then says a jump to such a future-connected event
should have an amplitude of $-\frac{m^{2}}{2\rho}$. This is equivalent to the
result of [11] where $-\frac{m^{2}}{2\rho}$ is the product of the hop and stop
amplitudes.

####  III.1.3 Results in 4 Dimensions

In 4 Dimensions, the retarded propagator takes the form:

$\displaystyle
K(y-x)=\nu(y-x)\bigg{(}\frac{1}{2\pi}\delta\Big{(}\tau(y-x)^{2}\Big{)}$
$\displaystyle-\frac{m}{4\pi\tau(y-x)}J_{1}\Big{(}m\tau(y-x)\Big{)}\bigg{)}$
(33)

This means the jump amplitudes must be of the form:

$\displaystyle
T(y-x)=\frac{1}{a}\nu(y-x)\bigg{(}\frac{1}{2\pi}\delta\Big{(}\tau(y-x)^{2}\Big{)}$
$\displaystyle-\frac{\pm\beta m}{4\pi\tau(y-x)}J_{1}\Big{(}\pm\beta
m\tau(y-x)\Big{)}\bigg{)}$ (34)

If we again set $a=-\frac{\rho}{m^{2}}$ and $\beta=0$ we get:

$T(y-x)=-\frac{m^{2}}{\rho}\frac{1}{2\pi}\delta\Big{(}\tau(y-x)^{2}\Big{)}\nu(y-x)$
(35)

As discussed in [11], we will need the result:

$\lim_{\rho\to\infty}\sqrt{\rho}\mu(y-x)=\frac{\sqrt{24}}{2}\delta\Big{(}\tau(y-x)^{2}\Big{)}\nu(y-x)$
(36)

Here I have again used $\mu(y-x)$ to represent the probability that $x$ is
linked to $y$. Then in the high density limit we have:

$T(y-x)\approx-\frac{m^{2}}{\rho}\frac{\sqrt{\rho}}{\sqrt{24}\pi}\mu(y-x)$
(37)

This says that if we allow only jumps between linked events and give them the
amplitude $-\frac{m^{2}}{\rho}\frac{\sqrt{\rho}}{\sqrt{24}\pi}$ then this will
give the correct propagator on average. This is the same as the product of hop
and stop amplitudes found in [11].

####  III.1.4 Numerical Results

While the previous calculations show that the causal set propagator should
match the continuum propagator for any value of $a$ on average, it is
conceivable that the variation may still be too large for the model to be
acceptable. To test this, we will use numerical simulations.

To start, events in the causal set are chosen using a Poisson sprinkling with
density $\rho=4500$ into a causal diamond in a flat 2D spacetime. Then the
causal order of the set is determined by assuming a Minkowski metric. The
proper time separating each pair of events is estimated from the causal
structure using equations 3 and 4. These proper times are used to calculate a
jump amplitude matrix:

$T_{xy}=C_{xy}\frac{m^{2}}{2\rho\alpha}J_{0}\left(\sqrt{1+\frac{1}{\alpha}}m\tau_{xy}\right)$
(38)

where $C_{xy}=1$ if $x\prec y$ and $0$ otherwise. Note that this formula has
the same form as the average jump amplitude from equation 30. In particular,
this formula assumes $a$ is of the form $a=\alpha\frac{\rho}{m^{2}}$.

There is a slight issue with this formula for the jump amplitudes. Even though
the average over sprinklings of $\tau_{xy}$ should be the manifold proper time
$\tau(y-x)$, the average over sprinklings of equation 38 will not always match
equation 30. This is because the average of a function is not generally the
same as the function of the average. However, we should expect this effect to
go away as $\rho\to\infty$ since the variation over sprinklings in $\tau_{xy}$
goes to zero in the limit [8].

Figure 4: Numerical results for the causal set retarded propagator (grey) and
the continuum retarded propagator (black) from a single sprinkling with
$\rho=4500$, $m=3$, and various values of $\alpha$. The propagators are
plotted as a function of the proper time measured in the manifold. The jump
amplitudes in this calculation are from equation 38 with the proper time
estimated from the causal structure using equations 3 and 4.

In figure 4, we see that this form of causal set propagator appears to agree
with the continuum propagator at various values of $\alpha$. The variation
also seems to decrease at larger proper times, though higher density
simulations over larger causal diamonds may be necessary to state this
conclusively.

While the variation does seem to be larger for positive values of $\alpha$,
there is good reason to believe this variation can be attributed to how we
have estimated the proper times used in the jump amplitudes. Figure 5 shows
the same graph for the propagator with $\alpha=1$, but in this case the jump
amplitudes were calculated with the manifold proper time instead of the causal
set estimate. As we can clearly see, the variation is significantly smaller.
Note that in equation 38, positive values of $\alpha$ will make the jump
amplitudes more sensitive to the proper time, so this variation is more
noticeable.

Figure 5: Numerical results for the causal set retarded propagator (grey) and
the continuum retarded propagator (black) from a single sprinkling with
$\rho=4500$, $m=3$, and $\alpha=1$. The propagators are plotted as a function
of the proper time measured in the manifold. The jump amplitudes in this
calculation are from equation 38 with the proper time calculated from the
manifold.

Though we have only discussed integer values of $\alpha$ so far, the only
limitation from the math is that $\alpha\neq 0$. Some conceptual problems do
arise from allowing $\alpha<<1$. If $\alpha$ was sufficiently small that could
cause $|T_{ij}|>1$ for some $i,j$. While, in theory, the path sum should still
average to the correct propagator, this situation would contradict the
probability amplitude interpretation of $T$.

We must also consider complex values of $\alpha$. $\alpha$ should be allowed
to be complex because both the jump amplitudes $T$ and the propagator $K$ can
be complex. Figure 6 shows the results for the 2D retarded propagator using
equation 38 with $\alpha=1+i$. As we can see, the causal set propagator is
still a close match for the continuum value.

Figure 6: Numerical results for the causal set retarded propagator (grey) and
the continuum retarded propagator (black) from a single sprinkling with
$\rho=4500$, $m=3$, and $\alpha=1+i$. The propagators are plotted as a
function of the proper time measured in the manifold. The jump amplitudes in
this calculation are from equation 38 with the proper time estimated from the
causal structure using equations 3 and 4. Plot (a) shows the real part of the
propagator and plot (b) shows the imaginary part.

###  III.2  Results for Feynman Propagator

The same process carried out to model the retarded propagator in the previous
subsection can also be applied to create a path sum for the Feynman
propagator. While past work such as [14] considered how one could obtain the
Feynman propagator for a free scalar field from the retarded and advanced
propagators, that work did not express the Feynman propagator as a path sum.
This is useful to consider since, in a continuum calculation, the Feynman
propagator can be directly calculated as a path integral but the retarded
propagator cannot [10].

In two dimensions [15], the Feynman propagator is

$\displaystyle
K(y-x)=\Theta(\tau_{xy}^{2})\left(-\frac{i}{4}H_{0}^{(2)}(m\tau_{xy})\right)$
$\displaystyle+\Theta(-\tau_{xy}^{2})\left(\frac{1}{2\pi}K_{0}(ms_{xy})\right)$
(39)

where $s_{xy}=\sqrt{-\tau_{xy}^{2}}$. Then, using equation 24, we must have
the jump amplitude function

$\displaystyle
T(y-x)=\Theta(\tau_{xy}^{2})\left(-\frac{i}{4a}H_{0}^{(2)}(\pm\beta
m\tau_{xy})\right)$ $\displaystyle+\Theta(-\tau_{xy}^{2})\left(\frac{1}{2\pi
a}K_{0}(\pm\beta ms_{xy})\right)$ (40)

Here, $H$ is a Hankel function and $K$ is a modified Bessel function. Note
that since $K_{0}$ decays for large arguments, spacelike jumps far from the
lightcone are very unlikely. By contrast, $H_{0}^{(2)}$ is oscillatory, so
timelike jumps far from the lightcone should still be expected.

In four dimensions [15], the Feynman propagator is

$\displaystyle
K(y-x)=\Theta(\tau_{xy}^{2})\left(\frac{m}{8\pi\tau_{xy}}H_{1}^{(1)}(m\tau_{xy})\right)$
$\displaystyle+\Theta(-\tau_{xy}^{2})\left(-\frac{im}{4\pi^{2}s_{xy}}K_{1}(ms_{xy})\right)$
(41)

This yields the corresponding jump amplitude function

$\displaystyle T(y-x)=\Theta(\tau_{xy}^{2})\left(\frac{\pm\beta m}{8\pi
a\tau_{xy}}H_{1}^{(1)}(\pm\beta m\tau_{xy})\right)$
$\displaystyle+\Theta(-\tau_{xy}^{2})\left(-\frac{\pm i\beta
m}{4\pi^{2}as_{xy}}K_{1}(\pm\beta ms_{xy})\right)$ (42)

If we follow the same reasoning as with the retarded propagator, we can
attempt to simplify the jump amplitudes in 4 dimensions by setting
$a=-\rho/m^{2}$ which sets $\beta=0$. While this does not fully remove the
$\tau$-dependence, it does greatly simplify the expression for $T(y-x)$. After
taking the limit as $\beta\to 0$, we find

$T(y-x)=\frac{im^{2}}{4\pi^{2}\rho|\tau_{xy}^{2}|}$ (43)

One challenge is that this path sum would be non-local, which makes it
difficult to verify these results numerically. A possible avenue for future
work would be to simulate this numerically over large finite region of a flat
spacetime to see if the results approach the continuum value for the
propagator. Then additional work may be necessary to show that trajectories
far from the lightcone do not contribute much. Alternatively, it may be
necessary to include boundary terms that account for the paths far from the
lightcone that cannot be modeled in a finite region.

##  IV  Conclusion

Constructing a propagator is a key step in establishing a field theory on a
causal set. While past work has shown examples of path sums for propagators
that match the continuum in the appropriate limits, these constructions were
not unique solutions. In this paper, we have derived a general equation for
how to relate the average value of a scalar field propagator to the possible
average jump amplitudes. This enabled us to solve for the jump amplitudes
necessary to recreate the correct continuum propagator on average. These were
tested numerically in the case of the 2 dimensional retarded propagator and
shown to match the continuum value. Even though these various constructions of
the propagators should agree for large proper times, at small proper times
they may differ greatly. This could make understanding possible values for
jump amplitudes important for the small scale dynamics of a quantum field
theory on a causal set.

###### Acknowledgements.

I would like to acknowledge my advisor, Dr. David Craig for the many
insightful conversations that shaped this paper. I would also like to
acknowledge Dr. Steven Johnston for feedback about the content of the paper.

## References

  * Hawking  _et al._ [1976] S. W. Hawking, A. R. King, and P. McCarthy, A new topology for curved space–time which incorporates the causal, differential, and conformal structures, Journal of mathematical physics 17, 174 (1976).
  * Malament [1977] D. Malament, Class of continuous timelike curves determines the topology of spacetime.[causal, topological, differential, and conformal structure], J. Math. Phys.(NY);(United States) 18 (1977).
  * Sorkin [2009] R. D. Sorkin, Light, links and causal sets, in  _Journal of Physics: Conference Series_ , Vol. 174 (IOP Publishing, 2009) p. 012018.
  * Bombelli  _et al._ [1987] L. Bombelli, J. Lee, D. Meyer, and R. D. Sorkin, Space-time as a causal set, Physical review letters 59, 521 (1987).
  * Surya [2019] S. Surya, The causal set approach to quantum gravity, Living Reviews in Relativity 22, 1 (2019).
  * Lewis and Shedler [1978] P. A. Lewis and G. S. Shedler,  _Simulation Methods for Poisson Processes in Nonstationary Systems._ , Tech. Rep. (NAVAL POSTGRADUATE SCHOOL MONTEREY CALIF, 1978).
  * Bombelli and Noldus [2004] L. Bombelli and J. Noldus, The moduli space of isometry classes of globally hyperbolic spacetimes, Classical and Quantum Gravity 21, 4429 (2004).
  * Roy  _et al._ [2013] M. Roy, D. Sinha, and S. Surya, Discrete geometry of a small causal diamond, Physical Review D 87, 044046 (2013).
  * Feynman [1948] R. P. Feynman, Space-time approach to non-relativistic quantum mechanics, Reviews of Modern Physics 20, 367 (1948).
  * Halliwell and Ortiz [1993] J. J. Halliwell and M. E. Ortiz, Sum-over-histories origin of the composition laws of relativistic quantum mechanics and quantum cosmology, Physical Review D 48, 748 (1993).
  * Johnston [2010] S. Johnston, Quantum fields on causal sets, arXiv preprint arXiv:1010.5514 (2010).
  * Johnston [2008] S. Johnston, Particle propagators on discrete spacetime, Classical and Quantum Gravity 25, 202001 (2008).
  * Scargle and Simić [2009] J. D. Scargle and S. N. Simić, Photon dispersion in causal sets, arXiv preprint arXiv:0912.3839 (2009).
  * Johnston [2009] S. Johnston, Feynman propagator for a free scalar field on a causal set, Physical Review Letters 103, 10.1103/physrevlett.103.180401 (2009).
  * Hong-Hao  _et al._ [2010] Z. Hong-Hao, F. Kai-Xi, Q. Si-Wei, Z. An, and L. Xue-Song, On analytic formulas of feynman propagators in position space, Chinese Physics C 34, 1576 (2010).


such that $x\stackrel{{\scriptstyle\sigma_{1}}}{{\leftrightarrow}}x^{\prime}$
and $x^{\prime}\alpha y$, then $\mathit{unfold}(x,\sigma_{1})\uparrow$ and
$\mathit{unfold}(\sigma_{1}(x),\sigma_{1})\uparrow$, hence $\sigma_{1}(x)$ is
a variable, and, since
$x\stackrel{{\scriptstyle\sigma_{1}}}{{\leftrightarrow}}\sigma_{1}(x)$, we get
$\sigma_{1}(x)\stackrel{{\scriptstyle\sigma_{1}}}{{\leftrightarrow}}x^{\prime}$,
hence, by definition of $s$,
$\theta_{1}(x)=\theta_{2}(y)=\theta_{1}(\sigma_{1}(x))=\sigma_{1}(x)\,\theta_{1}$;
otherwise, we have $\theta_{1}(x)=s(x)\,\theta_{1}=\sigma_{1}(x)\,\theta_{1}$,
as needed.

Finally, we can prove by coinduction that, for all open values
${\mathrm{v}}^{\prime}_{1}$ and ${\mathrm{v}}^{\prime}_{2}$ such that
$\textit{FV}({\mathrm{v}}^{\prime}_{1})\subseteq\mathit{dom}(\sigma_{1})$ and
$\textit{FV}({\mathrm{v}}^{\prime}_{2})\subseteq\mathit{dom}(\sigma_{2})$, if
$\mathit{T}({\mathrm{v}}^{\prime}_{1},\sigma_{1})=_{\alpha}\mathit{T}({\mathrm{v}}^{\prime}_{2},\sigma_{2})$
then
${\mathrm{v}}^{\prime}_{1}\,\theta_{1}={\mathrm{v}}^{\prime}_{2}\,\theta_{2}$.
There are two cases:

  * •

if $\mathit{unfold}({\mathrm{v}}^{\prime}_{1},\sigma_{1})\uparrow$, then
${\mathrm{v}}^{\prime}_{1}{=}x$, ${\mathrm{v}}^{\prime}_{2}=y$,
$\mathit{unfold}(y,\sigma_{2})\uparrow$ and $x\alpha y$, hence the thesis
follows by construction of $\theta_{1}$;

  * •

if $\mathit{unfold}({\mathrm{v}}^{\prime}_{1},\sigma_{1}){=}\texttt{new}\
\mathit{C}({\mathrm{v}}_{1,1},\ldots,{\mathrm{v}}_{1,n})$, then
$\mathit{T}({\mathrm{v}}^{\prime}_{1},\sigma_{1})=\texttt{new}\
\mathit{C}(\mathit{T}({\mathrm{v}}_{1,1},\sigma_{1}),\ldots,\mathit{T}({\mathrm{v}}_{1,n},\sigma_{1}))$
and $\mathit{T}({\mathrm{v}}^{\prime}_{2},\sigma_{2})=\texttt{new}\
\mathit{C}(\mathit{T}({\mathrm{v}}_{2,1},\sigma_{2}),\ldots,\mathit{T}({\mathrm{v}}_{2,n},\sigma_{2}))$,
hence, for all $1\in 1..n$ we have
$\mathit{T}({\mathrm{v}}_{1,i},\sigma_{1})=_{R}\mathit{T}({\mathrm{v}}_{2,i},\sigma_{2})$,
then the thesis follows by coinductive hypothesis.

Therefore, this proves that
$\llbracket{\mathrm{v}}_{2},\sigma_{2}\rrbracket\subseteq\llbracket{\mathrm{v}}_{1},\sigma_{1}\rrbracket$.
To get the other inclusion, it is enough to note that, if
$\mathit{T}({\mathrm{v}}_{1},\sigma_{1})=_{\alpha}\mathit{T}({\mathrm{v}}_{2},\sigma_{2})$,
then
$\mathit{T}({\mathrm{v}}_{2},\sigma_{2})=_{\alpha^{\circ}}\mathit{T}({\mathrm{v}}_{1},\sigma_{1})$,
hence the thesis follows from what we have just proved.

######  Proof A.4 (Proof of Prop. 6.6).

If $\mathit{unfold}({\mathrm{v}}_{1},\sigma_{1})\uparrow$ and
$\mathit{unfold}({\mathrm{v}}_{2},\sigma_{2})=\texttt{new}\
\mathit{C}({\mathrm{v}}^{\prime}_{1},\ldots,{\mathrm{v}}^{\prime}_{n})$, then
${\mathrm{v}}_{1}=x$ for some undetermined variable
$x\in\mathit{dom}(\sigma_{1})$ hence
$\llbracket{\mathrm{v}}_{1},\sigma_{1}\rrbracket={\cal V}\textsuperscript{a}$.
Instead, if $\textit{v}\in\llbracket{\mathrm{v}}_{2},\sigma_{2}\rrbracket$, we
have $\textit{v}=\texttt{new}\
\mathit{C}(\textit{v}_{1},\ldots,\textit{v}_{n})$. Therefore, the value
$\texttt{new}\
\mathit{C}(\textit{v}^{\prime}_{1},\ldots,\textit{v}^{\prime}_{n+1})\in{\cal
V}\textsuperscript{a}$ exists by definition of values, but it does not belong
to $\llbracket{\mathrm{v}}_{2},\sigma_{2}\rrbracket$, which is a
contradiction. This proves 1 and the first part of 2. To conclude, assume
$\mathit{unfold}({\mathrm{v}}_{1},\sigma_{1})=\texttt{new}\
\mathit{C}({\mathrm{v}}_{1,1},\ldots,{\mathrm{v}}_{1,n})$ and
$\mathit{unfold}({\mathrm{v}}_{2},\sigma_{2})=\texttt{new}\
\mathit{C}({\mathrm{v}}_{2,1},\ldots,{\mathrm{v}}_{2,n})$, and consider $i\in
1..n$. Consider a solution $\theta_{1}\in\textsf{Sol}(\sigma_{1})$, then
${\mathrm{v}}_{1,i}\,\theta_{1}\in\llbracket{\mathrm{v}}_{1,i},\sigma_{1}\rrbracket$,
and we have to prove
${\mathrm{v}}_{1,i}\,\theta_{1}\in\llbracket{\mathrm{v}}_{2,i},\sigma_{2}\rrbracket$.
By hypothesis, we know that there is a solution
$\theta_{2}\in\textsf{Sol}(\sigma_{2})$ such that
${\mathrm{v}}_{1}\,\theta_{1}={\mathrm{v}}_{2}\,\theta_{2}$, hence, by Prop.
6.2(4), we get $\texttt{new}\
\mathit{C}({\mathrm{v}}_{1,1}\,\theta_{1},\ldots,{\mathrm{v}}_{1,n}\,\theta_{1})=\texttt{new}\
\mathit{C}(\mathit{C}\,{\mathrm{v}}_{2,1}{\theta_{2}},\ldots,{\mathrm{v}}_{2,n}\,\theta_{2})$,
and in particular
${\mathrm{v}}_{1,i}\,\theta_{1}={\mathrm{v}}_{2,i}\,\theta_{2}\in\llbracket{\mathrm{v}}_{2,i},\sigma_{2}\rrbracket$,
as needed. This proves
$\llbracket{\mathrm{v}}_{1,i},\sigma_{1}\rrbracket\subseteq\llbracket{\mathrm{v}}_{2,i},\sigma_{2}\rrbracket$,
the other inclusion is immeidate.

######  Proof A.5 (Proof of Lemma 6.7).

Following [12], given an infinite open value $t$, each subtree of $t$ is
identified by a finite sequence $\beta$ of positive natural numbers, and it
will be denoted by $t(\beta)$. Extending the notation for capsules, we denote
by $\llbracket t,\sigma\rrbracket$ the set
$\\{t\,\theta\mid\theta\in\textsf{Sol}(\sigma)\\}$. Set
$t_{1}=\mathit{T}({\mathrm{v}}_{1},\sigma_{1})$ and
$t_{2}=\mathit{T}({\mathrm{v}}_{2},\sigma_{2})$, we prove that for all
$\beta$, if $\llbracket t_{1}(\beta),\sigma_{1}\rrbracket=\llbracket
t_{2}(\beta),\sigma_{2}\rrbracket$ then either $t_{1}(\beta)$ and
$t_{2}(\beta)$ are both variables, or $t_{1}(\beta)=\texttt{new}\
\mathit{C}(t_{1}(\beta 1),\ldots,t_{1}(\beta n))$, $t_{2}(\beta)=\texttt{new}\
\mathit{C}(t_{2}(\beta 1),\ldots,t_{2}(\beta n))$ and, for all $i\in 1..n$,
$\llbracket t_{1}(\beta i),\sigma_{1}\rrbracket=\llbracket t_{2}(\beta
i),\sigma_{2}\rrbracket$. The proof is by induction on $\beta$, since by
hypothesis $\llbracket t_{1},\sigma_{1}\rrbracket=\llbracket
t_{2},\sigma_{2}\rrbracket$ and using Prop. 6.6.

We define a relation
$\alpha\subseteq\textit{FV}(t_{1})\times\textit{FV}(t_{2})$ as follows:
$x\alpha y$ iff there is a sequence $\beta$ such that $x=t_{1}(\beta)$ and
$y=t_{2}(\beta)$. We verify it is a $\sigma_{1},\sigma_{2}$-renaming. . First
note that if $x\alpha y$, since $\llbracket
t_{1},\sigma_{1}\rrbracket=\llbracket t_{2},\sigma_{2}\rrbracket$, for all
$\theta_{1}\in\textsf{Sol}(\sigma_{1})$ and
$\theta_{2}\in\textsf{Sol}(\sigma_{2})$, if
$t_{1}\,\theta_{1}=t_{2}\,\theta_{2}$, then $\theta_{1}(x)=\theta_{2}(y)$.
Then, if $x_{1}\alpha y_{1}$, $x_{2}\alpha y_{2}$ and
$x_{1}\stackrel{{\scriptstyle\sigma_{1}}}{{\leftrightarrow}}x_{2}$, we have to
prove $y_{1}\stackrel{{\scriptstyle\sigma_{2}}}{{\leftrightarrow}}y_{2}$. By
contradiction, if
$y_{1}\stackrel{{\scriptstyle\sigma_{2}}}{{\leftrightarrow}}y_{2}$ does not
hold, since both $y_{1}$ and $y_{2}$ are undetermined variables by Prop.
6.2(2), there is a solution $\theta_{2}\in\textsf{Sol}(\sigma_{2})$ such that
$\theta_{2}(y_{1})\neq\theta_{2}(y_{2})$. Because $\llbracket
t_{1},\sigma_{1}\rrbracket=\llbracket t_{2},\sigma_{2}\rrbracket$, there is a
solution $\theta_{1}\in\textsf{Sol}(\sigma_{1})$ such that
$t_{1}\,\theta_{1}=t_{2}\,\theta_{2}$, hence, since $x_{1}\alpha y_{1}$ and
$x_{2}\alpha y_{2}$ we get, by definition of $\alpha$,
$\theta_{1}(x_{1})=\theta_{2}(y_{1})$ and
$\theta_{1}(x_{2})=\theta_{2}(y_{2})$. Now, since
$x_{1}\stackrel{{\scriptstyle\sigma_{1}}}{{\leftrightarrow}}x_{2}$, by Prop.
6.2(3), we have $\theta_{1}(x_{1})=\theta_{1}(x_{2})$, hence
$\theta_{2}(y_{1})=\theta_{2}(y_{2})$, which is a contradiction. The proof of
the other direction is the same.

Finally, we can prove by coinduction that, for all $\beta$,
$t_{1}(\beta)=_{\alpha}t_{2}(\beta)$, which, in particular, implies the
thesis.

######  Proof A.6 (Proof of Lemma 6.9).

We define systems of equations $s_{2}$ and $s_{1}$ as follows:

$s_{2}(x)=\begin{cases}\theta(x)&x\in\mathit{dom}(\sigma_{2}\cap\sigma_{1})\\\
\sigma_{2}(x)&\text{otherwise}\end{cases}$

$s_{1}(x)=\begin{cases}\theta(x)&x\in\mathit{dom}(\sigma_{1}\cap\sigma_{2})\\\
\theta_{2}(y)&x\notin\mathit{dom}(\sigma_{1}\cap\sigma_{2})\text{ and }\exists
x^{\prime}\in\mathit{dom}(\sigma_{1}).\
x\stackrel{{\scriptstyle\sigma_{1}}}{{\leftrightarrow}}x^{\prime}\text{ and
}x^{\prime}\alpha y\\\ \sigma_{1}(x)&\text{otherwise}\end{cases}$

Both systems are well-defined since $\alpha$ is a
$\sigma_{2},\sigma_{1}$-renaming (see the proof of Lemma 6.5 for details), and
have solutions $\theta_{2}$ and $\theta_{1}$, respectively, by results in
[12].

The fact that $\theta_{2}\in\textsf{Sol}(\sigma_{2})$ is trivial. We now prove
$\theta_{1}\in\textsf{Sol}(\sigma_{1})$. We have three cases:

  * •

If $x\in\mathit{dom}(\sigma_{1}\cap\sigma_{2})$, then
$\sigma_{1}(x)\,\theta_{1}=(\sigma_{1}\cap\sigma_{2})(x)\,\theta_{1}$ and, by
definition,
$\textit{FV}((\sigma_{1}\cap\sigma_{2})(x))\subseteq\mathit{dom}(\sigma_{1}\cap\sigma_{2})$,
hence we get
$(\sigma_{1}\cap\sigma_{2})(x)\,\subset_{1}=(\sigma_{1}\cap\sigma_{2})(x)\,\theta=\theta(x)$;
thus $\sigma_{1}(x)\,\theta_{1}=\theta(x)=\theta_{1}(x)$.

  * •

If $x\notin\mathit{dom}(\sigma_{1}\cap\sigma_{2})$ and there is
$x^{\prime}\in\mathit{dom}(\sigma_{1})$ such that
$x\stackrel{{\scriptstyle\sigma_{1}}}{{\leftrightarrow}}x^{\prime}$ and
$x^{\prime}\alpha y$, then $\theta_{1}(x)=\theta_{2}(y)$,
$\mathit{unfold}(\sigma_{1}(x),\sigma_{1})\uparrow$ and
$x\stackrel{{\scriptstyle\sigma_{1}}}{{\leftrightarrow}}\sigma_{1}(x)$, hence
we have to prove $\theta_{1}(\sigma_{1}(x))=\theta_{2}(y)$. Now, if
$\sigma_{1}(x)\in\mathit{dom}(\sigma_{1}\cap\sigma_{2})$, then
$\sigma_{1}(x)\in\mathit{dom}(\sigma_{2})$, hence, since $\alpha$ is strict,
we have
$\sigma_{1}(x)\stackrel{{\scriptstyle\sigma_{2}}}{{\leftrightarrow}}y$. Thus
we get, by Prop. 6.2(3), $\theta_{2}(y)=\theta_{2}(\sigma_{1}(x))$, and, by
definition, we have
$\theta_{2}(\sigma_{1}(x))=\theta(\sigma_{1}(x))=\theta_{1}(\sigma_{1}(x))$,
hence $\theta_{1}(x)=\theta_{2}(y)=\theta_{1}(\sigma_{1}(x))$.

  * •

Otherwise, we have
$\theta_{1}(x)=s_{1}(x)\,\theta_{1}=\sigma_{1}(x)\,\theta_{1}$.

Furthermore, we also have that, for all
$x\in\mathit{dom}(\sigma_{1}\cap\sigma_{2})$,
$<subst_{1}(x)=\theta(x)=\theta_{2}(x)$.

We now prove, by coinduction, that if
$({{{\mathrm{v}}^{\prime}_{1}},{\sigma_{1}}}){\approx_{\alpha}}({{{\mathrm{v}}^{\prime}_{2}},{\sigma_{2}}})$
then
${\mathrm{v}}^{\prime}_{1}\,\theta_{1}={\mathrm{v}}^{\prime}_{2}\,\theta_{2}$,
which in particular implies the thesis. If
$\mathit{unfold}({\mathrm{v}}^{\prime}_{1},\sigma_{1})\uparrow$, then
$\mathit{unfold}({\mathrm{v}}^{\prime}_{2},\sigma_{2})\uparrow$,
${\mathrm{v}}^{\prime}_{1}=x$, ${\mathrm{v}}^{\prime}_{2}=y$ and $x\alpha y$,
hence, by definition, $\theta_{1}(x)=\theta_{2}(y)$, as needed. Otherwise, the
thesis follows from Prop. 6.2(4) and coinduction hypothesis.

######  Proof A.7 (Proof of Lemma 6.13).

By induction on the definition of
$\textit{e},\sigma,\tau\\!\Downarrow\\!{\mathrm{v}},{\sigma^{\prime}}$.

(val): We have that
${\mathrm{v}},\sigma,\tau\\!\Downarrow\\!{\mathrm{v}},{\sigma}$. The thesis
trivially holds since $\sigma\leq\sigma$.

(field): By inductive hypothesis,
$\textit{e},\sigma,\tau\\!\Downarrow\\!{\mathrm{v}},{\sigma^{\prime}}$ holds,
and $\sigma\leq{\sigma^{\prime}}$. Hence,
$\textit{e}.\mathit{f},\sigma,\tau\\!\Downarrow\\!{\mathrm{v}}_{i},{\sigma^{\prime}}$
holds as well, and $\sigma\leq{\sigma^{\prime}}$.

(new): By inductive hypothesis,
$\textit{e}_{i},\sigma,\tau\\!\Downarrow\\!{\mathrm{v}}_{i},{{\sigma^{\prime}}}_{i}$
holds for all $i\in 1..n$, and $\sigma\leq{\sigma^{\prime}}_{i}$ for all $i\in
1..n$. Hence, $\texttt{new}\
\mathit{C}(\textit{e}_{1},\ldots,\textit{e}_{n}),\sigma,\tau\\!\Downarrow\\!\texttt{new}\
\mathit{C}({\mathrm{v}}_{1}\ldots{\mathrm{v}}_{n}),\bigsqcup_{i\in
1..n}{\sigma^{\prime}}_{i}$ holds as well, and, since
$\sigma\leq{\sigma^{\prime}}_{i}$ for all $i\in 1..n$, we have that
$\sigma\leq\bigsqcup_{i\in 1..n}{\sigma^{\prime}}_{i}$.

(invk-ok): By inductive hypothesis,
$\textit{e}_{i},\sigma,\tau\\!\Downarrow\\!{\mathrm{v}}_{i},{{\sigma^{\prime}}}_{i}$
holds for all $i\in 1..n$,
$\textit{e}[{\mathrm{v}}_{0}/\texttt{this}][\overline{{\mathrm{v}}}/\overline{\textit{x}}],{\widehat{\sigma}},{{\tau}\\{c:\\!x\\}}\\!\Downarrow\\!{\mathrm{v}},{\sigma^{\prime}}$
holds, $\sigma\leq{\sigma^{\prime}}_{i}$ for all $i\in 1..n$, and
${\widehat{\sigma}}\leq{\sigma^{\prime}}$. Hence,
$\textit{e}_{0}.\textit{m}(\overline{\textit{e}}),\sigma,\tau\\!\Downarrow\\!{\mathrm{v}},{\sigma^{\prime}}$
holds as well and, since $\sigma\leq{\widehat{\sigma}}$, and by the
transitivity of the relation $\leq$, $\sigma\leq{\sigma^{\prime}}$.

(invk-check): By inductive hypothesis,
$\textit{e}_{i},\sigma,\tau\\!\Downarrow\\!{\mathrm{v}}_{i},{{\sigma^{\prime}}}_{i}$
holds for all $i\in 1..n$,
$\textit{e}[{\mathrm{v}}_{0}/\texttt{this}][\overline{{\mathrm{v}}}/\overline{\textit{x}}],{\widehat{\sigma}},{{\tau}\\{c:\\!x\\}}\\!\Downarrow\\!{\mathrm{v}},{\sigma^{\prime}}$
holds,
$\textit{e}[{\mathrm{v}}_{0}/\texttt{this}][\overline{{\mathrm{v}}}/\overline{\textit{x}}],{\widehat{\sigma}}\sqcup{\sigma^{\prime}}\\{x:\\!{\mathrm{v}}\\},{\tau}\\{c:\\!x^{{\textsf{ck}}}\\}\\!\Downarrow\\!{\mathrm{v}}^{\prime},\sigma^{\prime\prime}$
holds, $\sigma\leq{\sigma^{\prime}}_{i}$ for all $i\in 1..n$,
${\widehat{\sigma}}\leq{\sigma^{\prime}}$, and
${\widehat{\sigma}}\sqcup{\sigma^{\prime}}\\{x:\\!{\mathrm{v}}\\}\leq\sigma^{\prime\prime}$.
Hence,
$\textit{e}_{0}.\textit{m}(\overline{\textit{e}}),\sigma,\tau\\!\Downarrow\\!\textit{x},{{\sigma^{\prime}}}\\{\textit{x}:\\!{\mathrm{v}}\\}$
holds as well and, since $\sigma\leq{\widehat{\sigma}}\leq{\sigma^{\prime}}$,
we have that $\sigma\leq{{\sigma^{\prime}}}\\{\textit{x}:\\!{\mathrm{v}}\\}$.

(corec): By inductive hypothesis,
$\textit{e}_{i},\sigma,\tau\\!\Downarrow\\!{\mathrm{v}}_{i},{{\sigma^{\prime}}}_{i}$
holds for all $i\in 1..n$,
$\textit{e}^{\prime}[{\mathrm{v}}_{0}/\texttt{this}][\overline{{\mathrm{v}}}/\overline{\textit{x}}][x/\texttt{any}],{{{\widehat{\sigma}}}\\{\textit{x}:\\!\textit{x}\\}},\tau\\!\Downarrow\\!{\mathrm{v}},{\sigma^{\prime}}$
holds, $\sigma\leq{\sigma^{\prime}}_{i}$ for all $i\in 1..n$, and
${{\widehat{\sigma}}}\\{\textit{x}:\\!\textit{x}\\}\leq{\sigma^{\prime}}$.
Hence,
$\textit{e}_{0}.\textit{m}(\textit{e}_{1},\ldots,\textit{e}_{n}),\sigma,\tau\\!\Downarrow\\!{\mathrm{v}},{\sigma^{\prime}}$
holds and, since
$\sigma\leq{{\widehat{\sigma}}}\\{\textit{x}:\\!\textit{x}\\}$, and by the
transitivity of the relation $\leq$,
$\sigma\leq{{{\sigma^{\prime}}}\\{\textit{x}:\\!\textit{x}\\}}$.

(look-up): By inductive hypothesis,
$\textit{e}_{i},\sigma,\tau\\!\Downarrow\\!{\mathrm{v}}_{i},{{\sigma^{\prime}}}_{i}$
holds for all $i\in 1..n$, and $\sigma\leq{\sigma^{\prime}}_{i}$ for all $i\in
1..n$. Hence,
$\textit{e}_{0}.\textit{m}(\overline{\textit{e}}),\sigma,\tau\\!\Downarrow\\!\textit{x},{\widehat{\sigma}}$
holds, and, $\sigma\leq{\widehat{\sigma}}$.

######  Proof A.8 (Proof of Lemma 6.17).

By induction on the definition of
$\textit{e},\emptyset,S\\!\Downarrow_{\textsc{IN}}\\!\textit{v},S^{\prime}$.

(IN-val)

By hypothesis, we have that
$\textit{v},\emptyset,S\\!\Downarrow_{\textsc{IN}}\\!\textit{v},\emptyset$.
The thesis is immediate by applying rule (abs-co-val).

(IN-field)

By hypothesis, we have that
$\textit{e},\emptyset,S\\!\Downarrow_{\textsc{IN}}\\!\textit{v},S^{\prime}$.
By inductive hypothesis, ${\cal I}_{\scriptscriptstyle\textsc{FJ}}{\cup}{\cal
I}^{co}_{\scriptscriptstyle\textsc{FJ}}\\!\vdash\\!{\textit{e}\\!\Downarrow\\!\textit{v}}$
holds. Thus, we can apply rule (abs-field) and get the thesis.

(IN-new)

By hypothesis, we have that
$\textit{e}_{i},\emptyset,S\\!\Downarrow_{\textsc{IN}}\\!\textit{v}_{i},S^{\prime}_{i}$
for all $i\in 1..n$. By inductive hypothesis, ${\cal
I}_{\scriptscriptstyle\textsc{FJ}}{\cup}{\cal
I}^{co}_{\scriptscriptstyle\textsc{FJ}}\\!\vdash\\!{\textit{e}_{i}\\!\Downarrow\\!\textit{v}_{i}}$
holds for all $i\in 1..n$. Thus, we can apply rule (abs-new) and get the
thesis.

(IN-invk-ok)-(IN-invk-check)

By hypothesis,
$\textit{e}_{i},\emptyset,S\\!\Downarrow_{\textsc{IN}}\\!\textit{v}_{i},S^{\prime}_{i}$
holds for all $i\in 0..n$, and
$\textit{e}[\textit{v}_{0}/\texttt{this}][\overline{\textit{v}}/\overline{\textit{x}}],\emptyset,S\cup\\{\mathit{c}\\}\\!\Downarrow_{\textsc{IN}}\\!\textit{v},S^{\prime}$
holds. By inductive hypothesis, ${\cal
I}_{\scriptscriptstyle\textsc{FJ}}{\cup}{\cal
I}^{co}_{\scriptscriptstyle\textsc{FJ}}\\!\vdash\\!{\textit{e}_{i}\\!\Downarrow\\!\textit{v}_{i}}$
holds for all $i\in 0..n$ and and also ${\cal
I}_{\scriptscriptstyle\textsc{FJ}}{\cup}{\cal
I}^{co}_{\scriptscriptstyle\textsc{FJ}}\\!\vdash\\!{\textit{e}[\textit{v}_{0}/\texttt{this}][\overline{\textit{v}}/\overline{\textit{x}}]\\!\Downarrow\\!\textit{v}}$
holds. Thus, we can apply rule (abs-invk) and get the thesis. Note that, in
order to get the thesis, the third premise of rule (invk-check) has not been
used.

(IN-corec)

By hypothesis,
$\textit{e}_{i},\emptyset,S\\!\Downarrow_{\textsc{IN}}\\!\textit{v}_{i},S^{\prime}_{i}$
holds for all $i\in 0..n$., and
$\textit{e}^{\prime}[\textit{v}_{0}/\texttt{this}][\overline{\textit{v}}/\overline{\textit{x}}][u/\texttt{any}],\emptyset,S\\!\Downarrow_{\textsc{IN}}\\!\textit{v},S^{\prime}$
holds. By inductive hypothesis, ${\cal
I}_{\scriptscriptstyle\textsc{FJ}}{\cup}{\cal
I}^{co}_{\scriptscriptstyle\textsc{FJ}}\\!\vdash\\!{\textit{e}_{i}\\!\Downarrow\\!\textit{v}_{i}}$
holds for all $i\in 0..n$, and also ${\cal
I}_{\scriptscriptstyle\textsc{FJ}}{\cup}{\cal
I}^{co}_{\scriptscriptstyle\textsc{FJ}}\\!\vdash\\!{\textit{e}^{\prime}[\textit{v}_{0}/\texttt{this}][\overline{\textit{v}}/\overline{\textit{x}}][u/\texttt{any}]\\!\Downarrow\\!\textit{v}}$
holds. Thus, we can apply rule (abs-co-invk) and get the thesis.

(IN-look-up)

This case is empty since to apply the rule it should be $\rho\neq\emptyset$.

######  Lemma A.9.

If
$\textit{e},\rho,S\cup\\{\mathit{c}\\}\\!\Downarrow_{\textsc{IN}}\\!\textit{v},S^{\prime}$,
and
$\textit{e},{\rho}\\{\mathit{c}:\\!\textit{v}\\},S\\!\Downarrow_{\textsc{IN}}\\!\textit{v},{S^{\prime\prime}}$,
then ${S^{\prime\prime}}\subseteq S^{\prime}\setminus\\{\mathit{c}\\}$.

######  Proof A.10.

By induction on the definition of
$\textit{e},\rho,S\cup\\{\mathit{c}\\}\\!\Downarrow_{\textsc{IN}}\\!\textit{v},S^{\prime}$.

######  Proof A.11 (Proof of Lemma 6.18).

For brevity, we use ${\hat{S}}$ in place of $S\cup\\{\mathit{c}\\}$. In rules
(IN-invk-ok), (IN-invk-check), (IN-corec) and (IN-look-up), ${\hat{S}}$
abbreviates $S\cup\\{\mathit{c}^{\prime}\\}$, so to distinguish between
different calls that could be present in the call trace at the same time.

By induction on the definition of
$\textit{e},\rho,{\hat{S}}\\!\Downarrow_{\textsc{IN}}\\!\textit{v},S^{\prime}$.

(IN-val)

By hypothesis,
$\textit{v},\rho,{\hat{S}}\\!\Downarrow_{\textsc{IN}}\\!\textit{v},\emptyset$.
We can trivially get the thesis by rule (IN-val)

(IN-field)

By hypothesis,
$\textit{e},\rho,{\hat{S}}\\!\Downarrow_{\textsc{IN}}\\!\textit{v},S^{\prime}$,
and $\mathit{c}\not\in S^{\prime}$. By inductive hypothesis,
$\textit{e},\rho,S\\!\Downarrow_{\textsc{IN}}\\!\textit{v},S^{\prime}$ holds.
Thus, we can apply rule (IN-field) and get the thesis.

(IN-new)

By hypothesis,
$\textit{e}_{i},\rho,{\hat{S}}\\!\Downarrow_{\textsc{IN}}\\!\textit{v}_{i},S^{\prime}_{i}$,
and $\mathit{c}\not\in S^{\prime}_{i}$ for all $i\in 1..n$. By inductive
hypothesis,
$\textit{e}_{i},\rho,S\\!\Downarrow_{\textsc{IN}}\\!\textit{v}_{i},S^{\prime}_{i}$
holds for all $i\in 1..n$. Thus, we can apply rule (IN-new) and get the
thesis.

(IN-invk-ok)

By hypothesis,
$\textit{e}_{i},\rho,{\hat{S}}\\!\Downarrow_{\textsc{IN}}\\!\textit{v}_{i},S^{\prime}_{i}$,
and $\mathit{c}^{\prime}\not\in S^{\prime}_{i}$ for all $i\in 0..n$. Also by
hypothesis,
$\textit{e}[\textit{v}_{0}/\texttt{this}][\overline{\textit{v}}/\overline{\textit{x}}],\rho,{\hat{S}}\cup\\{\mathit{c}\\}\\!\Downarrow_{\textsc{IN}}\\!\textit{v},S^{\prime}$
holds, and $\mathit{c}^{\prime}\not\in S^{\prime}$. By inductive hypothesis,
$\textit{e}_{i},\rho,S\\!\Downarrow_{\textsc{IN}}\\!\textit{v}_{i},S^{\prime}_{i}$
holds for all $i\in 0..n$ and
$\textit{e}[\textit{v}_{0}/\texttt{this}][\overline{\textit{v}}/\overline{\textit{x}}],\rho,S\cup\\{\mathit{c}\\}\\!\Downarrow_{\textsc{IN}}\\!\textit{v},S^{\prime}$
holds. Thus, we can apply rule (IN-invk-ok) and get the thesis.

(IN-invk-check)

By hypothesis,
$\textit{e}_{i},\rho,{\hat{S}}\\!\Downarrow_{\textsc{IN}}\\!\textit{v}_{i},S^{\prime}_{i}$,
and $\mathit{c}^{\prime}\not\in S^{\prime}_{i}$, hence by inductive
hypothesis,
$\textit{e}_{i},\rho,S\\!\Downarrow_{\textsc{IN}}\\!\textit{v}_{i},S^{\prime}_{i}$
holds, for all $i\in 0..n$. Moreover,
$\textit{e}[\textit{v}_{0}/\texttt{this}][\overline{\textit{v}}/\overline{\textit{x}}],\rho,{\hat{S}}\cup\\{\mathit{c}\\}\\!\Downarrow_{\textsc{IN}}\\!\textit{v},S^{\prime}$
holds with either $\mathit{c}^{\prime}\not\in S^{\prime}$ or
$\mathit{c}=\mathit{c}^{\prime}$. Then,
$\textit{e}[\textit{v}_{0}/\texttt{this}][\overline{\textit{v}}/\overline{\textit{x}}],\rho,S\cup\\{\mathit{c}\\}\\!\Downarrow_{\textsc{IN}}\\!\textit{v},S^{\prime}$
holds in the first case by inductive hypothesis, in the second case since
$S\cup\\{\mathit{c}\\}={\hat{S}}\cup\\{\mathit{c}\\}$. Finally,
$\textit{e}[\textit{v}_{0}/\texttt{this}][\overline{\textit{v}}/\overline{\textit{x}}],{\rho}\\{\mathit{c}:\\!\textit{v}\\},{\hat{S}}\\!\Downarrow_{\textsc{IN}}\\!\textit{v},{S^{\prime\prime}}$
holds, and, from Lemma A.9, $\mathit{c}^{\prime}\not\in S^{\prime\prime}$,
hence, by inductive hypothesis,
$\textit{e}[\textit{v}_{0}/\texttt{this}][\overline{\textit{v}}/\overline{\textit{x}}],{\rho}\\{\mathit{c}:\\!\textit{v}\\},S\\!\Downarrow_{\textsc{IN}}\\!\textit{v},{S^{\prime\prime}}$
hold. Thus, we can apply rule (IN-invk-check) and get the thesis.

(IN-corec)

By hypothesis,
$\textit{e}_{i},\rho,{\hat{S}}\\!\Downarrow_{\textsc{IN}}\\!\textit{v}_{i},S^{\prime}_{i}$
holds, and $\mathit{c}^{\prime}\not\in S^{\prime}_{i}$ for all $i\in 0..n$.
Also by hypothesis,
$\textit{e}^{\prime}[\textit{v}_{0}/\texttt{this}][\overline{\textit{v}}/\overline{\textit{x}}][u/\texttt{any}],\rho,{\hat{S}}\\!\Downarrow_{\textsc{IN}}\\!\textit{v},S^{\prime}$
holds and $\mathit{c}^{\prime}\not\in S^{\prime}$. By inductive hypothesis,
$\textit{e}_{i},\rho,S\\!\Downarrow_{\textsc{IN}}\\!\textit{v}_{i},S^{\prime}_{i}$
holds for all $i\in 0..n$ and
$\textit{e}^{\prime}[\textit{v}_{0}/\texttt{this}][\overline{\textit{v}}/\overline{\textit{x}}][u/\texttt{any}],\rho,S\\!\Downarrow_{\textsc{IN}}\\!\textit{v},\emptyset$
holds. Thus, we can apply rule (IN-corec) and get the thesis.

(IN-look-up)

By hypothesis,
$\textit{e}_{i},\rho,{\hat{S}}\\!\Downarrow_{\textsc{IN}}\\!\textit{v}_{i},S^{\prime}_{i}$
holds, and $\mathit{c}^{\prime}\not\in S^{\prime}_{i}$ for all $i\in 1..n$. By
inductive hypothesis,
$\textit{e}_{i},\rho,S\\!\Downarrow_{\textsc{IN}}\\!\textit{v}_{i},S^{\prime}_{i}$
holds $\forall i\in 0..n$. Thus, we can apply rule (IN-look-up) and get the
thesis.

######  Lemma A.12.

If $\textit{e},\rho,S\\!\Downarrow_{\textsc{IN}}\\!\textit{v},S^{\prime}$,
then the following judgments hold:

  1. 1.

$\textit{e},\rho,S\cup\\{\mathit{c}\\}\\!\Downarrow_{\textsc{IN}}\\!\textit{v},S^{\prime}$

  2. 2.

$\textit{e},{\rho}\\{\mathit{c}:\\!\textit{v}^{\prime}\\},S\\!\Downarrow_{\textsc{IN}}\\!\textit{v},S^{\prime}$
for any $\textit{v}^{\prime}\in{\cal V}\textsuperscript{a}$.

######  Proof A.13.

The proof of both points is by induction on the definition of
$\textit{e},\rho,S\\!\Downarrow_{\textsc{IN}}\\!\textit{v},S^{\prime}$.

######  Proof A.14 (Proof of Lemma 6.19).

In the proof of this lemma we will use $\rho^{\prime}$ in place of
${\rho}\\{\mathit{c}:\\!\textit{v}^{\prime}\\}$. In rules (IN-invk-ok), (IN-
invk-check), (IN-corec) and (IN-look-up), $\rho^{\prime}$ will be used in
place of ${\rho}\\{\mathit{c}^{\prime}:\\!\textit{v}^{\prime}\\}$ so to
distinguish between different calls that could be present in the call trace at
the same time.

We proceed by induction on the definition of
$\textit{e},\rho^{\prime},S\\!\Downarrow_{\textsc{IN}}\\!\textit{v},S^{\prime}$.

(IN-val)

By hypothesis,
$\textit{v},\rho^{\prime},S\\!\Downarrow_{\textsc{IN}}\\!\textit{v},\emptyset$.
The thesis trivially holds by applying rule (IN-val).

(IN-field)

By hypothesis,
$\textit{e},\rho^{\prime},S\\!\Downarrow_{\textsc{IN}}\\!\textit{v},S^{\prime}$.
By inductive hypothesis,
$\textit{e},\rho,S\\!\Downarrow_{\textsc{IN}}\\!\textit{v},S^{\prime}$ holds.
Thus, we can apply rule (IN-field) and get the thesis.

(IN-new)

By hypothesis,
$\textit{e}_{i},\rho^{\prime},S\\!\Downarrow_{\textsc{IN}}\\!\textit{v}_{i},S^{\prime}$
holds for all $i\in 1..n$. By inductive hypothesis,
$\textit{e}_{i},\rho,S\\!\Downarrow_{\textsc{IN}}\\!\textit{v}_{i},S^{\prime}_{i}$
holds for all $i\in 1..n$. Thus, we can apply rule (IN-new) and get the
thesis.

(IN-invk-ok)

By hypothesis,
$\textit{e}_{i},\rho^{\prime},S\\!\Downarrow_{\textsc{IN}}\\!\textit{v}_{i},S^{\prime}$
holds for all $i\in 0..n$. Also by hypothesis,
$\textit{e}[\textit{v}_{0}/\texttt{this}][\overline{\textit{v}}/\overline{\textit{x}}],\rho^{\prime},S\cup\\{\mathit{c}\\}\\!\Downarrow_{\textsc{IN}}\\!\textit{v},S^{\prime}$
holds. In order to use the inductive hypothesis, we apply Lemma A.12 to the
hypothesis
$\mathit{c}^{\prime},\rho,S\\!\Downarrow_{\textsc{IN}}\\!\textit{v}^{\prime},\emptyset$
and obtain
$\mathit{c}^{\prime},\rho,S\cup\\{\mathit{c}\\}\\!\Downarrow_{\textsc{IN}}\\!\textit{v}^{\prime},\emptyset$.
By inductive hypothesis,
$\textit{e}_{i},\rho,S\\!\Downarrow_{\textsc{IN}}\\!\textit{v}_{i},S^{\prime}_{i}$
holds for all $i\in 1..n$, and
$\textit{e}[\textit{v}_{0}/\texttt{this}][\overline{\textit{v}}/\overline{\textit{x}}],\rho,S\cup\\{\mathit{c}\\}\\!\Downarrow_{\textsc{IN}}\\!\textit{v},S^{\prime}$
holds. Thus, we can apply rule (IN-invk-ok) and get the thesis.

(IN-invk-check)

By hypothesis,
$\textit{e}_{i},\rho^{\prime},S\\!\Downarrow_{\textsc{IN}}\\!\textit{v}_{i},S^{\prime}$
holds for all $i\in 0..n$. Also by hypothesis,
$\textit{e}[\textit{v}_{0}/\texttt{this}][\overline{\textit{v}}/\overline{\textit{x}}],\rho^{\prime},S\cup\\{\mathit{c}\\}\\!\Downarrow_{\textsc{IN}}\\!\textit{v},S^{\prime}$
and
$\textit{e}[\textit{v}_{0}/\texttt{this}][\overline{\textit{v}}/\overline{\textit{x}}],{\rho^{\prime}}\\{\mathit{c}:\\!\textit{v}\\},S\\!\Downarrow_{\textsc{IN}}\\!\textit{v},{S^{\prime\prime}}$
hold. In order to use the inductive hypothesis, we apply Lemma A.12 to the
hypothesis
$\mathit{c}^{\prime},\rho,S\\!\Downarrow_{\textsc{IN}}\\!\textit{v}^{\prime},\emptyset$
and obtain
$\mathit{c}^{\prime},{\rho}\\{\mathit{c}:\\!\textit{v}\\},S\cup\\{\mathit{c}\\}\\!\Downarrow_{\textsc{IN}}\\!\textit{v}^{\prime},\emptyset$.
By inductive hypothesis,
$\textit{e}_{i},\rho,S\\!\Downarrow_{\textsc{IN}}\\!\textit{v}_{i},S^{\prime}_{i}$
holds for all $i\in 1..n$,
$\textit{e}[\textit{v}_{0}/\texttt{this}][\overline{\textit{v}}/\overline{\textit{x}}],\rho,S\cup\\{\mathit{c}\\}\\!\Downarrow_{\textsc{IN}}\\!\textit{v},S^{\prime}$
and
$\textit{e}[\textit{v}_{0}/\texttt{this}][\overline{\textit{v}}/\overline{\textit{x}}],{\rho}\\{\mathit{c}:\\!\textit{v}\\},S\\!\Downarrow_{\textsc{IN}}\\!\textit{v},{S^{\prime\prime}}$
hold. Thus, we can apply rule (IN-invk-check) and get the thesis.

(IN-corec)

By hypothesis,
$\textit{e}_{i},\rho^{\prime},S\\!\Downarrow_{\textsc{IN}}\\!\textit{v}_{i},S^{\prime}$
holds for all $i\in 0..n$. Also by hypothesis,
$\textit{e}^{\prime}[\textit{v}_{0}/\texttt{this}][\overline{\textit{v}}/\overline{\textit{x}}][u/\texttt{any}],\rho^{\prime},S\\!\Downarrow_{\textsc{IN}}\\!\textit{v},S^{\prime}$
holds. By inductive hypothesis,
$\textit{e}_{i},\rho,S\\!\Downarrow_{\textsc{IN}}\\!\textit{v}_{i},S^{\prime}_{i}$
holds for all $i\in 1..n$ and
$\textit{e}^{\prime}[\textit{v}_{0}/\texttt{this}][\overline{\textit{v}}/\overline{\textit{x}}][u/\texttt{any}],\rho,S\\!\Downarrow_{\textsc{IN}}\\!\textit{v},\emptyset$
holds. Thus, we can apply rule (IN-corec) and get the thesis.

(IN-look-up)

By hypothesis,
$\textit{e}_{i},\rho^{\prime},S\\!\Downarrow_{\textsc{IN}}\\!\textit{v}_{i},S^{\prime}$
holds for all $i\in 0..n$. By inductive hypothesis,
$\textit{e}_{i},\rho,S\\!\Downarrow_{\textsc{IN}}\\!\textit{v}_{i},S^{\prime}_{i}$
holds for all $i\in 1..n$. In order to proceed, we have to distinguish between
two cases (recall that
$\mathit{c}^{\prime}=\textit{v}_{0}^{\prime}.\textit{m}^{\prime}(\overline{\textit{v}}^{\prime})$
and $\mathit{c}=\textit{v}_{0}.\textit{m}(\overline{\textit{v}})$):

  * •

If $\mathit{c}^{\prime}\neq\mathit{c}$, then
$\rho^{\prime}(\mathit{c})=\rho(\mathit{c})=\textit{v}$, hence we get the
thesis by applying rule (look-up).

  * •

If $\mathit{c}^{\prime}=\mathit{c}$, then, since
$\mathit{c}^{\prime},\rho,S\\!\Downarrow_{\textsc{IN}}\\!\textit{v}^{\prime},S^{\prime}$
holds by hypothesis, and
$\textit{e}_{i},\rho,S\\!\Downarrow_{\textsc{IN}}\\!\textit{v}_{i},S^{\prime}$
holds by inductive hypothesis for all $i\in 0..n$, the judgment
$\textit{e}_{0}.\textit{m}(\overline{\textit{e}}),\rho,S\\!\Downarrow_{\textsc{IN}}\\!\textit{v}^{\prime},S^{\prime}$
can still be derived.

######  Proof A.15 (Proof of Theorem 6.14).

The proof is by induction on the definition of
$\textit{e},\sigma,\tau\\!\Downarrow\\!{\mathrm{v}},{\sigma^{\prime}}$.

(val)

Immediate by (IN-val), as $S^{\tau,\sigma}\setminus
S^{\tau,\sigma}=\emptyset$.

(field)

By induction hypothesis, we have
$\textit{e}\,\theta,\rho^{\tau}_{\theta},S^{\tau}_{\theta}\\!\Downarrow_{\textsc{IN}}\\!{\mathrm{v}}\,\theta,S$,
for some $S^{\tau,\sigma,\sigma^{\prime}}_{\theta}\subseteq S\subseteq
S^{\tau,\sigma^{\prime}}_{\theta}$ and, by Prop. 6.2(4), we get
${\mathrm{v}}\,\theta=\texttt{new}\
\mathit{C}({\mathrm{v}}_{1}\,\theta,\ldots,{\mathrm{v}}_{n}\,\theta)$, hence
the thesis follows by rule (IN-field).

(new)

Since $\sigma^{\prime}_{i}\leq\bigsqcup_{i\in 1..n}\sigma^{\prime}_{i}$, we
have $\theta\in\textsf{Sol}(\sigma^{\prime}_{i})$ by Lemma 6.12, hence, by
induction hypothesis, we have
$\textit{e}_{i}\,\theta,\rho^{\tau}_{\theta},S^{\tau}_{\theta}\\!\Downarrow_{\textsc{IN}}\\!{\mathrm{v}}_{i}\,\theta,S_{i}$,
with $S^{\tau,\sigma,\sigma_{i}}_{\theta}\subseteq S_{i}\subseteq
S^{\tau,\sigma^{\prime}_{i}}_{\theta}$, for all $i\in 1..n$. It is easy to see
that $S^{\tau,\bigsqcup_{i\in 1..n}\sigma^{\prime}_{i}}_{\theta}=\bigcup_{i\in
1..n}S^{\tau,\sigma^{\prime}_{i}}_{\theta}$, then, if
$\sigma^{\prime}=\bigsqcup_{i\in 1..n}\sigma^{\prime}_{i}$,
$S^{\tau,\sigma,\sigma^{\prime}}_{\theta}\subseteq\bigcup_{i\in
1..n}S_{i}\subseteq S^{\tau,\sigma^{\prime}}_{\theta}$, hence the thesis
follows by rule (IN-new).

(invk-ok)

Since $\sigma^{\prime}_{i}\leq{\widehat{\sigma}}\leq\sigma^{\prime}$, by Lemma
6.12, we get $\theta\in\textsf{Sol}(\sigma^{\prime}_{i})$, for all $i\in
1..n$. By induction hypothesis, we have
$\textit{e}_{i}\,\theta,\rho^{\tau}_{\theta},S^{\tau}_{\theta}\\!\Downarrow_{\textsc{IN}}\\!{\mathrm{v}}_{i}\,\theta,S_{i}$,
with $S^{\tau,\sigma,\sigma^{\prime}_{i}}_{\theta}\subseteq S_{i}\subseteq
S^{\tau,\sigma^{\prime}_{i}}_{\theta}$, for all $i\in 1..n$, and
$\textit{e}[{\mathrm{v}}_{0}/\texttt{this}][\overline{{\mathrm{v}}}/\overline{\textit{x}}]\,\theta,\rho^{\tau}_{\theta},S^{{{\tau}\\{\mathit{c}:\\!\textit{x}\\}}}_{\theta}\\!\Downarrow_{\textsc{IN}}\\!{\mathrm{v}}\,\theta,S$,
with
$S^{{{\tau}\\{\mathit{c}:\\!\textit{x}\\}},{\widehat{\sigma}},\sigma^{\prime}}_{\theta}\subseteq
S\subseteq
S^{{{\tau}\\{\mathit{c}:\\!\textit{x}\\}},\sigma^{\prime}}_{\theta}$. Then we
get $S^{\tau,\sigma,\sigma^{\prime}}_{\theta}\subseteq\bigcup_{i\in
1..n}S_{i}\cup S\subseteq S^{\tau,\sigma^{\prime}}_{\theta}$, hence, since
$S^{{\tau}\\{\mathit{c}:\\!\textit{x}\\}}_{\theta}=S^{\tau}_{\theta}\cup\\{\mathit{c}\,\theta\\}$,
in order to conclude by rule (IN-invk-ok), we have to prove that
$\mathit{c}\,\theta\notin S\setminus S^{\tau}_{\theta}$. Suppose
$\mathit{c}\,\theta\in S\setminus S^{\tau}_{\theta}\subseteq
S^{{{\tau}\\{\mathit{c}:\\!\textit{x}\\}},\sigma^{\prime}}_{\theta}\setminus
S^{\tau}_{\theta}$, hence, there is
$\mathit{c}^{\prime}\in{\mathit{dom}(\sigma^{\prime}\circ({\tau}\\{\mathit{c}:\\!\textit{x}\\})^{\neg\textsf{ck}})}$
such that $\mathit{c}^{\prime}\,\theta=\mathit{c}\,\theta$ and
$\mathit{c}^{\prime}\,\theta\notin S^{\tau}_{\theta}$. Since
$\textit{x}\notin\mathit{dom}(\sigma^{\prime})$, then
$\mathit{c}^{\prime}\neq\mathit{c}$, hence
$\mathit{c}^{\prime}\in{\mathit{dom}(\tau^{\neg\textsf{ck}})}$, hence
$\mathit{c}^{\prime}\,\theta\in S^{\tau}_{\theta}$, which is a contradiction.

(invk-check)

Since $\sigma^{\prime}_{i}\leq{\widehat{\sigma}}\leq\sigma^{\prime}$, by Lemma
6.12, we get $\theta\in\textsf{Sol}(\sigma^{\prime}_{i})$, for all $i\in
1..n$. By induction hypothesis, we have
$\textit{e}_{i}\,\theta,\rho^{\tau}_{\theta},S^{\tau}_{\theta}\\!\Downarrow_{\textsc{IN}}\\!{\mathrm{v}}_{i}\,\theta,S_{i}$,
with $S^{\tau,\sigma,\sigma^{\prime}_{i}}_{\theta}\subseteq S_{i}\subseteq
S^{\tau,\sigma^{\prime}_{i}}_{\theta}$, for all $i\in 1..n$, and
$\textit{e}[{\mathrm{v}}_{0}/\texttt{this}][\overline{{\mathrm{v}}}/\overline{\textit{x}}]\,\theta,\rho^{\tau}_{\theta},S^{{{\tau}\\{\mathit{c}:\\!\textit{x}\\}}}_{\theta}\\!\Downarrow_{\textsc{IN}}\\!{\mathrm{v}}\,\theta,S$,
with
$S^{{{\tau}\\{\mathit{c}:\\!\textit{x}\\}},{\widehat{\sigma}},\sigma^{\prime}}_{\theta}\subseteq
S\subseteq
S^{{{\tau}\\{\mathit{c}:\\!\textit{x}\\}},\sigma^{\prime}}_{\theta}$. Then we
get $S^{\tau,\sigma,\sigma^{\prime}}_{\theta}\subseteq\bigcup_{i\in
1..n}S_{i}\cup S\subseteq S^{\tau,\sigma^{\prime}}_{\theta}$. Since
$({{\textit{x}},{{\sigma^{\prime}}\\{\textit{x}:\\!{\mathrm{v}}\\}}}){\approx}({{{\mathrm{v}}^{\prime}},{\sigma^{\prime\prime}}})$,
by Corollary 6.15, there is
$\theta^{\prime}\in\textsf{Sol}(\sigma^{\prime\prime})$ such that
${\mathrm{v}}^{\prime}\,\theta^{\prime}=\theta(\textit{x})$ and, for all
$\textit{x}\in\mathit{dom}(\sigma^{\prime})$,
$\theta(\textit{x})=\theta^{\prime}(\textit{x})$. Therefore, by induction
hypothesis, we get
$\textit{e}[{\mathrm{v}}_{0}/\texttt{this}][\overline{{\mathrm{v}}}/\overline{\textit{x}}]\,\theta^{\prime},\rho^{{\tau}\\{\mathit{c}:\\!\textit{x}^{{\textsf{ck}}}\\}}_{\theta^{\prime}},S^{{\tau}\\{\mathit{c}:\\!\textit{x}^{{\textsf{ck}}}\\}}_{\theta^{\prime}}\\!\Downarrow_{\textsc{IN}}\\!{\mathrm{v}}^{\prime}\,\theta^{\prime},S^{\prime}$,
with
$S^{{\tau}\\{\mathit{c}:\\!\textit{x}^{{\textsf{ck}}}\\},\sigma^{\prime},\sigma^{\prime\prime}}_{\theta}\subseteq
S^{\prime}\subseteq
S^{{\tau}\\{\mathit{c}:\\!\textit{x}^{{\textsf{ck}}}\\},\sigma^{\prime\prime}}_{\theta}$.
Then, by construction of $\theta^{\prime}$, we have
$\textit{e}[{\mathrm{v}}_{0}/\texttt{this}][\overline{{\mathrm{v}}}/\overline{\textit{x}}]\,\theta^{\prime}=\textit{e}[{\mathrm{v}}_{0}/\texttt{this}][\overline{{\mathrm{v}}}/\overline{\textit{x}}]\,\theta$
and
$\rho^{{\tau}\\{\mathit{c}:\\!\textit{x}^{{\textsf{ck}}}\\}}_{\theta^{\prime}}={\rho^{\tau}_{\theta}}\\{\mathit{c}\,\theta:\\!\theta(\textit{x})\\}$
and
$S^{{\tau}\\{\mathit{c}:\\!\textit{x}^{{\textsf{ck}}}\\}}_{\theta^{\prime}}=S^{\tau}_{\theta}$.
Finally, since $\textit{x}\in\mathit{dom}(\sigma^{\prime})$, $\mathit{c}\in
S^{{{\tau}\\{\mathit{c}:\\!\textit{x}\\}},\sigma^{\prime}}$, but
$\mathit{c}\notin
S^{{{\tau}\\{\mathit{c}:\\!\textit{x}\\}},{\widehat{\sigma}}}$, since x is
fresh, hence $\mathit{c}\,\theta\in
S^{{{\tau}\\{\mathit{c}:\\!\textit{x}\\}},{\widehat{\sigma}},\sigma^{\prime}}_{\theta}\subseteq
S$, thus the thesis follows by rule (IN-invk-check).

(corec)

Since $\sigma^{\prime}_{i}\leq{\widehat{\sigma}}\leq\sigma^{\prime}$, by Lemma
6.12, we get $\theta\in\textsf{Sol}(\sigma^{\prime}_{i})$, for all $i\in
1..n$. By induction hypothesis, we have
$\textit{e}_{i}\,\theta,\rho^{\tau}_{\theta},S^{\tau}_{\theta}\\!\Downarrow_{\textsc{IN}}\\!{\mathrm{v}}_{i}\,\theta,S_{i}$,
with $S^{\tau,\sigma,\sigma^{\prime}_{i}}_{\theta}\subseteq S_{i}\subseteq
S^{\tau,\sigma^{\prime}_{i}}_{\theta}$, for all $i\in 1..n$, and
$\textit{e}^{\prime}[{\mathrm{v}}_{0}/\texttt{this}][\overline{{\mathrm{v}}}/\overline{\textit{x}}][{\textit{x}}{\texttt{any}}/\theta]\,,\rho^{\tau}_{\theta},S^{\tau}_{\theta}\\!\Downarrow_{\textsc{IN}}\\!{\mathrm{v}}\,\theta,S$,
with
$S^{\tau,{{\widehat{\sigma}}}\\{\textit{x}:\\!\textit{x}\\},\sigma^{\prime}}_{\theta}\subseteq
S\subseteq S^{\tau,\sigma^{\prime}}_{\theta}$. Then we get
$S^{\tau,\sigma,\sigma^{\prime}}_{\theta}\subseteq\bigcup_{i\in 1..n}S_{i}\cup
S\cup\\{\mathit{c}\,\theta\\}\subseteq S^{\tau,\sigma^{\prime}}_{\theta}$,
since $\textit{x}\in\mathit{dom}(\sigma^{\prime})$, hence $\mathit{c}\in
S^{\tau,\sigma^{\prime}}$. In order to conclude by rule (IN-corec), we have to
prove $\mathit{c}\,\theta\in S^{\tau}_{\theta}$. We know that
$({{\mathit{c}},{{\widehat{\sigma}}}}){\approx}({{\mathit{c}^{\prime}},{{\widehat{\sigma}}}})$
for some $\mathit{c}^{\prime}\in{\mathit{dom}(\tau^{\neg\textsf{ck}})}$,
hence, by Corollary 6.15, we have
$\mathit{c}\,\theta=\mathit{c}^{\prime}\,\theta$, since
$\theta\in\textsf{Sol}({\widehat{\sigma}})$. Therefore, $\mathit{c}\,\theta\in
S^{\tau}_{\theta}$, by definition.

(look-up)

Since $\sigma^{\prime}_{i}\leq{\widehat{\sigma}}$, by Lemma 6.12, we get
$\theta\in\textsf{Sol}(\sigma^{\prime}_{i})$, for all $i\in 1..n$. By
induction hypothesis, we have
$\textit{e}_{i}\,\theta,\rho^{\tau}_{\theta},S^{\tau}_{\theta}\\!\Downarrow_{\textsc{IN}}\\!{\mathrm{v}}_{i}\,\theta,S_{i}$,
with $S^{\tau,\sigma,\sigma^{\prime}_{i}}_{\theta}\subseteq S_{i}\subseteq
S^{\tau,\sigma^{\prime}_{i}}_{\theta}$, for all $i\in 1..n$, and Then we get
$S^{\tau,\sigma,{\widehat{\sigma}}}_{\theta}\subseteq\bigcup_{i\in
1..n}S_{i}\subseteq S^{\tau,{\widehat{\sigma}}}_{\theta}$. In order to
conclude by rule (IN-look-up), we have to prove that
$\rho^{\tau}_{\theta}(\mathit{c}\,\theta)=\theta(\textit{x})$. We know that
there exists $\mathit{c}^{\prime}\in{\mathit{dom}(\tau^{\textsf{ck}})}$ such
that
$({{\mathit{c}},{{\widehat{\sigma}}}}){\approx}({{\mathit{c}^{\prime}},{{\widehat{\sigma}}}})$
and $\tau(\mathit{c}^{\prime})=\textit{x}$, hence
$\rho^{\tau}_{\theta}(\mathit{c}\,\theta)=\theta(\textit{x})$, by definition.