48.9793pt\vbox{\vbox{}\hbox{\hskip-48.9793pt\hbox{\hbox{$\displaystyle\displaystyle\mathsf{join}(\mathsf{var}(x))\stackrel{{\scriptstyle\small{\mathsf{def}}}}{{=}}\mathsf{var}(x)$}}}}}}$}}\penalty
50\hskip 20.00003pt plus 0.5fil minus
5.0pt{\hbox{$\displaystyle\displaystyle{\hbox{\hskip
31.9271pt\vbox{\hbox{\hskip-31.92708pt\hbox{\hbox{$\displaystyle\displaystyle
x\in\mathsf{Trees}(\mathcal{N},\mathcal{V})$}}}\vbox{}}}\over\hbox{\hskip
38.27094pt\vbox{\vbox{}\hbox{\hskip-38.27092pt\hbox{\hbox{$\displaystyle\displaystyle\mathsf{join}(\mathsf{var}(x))\stackrel{{\scriptstyle\small{\mathsf{def}}}}{{=}}x$}}}}}}$}}$

###### Definition A.4 ($\pi$, $b\mathrel{\in_{\pi}}a$, $\mathsf{Subtrees}(a)$,
$\pi.\pi^{\prime}$, $\pi^{\prime}\geq\pi$).

We define a _path_ $\pi$, the relation $b\mathrel{\in_{\pi}}a$ if the path
$\pi$ relates the sub-tree $b$ to a parent tree $a$, and the multiset
$\mathsf{Subtrees}(a)$ of sub-trees of $a$.

$\displaystyle\begin{array}[]{llll}\pi&\mathrel{::=}&\emptyset&\\\
&\;\mathrel{|}&\pi.i&\qquad(i\in\mathbb{N})\\\ \end{array}\penalty 50\hskip
20.00003pt plus 0.5fil minus
5.0pt{\hbox{$\displaystyle\displaystyle{\hbox{\hskip
1.66496pt\vbox{\hbox{\hskip-1.66496pt\hbox{\hbox{$\displaystyle\displaystyle~{}$}}}\vbox{}}}\over\hbox{\hskip
10.01924pt\vbox{\vbox{}\hbox{\hskip-10.01923pt\hbox{\hbox{$\displaystyle\displaystyle
a\mathrel{\in_{\emptyset}}a$}}}}}}$}}\penalty 50\hskip 20.00003pt plus 0.5fil
minus 5.0pt{\hbox{$\displaystyle\displaystyle{\hbox{\hskip
10.68283pt\vbox{\hbox{\hskip-10.68283pt\hbox{\hbox{$\displaystyle\displaystyle
b\mathrel{\in_{\pi}}a_{i}$}}}\vbox{}}}\over\hbox{\hskip
36.80368pt\vbox{\vbox{}\hbox{\hskip-36.80367pt\hbox{\hbox{$\displaystyle\displaystyle
b\mathrel{\in_{\pi.i}}\mathsf{node}(c,\,({a_{i}})^{i})$}}}}}}$}}\penalty
50\hskip 20.00003pt plus 0.5fil minus
5.0pt\mathsf{Subtrees}(a)\stackrel{{\scriptstyle\small{\mathsf{def}}}}{{=}}\\{\mskip-5.0mu\\{{}b\mid\exists\pi,\
b\mathrel{\in_{\pi}}a\\}\mskip-5.0mu\\}$

Notice that the relation $b\mathrel{\in_{\pi}}a$ is compatible with the usual
notion of path concatenation $\pi.\pi^{\prime}$: if
$a_{1}\mathrel{\in_{\pi_{12}}}a_{2}$ and $a_{2}\mathrel{\in_{\pi_{23}}}a_{3}$,
then $a_{1}\mathrel{\in_{\pi_{12}.\pi_{23}}}a_{3}$.

Finally, we write that $\pi^{\prime}$ is an _extension_ of $\pi$, using the
notation $\pi^{\prime}\geq\pi$, if and only if $\pi^{\prime}$ is of the form
$\pi^{\prime\prime}.\pi$.

$\displaystyle\pi^{\prime}\geq\pi\penalty 50\hskip 20.00003pt plus 0.5fil
minus 5.0pt\stackrel{{\scriptstyle\small{\mathsf{def}}}}{{=}}\penalty 50\hskip
20.00003pt plus 0.5fil minus 5.0pt\exists\pi^{\prime\prime},\
\pi^{\prime}=\pi^{\prime\prime}.\pi$

###### Definition A.5 ($a{\left[\pi\leftarrow b\right]}$).

$a{\left[\pi\leftarrow b\right]}$ is the tree $a$ where the $\pi$-rooted sub-
tree is replaced by $b$:

$\displaystyle\displaystyle{\hbox{\hskip
1.66496pt\vbox{\hbox{\hskip-1.66496pt\hbox{\hbox{$\displaystyle\displaystyle~{}$}}}\vbox{}}}\over\hbox{\hskip
29.75403pt\vbox{\vbox{}\hbox{\hskip-29.75403pt\hbox{\hbox{$\displaystyle\displaystyle
a{\left[\emptyset\leftarrow
b\right]}\stackrel{{\scriptstyle\small{\mathsf{def}}}}{{=}}b$}}}}}}$
$\displaystyle\displaystyle{\hbox{\hskip
28.19846pt\vbox{\hbox{\hskip-28.19844pt\hbox{\hbox{$\displaystyle\displaystyle
a_{j}{\left[\pi\leftarrow b\right]}=a^{\prime}$}}}\vbox{}}}\over\hbox{\hskip
118.51634pt\vbox{\vbox{}\hbox{\hskip-118.51634pt\hbox{\hbox{$\displaystyle\displaystyle\mathsf{node}(c,\,({a_{i}})^{i\in
I}){\left[\pi.j\leftarrow
b\right]}\stackrel{{\scriptstyle\small{\mathsf{def}}}}{{=}}\mathsf{node}(c,\,\left(({a_{i}})^{i\in
I\setminus\\{j\\}},(j\mapsto a^{\prime})\right))$}}}}}}$

We use $n$-ary trees to model our annotated $\lambda$-terms.

###### Example A.6 (Trees of annotated terms).

Let us consider our annotated terms $\bar{t}$ as $n$-ary trees
$\mathsf{tree}(\bar{t})$; these trees belong to the set
$\mathsf{Trees}(\mathcal{T},\emptyset)$ for a set of tree node constructors
$\mathcal{T}$ defined by the following grammar:

$\displaystyle\mathcal{T}\ni
c\mathrel{::=}\;x\;\mathrel{|}\;{f}\mathrel{@}{l}\penalty-10000\hskip
20.00003pt plus 0.5fil minus
5.0pt\mathsf{tree}(x)\stackrel{{\scriptstyle\small{\mathsf{def}}}}{{=}}\mathsf{node}(x,\,\emptyset)\penalty
50\hskip 20.00003pt plus 0.5fil minus
5.0pt\mathsf{tree}({f{({\bar{t}_{i}})^{i}}}\mathrel{@}{l})\stackrel{{\scriptstyle\small{\mathsf{def}}}}{{=}}\mathsf{node}({f}\mathrel{@}{l},\,({\mathsf{tree}(\bar{t}_{i})})^{i})$

For example the annotated term
${f({g()}\mathrel{@}{l_{g}},x)}\mathrel{@}{l_{f}}$ becomes the tree

$\displaystyle\mathsf{node}({f}\mathrel{@}{l_{f}},\,\left(0\mapsto\mathsf{node}({g}\mathrel{@}{l_{g}},\,\emptyset),1\mapsto\mathsf{node}(x,\,\emptyset)\right))$

####  A.1.2. Tree expansion

We now define an expansion process for our $n$-ary trees, that generalizes our
reduction of terms. Informally, we consider the following expansion process:

  * •

A node (in arbitrary position) in the tree is chosen to be expanded. We call
_expanded sub-tree_ the sub-tree rooted at this node.;

  * •

The expansion process replaces this expanded sub-tree by another sub-tree
containing:

    * –

zero, or several _new_ nodes, that do not correspond to nodes from the
previous tree, and

    * –

an arbitrary number of copies of some sub-trees of the expanded sub-tree.

A sub-tree of the expanded sub-tree can disappear during an expansion, or be
duplicated into one or several sub-trees, placed inside the new sub-tree that
replaces the expanded sub-tree.

Formally:

###### Definition A.7 (Tree expansion).

A _head tree expansion_
$b\stackrel{{\scriptstyle\mathsf{head}}}{{\leadsto}}b^{\prime}$ replaces a
tree $b$ by another tree $b^{\prime}$, some sub-trees of which are strict sub-
trees of $b$ – not $b$ itself.

$\displaystyle\displaystyle{\hbox{\hskip
117.93758pt\vbox{\hbox{\hskip-117.93756pt\hbox{\hbox{$\displaystyle\displaystyle
b\in\mathsf{Trees}(\mathcal{N},\mathcal{V})$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle
b_{s}\in\mathsf{Trees}(\mathcal{N},\mathcal{V}\uplus(\mathsf{Subtrees}(b)\setminus\\{b\\}))$}}}}\vbox{}}}\over\hbox{\hskip
29.882pt\vbox{\vbox{}\hbox{\hskip-29.88199pt\hbox{\hbox{$\displaystyle\displaystyle
b\stackrel{{\scriptstyle\mathsf{head}}}{{\leadsto}}{\mathsf{join}(b_{s})}$}}}}}}$

A _tree expansion_ $a\leadsto a^{\prime}$ is a head tree expansion in a sub-
tree of $a$.

$\displaystyle\displaystyle{\hbox{\hskip
37.661pt\vbox{\hbox{\hskip-37.66098pt\hbox{\hbox{$\displaystyle\displaystyle
b\mathrel{\in_{\pi_{b}}}a$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle
b\stackrel{{\scriptstyle\mathsf{head}}}{{\leadsto}}b^{\prime}$}}}}\vbox{}}}\over\hbox{\hskip
29.19789pt\vbox{\vbox{}\hbox{\hskip-29.19788pt\hbox{\hbox{$\displaystyle\displaystyle
a\leadsto a{\left[\pi_{b}\leftarrow b^{\prime}\right]}$}}}}}}$

$a$ $b$ $c$ $d$ $e$ $f$ $\leadsto$ $a$ $b$ $c^{\prime}$ $d$ $e$ $f$ $a$ $b$
$e$ $f$ $a$ $b$ $c^{\prime}$ $c^{\prime\prime}$ $e$ $f$ $f$ $e$ $f$ Figure 1.
Tree expansions

###### Example A.8.

Figure 1 shows a tree on the left, and three possible expansions of it on the
right, all from the node with labeled by the constructor $c$, with new nodes
shown in red. In the first expansion, the node $c$ is replaced by the new node
$c^{\prime}$, which carries the children of $c$ (they were neither duplicated
nor erased). In the second expansion, there is no new node, $c$ has been
replaced by its sub-tree rooted in $e$ and $d$ was erased. In the third
expansion, there are two new nodes $c^{\prime}$ and $c^{\prime\prime}$, two
copies of the sub-tree rooted in $e$, one additional copy of the sub-tree
rooted in $f$, and $d$ is erased: the sub-tree of constructor $c$ has been
replaced by a sub-tree of the form $c^{\prime}(c^{\prime\prime}(x,y),x)$,
where the variable $x$ is the sub-sub-tree $e(f)$, and $y$ is the sub-sub-tree
$f$.

###### Fact 6.

The tree expansion process generalizes $\beta$-reduction of our annotated
first-order terms: for any definition environment $D$,

$\displaystyle\mathtt{let}~{}\mathtt{rec}~{}D~{}\mathtt{in}~{}\bar{t}\leadsto\mathtt{let}~{}\mathtt{rec}~{}D~{}\mathtt{in}~{}\bar{t}^{\prime}\penalty
50\hskip 20.00003pt plus 0.5fil minus 5.0pt\implies\penalty 50\hskip
20.00003pt plus 0.5fil minus
5.0pt\mathsf{tree}(\bar{t})\leadsto\mathsf{tree}(\bar{t}^{\prime})$

In particular, any infinite reduction sequence of annotated terms could be
mapped to an infinite sequence of tree expansions on the corresponding trees.

##### Remark

$\beta$-reductions in our annotated terms replace variables $x_{i}$ by
function parameters $\bar{t}_{i}$. In terms of tree, this corresponds to a
subset of expansions where the erased/duplicated sub-trees are always exactly
the immediate children of the expanded node, not sub-trees of arbitrary depth.
We believe that the ability to manipulate arbitrary sub-trees, which does not
make the proof more difficult, is in fact useful to express expansion
processes outside our model. In particular, it would be useful to model _type
constraints_ in the OCaml programming language:

⬇

type ’a t = (’b * bool) constraint ’a = ’b * ’b * int

which effectively allow to designate arbitrary sub-expressions of the type
parameters and use them directly in an abbreviation definition. In rewriting
systems it is also not uncommon to have complex left-hand-side that match on
their arguments in-depth.

###### Definition A.9 ($\mathsf{Trees}(\mathcal{N})$).

Variables $\mathcal{V}$ were used to define expansion by substitution. In the
rest of this document we will mostly work with _closed_ $n$-ary trees in
$\mathsf{Trees}(\mathcal{N},\emptyset)$, which we write as just
$\mathsf{Trees}(\mathcal{N})$.

###### Definition A.10 ($\mathsf{constr}(a)$).

For $a\in\mathsf{Trees}(\mathcal{N})$ we define $\mathsf{constr}(a)$ as the
head constructor of $a$ (which cannot be a variable as $a$ is in
$\mathsf{Trees}(\mathcal{N},\emptyset)$):

$\displaystyle\mathsf{constr}(\mathsf{node}(c,\,({a_{i}})^{i}))\stackrel{{\scriptstyle\small{\mathsf{def}}}}{{=}}c$

####  A.1.3. Measured expansions

###### Definition A.11 (Measure).

For a set $A$, we call _measure on A_ a function $m_{A}:A\to M$ into a set $M$
equipped with a well-founded partial order $(<_{M})$.777A (strict) partial
order $(<)$ is well-founded if it does not admit any infinite descending
chain, any sequence $({m_{i}})^{i\in\mathbb{N}}$ with $\forall
i\in\mathbb{N},\ m_{i}>m_{i+1}$..

###### Definition A.12 (Measured expansion).

Given a measure $m_{\mathcal{N}}$ on $\mathcal{N}$, we write that an expansion
$a\leadsto a^{\prime}\in\mathsf{Trees}(\mathcal{N})$ is _measured_ when the
new nodes of the expansion have strictly smaller measure than the expanded
node. Formally, an expansion

$\displaystyle\displaystyle{\hbox{\hskip
87.28806pt\vbox{\hbox{\hskip-87.28806pt\hbox{\hbox{$\displaystyle\displaystyle
b\mathrel{\in_{\pi_{b}}}a$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\raise
11.0pt\hbox{$\displaystyle{\hbox{$\displaystyle\displaystyle{\hbox{\hskip
65.21652pt\vbox{\hbox{\hskip-65.2165pt\hbox{\hbox{$\displaystyle\displaystyle
b_{s}\in\mathsf{Trees}(\mathcal{N},\mathsf{Subtrees}(a)\setminus\\{a\\})$}}}\vbox{}}}\over\hbox{\hskip
29.882pt\vbox{\vbox{}\hbox{\hskip-29.88199pt\hbox{\hbox{$\displaystyle\displaystyle
b\stackrel{{\scriptstyle\mathsf{head}}}{{\leadsto}}{\mathsf{join}(b_{s})}$}}}}}}$}}\hbox{}$
}$}}}}\vbox{}}}\over\hbox{\hskip
40.6221pt\vbox{\vbox{}\hbox{\hskip-40.62209pt\hbox{\hbox{$\displaystyle\displaystyle
a\leadsto a{\left[\pi\leftarrow\mathsf{join}(b_{s})\right]}$}}}}}}$

is measured if the nodes of $b_{s}$ are strictly below those of $b$:

$\displaystyle\forall{\pi},\
\mathsf{node}(c,\,\\_)\mathrel{\in_{\pi}}b_{s}\implies
m_{\mathcal{N}}(c)<m_{\mathcal{N}}(\mathsf{constr}(b))$

###### Lemma A.13.

The reduction of annotated terms is measured.

###### Proof.

Given a fixed environment $D$ of recursive definitions, we consider the subset
of tree expansions of the form
$\mathsf{tree}(\bar{t})\leadsto\mathsf{tree}(\bar{t}^{\prime})$ coming from a
reduction of annotated terms
$\mathtt{let}~{}\mathtt{rec}~{}D~{}\mathtt{in}~{}\bar{t}\leadsto\mathtt{let}~{}\mathtt{rec}~{}D~{}\mathtt{in}~{}\bar{t}^{\prime}$.

Such a reduction of annotated terms is of the form

$\displaystyle\displaystyle{\hbox{\hskip
54.89783pt\vbox{\hbox{\hskip-54.89781pt\hbox{\hbox{$\displaystyle\displaystyle(f{({x_{i}})^{i}}=t^{\prime})\in
D$}\hskip 20.00003pt\hbox{\hbox{$\displaystyle\displaystyle f\notin
l$}}}}\vbox{}}}\over\hbox{\hskip
118.72928pt\vbox{\vbox{}\hbox{\hskip-118.72926pt\hbox{\hbox{$\displaystyle\displaystyle\mathtt{let}~{}\mathtt{rec}~{}D~{}\mathtt{in}~{}C[{f{({\bar{t}_{i}})^{i}}}\mathrel{@}{l}]\leadsto\mathtt{let}~{}\mathtt{rec}~{}D~{}\mathtt{in}~{}C[t^{\prime}{\left[({x_{i}\leftarrow\bar{t}_{i}})^{i}\right]}^{@l,f}]$}}}}}}$

As a measure of an annotated node ${\dots}\mathrel{@}{l}$, we use the trace
$l$ ordered by anti-inclusion: $l\leq l^{\prime}$ if and only if $l\supseteq
l^{\prime}$. Our traces may not contain duplicates, and the number of function
names in $D$ is finite; its cardinality is the maximal size of any trace, so
the inclusion order is well-founded. We extend this order with a minimal
element for all free variables $x$, that cannot reduce further.

The replacement of ${f{({\bar{t}_{i}})^{i}}}\mathrel{@}{l}$ by
$t^{\prime}{\left[({x_{i}\leftarrow\bar{t}_{i}})^{i}\right]}^{@l,f}$
corresponds to a measured expansion, as the new nodes are (variables or)
annotated with the trace $l,f$ which is strictly smaller than $l$ for our
order. ∎

###  A.2. A measure on trees meant for measured expansions

To prove our termination result, we use the measure $m_{\mathcal{N}}$ on nodes
to build a measure on trees into a well-chosen set with a well-founded partial
order, such that measured expansions strictly decrease the tree measure.

Given a set $(S,<_{S})$ with a well-founded partial order, we can build a
well-founded partial order $(<_{\mathcal{P}(S)})$ on the set $\mathcal{P}(S)$
of sets of elements of $S$, and a well-founded partial order
$(<_{\mathcal{M}(S)})$ on the set $\mathcal{M}(S)$ of multisets of elements of
$S$. The multiset order is attributed to Dershowitz, Manna, Huet and Oppen).

  * •

$S_{1}<_{\mathcal{P}(S)}S_{2}$ if, for any $a\in S_{1}$, there exists $b\in
S_{2}$ such that $a<_{S}b$.

  * •

$M_{1}<_{\mathcal{M}(S)}M_{2}$ if $M_{1}$ is of the form $M+N_{1}$ and $M_{2}$
is of the form $M+N_{2}$ with
$\lfloor{}{N_{1}}\rfloor{}_{\mathsf{set}}<_{\mathcal{P}(S)}\lfloor{}{N_{2}}\rfloor{}_{\mathsf{set}}$.

Given a measure $m_{\mathcal{N}}:\mathcal{N}\to(O,<_{O})$ on the node
constructors of our tree (where $(<_{O})$ is a well-founded partial order), we
define for any closed tree $a\in\mathsf{Trees}(\mathcal{N})$ a measure
$m_{\mathsf{Node}(a)}:\mathsf{Subtrees}(a)\to(\mathcal{M}(O),<_{\mathcal{M}(O)})$
on the nodes of $a$, by considering for each node the path from this node
(included) to the root of the tree, seen as a multiset of nodes.

Formally, we define our measure $m_{\mathsf{Node}(a)}(b)$ into
$\mathcal{M}(O)$, for each node $b\in\mathsf{Subtrees}(a)$, as the multiset
sum of the measure of the constructor of $b$ and a measure
$m_{\mathsf{Path}(a)}$ also into $\mathcal{M}(O)$ defined by induction on the
predicate $b\mathrel{\in_{\pi}}a$.

$\displaystyle
m_{\mathsf{Node}(a)}(b)\quad\stackrel{{\scriptstyle\small{\mathsf{def}}}}{{=}}\quad\\{\mskip-5.0mu\\{{}m_{\mathcal{N}}(\mathsf{constr}(b))\\}\mskip-5.0mu\\}{}+m_{\mathsf{Path}(a)}(b\mathrel{\in_{\pi}}a)\penalty
50\hskip 20.00003pt plus 0.5fil minus
5.0ptm_{\mathsf{Path}(a)}\left({\hbox{$\displaystyle\vbox{\hbox{\hskip
10.01924pt\vbox{\vbox{}\hbox{\hskip-10.01923pt\hbox{\hbox{$\displaystyle\displaystyle
a\mathrel{\in_{\emptyset}}a$}}}}}}$}}\right)\stackrel{{\scriptstyle\small{\mathsf{def}}}}{{=}}\emptyset\penalty
50\hskip 20.00003pt plus 0.5fil minus
5.0ptm_{\mathsf{Path}(\mathsf{node}(c,\,({a_{i}})^{i}))}\left({\hbox{$\displaystyle\displaystyle{\hbox{\hskip
10.68283pt\vbox{\hbox{\hskip-10.68283pt\hbox{\hbox{$\displaystyle\displaystyle
b\mathrel{\in_{\pi}}a_{i}$}}}\vbox{}}}\over\hbox{\hskip
36.80368pt\vbox{\vbox{}\hbox{\hskip-36.80367pt\hbox{\hbox{$\displaystyle\displaystyle
b\mathrel{\in_{\pi.i}}\mathsf{node}(c,\,({a_{i}})^{i})$}}}}}}$}}\right)\stackrel{{\scriptstyle\small{\mathsf{def}}}}{{=}}\\{\mskip-5.0mu\\{{}m_{\mathcal{N}}(c)\\}\mskip-5.0mu\\}{}+m_{\mathsf{Path}(a_{i})}\left(b\mathrel{\in_{\pi}}a_{i}\right)$

Note that the measure of the root $a$ is not taken into account by our path
measure: we define $m_{\mathsf{Path}(a)}(a\mathrel{\in_{\emptyset}}a)$ as
$\emptyset$ rather than
$\\{\mskip-5.0mu\\{{}m_{\mathcal{N}}(a)\\}\mskip-5.0mu\\}{}$. This is
essential for the measure to be compatible with path concatenation:

###### Fact 7.

$\displaystyle a_{1}\mathrel{\in_{\pi_{12}}}a_{2}\quad\wedge\quad
a_{2}\mathrel{\in_{\pi_{23}}}a_{3}\penalty-10000\hskip 20.00003pt plus 0.5fil
minus 5.0pt\implies\penalty 50\hskip 20.00003pt plus 0.5fil minus
5.0ptm_{\mathsf{Path}(a_{3})}(a_{1}\mathrel{\in_{\pi_{12}.\pi_{23}}}a_{3})\quad=\quad
m_{\mathsf{Path}(a_{2})}(a_{1}\mathrel{\in_{\pi_{12}}}a_{2})+m_{\mathsf{Path}(a_{3})}(a_{2}\mathrel{\in_{\pi_{23}}}a_{3})$

From this measure on nodes
$m_{\mathsf{Node}(a)}:\mathsf{Subtrees}(a)\to(\mathcal{M}(O),<_{\mathcal{M}(O)})$
we now define a measure on trees
$m_{\mathsf{Tree}}:\mathsf{Trees}(\mathcal{N})\to(\mathcal{M}(\mathcal{M}(O)),<_{\mathcal{M}(\mathcal{M}(O))})$
by considering for each tree the multiset of measures of its nodes. Our trees
are thus measured as multisets of multisets of node constructors, themselves
equipped with a well-founded partial order.

$\displaystyle
m_{\mathsf{Tree}}(a)\stackrel{{\scriptstyle\small{\mathsf{def}}}}{{=}}\\{\mskip-5.0mu\\{{}m_{\mathsf{Node}(a)}(b)\mid
b\in\mathsf{Subtrees}(a)\\}\mskip-5.0mu\\}$

###  A.3. Termination of measured expansions

###### Theorem A.14 (Termination).

If $\mathcal{M}$ has a measure $m_{\mathcal{N}}$, then the tree expansions
that are measured for $m_{\mathcal{N}}$ are strictly decreasing for the order
$m_{\mathsf{Tree}}$. In particular, there are no infinite sequences of
measured expansions.

###### Proof.

A measured expansion $a\leadsto a^{\prime}$ is necessarily of the following
form, where a sub-tree $b$ at a path $\pi_{b}$ in $a$ is replaced by a sub-
tree $\mathsf{join}(b_{s})$, where the constructors of $b_{s}$ are of strictly
smaller measure than $b$:

$\displaystyle{\hbox{$\displaystyle\displaystyle{\hbox{\hskip
65.21652pt\vbox{\hbox{\hskip-65.2165pt\hbox{\hbox{$\displaystyle\displaystyle
b_{s}\in\mathsf{Trees}(\mathcal{N},\mathsf{Subtrees}(a)\setminus\\{a\\})$}}}\vbox{}}}\over\hbox{\hskip
50.28687pt\vbox{\vbox{}\hbox{\hskip-50.28687pt\hbox{\hbox{$\displaystyle\displaystyle{\hbox{$\displaystyle\displaystyle{\hbox{\hskip
50.28687pt\vbox{\hbox{\hskip-50.28687pt\hbox{\hbox{$\displaystyle\displaystyle
b\mathrel{\in_{\pi_{b}}}a$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle
b\stackrel{{\scriptstyle\mathsf{head}}}{{\leadsto}}{\mathsf{join}(b_{s})}$}}}}\vbox{}}}\over\hbox{\hskip
49.12561pt\vbox{\vbox{}\hbox{\hskip-49.1256pt\hbox{\hbox{$\displaystyle\displaystyle
a\leadsto
a{\left[\pi_{b}\leftarrow\mathsf{join}(b_{s})\right]}=a^{\prime}$}}}}}}$}}$}}}}}}$}}\penalty
50\hskip 20.00003pt plus 0.5fil minus
5.0pt\forall\pi,(\mathsf{node}(c,\,\\_))\mathrel{\in_{\pi}}b_{s}\implies
m_{\mathcal{N}}(c)<m_{\mathcal{N}}(\mathsf{constr}(b))$

We have to show that $m_{\mathsf{Tree}}(a)>m_{\mathsf{Tree}}(a^{\prime})$.

##### Nodes inside or outside $\pi_{b}$

We can partition the paths $\pi$ valid inside $a$ or $a^{\prime}$ in two
disjoint sets:

  * •

the paths to nodes _inside_ $\pi_{b}$, that is the paths $\pi\geq\pi_{b}$ that
extend $\pi_{b}$; they denote a sub-tree of $b$ (in $a$) or a sub-tree of
$\mathsf{join}(b_{s})$ (in $a^{\prime}$), and

  * •

the paths to nodes _outside_ $\pi_{b}$, that is the paths $\pi\ngeq\pi_{b}$
that do not extend $\pi_{b}$, they reach an unrelated part of the tree.

$\displaystyle\begin{array}[]{ll}&m_{\mathsf{Tree}}(a)\\\
=&\\{\mskip-5.0mu\\{{}m_{\mathsf{Node}(a)}(b^{\prime})\mid\exists
b^{\prime}\in\mathsf{Subtrees}(a)\\}\mskip-5.0mu\\}{}\\\
=&\\{\mskip-5.0mu\\{{}m_{\mathsf{Node}(a)}(b^{\prime})\mid\exists
b^{\prime}\exists\pi,\ b^{\prime}\mathrel{\in_{\pi}}a\\}\mskip-5.0mu\\}{}\\\
=&\\{\mskip-5.0mu\\{{}m_{\mathsf{Node}(a)}(b^{\prime})\mid\exists
b^{\prime}\exists\pi\geq\pi_{b},\
b^{\prime}\mathrel{\in_{\pi}}a\\}\mskip-5.0mu\\}{}+\\{\mskip-5.0mu\\{{}m_{\mathsf{Node}(a)}({b^{\prime}})\mid\exists
b^{\prime}\exists\pi\ngeq\pi_{b},\
b^{\prime}\mathrel{\in_{\pi}}a\\}\mskip-5.0mu\\}{}\\\\[10.00002pt] \penalty
50\hskip 20.00003pt plus 0.5fil minus 5.0pt&m_{\mathsf{Tree}}(a^{\prime})\\\
=&\\{\mskip-5.0mu\\{{}m_{\mathsf{Node}(a^{\prime})}({b^{\prime}})\mid\exists
b^{\prime}\exists\pi\geq\pi_{b},\
b^{\prime}\mathrel{\in_{\pi}}a^{\prime}\\}\mskip-5.0mu\\}{}+\\{\mskip-5.0mu\\{{}m_{\mathsf{Node}(a^{\prime})}({b^{\prime}})\mid\exists
b^{\prime}\exists\pi\ngeq\pi_{b},\
b^{\prime}\mathrel{\in_{\pi}}a^{\prime}\\}\mskip-5.0mu\\}{}\\\ \end{array}$

The measure $m_{\mathsf{Node}(a)}(b^{\prime})$ of a sub-tree $b^{\prime}$ of
$a$ depends only on the constructors along the path from the root $a$ to the
node $b^{\prime}$ included. In particular, if the node $b^{\prime}$ is at a
path $\pi\ngeq\pi_{b}$ that does not extend $\pi_{b}$, it is also present at
the same path as a sub-tree of $a^{\prime}$, where it has the same measure, as
$a^{\prime}$ and $a$ only differ inside $\pi_{b}$.

$\displaystyle\\{\mskip-5.0mu\\{{}m_{\mathsf{Node}(a)}({b^{\prime}})\mid\exists
b^{\prime}\exists\pi\ngeq\pi_{b},\
b^{\prime}\mathrel{\in_{\pi}}a\\}\mskip-5.0mu\\}{}\penalty 50\hskip 20.00003pt
plus 0.5fil minus 5.0pt=\penalty 50\hskip 20.00003pt plus 0.5fil minus
5.0pt\\{\mskip-5.0mu\\{{}m_{\mathsf{Node}(a^{\prime})}({b^{\prime}})\mid\exists
b^{\prime}\exists\pi\ngeq\pi_{b},\
b^{\prime}\mathrel{\in_{\pi}}a^{\prime}\\}\mskip-5.0mu\\}$

Recall that our multiset order is defined by inequalities
$M+N_{1}<_{\mathcal{M}(S)}M+N_{2}$ with
$\lfloor{}{N_{1}}\rfloor{}_{\mathsf{set}}<_{\mathcal{P}(S)}\lfloor{}{N_{2}}\rfloor{}_{\mathsf{set}}$.
We use the measures of the nodes outside $\pi_{b}$ as the multiset $M$ in that
definition. It remains to prove the set ordering between the measures of nodes
inside $\pi_{b}$, playing the role of $N_{1}$ and $N_{2}$ in the definition:

$\displaystyle\\{m_{\mathsf{Node}(a)}(b^{\prime})\mid\exists
b^{\prime}\exists\pi\geq\pi_{b},\ b^{\prime}\mathrel{\in_{\pi}}a\\}\penalty
50\hskip 20.00003pt plus 0.5fil minus
5.0pt>_{\mathcal{P}(\mathcal{M}(O))}\penalty 50\hskip 20.00003pt plus 0.5fil
minus 5.0pt\\{m_{\mathsf{Node}(a^{\prime})}({b^{\prime}})\mid\exists
b^{\prime}\exists\pi\geq\pi_{b},\ b^{\prime}\mathrel{\in_{\pi}}a^{\prime}\\}$

##### A classification of paths under $\mathsf{join}(b_{s})$

For each sub-tree under $\pi_{b}$ in $a^{\prime}$, that is each sub-tree of
$\mathsf{join}(b_{s})$, we have to show that there exists a sub-tree under
$\pi_{b}$ in $a$, that is a sub-tree of $b$, of strictly larger measure.

Let us remark (and prove) that a sub-tree $b^{\prime}$ of $a^{\prime}$ has a
path of the form $\pi_{s}.\pi_{n}.\pi_{b}$, with, reading right to left from
the root to the leaves:

  * •

the path $\pi_{b}$ from $b$ to the root $a$,

  * •

a path $\pi_{n}$ (_n_ ew node) inside zero, one or several “new” nodes
introduced by the expansion,

  * •

a path $\pi_{s}$ (_s_ ubtree), possibly empty, inside a copy of a strict
subtree of $b$.

When $\pi_{s}$ does indeed reach inside a subtree copied from $b$, we
furthermore define a path $\pi_{o}$ (_o_ ld node) from $b$ to the first old
node copied – otherwise $\pi_{v}$ is defined to be empty.

For example, in Figure 1, some paths into the nodes of the third expansion of
$c$ are as follows – for readability we write paths by marking the constructor
of the node, rather than its child index:

  * •

$[a,c^{\prime}]$, which has the decomposition $\pi_{b}=[a]$,
$\pi_{n}=[c^{\prime}]$, $\pi_{s}=[]$ with $\pi_{o}=[]$.

  * •

$[a,c^{\prime},c^{\prime\prime},f]$, which has the decomposition
$\pi_{b}=[a]$, $\pi_{n}=[c^{\prime},c^{\prime\prime}]$, $\pi_{s}=[f]$ with
$\pi_{v}=[e]$.

The presence of $\pi_{b}$ is by hypothesis, we are classifying the paths
$\pi\geq\pi_{b}$ which necessarily have $\pi=\pi^{\prime}.\pi_{b}$ for some
$\pi^{\prime}$ such that
$b^{\prime}\mathrel{\in_{\pi^{\prime}}}\mathsf{join}(b_{s})$. Formally, we
just defined how to split this sub-path $\pi^{\prime}$ into a pair
$(\pi_{s},\pi_{n})$ by defining a function
$\mathsf{split\\_join}\left({b_{s}},\
{b^{\prime}\mathrel{\in_{\pi^{\prime}}}\mathsf{join}(b_{s})}\right)$ by
induction on $b_{s}$ and inversion on the definition of
$\mathsf{join}(b_{s})$:

$\displaystyle\mathsf{split\\_join}\left({\mathsf{var}(x)},\
{{\hbox{$\displaystyle\displaystyle{\hbox{\hskip
31.9271pt\vbox{\hbox{\hskip-31.92708pt\hbox{\hbox{$\displaystyle\displaystyle
x\in\mathsf{Trees}(\mathcal{N},\mathcal{V})$}}}\vbox{}}}\over\hbox{\hskip
43.89886pt\vbox{\vbox{}\hbox{\hskip-43.89885pt\hbox{\hbox{$\displaystyle\displaystyle
b^{\prime}\mathrel{\in_{\pi^{\prime\prime}}}\mathsf{join}(\mathsf{var}(x))=x$}}}}}}$}}}\right)\stackrel{{\scriptstyle\small{\mathsf{def}}}}{{=}}(\pi^{\prime\prime},\emptyset)\penalty
50\hskip 20.00003pt plus 0.5fil minus
5.0pt\mathsf{split\\_join}\left({\mathsf{node}(c,\,\\_)},\
{{\hbox{$\displaystyle\displaystyle{\hbox{\hskip
1.66496pt\vbox{\hbox{\hskip-1.66496pt\hbox{\hbox{$\displaystyle\displaystyle~{}$}}}\vbox{}}}\over\hbox{\hskip
40.5065pt\vbox{\vbox{}\hbox{\hskip-40.5065pt\hbox{\hbox{$\displaystyle\displaystyle
b^{\prime}\mathrel{\in_{\emptyset}}\mathsf{node}(c,\,\\_)=b^{\prime}$}}}}}}$}}}\right)\stackrel{{\scriptstyle\small{\mathsf{def}}}}{{=}}(\emptyset,\emptyset)\penalty
50\hskip 20.00003pt plus 0.5fil minus
5.0pt\begin{array}[]{r}\mathsf{split\\_join}\left({\mathsf{node}(c,\,({a_{i}})^{i})},\
{{\hbox{$\displaystyle\displaystyle{\hbox{\hskip
24.4162pt\vbox{\hbox{\hskip-24.41618pt\hbox{\hbox{$\displaystyle\displaystyle
b^{\prime}\mathrel{\in_{\pi^{\prime\prime}}}\mathsf{join}(a_{i})$}}}\vbox{}}}\over\hbox{\hskip
50.53705pt\vbox{\vbox{}\hbox{\hskip-50.53703pt\hbox{\hbox{$\displaystyle\displaystyle
b^{\prime}\mathrel{\in_{\pi^{\prime\prime}.i}}\mathsf{join}(\mathsf{node}(c,\,({a_{i}})^{i}))$}}}}}}$}}}\right)\stackrel{{\scriptstyle\small{\mathsf{def}}}}{{=}}(\pi^{\prime\prime}_{s},\pi^{\prime\prime}_{n}.i)\\\
\quad\text{where}\quad(\pi^{\prime\prime}_{s},\pi^{\prime\prime}_{n})=\mathsf{split\\_join}\left({a_{i}},\
{b^{\prime}\mathrel{\in_{\pi^{\prime\prime}}}\mathsf{join}(a_{i})}\right)\end{array}$

By definition we have $\pi_{s}.\pi_{n}=\pi^{\prime}$, so
$b^{\prime}\mathrel{\in_{\pi_{s}.\pi_{n}}}\mathsf{join}(b_{s})$, and we also
have $b^{\prime}\mathrel{\in_{\pi_{s}}}\mathsf{join}(b_{s}^{\prime})$ and
$b_{s}^{\prime}\mathrel{\in_{\pi_{n}}}b_{s}$ for a sub-tree $b_{s}^{\prime}$
of $b_{s}$ such that:

  1. (1)

Either $b^{\prime}$ is not of the form $\mathsf{var}(x)$: the path
$\pi^{\prime}$ stops inside $b_{s}$ before reaching a node $\mathsf{var}(x)$.
In this case $b^{\prime}$ is a “new node” of $b_{s}$ – in particular, we know
that expansion generated at least one new node, otherwise we would have
$b_{s}=\mathsf{var}(\\_)$. On have $\pi_{s}=\emptyset$ by definition of
$\mathsf{split\\_join}\left({\\_},\ {\\_}\right)$, and we additionally define
$\pi_{o}$ as $\emptyset$: there is no path to a corresponding “old node” in
$b$.

  2. (2)

Or the path $\pi^{\prime}$ reaches a node
$b_{s}^{\prime}=\mathsf{var}(b^{\prime\prime})$ of $b_{s}$: $\pi_{n}$ is the
path between $b_{s}^{\prime}$ and $b_{s}$, and the rest of $\pi^{\prime}$ is a
path $b^{\prime}\mathrel{\in_{\pi_{s}}}b^{\prime\prime}$, possibly empty,
reaching a strict sub-tree $b^{\prime\prime}$ of $b$. We then define $\pi_{o}$
as the path of $b^{\prime\prime}$ in $b$, non-empty as $b^{\prime\prime}$ is a
strict sub-tree of $b$. strict.

We will come back to this distinction between those two cases (1) and (2) in
the rest of the proof.

We shall now conclude the proof by finding a sub-tree of $a$ under $\pi_{b}$
(thus inside $b$) whose measure is strictly larger than the measure of our
sub-tree $b^{\prime}$ of path $\pi_{s}.\pi_{n}.\pi_{b}$ inside $a^{\prime}$.

##### Larger path

Our candidate sub-tree, that we name $b^{\prime}_{v}$, is at the path
$\pi_{s}.\pi_{o}.\pi_{b}$ in $a$.

##### Case (1)

In the case (1) above ($\pi_{s}=\pi_{o}=\emptyset$), $b^{\prime}$ is a new
node, and $b^{\prime}_{o}$ is the sub-tree at path
$\emptyset.\emptyset.\pi_{b}$, that is $\pi_{b}$: the node $b^{\prime}_{o}$ is
exactly $b$. We have to show
$m_{\mathsf{Node}(a)}(b)>m_{\mathsf{Node}(a^{\prime})}(b^{\prime})$.

$\displaystyle\begin{array}[]{l}m_{\mathsf{Node}(a)}(b^{\prime}_{o})\\\
=m_{\mathsf{Node}(a)}(b)\\\
=m_{\mathsf{Path}(a)}(\pi_{b})+\\{\mskip-5.0mu\\{{}m_{\mathcal{N}}(\mathsf{constr}(b))\\}\mskip-5.0mu\\}{}\\\\[10.00002pt]
\end{array}\penalty 50\hskip 20.00003pt plus 0.5fil minus 5.0pt~{}\penalty
50\hskip 20.00003pt plus 0.5fil minus
5.0pt\begin{array}[]{l}m_{\mathsf{Node}(a^{\prime})}(b^{\prime})\\\
=m_{\mathsf{Path}(a^{\prime})}(\pi_{n}.\pi_{b})+\\{\mskip-5.0mu\\{{}m_{\mathcal{N}}(\mathsf{constr}(b^{\prime}))\\}\mskip-5.0mu\\}{}\\\
=m_{\mathsf{Path}(\mathsf{join}(b_{s}))}(\pi_{n})+m_{\mathsf{Path}(a^{\prime})}(\pi_{b})+\\{\mskip-5.0mu\\{{}m_{\mathcal{N}}(\mathsf{constr}(b^{\prime}))\\}\mskip-5.0mu\\}{}\\\
=m_{\mathsf{Path}(\mathsf{join}(b_{s}))}(\pi_{n})+m_{\mathsf{Path}(a)}(\pi_{b})+\\{\mskip-5.0mu\\{{}m_{\mathcal{N}}(\mathsf{constr}(b^{\prime}))\\}\mskip-5.0mu\\}{}\end{array}$

The expansion from $a$ to $a^{\prime}$ is measured, so we have
$m_{\mathcal{N}}(\mathsf{constr}(b))>m_{\mathcal{N}}(\mathsf{constr}(b^{\prime}))$,
which concludes the proof in this case.

##### Case (2)

In the case (2) above, $b^{\prime}$ is a sub-tree of $b^{\prime\prime}$, a
strict sub-tree of $b$ copied by the expansion generated by $b_{s}$. $\pi_{s}$
is the path of $b^{\prime}$ inside $b^{\prime\prime}$, and $\pi_{o}$ is the
(non-empty) path of $b^{\prime\prime}$ inside $b$. We have:

$\displaystyle\begin{array}[]{ccccccccc}m_{\mathsf{Node}(a)}(b^{\prime}_{o})&=&m_{\mathsf{Path}(a)}(\pi_{b})&+&m_{\mathsf{Path}(b)}(\pi_{o})&+&m_{\mathsf{Path}(b^{\prime\prime})}(\pi_{s})&+&m_{\mathcal{N}}(b^{\prime}_{o})\\\\[6.00006pt]
\penalty 50\hskip 20.00003pt plus 0.5fil minus
5.0pt&&(=)&&&&(=)&&(=)\\\\[6.00006pt] \penalty 50\hskip 20.00003pt plus 0.5fil
minus
5.0ptm_{\mathsf{Node}(a^{\prime})}(b^{\prime})&=&m_{\mathsf{Path}(a^{\prime})}(\pi_{b})&+&m_{\mathsf{Path}(b_{s})}(\pi_{n})&+&m_{\mathsf{Path}(b^{\prime\prime})}(\pi_{s})&+&m_{\mathcal{N}}(b^{\prime})\\\
\end{array}$

To conclude we have to show
$m_{\mathsf{Path}(b)}(\pi_{o})>m_{\mathsf{Path}(b_{s})}(\pi_{n})$. This is
true because $\pi_{o}$ is non-empty, so $m_{\mathsf{Path}(b)}(\pi_{o})$ is a
sum that contains in particular the measure of its root $m_{\mathcal{N}}(b)$,
which is strictly larger than the measure of all the nodes of $b_{s}$ as the
expansion is measured. ∎

###### Corollary A.15.

Annotated reduction is strongly normalizing.

We have proved that our on-the-fly termination checking strategy is _sound_ ,
in the sense that it does enforce termination: each reduction sequence
terminates in a finite number of step, either because it reaches a normal form
(also normal as an un-annotated term), or because it is blocked with all
reducible position trying to reduce a function already in the trace.

###  A.4. On-the-fly termination: completeness

In this section we establish _completeness_ of our on-the-fly termination
checking strategy, in the sense that it does not prevent any normalizing term
from reaching its normal form.

###### Theorem A.16 (Weak completeness).

If a reachable annotated program
$\mathtt{let}~{}\mathtt{rec}~{}D~{}\mathtt{in}~{}\bar{t}$ contains a blocked
redex ${f(({\bar{t}^{\prime}_{i}})^{i})}\mathrel{@}{l}$ with $f\in l$, then
its unannotated erasure $\left\lfloor\bar{t}\right\rfloor$ admits an infinite
reduction sequence.

###### Proof.

To make notations lighter, we will assume that $f$ takes a single argument.
This does not change the proof argument in the least.

Our proof proceed in three steps.

  1. (1)

We work backwards from the blocked redex $f(t^{\prime})$ with a trace of the
form $l_{1},f,l_{2}$, we rewind the trace, to exhibit a previous redex $f(u)$
with trace $l_{1}$ that reduces in at least one step to our term
$C^{\prime}[f(t^{\prime})]$:

$\displaystyle f(u)\leadsto t_{f}{\left[x\leftarrow
u\right]}^{@l,f}\leadsto^{\star}C^{\prime}[f(t^{\prime})]$

At this point we can erase the trace annotations and consider the
corresponding unannotated reduction sequence.

  2. (2)

We _generalize_ this reduction sequence to a valid, non-empty reduction
sequence that does not depend on $u$, with instead a fresh variable $x$:

$\displaystyle f(x)\leadsto
t_{f}\leadsto^{+}C^{\prime\prime}[f(t^{\prime\prime})]$

  3. (3)

At this point we can build an infinite reduction on unannotated terms by
repeating this generalized reduction sequence inside its own conclusion:

$\displaystyle f\left\lfloor
t^{\prime}\right\rfloor\leadsto^{+}C^{\prime\prime}\left[f(t^{\prime\prime})\right]{\left[x\leftarrow
t^{\prime}\right]}\leadsto^{+}C^{\prime\prime}\left[C^{\prime\prime}\left[f(t^{\prime\prime})\right]{\left[x\leftarrow
t^{\prime\prime}\right]}\right]{\left[x\leftarrow
t^{\prime}\right]}\leadsto^{\infty}\dots$

##### Step 1: rewinding the trace

We have a blocked redex of the form
${f(t^{\prime})}\mathrel{@}{(l_{1},f,l_{2})}$ that is reachable, that is
(Definition 6.2), that appears a reduction sequence starting from a term
$t{\left[\emptyset\right]}^{@\emptyset}$ with empty traces – we consider the
recursive environment $D$ fixed once and for all in this proof.

We claim that if a reachable term $\bar{t}$ has a trace of the form
$l,f^{\prime}$ for some function call $f^{\prime}$ (let us assume $f^{\prime}$
unary again for simplicity), then it necessarily arises from the reduction of
a call of the function $f^{\prime}$, followed possibly by some further
reduction steps. More precisely, there exists a non-empty reduction sequence:

$\displaystyle{f^{\prime}(u)}\mathrel{@}{l}\leadsto
t_{f^{\prime}}{\left[x\leftarrow
u\right]}^{@l,f^{\prime}}\leadsto^{\star}C[\bar{t}]$

We show this by induction on the reduction sequence reaching $\bar{t}$ (which
must be non-empty as it has a non-empty trace), doing a case analysis on the
reductions that can result in a term of the form
$C[{\bar{t}}\mathrel{@}{(l,f^{\prime})}]$:

  * •

If the last reduction was precisely the call to $f^{\prime}$ whose expansion
generated $\bar{t}$, we are done.

  * •

If the last reduction occurred in a strict subterm of $\bar{t}$, then its
source term $\bar{t}^{\prime}$ also has trace $l,f^{\prime}$; we use our
induction hypothesis to get a reduction from a ${f^{\prime}(u)}\mathrel{@}{l}$
to $C[\bar{t}^{\prime}]$ and complete with the last reduction step.

  * •

If the last reduction step occurred in the context outside $\bar{t}$ without
touching $\bar{t}$, we forget it and apply the induction hypothesis on the
strictly smaller (but still non-empty) reachable sequence.

  * •

Finally, if the last reduction step substituted $\bar{t}$ (unchanged) from a
different position in the term, our induction hypothesis immediately gives us
a suitable reduction sequence reaching this earlier occurrence of $\bar{t}$,
and we are done.

Now that we know how to rewind the last element from the trace, we can iterate
this process on the trace $l_{1},f,l_{2}$ of our blocked redex
$f(t^{\prime})$, once per element of $l_{2}$ and once for $f$. We thus get a
non-empty, $f$-repeating reduction sequence

$\displaystyle{f(u)}\mathrel{@}{l_{1}}\leadsto t_{f}{\left[x\leftarrow
u\right]}^{@l_{1},f}\leadsto^{\star}C^{\prime}[{f(t^{\prime})}\mathrel{@}{(l_{1},f,l_{2})}]$

##### Let us drop the annotations now

We crucially used our trace annotations to build this $f$-repeating reduction
sequence. In the rest of the proof we will not use the annotations anymore, so
we move to the lighter world on unannotated terms: we redefine

$\displaystyle u\stackrel{{\scriptstyle\small{\mathsf{def}}}}{{=}}\left\lfloor
u\right\rfloor\penalty 50\hskip 20.00003pt plus 0.5fil minus
5.0ptC^{\prime}\stackrel{{\scriptstyle\small{\mathsf{def}}}}{{=}}\left\lfloor
C^{\prime}\right\rfloor\penalty 50\hskip 20.00003pt plus 0.5fil minus
5.0ptt^{\prime}\stackrel{{\scriptstyle\small{\mathsf{def}}}}{{=}}\left\lfloor
t^{\prime}\right\rfloor$

and consider an unannotated, non-empty, $f$-repeating reduction sequence:

$\displaystyle f(u)\leadsto t_{f}{\left[x\leftarrow
u\right]}\leadsto^{\star}C^{\prime}[f(t^{\prime})]$

##### Step 2: generalizing the $f$-repeating sequence

We claim that our $f$-repeating reduction sequence (now unannotated) starting
in $f(u)$ can be generalized in a sequence starting in $f(x)$ for any fresh
variable $x$.

This proof step relies on the first-order restriction on our
$\lambda$-calculus: this works easily because substitution $u$ inside the body
of $f$ cannot create new redexes. After the substitution, we can reduce
redexes in copies of $u$ (if any), or reduce redexes already present in the
body of $f$ (possibly with a variable $x$ now replaced by $u$), but
substituting $u$ does not make new function calls possible.

In consequence, we can systematically replace $u$ by a fresh variable $x$ in
our reduction sequence, dropping any reduction step that is internal to $u$.
Notice that the first step in our sequence

$\displaystyle f(u)\leadsto t_{f}{\left[x\leftarrow
u\right]}\leadsto^{\star}C^{\prime}[f(t^{\prime})]$

is _not_ internal to $u$, so we know that it remains in the filtered reduction
sequence – we need it non-empty. Modulo $\alpha$-renaming we will assume that
our fresh variable $x$ is also the name of the bound variable in the
declaration of $f$. We get a filtered sequence of the form:

$\displaystyle f(x)\leadsto
t_{f}\leadsto^{\star}C^{\prime\prime}[f(t^{\prime\prime})]$

##### Step 3: profit

Our generalized $f$-repeating reduction sequence starts from $f(x)$ for a
fresh variable $x$ and, in at least one step, reduces to a term that contains
a call to $f$ again. We can immediately build an infinite reduction sequence
by repeatedly composing our generalized sequence with itself. ∎

What we have shown so far is that blocked redexes could generate infinite
reduction sequences. But our reduction is non-deterministic, so some terms
have both terminating and non-terminating reduction sequences – they are
normalizing but not strongly normalizing. Using standard(ization) results on
the $\lambda$-calculus we believe that we can get a stronger completeness
result – the proof below is a bit sketchy, so we degraded our claim from
Theorem to Conjecture.

###### Conjecture A.17 (Strong completeness).

If an annotated program
$\mathtt{let}~{}\mathtt{rec}~{}D~{}\mathtt{in}~{}\bar{t}$ has a weakly
normalizing erasure, that is, if $\left\lfloor t\right\rfloor$ has _some_
reduction path to a normal form, then $\bar{t}$ has an annotated reduction
sequence to a (non-blocked) $\beta$-normal form.

###### Proof.

A standard fact about the $\lambda$-calculus, which applies to our setting, is
that the leftmost-outermost reduction strategy is minimally diverging, in
particular it reaches the normal forms of any weakly normalizing term.

Our argument relies on studying the annotated leftmost-outermost reduction
sequence of the annotated term $\bar{t}$ (under the definitions $D$). If this
reduction sequence does not reach a blocked redex in leftmost-outermost
position, we are done: it reaches a $\beta$-normal form of
$\left\lfloor\bar{t}\right\rfloor$.

We now argue that $\bar{t}$ _cannot_ reach a blocked redex by following the
leftmost-outermost strategy. If $\bar{t}$ could reach a blocked redex, then
the proof of the previous theorem would provide an infinite reduction sequence
from that point. This infinite reduction sequence is obtained by repeating a
suffix of the reduction sequence to this block redex, which follows the
leftmost-outermost strategy. In consequence, the infinite reduction sequence
is itself a leftmost-outermost sequence. This is in contradiction with the
assumption that $\left\lfloor t\right\rfloor$ is weakly normalizing. ∎

Finally, it is interesting to study how those proofs break down when we move
from our first-order calculus its closed-higher-order extension presented in
Section 7.4. In that section, we show that completeness does not hold in the
closed-higher-order fragment, with the following counterexample:

⬇

let rec f(p,q) = p(f(q,q))

and id(x) = x

and stop(x) = done

in f(id, stop) (* $\rewto$ id(f(stop,stop)) $\rewto$ f(stop,stop)

$\rewto$ stop(f(stop,stop)) $\rewto$ done *)

The first blocked redex in this reduction sequence is the application of f in
the second term id(f(stop,stop)) of the sequence. Using the reasoning of our
proof of weak completeness, we can “generalize” the $f$-repeating sequence to
a sequence of the form f(k,stop) $\leadsto$ k(f(stop,stop)) for any k, whose
instantiations can be repeated into an infinite reduction sequence:

⬇

f(id,stop) $\rewto$ id(f(stop,stop)) $\rewto$ id(stop(f(stop,stop))) $\rewto$
id(stop(stop(…)))

On the other hand, this first occurrence of a blocked redex is _not_ in head
position for the leftmost-outermost reduction strategy, so our proof of the
strong completeness theorem does not applies.

Another blocked redex does appear in head position in the third term of the
reduction sequence, f(stop,stop). But then the reasoning of our proof of weak
completeness cannot be applied anymore: the reduction sequence

⬇

f(id,stop) $\rewto$ id(f(stop,stop)) $\rewto$ f(stop,stop)

crucially uses a parameter of f to create a new redex, and this sequence
cannot be generalized by replacing id by an arbitrary parameter k.

###  A.5. Proof of correctness for the closed-higher-order fragment

This is a proof missing from 7.4.

###### Theorem 0.

Our termination-monitoring algorithm remains correct for this closed-higher-
order language: the annotated language is strongly normalizing.

###### Proof.

The proof uses the same machinery as the first-order proof – see Appendix A.
We translate our terms to trees with measured expansions. We can then
immediately reuse our result that measured expansions are strongly
normalizing.

Let us recall the translation of our higher-order terms into trees (Example
A.6):

$\displaystyle\mathcal{T}\ni
c\mathrel{::=}\;x\;\mathrel{|}\;{f}\mathrel{@}{l}\penalty-10000\hskip
20.00003pt plus 0.5fil minus
5.0pt\mathsf{tree}(x)\stackrel{{\scriptstyle\small{\mathsf{def}}}}{{=}}\mathsf{node}(x,\,\emptyset)\penalty
50\hskip 20.00003pt plus 0.5fil minus
5.0pt\mathsf{tree}({f{({\bar{t}_{i}})^{i}}}\mathrel{@}{l})\stackrel{{\scriptstyle\small{\mathsf{def}}}}{{=}}\mathsf{node}({f}\mathrel{@}{l},\,({\mathsf{tree}(\bar{t}_{i})})^{i})$

This translation would use the function name $f$ directly as the node
constructor for an application node.

We now use an explicit $\mathsf{app}$ constructor for application nodes, as
the function name is not known at this point. The function term $t$ becomes
the first child of the application node;

$\displaystyle\mathcal{T}\ni
c\mathrel{::=}\;x\;\mathrel{|}\;f\;\mathrel{|}\;{\mathsf{app}}\mathrel{@}{l}\penalty-10000\hskip
20.00003pt plus 0.5fil minus
5.0pt\mathsf{tree}(x)\stackrel{{\scriptstyle\small{\mathsf{def}}}}{{=}}\mathsf{node}(x,\,\emptyset)\penalty
50\hskip 20.00003pt plus 0.5fil minus
5.0pt\mathsf{tree}(f)\stackrel{{\scriptstyle\small{\mathsf{def}}}}{{=}}\mathsf{node}(f,\,\emptyset)\penalty
50\hskip 20.00003pt plus 0.5fil minus
5.0pt\mathsf{tree}({t{({\bar{u}_{i}})^{i}}}\mathrel{@}{l})\stackrel{{\scriptstyle\small{\mathsf{def}}}}{{=}}\mathsf{node}({\mathsf{app}}\mathrel{@}{l},\,t::({\mathsf{tree}(\bar{u}_{i})})^{i})$

To conclude the proof we only have to remark that reductions of our closed-
higher-order terms become measured expansions of the corresponding trees,
extending Lemma A.13 to the closed-higher-order case. For each
$f(({x_{i}})^{i})=t^{\prime}$ in the ambient set of recursive definitions $D$,
we have tree expansions of the form

$\displaystyle\mathsf{node}({\mathsf{app}}\mathrel{@}{l},\,\mathsf{node}(f,\,\emptyset)::({a_{i}})^{i})\leadsto\mathsf{tree}(t^{\prime}{\left[\emptyset\right]}^{@l,f}){\left[({x_{i}\leftarrow
a_{i}})^{i}\right]}$

If $t^{\prime}$ is a variable, then this reduces to a strict sub-tree, one of
the arguments $a_{i}$. If $t^{\prime}$ is a function name $f$, this reduces to
a leaf node. Otherwise $t^{\prime}$ starts with an application node, which
gets annotated with the strictly larger trace $l,f$ in the resulting tree. In
all three cases, this is a measured tree expansion. ∎

##  Appendix B More on cpp

###  B.1. Relating our algorithm to Dave Prosser’s pseudo-code

The pseudo-code defines two mutually-recursive functions, expand which
computes the macro expansion of a full token list, and subst which expands a
single macro call. Let us quote the pseudo-code, slightly simplified, with all
parts related to irrelevant cpp features (stringization, concatenation)
elided:

⬇

expand(TS)

{

if TS is {} then

return {};

else if TS is T^HS $\cdot$ TS’ and T is in HS then

return T^HS $\cdot$ expand(TS’);

else if TS is T^HS $\cdot$ ( $\cdot$ TS’ and T is a function-like macro then

check TS’ is Actuals $\cdot$ )^HS’ $\cdot$ TS” and actuals are correct for T,

return expand(subst(ts(T), fp(T), Actuals, (HS $\cap$ HS’) $\uplus$ {T}, {})
$\cdot$ TS”);

else TS must be T^HS $\cdot$ TS’

return T^HS $\cdot$ expand(TS’);

}

expand(TS) processes a token sequence TS by expanding macro invocations. (TS
$\cdot$ TS’ is concatenation of token sequences.) The tokens T^HS of the
sequence are raw tokens T annotated with a “hide set” HS, which is a set of
macro names. Hide sets HS correspond to our traces $l$, and token sequences TS
to our annotated terms $\bar{t}$.

In the definition of expand, an annotated macro name T^HS is _not_ expanded if
its name occurs in its own trace. This corresponds to our blocked redexes. If
$T$ is not blocked by the hide set, then the function subst is called to
perform a $\beta$-reduction that also expands the macro parameters, and
expansion is rerun on the result. ts(T) is the code/body of the macro T, fp(T)
is an array of formal parameters, Actuals an array of actual parameters, the
hide set of the invocation adds T as expected. It computes an intersection of
HS and HS’ instead of just using HS; this only matters in the closed-higher-
order case, which we discuss in another section.

⬇

subst(IS, FP, AP, HS, OS)

{

if IS is {} then

return hsadd(HS, OS);

else if IS is T $\cdot$ IS’ and T is FP[i] then

return subst(IS’, FP, AP, HS, OS $\cdot$ expand(AP[i]));

else IS must be T^HS’ $\cdot$ IS’

return subst(IS’, FP, AP, HS, OS $\cdot$ T^HS’);

}

The function subst(IS, FP, AP, HS, OS) computes a single macro invocation by
processing the token sequence IS coming from the function body, replacing the
formal parameters from FP by the expansion of the actual parameters AP, with
hide set HS; it appends its results to the accumulator token sequence OS –
which is annotated with hide sets.

In the definition of subst, formal parameters found in the macro body are
replaced by the recursive expansion of the actual parameters. Note that the
name T of the macro being expanded was not added to the hide set of the actual
parameters. After the whole macro body IS has been traversed, we call the
auxiliary function hsadd on the output accumulator OS; this function arguments
the hide set of all tokens of OS by the invocation-site hide set HS.

(Note: we are not sure why IS is taken to be annotated with hide sets, while
it comes from a macro definition that should not be the result of any
expansion yet. As far as we can tell HS’ should always be empty in this
function, and this is the behavior of Spinellis’ CSout (Spinellis, 2003)
implementation.)

This subst function is related to our annotated substitution
$t{\left[\sigma\right]}^{@l}$, but not exactly the same: our definition only
uses the trace $l$ for the parts of the term coming from the function body
$t$, not for the substituted parameters in $\sigma$ – which remain unreduced.
In contrast subst adds the hide set HS to all the output, but only _after_
recursively expanding the actual parameters. In our algorithm this would
correspond to first reducing the arguments in $\sigma$ to a normal form, and
then extending their trace with $l$.

###  B.2. Relating the algorithms on the first-order fragment

For a precise comparison, here is our own rule for function calls, and a big-
step presentation of Dave Prosser’s algorithm:

our-rule $\displaystyle\displaystyle{\hbox{\hskip
54.89783pt\vbox{\hbox{\hskip-54.89781pt\hbox{\hbox{$\displaystyle\displaystyle(f{({x_{i}})^{i}}=t^{\prime})\in
D$}\hskip 20.00003pt\hbox{\hbox{$\displaystyle\displaystyle f\notin
l$}}}}\vbox{}}}\over\hbox{\hskip
118.72928pt\vbox{\vbox{}\hbox{\hskip-118.72926pt\hbox{\hbox{$\displaystyle\displaystyle\mathtt{let}~{}\mathtt{rec}~{}D~{}\mathtt{in}~{}C[{f{({\bar{t}_{i}})^{i}}}\mathrel{@}{l}]\leadsto\mathtt{let}~{}\mathtt{rec}~{}D~{}\mathtt{in}~{}C[t^{\prime}{\left[({x_{i}\leftarrow\bar{t}_{i}})^{i}\right]}^{@l,f}]$}}}}}}$
Prosser-rule $\displaystyle\displaystyle{\hbox{\hskip
176.30005pt\vbox{\hbox{\hskip-176.30005pt\hbox{\hbox{$\displaystyle\displaystyle(f{({x_{i}})^{i}}=t^{\prime})\in
D$}\hskip 20.00003pt\hbox{\hbox{$\displaystyle\displaystyle f\notin l$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\forall
i,\bar{t}_{i}\Downarrow_{D}\bar{u}_{i}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle
t^{\prime\prime}\stackrel{{\scriptstyle\small{\mathsf{def}}}}{{=}}(t^{\prime}{\left[({x_{i}\leftarrow\bar{u}_{i}})^{i}\right]}^{@\emptyset})^{l^{\prime}\mapsto
l^{\prime}\cup l,f}$}\hskip 20.00003pt\hbox{\hbox{$\displaystyle\displaystyle
C[t^{\prime\prime}]\Downarrow_{D}u^{\prime}$}}}}}}}\vbox{}}}\over\hbox{\hskip
33.96518pt\vbox{\vbox{}\hbox{\hskip-33.96516pt\hbox{\hbox{$\displaystyle\displaystyle
C[{f{({\bar{t}_{i}})^{i}}}\mathrel{@}{l}]\Downarrow_{D}u^{\prime}$}}}}}}$

In the definition of $t^{\prime\prime}$ we use a notation
${\bar{t}}^{l^{\prime}\mapsto\dots}$, which we mean as a map over the
annotations of $\bar{t}$, transforming the trace $l^{\prime}$ of each
syntactic node into another trace.

We claim that the two approaches give the same results on our first-order
calculus, or equivalently on the first-order macro fragment: the erasure of
the normal forms on both side are the same. Let us review the two differences
between the two rules:

  * •

The normalization of the $\bar{t}_{i}$ into $\bar{u}_{i}$ at substitution time
in Prosser’s rule corresponds to a call-by-value reduction strategy. Our
small-step reduction can model any reduction strategy, but it eventually
computes the same normal forms.

  * •

As we discussed, the evolution of traces differ: Prosser’s rule adds the
current trace $l,f$ to all the nodes of the substitution
$t^{\prime}{\left[({x_{i}\leftarrow\bar{u}_{i}})^{i}\right]}$, while we only
use it for the unannotated syntactic nodes coming from $t^{\prime}$. The
annotations on the nodes of $u_{i}$ thus differ in the final result – this is
the only difference. But this does not change the reduction dynamics, given
that the $u_{i}$ are already in normal form: no further reduction happens in
them, so in particular there are not more blocked redexes. After erasure we
get the same results.

###  B.3. Expanding closed-higher-order macros

Dave Prosser’s algorithm uses as hide set for a function call T(Actuals) the
intersection of the hide set HS of the function-macro symbol T and the hide
set HS’ of the closing parenthesis.

In the first-order case, those two hide-sets are always the same: each
syntactic occurrence of T in the source is followed by the closing
parenthesis, so their hide sets evolve in the exact same way during expansion.

This is not the case anymore on higher-order examples. Consider our NIL
example:

⬇

#define NIL(xxx) xxx

#define G_0(arg) NIL(G_1)(arg)

#define G_1(arg) NIL(arg)

G_0(42) // ~> NIL(G_1)(42) ~> G_1(42) ~> NIL(42) ~> 42

In the NIL reduction sequence, the third term is G_1(42); at this point the
hide set of G_1 contains G_0 and NIL, but the hide set of the closing
parenthesis contains only G_0. So the function call is expanded in the
intersected hide set G_0, and the occurrence of NIL that it creates can be
reduced. (C programmers were complaining to the C standard bodies about
implementations that would only consider the hide set of the function token,
and thus refuse to reduce NIL(42) further.)

Note that G_1 has the hide set G_0, NIL because this occurrence was created by
the expansion of G_0, and then taken as parameter and returned by the macro
NIL. With our own algorithm, we would only have G_0 in the trace at this
point, as we do not change the trace of parameters when expanding a function
application. In other words, the NIL comes from the call to hsadd on both the
function body and the parameters, and the hide-set intersection can be
presented as compensating this extension of the parameter hide sets – which we
have shown is unnecessary in the first-order case.