18323 LABEL:LastPageDec. 01, 2020Aug. 17, 2022

# Strongly Normalizing Higher-Order Relational Queries

Wilmer Ricciotti0000-0002-2361-8538  and  James Cheney0000-0002-1307-9286
Laboratory for Foundations of Computer Science, University of Edinburgh,
United Kingdom and The Alan Turing Institute, London, United Kingdom
<EMAIL_ADDRESS><EMAIL_ADDRESS>
###### Abstract.

Language-integrated query is a powerful programming construct allowing
database queries and ordinary program code to interoperate seamlessly and
safely. Language-integrated query techniques rely on classical results about
the nested relational calculus, stating that its queries can be
algorithmically translated to SQL, as long as their result type is a flat
relation. Cooper and others advocated _higher-order_ nested relational calculi
as a basis for language-integrated queries in functional languages such as
Links and F#. However, the translation of higher-order relational queries to
SQL relies on a rewrite system for which no _strong normalization_ proof has
been published: a previous proof attempt does not deal correctly with rewrite
rules that duplicate subterms. This paper fills the gap in the literature,
explaining the difficulty with a previous proof attempt, and showing how to
extend the _$\top\top$ -lifting_ approach of Lindley and Stark to accommodate
duplicating rewrites. We also show how to extend the proof to a recently-
introduced calculus for _heterogeneous_ queries mixing set and multiset
semantics.

###### Key words and phrases:

Strong normalization, $\top\top$-lifting, Nested relational calculus,
Language-integrated query

##  1\. Introduction

The Nested Relational Calculus ($\mathit{NRC}$) [BNTW95] provides a principled
foundation for integrating database queries into programming languages. Wong’s
conservativity theorem [Won96] generalized the classic flat-flat theorem
[PG92] to show that for any nesting depth $d$, a query expression over flat
input tables returning collections of depth at most $d$ can be expressed
without constructing intermediate results of nesting depth greater than $d$.
In the special case $d=1$, this implies the flat-flat theorem, namely that a
nested relational query mapping flat tables to flat tables can be expressed in
a semantically equivalent way using the flat relational calculus. In addition,
Wong’s proof technique was constructive, and gave an easily-implemented
terminating rewriting algorithm for normalizing NRC queries to flat relational
queries, which can in turn be easily translated to idiomatic SQL queries. The
basic approach has been extended in a number of directions, including to allow
for (nonrecursive) higher-order functions in queries [Coo09b], and to allow
for translating queries that return nested results to a bounded number of flat
relational queries [CLW14].

Normalization-based techniques are used in language-integrated query systems
such as Kleisli [Won00] and Links [CLWY07], and can improve both performance
and reliability of language-integrated query in F# [CLW13]. However, most work
on normalization considers _homogeneous_ queries in which there is a single
collection type (e.g. homogeneous sets or multisets). Currently, language-
integrated query systems such as C# and F# [MBB06] support duplicate
elimination via a $\mathtt{Distinct()}$ method, which is translated to SQL
queries in an ad hoc way, and comes with no guarantees regarding completeness
or expressiveness as far as we know, whereas Database-Supported Haskell (DSH)
[UG15] supports duplicate elimination but gives all operations list semantics
and relies on more sophisticated SQL:1999 features to accomplish this. Fegaras
and Maier [FM00] propose optimization rules for a nested object-relational
calculus with set and bag constructs but do not consider the problem of
conservativity with respect to flat queries.

Recently, we considered a _heterogeneous_ calculus for mixed set and bag
queries [RC19], and conjectured that it too satisfies strong normalization and
conservativity theorems. However, in attempting to extend Cooper’s proof of
normalization we discovered a subtle problem, which makes the original proof
incomplete.

Most techniques to prove the strong normalization property for higher-order
languages employ logical relations; among these, the Girard-Tait
_reducibility_ relation is particularly influential: reducibility interprets
types as certain sets of strongly normalizing terms enjoying desirable closure
properties with respect to reduction, called _candidates of reducibility_
[GLT89]. The fundamental theorem then proves that every well-typed term is
reducible, hence also strongly normalizing. In its traditional form,
reducibility has a limitation that makes it difficult to apply it to certain
calculi: the elimination form of every type is expected to be a _neutral_ term
or, informally, an expression that, when placed in an arbitrary evaluation
context, does not interact with it by creating new redexes. However, some
calculi possess _commuting conversions_ , i.e. reduction rules that apply to
nested elimination forms: such rules usually arise when the elimination form
for a type (say, pairs) is constructed by means of an auxiliary term of any
arbitrary, unrelated type. In this case, we expect nested elimination forms to
commute; for example, we could have the following commuting conversion
hoisting the elimination of pairs out of case analysis on disjoint unions:

$\begin{array}[]{l}\mathbf{cases}~{}(\mathbf{let}~{}(a,b)=p~{}\mathbf{in}~{}t)~{}\mathbf{of}~{}\mathbf{inl}(x)\Rightarrow
u;\mathbf{inr}(y)\Rightarrow v\\\
\mathrel{\leadsto}\mathbf{let}~{}(a,b)=p~{}\mathbf{in}~{}\mathbf{cases}~{}t~{}\mathbf{of}~{}\mathbf{inl}(x)\Rightarrow
u;\mathbf{inr}(y)\Rightarrow v\end{array}$

where $p$ has type $A\times B$, $t$ has type $C+D$, $u,v$ have type $U$, and
the bound variables $a,b$ are chosen fresh for $u$ and $v$. Since in the
presence of commuting conversions elimination forms are not neutral, a
straightforward adaptation of reducibility to such languages is precluded.

###  1.1. $\top\top$-lifting and $\mathit{NRC}_{\lambda}$

Cooper’s $\mathit{NRC}_{\lambda}$ [Coo09a, Coo09b] extends the simply typed
lambda calculus with collection types whose elimination form is expressed by
_comprehensions_ $\bigcup\mathopen{\textbf{\\{}}{M|x\leftarrow
N}\mathclose{\textbf{\\}}}$, where $M$ and $N$ have a collection type, and the
bound variable $x$ can appear in $M$:

$\Gamma\vdash N:\mathopen{\textbf{\\{}}{S}\mathclose{\textbf{\\}}}$
$\Gamma,x:S\vdash M:\mathopen{\textbf{\\{}}{T}\mathclose{\textbf{\\}}}$
$\Gamma\vdash\bigcup\mathopen{\textbf{\\{}}{M|x\leftarrow
N}\mathclose{\textbf{\\}}}:\mathopen{\textbf{\\{}}{T}\mathclose{\textbf{\\}}}$

(we use bold-style braces
$\mathopen{\textbf{\\{}}{\cdot}\mathclose{\textbf{\\}}}$ to indicate
collections as expressions or types of $\mathit{NRC}_{\lambda}$). In the rule
above, we typecheck a comprehension destructuring collections of type
$\mathopen{\textbf{\\{}}{S}\mathclose{\textbf{\\}}}$ to produce new
collections in $\mathopen{\textbf{\\{}}{T}\mathclose{\textbf{\\}}}$, where $T$
is an unrelated type: semantically, this corresponds to the union of all the
collections $M\left[{V}\middle/{x}\right]$, such that $V$ is in $N$. According
to the standard approach, we should attempt to define the reducibility
predicate for the collection type
$\mathopen{\textbf{\\{}}{S}\mathclose{\textbf{\\}}}$ as:

$\mathsf{Red}_{\mathopen{\textbf{\\{}}{S}\mathclose{\textbf{\\}}}}\triangleq\\{{N:\forall
x,T,\forall
M\in\mathsf{Red}_{\mathopen{\textbf{\\{}}{T}\mathclose{\textbf{\\}}}},\bigcup\mathopen{\textbf{\\{}}{M|x\leftarrow
N}\mathclose{\textbf{\\}}}\in\mathsf{Red}_{\mathopen{\textbf{\\{}}{T}\mathclose{\textbf{\\}}}}}\\}$

(we use roman-style braces $\\{{\cdot}\\}$ to express metalinguistic sets). Of
course the definition above is circular, since it uses reducibility over
collections to express reducibility over collections; however, this
inconvenience could in principle be circumvented by means of impredicativity,
replacing $\mathsf{Red}_{\mathopen{\textbf{\\{}}{T}\mathclose{\textbf{\\}}}}$
with a suitable, universally quantified candidate of reducibility (an approach
we used in [RC17] in the context of justification logic). Unfortunately, the
arbitrary return type of comprehensions is not the only problem: they are also
involved in commuting conversions, such as:

$\bigcup\mathopen{\textbf{\\{}}{M|x\leftarrow\bigcup\mathopen{\textbf{\\{}}{N|y\leftarrow
P}\mathclose{\textbf{\\}}}}\mathclose{\textbf{\\}}}\mathrel{\leadsto}\bigcup\mathopen{\textbf{\\{}}{\bigcup\mathopen{\textbf{\\{}}{M|x\leftarrow
N}\mathclose{\textbf{\\}}}|y\leftarrow
P}\mathclose{\textbf{\\}}}\qquad(y\notin FV(M))$

Because of this rule, comprehensions are not neutral terms, thus we cannot use
the closure properties of candidates of reducibility (in particular,
$\mathrm{CR3}$ [GLT89]) to prove that a collection term is reducible. To
address this problem, Lindley and Stark proposed a revised notion of
reducibility based on a technique they called $\top\top$-lifting [LS05].
$\top\top$-lifting, which derives from Pitts’s related notion of
$\top\top$-closure [Pit98], involves quantification over arbitrarily nested,
reducible elimination contexts (_continuations_); the technique is actually
composed of two steps: $\top$-lifting, used to define the set
$\mathsf{Red}_{T}^{\top}$ of reducible continuations for collections of type
$T$ in terms of $\mathsf{Red}_{T}$, and $\top\top$-lifting proper, defining
$\mathsf{Red}_{\mathopen{\textbf{\\{}}{T}\mathclose{\textbf{\\}}}}=\mathsf{Red}_{T}^{\top\top}$
in terms of $\mathsf{Red}_{T}^{\top}$. In our setting, if we use
$\mathcal{S}\mathcal{N}$ to denote the set of strongly normalizing terms, the
two operations can be defined as follows:

$\displaystyle\mathsf{Red}_{T}^{\top}$ $\displaystyle\triangleq\\{{K:\forall
M\in\mathsf{Red}_{T},K[\mathopen{\textbf{\\{}}{M}\mathclose{\textbf{\\}}}]\in\mathcal{S}\mathcal{N}}\\}$
$\displaystyle\mathsf{Red}_{T}^{\top\top}$
$\displaystyle\triangleq\\{{M:\forall
K\in\mathsf{Red}_{T}^{\top},K[M]\in\mathcal{S}\mathcal{N}}\\}$

Notice that, in order to avoid a circularity between the definitions of
reducible collection continuations and reducible collections, the former are
defined by lifting a reducible term $M$ of type $T$ to a singleton collection.

In $\mathit{NRC}_{\lambda}$, besides commuting conversions, we come across an
additional problem concerning the property of distributivity of comprehensions
over unions, represented by the following reduction rule:

$\bigcup\mathopen{\textbf{\\{}}{M\mathbin{\cup}N|x\leftarrow
P}\mathclose{\textbf{\\}}}\mathrel{\leadsto}\bigcup\mathopen{\textbf{\\{}}{M|x\leftarrow
P}\mathclose{\textbf{\\}}}\mathbin{\cup}\bigcup\mathopen{\textbf{\\{}}{N|x\leftarrow
P}\mathclose{\textbf{\\}}}$

One can immediately see that in
$\bigcup\mathopen{\textbf{\\{}}{M\mathbin{\cup}N|x\leftarrow\Box}\mathclose{\textbf{\\}}}$
the reduction above duplicates the hole, producing a multi-hole context that
is not a continuation in the Lindley-Stark sense.

Cooper, in his work, attempted to reconcile continuations with duplicating
reductions. While considering extensions to his language, we discovered that
his proof of strong normalization presents a nontrivial lacuna which we could
only fix by relaxing the definition of continuations to allow multiple holes.
This problem affected both the proof of the original result and our attempt to
extend it, and has an avalanche effect on definitions and proofs, yielding a
more radical revision of the $\top\top$-lifting technique which is the subject
of this paper.

The contribution of this paper is to place previous work on higher-order
programming for language-integrated query on a solid foundation. As we will
show, our approach also extends to proving normalization for a higher-order
heterogeneous collection calculus
$\mathit{NRC}_{\lambda}(\mathit{Set},\mathit{Bag})$ [RC19] and we believe our
proof technique can be extended further.

This article is a revised and expanded version of a conference paper [RC20].
Compared with the conference paper, this article refines the notion of
$\top\top$-lifting by omitting a harmless, but unnecessary generalization,
includes details of proofs that had to be left out, and expands the discussion
of related work. In addition, we fully comment on the extension of our result
to a language allowing to freely mix and compose set queries and bag queries,
which was only marginally discussed in the conference version. We also solved
a subtle problem with the treatment of variable capture in contexts by
reformulating the statement of Lemma 9.

###  1.2. Summary

Section 2 reviews $NRC_{\lambda}$ and its rewrite system. Section 3 presents
the refined approach to reducibility needed to handle rewrite rules with
branching continuations. Section 4 presents the proof of strong normalization
for $NRC_{\lambda}$. Section 5 outlines the extension to a higher-order
calculus $\mathit{NRC}_{\lambda}(\mathit{Set},\mathit{Bag})$ providing
heterogeneous set and bag queries. Sections 6 and 7 discuss related work and
conclude.

##  2\. Higher-order NRC

$\mathit{NRC}_{\lambda}$, a nested relational calculus with non-recursive
higher-order functions, is defined by the following grammar:

$\begin{array}[]{lrcl}\textbf{types}&S,T&::=&A\mathbin{~{}|~{}}S\to
T\mathbin{~{}|~{}}\langle{\overrightarrow{\ell:T}}\rangle\mathbin{~{}|~{}}\mathopen{\textbf{\\{}}{T}\mathclose{\textbf{\\}}}\\\
\textbf{terms}&L,M,N&::=&x\mathbin{~{}|~{}}c(\overrightarrow{M})\mathbin{~{}|~{}}\langle{\overrightarrow{\ell=M}}\rangle\mathbin{~{}|~{}}M.\ell\mathbin{~{}|~{}}\lambda
x.M\mathbin{~{}|~{}}(M~{}N)\\\
&&\mathbin{~{}|~{}}&\emptyset\mathbin{~{}|~{}}\mathopen{\textbf{\\{}}{M}\mathclose{\textbf{\\}}}\mathbin{~{}|~{}}M\mathbin{\cup}N\mathbin{~{}|~{}}\bigcup\mathopen{\textbf{\\{}}{M|x\leftarrow
N}\mathclose{\textbf{\\}}}\\\
&&\mathbin{~{}|~{}}&\mathtt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}empty}~{}M\mathbin{~{}|~{}}\mathtt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}where}~{}M~{}\mathtt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}do}~{}N\end{array}$

where $x$, $\ell$ and $c$ range over countably infinite and pairwise disjoint
sets of variables, record field labels, and constants.

Types include atomic types $A,B,\ldots$ (among which we have Booleans
$\mathbf{B}$), record types with named fields
$\langle{\overrightarrow{\ell:T}}\rangle$, collections
$\mathopen{\textbf{\\{}}{T}\mathclose{\textbf{\\}}}$; we define _relation
types_ as those in the form
$\mathopen{\textbf{\\{}}{\langle{\overrightarrow{\ell:A}}\rangle}\mathclose{\textbf{\\}}}$,
i.e. collections of records of atomic types. Terms include applied constants
$c(\overrightarrow{M})$, records with named fields and record projections
($\langle{\ell=M}\rangle$, $M.\ell$), various collection terms (empty,
singleton, union, and comprehension), the emptiness test
$\mathtt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}empty}$,
and one-sided conditional expressions for collection types
$\mathtt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}where}~{}M~{}\mathtt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}do}~{}N$;
we allow the type of records with no fields: consisting of a single, empty
record $\langle{}\rangle$. Notice that $\lambda x.M$ and
$\bigcup\mathopen{\textbf{\\{}}{M\mid x\leftarrow N}\mathclose{\textbf{\\}}}$
bind the variable $x$ in $M$.

We will allow ourselves to use sequences of generators in comprehensions,
which are syntactic sugar for nested comprehensions, e.g.:

$\bigcup\mathopen{\textbf{\\{}}{M|x\leftarrow N,y\leftarrow
R}\mathclose{\textbf{\\}}}\triangleq\bigcup\mathopen{\textbf{\\{}}{\bigcup\mathopen{\textbf{\\{}}{M|y\leftarrow
R}\mathclose{\textbf{\\}}}|x\leftarrow N}\mathclose{\textbf{\\}}}$

The typing rules, shown in Figure 1, are largely standard, and we only mention
those operators that are specific to our language: constants are typed
according to a fixed signature $\Sigma$, prescribing the types of the $n$
arguments and of the returned expression to be atomic; we assume that $\Sigma$
assigns the type $\mathbf{B}$ to the constants ${\mathsf{true}}$ and
${\mathsf{false}}$ (representing the two Boolean values), and the type
$(\mathbf{B},\mathbf{B})\to\mathbf{B}$ to the constant $\land$ (representing
the logical ‘and‘) and we will allow ourselves to write $M\land N$ instead of
$\land(M,N)$. The operation
$\mathtt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}empty}$
takes a collection and returns a Boolean indicating whether its argument is
empty;
$\mathtt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}where}$
takes a Boolean condition and a collection and returns the second argument if
the Boolean is true, otherwise the empty set. (Conventional two-way
conditionals, at any type, are omitted for convenience but can be added
without difficulty.)

$x:T\in\Gamma$ $\Gamma\vdash x:T$ $\Sigma(c)=\overrightarrow{A_{n}}\to
A^{\prime}$ $(\Gamma\vdash M_{i}:A_{i})_{i=1,\ldots,n}$ $\Gamma\vdash
c(\overrightarrow{M_{n}}):A^{\prime}$

$(\Gamma\vdash M_{i}:T_{i})_{i=1,\ldots,n}$
$\Gamma\vdash\langle{\overrightarrow{\ell_{n}=M_{n}}}\rangle:\langle{\overrightarrow{\ell_{n}:T_{n}}}\rangle$
$\Gamma\vdash M:\langle{\overrightarrow{\ell_{n}:T_{n}}}\rangle$
$i\in\\{{1,\ldots,n}\\}$ $\Gamma\vdash M.\ell_{i}:T_{i}$

$\Gamma,x:S\vdash M:T$ $\Gamma\vdash\lambda x.M:S\to T$ $\Gamma\vdash M:S\to
T$ $\Gamma\vdash N:S$ $\Gamma\vdash(M~{}N):T$

$\Gamma\vdash\emptyset:\mathopen{\textbf{\\{}}{T}\mathclose{\textbf{\\}}}$
$\Gamma\vdash M:T$
$\Gamma\vdash\mathopen{\textbf{\\{}}{M}\mathclose{\textbf{\\}}}:\mathopen{\textbf{\\{}}{T}\mathclose{\textbf{\\}}}$
$\Gamma\vdash M:\mathopen{\textbf{\\{}}{T}\mathclose{\textbf{\\}}}$
$\Gamma\vdash N:\mathopen{\textbf{\\{}}{T}\mathclose{\textbf{\\}}}$
$\Gamma\vdash
M\mathbin{\cup}N:\mathopen{\textbf{\\{}}{T}\mathclose{\textbf{\\}}}$

$\Gamma,x:T\vdash M:\mathopen{\textbf{\\{}}{S}\mathclose{\textbf{\\}}}$
$\Gamma\vdash N:\mathopen{\textbf{\\{}}{T}\mathclose{\textbf{\\}}}$
$\Gamma\vdash\bigcup\mathopen{\textbf{\\{}}{M|x\leftarrow
N}\mathclose{\textbf{\\}}}:\mathopen{\textbf{\\{}}{S}\mathclose{\textbf{\\}}}$

$\Gamma\vdash M:\mathopen{\textbf{\\{}}{T}\mathclose{\textbf{\\}}}$
$\Gamma\vdash\mathtt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}empty}~{}M:\mathbf{B}$
$\Gamma\vdash M:\mathbf{B}$ $\Gamma\vdash
N:\mathopen{\textbf{\\{}}{T}\mathclose{\textbf{\\}}}$
$\Gamma\vdash\mathtt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}where}~{}M~{}\mathtt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}do}~{}N:\mathopen{\textbf{\\{}}{T}\mathclose{\textbf{\\}}}$

Figure 1. Type system of $\mathit{NRC}_{\lambda}$.

Overall, our presentation of $\mathit{NRC}_{\lambda}$ is very similar to the
language of queries used by Cooper in [Coo09a]: two minor differences are that
$\mathit{NRC}_{\lambda}$ does not have a specific construct for input tables
(these can be simulated as free variables with relation type) and uses one-
armed conditionals instead of an if-then-else construct. Additionally, Cooper
provided a type-and-effect system to track the use of primitive operations
that may not be translated to SQL; the issue of translating to SQL is not
addressed directly in this paper (equivalently, we may assume that all the
primitive operations of $\mathit{NRC}_{\lambda}$ may be translated to SQL).

###  2.1. Reduction and normalization

$\mathit{NRC}_{\lambda}$ is equipped with a rewrite relation
$\mathrel{\leadsto}$ whose purpose is to convert expressions of relation type
into a sublanguage isomorphic to a fragment of SQL, even when the original
expression contains subterms whose type is not available in SQL, such as
nested collections. This rewrite relation is obtained from the basic
contraction $\mathrel{\breve{\leadsto}}$ shown in Figure 2, by taking its
congruence closure (Figure 3).

$(\lambda
x.M)~{}N\mathrel{\breve{\leadsto}}M[N/x]\qquad\langle{\ldots,\ell=M,\ldots}\rangle.\ell\mathrel{\breve{\leadsto}}M\qquad
c(c^{\prime}_{1},\ldots,c^{\prime}_{n})\mathrel{\breve{\leadsto}}\left\llbracket{c}\right\rrbracket(c^{\prime}_{1},\ldots,c^{\prime}_{n})$
---
$\bigcup\mathopen{\textbf{\\{}}{\emptyset|x\leftarrow
M}\mathclose{\textbf{\\}}}\mathrel{\breve{\leadsto}}\emptyset\qquad\bigcup\mathopen{\textbf{\\{}}{M|x\leftarrow\emptyset}\mathclose{\textbf{\\}}}\mathrel{\breve{\leadsto}}\emptyset\qquad\bigcup\mathopen{\textbf{\\{}}{M|x\leftarrow\mathopen{\textbf{\\{}}{N}\mathclose{\textbf{\\}}}}\mathclose{\textbf{\\}}}\mathrel{\breve{\leadsto}}M[N/x]$
$\bigcup\mathopen{\textbf{\\{}}{M\mathbin{\cup}N|x\leftarrow R}\mathclose{\textbf{\\}}}$$~{}\mathrel{\breve{\leadsto}}~{}$ | $\bigcup\mathopen{\textbf{\\{}}{M|x\leftarrow R}\mathclose{\textbf{\\}}}\mathbin{\cup}\bigcup\mathopen{\textbf{\\{}}{N|x\leftarrow R}\mathclose{\textbf{\\}}}$
$\bigcup\mathopen{\textbf{\\{}}{M|x\leftarrow N\mathbin{\cup}R}\mathclose{\textbf{\\}}}$$~{}\mathrel{\breve{\leadsto}}~{}$ | $\bigcup\mathopen{\textbf{\\{}}{M|x\leftarrow N}\mathclose{\textbf{\\}}}\mathbin{\cup}\bigcup\mathopen{\textbf{\\{}}{M|x\leftarrow R}\mathclose{\textbf{\\}}}$
$\bigcup\mathopen{\textbf{\\{}}{M|y\leftarrow\bigcup\mathopen{\textbf{\\{}}{R|x\leftarrow N}\mathclose{\textbf{\\}}}}\mathclose{\textbf{\\}}}$$~{}\mathrel{\breve{\leadsto}}~{}$ | $\bigcup\mathopen{\textbf{\\{}}{M|x\leftarrow N,y\leftarrow R}\mathclose{\textbf{\\}}}\qquad\text{(if $x\notin\operatorname{FV}(M)$)}$
$\bigcup\mathopen{\textbf{\\{}}{M|x\leftarrow\mathtt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}where}~{}N~{}\mathtt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}do}~{}R}\mathclose{\textbf{\\}}}$$~{}\mathrel{\breve{\leadsto}}~{}$ | $\mathtt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}where}~{}N~{}\mathtt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}do}~{}\bigcup\mathopen{\textbf{\\{}}{M|x\leftarrow R}\mathclose{\textbf{\\}}}$
$\mathtt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}where}~{}{\mathsf{true}}~{}\mathtt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}do}~{}M\mathrel{\breve{\leadsto}}M\qquad\mathtt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}where}~{}{\mathsf{false}}~{}\mathtt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}do}~{}M\mathrel{\breve{\leadsto}}\emptyset\qquad\mathtt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}where}~{}M~{}\mathtt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}do}~{}\emptyset\mathrel{\breve{\leadsto}}\emptyset$
$\mathtt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}where}~{}M~{}\mathtt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}do}~{}(N\mathbin{\cup}R)$$~{}\mathrel{\breve{\leadsto}}~{}$ | $(\mathtt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}where}~{}M~{}\mathtt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}do}~{}N)\mathbin{\cup}(\mathtt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}where}~{}M~{}\mathtt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}do}~{}R)$
$\mathtt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}where}~{}M~{}\mathtt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}do}~{}\bigcup\mathopen{\textbf{\\{}}{N|x\leftarrow R}\mathclose{\textbf{\\}}}$$~{}\mathrel{\breve{\leadsto}}~{}$ | $\bigcup\mathopen{\textbf{\\{}}{\mathtt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}where}~{}M~{}\mathtt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}do}~{}N|x\leftarrow R}\mathclose{\textbf{\\}}}\qquad\text{(if $x\notin\operatorname{FV}(M)$)}$
$\mathtt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}where}~{}M~{}\mathtt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}do}~{}\mathtt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}where}~{}N~{}\mathtt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}do}~{}R$$~{}\mathrel{\breve{\leadsto}}~{}$ | $\mathtt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}where}~{}(M\land N)~{}\mathtt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}do}~{}R$
$\mathtt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}empty}~{}M$$~{}\mathrel{\breve{\leadsto}}~{}$ | $\mathtt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}empty}~{}(\bigcup\mathopen{\textbf{\\{}}{\langle{}\rangle|x\leftarrow M}\mathclose{\textbf{\\}}})\qquad\text{(if $M$ is not relation-typed)}$
Figure 2. Query normalization (basic contraction rules)

$M\mathrel{\breve{\leadsto}}M^{\prime}$ $M\mathrel{\leadsto}M^{\prime}$
$M\mathrel{\leadsto}M^{\prime}$
$c(\overrightarrow{L},M,\overrightarrow{N})\mathrel{\leadsto}c(\overrightarrow{L},M^{\prime},\overrightarrow{N})$

$M\mathrel{\leadsto}M^{\prime}$
$\langle{\overrightarrow{\ell_{1}=L},\ell=M,\overrightarrow{\ell_{2}=N}}\rangle\mathrel{\leadsto}\langle{\overrightarrow{\ell_{1}=L},\ell=M^{\prime},\overrightarrow{\ell_{2}=N}}\rangle$
$M\mathrel{\leadsto}M^{\prime}$ $M.\ell\mathrel{\leadsto}M^{\prime}.\ell$

$M\mathrel{\leadsto}M^{\prime}$ $\lambda x.M\mathrel{\leadsto}\lambda
x.M^{\prime}$ $M\mathrel{\leadsto}M^{\prime}$
$M~{}N\mathrel{\leadsto}M^{\prime}~{}N$ $M\mathrel{\leadsto}M^{\prime}$
$L~{}M\mathrel{\leadsto}L~{}M^{\prime}$

$M\mathrel{\leadsto}M^{\prime}$
$\mathopen{\textbf{\\{}}{M}\mathclose{\textbf{\\}}}\mathrel{\leadsto}\mathopen{\textbf{\\{}}{M^{\prime}}\mathclose{\textbf{\\}}}$
$M\mathrel{\leadsto}M^{\prime}$
$M\mathbin{\cup}N\mathrel{\leadsto}M^{\prime}\mathbin{\cup}N$
$M\mathrel{\leadsto}M^{\prime}$
$L\mathbin{\cup}M\mathrel{\leadsto}L\mathbin{\cup}M^{\prime}$

$M\mathrel{\leadsto}M^{\prime}$ $\bigcup\mathopen{\textbf{\\{}}{M|x\leftarrow
N}\mathclose{\textbf{\\}}}\mathrel{\leadsto}\bigcup\mathopen{\textbf{\\{}}{M^{\prime}|x\leftarrow
N}\mathclose{\textbf{\\}}}$ $M\mathrel{\leadsto}M^{\prime}$
$\bigcup\mathopen{\textbf{\\{}}{L|x\leftarrow
M}\mathclose{\textbf{\\}}}\mathrel{\leadsto}\bigcup\mathopen{\textbf{\\{}}{L|x\leftarrow
M^{\prime}}\mathclose{\textbf{\\}}}$

$M\mathrel{\leadsto}M^{\prime}$
$\mathtt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}empty}~{}M\mathrel{\leadsto}\mathtt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}empty}~{}M^{\prime}$

$M\mathrel{\leadsto}M^{\prime}$
$\mathtt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}where}~{}M~{}\mathtt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}do}~{}N\mathrel{\leadsto}\mathtt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}where}~{}M^{\prime}~{}\mathtt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}do}~{}N$
$M\mathrel{\leadsto}M^{\prime}$
$\mathtt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}where}~{}L~{}\mathtt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}do}~{}M\mathrel{\leadsto}\mathtt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}where}~{}L~{}\mathtt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}do}~{}M^{\prime}$

Figure 3. Query normalization (congruence closure of
$\mathrel{\breve{\leadsto}}$)

We will allow ourselves to say “induction on the derivation of reduction” to
mean the structural induction induced by the notion of congruence closure,
followed by a case analysis on the basic reduction rules used as its base
case.

We now discuss the basic reduction rules in more detail. 0-ary constants are
values of atomic type and do not reduce. Applied constants (with positive
arity) reduce when all of their arguments are (0-ary) constants: the reduction
rule relies on a fixed semantics $\left\llbracket{\cdot}\right\rrbracket$
which assigns to each constant $c$ of signature
$\Sigma(c)=\overrightarrow{A^{\prime}_{n}}\to A$ a function mapping constants
$c^{\prime}_{1},\ldots,c^{\prime}_{n}$ of type
$\overrightarrow{A^{\prime}_{n}}$ to values of type $A$. The rules for
collections and conditionals are mostly standard. The reduction rule for the
emptiness test is triggered when the argument $M$ is not of relation type
(but, for instance, of nested collection type) and employs comprehension to
generate a (trivial) relation that is empty if and only if $M$ is.

The normal forms of queries under these rewriting rules construct no
intermediate nested structures, and are straightforward to translate to
syntactically isomorphic (up to notational differences) and semantically
equivalent SQL queries. For example, consider the following
$\mathit{NRC}_{\lambda}$ query which, given a table $t$, first wraps the $id$
field of every tuple of $t$ into a singleton, yielding a collection of
singletons (i.e. a nested collection), then converts it back to a flat
collection by performing the grand union of all of its elements:

$\bigcup\mathopen{\textbf{\\{}}{y\mid
y\leftarrow\bigcup\mathopen{\textbf{\\{}}{\mathopen{\textbf{\\{}}{\mathopen{\textbf{\\{}}{x.id}\mathclose{\textbf{\\}}}}\mathclose{\textbf{\\}}}\mid
x\leftarrow t}\mathclose{\textbf{\\}}}}\mathclose{\textbf{\\}}}$

The normal form of this query does not create the unnecessary intermediate
nested collection:

$\bigcup\mathopen{\textbf{\\{}}{\mathopen{\textbf{\\{}}{x.id}\mathclose{\textbf{\\}}}\mid
x\leftarrow t}\mathclose{\textbf{\\}}}$

Such a query is easily translated to SQL as:

${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathtt{SELECT}}~{}x.id~{}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathtt{FROM}}~{}t~{}x$

Cooper [Coo09b] and Lindley and Cheney [LC12] give a full account of the
translation from $\mathit{NRC}_{\lambda}$ normal forms to SQL. Cheney et al.
[CLW13] showed how to improve the performance and reliability of LINQ in F#
using normalization and gave many examples showing how higher-order queries
support a convenient, compositional language-integrated query programming
style.

##  3\. Reducibility with branching continuations

We introduce here the extension of $\top\top$-lifting we use to derive a proof
of strong normalization for $\mathit{NRC}_{\lambda}$. The main contribution of
this section is a refined definition of continuations with branching structure
and multiple holes, as opposed to the linear structure with a single hole used
by standard $\top\top$-lifting. In our definition, continuations (as well as
the more general notion of context) are particular forms of terms: in this
way, the notion of term reduction can be used for continuations as well,
without need for auxiliary definitions.

###  3.1. Contexts and continuations

We start our discussion by introducing _contexts_ , or terms with multiple,
labelled holes that can be instantiated by plugging other terms (including
other contexts) into them.

[context] Let us fix a countably infinite set $\mathcal{P}$ of indices: a
_context_ $C$ is a term that may contain distinguished free variables
$\mathop{\left[{p}\right]}$, also called _holes_ , where $p\in\mathcal{P}$.
Holes are never bound by any of the binders (we disallow terms of the form
$\lambda\mathop{\left[{p}\right]}.M$ or
$\bigcup\mathopen{\textbf{\\{}}{M\mid\mathop{\left[{p}\right]}\leftarrow
N}\mathclose{\textbf{\\}}}$).

Given a finite map from indices to terms $[p_{1}\mapsto
M_{1},\ldots,p_{n}\mapsto M_{n}]$ (_context instantiation_), the notation
$C[p_{1}\mapsto M_{1},\ldots,p_{n}\mapsto M_{n}]$ (_context application_)
denotes the term obtained by simultaneously plugging $M_{1},\ldots,M_{n}$ into
the holes
$\mathop{\left[{p_{1}}\right]},\ldots,\mathop{\left[{p_{n}}\right]}$. Notice
that the $M_{i}$ are allowed to contain holes.

We will use metavariables $\eta,\theta$ to denote context instantiations.

[support] Given a context $C$, its _support_ $\operatorname{supp}(C)$ is
defined as the set of the indices $p$ such that $\mathop{\left[{p}\right]}$
occurs in $C$:

$\operatorname{supp}(C)\triangleq\\{{p:\mathop{\left[{p}\right]}\in\operatorname{FV}(C)}\\}$

(it suffices to use $\operatorname{FV}(C)$ as holes are never used as bound
variables).

When a term does not contain any $\mathop{\left[{p}\right]}$, we say that it
is a _pure_ term; when it is important that a term be pure, we will refer to
it by using overlined metavariables
$\overline{L},\overline{M},\overline{N},\overline{R},\ldots$

We introduce a notion of _permutable_ multiple context instantiation.

A context instantiation $\eta$ is _permutable_ iff for all
$p\in\operatorname{dom}(\eta)$ we have
$\operatorname{FV}(\eta(p))\cap\operatorname{dom}(\eta)=\emptyset$. The word
“permutable” is explained by the following properties:

######  Lemma 1.

Let $\eta$ be permutable, and $p_{1},\ldots,p_{k}$ be an enumeration of all
the elements of $\operatorname{dom}(\eta)$ without repetitions, in any order.
Then, for all contexts $C$, we have:

$C\eta=C[p_{1}\mapsto\eta(p_{1})]\cdots[p_{k}\mapsto\eta(p_{k})]$

######  Proof 3.1.

By structural induction on $C$. The relevant case is when
$C=\mathop{\left[{p_{i}}\right]}$, for some $i\in\\{{1,...,k}\\}$. By
definition, the left-hand side rewrites to $\eta(p_{i})$; we can express the
right-hand side as
$\mathop{\left[{p_{i}}\right]}\overrightarrow{[p_{j}\mapsto\eta(p_{j})]}_{j=1,\ldots,i-1}[p_{i}\mapsto\eta(p_{i})]\overrightarrow{[p_{j}\mapsto\eta(p_{j})]}_{j=i+1,\ldots,k}$.
Then we prove:

  * •

$\mathop{\left[{p_{i}}\right]}\overrightarrow{[p_{j}\mapsto\eta(p_{j})]}_{j=1,\ldots,i-1}=\mathop{\left[{p_{i}}\right]}$,
because for all $j$, $p_{i}\neq p_{j}$;

  * •

$\mathop{\left[{p_{i}}\right]}[p_{i}\mapsto\eta(p_{i})]=\eta(p_{i})$ by
definition;

  * •

$\eta(p_{i})\overrightarrow{[p_{j}\mapsto\eta(p_{j})]}_{j=i+1,\ldots,k}=\eta(p_{i})$
because, by the permutability hypothesis, for all $j$ we have that
$\mathop{\left[{p_{j}}\right]}\notin\operatorname{FV}(\eta(p_{i}))$.

Then the right-hand side also rewrites to $\eta(p_{i})$, proving the thesis.

All the other cases are trivial, applying induction hypotheses where needed.

######  Lemma 2.

Let $\eta$ be permutable and let us denote by $\eta_{\lnot p}$ the restriction
of $\eta$ to indices other than $p$. Then for all
$p\in\operatorname{dom}(\eta)$ we have:

$C\eta=C[p\mapsto\eta(p)]\eta_{\lnot p}=C\eta_{\lnot p}[p\mapsto\eta(p)]$

######  Proof 3.2.

Immediate, by Lemma 1.

We can now define continuations as certain contexts that capture how one or
more collections can be used in a program.

[continuation] Continuations $K$ are defined as the following subset of
contexts:

$\displaystyle K,H::=$
$\displaystyle\quad\mathop{\left[{p}\right]}\mathbin{~{}|~{}}\overline{M}\mathbin{~{}|~{}}K\mathbin{\cup}K\mathbin{~{}|~{}}\bigcup\mathopen{\textbf{\\{}}{\overline{M}|x\leftarrow
K}\mathclose{\textbf{\\}}}\mathbin{~{}|~{}}\mathtt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}where}~{}\overline{B}~{}\mathtt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}do}~{}K$

where for all indices $p$, $\mathop{\left[{p}\right]}$ can occur at most once.

This definition differs from the traditional one in two ways: first, holes are
decorated with an index; secondly, and most importantly, the production
$K\mathbin{\cup}K$ allows continuations to branch and, as a consequence, to
use more than one hole. Note that the grammar above is ambiguous, in the sense
that certain expressions like
$\mathtt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}where}~{}\overline{B}~{}\mathtt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}do}~{}\overline{N}$
can be obtained either from the production
$\mathtt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}where}~{}\overline{B}~{}\mathtt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}do}~{}K$
with $K=\overline{N}$, or as pure terms by means of the production
$\overline{M}$: we resolve this ambiguity by parsing these expressions as pure
terms whenever possible, and as continuations only when they are proper
continuations.

An additional complication of $\mathit{NRC}_{\lambda}$ when compared to the
computational metalanguage for which $\top\top$-lifting was devised lies in
the way conditional expressions can reduce when placed in an arbitrary
context: continuations in the grammar above are not liberal enough to adapt to
such reductions, therefore, like Cooper, we will need an additional definition
of _auxiliary_ continuations allowing holes to appear in the body of a
comprehension (in addition to comprehension generators). [auxiliary
continuation] Auxiliary continuations are defined as the following subset of
contexts:

$\displaystyle Q,O::=$
$\displaystyle\quad\mathop{\left[{p}\right]}\mathbin{~{}|~{}}\overline{M}\mathbin{~{}|~{}}Q\mathbin{\cup}Q\mathbin{~{}|~{}}\bigcup\mathopen{\textbf{\\{}}{Q|x\leftarrow
Q}\mathclose{\textbf{\\}}}\mathbin{~{}|~{}}\mathtt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}where}~{}\overline{B}~{}\mathtt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}do}~{}Q$

where for all indices $p$, $\mathop{\left[{p}\right]}$ can occur at most once.
We can then see that regular continuations are a special case of auxiliary
continuations; however, an auxiliary continuation is allowed to branch not
only with unions, but also with comprehensions.111It is worth noting that
Cooper’s original definition of auxiliary continuation does not use branching
comprehension (nor branching unions), but is linear just like the original
definition of continuation. The only difference between regular and auxiliary
continuations in his work is that the latter allowed nesting not just within
comprehension generators, but also within comprehension bodies (in our
notation, this would correspond to two separate productions
$\bigcup\mathopen{\textbf{\\{}}{\overline{M}|x\leftarrow
Q}\mathclose{\textbf{\\}}}$ and
$\bigcup\mathopen{\textbf{\\{}}{Q|x\leftarrow\overline{N}}\mathclose{\textbf{\\}}}$).

We use the following definition of _frames_ to represent certain continuations
with a distinguished shallow hole denoted by $\Box$. [frame] Frames are
defined by the following grammar:

$\displaystyle F::=$
$\displaystyle\quad\bigcup\mathopen{\textbf{\\{}}{Q|x\leftarrow\Box}\mathclose{\textbf{\\}}}\mathbin{~{}|~{}}\bigcup\mathopen{\textbf{\\{}}{\Box|x\leftarrow
Q}\mathclose{\textbf{\\}}}\mathbin{~{}|~{}}\mathtt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}where}~{}\overline{B}~{}\mathtt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}do}~{}\Box$

where $\Box$ does not occur in $Q$, and for all indices $p$,
$\mathop{\left[{p}\right]}$ can occur in $Q$ at most once.

The operation $F^{p}$, lifting a frame to an auxiliary continuation with a
distinguished hole $\mathop{\left[{p}\right]}$ is defined as:

$F^{p}:=F[\Box\mapsto\mathop{\left[{p}\right]}]\qquad(p\notin\operatorname{supp}(F))$

The composition operation $Q\mathop{\ooalign{\hfil\raise
0.86108pt\hbox{$\scriptscriptstyle p$}\hfil\crcr{$\bigcirc$}}}F$ is defined
as:

$Q\mathop{\ooalign{\hfil\raise 0.86108pt\hbox{$\scriptscriptstyle
p$}\hfil\crcr{$\bigcirc$}}}F=Q[p\mapsto F^{p}]$

We generally use frames in conjunction with continuations or auxiliary
continuations when we need to partially expose their leaves: for example, if
we write $K=K_{0}\mathop{\ooalign{\hfil\raise
0.86108pt\hbox{$\scriptscriptstyle
p$}\hfil\crcr{$\bigcirc$}}}\bigcup\mathopen{\textbf{\\{}}{\overline{M}|x\leftarrow\Box}\mathclose{\textbf{\\}}}$,
we know that instantiating $K$ at index $p$ with (for example) a singleton
term will create a redex:
$K[p\mapsto\mathopen{\textbf{\\{}}{\overline{L}}\mathclose{\textbf{\\}}}]\mathrel{\leadsto}K_{0}[p\mapsto\overline{M}\left[{\overline{L}}\middle/{x}\right]]$.
We say that such a reduction is a _reduction at the interface_ between the
continuation and the instantiation (we will make this notion formal in Lemma
14).

In certain proofs by induction that make use of continuations, we will need to
use a _measure_ of continuations to show that the induction is well-founded.
We introduce here two measures $\left|\cdot\right|_{p}$ and
$\left\|\cdot\right\|_{p}$ denoting the nesting depth of a hole
$\mathop{\left[{p}\right]}$: the two measures differ in the treatment of
nesting within the body of a comprehension. The measures $\left|Q\right|_{p}$
and $\left\|Q\right\|_{p}$ are defined as follows:

$\begin{array}[]{c}\left|\mathop{\left[{q}\right]}\right|_{p}=\left\|\mathop{\left[{q}\right]}\right\|_{p}=\left\\{\begin{array}[]{ll}1&\mbox{if
$p=q$}\\\ 0&\mbox{else}\end{array}\right.\\\
\left|\overline{M}\right|_{p}=\left\|\overline{M}\right\|_{p}=0\\\
\left|Q_{1}\mathbin{\cup}Q_{2}\right|_{p}=\max(\left|Q_{1}\right|_{p},\left|Q_{2}\right|_{p})\qquad\left\|Q_{1}\mathbin{\cup}Q_{2}\right\|_{p}=\max(\left\|Q_{1}\right\|_{p},\left\|Q_{2}\right\|_{p})\\\
\left|\mathtt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}where}~{}B~{}Q\right|_{p}=\left|Q\right|_{p}+1\qquad\left\|\mathtt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}where}~{}B~{}Q\right\|_{p}=\left\|Q\right\|_{p}+1\\\
\left|\bigcup\mathopen{\textbf{\\{}}{Q_{1}|x\mapsto
Q_{2}}\mathclose{\textbf{\\}}}\right|_{p}=\left\\{\begin{array}[]{ll}\hbox{\pagecolor{Gold}$\left|Q_{1}\right|_{p}$}&\mbox{if
$p\in\operatorname{supp}(Q_{1})$}\\\ \left|Q_{2}\right|_{p}+1&\mbox{if
$p\in\operatorname{supp}(Q_{2})$}\\\ 0&\mbox{else}\end{array}\right.\\\
\left\|\bigcup\mathopen{\textbf{\\{}}{Q_{1}|x\mapsto
Q_{2}}\mathclose{\textbf{\\}}}\right\|_{p}=\left\\{\begin{array}[]{ll}\hbox{\pagecolor{Gold}$\left\|Q_{1}\right\|_{p}+1$}&\mbox{if
$p\in\operatorname{supp}(Q_{1})$}\\\ \left\|Q_{2}\right\|_{p}+1&\mbox{if
$p\in\operatorname{supp}(Q_{2})$}\\\
0&\mbox{else}\end{array}\right.\end{array}$

We will also use $\left|Q\right|$ and $\left\|Q\right\|$ to refer to the
derived measures:

$\left|Q\right|=\sum_{p\in\operatorname{supp}(Q)}\left|Q\right|_{p}\qquad\qquad\left\|Q\right\|=\sum_{p\in\operatorname{supp}(Q)}\left\|Q\right\|_{p}$

The definitions of frames and measures are designed in such a way that the
following property holds.

######  Lemma 3.

Let $Q$ be an auxiliary continuation such that $p\in\operatorname{supp}(Q)$;
then for all frames $F$:

  1. (1)

$\left\|Q\right\|_{p}<\left\|Q\mathop{\ooalign{\hfil\raise
0.86108pt\hbox{$\scriptscriptstyle p$}\hfil\crcr{$\bigcirc$}}}F\right\|_{p}$
and $\left\|Q\right\|<\left\|Q\mathop{\ooalign{\hfil\raise
0.86108pt\hbox{$\scriptscriptstyle p$}\hfil\crcr{$\bigcirc$}}}F\right\|$

  2. (2)

if $F$ is not of the form $\bigcup\mathopen{\textbf{\\{}}{\Box\mid x\leftarrow
O}\mathclose{\textbf{\\}}}$, then
$\left|Q\right|_{p}<\left|Q\mathop{\ooalign{\hfil\raise
0.86108pt\hbox{$\scriptscriptstyle p$}\hfil\crcr{$\bigcirc$}}}F\right|_{p}$
and $\left|Q\right|<\left|Q\mathop{\ooalign{\hfil\raise
0.86108pt\hbox{$\scriptscriptstyle p$}\hfil\crcr{$\bigcirc$}}}F\right|$

  3. (3)

if $F=\bigcup\mathopen{\textbf{\\{}}{\Box\mid x\leftarrow
O}\mathclose{\textbf{\\}}}$, then
$\left|Q\right|_{p}=\left|Q\mathop{\ooalign{\hfil\raise
0.86108pt\hbox{$\scriptscriptstyle p$}\hfil\crcr{$\bigcirc$}}}F\right|_{p}$
and $\left|Q\right|=\left|Q\mathop{\ooalign{\hfil\raise
0.86108pt\hbox{$\scriptscriptstyle p$}\hfil\crcr{$\bigcirc$}}}F\right|$.

######  Proof 3.3.

By induction on the structure of $Q$. When examining the forms $Q$ can assume,
we will have to consider subexpressions $Q^{\prime}$ for which $p$ may or may
not be in $\operatorname{supp}(Q^{\prime})$: in the first case, we can apply
the induction hypothesis; otherwise, we prove
$\left\|Q^{\prime}\right\|_{p}=\left\|Q^{\prime}\mathop{\ooalign{\hfil\raise
0.86108pt\hbox{$\scriptscriptstyle p$}\hfil\crcr{$\bigcirc$}}}F\right\|=0$ and
$\left|Q^{\prime}\right|_{p}=\left|Q^{\prime}\mathop{\ooalign{\hfil\raise
0.86108pt\hbox{$\scriptscriptstyle p$}\hfil\crcr{$\bigcirc$}}}F\right|=0$.

$\mathit{NRC}_{\lambda}$ reduction can be used immediately on contexts
(including regular and auxiliary continuations) since these are simply terms
with distinguished free variables; we will also abuse notation to allow
ourselves to specify reduction on context instantiations: whenever
$\eta(p)\mathrel{\leadsto}N$ and $\eta^{\prime}=\eta_{\lnot p}[p\mapsto N]$,
we can write $\eta\mathrel{\leadsto}\eta^{\prime}$.

We will denote the set of strongly normalizing terms by
$\mathcal{S}\mathcal{N}$. Strongly-normalizing applied contexts satisfy the
following property:

For strongly normalizing terms (and by extension for context instantiations
containing only strongly normalizing terms), we can introduce the concept of
maximal reduction length.

[maximal reduction length] Let $M\in\mathcal{S}\mathcal{N}$: we define
$\nu(M)$ as the maximum length of all reduction sequences starting with $M$.
We also define $\nu(\eta)$ as
$\sum_{p\in\operatorname{dom}(\eta)}\nu(\eta(p))$, whenever all the terms in
the codomain of $\eta$ are strongly normalizing.

Since each term can only have a finite number of contracta, it is easy to see
that $\nu(M)$ is defined for any strongly normalizing term $M$. Furthermore,
$\nu(M)$ is strictly decreasing under reduction.

######  Lemma 4.

For all strongly normalizing terms $M$, if $M\mathrel{\leadsto}M^{\prime}$,
then $\nu(M^{\prime})<\nu(M)$.

######  Proof 3.4.

If $\nu(M^{\prime})\geq\nu(M)$, by pre-composing
$M\mathrel{\leadsto}M^{\prime}$ with a reduction chain of maximal length
starting at $M^{\prime}$ we obtain a new reduction chain starting at $M$ with
length strictly greater than $\nu(M)$; this contradicts the definition of
$\nu(M)$.

###  3.2. Renaming reduction

According to the Definitions 3.2 and 3.2, in order for a context to be a
continuation or an auxiliary continuation, it must on one hand agree with the
respective grammar, and on the other hand satisfy the condition that no hole
occurs more than once. We immediately see that, since holes can be duplicated
under reduction, the sets of plain and auxiliary continuations are not closed
under reduction. For instance:

$K=\bigcup\mathopen{\textbf{\\{}}{M\cup N\mid
x\leftarrow\mathop{\left[{p}\right]}}\mathclose{\textbf{\\}}}\mathrel{\leadsto}\bigcup\mathopen{\textbf{\\{}}{M\mid
x\leftarrow\mathop{\left[{p}\right]}}\mathclose{\textbf{\\}}}\cup\bigcup\mathopen{\textbf{\\{}}{N\mid
x\leftarrow\mathop{\left[{p}\right]}}\mathclose{\textbf{\\}}}=C$

where $K$ is a continuation, but $C$ is not due to the two occurrences of
$\mathop{\left[{p}\right]}$. For this reason, we introduce a refined notion of
renaming reduction which we can use to rename holes in the results so that
each of them occurs at most one time.

Given a term $M$ with holes and a finite map
$\sigma:\mathcal{P}\to\mathcal{P}$, we write $M\sigma$ for the term obtained
from $M$ by replacing each hole $\mathop{\left[{p}\right]}$ such that
$\sigma(p)$ is defined with $\mathop{\left[{\sigma(p)}\right]}$.

Even though finite renaming maps are partial functions, it is convenient to
extend them to total functions by taking $\sigma(p)=p$ whenever
$p\notin\operatorname{dom}(\sigma)$; we will write $\mathsf{id}$ to denote the
empty renaming map, whose total extension is the identity function on
$\mathcal{P}$.

[renaming reduction] $M$ $\sigma$-reduces to $N$ (notation:
$M\mathrel{\stackrel{{\scriptstyle\sigma}}{{\leadsto}}}N$) iff
$M\mathrel{\leadsto}N\sigma$.

Terms only admit a finite number of redexes and consequently, under regular
reduction, any given term has a finite number of possible contracta. However,
under renaming reduction, infinite contracta are possible: if
$M\mathrel{\leadsto}N$, there may be infinite $R,\sigma$ such that
$N=R\sigma$. When a strongly normalizing term $M$ admits infinite contracta,
it does not necessarily have a maximal reduction sequence (just like the
maximum of an infinite set of finite numbers is not necessarily defined).
Fortunately, we can prove (Lemma 6) that to every renaming reduction chain
there corresponds a plain reduction chain of the same length, and vice-versa.

######  Lemma 5.

If $M\mathrel{\leadsto}N$, then for all $\sigma$ we have
$M\sigma\mathrel{\leadsto}N\sigma$.

######  Proof 3.5.

Routine induction on the derivation of $M\mathrel{\leadsto}N$.

######  Lemma 6.

For every finite plain reduction sequence, there is a corresponding renaming
reduction sequence of the same length (using the identity renaming
$\mathsf{id}$); and conversely, for every finite renaming reduction sequence,
there is a corresponding plain reduction sequence of the same length involving
renamed terms. More precisely:

  1. (1)

If $M_{0}\mathrel{\leadsto}\cdots\mathrel{\leadsto}M_{n}$, then
$M_{0}\mathrel{\stackrel{{\scriptstyle\mathsf{id}}}{{\leadsto}}}\cdots\mathrel{\stackrel{{\scriptstyle\mathsf{id}}}{{\leadsto}}}M_{n}$

  2. (2)

If
$M_{0}\mathrel{\stackrel{{\scriptstyle\sigma_{1}}}{{\leadsto}}}\cdots\mathrel{\stackrel{{\scriptstyle\sigma_{n-1}}}{{\leadsto}}}M_{n-1}\mathrel{\stackrel{{\scriptstyle\sigma_{n}}}{{\leadsto}}}M_{n}$,
then $M_{0}\mathrel{\leadsto}\cdots
M_{n-1}\sigma_{n-1}\cdots\sigma_{1}\mathrel{\leadsto}M_{n}\sigma_{n}\cdots\sigma_{1}$

######  Proof 3.6.

The first part of the lemma is trivial. For the second part, proceed by
induction on the length of the reduction chain: in the inductive case, we have
$M_{0}\mathrel{\stackrel{{\scriptstyle\sigma_{1}}}{{\leadsto}}}\cdots\mathrel{\stackrel{{\scriptstyle\sigma_{n}}}{{\leadsto}}}M_{n}\mathrel{\stackrel{{\scriptstyle\sigma_{n+1}}}{{\leadsto}}}M_{n+1}$
by hypothesis and
$M_{0}\mathrel{\leadsto}\cdots\mathrel{\leadsto}M_{n}\sigma_{n}\cdots\sigma_{1}$
by induction hypothesis; to obtain the thesis, we only need to prove that

$M_{n}\sigma_{n}\cdots\sigma_{1}\mathrel{\leadsto}M_{n+1}\sigma_{n+1}\sigma_{n}\cdots\sigma_{1}$

In order for this to be true, by Lemma 5, it is sufficient to show that
$M_{n}\mathrel{\leadsto}M_{n+1}\sigma_{n+1}$; this is by definition equivalent
to $M_{n}\mathrel{\stackrel{{\scriptstyle\sigma_{n+1}}}{{\leadsto}}}M_{n+1}$,
which we know by hypothesis.

######  Corollary 7.

Suppose $M\in\mathcal{S}\mathcal{N}$: if
$M\mathrel{\stackrel{{\scriptstyle\sigma}}{{\leadsto}}}M^{\prime}$, then
$\nu(M^{\prime})$ is defined and $\nu(M^{\prime})<\nu(M)$.

######  Proof 3.7.

By Lemma 6, for any plain reduction chain there exists a renaming reduction
chain of the same length, and vice-versa. Thus, since plain reduction lowers
the length of the maximal reduction chain (Lemma 4), the same holds for
renaming reduction.

The results above prove that the set of strongly normalizing terms is the same
under the two notions of reduction, thus $\nu(M)$ can be used to refer to the
maximal length of reduction chains starting at $M$ either with or without
renaming.

Our goal is to describe the reduction of pure terms expressed in the form of
applied continuations. One first difficulty we need to overcome is that, as we
noted, the sets of continuations (both regular and auxiliary) are not closed
under reduction: the duplication of holes performed by reduction will produce
contexts that are not continuations or auxiliary continuations because they do
not satisfy the condition of the linearity of holes. Thankfully, renaming
reduction allows us to restore the linearity of holes, as we show in the
following lemma.

######  Lemma 8.

  1. (1)

For all continuations $K$, if $K\mathrel{\leadsto}C$, there exist a
continuation $K^{\prime}$ and a finite map $\sigma$ such that
$K\mathrel{\stackrel{{\scriptstyle\sigma}}{{\leadsto}}}K^{\prime}$ and
$K^{\prime}\sigma=C$.

  2. (2)

For all auxiliary continuations $Q$, if $Q\mathrel{\leadsto}C$, there exist an
auxiliary continuation $Q^{\prime}$ and a finite map $\sigma$ such that
$Q\mathrel{\stackrel{{\scriptstyle\sigma}}{{\leadsto}}}Q^{\prime}$ and
$Q^{\prime}\sigma=C$.

Furthermore, the $\sigma,K^{\prime},Q^{\prime}$ in the statements above can be
chosen so that $\operatorname{dom}(\sigma)$ is fresh with respect to any given
finite set of indices $\mathcal{S}$.

######  Proof 3.8.

Let $\mathcal{S}$ be a finite set of indices and $C$ a contractum of the
continuation we wish to reduce. This contractum will not, in general, satisfy
the linearity condition of holes that is mandated by the definitions of plain
and auxiliary continuations; however we can show that, for any context with
duplicated holes, there exists a structurally equal context with linear holes.

Operationally, if $C$ contains $n$ holes, we generate $n$ different indices
that are fresh for $\mathcal{S}$, and replace the index of each hole in $C$
with a different fresh index to obtain a new context $C^{\prime}$: this
induces a finite map
$\sigma:\operatorname{supp}(C^{\prime})\to\operatorname{supp}(C)$ such that
$C^{\prime}\sigma=C$. By the definition of renaming reduction, we have
$K\mathrel{\stackrel{{\scriptstyle\sigma}}{{\leadsto}}}C^{\prime}$ (resp.
$Q\mathrel{\stackrel{{\scriptstyle\sigma}}{{\leadsto}}}C^{\prime}$). To prove
that $C^{\prime}$ is a continuation (resp. auxiliary continuation) we need to
show that it satisfies the linearity condition and that it meets the grammar
in Definition 3.2 (resp. Definition 3.2). The first part holds by
construction; the proof that $C^{\prime}$ satisfies the required grammar is
obtained by structural induction on the derivation of the reduction, with a
case analysis on the structure of $K$ (or on the structure of $Q$).

By construction of $\sigma$, we also have that
$\operatorname{dom}(\sigma)\cap\mathcal{S}=\emptyset$, as required by the
Lemma statement.

A further problem concerns variable capture: if we reduce
$C\mathrel{\leadsto}C^{\prime}$, there is no guarantee that
$C\eta\mathrel{\leadsto}C^{\prime}\eta$ for a given context instantiation
$\eta$. This happens for two reasons: the first one is that reducing a context
$C$ may cause a hole to move within the scope of a new binder. So,

$\begin{array}[]{c}\bigcup\mathopen{\textbf{\\{}}{\mathop{\left[{p}\right]}\mid
y\leftarrow\bigcup\mathopen{\textbf{\\{}}{N\mid x\leftarrow
M}\mathclose{\textbf{\\}}}}\mathclose{\textbf{\\}}}\mathrel{\leadsto}\bigcup\mathopen{\textbf{\\{}}{\mathop{\left[{p}\right]}\mid
x\leftarrow M,y\leftarrow N}\mathclose{\textbf{\\}}}\\\ \text{but}\\\
\bigcup\mathopen{\textbf{\\{}}{\mathop{\left[{p}\right]}\mid
y\leftarrow\bigcup\mathopen{\textbf{\\{}}{N\mid x\leftarrow
M}\mathclose{\textbf{\\}}}}\mathclose{\textbf{\\}}}[p\mapsto
x]\not\mathrel{\leadsto}\bigcup\mathopen{\textbf{\\{}}{\mathop{\left[{p}\right]}\mid
x\leftarrow M,y\leftarrow N}\mathclose{\textbf{\\}}}[p\mapsto x]\end{array}$

because the first term is equal to $\bigcup\mathopen{\textbf{\\{}}{x\mid
y\leftarrow\bigcup\mathopen{\textbf{\\{}}{N\mid x\leftarrow
M}\mathclose{\textbf{\\}}}}\mathclose{\textbf{\\}}}$ where the $x$ in the head
of the outer comprehension is free, and the reduction is blocked until we
rename the bound $x$ of the inner comprehension.

The second reason for which the reduction of a context may be disallowed if we
apply it to a context instantiation is that, due to variable capture, the
reduction may involve the context instantiation in a non-trivial way:

$\begin{array}[]{c}(\lambda
z.\mathop{\left[{p}\right]})~{}N\mathrel{\leadsto}\mathop{\left[{p}\right]}\\\
\text{but}\\\ ((\lambda z.\mathop{\left[{p}\right]})~{}N)[p\mapsto
z]\not\mathrel{\leadsto}\mathop{\left[{p}\right]}[p\mapsto z]\end{array}$

because the left-hand term is equal to $(\lambda
z.\mathop{\left[{p}\right]}[p\mapsto z])~{}N$, and the right-hand one is $z$,
and the former does not reduce to the latter, but to
$\mathop{\left[{p}\right]}[p\mapsto z]\left[{N}\middle/{z}\right]=N$.

While we understand that the first of the two problems should be handled with
a suitable alpha-renaming of the redex, the other is more complicated.
Fortunately, in most cases we are not interested in the reduction of generic
contexts, but only in that of auxiliary continuations: due to their restricted
term shape, auxiliary continuations only allow some reductions, most of which
do not present the problem above; the exception is when a reduction is
obtained by contracting a subterm using the comprehension-singleton rule:

$\bigcup\mathopen{\textbf{\\{}}{Q_{0}\mid
z\leftarrow\mathopen{\textbf{\\{}}{\overline{L}}\mathclose{\textbf{\\}}}}\mathclose{\textbf{\\}}}\mathrel{\leadsto}Q_{0}\left[{\overline{L}}\middle/{z}\right]$

By applying a context instantiation $\eta$ to both sides, we obtain an
incorrect contraction:

$\bigcup\mathopen{\textbf{\\{}}{Q_{0}\mid
z\leftarrow\mathopen{\textbf{\\{}}{\overline{L}}\mathclose{\textbf{\\}}}}\mathclose{\textbf{\\}}}\eta=\bigcup\mathopen{\textbf{\\{}}{Q_{0}\eta\mid
z\leftarrow\mathopen{\textbf{\\{}}{\overline{L}}\mathclose{\textbf{\\}}}}\mathclose{\textbf{\\}}}\not\mathrel{\leadsto}Q_{0}\left[{\overline{L}}\middle/{z}\right]\eta$

where the left-hand term does not reduce to the right-hand one because in the
latter the codomain of $\eta$ might contain free instances of $z$ that have
not been replaced by $\overline{L}$. In the rest of the paper, we will call
reductions using the comprehension-singleton rule _special reductions_. When
$Q\mathrel{\leadsto}Q^{\prime}$ by means of a special reduction, we know that
in general $Q\eta\not\mathrel{\leadsto}Q^{\prime}\eta$ (not even after alpha-
renaming), and we will have to handle such a case differently.

If however $Q\mathrel{\leadsto}Q^{\prime}$ is _not_ a special reduction, to
mimic that reduction within $Q\eta$ we may start by renaming the bound
variables of this term in such a way that no reduction is blocked: we obtain a
term in the form $O\theta$, where $O$ is an auxiliary continuation alpha-
equivalent222 In our setting, contexts are defined as a particular case of
terms, allowing special “hole” free variables that are not used in binders;
thus, we only have a single notion of alpha-equivalence for terms that we also
apply to contexts (just like our notion of reduction works on terms and
contexts alike). This may look surprising and perhaps suspicious, considering
that in some formal treatments of contexts (e.g. [BdV01]) the alpha-renaming
of contexts is forbidden; however, our work does not need to provide a general
treatment of alpha-renaming in contexts: we only use it under special
conditions that ensure its consistency.  to $Q$, and $\theta$ is obtained from
$\eta$ by replacing some of its free variables with other free variables,
consistently with the renaming of $Q$ to $O$, as shown by the following lemma
(a more general result applying to all reductions
$C\mathrel{\leadsto}C^{\prime}$ and all context instantiations $\eta$, which
however gives weaker guarantees on the result of contracting $C\eta$, will be
provided as Lemma 18).

######  Lemma 9.

For all auxiliary continuations $Q$ and for all permutable context
instantiations $\eta$, there exist an auxiliary continuation $O$ and a context
instantiation $\theta$ such that:

  1. (1)

$Q=_{\alpha}O$ and $Q\eta=_{\alpha}O\theta$

  2. (2)

$\theta=[p\mapsto\eta(p)\left[{\overrightarrow{y_{p}}}\middle/{\overrightarrow{x_{p}}}\right]\mid
p\in\operatorname{dom}(\eta)]$ for some
$\overrightarrow{x_{p}},\overrightarrow{y_{p}}$ (i.e. $\theta$ is equal to
$\eta$ up to a renaming of the free variables in its codomain)

  3. (3)

for all $C^{\prime}$ such that $Q\mathrel{\leadsto}C^{\prime}$ with a non-
special reduction, there exists $D^{\prime}=_{\alpha}C^{\prime}$ such that
$O\mathrel{\leadsto}D^{\prime}$ and we also have
$O\theta\mathrel{\leadsto}D^{\prime}\theta$

######  Proof 3.9.

We proceed by induction on the size of $Q$ followed by a case analysis on its
structure; for each case, after considering all possible reductions starting
in that particular shape of $Q$ (where we are allowed, by the hypothesis, to
ignore special reductions), we perform a renaming of $Q\eta$ to $O\theta$ that
is guaranteed to allow us to prove the thesis. Particular care is needed when
context instantiations cross binders, as variable capture is allowed to
happen:

  * •

Case $Q=\mathop{\left[{p}\right]}$: no reduction of $Q$ is possible, so we can
choose $O:=Q$, $\theta:=\eta$, and the thesis holds trivially.

  * •

Case $Q=\overline{M}$: for all reductions
$\overline{M}\mathrel{\leadsto}\overline{M^{\prime}}$, we have
$\overline{M}\eta=\overline{M}$ and
$\overline{M^{\prime}}\eta=\overline{M^{\prime}}$, because context
instantiation is ineffective on pure terms; so we can choose $O:=Q$,
$\theta:=\eta$, and the thesis holds trivially.

  * •

Case $Q=Q_{1}\cup Q_{2}$. Since the holes in $Q$ are linear and $\eta$ is
permutable, we can decompose $\eta=\eta_{1}\eta_{2}$, such that
$Q\eta=Q_{1}\eta_{1}\cup Q_{2}\eta_{2}$; we apply the induction hypothesis
twice on the two subterms, to obtain $O_{1},O_{2},\theta_{1},\theta_{2}$ such
that for $i=1,2$, we have $O_{i}=_{\alpha}Q_{i}$,
$O_{i}\theta_{i}=_{\alpha}Q_{i}\eta_{i}$, $\theta_{i}$ is equal to $\eta_{i}$
up to a renaming of the free variables in its codomain, and for all
$C^{\prime}_{i}$ such that $Q_{i}\mathrel{\leadsto}C^{\prime}_{i}$ where the
reduction is not special, there exists
$D^{\prime}_{i}=_{\alpha}C^{\prime}_{i}$ such that
$O_{i}\mathrel{\leadsto}D^{\prime}_{i}$ and
$O_{i}\theta_{i}\mathrel{\leadsto}D^{\prime}_{i}\theta_{i}$. Now, to prove the
thesis, we fix $O:=O_{1}\cup O_{2}$ and $\theta:=\theta_{1}\theta_{2}$; we
easily show that $O=_{\alpha}Q$, $O\theta=_{\alpha}Q\eta$ and that $\theta$ is
equal to $\eta$ up to a renaming of the free variables in its codomain. To
conclude the proof, we consider any given reduction
$Q\mathrel{\leadsto}C^{\prime}$, and we see by case analysis that either
$C^{\prime}=Q_{1}^{\prime}\cup Q_{2}$ such that
$Q_{1}\mathrel{\leadsto}Q_{1}^{\prime}$, or $C^{\prime}=Q_{1}\cup
Q_{2}^{\prime}$ such that $Q_{2}\mathrel{\leadsto}Q_{2}^{\prime}$: in the
first case, we know that there exists $D^{\prime}_{1}=_{\alpha}C^{\prime}_{1}$
such that $O_{1}\mathrel{\leadsto}D^{\prime}_{1}$ and
$O_{1}\theta_{1}\mathrel{\leadsto}D^{\prime}_{1}$: we fix
$D^{\prime}:=D^{\prime}_{1}\cup C^{\prime}_{2}$ and easily prove
$D^{\prime}=_{\alpha}C^{\prime}$, $D^{\prime}\theta=_{\alpha}C^{\prime}\eta$,
and $O\theta\mathrel{\leadsto}D^{\prime}\theta$.

  * •

Case $Q=\bigcup\mathopen{\textbf{\\{}}{Q_{1}\mid
y\leftarrow\bigcup\mathopen{\textbf{\\{}}{Q_{2}\mid z\leftarrow
Q_{3}}\mathclose{\textbf{\\}}}}\mathclose{\textbf{\\}}}$. Since the holes in
$Q$ are linear and $\eta$ is permutable, we can decompose
$\eta=\eta_{1}\eta_{2}\eta_{3}$, such that

$Q\eta=\bigcup\mathopen{\textbf{\\{}}{Q_{1}\eta_{1}\mid
y\leftarrow\bigcup\mathopen{\textbf{\\{}}{Q_{2}\eta_{2}\mid z\leftarrow
Q_{3}\eta_{3}}\mathclose{\textbf{\\}}}}\mathclose{\textbf{\\}}};$

$Q$ can reduce either in the subcontinuations $Q_{1}$, $Q_{2}$, $Q_{3}$ or, if
$z\notin\operatorname{FV}(Q_{1})$, by applying the unnesting reduction;
however, the last reduction might be blocked in $Q\eta$, if
$z\in\operatorname{FV}(Q_{1}\eta_{1})$. For this reason, we start by choosing
a non-hole variable $z^{*}\notin\operatorname{FV}(Q_{1}\eta_{1})$ and renaming
$Q$ as $Q^{*}:=\bigcup\mathopen{\textbf{\\{}}{Q_{1}\mid
y\leftarrow\bigcup\mathopen{\textbf{\\{}}{Q^{*}_{2}\mid z^{*}\leftarrow
Q_{3}}\mathclose{\textbf{\\}}}}\mathclose{\textbf{\\}}}$, where we have
defined $Q^{*}_{2}:=Q_{2}\left[{z^{*}}\middle/{z}\right]$. Clearly,
$Q^{*}=_{\alpha}Q$ and, if we fix
$\eta^{*}_{2}:=[\eta_{2}(p)\left[{z^{*}}\middle/{z}\right]\mid
p\in\operatorname{dom}(\eta)]$ and $\eta^{*}:=\eta_{1}\eta^{*}_{2}\eta_{3}$,
we also have $Q^{*}\eta^{*}=_{\alpha}Q\eta$; furthermore, since $z^{*}$ is not
a hole, we can see $\eta^{*}$ must still permutable. Now, since
$Q^{*}\eta^{*}=\bigcup\mathopen{\textbf{\\{}}{Q_{1}\eta_{1}\mid
y\leftarrow\bigcup\mathopen{\textbf{\\{}}{Q_{2}^{*}\eta_{2}^{*}\mid
z^{*}\leftarrow
Q_{3}\eta_{3}}\mathclose{\textbf{\\}}}}\mathclose{\textbf{\\}}}$, we apply the
induction hypothesis three times on the subterms, to obtain:

    * –

$O_{1},\theta_{1}$ such that $O_{1}=_{\alpha}Q_{1}$,
$O_{1}\theta_{1}=_{\alpha}Q_{1}\eta_{1}$, $\theta_{1}$ is equal to $\eta_{1}$
up to a renaming of the free variables in its codomain, and for all
$C^{\prime}_{1}$ such that $Q_{1}\mathrel{\leadsto}C^{\prime}_{1}$ where the
reduction is not special, there exists
$D^{\prime}_{1}=_{\alpha}C^{\prime}_{1}$ such that
$O_{1}\mathrel{\leadsto}D^{\prime}_{1}$ and
$O_{1}\theta_{1}\mathrel{\leadsto}D^{\prime}_{1}\theta_{1}$

    * –

$O_{2},\theta_{2}$ such that $O_{2}=_{\alpha}Q^{*}_{2}$,
$O_{2}\theta_{2}=_{\alpha}Q^{*}_{2}\eta^{*}_{2}$, $\theta_{1}$ is equal to
$\eta^{*}_{2}$ (and thus to $\eta_{2}$) up to a renaming of the free variables
in its codomain, and for all $C^{\prime}_{2}$ such that
$Q^{*}_{2}\mathrel{\leadsto}C^{\prime}_{2}$ where the reduction is not
special, there exists $D^{\prime}_{2}=_{\alpha}C^{\prime}_{2}$ such that
$O_{2}\mathrel{\leadsto}D^{\prime}_{2}$ and
$O_{2}\theta_{2}\mathrel{\leadsto}D^{\prime}_{2}\theta_{2}$

    * –

$O_{3},\theta_{3}$ such that $O_{3}=_{\alpha}Q_{3}$,
$O_{3}\theta_{3}=_{\alpha}Q_{3}\eta_{3}$, $\theta_{3}$ is equal to $\eta_{3}$
up to a renaming of the free variables in its codomain, and for all
$C^{\prime}_{3}$ such that $Q_{3}\mathrel{\leadsto}C^{\prime}_{3}$ where the
reduction is not special, there exists
$D^{\prime}_{3}=_{\alpha}C^{\prime}_{3}$ such that
$O_{3}\mathrel{\leadsto}D^{\prime}_{3}$ and
$O_{3}\theta_{3}\mathrel{\leadsto}D^{\prime}_{3}\theta_{3}$

Note that the first and third case are similar, but the second one has
slightly different properties to account for the renaming of $z$ to $z^{*}$.

Now we fix $O:=\bigcup\mathopen{\textbf{\\{}}{O_{1}\mid
y\leftarrow\bigcup\mathopen{\textbf{\\{}}{O_{2}\mid z^{*}\leftarrow
O_{3}}\mathclose{\textbf{\\}}}}\mathclose{\textbf{\\}}}$ and
$\theta:=\theta_{1}\theta_{2}\theta_{3}$. We easily show that $O=_{\alpha}Q$,
$O\theta=_{\alpha}Q\eta$ and that $\theta$ is equal to $\eta$ up to a renaming
of the free variables in its codomain. To conclude the proof, we consider any
given reduction $Q\mathrel{\leadsto}C^{\prime}$, and we see by case analysis
that either the reduction corresponds to a reduction in the subcontinuations
$Q_{i}$ (in which case we conclude by a reasoning on the subterms and
induction hypotheses, similarly to the union case above), or to one of the
following:

    * –

$C^{\prime}=\bigcup\mathopen{\textbf{\\{}}{Q_{1}\mid z\leftarrow
Q_{3},y\leftarrow Q_{2}}\mathclose{\textbf{\\}}}$: in this case, we fix
$D^{\prime}:=\bigcup\mathopen{\textbf{\\{}}{Q_{1}\mid z^{*}\leftarrow
Q_{3},y\leftarrow Q^{*}_{2}}\mathclose{\textbf{\\}}}$ and we prove, as
required, that $D^{\prime}=_{\alpha}C^{\prime}$,
$O\mathrel{\leadsto}D^{\prime}$, and
$O\theta\mathrel{\leadsto}D^{\prime}\theta$.

    * –

$Q_{1}=\emptyset$ and $C^{\prime}=\emptyset$: we easily see that
$O_{1}=\emptyset$, so we can fix $D^{\prime}=\emptyset$ and show the thesis.

    * –

$Q_{1}=Q_{11}\cup Q_{12}$ and

$C^{\prime}=\bigcup\mathopen{\textbf{\\{}}{Q_{11}\mid
y\leftarrow\bigcup\mathopen{\textbf{\\{}}{Q_{2}\mid z\leftarrow
Q_{3}}\mathclose{\textbf{\\}}}}\mathclose{\textbf{\\}}}\cup\bigcup\mathopen{\textbf{\\{}}{Q_{12}\mid
y\leftarrow\bigcup\mathopen{\textbf{\\{}}{Q_{2}\mid z\leftarrow
Q_{3}}\mathclose{\textbf{\\}}}}\mathclose{\textbf{\\}}}:$

we prove that there exist $O_{11},O_{12}$ such that $Q_{11}=_{\alpha}O_{11}$,
$Q_{12}=_{\alpha}O_{12}$, and $O_{1}=O_{11}\cup O_{12}$, fix
$D^{\prime}=\bigcup\mathopen{\textbf{\\{}}{Q_{11}\mid
y\leftarrow\bigcup\mathopen{\textbf{\\{}}{Q_{2}\mid z\leftarrow
Q_{3}}\mathclose{\textbf{\\}}}}\mathclose{\textbf{\\}}}\cup\bigcup\mathopen{\textbf{\\{}}{Q_{12}\mid
y\leftarrow\bigcup\mathopen{\textbf{\\{}}{Q_{2}\mid z\leftarrow
Q_{3}}\mathclose{\textbf{\\}}}}\mathclose{\textbf{\\}}}$, and prove the
thesis.

  * •

Case $Q=\bigcup\mathopen{\textbf{\\{}}{Q_{1}\mid y\leftarrow
Q_{2}}\mathclose{\textbf{\\}}}$ where $Q_{2}$ is not a comprehension: this is
similar to the case above, but instead of comprehension unnesting we have to
consider two possible reductions

    * –

$Q_{2}=\mathtt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}where}~{}\overline{B}~{}\mathtt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}do}~{}Q_{3}$
and
$C^{\prime}=\mathtt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}where}~{}\overline{B}~{}\mathtt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}do}~{}\bigcup\mathopen{\textbf{\\{}}{Q_{1}\mid
y\leftarrow Q_{3}}\mathclose{\textbf{\\}}}$

    * –

$Q_{2}=Q_{3}\cup Q_{4}$ and
$C^{\prime}=\bigcup\mathopen{\textbf{\\{}}{Q_{1}\mid y\leftarrow
Q_{3}}\mathclose{\textbf{\\}}}\cup\bigcup\mathopen{\textbf{\\{}}{Q_{1}\mid
y\leftarrow Q_{4}}\mathclose{\textbf{\\}}}$

However, these reductions do not require us to perform renamings and do not
pose any problems.

  * •

Case
$Q=\mathtt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}where}~{}\overline{B}~{}\mathtt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}do}~{}Q_{1}$.
Besides reductions in the subterms, we have to consider the following cases:

    * –

$Q_{1}=\bigcup\mathopen{\textbf{\\{}}{Q_{2}\mid y\leftarrow
Q_{3}}\mathclose{\textbf{\\}}}$ and
$C^{\prime}=\bigcup\mathopen{\textbf{\\{}}{\mathtt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}where}~{}\overline{B}~{}\mathtt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}do}~{}Q_{1}\mid
z\leftarrow Q_{2}}\mathclose{\textbf{\\}}}$ where
$z\notin\operatorname{FV}(\overline{B})$

    * –

$\overline{B}={\mathsf{true}}$ and $C^{\prime}=Q_{1}$

    * –

$\overline{B}={\mathsf{false}}$ and $C^{\prime}=\emptyset$

    * –

$Q_{1}=Q_{2}\cup Q_{3}$ and
$C^{\prime}=(\mathtt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}where}~{}\overline{B}~{}\mathtt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}do}~{}Q_{2})\cup(\mathtt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}where}~{}\overline{B}~{}\mathtt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}do}~{}Q_{3})$

    * –

$Q_{1}=\mathtt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}where}~{}\overline{B_{0}}~{}\mathtt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}do}~{}Q_{2}$
and
$C^{\prime}=\mathtt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}where}~{}(B\land
B_{0})~{}\mathtt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}do}~{}Q_{2}$.

In all these cases, no renaming is required (besides those produced by
applying the induction hypothesis); in particular, the first reduction is
always possible without renaming because $\overline{B}$ is a pure term, so
$z\notin\operatorname{FV}(\overline{B}\eta)$ because
$\overline{B}\eta=\overline{B}$. Therefore, we prove the thesis using the
induction hypothesis and an exhaustive case analysis on the possible reduction
as we did above, without particular problems.

######  Remark 10.

It is important to understand that, unlike all other operations on terms,
context instantiation is not defined on the abstract syntax, independently of
the particular choice of names, but on the concrete syntax. In other words,
all operations and proofs that do not use context instantiation work on alpha-
equivalence classes of terms; but when context instantiation is used, say on a
context $C$, we need to choose a representative of the alpha-equivalence class
of $C$.

Thanks to Lemma 9, whenever we need to reduce $Q$ with a non-special reduction
in a term of the form $Q\eta$, we may assume without loss of generality that
the representative of the alpha-equivalence class of $Q\eta$ is chosen so that
if $Q\mathrel{\leadsto}C^{\prime}$, then
$Q\eta\mathrel{\leadsto}C^{\prime}\eta$. Technically, we prove that there
exist $O,D^{\prime},\theta$ such that $Q=_{\alpha}O$,
$C^{\prime}=_{\alpha}D^{\prime}$, $\theta$ is equal to $\eta$ up to renaming,
and $O\theta\mathrel{\leadsto}D^{\prime}\theta$, but after the context
instantiation is completed, we return to consider terms as equal up to alpha-
equivalence. The result will be used in the proof of the following Lemma 12,
where we have clarified the technical parts.

Finally, given a non-special renaming reduction
$Q\mathrel{\stackrel{{\scriptstyle\sigma}}{{\leadsto}}}Q^{\prime}$, we want to
be able to express the corresponding reduction on $Q\eta$: due to the renaming
$\sigma$, it is not enough to change $Q$ to $Q^{\prime}$, but we also need to
construct some $\eta^{\prime}$ containing precisely those mappings $[q\mapsto
M]$ such that, if $\sigma(q)=p$, then $p\in\operatorname{dom}(\eta)$ and
$\eta(p)=M$. This construction is expressed by means of the following
operation. For all context instantiations $\eta$ and renamings $\sigma$, we
define $\eta^{\sigma}$ as the context instantiation such that:

  * •

if $\sigma(p)\in\operatorname{dom}(\eta)$ then
$\eta^{\sigma}(p)=\eta(\sigma(p))$;

  * •

in all other cases, $\eta^{\sigma}(p)=p$.

The results above allow us to express what happens when a reduction duplicates
the holes in a continuation which is then combined with a context
instantiation.

######  Lemma 11.

For all contexts $C$, finite maps $\sigma$, and context instantiations $\eta$
such that, for all $p\in\operatorname{dom}(\eta)$,
$\operatorname{supp}(\eta(p))\cap\operatorname{dom}(\sigma)=\emptyset$, we
have $C\sigma\eta=C\eta^{\sigma}\sigma$.

######  Proof 3.10.

By structural induction on $C$. The interesting case is when
$C=\mathop{\left[{p}\right]}$. If $\sigma(p)\in\operatorname{dom}(\eta)$:

$\displaystyle\mathop{\left[{p}\right]}\sigma\eta$
$\displaystyle=\mathop{\left[{\sigma(p)}\right]}\eta$ (Definition 3.2)
$\displaystyle=\eta(\sigma(p))$ (Definition 3.1)
$\displaystyle=\eta(\sigma(p))\sigma$
($\operatorname{supp}(\eta(p))\cap\operatorname{dom}(\sigma)=\emptyset$)
$\displaystyle=\mathop{\left[{p}\right]}\eta^{\sigma}\sigma$ (Definition 3.2,
with $\sigma(p)\in\operatorname{dom}(\eta)$)

If instead $\sigma(p)\notin\operatorname{dom}(\eta)$:

$\displaystyle\mathop{\left[{p}\right]}\sigma\eta$
$\displaystyle=\mathop{\left[{\sigma(p)}\right]}\eta$ (Definition 3.2)
$\displaystyle=\mathop{\left[{\sigma(p)}\right]}$
($\sigma(p)\notin\operatorname{dom}(\eta)$)
$\displaystyle=\mathop{\left[{p}\right]}\sigma$ (Definition 3.2)
$\displaystyle=\mathop{\left[{p}\right]}\eta^{\sigma}\sigma$ (Definition 3.2,
with $\sigma(p)\notin\operatorname{dom}(\eta)$)

######  Lemma 12.

For all auxiliary continuations $Q$, renamings $\sigma$, and permutable
context instantiations $\eta$ such that, for all
$p\in\operatorname{dom}(\eta)$,
$\operatorname{supp}(\eta(p))\cap\operatorname{dom}(\sigma)=\emptyset$, there
exist an auxiliary continuation $O$ and a context instantiation $\theta$ such
that:

  1. (1)

$O=_{\alpha}Q$ and $O\theta=_{\alpha}Q\eta$

  2. (2)

$\theta=[p\mapsto\eta(p)\left[{\overrightarrow{y_{p}}}\middle/{\overrightarrow{x_{p}}}\right]\mid
p\in\operatorname{dom}(\eta)]$ for some
$\overrightarrow{x_{p}},\overrightarrow{y_{p}}$ (i.e. $\theta$ is equal to
$\eta$ up to a renaming of the free variables in its codomain)

  3. (3)

for all $Q^{\prime}$ such that
$Q\mathrel{\stackrel{{\scriptstyle\sigma}}{{\leadsto}}}Q^{\prime}$ with a non-
special reduction, there exists $O^{\prime}=_{\alpha}Q^{\prime}$ such that
$O\mathrel{\stackrel{{\scriptstyle\sigma}}{{\leadsto}}}O^{\prime}$ and we also
have $O\theta\mathrel{\leadsto}O^{\prime}\theta$

######  Proof 3.11.

By Lemma 11, we obtain $O$ and $\theta$ such that the alpha-equivalences and
the condition on $\theta$ hold. Furthermore, by the definition of
$\mathrel{\stackrel{{\scriptstyle\sigma}}{{\leadsto}}}$, we have
$O\mathrel{\leadsto}O^{\prime}\sigma$; then, again by Lemma 9, we obtain
$O\theta\mathrel{\leadsto}O^{\prime}\sigma\theta$; by Lemma 11, we know
$O^{\prime}\sigma\eta=O^{\prime}\eta^{\sigma}\sigma$; then the thesis
$O\theta\mathrel{\stackrel{{\scriptstyle\sigma}}{{\leadsto}}}O^{\prime}\eta^{\sigma}$
follows immediately by the definition of
$\mathrel{\stackrel{{\scriptstyle\sigma}}{{\leadsto}}}$.

######  Remark 13.

In [Coo09a], Cooper attempts to prove strong normalization for
$\mathit{NRC}_{\lambda}$ using a similar, but weaker result:

> If $K\mathrel{\leadsto}C$, then for all terms $M$ there exists
> $K^{\prime}_{M}$ such that $C[M]=K^{\prime}_{M}[M]$ and
> $K[M]\mathrel{\leadsto}K^{\prime}_{M}[M]$.

Since he does not have branching continuations and renaming reductions,
whenever a hole is duplicated, e.g.

$K=\bigcup\mathopen{\textbf{\\{}}{N_{1}\cup
N_{2}|x\leftarrow\Box}\mathclose{\textbf{\\}}}\mathrel{\leadsto}\bigcup\mathopen{\textbf{\\{}}{N_{1}|x\leftarrow\Box}\mathclose{\textbf{\\}}}\cup\bigcup\mathopen{\textbf{\\{}}{N_{2}|x\leftarrow\Box}\mathclose{\textbf{\\}}}=C$

he resorts to obtaining a continuation from $C$ simply by filling one of the
holes with the term $M$:

$K^{\prime}_{M}=\bigcup\mathopen{\textbf{\\{}}{N_{1}|x\leftarrow
M}\mathclose{\textbf{\\}}}\cup\bigcup\mathopen{\textbf{\\{}}{N_{2}|x\leftarrow\Box}\mathclose{\textbf{\\}}}$

Hence, $K^{\prime}_{M}[M]=C[M]$. Unfortunately, subsequent proofs rely on the
fact that $\nu(K)$ must decrease under reduction: since we have no control
over $\nu(M)$, which could potentially be much greater than $\nu(K)$, it may
be that $\nu(K^{\prime}_{M})\geq\nu(K)$.

In our setting, by combining Lemmas 8 and 12, we can find a $K^{\prime}$ which
is a proper contractum of $K$. By Lemma 4, we get $\nu(K^{\prime})<\nu(K)$, as
required by subsequent proofs.

More generally, the following lemma will help us in performing case analysis
on the reduction of an applied continuation.

######  Lemma 14 (classification of reductions in applied continuations).

Suppose $Q\eta\mathrel{\leadsto}N$, where $\eta$ is permutable, and
$\operatorname{dom}(\eta)\subseteq\operatorname{supp}(Q)$; then one of the
following holds:

  1. (1)

there exist an auxiliary continuation $Q^{\prime}$ and a finite map $\sigma$
such that $N=Q^{\prime}\eta^{\sigma}$,
$Q\mathrel{\stackrel{{\scriptstyle\sigma}}{{\leadsto}}}Q^{\prime}$ and, for
all $p\in\operatorname{dom}(\eta)$,
$\operatorname{supp}(\eta(p))\cap\operatorname{dom}(\sigma)=\emptyset$: we say
that this is a reduction of the continuation $Q$;

  2. (2)

there exist auxiliary continuations $Q_{1},Q_{2}$, an index
$q\in\operatorname{supp}(Q_{1})$, a variable $x$, and a term $L$ such that
$Q=(Q_{1}\mathop{\ooalign{\hfil\raise 0.86108pt\hbox{$\scriptscriptstyle
q$}\hfil\crcr{$\bigcirc$}}}\bigcup\mathopen{\textbf{\\{}}{\Box\mid
x\leftarrow\mathopen{\textbf{\\{}}{\overline{L}}\mathclose{\textbf{\\}}}}\mathclose{\textbf{\\}}})[q\mapsto
Q_{2}]$, $N=Q^{\prime}\eta^{*}$, and $Q\mathrel{\leadsto}Q^{\prime}$, where we
define $Q^{\prime}=Q_{1}[q\mapsto
Q_{2}\left[{\overline{L}}\middle/{x}\right]]$ and
$\eta^{*}(p)=\eta(p)\left[{\overline{L}}\middle/{x}\right]$ for all
$p\in\operatorname{supp}(Q_{2})$, otherwise $\eta^{*}(p)=\eta(p)$: this is a
special reduction of the continuation $Q$;

  3. (3)

there exists a permutable $\eta^{\prime}$ such that $N=Q\eta^{\prime}$ and
$\eta\mathrel{\leadsto}\eta^{\prime}$: in this case we say the reduction is
_within $\eta$_;

  4. (4)

there exist an auxiliary continuation $Q_{0}$, an index $p$ such that
$p\in\operatorname{supp}(Q_{0})$ and $p\in\operatorname{dom}(\eta)$, a frame
$F$ and a term $M$ such that $N=Q_{0}[p\mapsto M]\eta_{\lnot p}$,
$Q=Q_{0}\mathop{\ooalign{\hfil\raise 0.86108pt\hbox{$\scriptscriptstyle
p$}\hfil\crcr{$\bigcirc$}}}F$, and
$F^{p}[p\mapsto\eta(p)]\mathrel{\leadsto}M$: in this case we say the reduction
is _at the interface_.

Furthermore, if $Q$ is a regular continuation $K$, then the $Q^{\prime}$ in
case 1 can be chosen to be a regular continuation $K^{\prime}$, and case 2
cannot happen.

######  Proof 3.12.

By induction on $Q$ with a case analysis on the reduction rule applied. In
case 1, to satisfy the property relating $\eta$ and $\sigma$, we use Lemma 8
to generate a $\sigma$ such that the indices of its domain are fresh with
respect to the codomain of $\eta$. To see that this partition of reductions is
exhaustive, the most difficult part is to check that whenever we are in the
case of a reduction at the interface, there is a suitable $F$ such that $Q$
can be decomposed as $Q_{0}\mathop{\ooalign{\hfil\raise
0.86108pt\hbox{$\scriptscriptstyle p$}\hfil\crcr{$\bigcirc$}}}F$; while there
are some reduction rules for which we cannot find a suitable $F$, the
structure of $Q$ prevents these from happening at the interface between $Q$
and $\eta$: for example, in a reduction $(Q_{0}\mathop{\ooalign{\hfil\raise
0.86108pt\hbox{$\scriptscriptstyle
p$}\hfil\crcr{$\bigcirc$}}}(\Box~{}L))[p\mapsto\lambda
x.M]=Q_{0}[p\mapsto(\lambda x.M)~{}L]\mathrel{\leadsto}Q_{0}[p\mapsto
M\left[{L}\middle/{x}\right]]$, $(\Box~{}L)$ is not a valid frame: but we do
not have to consider this case, because $Q$ cannot be of the form
$Q_{0}\mathop{\ooalign{\hfil\raise 0.86108pt\hbox{$\scriptscriptstyle
p$}\hfil\crcr{$\bigcirc$}}}(\Box~{}L)$, since the latter is not a valid
auxiliary continuation.

For all context instantiations $\eta$, case 1 of the Lemma above generates a
renaming $\sigma$ satisfying the hypotheses of Lemma 11 and Lemma 12.
Additionally, the following result states that $\eta^{\sigma}$ must be
permutable.

######  Lemma 15.

Suppose that for all $p\in\operatorname{dom}(\eta)$,
$\operatorname{supp}(\eta(p))\cap\operatorname{dom}(\sigma)=\emptyset$. Then,
$\eta^{\sigma}$ is permutable.

######  Proof 3.13.

We need to prove that, for all $p\in\operatorname{dom}(\eta^{\sigma})$,
$\operatorname{supp}(\eta^{\sigma}(p))\cap\operatorname{dom}(\sigma)=\emptyset$.
If $p\in\operatorname{dom}(\eta^{\sigma})$, then
$\sigma(p)\in\operatorname{dom}(\eta)$; then, by hypothesis, we prove
$\operatorname{supp}(\eta(\sigma(p)))\cap\operatorname{dom}(\sigma)=\emptyset$.
Since $\eta(\sigma(p))=\eta^{\sigma}(p)$, this proves the thesis.

######  Lemma 16.

For all contexts $C$, context instantiations $\eta$, and sets of hole indices
$\mathcal{S}$, there exist a context $D$, a context instantiation $\theta$,
and a hole renaming $\sigma$ such that:

  * •

$D\sigma=C$ and $D\theta\sigma=C\eta$

  * •

the holes in $D$ are linear and
$\forall\mathop{\left[{q}\right]}\in\operatorname{FV}(D)$,
$q\notin\mathcal{S}$

  * •

$\operatorname{dom}(\theta)\cup\operatorname{dom}(\sigma)\subseteq\operatorname{FV}(D)$

  * •

$\theta$ is permutable

######  Proof 3.14 (Proof sketch).

If $C$ has $n$ hole occurrences, we generate $n$ distinct indices
$p_{1},\ldots,p_{n}$ (which we take to be fresh with respect to $\mathcal{S}$
and the free variables of the codomain of $\eta$) and replace each hole
occurrence within $C$ with a different $\mathop{\left[{p_{i}}\right]}$: this
induces a context $D$ and a renaming $\sigma$ such that $D\sigma=C$. By Lemma
11 we prove $C\eta=D\sigma\eta=D\eta^{\sigma}\sigma$ (we can apply this lemma
thanks to the careful choice of the $p_{i}$). We take
$\theta\triangleq\eta^{\sigma}$ and the remaining properties follow easily
(the permutability of $\theta$, again, descends from choosing sufficiently
fresh indices $p_{i}$).

######  Lemma 17.

Let $C_{1},C_{2}$ be contexts and $\eta_{1},\eta_{2}$ context instantiations.
Then for all free variables $x$ and sets of hole indices $\mathcal{S}$, there
exist a context $D$, a permutable context instantiation $\theta$, and a hole
renaming $\sigma$ such that:

  * •

$D\sigma=_{\alpha}C_{1}\left[{C_{2}}\middle/{x}\right]$ and
$D\theta\sigma=_{\alpha}(C_{1}\eta_{1})\left[{C_{2}\eta_{2}}\middle/{x}\right]$

  * •

The holes in $D$ are linear and fresh with respect to $S$

  * •

For all $q\in\operatorname{dom}(\theta)\cup\operatorname{dom}(\sigma)$,
$\mathop{\left[{q}\right]}\in\operatorname{FV}(D)$

  * •

$\theta$ is permutable

######  Proof 3.15.

The proof is by induction on the size of $C_{1}$, followed by a case analysis
on its structure. Here we consider the variable cases, lambda as a template
for binder cases, and application as a template for cases with multiple
subterms.

  * •

If $C_{1}=x$, we have $x\left[{C_{2}}\middle/{x}\right]=C_{2}$ and
$(x\eta_{1})\left[{C_{2}\eta_{2}}\middle/{x}\right]=C_{2}\eta_{2}$. By Lemma
17, we find $D,\theta,\sigma$ such that $D\sigma=C_{2}$,
$D\theta\sigma=C_{2}\eta_{2}$, the holes in $D$ are linear and arbitrarily
fresh, for all $q\in\operatorname{dom}(\theta)\cup\operatorname{dom}(\sigma)$,
$\mathop{\left[{q}\right]}\in\operatorname{FV}(D)$, and $\theta$ is
permutable; this proves the thesis.

  * •

If $C_{1}=\mathop{\left[{p}\right]}\in\operatorname{dom}(\eta_{1})$, then
$\mathop{\left[{p}\right]}\left[{C_{2}}\middle/{x}\right]=\mathop{\left[{p}\right]}$
and
$\mathop{\left[{p}\right]}\eta_{1}\left[{C_{2}\eta_{2}}\middle/{x}\right]=\eta_{1}(p)\left[{C_{2}\eta_{2}}\middle/{x}\right]$;
for all sets of hole indices $\mathcal{S}$, we choose $p^{*}\notin\mathcal{S}$
such that
$\mathop{\left[{p^{*}}\right]}\notin\operatorname{FV}(\eta_{1}(p)\left[{C_{2}\eta_{2}}\middle/{x}\right])$;
finally we choose $D=\mathop{\left[{p^{*}}\right]}$,
$\theta=[p^{*}\mapsto\eta_{1}(p)\left[{C_{2}\eta_{2}}\middle/{x}\right]]$, and
$\sigma=[p^{*}\mapsto p]$ and prove the thesis.

  * •

If $C_{1}$ is a free variable $y$ not covered by the previous cases, we choose
$D=y$, $\theta=[]$ (the empty instantiation), $\sigma=[]$ (the empty renaming)
to trivially prove the thesis.

  * •

If $C_{1}=\lambda y.C_{0}$, let us choose a variable
$y^{*}\notin\\{{x}\\}\cup\operatorname{FV}(C_{2}\eta_{2})$, such that $y^{*}$
is not a hole; let us define the following abbreviations:

$C_{0}^{*}\triangleq
C_{0}\left[{y^{*}}\middle/{y}\right]\qquad\eta_{1}^{*}\triangleq[p\mapsto\eta_{1}(p)\left[{y^{*}}\middle/{y}\right]|p\in\operatorname{dom}(\eta_{1})]$

Since $C_{0}^{*}$ is equal to $C_{0}$ up to a renaming, it is smaller than
$C_{1}$ and by induction hypothesis we get that there exist
$D_{0},\theta_{0},\sigma_{0}$ such that
$D_{0}\sigma_{0}=_{\alpha}C_{0}^{*}\left[{C_{2}}\middle/{x}\right]$ and
$D_{0}\theta_{0}\sigma_{0}=_{\alpha}C_{0}^{*}\eta_{1}^{*}\left[{C_{2}\eta_{2}}\middle/{x}\right]$,
where the holes in $D_{0}$ are linear and arbitrarily fresh, for all
$q\in\operatorname{dom}(\theta_{0})\cup\operatorname{dom}(\sigma_{0})$ we have
$\mathop{\left[{q}\right]}\in\operatorname{FV}(D_{0})$, and $\theta_{0}$ is
permutable. Then we can choose $D=\lambda y^{*}.D_{0}$, $\theta=\theta_{0}$,
$\sigma=\sigma_{0}$ and show that:

$\begin{array}[]{rll}D\sigma&=&(\lambda y^{*}.D_{0})\sigma_{0}\\\ &=&\lambda
y^{*}.D_{0}\sigma_{0}\\\ &=_{\alpha}&\lambda
y^{*}.C_{0}^{*}\left[{C_{2}}\middle/{x}\right]\\\ &=&(\lambda
y.C_{0})\left[{C_{2}}\middle/{x}\right]\\\ D\theta\sigma&=&(\lambda
y^{*}.D_{0})\theta_{0}\sigma_{0}\\\ &=&\lambda
y^{*}.D_{0}\theta_{0}\sigma_{0}\\\ &=_{\alpha}&\lambda
y^{*}.C_{0}^{*}\eta_{1}^{*}\left[{C_{2}\eta_{2}}\middle/{x}\right]\\\
&=&(\lambda y.C_{0}\eta_{1})\left[{C_{2}\eta_{2}}\middle/{x}\right]\\\
&=&(\lambda
y.C_{0})\eta_{1}\left[{C_{2}\eta_{2}}\middle/{x}\right]\end{array}$

We can easily show that the other required properties of $D,\theta,\sigma$ are
verified, thus proving the thesis.

  * •

If $C_{1}=(C_{11}~{}C_{12})$, then  (C_11 C_12)[C_2/x] = (C_11[C_2/x]
C_12[C_2/x]) and (C_11 C_12η_1)[C_2η_2/x] = (C_11η_1[C_2η_2/x]
C_12η_1[C_2η_2/x]); by the induction hypothesis, we find
$D_{11},\theta_{11},\sigma_{11}$ and $D_{12},\theta_{12},\sigma_{12}$ such
that $D_{11}\sigma_{11}=_{\alpha}C_{11}\left[{C_{2}}\middle/{x}\right]$,
$D_{11}\theta_{11}\sigma_{11}=_{\alpha}C_{11}\eta_{1}\left[{C_{2}\eta_{2}}\middle/{x}\right]$:
we are allowed to choose these expressions in such a way that the holes in the
$D_{i}$ are fresh, so we ensure that the sets of holes of $D_{11}$ and
$D_{12}$ are disjoint – this in turn ensures that $\theta_{11},\theta_{12}$
and $\sigma_{11},\sigma_{12}$ can be combined together, since their domains
are also disjoint. Then we choose $D=(D_{11}~{}D_{12})$,
$\theta=\theta_{11}\theta_{12}$, $\sigma=\sigma_{11}\sigma_{12}$ and show
that;

$\begin{array}[]{rll}D\sigma&=&(D_{11}~{}D_{12})\sigma_{11}\sigma_{12}\\\
&=&(D_{11}\sigma_{11}\sigma_{12}~{}D_{12}\sigma_{11}\sigma_{12})\\\
&=&(D_{11}\sigma_{11}~{}D_{12}\sigma_{12})\\\
&=_{\alpha}&(C_{11}\left[{C_{2}}\middle/{x}\right]~{}C_{12}\left[{C_{2}}\middle/{x}\right])\\\
D\theta\sigma&=&(D_{11}~{}D_{12})\theta_{11}\theta_{12}\sigma_{11}\sigma_{12}\\\
&=&(D_{11}\theta_{11}\theta_{12}\sigma_{11}\sigma_{12}~{}D_{12}\theta_{11}\theta_{12}\sigma_{11}\sigma_{12})\\\
&=&(D_{11}\theta_{11}\sigma_{11}~{}D_{12}\theta_{12}\sigma_{12})\\\
&=_{\alpha}&(C_{11}\eta_{1}\left[{C_{2}\eta_{2}}\middle/{x}\right]~{}C_{12}\eta_{1}\left[{C_{2}\eta_{2}}\middle/{x}\right])\end{array}$

Furthermore, the induction hypothesis provides enough information on the
$D_{i},\theta_{i},\sigma_{i}$ to guarantee that the holes in $D$ are linear
and arbitrarily fresh, for all
$q\in\operatorname{dom}(\theta)\cup\operatorname{dom}(\sigma)$ we have
$\mathop{\left[{q}\right]}\in\operatorname{FV}(D)$, and $\theta$ is
permutable, as required.

######  Lemma 18.

Let $C,C^{\prime}$ be contexts such that $C\mathrel{\leadsto}C^{\prime}$;
then, for all context instantiations $\eta$, there exist a context $D$,
context instantiation $\theta$, and renaming $\sigma$ such that
$D\sigma=_{\alpha}C^{\prime}$ (and consequently
$C\mathrel{\stackrel{{\scriptstyle\sigma}}{{\leadsto}}}D$) and
$C\eta\mathrel{\stackrel{{\scriptstyle\sigma}}{{\leadsto}}}D\theta$.

######  Proof 3.16.

By structural induction on the derivation of $C\mathrel{\leadsto}C^{\prime}$.
The property we need to prove essentially states that any reduction of $C$ can
still be performed after applying any instantiation $\eta$; however, due to
variable capture and the possibility that some redexes of $C$ may be blocked
in $C\eta$, the statement is complicated by explicit alpha-conversions and
hole renamings. We present here the two interesting cases of the proof:

  * •

$(\lambda
x.C_{1})~{}C_{2}\mathrel{\leadsto}C_{1}\left[{C_{2}}\middle/{x}\right]$: by
Lemma 17 we obtain $D,\theta,\sigma$ such that
$D\sigma=_{\alpha}C_{1}\left[{C_{2}}\middle/{x}\right]$ and
$D\theta\sigma=_{\alpha}(C_{1}\eta)\left[{C_{2}\eta}\middle/{x}\right]$; since
$((\lambda x.C_{1})~{}C_{2})\eta=(\lambda
x.C_{1}\eta)~{}(C_{2}\eta)\mathrel{\leadsto}(C_{1}\eta)\left[{C_{2}\eta}\middle/{x}\right]=_{\alpha}D\theta\sigma$,
we have $((\lambda
x.C_{1})~{}C_{2})\eta\mathrel{\stackrel{{\scriptstyle\sigma}}{{\leadsto}}}D\theta$.

  * •

$\bigcup\mathopen{\textbf{\\{}}{C_{1}\mid
x\leftarrow\bigcup\mathopen{\textbf{\\{}}{C_{2}\mid y\leftarrow
C_{3}}\mathclose{\textbf{\\}}}}\mathclose{\textbf{\\}}}\mathrel{\leadsto}\bigcup\mathopen{\textbf{\\{}}{C_{1}\mid
y\leftarrow C_{3},x\leftarrow C_{2}}\mathclose{\textbf{\\}}}$, where
$y\notin\operatorname{FV}(C_{1})$: let us choose a variable
$y^{*}\notin\operatorname{FV}(C_{1}\eta)$ and define $C^{*}_{2}\triangleq
C_{2}\left[{y^{*}}\middle/{y}\right]$ and
$\eta^{*}=[p\mapsto\eta(p)\left[{y^{*}}\middle/{y}\right]|p\in\operatorname{dom}(\eta)]$:
then we can alpha-rename the contractum as

$\bigcup\mathopen{\textbf{\\{}}{C_{1}\mid y\leftarrow C_{3},x\leftarrow
C_{2}}\mathclose{\textbf{\\}}}=_{\alpha}\bigcup\mathopen{\textbf{\\{}}{C_{1}\mid
y^{*}\leftarrow C_{3},x\leftarrow C^{*}_{2}}\mathclose{\textbf{\\}}}$

By repeated applications of Lemma 16, we obtain contexts
$C^{\prime}_{1},C^{\prime}_{2},C^{\prime}_{3}$, context instantiations
$\eta^{\prime}_{1},\eta^{\prime}_{2},\eta^{\prime}_{3}$, and renamings
$\sigma_{1},\sigma_{2},\sigma_{3}$, such that
$\bigcup\mathopen{\textbf{\\{}}{C^{\prime}_{1}\mid y\leftarrow
C^{\prime}_{3},x\leftarrow C^{\prime}_{2}}\mathclose{\textbf{\\}}}$ has
linear, arbitrarily fresh holes, for $i=1,2,3$ we have
$\operatorname{dom}(\eta^{\prime}_{i})\cup\operatorname{dom}(\sigma_{i})\subseteq\operatorname{FV}(C^{\prime}_{i})$
and $\eta^{\prime}_{i}$ is permutable, and such that:

$\begin{array}[]{c}C^{\prime}_{1}\sigma_{1}=C_{1}\qquad
C^{\prime}_{2}\sigma_{1}=C^{*}_{2}\qquad\qquad
C^{\prime}_{3}\sigma_{3}=C_{3}\\\
C^{\prime}_{1}\eta^{\prime}_{1}\sigma_{1}=C_{1}\eta\qquad
C^{\prime}_{2}\eta^{\prime}_{2}\sigma_{2}=C^{*}_{2}\eta^{*}\qquad
C^{\prime}_{3}\eta^{\prime}_{3}\sigma_{3}=C_{3}\eta\end{array}$

Then we take $D\triangleq\bigcup\mathopen{\textbf{\\{}}{C^{\prime}_{1}\mid
y^{*}\leftarrow C^{\prime}_{3},x\leftarrow
C^{\prime}_{2}}\mathclose{\textbf{\\}}}$,
$\theta=\eta^{\prime}_{1}\eta^{\prime}_{2}\eta^{\prime}_{3}$ and
$\sigma=\sigma_{1}\sigma_{2}\sigma_{3}$. We prove:

$\begin{array}[]{rll}D\sigma&=&\bigcup\mathopen{\textbf{\\{}}{C^{\prime}_{1}\sigma_{1}\mid
y^{*}\leftarrow C^{\prime}_{3}\sigma_{3},x\leftarrow
C^{\prime}_{2}\sigma_{2}}\mathclose{\textbf{\\}}}\\\
&=&\bigcup\mathopen{\textbf{\\{}}{C_{1}\mid y^{*}\leftarrow C_{3},x\leftarrow
C^{*}_{2}}\mathclose{\textbf{\\}}}\\\
&=_{\alpha}&\bigcup\mathopen{\textbf{\\{}}{C_{1}\mid y\leftarrow
C_{3},x\leftarrow C_{2}}\mathclose{\textbf{\\}}}\\\
D\theta\sigma&=&\bigcup\mathopen{\textbf{\\{}}{C^{\prime}_{1}\eta^{\prime}_{1}\sigma_{1}\mid
y^{*}\leftarrow C^{\prime}_{3}\eta^{\prime}_{3}\sigma_{3},x\leftarrow
C^{\prime}_{2}\eta^{\prime}_{2}\sigma_{2}}\mathclose{\textbf{\\}}}\\\
&=&\bigcup\mathopen{\textbf{\\{}}{C_{1}\eta\mid y^{*}\leftarrow
C_{3}\eta,x\leftarrow C^{*}_{2}\eta^{*}}\mathclose{\textbf{\\}}}\end{array}$

By the last equality, we have $\bigcup\mathopen{\textbf{\\{}}{C_{1}\mid
y^{*}\leftarrow C_{3},x\leftarrow
C^{*}_{2}}\mathclose{\textbf{\\}}}\mathrel{\leadsto}D\theta\sigma$, which by
definition is $\bigcup\mathopen{\textbf{\\{}}{C_{1}\mid y^{*}\leftarrow
C_{3},x\leftarrow
C^{*}_{2}}\mathclose{\textbf{\\}}}\mathrel{\stackrel{{\scriptstyle\sigma}}{{\leadsto}}}D\theta$.

The following result, like many others in the rest of this section, proceeds
by well-founded induction; we will use the following notation to represent
well-founded relations:

  * •

$<$ stands for the standard less-than relation on $\mathbb{N}$, which is well-
founded;

  * •

$\lessdot$ is the lexicographic extension of $<$ to $k$-tuples in
$\mathbb{N}^{k}$ (for a given $k$), also well-founded;

  * •

$\prec$ will be used to provide a decreasing metric that depends on the
specific proof: such metrics are defined as subsets of $\lessdot$ and are thus
well-founded.

######  Lemma 19.

Let $C$ be a context and $\eta$ a context instantiation such that
$C\eta\in\mathcal{S}\mathcal{N}$. Then we have:

  1. (1)

$C\in\mathcal{S}\mathcal{N}$

  2. (2)

$\nu(C)\leq\nu(C\eta)$

  3. (3)

for all $p\in\operatorname{dom}(\eta)$, if
$\mathop{\left[{p}\right]}\in\operatorname{FV}(C)$, then
$\eta(p)\in\mathcal{S}\mathcal{N}$.

######  Proof 3.17.

Property 3 follows immediately by induction on $\nu(C\eta)$ by noticing that,
since $\mathop{\left[{p}\right]}\in\operatorname{FV}(C)$ implies that
$\eta(p)$ appears as a subexpression of $C\eta$, and since reduction is
defined by congruence closure, every reduction of $\eta(p)$ can be mimicked by
a corresponding reduction within $C\eta$.

To prove the first two properties, we proceed by well-founded induction on
$(C,\eta)$ using the metric:

$(C_{1},\eta_{1})\prec(C_{2},\eta_{2})\iff\exists\sigma:C_{2}\eta_{2}\mathrel{\stackrel{{\scriptstyle\sigma}}{{\leadsto}}}C_{1}\eta_{1}$

We consider all the possible contractions $C\mathrel{\leadsto}C^{\prime}$. By
Lemma 18, we find $D,\sigma,\theta$ such that
$C\eta\mathrel{\stackrel{{\scriptstyle\sigma}}{{\leadsto}}}D\theta$ and
$D\sigma=_{\alpha}C^{\prime}$; consequently,
$C\mathrel{\stackrel{{\scriptstyle\sigma}}{{\leadsto}}}D$. By induction
hypothesis we obtain $D\in\mathcal{S}\mathcal{N}$ and
$\nu(D)\leq\nu(D\theta)<\nu(C\eta)$; we easily prove
$D\sigma=_{\alpha}C^{\prime}\in\mathcal{S}\mathcal{N}$ and
$\nu(C^{\prime})=\nu(D)$. Furthermore, since
$\nu(C)=1+\max_{C^{\prime}:C\mathrel{\leadsto}C^{\prime}}\nu(C^{\prime})$ and
for all such $C^{\prime}$ we have proved $\nu(C^{\prime})<\nu(C\eta)$, we get
$\nu(C)\leq\nu(C\eta)$.

A similar property about the composition of continuations and frames follows
immediately.

######  Corollary 20.

If $Q\mathop{\ooalign{\hfil\raise 0.86108pt\hbox{$\scriptscriptstyle
p$}\hfil\crcr{$\bigcirc$}}}F\in\mathcal{S}\mathcal{N}$, then
$Q\in\mathcal{S}\mathcal{N}$ and $\nu(Q)\leq\nu(Q\mathop{\ooalign{\hfil\raise
0.86108pt\hbox{$\scriptscriptstyle p$}\hfil\crcr{$\bigcirc$}}}F)$.

######  Proof 3.18.

By definition, $Q\mathop{\ooalign{\hfil\raise
0.86108pt\hbox{$\scriptscriptstyle p$}\hfil\crcr{$\bigcirc$}}}F=Q[p\mapsto
F^{p}]$: then we use Lemma 19, with $\eta=[p\mapsto F^{p}]$.

######  Lemma 21.

Let $Q$ be an auxiliary continuation, and let $\eta,\theta$ be context
instantiations s.t. their union is permutable. If
$Q\eta\in\mathcal{S}\mathcal{N}$ and $Q\theta\in\mathcal{S}\mathcal{N}$, then
$Q\eta\theta\in\mathcal{S}\mathcal{N}$.

######  Proof 3.19.

We assume that
$\operatorname{dom}(\eta)\cup\operatorname{dom}(\theta)\subseteq\operatorname{supp}(Q)$
(otherwise, we can find strictly smaller permutable
$\eta^{\prime},\theta^{\prime}$ such that
$Q\eta\theta=Q\eta^{\prime}\theta^{\prime}$, and their domains are subsets of
$\operatorname{supp}(Q)$). We show $Q\eta\in\mathcal{S}\mathcal{N}$ and
$Q\theta\in\mathcal{S}\mathcal{N}$ imply $Q\in\mathcal{S}\mathcal{N}$,
$\eta\in\mathcal{S}\mathcal{N}$ and $\theta\in\mathcal{S}\mathcal{N}$; thus we
can then prove the theorem by well-founded induction on $(Q,\eta,\theta)$
using the following metric:

$(Q_{1},\eta_{1},\theta_{1})\prec(Q_{2},\eta_{2},\theta_{2})\iff(\nu(Q_{1}),\left\|Q_{1}\right\|,\nu(\eta_{1})+\nu(\theta_{1}))\lessdot(\nu(Q_{2}),\left\|Q_{2}\right\|,\nu(\eta_{2})+\nu(\theta_{2}))$

We show that all of the possible contracta of $Q\eta\theta$ are s.n. by case
analysis on the contraction:

  * •

$Q^{\prime}\eta^{\sigma}\theta^{\sigma}$, where
$Q\mathrel{\stackrel{{\scriptstyle\sigma}}{{\leadsto}}}Q^{\prime}$: it is easy
to see that $\nu(\eta^{\sigma})$ and $\nu(\theta^{\sigma})$ are defined
because $\nu(\eta)$ and $\nu(\theta)$ are; then the thesis follows from the
induction hypothesis, knowing that $\nu(Q^{\prime})<\nu(Q)$ (Lemma 4).

  * •

$Q^{\prime}\eta^{*}\theta^{*}$ where $Q^{\prime}=Q_{1}[q\mapsto
Q_{2}\left[{\overline{L}}\middle/{x}\right]]$, for some
$Q_{1},Q_{2},x,q\in\operatorname{supp}(Q_{1}),\eta^{*},\theta^{*}$ such that
$Q=(Q_{1}\mathop{\ooalign{\hfil\raise 0.86108pt\hbox{$\scriptscriptstyle
q$}\hfil\crcr{$\bigcirc$}}}\bigcup\mathopen{\textbf{\\{}}{\Box\mid
x\leftarrow\mathopen{\textbf{\\{}}{\overline{L}}\mathclose{\textbf{\\}}}}\mathclose{\textbf{\\}}})[q\mapsto
Q_{2}]$ and $\eta^{*}(p)=\eta(p)\left[{\overline{L}}\middle/{x}\right]$,
$\theta^{*}(p)=\theta(p)\left[{\overline{L}}\middle/{x}\right]$ for all
$p\in\operatorname{supp}(Q_{2})$, otherwise $\eta^{*}(p)=\eta(p)$ and
$\theta^{*}(p)=\theta(p)$; since $Q\mathrel{\leadsto}Q^{\prime}$, we know
$\nu(Q^{\prime})<\nu(Q)$; furthermore, since
$Q\eta\mathrel{\leadsto}Q^{\prime}\eta^{*}$ and
$Q\eta\in\mathcal{S}\mathcal{N}$, it is easy to see that
$Q^{\prime}\eta^{*}\in\mathcal{S}\mathcal{N}$ and $\nu(\eta^{*})$ is defined;
similarly, $Q^{\prime}\theta^{*}\in\mathcal{S}\mathcal{N}$ and
$\nu(\theta^{*})$ is defined; then
$Q^{\prime}\eta^{*}\theta^{*}\in\mathcal{S}\mathcal{N}$ by induction
hypothesis.

  * •

$Q\eta^{\prime}\theta$, where $\eta\mathrel{\leadsto}\eta^{\prime}$: the
thesis follows by induction hypothesis, knowing $\nu(\eta^{\prime})<\nu(\eta)$
(Lemma 4).

  * •

$Q_{0}[p\mapsto N]\eta_{0}\theta$ where $Q=Q_{0}\mathop{\ooalign{\hfil\raise
0.86108pt\hbox{$\scriptscriptstyle p$}\hfil\crcr{$\bigcirc$}}}F$,
$\eta=[p\mapsto M]\eta_{0}$, and $F^{p}[p\mapsto M]\mathrel{\leadsto}N$ by
means of a reduction at the interface. By Lemma 20 we know
$\nu(Q_{0})\leq\nu(Q)$; by Lemma 3 we prove
$\left\|Q_{0}\right\|<\left\|Q\right\|$. We take $\eta^{\prime}=[p\mapsto
N]\eta_{0}$: since $Q\eta$ reduces to $Q_{0}\eta^{\prime}$ and both terms are
strongly normalizing, we have that $\nu(\eta^{\prime})$ is defined. Then we
observe $(Q_{0},\eta^{\prime},\theta)\prec(Q,\eta,\theta)$ and obtain the
thesis by induction hypothesis. A symmetric case with
$p\in\operatorname{dom}(\theta)$ is proved similarly.

######  Corollary 22.

$Q[p\mapsto M]^{\sigma}\in\mathcal{S}\mathcal{N}$ iff for all $q$ s.t.
$\sigma(q)=p$, we have $Q[q\mapsto M]\in\mathcal{S}\mathcal{N}$.

######  Proof 3.20.

By the definition of $[p\mapsto M]^{\sigma}$, using Lemma 21 to decompose the
resulting context instantiation.

###  3.3. Candidates of reducibility

We here define the notion of _candidates of reducibility_ : sets of strongly
normalizing terms enjoying certain closure properties that can be used to
overapproximate the sets of terms of a certain type. Our version of candidates
for $\mathit{NRC}_{\lambda}$ is a straightforward adaptation of the standard
definition given by Girard and like that one is based on a notion of _neutral
terms_ , i.e. those terms that, when placed in an arbitrary context, do not
create additional redexes.

[neutral term] A term $M$ is _neutral_ if it belongs to the following grammar:

$W\mathrel{::=}x\mathbin{~{}|~{}}c(\overrightarrow{M_{n}})\mathbin{~{}|~{}}M.\ell\mathbin{~{}|~{}}(M~{}N)\mathbin{~{}|~{}}\mathtt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}empty}~{}M$

where $n\geq 1$.

The set of neutral terms is denoted by $\mathcal{N}\mathcal{T}$.

Let us introduce the following notation for Girard’s CRx properties of sets
[GLT89]:

  * •

$\mathrm{CR1}(\mathcal{C})\triangleq\mathcal{C}\subseteq\mathcal{S}\mathcal{N}$

  * •

$\mathrm{CR2}(\mathcal{C})\triangleq\forall M\in\mathcal{C},\forall
M^{\prime}.M\mathrel{\leadsto}M^{\prime}\mathrel{\Longrightarrow}M^{\prime}\in\mathcal{C}$

  * •

$\mathrm{CR3}(\mathcal{C})\triangleq\forall
M\in\mathcal{N}\mathcal{T}.(\forall
M^{\prime}.M\mathrel{\leadsto}M^{\prime}\mathrel{\Longrightarrow}M^{\prime}\in\mathcal{C})\mathrel{\Longrightarrow}M\in\mathcal{C}$

The set $\mathcal{C}\mathcal{R}$ of the candidates of reducibility is then
defined as the collection of those sets of terms which satisfy all the CRx
properties. Some standard results include the non-emptiness of candidates (in
particular, all free variables are in every candidate) and that
$\mathcal{S}\mathcal{N}\in\mathcal{C}\mathcal{R}$.

###  3.4. Reducibility sets

In this section we introduce _reducibility sets_ , which are sets of terms
that we will use to provide an interpretation of the types of
$\mathit{NRC}_{\lambda}$; we will then prove that reducibility sets are
candidates of reducibility, hence they only contain strongly normalizing
terms. The following notation will be useful as a shorthand for certain
operations on sets of terms that are used to define reducibility sets:

  * •

$\mathcal{C}\to\mathcal{D}\triangleq\\{{M:\forall
N\in\mathcal{C},(M~{}N)\in\mathcal{D}}\\}$

  * •

$\langle{\overrightarrow{\ell_{k}:\mathcal{C}_{k}}}\rangle\triangleq\\{{M:\forall
i=1,\ldots,k,M.\ell_{i}\in\mathcal{C}_{i}}\\}$

  * •

$\mathcal{C}_{p}^{\top}\triangleq\\{{K:\forall
M\in\mathcal{C}.K[p\mapsto\mathopen{\textbf{\\{}}{M}\mathclose{\textbf{\\}}}]\in\mathcal{S}\mathcal{N}}\\}$

  * •

$\mathcal{C}^{\top\top}\triangleq\\{{M:\forall p,\forall
K\in\mathcal{C}_{p}^{\top},K[p\mapsto M]\in\mathcal{S}\mathcal{N}}\\}$

The sets $\mathcal{C}_{p}^{\top}$ and $\mathcal{C}^{\top\top}$ are called the
_$\top$ -lifting_ and _$\top\top$ -lifting_ of $\mathcal{C}$. These
definitions refine the ones used in the literature by using indices:
$\top$-lifting is defined with respect to a given index $p$, while the
definition of $\top\top$-lifting uses any index (in the standard definitions,
continuations only contain a single hole, and no indices are mentioned).

[reducibility] For all types $T$, the set $\mathsf{Red}_{T}$ of reducible
terms of type $T$ is defined by recursion on $T$ by means of the rules:

$\begin{array}[]{rclcrcl}\mathsf{Red}_{A}&\triangleq&\mathcal{S}\mathcal{N}&&\mathsf{Red}_{S\to
T}&\triangleq&\mathsf{Red}_{S}\to\mathsf{Red}_{T}\\\
\mathsf{Red}_{\langle{\overrightarrow{\ell_{k}:T_{k}}}\rangle}&\triangleq&\langle{\overrightarrow{\ell_{k}:\mathsf{Red}_{T_{k}}}}\rangle&&\mathsf{Red}_{\mathopen{\textbf{\\{}}{T}\mathclose{\textbf{\\}}}}&\triangleq&\mathsf{Red}_{T}^{\top\top}\end{array}$

Let us use metavariables $\mathcal{S},\mathcal{S}^{\prime},\ldots$ to denote
finite sets of indices: we provide a refined notion of $\top$-lifting
$\mathcal{C}_{\mathcal{S}}^{\top}$ depending on a set of indices rather than a
single index, defined by pointwise intersection. This notation is useful to
track a $\top$-lifted candidate under renaming reduction.
$\mathcal{C}_{\mathcal{S}}^{\top}\triangleq\bigcap_{p\in\mathcal{S}}\mathcal{C}_{p}^{\top}$.

Let $\mathcal{C}$ and $\mathcal{S}$ be sets of terms and indices respectively,
and $\sigma$ a finite renaming: then we define
$(\mathcal{C}_{\mathcal{S}}^{\top})^{\sigma}:=\mathcal{C}_{\sigma^{-1}(\mathcal{S})}^{\top}$,
where $\sigma^{-1}(\mathcal{S})=\\{{q:\sigma(q)\in\mathcal{S}}\\}$

We now proceed with the proof that all the sets $\mathsf{Red}_{T}$ are
candidates of reducibility: we will only focus on collections since for the
other types the result is standard. The proofs of $\mathrm{CR1}$ and
$\mathrm{CR2}$ do not differ much from the standard $\top\top$-lifting
technique.

######  Lemma 23.

Suppose $\mathrm{CR1}(\mathcal{C})$: then for all indices $p,q$,
$\mathop{\left[{p}\right]}\in\mathcal{C}_{q}^{\top}$.

######  Proof 3.21.

To prove the lemma, it is sufficient to show that for all $M\in\mathcal{C}$ we
have
$\mathop{\left[{p}\right]}[q\mapsto\mathopen{\textbf{\\{}}{M}\mathclose{\textbf{\\}}}]\in\mathcal{S}\mathcal{N}$.
This term is equal to either
$\mathopen{\textbf{\\{}}{M}\mathclose{\textbf{\\}}}$ (if $p=q$) or to
$\mathop{\left[{p}\right]}$ (otherwise); both terms are s.n. (in the case of
$\mathopen{\textbf{\\{}}{M}\mathclose{\textbf{\\}}}$, this is because
$\mathrm{CR1}$ holds for $\mathcal{C}$, thus $M\in\mathcal{S}\mathcal{N}$).

######  Lemma 24 (CR1 for continuations).

For all $p$ and all non-empty $\mathcal{C}$,
$\mathcal{C}_{p}^{\top}\subseteq\mathcal{S}\mathcal{N}$.

######  Proof 3.22.

We assume $K\in\mathcal{C}_{p}^{\top}$ and $M\in\mathcal{C}$: by definition,
we know that
$K[p\mapsto\mathopen{\textbf{\\{}}{M}\mathclose{\textbf{\\}}}]\in\mathcal{S}\mathcal{N}$;
then we have $K\in\mathcal{S}\mathcal{N}$ by Lemma 19.

######  Lemma 25 (CR1 for collections).

If $\mathrm{CR1}(\mathcal{C})$, then $\mathrm{CR1}(\mathcal{C}^{\top\top})$.

######  Proof 3.23.

We need to prove that if $M\in\mathcal{C}^{\top\top}$, then
$M\in\mathcal{S}\mathcal{N}$. By the definition of $\mathcal{C}^{\top\top}$,
we know that for all $p$, $K[p\mapsto M]\in\mathcal{S}\mathcal{N}$ whenever
$K\in\mathcal{C}_{p}^{\top}$. Now assume any $p$, and by Lemma 23 choose
$K=\mathop{\left[{p}\right]}$: then $K[p\mapsto
M]=M\in\mathcal{S}\mathcal{N}$, which proves the thesis.

######  Lemma 26 (CR2 for collections).

If $M\in\mathcal{C}^{\top\top}$ and $M\mathrel{\leadsto}M^{\prime}$, then
$M^{\prime}\in\mathcal{C}^{\top\top}$.

######  Proof 3.24.

Let $p$ be an index, and take $K\in\mathcal{C}_{p}^{\top}$: we need to prove
$K[p\mapsto M^{\prime}]\in\mathcal{S}\mathcal{N}$. By the definition of
$M\in\mathcal{C}^{\top\top}$, we have $K[p\mapsto
M]\in\mathcal{S}\mathcal{N}$; if $p\notin\operatorname{supp}(K)$, $K[p\mapsto
M^{\prime}]=K[p\mapsto M]$ and the thesis trivially holds; otherwise the
instantiation is effective and we have $K[p\mapsto
M]\mathrel{\leadsto}K[p\mapsto M^{\prime}]$, and this last term, being a
contractum of a strongly normalizing term, is strongly normalizing as well.
This proves the thesis.

In order to prove $\mathrm{CR2}$ for all types (and particularly for
collections), we do not need to establish an analogous property on
continuations; however such a property is still useful for subsequent results
(particularly $\mathrm{CR3}$). Its statement must, of course, consider that
reduction may duplicate (or indeed delete) holes, and thus employs renaming
reduction. We can show that whenever we need to prove a statement about
$n$-ary permutable instantiations of $n$-ary continuations, we can simply
consider each hole separately, as stated in the following lemma.

######  Lemma 27.

$K\in(\mathcal{C}_{\mathcal{S}}^{\top})^{\sigma}$ if, and only if, for all
$q\in\sigma^{-1}(\mathcal{S})$, we have $K\in\mathcal{C}_{q}^{\top}$.
In particular, $K\in(\mathcal{C}_{p}^{\top})^{\sigma}$ if, and only if, for
all $q$ s.t. $\sigma(q)=p$, we have $K\in\mathcal{C}_{q}^{\top}$.

######  Proof 3.25.

By definition of $(\cdot)^{\sigma}$ and $(\cdot)^{\top}$:

$K\in(\mathcal{C}^{\top}_{\mathcal{S}})^{\sigma}\iff
K\in\mathcal{C}^{\top}_{\sigma^{-1}(\mathcal{S})}\iff
K\in\bigcap_{q\in\sigma^{-1}(\mathcal{S})}\mathcal{C}^{\top}_{q}\iff\forall
q\in\sigma^{-1}(\mathcal{S}),K\in\mathcal{C}^{\top}_{q}$

######  Lemma 28 (CR2 for continuations).

If $K\in\mathcal{C}_{\mathcal{S}}^{\top}$ and
$K\mathrel{\stackrel{{\scriptstyle\sigma}}{{\leadsto}}}K^{\prime}$, then
$K^{\prime}\in(\mathcal{C}_{\mathcal{S}}^{\top})^{\sigma}$.

######  Proof 3.26.

By Lemma 27 and the definition of $(\cdot)^{\top}$, it suffices to prove that
$K^{\prime}[q\mapsto\mathopen{\textbf{\\{}}{M}\mathclose{\textbf{\\}}}]\in\mathcal{S}\mathcal{N}$
for all $q$ such that $\sigma(q)\in\mathcal{S}$ and $M\in\mathcal{C}$. Then we
know
$K[\sigma(q)\mapsto\mathopen{\textbf{\\{}}{M}\mathclose{\textbf{\\}}}]\in\mathcal{S}\mathcal{N}$,
and consequently
$K^{\prime}[\sigma(q)\mapsto\mathopen{\textbf{\\{}}{M}\mathclose{\textbf{\\}}}]^{\sigma}\in\mathcal{S}\mathcal{N}$
as well, since the latter is a contractum of the former; finally, by Corollary
22,
$K^{\prime}[q\mapsto\mathopen{\textbf{\\{}}{M}\mathclose{\textbf{\\}}}]\in\mathcal{S}\mathcal{N}$,
as we needed.

This is everything we need to prove $\mathrm{CR3}$.

######  Lemma 29 (CR3 for collections).

Let $\mathcal{C}\in\mathcal{C}\mathcal{R}$, and $M$ a neutral term such that
for all reductions $M\mathrel{\leadsto}M^{\prime}$ we have
$M^{\prime}\in\mathcal{C}^{\top\top}$. Then $M\in\mathcal{C}^{\top\top}$.

######  Proof 3.27.

By definition, we need to prove $K[p\mapsto M]\in\mathcal{S}\mathcal{N}$
whenever $K\in\mathcal{C}_{p}^{\top}$ for some index $p$. By Lemma 24, knowing
that $\mathcal{C}$, being a candidate, is non-empty, we have
$K\in\mathcal{S}\mathcal{N}$. We can thus proceed by well-founded induction on
$\nu(K)$ to prove the strengthened statement: for all indices $q$, if
$K\in\mathcal{C}_{q}^{\top}$, then $K[q\mapsto M]\in\mathcal{S}\mathcal{N}$.
Equivalently, we prove that all the contracta of $K[q\mapsto M]$ are s.n. by
cases on the possible contracta:

  * •

$K^{\prime}[q\mapsto M]^{\sigma}$ (where
$K\mathrel{\stackrel{{\scriptstyle\sigma}}{{\leadsto}}}K^{\prime}$): to prove
this term is s.n., by Corollary 22, we need to show
$K^{\prime}[q^{\prime}\mapsto M]\in\mathcal{S}\mathcal{N}$ whenever
$\sigma(q^{\prime})=q$; by Lemmas 28 and 27, we know
$K^{\prime}\in\mathcal{C}_{q^{\prime}}^{\top}$, and naturally
$\nu(K^{\prime})<\nu(K)$ (Lemma 4), thus the thesis follows by the IH.

  * •

$K[p\mapsto M^{\prime}]$ (where $M\mathrel{\leadsto}M^{\prime}$): this is s.n.
because $M^{\prime}\in\mathcal{C}^{\top\top}$ by hypothesis.

  * •

Since $M$ is neutral, there are no reductions at the interface.

######  Theorem 30.

For all types $T$, $\mathsf{Red}_{T}\in\mathcal{C}\mathcal{R}$.

######  Proof 3.28.

Standard by induction on $T$. For
$T=\mathopen{\textbf{\\{}}{T^{\prime}}\mathclose{\textbf{\\}}}$, we use Lemmas
25, 26, and 29.

##  4\. Strong normalization

We have proved that the reducibility sets of all types are candidates of
reducibility. We are now going to prove that every well-typed term is in the
reducibility set corresponding to its type: strong normalization will then
follow as a corollary, by using the $\mathrm{CR1}$ property of candidates of
reducibility.

The proof that well-typed terms are reducible is by structural induction on
the derivation of the typing judgment. We will proceed by first proving lemmas
that show the typing rules preserve reducibility, concluding at the end with
the fundamental theorem. Once again, we will focus our attention on the
results corresponding to collection types, as the rest are standard.

Reducibility of singletons is trivial by definition, while that of empty
collections is proved in the same style as [Coo09a], with the obvious
adaptations.

######  Lemma 31 (reducibility for singletons).

For all $\mathcal{C}$, if $M\in\mathcal{C}$, then
$\mathopen{\textbf{\\{}}{M}\mathclose{\textbf{\\}}}\in\mathcal{C}^{\top\top}$.

######  Proof 4.1.

Trivial by definition of $\top$-lifting and $\top\top$-lifting.

######  Lemma 32.

If $K\in\mathcal{S}\mathcal{N}$ is a continuation, then for all indices $p$ we
have $K[p\mapsto\emptyset]\in\mathcal{S}\mathcal{N}$.

######  Corollary 33 (reducibility for $\emptyset$).

For all $\mathcal{C}$, $\emptyset\in\mathcal{C}^{\top\top}$.

As for unions, we will prove a more general statement on auxiliary
continuations.

######  Lemma 34.

For all auxiliary continuations $Q,O_{1},O_{2}$ with pairwise disjoint
supports, if $Q[p\mapsto O_{1}]\in\mathcal{S}\mathcal{N}$ and $Q[p\mapsto
O_{2}]\in\mathcal{S}\mathcal{N}$, then $Q[p\mapsto
O_{1}\mathbin{\cup}O_{2}]\in\mathcal{S}\mathcal{N}$.

The proof of the lemma above follows the same style as [Coo09a]; however since
our definition of auxiliary continuations is more general, the theorem
statement mentions $O_{1},O_{2}$ rather than pure terms: the hypothesis on the
supports of the continuations being disjoint is required by this
generalization.

######  Corollary 35 (reducibility for unions).

If $M\in\mathcal{C}^{\top\top}$ and $N\in\mathcal{C}^{\top\top}$, then
$M\mathbin{\cup}N\in\mathcal{C}^{\top\top}$.

In some of the following proofs, a result that mirrors Lemma 34 will also be
useful.

######  Lemma 36.

If $Q[p\mapsto M\mathbin{\cup}N]\in\mathcal{S}\mathcal{N}$, then $Q[p\mapsto
M]\in\mathcal{S}\mathcal{N}$ and $Q[p\mapsto N]\in\mathcal{S}\mathcal{N}$;
furthermore, we have:

$\displaystyle\nu(Q[p\mapsto M])\leq\nu(Q[p\mapsto M\mathbin{\cup}N])$
$\displaystyle\nu(Q[p\mapsto N])\leq\nu(Q[p\mapsto M\mathbin{\cup}N])$

######  Proof 4.2.

We assume $p\in\operatorname{supp}(Q)$ (otherwise, $Q[p\mapsto M]=Q[p\mapsto
N]=Q[p\mapsto M\mathbin{\cup}N]$, and the thesis holds trivially), then we
show that any contraction in $Q[p\mapsto M]$ has a corresponding non-empty
reduction sequence in $Q[p\mapsto M\mathbin{\cup}N]$, and the two reductions
preserve the term form, therefore no reduction sequence of $Q[p\mapsto M]$ is
longer than the maximal one in $Q[p\mapsto M\mathbin{\cup}N]$. The same
reasoning applies to $Q[p\mapsto N]$.

Like in proofs based on standard $\top\top$-lifting, the most challenging
cases are those dealing with commuting conversions – in our case,
comprehensions and conditionals.

######  Lemma 37.

Let $K$, $\overline{L}$, $\overline{N}$ be such that
$K[p\mapsto\overline{N}\left[{\overline{L}}\middle/{x}\right]]\in\mathcal{S}\mathcal{N}$
and $\overline{L}\in\mathcal{S}\mathcal{N}$. Then
$K[p\mapsto\bigcup\mathopen{\textbf{\\{}}{\overline{N}|x\leftarrow\mathopen{\textbf{\\{}}{\overline{L}}\mathclose{\textbf{\\}}}}\mathclose{\textbf{\\}}}]\in\mathcal{S}\mathcal{N}$.

######  Proof 4.3.

In this proof, we assume the names of bound variables are chosen so as to
avoid duplicates, and are distinct from the free variables. We proceed by
well-founded induction on $(K,p,\overline{N},\overline{L})$ using the
following metric:

$\begin{array}[]{l}(K_{1},p_{1},\overline{N_{1}},\overline{L_{1}})\prec(K_{2},p_{2},\overline{N_{2}},\overline{L_{2}})\\\
\iff(\nu(K_{1}[p_{1}\mapsto\overline{N_{1}}\left[{\overline{L_{1}}}\middle/{x}\right]])+\nu(\overline{L_{1}}),\left\|K_{1}\right\|_{p_{1}},\mathrm{size}(\overline{N_{1}}))\\\
\qquad\quad\lessdot(\nu(K_{2}[p_{2}\mapsto\overline{N_{2}}\left[{\overline{L_{2}}}\middle/{x}\right]])+\nu(\overline{L_{2}}),\left\|K_{2}\right\|_{p_{2}},\mathrm{size}(\overline{N_{2}}))\end{array}$

Now we show that every contractum must be a strongly normalizing:

  * •

$K[p\mapsto\overline{N}\left[{\overline{L}}\middle/{x}\right]]$: this term is
s.n. by hypothesis.

  * •

$K^{\prime}[p\mapsto\bigcup\mathopen{\textbf{\\{}}{N|x\leftarrow\mathopen{\textbf{\\{}}{\overline{L}}\mathclose{\textbf{\\}}}}\mathclose{\textbf{\\}}}]^{\sigma}$,
where $K\mathrel{\stackrel{{\scriptstyle\sigma}}{{\leadsto}}}K^{\prime}$.
Lemma 4 allows us to prove
$\nu(K^{\prime}[p\mapsto\overline{N}\left[{\overline{L}}\middle/{x}\right]]^{\sigma})<\nu(K[p\mapsto\overline{N}\left[{\overline{L}}\middle/{x}\right]])$
(since the former is a contractum of the latter), which implies
$\nu(K^{\prime}[q\mapsto\overline{N}\left[{\overline{L}}\middle/{x}\right]])\leq\nu(K^{\prime}[p\mapsto\overline{N}\left[{\overline{L}}\middle/{x}\right]]^{\sigma})<\nu(K[p\mapsto\overline{N}\left[{\overline{L}}\middle/{x}\right]])$
for all $q$ s.t. $\sigma(q)=p$ by means of Lemma 19 (because
$[q\mapsto\overline{N}\left[{\overline{L}}\middle/{x}\right]]$ is a
subinstantiation of
$[p\mapsto\overline{N}\left[{\overline{L}}\middle/{x}\right]]^{\sigma}$); then
we can apply the IH to obtain, for all $q$ s.t. $\sigma(q)=p$,
$K^{\prime}[q\mapsto\bigcup\mathopen{\textbf{\\{}}{\overline{N}|x\leftarrow\mathopen{\textbf{\\{}}{\overline{L}}\mathclose{\textbf{\\}}}}\mathclose{\textbf{\\}}}]\in\mathcal{S}\mathcal{N}$;
by Corollary 22, this implies the thesis.

  * •

$K[p\mapsto\emptyset]$ (when $N=\emptyset$): this is equal to
$K[p\mapsto\emptyset\left[{\overline{L}}\middle/{x}\right]]$, which is s.n. by
hypothesis.

  * •

$K[p\mapsto\bigcup\mathopen{\textbf{\\{}}{\overline{N_{1}}|x\leftarrow\mathopen{\textbf{\\{}}{\overline{L}}\mathclose{\textbf{\\}}}}\mathclose{\textbf{\\}}}\mathbin{\cup}\bigcup\mathopen{\textbf{\\{}}{\overline{N_{2}}|x\leftarrow\mathopen{\textbf{\\{}}{\overline{L}}\mathclose{\textbf{\\}}}}\mathclose{\textbf{\\}}}]$
(when $\overline{N}=\overline{N_{1}}\mathbin{\cup}\overline{N_{2}}$); by IH
(since
$\mathrm{size}(\overline{N_{i}})<\mathrm{size}(\overline{N_{1}}\mathbin{\cup}\overline{N_{2}})$,
and all other metrics do not increase) we prove
$K[p\mapsto\bigcup\mathopen{\textbf{\\{}}{\overline{N_{i}}|x\leftarrow\mathopen{\textbf{\\{}}{\overline{L}}\mathclose{\textbf{\\}}}}\mathclose{\textbf{\\}}}]\in\mathcal{S}\mathcal{N}$
(for $i=1,2$), and consequently obtain the thesis by Lemma 34.

  * •

$K_{0}[p\mapsto\bigcup\mathopen{\textbf{\\{}}{\bigcup\mathopen{\textbf{\\{}}{\overline{M}|y\leftarrow\overline{N}}\mathclose{\textbf{\\}}}|x\leftarrow\mathopen{\textbf{\\{}}{\overline{L}}\mathclose{\textbf{\\}}}}\mathclose{\textbf{\\}}}]$,
where $K=K_{0}\mathop{\ooalign{\hfil\raise 0.86108pt\hbox{$\scriptscriptstyle
p$}\hfil\crcr{$\bigcirc$}}}\bigcup\mathopen{\textbf{\\{}}{\overline{M}|y\leftarrow\Box}\mathclose{\textbf{\\}}}$;
since we know, by the hypothesis on the choice of bound variables, that
$x\notin\operatorname{FV}(\overline{M})$, we note that
$K_{0}[p\mapsto\bigcup\mathopen{\textbf{\\{}}{\overline{M}|y\leftarrow\overline{N}}\mathclose{\textbf{\\}}}\left[{\overline{L}}\middle/{x}\right]]=K[p\mapsto\overline{N}\left[{\overline{L}}\middle/{x}\right]]$;
furthermore, by Lemma 3 we know
$\left\|K_{0}\right\|_{p}<\left\|K\right\|_{p}$; then we can apply the IH to
obtain the thesis.

  * •

$K_{0}[p\mapsto\bigcup\mathopen{\textbf{\\{}}{\mathtt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}where}~{}\overline{B}~{}\mathtt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}do}~{}\overline{N}|x\leftarrow\mathopen{\textbf{\\{}}{\overline{L}}\mathclose{\textbf{\\}}}}\mathclose{\textbf{\\}}}]$
(when $K=K_{0}\mathop{\ooalign{\hfil\raise 0.86108pt\hbox{$\scriptscriptstyle
p$}\hfil\crcr{$\bigcirc$}}}\mathtt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}where}~{}\overline{B}~{}\mathtt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}do}~{}\Box$):
since we know, from the hypothesis on the choice of bound variables, that
$x\notin\operatorname{FV}(B)$, we note that
$K_{0}[p\mapsto(\mathtt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}where}~{}\overline{B}~{}\mathtt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}do}~{}\overline{N})\left[{\overline{L}}\middle/{x}\right]]=K[p\mapsto\overline{N}\left[{\overline{L}}\middle/{x}\right]]$;
furthermore, by Lemma 3 we know
$\left\|K_{0}\right\|_{p}<\left\|K\right\|_{p}$; then we can apply the IH to
obtain the thesis.

  * •

reductions within $N$ or $L$ follow from the IH by reducing the induction
metric.

######  Lemma 38 (reducibility for comprehensions).

Assume $\mathrm{CR1}(\mathcal{C})$, $\mathrm{CR1}(\mathcal{D})$,
$\overline{M}\in\mathcal{C}^{\top\top}$ and for all
$\overline{L}\in\mathcal{C}$,
$\overline{N}\left[{\overline{L}}\middle/{x}\right]\in\mathcal{D}^{\top\top}$.
Then
$\bigcup\mathopen{\textbf{\\{}}{\overline{N}|x\leftarrow\overline{M}}\mathclose{\textbf{\\}}}\in\mathcal{D}^{\top\top}$.

######  Proof 4.4.

We assume $p$, $K\in\mathcal{D}_{p}^{\top}$ and prove
$K[p\mapsto\bigcup\mathopen{\textbf{\\{}}{\overline{N}|x\leftarrow\overline{M}}\mathclose{\textbf{\\}}}]\in\mathcal{S}\mathcal{N}$.
We start by showing that $K^{\prime}=K\mathop{\ooalign{\hfil\raise
0.86108pt\hbox{$\scriptscriptstyle
p$}\hfil\crcr{$\bigcirc$}}}\bigcup\mathopen{\textbf{\\{}}{\overline{N}|x\leftarrow\Box}\mathclose{\textbf{\\}}}\in\mathcal{C}_{p}^{\top}$,
or equivalently that for all $\overline{L}\in\mathcal{C}$,
$K^{\prime}[p\mapsto\mathopen{\textbf{\\{}}{\overline{L}}\mathclose{\textbf{\\}}}]=K[p\mapsto\bigcup\mathopen{\textbf{\\{}}{\overline{N}|x\leftarrow\mathopen{\textbf{\\{}}{\overline{L}}\mathclose{\textbf{\\}}}}\mathclose{\textbf{\\}}}]\in\mathcal{S}\mathcal{N}$:
since $\mathrm{CR1}(\mathcal{C})$, we know
$\overline{L}\in\mathcal{S}\mathcal{N}$, and since
$\overline{N}\left[{\overline{L}}\middle/{x}\right]\in\mathcal{D}^{\top\top}$,
$K[p\mapsto\overline{N}\left[{\overline{L}}\middle/{x}\right]]\in\mathcal{S}\mathcal{N}$;
then we can apply Lemma 37 to obtain
$K^{\prime}[p\mapsto\mathopen{\textbf{\\{}}{\overline{L}}\mathclose{\textbf{\\}}}]\in\mathcal{S}\mathcal{N}$
and consequently $K^{\prime}\in\mathcal{C}_{p}^{\top}$. But then, since
$\overline{M}\in\mathcal{C}^{\top\top}$, we have
$K^{\prime}[p\mapsto\overline{M}]=K[p\mapsto\bigcup\mathopen{\textbf{\\{}}{\overline{N}|x\leftarrow\overline{M}}\mathclose{\textbf{\\}}}]\in\mathcal{S}\mathcal{N}$,
which is what we needed to prove.

Reducibility for conditionals is proved in a similar manner. However, to make
the induction work under all the conversions commuting with
$\mathtt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}where}$,
we cannot prove the strong normalization statement within regular
continuations $K$, but we need to generalize it to auxiliary continuations. A
minor complication with the merging of nested
$\mathtt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}where}$
is handled by a separate lemma. Additionally, due to the more complicated
structure of auxiliary continuations, we will need to ensure that the free
variables of the Boolean guard of the
$\mathtt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}where}$
expression do not get captured: the assumption uses an auxiliary operation
$\operatorname{BV}$ denoting the set of variables bound over holes: The
operation $\operatorname{BV}(Q)$ is defined as follows:

$\displaystyle\operatorname{BV}(\mathop{\left[{p}\right]})$
$\displaystyle=\operatorname{BV}(\overline{M})=\emptyset$
$\displaystyle\operatorname{BV}(Q_{1}\cup Q_{2})$
$\displaystyle=\operatorname{BV}(Q_{1})\cup\operatorname{BV}(Q_{2})$
$\displaystyle\operatorname{BV}(\mathtt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}where}~{}\overline{B}~{}\mathtt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}do}~{}Q)$
$\displaystyle=\operatorname{BV}(Q)$
$\displaystyle\operatorname{BV}(\bigcup\mathopen{\textbf{\\{}}{Q_{1}\mid
x\leftarrow Q_{2}}\mathclose{\textbf{\\}}})$
$\displaystyle=\left\\{\begin{array}[]{ll}\\{{x}\\}\cup\operatorname{BV}(Q_{1})\cup\operatorname{BV}(Q_{2})&\text{if
$\operatorname{supp}(Q_{1})\neq\emptyset$}\\\
\operatorname{BV}(Q_{1})\cup\operatorname{BV}(Q_{2})&\text{otherwise}\end{array}\right.$

######  Lemma 39.

Suppose
$Q[p\mapsto\mathtt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}where}~{}B~{}\mathtt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}do}~{}M]\in\mathcal{S}\mathcal{N}$.
Then for all $B^{\prime}\in\mathcal{S}\mathcal{N}$ such that
$\operatorname{BV}(Q)$ and $\operatorname{FV}(B^{\prime})$ are disjoint,
$Q[p\mapsto\mathtt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}where}~{}B\land
B^{\prime}~{}\mathtt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}do}~{}M]\in\mathcal{S}\mathcal{N}$.

######  Lemma 40.

Let $Q$, $B$, $O$ such that $Q[p\mapsto O]\in\mathcal{S}\mathcal{N}$,
$B\in\mathcal{S}\mathcal{N}$,
$\operatorname{BV}(Q)\cap\operatorname{FV}(B)=\emptyset$ and
$\operatorname{supp}(Q)\cap\operatorname{supp}(O)=\emptyset$. Then
$Q[p\mapsto\mathtt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}where}~{}B~{}\mathtt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}do}~{}O]\in\mathcal{S}\mathcal{N}$.

######  Proof 4.5.

In this proof, we assume the names of bound variables are chosen so as to
avoid duplicates, and distinct from the free variables. It is important to
notice that this is the main proof in which auxiliary continuations, as
opposed to regular continuations, are needed to obtain a usable induction
hypothesis when the argument of
$\mathtt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}where}$
happens to be a comprehension. We proceed by well-founded induction on
$(Q,B,O,p)$ using the following metric:

$\begin{array}[]{l}(Q_{1},B_{1},O_{1},p_{1})\prec(Q_{2},B_{2},O_{2},p_{2})\iff\\\
\qquad(\nu(Q_{1}[p_{1}\mapsto
O_{1}]),\left|Q_{1}\right|_{p_{1}},\mathrm{size}(O_{1}),\nu(B_{1}))\\\
\qquad\lessdot(\nu(Q_{2}[p_{2}\mapsto
O_{2}]),\left|Q_{2}\right|_{p_{2}},\mathrm{size}(O_{2}),\nu(B_{2}))\end{array}$

We will consider all possible contracta and show that each of them must be a
strongly normalizing term; we will apply the induction hypothesis to new
auxiliary continuations obtained by placing pieces of $O$ into $Q$ or vice-
versa: the hypothesis on the supports of $Q$ and $O$ being disjoint is used to
make sure that the new continuations do not contain duplicate holes and are
thus well-formed. By cases on the possible contracta:

  * •

$Q_{1}[q\mapsto
Q_{2}\left[{\overline{L}}\middle/{x}\right]][p\mapsto(\mathtt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}where}~{}B~{}\mathtt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}do}~{}O)\left[{\overline{L}}\middle/{x}\right]]$,
where $Q=(Q_{1}\mathop{\ooalign{\hfil\raise 0.86108pt\hbox{$\scriptscriptstyle
q$}\hfil\crcr{$\bigcirc$}}}\bigcup\mathopen{\textbf{\\{}}{\Box\mid
x\leftarrow\mathopen{\textbf{\\{}}{\overline{L}}\mathclose{\textbf{\\}}}}\mathclose{\textbf{\\}}})[q\mapsto
Q_{2}]$, $q\in\operatorname{supp}(Q_{1})$, and
$p\in\operatorname{supp}(Q_{2})$; by the freshness condition we know
$x\notin\operatorname{FV}(B)$, thus
$(\mathtt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}where}~{}B~{}\mathtt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}do}~{}O)\left[{\overline{L}}\middle/{x}\right]=\mathtt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}where}~{}B~{}\mathtt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}do}~{}(O\left[{\overline{L}}\middle/{x}\right])$;
we take $Q^{\prime}=Q_{1}[q\mapsto