######  Proposition C.3 ([15]).

The pullback of a fibration for logical relations along a finite product
preserving functor is a fibration for logical relations.

In particular, the usual subscone fibration is recovered as a change of base
along the functor $\mathbb{B}(1,-):\mathbb{B}\to\mathbf{Set}$.

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

Let $p:\mathbb{\mathbb{E}}\to\mathbb{\mathbb{B}}$ be a functor. Given
$X,Y\in\mathbb{E}$, and $f:pX\to pY$, we write
$f:X\stackrel{{\scriptstyle\cdot}}{{\to}}Y$ to denote the following
proposition: $\exists\stackrel{{\scriptstyle\cdot}}{{f}}:X\to
Y.p(\stackrel{{\scriptstyle\cdot}}{{f}})=f$. We say that $f$ has a lift (in
$\mathbb{E}$).

The setting of Katsumata [15] works for fairly general languages with effects.
One way to describe them is in terms of algebraic operations, or equivalently
in terms of generic effects.

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

Let $\mathbf{C}$ be a category and $T$ a strong monad on it. Given objects
$C,D$ f $\mathbf{C}$, a $(D,C)$ algebraic operation or generic effect for is a
morphism $C\to TD$.

A lambda-calculus with effect is parametrized by a set of base types and
(effectful) primitives, each having an arity and coarity, describing the
number and types of arguments and return values. This is encapsulated as a
signature:

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

A $\lambda_{c}$-signature $\Sigma$ is a tuple $(B,K,O,ar,car:K\bigcup O\to
GType(B))$ where $B$ is a set of base types, $K$ a set of effect-free
constants, $O$ a set of algebraic operations, and $GType(B)$ the set of ground
types on $B$. $ar,car$ are the arity and co-arity functions.

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

Let $\Sigma$ be a signature. A $\lambda_{c}(\Sigma)$-structure is a tuple
$A=(\mathbb{B},T,A,a)$ where $\mathbb{B}$ is a bi-CCC, $T$ a strong monad on
$\mathbb{B}$, $A$ a functor $B\to\mathbb{B}$.

In other words, a $\lambda_{c}(\Sigma)$-structure gives an interpretation of
the base types and primitives of the language. Note that we can always extend
$A$ to a structure preserving functor
$A\llbracket-\rrbracket:Gtype(B)\to\mathbb{B}$.

We now recall the main theorems from [15]:

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

A property over a $\lambda_{c}(\Sigma)$-structure $A$ is a pair $(V,C)$ of
functors $V,C:B\to\mathbb{E}$ such that $p\circ V=A$ and $p\circ C=T\circ A$

That is, a property is the choice for any base type $b\in B$ of a predicate
$Vb$ in the category of predicates $\mathbb{E}$ over values of type $b$, and
of a predicate $Cb$ over computations $T(Ab)$ of type $b$. The question of
interest is then whether all programs preserve the property, which is answered
with the following theorem.

######  Theorem C.4 (Logical relations, [15]).

Let $\Sigma$ be a signature, $A=(\mathbb{B},T,A,a)$ be an
$\lambda_{c}(\Sigma)$-structure, $p:\mathbb{\mathbb{E}}\to\mathbb{\mathbb{B}}$
be a fibration for logical relations and $(V,C)$ be a property over $A$. If
the property satisfies the following conditions

  * •

for all $b\in B$,
$\mathbf{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}{return}}$
has a lift

  * •

for all $k\in K$, $A\llbracket k\rrbracket$ has a lift

  * •

for all $o\in O$, $\llbracket o\rrbracket$ has a lift

then for all well-typed terms $x_{1}:b_{1},\ldots,x_{n}:b_{n}\vdash t:b$,
$A\llbracket t\rrbracket$ lifts to the total category.

####  C-A3 Fibrations for logical relations for effectful languages with
recursion

So far, we have reviewed the way to use fibrations for logical relations for
higher-order effectful languages, but not for languages with recursion. We
review this next.

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

An $\omega$cpo-enriched bi-CCC is a bi-CCC $\mathbf{C}$ such that each homset
is an $\omega$cpo, and the composition, tupling $(-,-)$, cotupling $[-,-]$ and
currying $\lambda(-)$ of the bi-CC structure on $\mathbf{C}$ are all monotone
and continuous.

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

A pseudo-lifting monad on an $\omega$cpo-enriched bi-CC category $\mathbb{B}$
is a monad on the underlying non-enriched category such that it has an
algebraic operation $bt$ such that its component at $I$, $bt_{I}:1\to TI$, is
the least morphism.

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

An $\omega$cpo-enriched $\lambda_{c}(\Sigma)$-structure is a tuple
$(\mathbb{B},T,A,a)$ such that $\mathbb{B}$ is an $\omega$cpo-enriched bi-CCC,
T is a pseudo-lifting monad over $\mathbb{B}$ and $(\mathbb{B},T,A,a)$ is a
$\lambda_{c}(\Sigma)$-structure.

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

We call $X\in\mathbb{E}$ above $TI\in\mathbb{B}$ admissible if

  * •

$\bot_{pX}:1\stackrel{{\scriptstyle\cdot}}{{\to}}X$

  * •

for all $Y\in\mathbb{E}$ and $\omega$-chain $f_{i}\in\mathbb{B}(pY,pX)$ such
that $f_{i}:Y\stackrel{{\scriptstyle\cdot}}{{\to}}X$, we have
$\bigsqcup_{i=0}^{\infty}f_{i}:Y\stackrel{{\scriptstyle\cdot}}{{\to}}X$.

######  Theorem C.5 (Logical relations for language with recursion, [15]).

Let $\Sigma$ be a signature, $A=(\mathbb{B},T,A,a)$ an $\omega$cpo-enriched
$\lambda_{c}(\Sigma)$-structure, $p:\mathbb{\mathbb{E}}\to\mathbb{\mathbb{B}}$
a fibration for logical relations and $(V,C)$ be a property over $A$. If the
property satisfies

  * •

the conditions of Theorem C.4

  * •

for all $b\in\mathbb{B},Cb$ is admissible

Then for all well-typed terms of the language with iteration,
$x_{1}:b_{1},\ldots,x_{n}:b_{n}\vdash t:b$ we have $A\llbracket
t\rrbracket:\prod_{i}Vb_{i}\stackrel{{\scriptstyle\cdot}}{{\to}}Cb$.

###  C-B Correctness of AD

We will show correctness of AD (Theorem III.3) via the theory of fibrations
for logical relations. The goal is to construct a category of predicates on
$\omega\text{PAP}{}$ and to encode correctness of AD as a predicate
preservation property. To construct such a fibrations for logical relations,
we obtain one by pulling back another one along a product preserving functor.
There are several possibilities that give us different sort of predicates on
$\omega$PAP spaces. One constraint is that we need to be able to interpret our
choice of logical predicate for AD as such a predicate, and make sure all of
our constants are predicate preserving. This is in particular non-trivial when
dealing with constants involving coproducts, such as
$<:\mathbf{real}\times\mathbf{real}\to\mathbb{B}$ as the booleans are
interpreted as the coproduct $1+1$. Lastly, we need to make sure that our
choice of predicate for base types is closed under lubs of $\omega$-chains.

We organize this section as follows. First, we construct a suitable category
of predicates on $\omega\text{PAP}{}\times\omega\text{PAP}{}$ (i.e. a
fibration for logical relations). Second, we construct a property (Definition
C.11) on this category of predicates. Note that the fact that derivatives are
not unique any more is what will make this logical relation more complex.
Lastly, we will show the correctness of AD by combining these elements and
Theorem C.5.

####  C-B1 A fibration for logical relations on
$\omega\text{PAP}{}\times\omega\text{PAP}{}$

######  Definition C.16.

We define the category $\mathbf{Inj}$, a subcategory of $cPAP{}$, whose
objects are c-analytic sets and morphisms are PAP injections.

######  Lemma C.6.

$\mathbf{Inj}$ is a site, with coverage $\mathcal{J}$ where coverings are
given as in cPAP.

###### Proof.

The proof for the case of cPAP carries through to this restricted setting. ∎

######  Definition C.17.

We define $\mathbf{Sh(Inj)}$ to be the category of sheaves on the site
$\mathbf{Inj}$.

######  Lemma C.7.

$\mathbf{Sh(Inj)}$ is a Grothendieck topos, and in particular it is Cartesian-
closed, complete and co-complete.

###### Proof.

This is standard sheaf theory, see e.g. MacLane and Moerdijk [41]. ∎

By a subsheaf $P$ of $F$, we mean a sheaf $F$ such that for all c-analytic set
$A$, $P(A)\subseteq F(A)$, and $P(f)$ is the restriction of $F(f)$ for all
morphisms $f$.

######  Definition C.18.

We denote by $\mathbf{Sub(Sh(Inj))}$ the category whose objects are pairs of
sheaves $(P,F)$ of $\mathbf{Sh(Inj)}$, where $P$ is a subsheaf of $F$, and
morphisms $(P,F)\to(P^{\prime},F^{\prime})$ are natural transformations $F\to
F^{\prime}$ that restrict to the subsheaves.

######  Lemma C.8.

The second projection $(P,F)\mapsto F$ is a fibrations for logical relations
$p:\mathbf{Sub(Sh(Inj))}\to\mathbf{Sh(Inj)}$.

###### Proof.

As $\mathbf{Sh(Inj)}$ has pullbacks, it is a fibration. It is clearly
faithful. By the theory of glueing ([42, 43, 44, 39]), as
$\mathbf{Sub(Sh(Inj))}$ is a CCC and has an epi-mono factorisation system,
$\mathbf{Sub(Sh(Inj))}$ is a CCC, has finite colimits, and $p$ preserves the
CCC-structure. In addition, each fibre category is a partial order and has
small products. It remains to show that $cod$ is an opfibration and that $p$
preserves coproducts. By Lemma 4.6 in Kammar and McDermott [45], it suffices
to show that monos are closed under coproducts, as we already have the other
conditions for having a factorization system for logical relations. The arrow
category on $\mathbf{Sh(Inj)}$ is cocomplete, as $\mathbf{Sh(Inj)}$ is (it is
a topos). As $\mathbf{Sh(Inj)}$ is a topos, it has a epi-mono factorization
system, and therefore it has image factorization. Therefore, the category of
monos is a reflective subcategory of the arrow category. As such, it is
cocomplete, and in particular it has coproducts. So monos are closed under
coproducts, and we conclude by Lemma 4.6 in Kammar and McDermott [45], as said
above. ∎

We now define the functor
$F:\omega\text{PAP}{}\times\omega\text{PAP}{}\to\mathbf{Sub(Sh(Inj))}$ given
by $F(X,Y)=X\times\prod_{i\in\mathbb{N}}Y$, where
$X\times\prod_{i\in\mathbb{N}}Y$ forgets that it is an $\omega$-concrete sheaf
on the site $cPAP{}$, and only remembers that it is in particular a sheaf on
the site $\mathbf{Inj}$. It is a product preserving functor, and therefore, by
Proposition C.3, the pullback of
$p:\mathbf{Sub(Sh(Inj))}\to\mathbf{Sub(Sh(Inj))}$ along $F$ is a fibration for
logical relations. We denote this pullback by
$\pi:\mathbf{Gl}:\to\omega\text{PAP}{}\times\omega\text{PAP}{}$.

######  Remark C.1.

Before moving on, let us say a few words on this category of predicates
$\mathbf{Gl}$. One reason why we defined the category of sheaves
$\mathbf{Sub(Sh(Inj))}$ is that the property we will define for the
correctness of AD will _not_ be a concrete subsheaf, and this excludes
directly using subobjects on $\omega\text{PAP}{}$ as the fibration for logical
relations of interest. Secondly, the base type $\mathbb{B}$ is interpreted as
a coproduct, and if we simply choose the category of presheaves on
$\mathbf{Inj}$, primitives like $>$ will not lift, for a similar reason to the
one presented in Vákár [4]. We could have chosen sheaves on $cPAP{}$ instead.
This would not change much, but this is a bit overkill for our purpose and
simply adds some unnecessary complexity. Thirdly, we do seem to need to have
the property indexed by all c-analytic sets $A$. One reason is that the fact
that we have partial functions forces the definition of a lift for
$\mathbf{L}\mathbb{R}$, as well as for $\mathbb{R}$. A second reason is that
the non-uniqueness of intentional derivatives creates a technical
complication: being a correct intentional derivative at a point is essentially
non-informative, so we cannot use the same trick as we did in the smooth case.
That is, the problem is that the input space $\mathbb{R}$ is smaller than
$\mathbb{R}^{n}$, and the quantification only shows that $h$ is ‘correct’ on a
set of at most the size of $\mathbb{R}$ inside $\mathbb{R}^{n}$, which is
Lebesgue-negligible. This problem disappears when we can show that $h$ is
correct on each open of an open cover of its domain.

####  C-B2 A property for the correctness of AD

######  Definition C.19.

Let $f:A\subseteq\mathbb{R}^{n}\to\mathbb{R}$ a PAP function. Given any
intentional derivative $g:A\to\mathbb{R}^{n}$ of $f$, we call $\pi_{i}\circ
g:A\to\mathbb{R}$ an $i$-th partial intentional derivative of $f$.

We write $hot_{i}$ for the vector in $\mathbb{R}^{n}$ that consist only of
zeros, except it has a single 1 at the $i$-th position. Given any dual-number
intentional representation $g:A\times\mathbb{R}^{n}\to\mathbb{R}^{2}$ of $f$,
define the PAP function $g_{i}:A\to\mathbb{R}^{2}$ given by

$g_{i}(x)=g(x,hot_{i})$

$g_{i}$ is called an $i$-th partial dual-number intentional representation of
$f$, and its second component is an $i$-th partial intentional derivative of
$f$. We write $\partial^{i}_{DNR}f$ for the set of $i$-th partial dual-number
intentional representations of $f$.

We extend the definition of $\partial^{i}_{DNR}f$ to all natural numbers $i$
by setting $\partial^{i}_{DNR}f=\\{\lambda x.0\\}$ for any $i>n$.

######  Definition C.20.

Let
$V(\mathbb{R}):=(\mathbb{R},\prod_{i\in\mathbb{N}}\mathbb{R}\times\mathbb{R},V_{\mathbb{R}})$
where for each c-analytic set $A$, we have

$\displaystyle V_{\mathbb{R}}(A)$
$\displaystyle=\\{(f:A\to\mathbb{R},(g_{i}:A\to\mathbb{R}^{2})_{i\in\mathbb{N}})~{}\mid$
$\displaystyle\qquad~{}f,g\text{ PAP, and }g_{i}\in\partial^{i}_{DNR}f\\}$

Likewise, let
$C(\mathbb{R}):=(\mathbf{L}\mathbb{R},\mathbf{L}(\prod_{i\in\mathbb{N}}\mathbb{R}\times\mathbb{R}),C_{\mathbb{R}})$
where for each c-analytic set $A$, we have

$\displaystyle C_{\mathbb{R}}(A)$
$\displaystyle=\\{(f:A\to\mathbf{L}\mathbb{R},g:A\to\mathbf{L}(\prod_{i\in\mathbb{N}}\mathbb{R}\times\mathbb{R}))~{}\mid~{}$
$\displaystyle\qquad Dom(f)=Dom(g)\text{ and}$ $\displaystyle\qquad\forall
i.(\widetilde{f},\widetilde{L\pi_{i}\circ g})\in V_{\mathbb{R}}(Dom(f))\\}$

Let
$V(\mathbb{B})=(\mathbb{B},\prod_{i\in\mathbb{N}}\mathbb{B},V_{\mathbb{B}})$
where for each c-analytic set $A$, we have

$V_{\mathbb{B}}(A)=\\{f:A\to\mathbb{B},g:A\to\prod_{i\in\mathbb{N}}\mathbb{B}~{}\mid~{}\forall
i,\pi_{i}\circ g=f\\}$

Let
$C(\mathbb{B})=(\mathbf{L}\mathbb{B},\mathbf{L}(\prod_{i\in\mathbb{N}}\mathbb{B}),C_{\mathbb{B}})$
where for each c-analytic set $A$, we have

$\displaystyle C_{\mathbb{B}}(A)$
$\displaystyle=\\{(f:A\to\mathbf{L}\mathbb{B},g:A\to\mathbf{L}(\prod_{i\in\mathbb{N}}\mathbb{B}))~{}\mid~{}$
$\displaystyle\qquad Dom(f)=Dom(g)\text{ and}$ $\displaystyle\qquad\forall
i.(\widetilde{f},\widetilde{L\pi_{i}\circ g})\in V_{\mathbb{B}}(Dom(f))\\}$

######  Lemma C.9.

We have defined a property for our language.

###### Proof.

The only thing to show is that
$V_{\mathbb{R}},C_{\mathbb{R}},V_{\mathbb{B}},C_{\mathbb{B}}$ are subsheaves
of
$\mathbb{R}\times\prod_{i\in\mathbb{N}}\mathbb{R}^{2},\mathbf{L}\mathbb{R}\times\mathbf{L}\prod_{i\in\mathbb{N}}\mathbb{R}^{2},\mathbb{B}\times\prod_{i\in\mathbb{N}}\mathbb{B},\mathbf{L}\mathbb{B}\times\mathbf{L}\prod_{i\in\mathbb{N}}\mathbb{B}$
respectively. It is immediate for the $C$’s once we have shown the result for
the $V$’s. For $V_{\mathbb{R}}$, it amounts to showing two things. First,
whether partial intentional derivatives restrict to a subset of the domain of
a function, which is evidently true. Second, whether partial intentional
derivatives glue if they agree on their intersection, which as for usual
derivatives, is true as well. For $V_{\mathbb{B}}$, it is immediate as it is
an equalizer of $\mathbb{B}\times\prod_{i\in\mathbb{N}}\mathbb{B}$, which
exists in any topos and the canonical map
$V_{\mathbb{B}}\rightarrowtail\mathbb{B}\times\prod_{i\in\mathbb{N}}\mathbb{B}$
is a mono. ∎

Let us now look a bit more into what morphisms preserving the property look
like.

######  Definition C.21.

Let
$V(\mathbb{R}^{k}):=(\mathbb{R}^{k},(\prod_{i\in\mathbb{N}}\mathbb{R}\times\mathbb{R})^{k},V_{\mathbb{R}^{k}})$
where for each c-analytic set $A$, we have

$\displaystyle V_{\mathbb{R}^{k}}(A)$
$\displaystyle=\\{(f:A\to\mathbb{R}^{k},g:A\to(\prod_{i\in\mathbb{N}}\mathbb{R}\times\mathbb{R})^{k})~{}\mid$
$\displaystyle\qquad~{}\forall 1\leq j\leq k,(\pi_{j}f,\pi_{j}g)\in
V_{\mathbb{R}}(A)\\}$

Let $f:\mathbb{R}^{n}\to\mathbf{L}\mathbb{R}$ represent a PAP function. We
define $V(f)$ to be pairs of functions $(f,h)$, where
$h:(\prod_{i\in\mathbb{N}}\mathbb{R}\times\mathbb{R})^{k}\to\mathbf{L}(\prod_{i\in\mathbb{N}}\mathbb{R}\times\mathbb{R})$
is $\omega\text{PAP}{}$, and such that for any c-analytic set $A$, and any
$(g_{1},g_{2})\in V_{\mathbb{R}^{k}}(A)$, $(f\circ g_{1},h\circ g_{2})\in
C_{\mathbb{R}}(A)$.

This means that given a PAP functions $g_{1},\ldots,g_{n}:A\to\mathbb{R}$, $h$
will send $i$-th partial intentional representations of each of the $g_{i}$ to
$i$-th partial intentional representations of $f\circ\langle
g_{1},\ldots,g_{n}\rangle$. Note that if $A\subseteq\mathbb{R}^{k}$, this will
be trivially satisfied for any $i>k$.

Let us now see how we will interpret and a lift primitive
$t:\mathbf{real}^{2}\to\mathbf{real}$ of our language. This interpretation
will only be required for the correctness proof. We set $\llbracket
t\rrbracket_{\omega\text{PAP}{}\times\omega\text{PAP}{}}=(\llbracket
t\rrbracket,\prod_{i\in\mathbb{N}}\llbracket\mathcal{D}(t)\rrbracket)$. In
other words, we make countably many copies of the semantics of the AD-
translation of $t$. We can now more generally show that every primitive of the
language, whose semantics is interpreted in
$\omega\text{PAP}{}\times\omega\text{PAP}{}$ following the example above, will
lift to $\mathbf{Gl}$.

######  Lemma C.10.

Every primitive of the language has a lift in $\mathbf{Gl}$.

Finally, to satisfy the conditions of Theorem C.5, we need to show that for
each base $B$, $C(B)$ is admissible.

######  Lemma C.11.

$C(\mathbb{B})$ and $C(\mathbb{R})$ are admissible.

####  C-B3 Correctness of AD

######  Lemma C.12.

$\omega$PAP is an $\omega$cpo-enriched bi-CCC.

###### Proof.

Each homset is an $\omega$cpo by forgetting the PAP-structure. For composition
and coproducts, it is immediate as lubs are taken point-wise. For products, if
$f=\bigvee_{i}f_{i}$ and $g=\bigvee_{i}g_{i}$, then
$(f,g)=(\bigvee_{i}f_{i},\bigvee_{i}g_{i})=\bigvee_{i}(f_{i},g_{i})$. Finally,
if $f_{i}:X\times Y\to Z$, for currying we have $(\bigvee f_{i})(x,y)=\bigvee
f_{i}(x,y)=\bigvee\lambda(f_{i})(x)(y)$. As lubs are taken pointwise, we have
$\bigvee\lambda(f_{i})(x)(y)=(\bigvee\lambda(f_{i})(x))(y)$. This means that
$\lambda(\bigvee f_{i})=\bigvee\lambda(f_{i})$. The monotonicity part is
similar.

In summary, it follows from the fact that the forgetful functor
$\omega\text{PAP}{}\to\mathbf{\omega CPO}{}$ preserves and reflects limits,
coproducts, exponentials, and the $\omega$cpo-structure. ∎

######  Lemma C.13.

Let $f:A\subseteq\mathbb{R}^{n}\to\mathbb{R}$ be PAP. Then
$h:A\times\mathbb{R}^{n}\to\mathbb{R}^{2}$ is a dual-number representation of
$f$ iff for all natural number $i$, $h(x,hot_{i})$ is an $i$-th partial dual
number representation of $f$.

######  Theorem C.14.

For any $x_{1}:\mathbf{real},\ldots,x_{n}:\mathbf{real}\vdash
t:\mathbf{real}$, $\llbracket
t\rrbracket_{\omega\text{PAP}{}\times\omega\text{PAP}{}}$ has a lift.

###### Proof.

We have done all the work in the previous subsections. We simply check the
condition to apply Theorem C.5.

First, note that we indeed have a semantics in
$\omega\text{PAP}{}\times\omega\text{PAP}{}$, given by $\llbracket
t\rrbracket_{\omega\text{PAP}{}\times\omega\text{PAP}{}}:=(\llbracket
t\rrbracket,\prod_{i\in\mathbb{N}}\llbracket\mathcal{D}(t)\rrbracket)$,
extending what we have seen in Section C-B2. Then,

  * •

We have defined a fibrations for logical-relations
$\pi:\mathbf{Gl}\to\omega\text{PAP}{}\times\omega\text{PAP}{}$ in Section
C-B1.

  * •

We have defined a property $(V,C)$ in $\mathbf{Gl}$ in Section C-B2.

  * •

We check that
$x\mapsto\mathbf{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}{return}}(x)$
lifts, but this is immediate.

  * •

Each primitive has a lift, by Lemma C.10.

  * •

$\omega$PAP is an $\omega$cpo-enriched bi-CCC by Lemma C.12.

  * •

$\mathbf{L}$ is a pseudo-lifting monad. It means that we have an algebraic
element $\bot_{A}:1\to\mathbf{L}A$ that is interpreted in $\mathbf{L}A$ as the
bottom element. This is true by construction.

  * •

$C(\mathbb{R})$ and $C(\mathbb{B})$ are admissible, by Lemma C.11.

∎

######  Corollary C.14.1 (Correctness of AD (limited)).

For any term
$x_{1}\colon\mathbf{real},\dots,x_{n}\colon\mathbf{real}\vdash{t}:\mathbf{real}$,
the PAP function
$\llbracket\mathcal{D}({t})\rrbracket:A\times\mathbb{R}^{n}\to\mathbb{R}\times\mathbb{R}$
is a dual-number intentional representation of
$\llbracket{t}\rrbracket:A\subseteq\mathbb{R}^{n}\to\mathbb{R}$.

###### Proof.

Let
$x_{1}\colon\mathbf{real},\dots,x_{n}\colon\mathbf{real}\vdash{t}:\mathbf{real}$.
By Theorem C.14, $\llbracket
t\rrbracket_{\omega\text{PAP}{}\times\omega\text{PAP}{}}$ has a lift. Consider
the c-analytic set $\mathbb{R}^{n}$ and the pair

$(id_{\mathbb{R}^{n}},\lambda x.\prod_{i\leq k\leq
n}\prod_{i\in\mathbb{N}}(\pi_{k}(x),[i=k]\pi_{i}^{\prime}(x)))$

where, by convention, $\pi_{i}(x)=\pi_{i}^{\prime}(x)=0$ whenever $i>n$. We
use Iverson brackets, $[i=k]$, which equals to $1$ when the condition is
satisfied, and $0$ otherwise. This pair is an element of
$V_{\mathbb{R}^{k}}(\mathbb{R}^{n})$. This means that

$\displaystyle\Big{(}\llbracket t\rrbracket,\prod_{i\leq k\leq
n}\prod_{i\in\mathbb{N}}\llbracket\mathcal{D}(t)\rrbracket\circ\big{(}\lambda
x.\prod_{1\leq k\leq n}(\pi_{k}(x),$
$\displaystyle\qquad\qquad[i=k]\pi_{i}^{\prime}(x))\big{)}\Big{)}\in
C_{\mathbb{R}}(\mathbb{R}^{n})$

xw This simplifies a bit more, and by the definition of
$C_{\mathbb{R}}(\mathbb{R}^{n})$, this means that for all $i$,
$\llbracket\mathcal{D}(t)\rrbracket(x,hot_{i})$ is an $i$-th intentional
partial representation of $\llbracket t\rrbracket$. By Lemma C.13, this means
that $\llbracket\mathcal{D}(t)\rrbracket$ is a dual-number intentional
representation for $\llbracket t\rrbracket$, as desired. ∎

With the same proof, Theorem C.14 gives us directly the stronger result at all
ground types:

######  Corollary C.14.2 (Correctness of AD (full)).

For any term well-typed term $\Gamma\vdash{t}:{\tau}$ of ground type ${\tau}$
in a ground context $\Gamma$, the PAP function
$\llbracket\mathcal{D}({t})\rrbracket:A\times\mathbb{R}^{n}\to\mathbb{R}\times\mathbb{R}$
is a dual-number intentional representation of
$\llbracket{t}\rrbracket:A\subseteq\mathbb{R}^{n}\to\mathbb{R}$.

##  Appendix D Failure and convergence of Gradient Descent

###  D-A Failure of gradient descent for PAP functions

###### Proof.

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

⬇

# Recursive helper

def g(x, n):

if x > 0:

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

if x == 0:

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

else:

return g(x+1, n+1)

\pardef P(x) = g(x,0)

This can easily be written in our language with recursion and conditionals,
but it would slightly impact readability.

$\llbracket P\rrbracket$ is PAP, and by inspection, we see that $\llbracket
P\rrbracket=x\mapsto\frac{x^{2}}{2\epsilon}$. This is proved by simple
induction on $\mathbb{N}$ in inner the recursive function $g$ defining $P$.
Let’s now show that $f:=\llbracket P\rrbracket$ satisfies the hypothesis of
Theorem III.4 and is strictly convex:

  * •

$f$ is strictly convex: this is well-known for the $x^{2}$ function

  * •

$f$ is bounded below: $f\geq 0$

  * •

$f$ is $L$-smooth for some $L$:

$\displaystyle\nabla f(x)-\nabla
f(y)=\frac{2x}{2\epsilon}-\frac{2y}{2\epsilon}=\frac{1}{\epsilon}(x-y)$

And therefore $f$ is $\frac{1}{\epsilon}$-smooth.

This means that for all
$0<\epsilon^{\prime}<\frac{2}{\frac{1}{\epsilon}}=2\epsilon$, gradient descent
on $f$ converges to the global minimum 0. Now, let us see that this is not the
case when we use the intentional derivatives for $f$ computed by AD, in the
case $\epsilon^{\prime}:=\epsilon$.

Applying our standard AD macro to $P$, we obtain a PAP function $P^{\prime}$
that returns $\frac{x}{\epsilon}$ when $x\in\mathbb{R}_{>0}$, and
$\frac{(x+\lfloor|x|\rfloor+1)-(\lfloor|x|\rfloor+1)}{\epsilon}$ when
$x\in\mathbb{R}_{<0}-\\{-n~{}|~{}n\in\mathbb{N}\\}$, and $\frac{1}{\epsilon}$
for $x\in\\{-n~{}|~{}n\in\mathbb{N}\\}$.

Let $x^{0}\in\mathbb{R}$ be any initialization for the gradient descent
algorithm. Then, after one step of gradient descent, we obtain
$x^{1}:=x^{0}-\epsilon\times P^{\prime}(x^{0})$. If $x^{0}>0$, then
$\llbracket P^{\prime}(x^{0})\rrbracket=\frac{x^{0}}{\epsilon}$ and thus
$x^{1}=0$. When $x^{0}<0$ is not an integer, $\llbracket
P^{\prime}(x^{0}\rrbracket=\frac{x^{0}}{\epsilon}$ as thus $x^{1}=0$ as well.
Finally, when $x^{0}<0$ is an integer, $\llbracket
P^{\prime}(x^{0})\rrbracket=\frac{1}{\epsilon}$ and therefore $x^{1}=x^{0}-1$.
In any case, $x^{1}$ is a non-positive integer, and for $x^{2}$ we’ll always
have $x^{2}=x^{1}-1$. Therefore, $x^{t}\to-\infty$ as $t\to\infty$.

A similar program $P$ can be constructed when the learning rate is non-fixed.
The recursive program inside $P$’s definition simply calls $\epsilon(n)$
instead of using $\epsilon$, and the analysis will be very similar, except
that $x^{1}$ will not necessarily be an integer when $x^{0}$ is a non-positive
integer, but this happens for almost no $x^{0}$. ∎

###  D-B Almost-sure convergence of Gradient Descent

###### Proof.

Given a fixed intentional derivative $\nabla f$ of $f$, let
$F_{int}(\epsilon,x)=(\epsilon,x-\epsilon\nabla_{x}f)$. Let
$F_{true}(\epsilon,x)=(\epsilon,x-\epsilon\nabla^{*}_{x}f)$ where
$\nabla^{*}_{x}f$ is the true gradient of the differentiable function $f$. We
restrict the domain of $F_{true}$ and $F_{int}$ to
$(0,\frac{2}{L})\times\mathbb{R}^{d}$. For $\delta>0$ and $t\in\mathbb{N}$, we
define

$X_{t,\delta}^{*}:=\\{(\epsilon,x^{0})\in(0,\frac{2}{L})\times\mathbb{R}^{d}~{}\mid~{}|\nabla^{*}f(\pi_{2}F^{t}_{true}(\epsilon,x^{0}))|\leq\delta\\}$

where $g^{t}$ is the $t$-fold composition of a function $g$ with itself. As
$f$ is $L$-smooth, $\nabla^{*}f$ is locally $L$-Lipschitz and thus continuous.
Therefore, by the first conclusion of Theorem III.4, for any $\delta>0$,

$\bigcup_{t=0}^{\infty}X_{t,\delta}^{*}=(0,\frac{2}{L})\times\mathbb{R}^{d}$

We define similarly, for any $\delta>0$,

$X_{t,\delta}:=\\{(\epsilon,x^{0})\in(0,\frac{2}{L})\times\mathbb{R}^{d}~{}\mid~{}|\nabla^{*}f(\pi_{2}F^{t}_{int}(\epsilon,x^{0}))|\leq\delta\\}$

We will show by induction on $t\in\mathbb{N}$ that $X_{t,\delta}$ and
$X_{t,\delta}^{*}$ only differ by a null-set, i.e. that there exists null-sets
$N_{t,\delta}$ and $M_{t,\delta}$ such that $X_{t,\delta}\cap
N_{t,\delta}=X_{t,\delta}^{*}\cap M_{t,\delta}$. This implies that

$\displaystyle\bigcup_{t=0}^{\infty}X_{t,\delta}$
$\displaystyle\supseteq\bigcup_{t=0}^{\infty}X_{t,\delta}\cap N_{t,\delta}$
$\displaystyle=\bigcup_{t=0}^{\infty}X_{t,\delta}^{*}\cap M_{t,\delta}$
$\displaystyle\supseteq(\bigcup_{t=0}^{\infty}X_{t,\delta}^{*})\cap((0,\frac{2}{L})\times\mathbb{R}^{d}-\bigcup_{t=0}^{\infty}M_{t,\delta})$
$\displaystyle=(0,\frac{2}{L})\times\mathbb{R}^{d}\cap((0,\frac{2}{L})\times\mathbb{R}^{d}-\bigcup_{t=0}^{\infty}M_{t,\delta})$
$\displaystyle=(0,\frac{2}{L})\times\mathbb{R}^{d}-\bigcup_{t=0}^{\infty}M_{t,\delta}$

As a countable union of negligible sets is negligible, this means that
$\bigcup_{t=0}^{\infty}X_{t,\delta}$ equals
$(0,\frac{2}{L})\times\mathbb{R}^{d}$ up to a negligible set, as desired.

By induction on $t\in\mathbb{N}$, we show the following property:

$\displaystyle\forall A\subseteq(0,\frac{2}{L})\times\mathbb{R}^{d}\text{
measurable of measure }0,$
$\displaystyle\\{(\epsilon,x)~{}\mid~{}F_{true}^{t}(\epsilon,x)\in A\\}\text{
is measurable with measure }0$

If $t=0$, $F_{true}^{t}$ is the identity and it’s obvious. Let
$t\in\mathbb{N}$ such that the property holds. Let
$A\subseteq(0,\frac{2}{L})\times\mathbb{R}^{d}$ be of measure 0. To use the
induction hypothesis, it suffices to show that $F_{true}^{-1}(A)$ has measure
0. The Jacobian matrix of $F$ is an $(n+1)\times(n+1)$ matrix, given by

$J(F_{true})_{\epsilon,x}=\begin{pmatrix}1&0_{n}^{T}\\\
Jf_{x}^{T}&I_{n}-\epsilon Hf_{x}&\end{pmatrix}$

where $I_{n}$ is the $n\times n$ identity matrix, $0_{n}$ the zero vector in
$\mathbb{R}^{n}$, $Hf_{x}$ is the Hessian matrix of $f$, and $(-)^{T}$ is the
transpose operation.

The rank of $J(F_{true})_{\epsilon,x}$ is lower bounded by one plus the rank
of $I_{n}-\epsilon Hf_{x}$. The latter is strictly less than $n$ exactly when
$\frac{1}{\epsilon}$ is an eigenvalue of $Hf_{x}$. For a fixed $x$, this can
only occur for finitely many $\epsilon$ (at most $n$). Thus,
$J(F_{true})_{\epsilon,x}$ has max rank $n+1$ almost everywhere. Denote by $R$
this set. $f$ being PAP, $F$ is PAP as well. Therefore, $F$ is almost
everywhere analytic, and denote this set $C$. Let $N=R\cap C$, and let $Z$ be
its complement. Note that $Z$ is negligible. On $N$, $F$ is
$F\in\mathcal{C}^{1}$ and its Jacobian is invertible. Therefore, by the
implicit function theorem, the result is locally true around any point $x\in
N$. We can use a countable cover $\\{U_{i}\\}_{i}$ of N, and thus

$\displaystyle F_{true}^{-1}(A)$ $\displaystyle=F_{true}^{-1}(A)\cap N\cup
F^{-1}(A)\cap Z$ $\displaystyle\subseteq
F_{true}^{-1}(A)\cap(\bigcup_{i}U_{i})\cup Z$
$\displaystyle=\bigcup_{i}F_{true}^{-1}(A)\cap U_{i}\cup Z$

$F_{true}^{-1}(A)$ is obviously measurable as $A$ is, and as null-sets are
closed under countable unions, this shows that $F_{true}^{-1}(A)$ has measure
0, which concludes the induction.

Now, we show by induction on $t\in\mathbb{N}$ that for almost all
$(\epsilon,x^{0})\in(0,\frac{2}{L})\times\mathbb{R}^{d}$,

$F_{true}^{t}(\epsilon,x^{0})=F_{int}^{t}(\epsilon,x^{0})$

Once again, the base case is immediate. Let $t\in\mathbb{N}$ such that the
property holds. As $\nabla f$ is an intentional derivative of $f$, for almost
all $x\in\mathbb{R}$, we have that $\nabla_{x}f=\nabla_{x}^{*}f$. Therefore,
for almost all $(\epsilon,x)$, we have that
$F_{true}(\epsilon,x)=F_{int}(\epsilon,x)$. Let $A$ be the set of points on
which they differ. By the previous proposition, $F_{true}^{-1}(A)$ has measure
0. Therefore, $F^{t+1}_{true}$ and $F^{t+1}_{int}$ may differ only on the set
$F_{true}^{-1}(A)$, which has measure 0. This concludes the induction.

As a corollary of what we have just shown, we have that for almost all
$(\epsilon,x^{0})$, $x^{t}$ is the same, whether it was obtained from true or
AD-computed gradients. Indeed, $x^{t}$ is either
$\pi_{2}F^{t}_{true}(epsilon,x^{0})$ or $\pi_{2}F^{t}_{int}(epsilon,x^{0})$,
and we have shown that $F^{t}_{true}(epsilon,x^{0})$ and
$F^{t}_{true}(epsilon,x^{0})$ agree almost everywhere. Therefore
$f(x^{t=1})\leq f(x^{t})$ remains true almost-everywhere for all $t$, as a
countable union of negligible sets is negligible. Finally, if $f$ is strongly
convex, then $\\{x^{t}\\}_{t}$ will reach the global minimum. As $x^{t}$ is
the same, whether it was obtained from true or AD-computed gradients, for
almost all $(\epsilon,x^{0})$, this means that gradient-descent with AD-
computed gradients will also almost surely converge to the global minimum. ∎

##  Appendix E s-Hausdorff measures

###  E-A Monad of measure on $\omega$PAP

The goal of this section is to give the key steps in the proof of Theorem
IV.2. These are the following. We adapt the proof technique used in Vákár et
al. [2]. We define an expectation operator
$\mathbf{Int}_{X}:\mathbf{S}X\to(X\to\mathbb{W})\to\mathbb{W})$. We show that
it is a well-defined $\omega\text{PAP}{}$-morphism, and natural in $X$. Next,
we show that $\omega\text{PAP}{}$ admits a proper orthogonal-factorization
system, extending the known result on categories of concrete sheaves to this
category of $\omega$-concrete sheaves. Using a theorem from Kammar and
McDermott [45], we show that the image of $\mathbf{Int}$ induces a strong
monad $\mathbf{M}$ on $\omega$PAP. This monad is easily shown to be
commutative.

###  E-B Pushforward of PAP functions

In this section, we prove the following Theorem:

######  Theorem E.1.

Let $f:U\to\mathbb{R}^{n}$ be the total restriction of a partial $\omega$PAP
morphism to its domain $U\subseteq\mathbb{R}^{m}$. Let $\lambda$ be the
restriction of the Lebesgue measure to $U$. Then $f_{*}\lambda$ has a density
w.r.t. some s-Hausdorff measure $\mu$ on $\mathbb{R}^{n}$.

It is the core technical theorem that is required to prove Theorem IV.3. To
prove Theorem E.1, we will first prove a restricted form of it:

######  Theorem E.2.

Let $f:U\subseteq\mathbb{R}^{n}\to\mathbb{R}^{m}$ be real analytic on a
connected open $U$. Then there is an integer $k$ such that $f(U)$ is contained
is a countable union $M:=\bigcup_{i\in\mathbb{N}}M_{i}$ of smooth submanifolds
$M_{i}$ of $\mathbb{R}^{m}$ of dimension $k$, up to a set of $k$-Hausdorff
measure 0. Furthermore, $f_{*}\lambda$ has a density w.r.t. the $k$-Hausdorff
measure on $M$.

Before proving the theorem, we need a few other technical lemmas.

######  Lemma E.3.

Let $\mu=\sum_{0\leq k\leq
m}\sum_{i\in\mathbb{N}}f_{i}^{k}.\mu^{k}_{i}\in\mathcal{M}\mathbb{R}^{m}$ for
some non-negative measurable functions
$f_{i}^{k}:\mathbb{R}^{m}\to\mathbb{R}^{+}\cup\\{\infty\\}$, and such that
$\mu^{k}_{i}$ is the $k$-Hausdorff measure on some $k$-dimensional submanifold
$M_{i}^{k}$ of $\mathbb{R}^{m}$. Let $B$ be the s-Hausdorff measure given by
the $(\mu^{k}_{i})$. Then $\mu$ has a density w.r.t. $B$.

###### Proof.

Let $X_{k}=\bigcup_{i}M_{i}^{k}$ and $\mu_{k}$ be the $k$-Hausdorff measure on
$X_{k}$. Let $g_{k}=\sum_{i\in\mathbb{N}}1_{x\in M^{k}_{i}}.f_{i}^{k}$. As the
$f_{i}^{k}$ are non-negative and can take the value $\infty$, the limit exists
and therefore the $g_{k}$ are measurable. By construction, we have the
equality $\sum_{i\in\mathbb{N}}f_{i}^{k}.\mu^{k}_{i}=g_{k}.\mu^{k}$ for all
$0\leq k\leq m$. This follows from the simpler equality
$f_{1}.\nu|_{A}+f_{2}.\nu|_{B}=(f_{1}+f_{2}).\nu|_{A\cup B}$ which is also
valid for countable unions, given that the $\mu^{k}_{i}$ are all restrictions
of the $k$-Hausdorff measure. Therefore $\mu=\sum_{1\leq k\leq
m}g_{k}.\mu_{k}$.

Let $g=g_{0}+1_{x\not\in X_{0}}(g_{1}+1_{x\not\in X_{1}}(g_{2}+1_{x\not\in
X_{2}}(\ldots+1_{x\not\in X_{m-1}}g_{m})))$. $g$ is clearly measurable and
non-negative (with the convention that $0.\infty=0$ here). For all $i<k$,
$X_{i}$ is $H^{k}$ negligible. Thus
$g_{k}.\mu_{k}=g_{k}.\mu_{k}|_{X_{k}-X_{i}}=(1_{x\not\in
X_{i}}g_{k}).\mu_{k}$. From this fact, we deduce that $\sum_{1\leq k\leq
m}g_{k}.\mu_{k}=g.B$, and therefore conclude that $\mu=g.B$, i.e. that $\mu$
has a density w.r.t. $B$. ∎

######  Lemma E.4.

Let $f:U\subseteq\mathbb{R}^{n}\to\mathbb{R}^{m}$ be real analytic on a
connected open $U$. Let $k$ be the maximal rank of $f$ on $U$. Then
$V:=\\{x\in U~{}|~{}rank(f(x))=k\\}$ is

  * •

open,

  * •

dense in $U$,

  * •

and $\lambda(U-V)=0$.

###### Proof.

Let’s first show $V$ is open. Given a coordinate system for $U$ and $V$, for
any $x\in V$, denote by $G(x)$ the matrix for $T_{x}f$ in these bases. By
hypothesis, $G(x)$ has at least an invertible $k\times k$ sub-matrix, and this
is a characterisation of rank. Then denote by $H:M_{n\times
m}(\mathbb{R})\to\mathbb{R}:A\mapsto\sum_{B~{}k\times
k~{}submatrix~{}of~{}A}|det(B)|$. $H$ is continuous as the determinant is, and
$V=(HG)^{-1}(\mathbb{R}-\\{0\\})$ is thus open. Let’s show $V$ is dense. Note
that this is not true in general for smooth functions. Pick a base for $U$ and
$V$ again, and let $G(x)$ the matrix for $T_{x}f$ in these bases. Thus
$x\mapsto G(x)$ is also real analytic.

Let $p\in\bar{V}-V$. Pick a $k\times k$ submatrix $B$ of matrices in
$M_{n\times m}(\mathbb{R})$, then let $H_{B}:M_{n\times
m}(\mathbb{R})\to\mathbb{R}$ be the determinant of that submatrix. Assume
$H_{B}G$ is $0$ on a open neighbourhood $W_{B}$ of $p$ for all $B$. Then
$W=\cap W_{B}$ is a finite intersection of opens and thus is open, and $W\cap
V\neq\emptyset$ as by assumption $p$ is in the boundary of $V$. But that’s a
contradiction as we know that for some $B$ and any $x$ in the intersection,
$H_{B}G(x)\neq 0$. Therefore, there is a $B$ such that $H_{B}G$ is not 0 at
some point $x$ in a neighbourhood $W_{B}$ on $p$. As $f$ is analytic, so is
$df$, and so is $G$. The determinant is a polynomial function of its
arguments, it is thus real analytic, and thus so is $H_{B}$. As $H_{B}G$ is
analytic and non-identically 0 on $W_{B}$, it must be non-zero on a dense
subset of $W_{B}$. Let’s assume that the closure $\bar{V}$ is not all of $U$.
We obtain a contradiction by picking a point close to $\bar{V}$ that would end
up in one of the $W_{B}$. In more detail, assume by ways of contradiction that
$U-\bar{V}\neq\emptyset$. Let $p\in U-\bar{V}$. Let $g:U\to\mathbb{R}^{+}$ be
defined as $g(x)=d(x,\bar{V})$. By assumption, as $\bar{V}$ is closed, we have
$g(p)>0$. Also, note that $g$ is continuous. As $k$ is the maximal ranked
reached by $f$, $\bar{V}\neq\emptyset$. Thus, there exists $y\in\bar{V}$ such
that $g(y)=0$. As $U$ is connected (and thus path connected, as an open of a
Euclidean space), there is a continuous path $c:[0,1]\to U$ such that $c(0)=y$
and $c(1)=p$. The composition $g\circ c$ is continuous and so there a point
$x\in\bar{V}-V$ such that $c(t)=x$ and $g(x)=0$ for some $t_{0}<1$. By
compactness of $[0,1]$, let’s choose the biggest such $t_{0}$, which exists as
$c(1)=p\not\in\bar{V}$. For all $t>t_{0}$, we therefore have $g(c(t))>0$.
However, by the result above, there is a dense open subset $W$ of a $W_{B}$, a
neighbourhood of $x$, such that $W\subseteq V$. By density of $W$, this means
that $c(t)=0$ on $c^{-1}(W_{B})\cap[t_{0},1]\neq\emptyset$, a contradiction.

We will now prove that $X:=U-V$ has Lebesgue measure 0. For a fixed $k\times
k$ matrix $B$ of any $n\times m$ matrix, consider the same analytic function
$H_{B}$ as above. Then $g_{B}:=G;H_{B}:U\to\mathbb{R}$ is analytic. Using the
theorem from Mityagin [46], it is either the 0 function or the preimage of $0$
has Lebesgue measure 0. We can write $X=\bigcap_{B~{}k\times
k~{}submatrix}g_{B}^{-1}(\\{0\\})$. As $f$ has rank $k$ somewhere, not every
$g_{B}$ is the 0 analytic function, and thus $X$ is contained in a Lebesgue
measure 0 set, and therefore has Lebesgue measure 0. ∎

######  Lemma E.5.

Let $f:A\to C$ where $A\subseteq\mathbb{R}^{n}$ is $\lambda$-measurable, and
let $U\subseteq A$ be $\lambda$-measurable. Assume that $\lambda(A-U)=0$. Then
$f_{*}\lambda=(f|_{U})_{*}\lambda$.

###### Proof.

$\displaystyle f_{*}\lambda(S)$ $\displaystyle=\lambda(f^{-1}(S))$
$\displaystyle=\lambda(f^{-1}(S)\cap A)$
$\displaystyle=\lambda(f^{-1}(S)\cap(A-U+U))$
$\displaystyle=\lambda((f^{-1}(S)\cap(A-U))\cup(f^{-1}(S)\cap U))$
$\displaystyle\leq\lambda(f^{-1}(S)\cap(A-U))+\lambda(f^{-1}(S)\cap U)$
$\displaystyle\leq\lambda(A-U)+\lambda|_{U}(f^{-1}(S)$
$\displaystyle=0+\lambda|_{U}(f^{-1}(S))$
$\displaystyle=(f|_{U})_{*}\lambda(S)$

As the other inequality is obvious, we showed that
$f_{*}\lambda(S)=(f|_{U})_{*}\lambda(S)$. ∎

######  Lemma E.6.

Let $f:U\subseteq\mathbb{R}^{n}\to\mathbb{R}^{m}$ be real analytic on a
connected open $U$. Further, assume $f$ has constant rank. Then $f(U)$ is a
countable union of manifolds.

###### Proof.

As $f$ has constant rank, by the constant rank theorem, $f$ is locally of the
form $(x_{1},\ldots,x_{n})\mapsto(x_{1},\ldots,x_{k},0,\ldots,0)$. More
precisely, around any $x\in U$, there is a neighborhood $W$ of $x$ and smooth
diffeomorphisms $\phi,\psi$ such that $g:=\phi\circ
f|_{W}\circ\psi(x_{1},\ldots,x_{n})=(x_{1},\ldots,x_{k},0,\ldots,0)$. As $g$
is a projection, it is an open map. As $\phi,\psi$ are diffeomorphisms,
$f|_{W}$ is also an open map. This means that $f(W)$ is a $k$-dimensional
submanifold of $\mathbb{R}^{m}$ (technically it is direct if $k=m$, otherwise
we need an extra argument where we post-compose with a projection first,
obtain the result above, and then use the submersion theorem to obtain that
the $0$ level of the projection is a manifold, which is $f(W)$).

Now consider the open cover of $U$ given by $\\{W_{x}~{}|~{}x\in U\\}$ where
$W_{x}$ is a neighbourhood of $x$ as above. As opens of Euclidean spaces are
Lindelöf spaces, we can extract a countable open sub-cover of $U$. Thus,
$F(V)$ is a countable union of $k$-dimensional manifolds. ∎

###### Proof of Theorem E.2.

Let $k$ be the maximal rank of $f$ on $U$. Let $V:=\\{x\in
U~{}|~{}rank(f(x))=k\\}$. Let’s first show that it is sufficient to show the
result for $f|_{V}$.

By Lemma E.4, $V$ is open and dense in $U$, and $U-V$ has Lebesgue measure 0.
By Lemma E.5, $f_{*}\lambda=(f|_{V})_{*}\lambda$, so we reduced the second
statement to showing it for $(f|_{V})$. In addition, by Sard’s theorem,
$f(U-V)$ has $k$-Hausdorff measure 0. Therefore, it is sufficient to prove the
theorem for $f|_{V}$, which we call $f$ again.

Now, write $V=\bigsqcup_{i}V_{i}$ where the $V_{i}$ are the connected
components of $V$. On each connected component $V_{i}$, $f|_{V_{i}}$ verifies
the hypothesis of Lemma E.6. Thus $f(V_{i})$ is a countable union of
$k$-dimensional manifolds for each $V_{i}$. As Euclidean spaces are locally
connected spaces with a countable basis, the same holds for $V$. Therefore,
$V$ has at most countably many connected components $V_{i}$. A countable union
of countable sets is countable, and we finished proving the first part of the
theorem.

Finally, it remains to show that $f_{*}\lambda$ has a density w.r.t. the
$k$-Hausdorff measure on $f(V)$. By Lemma E.3, it is sufficient to show it for
each $(f|_{W})_{*}\lambda,f(W)$, where $W$ is as constructed above. First,
let’s show that it is also sufficient to restrict to the case where $W$ is
contained in a compact set. There exists a countable cover $K_{i}$ of compact
sets of $\mathbb{R}^{n}$ that cover $W$ (e.g. by taking closed spheres of
radius 1 at points with rational coordinates). Each $W_{i}:=K_{i}\cap W$ is
thus compact in $W$. Assume for now that we have proved that
$(f|_{W_{i}})_{*}\lambda$ has a density w.r.t. $f(W)$, i.e. that
$(f|_{W_{i}})_{*}\lambda(A)=\int_{A}h_{i}(x)d\mathcal{H}^{k}(x)$ for some
measurable function $h_{i}:f(W)\to\mathbb{R}^{+}\cup\\{\infty\\}$. Then,

$\displaystyle f_{*}\lambda(A)$
$\displaystyle=\sum_{i}(f|_{W_{i}})_{*}\lambda(A)$
$\displaystyle=\sum_{i}\int_{A}h_{i}(x)d\mathcal{H}^{k}(x)$
$\displaystyle=\int_{A}(\sum_{i}h_{i}(x))d\mathcal{H}^{k}(x)$

where the last equality holds by the Fubini-Tonelli theorem as $h_{i}\geq 0$.
$h:=\sum_{i}h$ is measurable, and we are done.

So we can now assume that $W$ is contained in a compact set. As $f$ is
analytic, it is locally Lipschitz and is thus Lipschitz on $W$, as $W$ is
contained in a compact set. What’s more, As $f$ has rank $k$, its Jacobian
matrix $J_{x}$ at every point $x$ has rank $k$. A standard result in linear
algebra asserts that $J_{x}J_{x}^{T}$ also has rank $k$ and therefore the
correction term $J_{W}f(x)$ is non-zero for all $x$. Let
$g(x):=\frac{1}{J_{W}f(x)}$ is therefore measurable and non-negative. By the
co-area formula, we have

$\displaystyle f_{*}\lambda(A)$ $\displaystyle=\lambda(f^{-1}(A))$
$\displaystyle=\int_{f^{-1}(A)}1.d\lambda$
$\displaystyle=\int_{f^{-1}(A)}g(x)J_{W}f(x).d\lambda$
$\displaystyle=\int_{f(W)}\Big{(}\int_{f^{-1}(y)}g(x)d\mathcal{H}^{n-k}(x)\Big{)}d\mathcal{H}^{k}(y)$
$\displaystyle=\int_{f(W)}h(y)d\mathcal{H}^{k}(y)$

where $h(y):=\int_{f^{-1}(y)}g(x)d\mathcal{H}^{n-k}(x)$ is measurable and non-
negative, yet possibly infinite.

∎

######  Lemma E.7.

Let $A$ be an analytic set. There is an open $U\subseteq A$ such that
$\lambda(A-U)=0$.

###### Proof.

Let $A=\cap_{i}X_{i}^{+}\cap\cap_{j}X_{j}^{-}$ as in the definition of
analytic sets. Write $X_{j}^{-}=X_{j}\sqcup Z_{j}$ where
$Z_{j}=(g_{j}^{-})^{-1}(\\{0\\})$. Without loss of generality, assume that
none of the $g_{j}^{-}$ are the constant 0 function. Then,
$U:=\cap_{i}X_{i}^{+}\cap\cap_{j}X_{j}$ is clearly open and $U\subseteq A$.
Let’s now show that $A-U$ has Lebesgue measure 0. It suffices to show that
this is the case for each $Z_{j}$, as they cover $A-U$. However, by Mityagin
[46]’s result, $g_{j}^{-}$ is either the 0 function or the preimage of $0$ has
Lebesgue measure 0. This shows that $Z_{j}$ have Lebesgue measure 0, as
desired. ∎

######  Theorem E.8.

Let $f:A\to\mathbb{R}^{m}$ be PAP. Then $f_{*}\lambda$ has a density w.r.t. an
s-Hausdorff measure $\mu$ on $\mathbb{R}^{m}$.

###### Proof.

Let $f:A\to\mathbb{R}^{m}$ be PAP. $A$ is c-analytic, so we can write it as
$A=\bigsqcup_{i}A_{i}$ where each $A_{i}$ is analytic and $(f_{i},A_{i})$ is a
PAP representation for $f$. By Lemma E.7, there is an open $U_{i}\subseteq
A_{i}$ such that $\lambda(A_{i}-U_{i})=0$. By Lemma E.5, it is thus sufficient
to consider the case where $f_{i}$ is defined on an open set $U_{i}$. Any open
$V\subseteq\mathbb{R}^{n}$ can always be written as $V=\bigsqcup_{i}V_{i}$ for
a countable family of connected opens $V_{i}$. Applying this to the $U_{i}$,
we have a countable family of analytic functions
$f_{i,j}:U_{i,j}\to\mathbb{R}^{m}$ defined on connected opens $U_{i,j}$, where
$f_{i,j}$ is the restriction of $f_{i}$ to $U_{i,j}$. By theorem E.2, for each
$(i,j)$, there exists an integer $0\leq k_{i,j}\leq m$ such that
$(f_{i,j})_{*}\lambda=\sum_{l\in\mathbb{N}}f_{l}^{k_{i,j}}m^{k_{i,j}}_{l}$,
where each $f_{l}^{k_{i,j}}:\mathbb{R}^{m}\to\mathbb{R}^{+}\cup\\{\infty\\}$
is measurable, and each $m^{k_{i,j}}_{l}$ is the $k_{i,j}$-Hausdorff measure
on some $k_{i,j}$-submanifold $M^{i,j}_{l}$ of $\mathbb{R}^{m}$. Therefore,

$\displaystyle f_{*}\lambda$ $\displaystyle=\sum_{i,j}(f_{i,j})_{*}\lambda$
$\displaystyle=\sum_{i,j}\sum_{l\in\mathbb{N}}f_{l}^{k_{i,j}}m^{k_{i,j}}_{l}$
$\displaystyle=\sum_{0\leq k\leq
m}\sum_{\\{(i,j)~{}|~{}k_{i,j}=k\\}}\sum_{l}f_{l}^{k_{i,j}}m^{k_{i,j}}_{l}$
$\displaystyle=\sum_{0\leq k\leq m}\sum_{n}f_{n}^{k}m^{k}_{n}$

where in the last equality we simply re-index the countable sum. We can now
conclude by Lemma E.3 that $f_{*}\lambda$ has a density w.r.t. some
s-Hausdorff measure. ∎

Finally, we prove Theorem IV.4.

###### Proof.

By a theorem of Whitney (refined by Morrey and Grauert), all (finite-
dimensional, second-countable, Hausdorff, without boundary) smooth manifolds
admit a (unique) analytic structure, and two smooth manifolds are
diffeomorphic iff they are analytic-equivalent. Our case is even simpler, as
we consider embedded submanifolds of $\mathbb{R}^{n}$. Let $M$ be a smooth
submanifold of $\mathbb{R}^{n}$. There exists a tubular envelope
$U\subseteq\mathbb{R}^{n}$ of $M$, and a smooth projection
$p:U\to\mathbb{R}^{n}$ such that $M=p(U)$. This means that $p_{*}\lambda|_{U}$
and $H^{k}$ on $M$ are mutually absolutely continuous. By reasoning in local
coordinates, using analytic charts, we see that $p$ is locally a linear
projection, and is thus analytic, and therefore PAP. Now let $\mu$ be an
arbitrary s-Hausdorff measure, and $\\{M^{k}_{i}\\}_{i,k}$ be a support for
$\mu$. Let $p_{i,k}:U_{i,k}\to\mathbb{R}^{n}$ be analytic projections such
that $p(U_{i,k})=M^{k}_{i}$. Every open set $U\subseteq\mathbb{R}^{n}$ is
diffeomorphic to a bounded open $V$ of radius at most 1, and the
diffeomorphism and its inverse can be chosen to be analytic functions. Let
$\phi_{i,k}:V_{i,k}\to U_{i,k}$ be such functions. Let $W_{i,k}$ be the same
opens as the $V_{i,k}$, but translated to be disjoint, which is always
possible as the $V_{i,k}$ have radius at most 1 and there are countably many
of them. Let $t_{i,k}:W_{i,k}\to V_{i,k}$ be the associated translations,
which are linear and therefore analytic. Let $W=\bigsqcup_{i,k}W_{i,k}$. Then
the function $f:W\to\mathbb{R}^{n}$ defined by $x\in W_{i,j}\mapsto
t_{i,k};\phi_{i,k};p_{i,k}$ is analytic, and $f_{*}\lambda$ and $\mu$ are
mutually absolutely continuous. ∎


First observe that the projection operation is a homomorphism and
$L(R_{d,d^{\prime}}))$ is a regular language; hence by virtue of $\mathcal{C}$
being a full trio $L_{d\sigma d^{\prime}}$ as defined above is in
$\mathcal{C}$. The conditions $\exists
w\in(\Sigma\cup\Sigma_{\mathsf{i}})^{*}\colon
d\overset{w}{\underset{R}{\Rightarrow}^{*}}d^{\prime}\land w\in
L_{\sigma}\land\mathbf{m}^{\prime}={\mathsf{Parikh}}_{\Sigma}(w)$ and $\exists
w\in L_{d\sigma d^{\prime}}\colon{\mathsf{Parikh}}(w)=\mathbf{m}^{\prime}$ are
seen to be equivalent from the definition of $L_{d\sigma d^{\prime}}$,
concluding the proof of the lemma.

##  Appendix B Proof of Proposition 2

We prove the following proposition.

Let $\mathfrak{P}=(D,\Sigma,(L_{c})_{c\in\mathfrak{C}},d_{0},\mathbf{m}_{0})$
be an asynchronous program. Then
$\mathord{\downarrow}{\mathsf{Runs}(\mathord{\downarrow}{\mathfrak{P}})}=\mathord{\downarrow}{\mathsf{Runs}(\mathfrak{P})}$.
In particular,

  1. (1)

For every $d\in D$, $\mathfrak{P}$ can reach $d$ if and only if
$\mathord{\downarrow}{\mathfrak{P}}$ can reach $d$.

  2. (2)

$\mathfrak{P}$ is terminating if and only if
$\mathord{\downarrow}{\mathfrak{P}}$ is terminating.

  3. (3)

$\mathfrak{P}$ is bounded if and only if $\mathord{\downarrow}{\mathfrak{P}}$
is bounded.

######  Proof B.1.

A run of the asynchronous program $\mathfrak{P}$ is defined as a sequence
$c_{0},\sigma_{1},c_{1},\sigma_{2},\ldots$ containing alternating elements of
configurations $c_{i}$ and letters $\sigma_{i}$ beginning with the
configuration $c_{0}=(d_{0},\mathbf{m}_{0})$. First we observe that

$\mathsf{Runs}(\mathfrak{P})\subseteq\mathsf{Runs}(\mathord{\downarrow}{\mathfrak{P}})$
(6)

because every transition enabled in $\mathfrak{P}$ is also enabled in
$\mathord{\downarrow}{\mathfrak{P}}$. Next, we claim:

$\forall\;\rho\in\mathsf{Runs}(\mathord{\downarrow}{\mathfrak{P}})\;\exists\;\rho^{\prime}\in\mathsf{Runs}(\mathfrak{P})\;\rho\trianglelefteq\rho^{\prime}$
(7)

Let
$\rho|_{k}=(d_{0},\mathbf{m}_{0}),\sigma_{1},(d_{1},\mathbf{m}_{1}),\sigma_{2},...,\sigma_{k},(d_{k},\mathbf{m}_{k})$
be the $2k+1-$length prefix of $\rho$. We show that for each $\rho|_{k}$ there
exists $\rho^{\prime}_{k}\in\mathsf{Runs}(\mathfrak{P})$ such that
$\rho|_{k}\trianglelefteq\rho^{\prime}_{k}$ and in addition, $\forall
k\;\forall i\leq k\;\rho^{\prime}_{k}(i)=\rho^{\prime}_{k+1}(i)$. We can then
define $\rho^{\prime}(i):=\rho^{\prime}_{i}(i)$ and clearly
$\rho\trianglelefteq\rho^{\prime}$.

We prove by induction on $k$.
Base Case: $\rho|_{0}=\rho^{\prime}|_{0}=(d_{0},\mathbf{m}_{0})$.
Induction Step: Let
$\rho|_{k}=(d_{0},\mathbf{m}_{0}),\sigma_{1},(d_{1},\mathbf{m}_{1}),\sigma_{2},...,(d_{k},\mathbf{m}_{k})\in\mathsf{Runs}(\mathord{\downarrow}{\mathfrak{P}})$.
By induction hypothesis there is
$\rho^{\prime}_{k-1}=(d_{0},\mathbf{m}_{0}),\sigma_{1},(d_{1},\mathbf{m}_{1}^{\prime}),\sigma_{2},...,(d_{k-1},\mathbf{m}_{k-1}^{\prime})\in\mathsf{Runs}(\mathfrak{P})$
such that $\rho_{k-1}\trianglelefteq\rho^{\prime}_{k-1}$.

$\displaystyle(d_{k-1},\mathbf{m}_{k-1})\overset{\sigma_{k}}{\underset{\mathord{\downarrow}{\mathfrak{P}}}{\rightarrow}}(d_{k},\mathbf{m}_{k})$
$\displaystyle\Rightarrow\exists\mathbf{m}_{k-1}^{\prime\prime}\colon\mathbf{m}_{k-1}=\mathbf{m}_{k-1}^{\prime\prime}\oplus{\llbracket\sigma_{k}\rrbracket}\land(d_{k-1},\mathbf{m}_{k-1}^{\prime\prime}\oplus{\llbracket\sigma_{k}\rrbracket})\overset{\sigma_{k}}{\underset{\mathord{\downarrow}{\mathfrak{P}}}{\rightarrow}}(d_{k},\mathbf{m}_{k})$
$\displaystyle\Rightarrow\exists w\in\Sigma^{*}\colon
w\in\mathord{\downarrow}{L_{d_{k-1}\sigma_{k}d_{k}}}\land{\mathsf{Parikh}}(w)\oplus\mathbf{m}_{k-1}^{\prime\prime}=\mathbf{m}_{k}$
$\displaystyle\Rightarrow\exists w^{\prime}\in\Sigma^{*}\colon w\sqsubseteq
w^{\prime}\land w^{\prime}\in L_{d_{k-1}\sigma_{k}d_{k}}$
$\displaystyle\Rightarrow(d_{k-1},\mathbf{m}_{k-1})\overset{\sigma_{k}}{\underset{\mathfrak{P}}{\rightarrow}}(d_{k},\mathbf{m}_{k}\oplus\mathbf{m}_{\Delta})\text{where
}\mathbf{m}_{\Delta}\oplus{\mathsf{Parikh}}(w)={\mathsf{Parikh}}(w^{\prime})$
$\displaystyle\Rightarrow(d_{k-1},\mathbf{m}_{k-1}^{\prime})\overset{\sigma_{k}}{\underset{\mathfrak{P}}{\rightarrow}}(d_{k},\mathbf{m}_{k}^{\prime})\text{
where
}\mathbf{m}_{k}^{\prime}=\mathbf{m}_{k}\oplus\mathbf{m}_{\Delta}\oplus(\mathbf{m}^{\prime}_{k-1}\ominus\mathbf{m}_{k-1})$

Defining
$\rho^{\prime}_{k}:=\rho^{\prime}_{k-1},\sigma_{k},(d_{k},\mathbf{m}_{k}^{\prime})$
we see that $\rho|_{k}\trianglelefteq\rho^{\prime}_{k}$, completing the proof
of Equation 7. We are now ready to show that
$\mathord{\downarrow}{\mathsf{Runs}(\mathord{\downarrow}{\mathfrak{P}})}=\mathord{\downarrow}{\mathsf{Runs}(\mathfrak{P})}$.
The direction
$\mathord{\downarrow}{\mathsf{Runs}(\mathfrak{P})}\subseteq\mathord{\downarrow}{\mathsf{Runs}(\mathord{\downarrow}{\mathfrak{P}})}$
follows immediately from Equation (6). Conversely, let

$\displaystyle\rho=(s_{0},\mathbf{n}_{0}),\sigma_{1},(s_{1},\mathbf{n}_{1}),\sigma_{2},...\in\mathord{\downarrow}{\mathsf{Runs}(\mathord{\downarrow}{\mathfrak{P}})}$
$\displaystyle\Rightarrow$
$\displaystyle\exists\rho^{\prime}\in\mathsf{Runs}(\mathord{\downarrow}{\mathfrak{P}})\;\rho\trianglelefteq\rho^{\prime}$
$\displaystyle\Rightarrow$
$\displaystyle\exists\rho^{\prime\prime}\in\mathsf{Runs}(\mathfrak{P})\;\rho^{\prime}\trianglelefteq\rho^{\prime\prime}\;$
by Equation (7) $\displaystyle\Rightarrow$
$\displaystyle\rho\in\mathord{\downarrow}{\mathsf{Runs}(\mathfrak{P})}$

We have proved that
$\mathord{\downarrow}{\mathsf{Runs}(\mathord{\downarrow}{\mathfrak{P}})}=\mathord{\downarrow}{\mathsf{Runs}(\mathfrak{P})}$.
We now show that each of the three properties i.e. safety, termination and
boundedness only depend on the downclosure of the runs.

Safety:

$\displaystyle d\text{ is reachable in }\mathfrak{P}$ iff
$\displaystyle\exists\rho=(d_{0},\mathbf{m}_{0}),\sigma_{1},(d_{1},\mathbf{m}_{1}),\sigma_{2},...,\sigma_{k},(d_{k},\mathbf{m}_{k})\in\mathsf{Runs}(\mathfrak{P})\colon
d_{k}=d$

By Equation 6, we know $\rho\in\mathsf{Runs}(\mathfrak{P})$ implies
$\rho\in\mathord{\downarrow}{\mathsf{Runs}(\mathfrak{P})}$. Conversely, if
there is
$\rho^{\prime}=(s_{0},\mathbf{n}_{0}),\sigma_{1},(s_{1},\mathbf{n}_{1}),\sigma_{2},...,\sigma_{k},(s_{k},\mathbf{n}_{k})\in\mathord{\downarrow}{\mathsf{Runs}(\mathfrak{P})}$
with $s_{k}=d$, then by Equation 7, there is
$\rho=(d_{0},\mathbf{m}_{0}),\sigma_{1},(d_{1},\mathbf{m}_{1}),\sigma_{1},...,\sigma_{k},(d_{k},\mathbf{m}_{k})\in\mathsf{Runs}(\mathfrak{P})$
with $\rho^{\prime}\trianglelefteq\rho$ which implies $d_{k}=d$. Hence we have

$\displaystyle d\text{ is reachable in }\mathfrak{P}$ iff
$\displaystyle\exists\rho=(s_{0},\mathbf{n}_{0}),\sigma_{1},(s_{1},\mathbf{n}_{1}),\sigma_{2},...,\sigma_{k},(s_{k},\mathbf{n}_{k})\in\mathord{\downarrow}{\mathsf{Runs}(\mathfrak{P})}\colon
s_{k}=d$

By a similar argument as above we also have:
Termination:

$\displaystyle\mathfrak{P}\text{ does not terminate }$ iff
$\displaystyle\exists\rho\in\mathsf{Runs}(\mathfrak{P})\colon\rho\text{ is
infinite }$ iff
$\displaystyle\exists\rho\in\mathord{\downarrow}{\mathsf{Runs}(\mathfrak{P})}\colon\rho\text{
is infinite }$

Boundedness:

$\displaystyle\mathfrak{P}\text{ is bounded }$ iff $\displaystyle\exists
N\in{\mathbb{N}}\;\forall\rho\in\mathsf{Runs}(\mathfrak{P})\;\forall
i\;|\rho(2i).m|<N$ iff $\displaystyle\exists
N\in{\mathbb{N}}\;\forall\rho\in\mathord{\downarrow}{\mathsf{Runs}(\mathfrak{P})}\;\forall
i\;|\rho(2i).m|<N$

In each of the three cases, the property only depends on the downclosure and
hence one may equivalently replace $\mathfrak{P}$ by
$\mathord{\downarrow}{\mathfrak{P}}$ since
$\mathord{\downarrow}{\mathsf{Runs}(\mathord{\downarrow}{\mathfrak{P}})}=\mathord{\downarrow}{\mathsf{Runs}(\mathfrak{P})}$.

##  Appendix C Proof of Proposition 6

We begin with a simple observation. For every $\mathsf{HORS}$
$\mathscr{S}=(\Sigma,\mathcal{N},S,\mathcal{R})$, there exists another
$\mathsf{HORS}$
$\mathscr{S}^{\prime}=(\Sigma^{\prime},\mathcal{N}^{\prime},S,\mathcal{R}^{\prime})$
where $\Sigma^{\prime}=\\{\mathtt{br},\mathsf{e}\\}\cup\tilde{\Sigma}$ with
$\mathtt{br}$ of arity 2, $\mathsf{e}$ of arity 0 and all symbols in
$\tilde{\Sigma}$ of arity 1; such that
$\mathcal{L}_{\mathsf{p}}(\mathscr{S})=\mathcal{L}_{\mathsf{p}}(\mathscr{S}^{\prime})$.

By rewriting every terminal symbol $A$ of arity $n\geq 2$ using the rule

$Ax_{1}x_{2}\cdots
x_{n}\twoheadrightarrow\mathtt{br}(x_{1}\mathtt{br}(x_{2}\mathtt{br}(\cdots\mathtt{br}(x_{n-1}x_{n}))$

and by replacing the occurrence of every nullary symbol in $\mathscr{S}$ by
$\mathtt{e}$, we get $\mathscr{S}^{\prime}$, which has the same path language.

We assume due to the above observation that
$\Sigma=\\{\mathtt{br},\mathsf{e}\\}\cup\tilde{\Sigma}$ where $\mathtt{br}$ is
binary, $\mathsf{e}$ is nullary and all letters in $\tilde{\Sigma}$ are unary.
Define
$\mathscr{S}^{\prime}=(\Sigma^{\prime},\mathcal{N}^{\prime},S^{\prime},\mathcal{R}^{\prime})$
as
$\Sigma^{\prime}=\tilde{\Sigma}\cup\\{\mathsf{e}\\},\mathcal{N}^{\prime}=\mathcal{N}\cup\\{B:\mathtt{o}\rightarrow(\mathtt{o}\rightarrow\mathtt{o})\\},\mathcal{R}^{\prime}=\\{r[\mathtt{br}/B]\mid
r\in\mathcal{R}\\}\cup\\{Bxy\twoheadrightarrow x,Bxy\twoheadrightarrow y\\}$,
where by $r[\mathtt{br}/B]$ we mean the rule $r$ with $\mathtt{br}$ uniformly
replaced by $B$. Note that the only new non-terminal symbol introduced is $B$,
which is of order 1. Hence the obtained word scheme $\mathscr{S}^{\prime}$ is
of the same order as $\mathscr{S}$.
$\mathcal{L}_{\mathsf{p}}(\mathscr{S})\subseteq\mathcal{L}_{\mathsf{w}}(\mathscr{S}^{\prime})$:
Let $w\in\mathcal{L}_{\mathsf{p}}(\mathscr{S})$. Therefore there exists a
finite path $\Pi$ in a sentential form $t$ such that $\forall\bar{n}\in
dom(\Pi)\;w_{\Pi}(\bar{n})\in\Sigma$. We derive $t^{\prime}:=t[\mathtt{br}/B]$
using the corresponding rules in $\mathcal{R}^{\prime}$. Note that the
corresponding path $\Pi^{\prime}$ in $t^{\prime}$ satisfies
$\forall\bar{n}\in\operatorname{dom}(\Pi^{\prime})w_{\Pi^{\prime}}(\bar{n})\in\Sigma\cup\\{B\\}$.
We then apply either $Bxy\twoheadrightarrow x$ or $Bxy\twoheadrightarrow y$ to
each $B$ in $t^{\prime}$ according to the path $\Pi^{\prime}$ to obtain $w$ in
the word scheme.
$\mathcal{L}_{\mathsf{w}}(\mathscr{S}^{\prime})\subseteq\mathcal{L}_{\mathsf{p}}(\mathscr{S})$:
We define the order $\leq_{\mathsf{pre}}$ on sequences of natural numbers
$\bar{n},\bar{m}$ as $\bar{n}\leq_{\mathsf{pre}}\bar{m}$ if
$\bar{m}=\bar{n}\bar{k}$ for some sequence $\bar{k}$.

Suppose that for given a sentential form $t^{\prime}$ of
$\mathscr{S}^{\prime}$ there exists a sentential form $t$ of $\mathscr{S}$ and
a map $\alpha:\operatorname{dom}(t^{\prime})\rightarrow\operatorname{dom}(t)$
(simply called embedding henceforth) satisfying the following conditions:

  * •

$\forall\bar{n}\in\operatorname{dom}(t^{\prime})$

$t^{\prime}(\bar{n})=\begin{cases}B\text{ if
}t(\alpha(\bar{n}))=\mathtt{br}\\\ t(\alpha(\bar{n}))\text{
otherwise}.\end{cases}$ (8)

  * •

$\forall\bar{n},\bar{m}\in\operatorname{dom}(t^{\prime}),\bar{n}\leq_{\mathsf{pre}}\bar{m}$
implies

$\alpha(\bar{n})\leq_{\mathsf{pre}}\alpha(\bar{m})\text{, and}$ (9)

$\displaystyle(\forall\bar{l}\;(\bar{n}<_{\mathsf{pre}}\bar{l}<_{\mathsf{pre}}\bar{m})\text{
implies }t^{\prime}(\bar{l})\notin\tilde{\Sigma})\text{ implies }$ (10)
$\displaystyle(\forall\bar{k}\;\alpha(\bar{n})<_{\mathsf{pre}}\bar{k}<_{\mathsf{pre}}\alpha(\bar{m})\text{
implies }t(\bar{k})\notin\tilde{\Sigma})$

Informally, Equations 8, 9 and 10 state the following: $\alpha$ preserves
labels, except for the case of $\mathtt{br}$ where it maps to $B$, $\alpha$
preserves the order $\leq_{\mathsf{pre}}$ and the images of any two nodes with
node labels from $\tilde{\Sigma}$ with no node label from $\tilde{\Sigma}$ in
between are mapped to two such nodes with the same property.

We will show by induction on the length of the derivation that such a pair
$(t,\alpha)$ always exists given some $t^{\prime}$. Let us see how the
existence of such $t$ and $\alpha$ gives us the proposition. Consider a word
$w=w_{1}w_{2}...w_{n}\in\mathcal{L}_{\mathsf{w}}(\mathscr{S}^{\prime})$. In
other words, there is a term
$t^{\prime}=w_{1}(w_{2}...(w_{n}(\mathsf{e}))...)$ such that
$S^{\prime}\underset{\mathscr{S}^{\prime}}{\twoheadrightarrow}^{*}t^{\prime}$.
Corresponding to this, we have a sentential form
$S\underset{\mathscr{S}}{\twoheadrightarrow}^{*}t$ and $\alpha$ satisfying the
given conditions. In particular, there exists a path $\Pi$ with
$\operatorname{dom}(\Pi)\subseteq dom(t)$ which is the path in $t$ connecting
the $\alpha(\varepsilon)$ to $\alpha(0^{n})$. It is immediate that
$\mathrm{Proj}_{\tilde{\Sigma}}(\Pi)=w$. It remains to show the existence of
$t$ and $\alpha$ by induction on the length of derivations.

$t^{\prime}_{0}$$\bar{n}$$u_{0}^{\prime}$$l_{0}^{\prime}$$r_{0}^{\prime}$$Bxy\twoheadrightarrow
x$$\mathscr{S}^{\prime}$$t^{\prime}$$\bar{n}$$u_{0}^{\prime}$$l_{0}^{\prime}$$t_{0}$$\alpha_{0}(\bar{n})$$u_{0}$$l_{0}$$r_{0}$$\alpha_{0}$$t_{0}$$u_{0}$$\alpha(\bar{n})$$l_{0}$$r_{0}$$\alpha$
Figure 2. Construction of embedding $\alpha$ from $\alpha_{0}$ in the case of
the rule $Bxy\twoheadrightarrow x$
$t^{\prime}_{0}$$\bar{n}$$u_{0}^{\prime}$$l_{0}^{\prime}$$r_{0}^{\prime}$$Nxy\twoheadrightarrow
t_{1}$$\mathscr{S}^{\prime}$$t^{\prime}$$\bar{n}$$u_{0}^{\prime}$$\bar{m}$$\bar{k}$$l_{0}^{\prime}$$r_{0}^{\prime}$$t_{1}[x/l^{\prime}_{0},y/r^{\prime}_{0}]$$t_{0}$$\alpha_{0}(\bar{n})$$u_{0}$$l_{0}$$r_{0}$$\alpha_{0}$$Nxy\twoheadrightarrow
t_{1}$$\mathscr{S}$$t$$\alpha(\bar{n})$$u_{0}$$\alpha(\bar{m})$$\alpha(\bar{k})$$l_{0}$$r_{0}$$t_{1}[x/l_{0},y/r_{0}]$$\alpha$
Figure 3. Construction of embedding $\alpha$ from $\alpha_{0}$ when the rule
is $Nxy\twoheadrightarrow t_{1}$

Base case: This is trivial since $t=t^{\prime}=S$.
Induction step: Suppose
$t_{0}^{\prime}\underset{r\in\mathcal{R}^{\prime}}{\twoheadrightarrow}t^{\prime}$
where $t_{0}^{\prime}$ is a sentential form. By induction hypothesis, there is
a sentential form $t_{0}$ of $\mathscr{S}$ and $t_{0}^{\prime}$ embeds into
$t_{0}$ via map $\alpha_{0}$. Assume that the rule $r$ is applied at position
$\bar{n}$ on $t_{0}^{\prime}$. We now have two cases to consider:
Case 1: The rule $r$ is
$Bxy\underset{\mathscr{S}^{\prime}}{\twoheadrightarrow}x$ (the case
$Bxy\underset{\mathscr{S}^{\prime}}{\twoheadrightarrow}y$ being symmetric). By
induction hypothesis, we have $t_{0}$ and and an embedding $\alpha_{0}$ of
$t_{0}^{\prime}$ into $t_{0}$. Refering to Figure 2, we see that $t$ can be
taken to be $t_{0}$ and $\alpha$ maps all nodes in the subtree
$u^{\prime}_{0}$ into $u_{0}$ as before, while the subtree $l^{\prime}_{0}$
rooted at $\bar{n}$ is mapped into $l_{0}$. It is immediate that $\alpha$
preserves the order and since by induction hypothesis $\alpha_{0}(\bar{n})$
has label $\mathtt{br}$, Equation 10 is also satisfied by $\alpha$ since no
new $\tilde{\Sigma}$ labelled nodes have been added.
Case 2: We demonstrate for the case when a non-terminal of arity two is
replaced for an easier reading of the proof: the rule $r$ is
$Nxy\underset{\mathscr{S}^{\prime}}{\twoheadrightarrow}t_{1}$ for some
nonterminal $N\neq B$. Refering to Figure 3, the rule replaces the subtree
rooted at $\bar{n}$ in $t^{\prime}_{0}$ with
$t_{1}[x/l^{\prime}_{0},y/r^{\prime}_{0}]$ where
$l^{\prime}_{0},r^{\prime}_{0}$ are respectively the left and right subtrees
of the subtree rooted at $\bar{n}$ in $u^{\prime}_{0}$. For nodes in the
subtree $u^{\prime}_{0}$ of $t^{\prime}$, $\alpha$ mimics $\alpha_{0}$. By
induction we know that the subtrees $l^{\prime}_{0},r^{\prime}_{0}$ of
$t^{\prime}_{0}$ embed respectively into $l_{0},r_{0}$ of $t_{0}$. Thus
$\alpha$ maps every subtree $l^{\prime}_{0}$ (resp. $r^{\prime}_{0}$) rooted
at $\bar{m}$ (resp. $\bar{k}$) in $t_{1}[x/l^{\prime}_{0},y/r^{\prime}_{0}]$
into the corresponding subtree $l_{0}$ (resp. $r_{0}$) rooted at
$\alpha(\bar{m})$ (resp. $\alpha(\bar{k})$). Note that $\alpha(\bar{m})$ can
be defined as the root of the $i$-th occurrence of $l_{0}$ from left to right
if $\bar{m}$ is the $i$-th occurrence of $l^{\prime}_{0}$ from left to right.
Nodes in $t_{1}[x/l^{\prime}_{0},y/r^{\prime}_{0}]$ which are not in any of
the $l_{0}^{\prime}$ (or $r_{0}^{\prime}$) subtrees (i.e.) between $\bar{n}$
and $\bar{m}$ (or $\bar{k})$) have corresponding nodes in
$t_{1}[x/l_{0},y/r_{0}]$ to which they can be mapped. Label preservation and
order preservation immediately follow by appeal to the induction hypothesis.
In order to see that Equation 10 holds, consider consecutive $\tilde{\Sigma}$
nodes $\bar{n}^{\prime},\bar{m}^{\prime}$ in $t^{\prime}$ (i.e.
$\bar{n}^{\prime}<_{\mathit{pre}}\bar{m}^{\prime}$ and there are no
$\tilde{\Sigma}$ labels in between). If both $\bar{n}^{\prime}$ and
$\bar{m}^{\prime}$ are in $u_{0}^{\prime}$ or in one of the $l^{\prime}_{0}$
(or $r_{0}^{\prime}$) then the induction hypothesis applies. In the case where
$\bar{n}^{\prime}\in u_{0}^{\prime}$ and $\bar{m}^{\prime}\in l_{0}^{\prime}$
(resp. $r_{0}^{\prime}$,) this means that no $\tilde{\Sigma}$ labels are
present in the path from $\bar{n}$ to $\bar{m}$ (resp. $\bar{k}$),
$\bar{n}^{\prime}$ to $\bar{n}$ nor $\bar{m}$ (resp. $\bar{k}$) to
$\bar{m}^{\prime}$. The path from $\alpha(\bar{n})$ to $\alpha(\bar{m})$ is
identical to that from $\bar{n}$ to $\bar{m}$ (resp. $\bar{k}$). The induction
hypothesis also implies that the first $\mathtt{a}$ label for some
$\mathtt{s}\in\tilde{\Sigma}$ in $l_{0}^{\prime}$ must be mapped to first
$\mathtt{a}$ label in $l_{0}$ (or $u_{0}^{\prime}$ does not contain any
$\tilde{\Sigma}$ labels). Hence there are no $\tilde{\Sigma}$ labels between
$\alpha(\bar{m})$ (resp. $\alpha(\bar{k})$) and $\alpha(\bar{m}^{\prime})$ and
similarly between $\alpha(\bar{n}^{\prime})$ and $\alpha(\bar{n})$. The final
case is when either $\bar{n}^{\prime}$ or $\bar{m}^{\prime}$ lies between
$\alpha(\bar{n})$ and $\alpha(\bar{m})$ (resp. $\alpha(\bar{k})$). There are
subcases here to consider when the other point lies in $u_{0}^{\prime}$,
$l_{0}$ or also between $\bar{n}$ and $\bar{m}$. In all of these subcases, it
easily follows that there are no extra $\tilde{\Sigma}$ labels introduced in
between two consecutive nodes which are in the image of $\alpha$.