text:
\section{Strong bisimulation}
\label{s:bisimulation}

In this section we prove the simulation of one calculus by the other via the
proper translation and, most importantly, the strong bisimulation that follows
after the invertibility result (\emph{cf.}~ Thm.~\ref{t:translation:inverse}). This
strong bisimulation result will allow to port many important properties already
known for $\ensuremath{\mathsf{PPC}}$ into $\ensuremath{\mathsf{PPC}_\mathtt{dB}}$, as we will discuss later.

\medskip
We start by extending the increment function to substitutions and matches. The
\emph{increment at depth $k$} for variable indices in a substitution at level
$1$ is defined as $\fincv[k]{\sigma} \ensuremath{\triangleq}
\subs{\termidxv{1}[j]}{\fincv[k]{\subsapply{\sigma}{\termidxv{1}[j]}}}_{\termidx{1}[j] \in \dom{\sigma}}$.
As for matches, we simply define $\fincv[k]{\ensuremath{\mathtt{fail}}} \ensuremath{\triangleq} \ensuremath{\mathtt{fail}}$ and
$\fincv[k]{\ensuremath{\mathtt{wait}}} \ensuremath{\triangleq} \ensuremath{\mathtt{wait}}$, and use the definition over
substitution for successful matches. Recall that the matching operation yields
only substitutions at level 1. Then, the following result holds.

\begin{lemma}
Let $p,u \in \Term{\ensuremath{\mathsf{PPC}_\mathtt{dB}}}$. Then, $\match[n]{p}{\fincv{u}} =
\fincv{\match[n]{p}{u}}$.
\label{l:bisimulation:fincv-lifting}
\end{lemma}

\begin{proof}
By straightforward induction on $p$.
\end{proof}

Let us focus first on simulating $\ensuremath{\mathsf{PPC}}$ by $\ensuremath{\mathsf{PPC}_\mathtt{dB}}$. The key step here
is the preservation of the matching operation shown for $\toPPCX{\_}$ in
Lem.~\ref{l:translation:to-ppcx-match}. It guarantees that every redex in
$\ensuremath{\mathsf{PPC}}$ turns into a redex in $\ensuremath{\mathsf{PPC}_\mathtt{dB}}$ too. Then, the appropiate
definition of the operational semantics given for $\ensuremath{\mathsf{PPC}_\mathtt{dB}}$ in
Sec.~\ref{s:ppcx} allows us to conclude.

\begin{lemma}
Let $t \in \Term{\ensuremath{\mathsf{PPC}}}$. If $t \reduce[\ensuremath{\mathtt{PPC}}] t'$, then $\toPPCX[V][M]{t}
\reduce[\ensuremath{\mathtt{dB}}] \toPPCX[V][M]{t'}$.
\label{l:bisimulation:ppc-ppcx}
\end{lemma}

\input{proofs/bisimulation/ppc-ppcx}

\begin{theorem}
Let $t \in \Term{\ensuremath{\mathsf{PPC}}}$. If $t \reduce[\ensuremath{\mathtt{PPC}}] t'$, then $\toPPCX{t}
\reduce[\ensuremath{\mathtt{dB}}] \toPPCX{t'}$.
\label{t:bisimulation:ppc-ppcx}
\end{theorem}

\begin{proof}
The property is an immediate consequence of Lem.~\ref{l:bisimulation:ppc-ppcx},
taking $V = M = X$ as given in Def.~\ref{d:translation:to-ppcx}.
\end{proof}

Regarding the converse simulation, \emph{i.e.}~ $\ensuremath{\mathsf{PPC}_\mathtt{dB}}$ into $\ensuremath{\mathsf{PPC}}$, we resort
here to the fact that the embedding $\toPPC{\_}$ also preserves the matching
operation (\emph{cf.}~ Lem.~\ref{l:translation:to-ppc-match}). Then, every redex in
$\ensuremath{\mathsf{PPC}_\mathtt{dB}}$ is translated into a redex in $\ensuremath{\mathsf{PPC}}$ as well.

\begin{lemma}
Let $t \in \Term{\ensuremath{\mathsf{PPC}_\mathtt{dB}}}$. If $t \reduce[\ensuremath{\mathtt{dB}}] t'$, then $\toPPC[V][M]{t}
\reduce[\ensuremath{\mathtt{PPC}}] \toPPC[V][M]{t'}$.
\label{l:bisimulation:ppcx-ppc}
\end{lemma}

\input{proofs/bisimulation/ppcx-ppc}

\begin{theorem}
Let $t \in \Term{\ensuremath{\mathsf{PPC}_\mathtt{dB}}}$. If $t \reduce[\ensuremath{\mathtt{dB}}] t'$, then $\toPPC{t}
\reduce[\ensuremath{\mathtt{PPC}}] \toPPC{t'}$.
\label{t:bisimulation:ppcx-ppc}
\end{theorem}

\begin{proof}
The property is an immediate consequence of Lem.~\ref{l:bisimulation:ppcx-ppc},
taking $V = M = X$ as given in Def.~\ref{d:translation:to-ppc}.
\end{proof}

As already commented, these previous results may be combined to obtain a
strong bisimulation between the two calculi. The invertibility result allows
to define a relation between terms in $\ensuremath{\mathsf{PPC}}$ and $\ensuremath{\mathsf{PPC}_\mathtt{dB}}$. Given $t \in
\Term{\ensuremath{\mathsf{PPC}_\mathtt{dB}}}$ and $s \in \Term{\ensuremath{\mathsf{PPC}}}$, let us write $t \ensuremath{\Mapsto} s$
whenever $\toPPC{t} \ensuremath{=_{\alpha}} s$ and, therefore, $\toPPCX{s} = t$ by
Thm.~\ref{t:translation:inverse}. Then, the strong bisimulation result states
that whenever $t \ensuremath{\Mapsto} s$ and $t \reduce[\ensuremath{\mathtt{dB}}] t'$, there exists a term
$s'$ such that $t' \ensuremath{\Mapsto} s'$ and $s \reduce[\ensuremath{\mathtt{PPC}}] s'$, and the other way
around. Graphically: \[
\begin{array}{c@{\qquad\text{and}\qquad}c}
\begin{tikzcd}[ampersand replacement=\&]
t \arrow{d}[anchor=north,left]{\ensuremath{\mathtt{dB}}}
  \&[-25pt] \ensuremath{\Mapsto}
  \&[-25pt] s \arrow[densely dashed]{d}[anchor=north,left]{\ensuremath{\mathtt{PPC}}} \\
t'
  \&[-25pt] \ensuremath{\Mapsto}
  \&[-25pt] s'
\end{tikzcd}
&
\begin{tikzcd}[ampersand replacement=\&]
t \arrow[densely dashed]{d}[anchor=north,left]{\ensuremath{\mathtt{dB}}}
  \&[-25pt] \ensuremath{\Mapsto}
  \&[-25pt] s \arrow{d}[anchor=north,left]{\ensuremath{\mathtt{PPC}}} \\
t'
  \&[-25pt] \ensuremath{\Mapsto}
  \&[-25pt] s'
\end{tikzcd}
\end{array} \]

\begin{theorem}[Strong bisimulation]
The relation $\ensuremath{\Mapsto}$ is a strong bisimulation with respect to
the reduction relations $\reduce[\ensuremath{\mathtt{PPC}}]$ and $\reduce[\ensuremath{\mathtt{dB}}]$ respectively.
\label{t:bisimulation}
\end{theorem}

\begin{proof}
The proof follows immediately from Thm.~\ref{t:bisimulation:ppc-ppcx}
and~\ref{t:bisimulation:ppcx-ppc} above, and the invertibility result
(Thm.~\ref{t:translation:inverse}) given in Sec.~\ref{s:translation}.
\end{proof}

The importance of this result resides in the fact that it guarantees that
$\ensuremath{\mathsf{PPC}}$ and $\ensuremath{\mathsf{PPC}_\mathtt{dB}}$ have exactly the same operational semantics. An
immediate consequence of this is the confluence of $\reduce[\ensuremath{\mathtt{dB}}]$.

\begin{theorem}[Confluence]
The reduction relation $\reduce[\ensuremath{\mathtt{dB}}]$ is confluent (CR).
\label{t:bisimulation:cr}
\end{theorem}

\begin{proof}
The result follows directly from Thm.~\ref{t:preliminaries:ppc:cr} and the
strong bisimulation:
\begin{center}
\begin{tikzcd}[ampersand replacement=\&]
  \&[-15pt]  \&[-15pt] t \arrow[twoheadrightarrow]{ddll}[inner sep=5pt,above]{\ensuremath{\mathtt{dB}}}
              \arrow[twoheadrightarrow]{ddrr}[inner sep=5pt,above]{\ensuremath{\mathtt{dB}}}
              \arrow[Mapsto]{d}{}
\\[-5pt]
  \&[-15pt]  \&[-15pt] s \arrow[dashed,twoheadrightarrow]{dl}[inner sep=5pt,above]{\ensuremath{\mathtt{PPC}}}
              \arrow[dashed,twoheadrightarrow]{dr}[inner sep=5pt,above]{\ensuremath{\mathtt{PPC}}}
\\
t_0 \arrow[dashed,twoheadrightarrow]{ddrr}[inner sep=5pt,below]{\ensuremath{\mathtt{dB}}}
    \arrow[Mapsto]{r}{}
  \&[-15pt] s_0 \arrow[dashed,twoheadrightarrow]{dr}[inner sep=5pt,below]{\ensuremath{\mathtt{PPC}}}
  \&[-15pt] \text{Thm.~\ref{t:preliminaries:ppc:cr}}
  \&[-15pt] s_1 \arrow[dashed,twoheadrightarrow]{dl}[inner sep=5pt,below]{\ensuremath{\mathtt{PPC}}}
  \&[-15pt] t_1 \arrow[dashed,twoheadrightarrow]{ddll}[inner sep=5pt,below]{\ensuremath{\mathtt{dB}}}
                \arrow[Mapsto]{l}{}
\\
  \&[-15pt]  \&[-15pt] s'
\\[-5pt]
  \&[-15pt]  \&[-15pt] t' \arrow[Mapsto]{u}{}
\end{tikzcd}
\end{center}
\end{proof}

Another result of relevance to our line of research, is the existence of
normalising reduction strategies for $\ensuremath{\mathsf{PPC}}$, as it is shown
in~\cite{BonelliKLR17}. This result is particularly challenging since reduction
in $\ensuremath{\mathsf{PPC}}$ is shown to be \emph{non-sequential} due to the nature of its
matching operation. This implies that the notion of \emph{needed redexes} (a
key concept for defining normalising strategies) must be generalised to
\emph{necessary sets}~\cite{Raamsdonk97} of redexes. Moreover, the notion of
\emph{gripping}~\cite{Mellies96} is also captured by $\ensuremath{\mathsf{PPC}}$, representing a
further obstacle in the definition of such a normalising strategy. All in all,
in~\cite{BonelliKLR17} the authors introduce a reduction strategy $\S$ that is
shown to be normalising, overcoming all the aforementioned issues. Thanks to
the strong bisimulation result presented above, this strategy $\S$ can also be
guaranteed to normalise for $\ensuremath{\mathsf{PPC}_\mathtt{dB}}$.

\section{Conclusion}
\label{s:conclusion}

In this paper we introduced a novel presentation of the \emph{Pure Pattern
Calculus} ($\ensuremath{\mathsf{PPC}}$)~\cite{JayK09} in de Bruijn's style. This required
extending de Bruijn ideas for a setting where each binder may capture more than
one variable at once. To this purpose we defined \emph{bidimensional indices}
of the form $\termidx{i}[j]$ where $\termidx{i}$ is dubbed the \emph{primary
index} and $\termidx{j}$ the \emph{secondary index}, so that the primary index
determines the binding abstraction and the secondary index identifies the
variable among those (possibly many) bound ones. Moreover, given the nature of
$\ensuremath{\mathsf{PPC}}$ semantics, our extension actually deals with two kinds of
bidimensional indices, namely \emph{variable indices} and \emph{matchable
indices}. This newly introduced calculus is simply called \emph{Pure Pattern
Calculus with de Bruijn indices} ($\ensuremath{\mathsf{PPC}_\mathtt{dB}}$).

Our main result consists of showing that the relation between $\ensuremath{\mathsf{PPC}}$ and
$\ensuremath{\mathsf{PPC}_\mathtt{dB}}$ is a strong bisimulation with respect to their respective redution
relations, \emph{i.e.}~ they have exactly the same operational semantics. For that
reason, proper translations between the two calculi were defined, $\toPPCX{\_}
: \Term{\ensuremath{\mathsf{PPC}}} \to \Term{\ensuremath{\mathsf{PPC}_\mathtt{dB}}}$ and $\toPPC{\_} : \Term{\ensuremath{\mathsf{PPC}_\mathtt{dB}}} \to
\Term{\ensuremath{\mathsf{PPC}}}$, in such a way that $\toPPCX{\_}$ is the inverse of
$\toPPC{\_}$ and vice-versa (modulo $\alpha$-conversion). Most notably, these
embeddings are shown to preserve the matching operation of their respective
domain calculus.

The strong bisimulation result allows to port into $\ensuremath{\mathsf{PPC}_\mathtt{dB}}$ many already
known results for $\ensuremath{\mathsf{PPC}}$. Of particular interest for our line of research
are the confluence and the existence of normalising reduction strategies for
$\ensuremath{\mathsf{PPC}}$~\cite{BonelliKLR17}, a rather complex result that requires dealing
with notions of \emph{gripping}~\cite{Mellies96} and \emph{necessary
sets}~\cite{Raamsdonk97} of redexes. The result introduced on this paper may
allow for a direct implementation of such strategies without the inconveniences
of working modulo $\alpha$-conversion.

As commented before, the ultimate goal of our research is the implementation of
a prototype for a typed functional programming language capturing \emph{path
polymorphism}. This development is based on the \emph{Calculus of Applicative
Patterns} ($\textsf{CAP}$)~\cite{Ayala-RinconBEV19}, for which a static type
system has already been introduced, guaranteeing well-behaved operational
semantics, together with its corresponding efficient type-checking algorithm.
$\textsf{CAP}$ is essentially the static fragment of $\ensuremath{\mathsf{PPC}}$, where the
abstraction is generalised into an alternative (\emph{i.e.}~ abstracting multiple
branches at once). These two calculi are shown to be equivalent. Thus, future
lines of work following the results presented in this paper involve porting
$\textsf{CAP}$ to the bidimensional indices setting and formalising the ideas
of~\cite{BonelliKLR17} into such framework. This will lead to a first
functional version of the sought-after prototype.

\section{Introduction}
\label{c:intro}

The foundations of functional programming languages like LISP, Miranda, Haskell
or the ones in the ML family (Caml, SML, OCaml, etc.) rely strongly on the
study of the $\ensuremath{\lambda}$-calculus~\cite{Barendregt85} and its many variants
introduced over the years. Among them there are the \emph{pattern
calculi}~\cite{Oostrom90,CirsteaK98,Kahl03,CerritoK04,JayK06,Jay04,KlopOV08},
whose key feature can be identified as \emph{pattern-matching}.
Pattern-matching has been extensively used in programming languages as a means
for writing succinct and elegant programs. It stands for the possibility of
defining functions by cases, analysing the shape of their arguments, while
providing a syntactic tool to decompose such arguments in their parts when
applying the function.

In the standard $\ensuremath{\lambda}$-calculus, functions are represented by
expressions of the form $\termabs{x}{t}$, where $x$ is the formal parameter and
$t$ the body of the function. Such a function may be applied to any term,
regardless of its form, as dictated by the $\ensuremath{\beta}$-reduction rule:
$\termapp{(\termabs{x}{t})}{u} \rrule{\ensuremath{\beta}} \subsapply{\subs{x}{u}}{t}$,
where $\subsapply{\subs{x}{u}}{t}$ stands for the result of replacing all free
occurrences of $x$ in $t$ by $u$. Note that no requirement on the shape of $u$
is placed. Pattern calculi, on the contrary, provide generalisations of the
$\ensuremath{\beta}$-reduction rule in which abstractions $\termabs{x}{t}$ are replaced by
more general terms like $\termabs{p}{t}$ where $p$ is called a \emph{pattern}.
For example, consider the function $\termabs{\termpair{x}{y}}{x}$ that projects
the first component of a pair. Here the pattern is the pair $\termpair{x}{y}$
and the expression $\termapp{(\termabs{\termpair{x}{y}}{x})}{u}$ will only be
able to reduce if $u$ is indeed of the form $\termpair{u_1}{u_2}$. Otherwise,
reduction will be blocked.

We are particularly interested in studying the \emph{Pure Pattern
Calculus} ($\ensuremath{\mathsf{PPC}}$)~\cite{JayK09} and the novel features it introduced in
the field of pattern calculi, namely \emph{path polymorphism} and \emph{pattern
polymorphism}. The former refers to the possibility of defining functions that
uniformly traverse arbitrary data structures, while the latter allows to
consider patterns as parameters that may be dynamically generated in run-time.
Developing such a calculus implies numerous technical challenges to guarantee
well-behaved operational semantics in the untyped framework. Recently, a static
type system has been introduced for a restriction of $\ensuremath{\mathsf{PPC}}$ called
\emph{Calculus of Applicative Patterns} ($\textsf{CAP}$)~\cite{VisoBA16}, which is
able to capture the path polymorphic aspect of $\ensuremath{\mathsf{PPC}}$. Moreover,
type-checking algorithms for such a formalism has also been
studied~\cite{EdiVB15}, as a first step towards an implementation of a
prototype for a typed functional programming language capturing such features.
Following this line of research, studies on the definition of normalising
strategies for $\ensuremath{\mathsf{PPC}}$ have been done as
well~\cite{BonelliKLR12,BonelliKLR17}. Such results are ported to $\textsf{CAP}$ by
means of a simple embedding~\cite{Viso20} where the static typing discipline
gives further guarantees on the well-behaved semantics of terms.

Within this framework, the present work aims to throw some light on the
implementation aspects of these formalisms. In particular, working modulo
$\alpha$-conversion~\cite{Barendregt85} implies dealing with variable renaming
during the implementation. Such an approach is known to be error-prone and
computationally expensive. One way of getting rid of this problem in the
$\ensuremath{\lambda}$-calculus setting is adopting de Bruijn
notation~\cite{Bruijn72,Bruijn78}, a technique that simply avoids working
modulo $\alpha$-conversion. To the best of our knowledge, no dynamic pattern
calculi in the likes of $\ensuremath{\mathsf{PPC}}$ with de Bruijn indices has been formalised
in the literature. However, there are some references worth mentioning.
In~\cite{OostromR14} an alternative presentation of $\ensuremath{\mathsf{PPC}}$ is given in the
framework of \emph{Higher-Order Pattern Rewriting System}
(HRS)~\cite{Nipkow91,MayrN98}, together with translations between the two
systems. On the other hand, in~\cite{BonelliKR05} de Bruijn ideas had been
extended to \emph{Expression Reduction Systems} (ERS)~\cite{GlauertKK05} also
providing formal translations from systems with names to systems with indices,
and vice-versa. Moreover, the correspondence between HRS and ERS has already
been established~\cite{Raamsdonk80}. The composition of such translations might
derive a higher order system \emph{\`{a} la} de Bruijn capturing the features
of $\ensuremath{\mathsf{PPC}}$. However, this would result in a rather indirect solution to our
problem where many technicalities still need to be sorted out.

We aim to formalise an intuitive variant of $\ensuremath{\mathsf{PPC}}$ with de Bruijn indices
where known results for the original calculus, such as the existence of
normalising strategies, may easily be ported and reused.

\subsection{Contributions}
\label{c:intro:contributions}

This paper extends de Bruijn's ideas to handle binders that capture multiple
symbols at once, by means of what we call \emph{bidimensional indices}. These
ideas are illustrated by introducing a novel presentation of $\ensuremath{\mathsf{PPC}}$,
without variable/matchable names, called $\ensuremath{\mathsf{PPC}_\mathtt{dB}}$. Moreover, binders in the
new proposed calculus are capable of handling two kinds of indices, namely
variable and matchable indices, as required by the $\ensuremath{\mathsf{PPC}}$ operational
semantics.

Proper translations from $\ensuremath{\mathsf{PPC}}$ to $\ensuremath{\mathsf{PPC}_\mathtt{dB}}$ and back are introduced.
This functions preserve the matching operation and, hence, the operational
semantics of both calculi. Moreover, they turn out to be the inverse of each
other. This leads to a crucial strong bisimulation result between the two
calculi, which allows to import many known properties of $\ensuremath{\mathsf{PPC}}$ into
$\ensuremath{\mathsf{PPC}_\mathtt{dB}}$, for instance confluence and the existence of normalising
strategies.

\subsection{Structure of the paper}
\label{c:intro:structure}

We start by briefly introducing $\ensuremath{\mathsf{PPC}}$ and reminding the mechanism of de
Bruijn indices for the $\ensuremath{\lambda}$-calculus in Sec.~\ref{s:preliminaries}.
The novel $\ensuremath{\mathsf{PPC}_\mathtt{dB}}$ is formalised in Sec.~\ref{s:ppcx}, followed by the
introduction of the translations in Sec.~\ref{s:translation}. The strong
bisimulation result is presented in Sec.~\ref{s:bisimulation} together with a
discussion of different properties of $\ensuremath{\mathsf{PPC}_\mathtt{dB}}$ that follow from it. We
conclude in Sec.~\ref{s:conclusion} and discuss possible lines of future work.

\section{The Pure Pattern Calculus with de Bruijn indices}
\label{s:ppcx}

This section introduces the novel \emph{Pure Pattern Calculus with de Bruijn
indices} ($\ensuremath{\mathsf{PPC}_\mathtt{dB}}$). It represents a natural extension of de Bruijn ideas to
a framework where a binder may capture more than one symbol. In the particular
case of $\ensuremath{\mathsf{PPC}}$ there are two kinds of captured symbols, namely variables
and matchables. This distinction is preserved in $\ensuremath{\mathsf{PPC}_\mathtt{dB}}$ while extending
indices to pairs (\emph{a.k.a.}~bidimensional indices) to distinguish the
binder that captures the symbol and the individual symbol among all those
captured by the same binder.

The sets of \emph{terms} $\Term{\ensuremath{\mathsf{PPC}_\mathtt{dB}}}$, \emph{contexts}, \emph{data
structures} $\TermData{\ensuremath{\mathsf{PPC}_\mathtt{dB}}}$ and \emph{matchable forms}
$\Matchable{\ensuremath{\mathsf{PPC}_\mathtt{dB}}}$ of $\ensuremath{\mathsf{PPC}_\mathtt{dB}}$ are given by the following grammar: \[
\begin{array}{c@{\qquad}c}
\begin{array}{rrcl}
\textbf{Terms}    & t         & \ensuremath{:\coloneq}  & \termidxv{i}[j] \mid \termidxm{i}[j] \mid \termapp{t}{t} \mid \termabs[n]{t}{t} \\
\textbf{Contexts} & \ctxt{C}  & \ensuremath{:\coloneq}  & \Box \mid \termapp{\ctxt{C}}{t} \mid \termapp{t}{\ctxt{C}} \mid \termabs[n]{\ctxt{C}}{t} \mid \termabs[n]{t}{\ctxt{C}}
\end{array}
&
\begin{array}{rrcl}
\textbf{Data structures}  & d & \ensuremath{:\coloneq}  & \termidxm{i}[j] \mid \termapp{d}{t} \\
\textbf{Matchable forms}  & m & \ensuremath{:\coloneq}  & d \mid \termabs[n]{t}{t}
\end{array}
\end{array}
\] where $\termidxv{i}[j]$ is dubbed a \emph{bidimensional index} and denotes
an ordered pair in $\ensuremath{{\mathbb{N}}}_{\geq 1} \times \ensuremath{{\mathbb{N}}}_{\geq 1}$ with
\emph{primary index} $\termidx{i}$ and \emph{secondary index} $\termidx{j}$.
The sub-index $n \in \ensuremath{{\mathbb{N}}}$ in an abstraction represents the amount of
indices (pairs) being captured by it. The primary index of a pair is used to
determine if the pair is bound by an abstraction, while the secondary index
identifies the pair among those (possibly many) bound ones. As for $\ensuremath{\mathsf{PPC}}$,
an index of the form $\termidxv{i}[j]$ is called a \emph{variable index} while
$\termidxm{i}[j]$ is dubbed a \emph{matchable index}. The \emph{free variables}
and \emph{free matchables} of a term are thus defined as follows: \[
\begin{array}{c@{\qquad}c}
\begin{array}{rcl}
\fv{\termidxv{i}[j]}    & \ensuremath{\triangleq}  & \set{\termidx{i}[j]} \\
\fv{\termidxm{i}[j]}    & \ensuremath{\triangleq}  & \emptyset \\
\fv{\termapp{t}{u}}     & \ensuremath{\triangleq}  & \fv{t} \cup \fv{u} \\
\fv{\termabs[n]{p}{t}}  & \ensuremath{\triangleq}  & \fv{p} \cup (\fv{t} - 1)
\end{array}
&
\begin{array}{rcl}
\fm{\termidxv{i}[j]}    & \ensuremath{\triangleq}  & \emptyset \\
\fm{\termidxm{i}[j]}    & \ensuremath{\triangleq}  & \set{\termidx{i}[j]} \\
\fm{\termapp{t}{u}}     & \ensuremath{\triangleq}  & \fm{t} \cup \fm{u} \\
\fm{\termabs[n]{p}{t}}  & \ensuremath{\triangleq}  & (\fm{p} - 1) \cup \fm{t}
\end{array}
\end{array}
\] where $X - k$ stands for subtracting $k$ from the primary index of each
element of the set $X$, removing those that result in a non-positive index.

\begin{wrapfigure}{R}{0.2\textwidth}
\begin{tikzpicture}[baseline=(current bounding box.center),->,auto,node distance=5pt]
\node (ABS1a)                               {$\vphantom{(}\ensuremath{\lambda}_{1}$};
\node (PTN1)  [right of=ABS1a, xshift=5pt]  {$\vphantom{(}\termidxm{1}[1]$};
\node (ABS1b) [right of=PTN1,  xshift=3pt]  {$\vphantom{(}.($};
\node (ABS2a) [right of=ABS1b, xshift=4pt]  {$\vphantom{(}\ensuremath{\lambda}_{1}$};
\node (PTN2a) [right of=ABS2a, xshift=5pt]  {$\vphantom{(}\termidxv{1}[1]$};
\node (PTN2b) [right of=PTN2a, xshift=6pt]  {$\vphantom{(}\termidxm{1}[1]$};
\node (ABS2b) [right of=PTN2b, xshift=1pt]  {$\vphantom{(}.$};
\node (BODY)  [right of=ABS2b, xshift=1pt]  {$\vphantom{(}\termidxv{1}[1]$};
\node (ABS1c) [right of=BODY]               {$\vphantom{(})$};

\path (ABS1a.south) edge [bend right=45] node[left] {} (PTN1.south)
      (ABS1a.south) edge [bend right=90] node[left] {} (PTN2a.south)
      (ABS2a.south) edge [bend right=90] node[left] {} (PTN2b.south)
      (ABS2a.south) edge [bend right=90] node[left] {} (BODY.south);
\end{tikzpicture}
\end{wrapfigure}

Let us illustrate these concepts with a similar example as that given for
$\ensuremath{\mathsf{PPC}}$, namely the function $\mathsf{elim} =
\termabs[\lista{x}]{\termmatch{x}}{(\termabs[\lista{y}]{\termapp{\termvar{x}}{\termmatch{y}}}{\termvar{y}})}$.
An equivalent term in the $\ensuremath{\mathsf{PPC}_\mathtt{dB}}$ framework would be
$\termabs[1]{\termidxm{1}[1]}{(\termabs[1]{\termapp{\termidxv{1}[1]}{\termidxm{1}[1]}}{\termidxv{1}[1]})}$.
Note that variable indices in the context of a pattern are not bound by the
respective abstraction, in the same way that matchable indices in the body of
the abstraction are not captured either. Thus, the first occurrence of
$\termidxv{1}[1]$ is actually bound by the outermost abstraction, together with
the first occurrence of the matchable index $\termidxm{1}[1]$. The rest of the
indices in the term are bound by the inner abstraction as depicted in the
figure to the right. As a further (more interesting) example, consider the term
$\termabs[\lista{x,y}]{\termapp{\termmatch{x}}{\termmatch{y}}}{\termabs[\lista{}]{\termvar{x}}{\termvar{y}}}$
from $\ensuremath{\mathsf{PPC}}$, whose counter-part in $\ensuremath{\mathsf{PPC}_\mathtt{dB}}$ would look like
$\termabs[2]{\termapp{\termidxm{1}[1]}{\termidxm{1}[2]}}{\termabs[0]{\termidxv{1}[1]}{\termidxv{2}[2]}}$.
This example illustrates the use of secondary indices to identify symbols
bound by the same abstraction. It also shows how the primary index of a
variable is increased when occurring within the body of an internal
abstraction, while this is not the case for occurrences in a pattern position.
Thus, both $\termidxv{1}[1]$ and $\termidxv{2}[2]$ are bound by the outermost
abstraction, as well as $\termidxm{1}[1]$ and $\termidxm{1}[2]$. Note how the
inner abstraction does not bind any index at all.

A term $t$ is said to be \emph{well-formed} if all the free bidimensional
indices (variables and matchables) of $t$ have their secondary index equal to
1, and for every sub-term of the form $\termabs[n]{p}{s}$ (written
$\termabs[n]{p}{s} \ensuremath{\subseteq} t$) all the pairs captured by the abstraction have
their secondary index within the range $[1,n]$. Formally, $\set{\termidx{i}[j]
\mid \termidx{i}[j] \in \fm{t} \cup \fv{t}, j > 1} \cup
(\bigcup_{\termabs[n]{p}{s} \ensuremath{\subseteq} t}{\set{\termidx{1}[j] \mid \termidx{1}[j] \in \fm{p} \cup \fv{s}, j > n}})
= \emptyset$.

\medskip
Before introducing a proper notion of substitution for $\ensuremath{\mathsf{PPC}_\mathtt{dB}}$ it is
necessary to have a mechanism to update indices at a certain depth within the
term. The \emph{increment at depth $k$} for variable and matchable indices in a
term $t$, written $\fincv[k]{t}$ and $\fincm[k]{t}$ respectively, are
inductively defined as follows \[
\begin{array}{c@{\qquad}c}
\begin{array}{rcll}
\fincv[k]{\termidxv{i}[j]}    & \ensuremath{\triangleq}  & \begin{cases}
                                          \termidxv{(i+1)}[j] & \text{if $i > k$} \\
                                          \termidxv{i}[j]     & \text{if $i \leq k$}
                                          \end{cases} \\
\fincv[k]{\termidxm{i}[j]}    & \ensuremath{\triangleq}  & \termidxm{i}[j] \\
\fincv[k]{\termapp{t}{u}}     & \ensuremath{\triangleq}  & \termapp{\fincv[k]{t}}{\fincv[k]{u}} \\
\fincv[k]{\termabs[n]{p}{t}}  & \ensuremath{\triangleq}  & \termabs[n]{\fincv[k]{p}}{\fincv[k+1]{t}}
\end{array}
&
\begin{array}{rcll}
\fincm[k]{\termidxv{i}[j]}    & \ensuremath{\triangleq}  & \termidxv{i}[j] \\
\fincm[k]{\termidxm{i}[j]}    & \ensuremath{\triangleq}  & \begin{cases}
                                          \termidxm{(i+1)}[j] & \text{if $i > k$} \\
                                          \termidxm{i}[j]     & \text{if $i \leq k$}
                                          \end{cases} \\
\fincm[k]{\termapp{t}{u}}     & \ensuremath{\triangleq}  & \termapp{\fincm[k]{t}}{\fincm[k]{u}} \\
\fincm[k]{\termabs[n]{p}{t}}  & \ensuremath{\triangleq}  & \termabs[n]{\fincm[k+1]{p}}{\fincm[k]{t}}
\end{array}
\end{array}
\] Similarly, the \emph{decrement at depth} $k$ for variables ($\fdecv[k]{\_}$)
and matchables ($\fdecm[k]{\_}$) are defined by subtracting one from the
primary index above $k$ in the term. Most of the times these functions are used
with $k = 0$, thus the subindex will be omitted when it is clear from context.
In particular, the decrement function for variables will allow us to generalise
the idea of substitution at level $i$ with respect to the original one
presented in Sec.~\ref{s:preliminaries:indices}, which only holds in the
context of a $\ensuremath{\beta}$-reduction, by making the necessary adjustments to the
indices at the moment of the redution instead of hard-coding them into the
substitution meta-operation.

\begin{lemma}
Let $t \in \Term{\ensuremath{\mathsf{PPC}_\mathtt{dB}}}$. Then,
\begin{enumerate}
  \item \label{l:appendix:finc:var} $\fincv[k]{\fincv[l]{t}} =
  \fincv[l]{\fincv[k-1]{t}}$ if $l < k$.
  \item \label{l:appendix:finc:match} $\fincv[k]{\fincm[l]{t}} =
  \fincm[l]{\fincv[k]{t}}$.
  \item \label{l:appendix:finc:fdec-l} $\fdecv[k]{\fincv[k]{t}} = t$.
  \item \label{l:appendix:finc:fdec-r} $\fincv[k]{\fdecv[k]{t}} = t$ iff
  $\termidx{(k+1)}[j] \notin \fv{t}$ for any $j \in \ensuremath{{\mathbb{N}}}_{\geq 1}$.
\end{enumerate}
\label{l:appendix:finc}
\end{lemma}

\begin{proof}
All items follow by straightforward induction on $t$.
\end{proof}

A \emph{substitution at level $i$} is a partial function from variable indices
to terms. It maps free variable indices at level $i$ to terms, performing the
appropriate updates as it traverses the substituted term, to avoid undesired
captures. \[
\begin{array}{c@{\quad}c}
\begin{array}{rcl@{\quad}l}
\subsapply{\subs{\termidxv{i}[j]}{u_j}_{j \in J}}{\termidxv{i'}[k]}   & \ensuremath{\triangleq}  & \begin{cases}
                                                                                u_k               & \text{if $i' = i, k \in J$} \\
                                                                                \termidxv{i'}[k]  & \text{if $i' \neq i$}
                                                                                \end{cases} \\
\subsapply{\subs{\termidxv{i}[j]}{u_j}_{j \in J}}{\termidxm{i'}[k]}   & \ensuremath{\triangleq}  & \termidxm{i'}[k]
\end{array}
&
\begin{array}{rcl@{\quad}l}
\subsapply{\subs{\termidxv{i}[j]}{u_j}_{j \in J}}{(\termapp{t}{s})}   & \ensuremath{\triangleq}  & \termapp{\subsapply{\subs{\termidxv{i}[j]}{u_j}_{j \in J}}{t}}{\subsapply{\subs{\termidxv{i}[j]}{u_j}_{j \in J}}{s}} \\
\subsapply{\subs{\termidxv{i}[j]}{u_j}_{j \in J}}{\termabs[n]{p}{t}}  & \ensuremath{\triangleq}  & \termabs[n]{\subsapply{\subs{\termidxv{i}[j]}{\fincm{u_j}}_{j \in J}}{p}}{\subsapply{\subs{\termidxv{(i+1)}[j]}{\fincv{u_j}}_{j \in J}}{t}}
\end{array}
\end{array} \] It is worth noticing that the base case for variable indices is
undefined if $i' = i$ and $k \notin J$. Such case will render the result of
the substitution undefined as well. In the operational semantics of
$\ensuremath{\mathsf{PPC}_\mathtt{dB}}$, the matching operation presented below will be responsible for
avoiding this undesired situation, as we will see later. The \emph{domain} of a
substitution at level $i$ is given by
$\dom{\subs{\termidxv{i}[j]}{u_j}_{j \in J}} \ensuremath{\triangleq}
\set{\termidxv{i}[j]}_{j \in J}$. The identity substitution (\emph{i.e.}~ with empty
domain) is denoted $\ensuremath{{\color{metacolor}\{\}}}$ or $\ensuremath{\mathit{id}}$.

As in $\ensuremath{\mathsf{PPC}}$, a match ($\mu, \nu, \ldots$) may succeed, fail ($\ensuremath{\mathtt{fail}}$)
or be undetermined ($\ensuremath{\mathtt{wait}}$). For $\ensuremath{\mathsf{PPC}_\mathtt{dB}}$, a successful match will
yield a substitution at level 1, as given by the following \emph{matching
operation}, where the rules are applied in order as in $\ensuremath{\mathsf{PPC}}$: \[
\begin{array}{rcl@{\qquad}l}
\match[n]{\termidxm{1}[j]}{u}                 & \ensuremath{\triangleq}  & \subs{\termidxv{1}[j]}{u} \\
\match[n]{\termidxm{i+1}[j]}{\termidxm{i}[j]} & \ensuremath{\triangleq}  & \ensuremath{{\color{metacolor}\{\}}} \\
\match[n]{\termapp{p}{q}}{\termapp{t}{u}}     & \ensuremath{\triangleq}  & \matchunion{\match[n]{p}{t}}{\match[n]{q}{u}} & \text{if $\termapp{t}{u}, \termapp{p}{q} \in \Matchable{\ensuremath{\mathsf{PPC}_\mathtt{dB}}}$} \\
\match[n]{p}{u}                               & \ensuremath{\triangleq}  & \ensuremath{\mathtt{fail}}                                    & \text{if $u, p \in \Matchable{\ensuremath{\mathsf{PPC}_\mathtt{dB}}}$} \\
\match[n]{p}{u}                               & \ensuremath{\triangleq}  & \ensuremath{\mathtt{wait}}                                   & \text{otherwise}
\end{array}
\] where disjoint union of matching is adapted to $\ensuremath{\mathsf{PPC}_\mathtt{dB}}$ from $\ensuremath{\mathsf{PPC}}$
in a straightforward way. The first two rules in the matching operation for
$\ensuremath{\mathsf{PPC}_\mathtt{dB}}$ are worth a comment. As the matching operation should be understood
in the context of a redex, the matchable symbols bound in the pattern are those
with primary index equal to 1. Thus, $\ensuremath{\mathsf{PPC}_\mathtt{dB}}$'s counter-part of the
membership check $x \in \theta$ from $\ensuremath{\mathsf{PPC}}$'s matching operation is a
simple syntactic check on the primary index. Similarly, $x \notin \theta$
corresponds to the primary index being greater than 1, as checked by the second
rule of the definition. However, a primary index $\termidxm{i+1}$ within the
pattern should match primary index $\termidxm{i}$ from the argument, since the
former is affected by an extra binder in a redex. For instance, in the term
$\termapp{(\termabs[1]{\termapp{\termidxm{2}[1]}{\termidxm{1}[1]}}{\termidxv{1}[1]})}{(\termapp{\termidxm{1}[1]}{t'})}$
the matchable $\termidxm{2}[1]$ is free and corresponds to $\termidxm{1}[1]$ in
the argument, while $\termidxm{1}[1]$ from the pattern is bound by the
abstraction. Its counter-part in $\ensuremath{\mathsf{PPC}}$ would be $\alpha$-equivalent to
$\termapp{(\termabs[\lista{x}]{\termapp{\termmatch{y}}{\termmatch{x}}}{\termvar{x}})}{(\termapp{\termmatch{y}}{t})}$.
Hence,
$\match[1]{\termapp{\termidxm{2}[1]}{\termidxm{1}[1]}}{\termapp{\termidxm{1}[1]}{t'}}
= \subs{\termidxv{1}[1]}{t'}$.

As for $\ensuremath{\mathsf{PPC}}$, an additional post-condition is checked over
$\match[n]{p}{u}$ to prevent indices from going out of scope. It requires
$\dom{\match[n]{p}{u}} = \set{\termidx{1}[1], \ldots, \termidx{1}[n]}$, which
essentially implies that all the bound indices are assigned a value by the
resulting substitution. This condition can be guaranteed by requesting
$\set{\termidx{1}[1], \ldots, \termidx{1}[n]} \subseteq \fm{p}$, for each
abstraction $\termabs[n]{p}{t}$ within a well-formed term. To illustrate the
need of such a check, consider the term
$\termapp{(\termabs[2]{\termidxm{1}[1]}{\termidxv{1}[2]})}{u'}$ (\emph{i.e.}~ the
$\ensuremath{\mathsf{PPC}_\mathtt{dB}}$ counter-part of
$\termapp{(\termabs[\lista{x,y}]{\termmatch{x}}{\termvar{y}})}{u}$, given in
Sec.~\ref{s:preliminaries:ppc}). If the matching
$\match[2]{\termidxm{1}[1]}{u'} = \subs{\termidxv{1}[1]}{u'}$ is considered
correct, then no replacement for the variable index $\termidxv{1}[2]$ in the
body of the abstraction is set, resulting in an ill-behaved operational
semantics.

\medskip
The reduction relation $\reduce[\ensuremath{\mathtt{dB}}]$ of $\ensuremath{\mathsf{PPC}_\mathtt{dB}}$ is given by the closure
by contexts of the rewriting rule: \[
\termapp{(\termabs[n]{p}{s})}{u} \rrule{\ensuremath{\mathtt{dB}}} \fdecv{\matchapply{\match[n]{p}{\fincv{u}}}{s}}
\] whenever $\match[n]{p}{\fincv{u}}$ is a decided match. The decrement
function for variable indices is applied to the reduct to compensate for the
loss of a binder over $s$. However, the variable indices of $u$ are not
affected by such binder in the redex. Hence the need of incrementing them prior
to the (eventual) substitution.

Following the reduction example given above for $\ensuremath{\mathsf{PPC}}$, consider these
codifications of $\mathsf{elim} =
\termabs[\lista{x}]{\termmatch{x}}{(\termabs[\lista{y}]{\termapp{\termvar{x}}{\termmatch{y}}}{\termvar{y}})}$
and
$\termabs[\lista{z}]{\termmatch{z}}{\termapp{\termapp{\termmatch{c}}{\termvar{z}}}{\termmatch{n}}}$
respectively:
$\termabs[1]{\termidxm{1}[1]}{(\termabs[1]{\termapp{\termidxv{1}[1]}{\termidxm{1}[1]}}{\termidxv{1}[1]})}$
and
$\termabs[1]{\termidxm{1}[1]}{\termapp{\termapp{\termidxm{1}[1]}{\termidxv{1}[1]}}{\termidxm{2}[1]}}$.
Note how the first occurrence of $\termidxv{1}[1]$ is actually bound by the
outermost abstraction, since abstractions do not bind variable indices in
their pattern. Similarly, the matchable index $\termidxm{1}[1]$ in the body
of
$\termabs[1]{\termidxm{1}[1]}{\termapp{\termapp{\termidxm{1}[1]}{\termidxv{1}[1]}}{\termidxm{2}[1]}}$
turns out to be free as well as $\termidxm{2}[1]$. Then, as expected, we have
the following sequence: \[
\termapp{(\termabs[1]{\termidxm{1}[1]}{(\termabs[1]{\termapp{\termidxv{1}[1]}{\termidxm{1}[1]}}{\termidxv{1}[1]})})}{(\termabs[1]{\termidxm{1}[1]}{\termapp{\termapp{\termidxm{1}[1]}{\termidxv{1}[1]}}{\termidxm{2}[1]}})}
\quad\reduce[\ensuremath{\mathtt{dB}}]\quad
\termabs[1]{\termapp{(\termabs[1]{\termidxm{1}[1]}{\termapp{\termapp{\termidxm{2}[1]}{\termidxv{1}[1]}}{\termidxm{3}[1]}})}{\termidxm{1}[1]}}{\termidxv{1}[1]}
\quad\reduce[\ensuremath{\mathtt{dB}}]\quad
\termabs[1]{\termapp{\termapp{\termidxm{2}[1]}{\termidxm{1}[1]}}{\termidxm{3}[1]}}{\termidxv{1}[1]}
\] In the first step,
$\termabs[1]{\termidxm{1}[1]}{\termapp{\termapp{\termidxm{1}[1]}{\termidxv{1}[1]}}{\termidxm{2}[1]}}$
is substituted for $\termidxv{1}[1]$ into the pattern
$\termapp{\termidxv{1}[1]}{\termidxm{1}[1]}$. The fact that the substitution
takes place within the context of a pattern forces the application of
$\fincm{\_}$, thus updating the matchable indices and obtaining
$\termabs[1]{\termidxm{1}[1]}{\termapp{\termapp{\termidxm{2}[1]}{\termidxv{1}[1]}}{\termidxm{3}[1]}}$.
Note that the increment and decrement added by the reduccion rule take no
effect as there are no free variable indices in the term. In the second step,
the resulting application is reduced, giving place to a term whose counter-part
in $\ensuremath{\mathsf{PPC}}$ would be equivalent to
$\termabs[\lista{y}]{\termapp{\termapp{\termmatch{c}}{\termmatch{y}}}{\termmatch{n}}}{\termvar{y}}$
(\emph{cf.}~ the reduction example in Sec.~\ref{s:preliminaries:ppc}).

\medskip
In the following sections $\ensuremath{\mathsf{PPC}_\mathtt{dB}}$ is shown to be equivalent to $\ensuremath{\mathsf{PPC}}$
in terms of expressive power and operational semantics. The main advantage of
this new presentation is that it gets rid of $\alpha$-conversion, since there
is no possible collision between free and bound variables/matchables. However,
there is one minor drawback with respect to the use of de Bruijn indices for
the standard $\ensuremath{\lambda}$-calculus. As mentioned above, when working with de
Bruijn indices in the standard $\ensuremath{\lambda}$-calculus, $\alpha$-equivalence
becomes syntactical equality.

Unfortunately, this is not the case when working with bidimensional indices.
For instance, consider the terms
$\termabs[2]{\termapp{\termidxm{1}[1]}{\termidxm{1}[2]}}{\termidxv{1}[1]}$ and
$\termabs[2]{\termapp{\termidxm{1}[2]}{\termidxm{1}[1]}}{\termidxv{1}[2]}$.
Both represent the function that decomposes an application and projects its
first component. But they differ in the way the secondary indices are assigned.
Moreover, one may be tempted to impose an order for the way the secondary
indices are assigned within the pattern to avoid this situation (recall that
the post-condition of the matching operation forces all bound symbols to appear
in the pattern). Given the dynamic nature of patterns in the $\ensuremath{\mathsf{PPC}}$
framework, this enforcement would not solve the problem since patterns may
reduce and such an order is not closed under reduction. For example, consider
$\termabs[2]{\termapp{(\termabs[2]{\termapp{\termidxm{1}[1]}{\termidxm{1}[2]}}{\termapp{\termidxv{1}[2]}{\termidxv{1}[1]}})}{(\termapp{\termidxm{1}[1]}{\termidxm{1}[2]})}}{\termidxv{1}[1]}
\reduce[\ensuremath{\mathtt{dB}}]
\termabs[2]{\termapp{\termidxm{1}[2]}{\termidxm{1}[1]}}{\termidxv{1}[1]}$.

Fortunately enough, this does not represent a problem from the implementation
point of view, since the ambiguity is local to a binder and does not imply the
need for ``renaming'' variables/matchables while reducing a term, \emph{i.e.}~ no
possible undesired capture can happen because of it. It is important to note
though, that in the sequel, when refering to equality over terms of
$\ensuremath{\mathsf{PPC}_\mathtt{dB}}$, it is not syntactical equality but equality modulo these
assignments for secondary indices that we are using.

\section{Preliminaries}
\label{s:preliminaries}

This section introduces preliminary concepts that guide our development and
will help the reader follow the new ideas presented in this work.

\subsection{The Pure Pattern Calculus}
\label{s:preliminaries:ppc}

We start by briefly introducing the \emph{Pure Pattern Calculus}
($\ensuremath{\mathsf{PPC}}$)~\cite{JayK09}, an extension of the $\ensuremath{\lambda}$-calculus where
virtually any term can be abstracted. This gives place to two versatile forms
of polymorphism that set the foundations for adding novel features to future
functional programming languages: namely \emph{path polymorphism} and
\emph{pattern polymorphism}. This work, however, focuses on implementation
related aspects of $\ensuremath{\mathsf{PPC}}$ and will not delve deeper into these new forms of
polymorphism. We refer the reader to~\cite{JayK09,Jay09} for an in-depth study
of them.

\medskip
Given an infinitely countable set of \emph{symbols} $\ensuremath{{\mathbb{V}}}$ ($x, y, z,
\ldots$), the sets of \emph{terms} $\Term{\ensuremath{\mathsf{PPC}}}$ and \emph{contexts} are
given by the following grammar: \[
\begin{array}{c@{\qquad}c}
\begin{array}{rrcl}
\textbf{Terms}    & t         & \ensuremath{:\coloneq}  & \termvar{x} \mid \termmatch{x} \mid \termapp{t}{t} \mid \termabs[\theta]{t}{t}
\end{array}
&
\begin{array}{rrcl}
\textbf{Contexts} & \ctxt{C}  & \ensuremath{:\coloneq}  & \Box \mid \termapp{\ctxt{C}}{t} \mid \termapp{t}{\ctxt{C}} \mid \termabs[\theta]{\ctxt{C}}{t} \mid \termabs[\theta]{t}{\ctxt{C}}
\end{array}
\end{array}
\] where $\theta$ is a list of symbols that are bound by the abstraction. A
symbol $\termvar{x}$ appearing in a term is dubbed a \emph{variable symbol}
while $\termmatch{x}$ is called a \emph{matchable symbol}. In particular,
given $\termabs[\theta]{p}{t}$, $\theta$ binds variable symbols in the
\emph{body} $t$ and matchable symbols in the \emph{pattern} $p$. Thus, the set
of \emph{free variables} and \emph{free matchables} of a term $t$, written
$\fv{t}$ and $\fm{t}$ respectively, are inductively defined as: \[
\begin{array}{c@{\qquad}c}
\begin{array}{rcl}
\fv{\termvar{x}}            & \ensuremath{\triangleq}  & \set{x} \\
\fv{\termmatch{x}}          & \ensuremath{\triangleq}  & \emptyset \\
\fv{\termapp{t}{u}}         & \ensuremath{\triangleq}  & \fv{t} \cup \fv{u} \\
\fv{\termabs[\theta]{p}{t}} & \ensuremath{\triangleq}  & \fv{p} \cup (\fv{t} \setminus \theta)
\end{array}
&
\begin{array}{rcl}
\fm{\termvar{x}}            & \ensuremath{\triangleq}  & \emptyset \\
\fm{\termmatch{x}}          & \ensuremath{\triangleq}  & \set{x} \\
\fm{\termapp{t}{u}}         & \ensuremath{\triangleq}  & \fm{t} \cup \fm{u} \\
\fm{\termabs[\theta]{p}{t}} & \ensuremath{\triangleq}  & (\fm{p} \setminus \theta) \cup \fm{t}
\end{array}
\end{array}
\] A term is said to be \emph{closed} if it has no free variables. Note that
free matchables are allowed, and should be understood as \emph{constants} or
\emph{constructors} for data structures. The pattern $p$ of an abstraction
$\termabs[\theta]{p}{t}$ is \emph{linear} if every symbol $x \in \theta$ occurs
at most once in $p$.

\begin{wrapfigure}{R}{0.2\textwidth}
\begin{tikzpicture}[baseline=(current bounding box.center),->,auto,node distance=5pt]
\node (ABS1a)                               {$\vphantom{(}\ensuremath{\lambda}_{\lista{x}}$};
\node (PTN1)  [right of=ABS1a, xshift=6pt]  {$\vphantom{(}\termmatch{x}$};
\node (ABS1b) [right of=PTN1,  xshift=1pt]  {$\vphantom{(}.($};
\node (ABS2a) [right of=ABS1b, xshift=6pt]  {$\vphantom{(}\ensuremath{\lambda}_{\lista{y}}$};
\node (PTN2a) [right of=ABS2a, xshift=6pt]  {$\vphantom{(}\termvar{x}$};
\node (PTN2b) [right of=PTN2a, xshift=3pt]  {$\vphantom{(}\termmatch{y}$};
\node (ABS2b) [right of=PTN2b]              {$\vphantom{(}.$};
\node (BODY)  [right of=ABS2b]              {$\vphantom{(}\termvar{y}$};
\node (ABS1c) [right of=BODY]               {$\vphantom{(})$};

\path (ABS1a.south) edge [bend right=45] node[left] {} (PTN1.south)
      (ABS1a.south) edge [bend right=90] node[left] {} (PTN2a.south)
      (ABS2a.south) edge [bend right=90] node[left] {} (PTN2b.south)
      (ABS2a.south) edge [bend right=90] node[left] {} (BODY.south);
\end{tikzpicture}
\end{wrapfigure}

To illustrate how variables and matchables are bound, consider the function
$\mathsf{elim}$ defined as
$\termabs[\lista{x}]{\termmatch{x}}{(\termabs[\lista{y}]{\termapp{\termvar{x}}{\termmatch{y}}}{\termvar{y}})}$.
The inner abstraction binds the only occurrence of the matchable
$\termmatch{y}$ in the pattern $\termapp{\termvar{x}}{\termmatch{y}}$ and that
of the variable $\termvar{y}$ in the body $\termvar{y}$. However, the
occurrence of $\termvar{x}$ in $\termapp{\termvar{x}}{\termmatch{y}}$ is not
bound by the inner abstraction, as it is excluded from $\lista{y}$, acting as a
place-holder in that pattern. It is the outermost abstraction that binds both
$\termvar{x}$ in the inner pattern and $\termmatch{x}$ in the outermost
pattern. This is graphically depicted above.

\medskip
A \emph{substitution} ($\sigma, \rho, \ldots$) is a partial function from
variables to terms. The substitution $\sigma = \subs{x_i}{u_i}_{i \in I}$,
where $I$ is a set of indices, maps the variable $x_i$ into the term $u_i$ (\emph{i.e.}~
$\funcapply{\sigma}{x_i} \ensuremath{\triangleq} u_i$) for each $i \in I$. Thus, its
\emph{domain} and \emph{image} are defined as $\dom{\sigma} \ensuremath{\triangleq}
\set{x_i}_{i \in I}$ and $\img{\sigma} \ensuremath{\triangleq} \set{u_i}_{i \in I}$
respectively. For convenience, a substitution $\sigma$ is usually turned into a
total function by defining $\funcapply{\sigma}{x} \ensuremath{\triangleq} x$ for every $x \notin
\dom{\sigma}$. Then, the identity substitution is denoted $\ensuremath{{\color{metacolor}\{\}}}$ or simply
$\ensuremath{\mathit{id}}$.

A \emph{match} ($\mu, \nu, \ldots$) may be successful (yielding a
substitution), it may fail (returning a special symbol $\ensuremath{\mathtt{fail}}$) or be
undetermined (denoted by a special symbol $\ensuremath{\mathtt{wait}}$). The cases of success
and failure are called \emph{decided matches}. All concepts and notation
relative to substitutions are extended to matches so that, for example, the
domain of $\ensuremath{\mathtt{fail}}$ is empty while that of $\ensuremath{\mathtt{wait}}$ is undefined. The
sets of free variable and free matchable symbols of $\sigma$ are defined as the
union of $\fv{\subsapply{\sigma}{x}}$ and $\fm{\subsapply{\sigma}{x}}$ for
every $x \in \dom{\sigma}$ respectively, while $\fv{\ensuremath{\mathtt{fail}}} =
\fm{\ensuremath{\mathtt{fail}}} = \emptyset$ and they are undefined for $\ensuremath{\mathtt{wait}}$. The set
of symbols of a substitution is defined as $\sym{\sigma} \ensuremath{\triangleq} \dom{\sigma}
\cup \fv{\sigma} \cup \fm{\sigma}$. The predicate $\pavoids{x}{\sigma}$ states
that $x \notin \sym{\sigma}$. It is extended to sets and matches as expected.
In particular, $\pavoids{\theta}{\mu}$ implies that $\mu$ must be decided.

The result of applying a substitution $\sigma$ to a term $t$, denoted
$\subsapply{\sigma}{t}$, is inductively defined as: \[
\begin{array}{c@{\qquad}c}
\begin{array}{rcl@{\quad}l}
\subsapply{\sigma}{\termvar{x}}             & \ensuremath{\triangleq}  & \funcapply{\sigma}{x} \\
\subsapply{\sigma}{\termmatch{x}}           & \ensuremath{\triangleq}  & \termmatch{x}
\end{array}
&
\begin{array}{rcl@{\quad}l}
\subsapply{\sigma}{(\termapp{t}{u})}        & \ensuremath{\triangleq}  & \termapp{\subsapply{\sigma}{t}}{\subsapply{\sigma}{u}} \\
\subsapply{\sigma}{\termabs[\theta]{p}{t}}  & \ensuremath{\triangleq}  & \termabs[\theta]{\subsapply{\sigma}{p}}{\subsapply{\sigma}{t}}  & \text{if $\pavoids{\theta}{\sigma}$}
\end{array}
\end{array} \] The restriction in the case of the abstraction is required to
avoid undesired captures of variables/matchables. However, it can always be
satisfied by resorting to $\alpha$-conversion.

The result of applying a match $\mu$ to a term $t$, denoted
$\matchapply{\mu}{t}$, is defined as:
\begin{inparaenum}
  \item if $\mu = \sigma$ a substitution, then $\matchapply{\mu}{t} \ensuremath{\triangleq}
  \subsapply{\sigma}{t}$;
  \item if $\mu = \ensuremath{\mathtt{fail}}$, then $\matchapply{\mu}{t} \ensuremath{\triangleq}
  \termabs[\lista{x}]{\termmatch{x}}{\termvar{x}}$ (\emph{i.e.}~ the identity function);
  or
  \item if $\mu = \ensuremath{\mathtt{wait}}$, then $\matchapply{\mu}{t}$ is undefined.
\end{inparaenum}

The \emph{composition} $\subscomp{\sigma}{\sigma'}$ of substitutions is defined
as usual, \emph{i.e.}~ $\subsapply{(\subscomp{\sigma}{\sigma'})}{x} \ensuremath{\triangleq}
\subsapply{\sigma}{(\subsapply{\sigma'}{x})}$, and the notion is extended to
matches by defining $\matchcomp{\mu}{\mu'} \ensuremath{\triangleq} \ensuremath{\mathtt{fail}}$ if any of the two
matches is $\ensuremath{\mathtt{fail}}$. Otherwise, if at least one of the two is
$\ensuremath{\mathtt{wait}}$, then $\matchcomp{\mu}{\mu'} \ensuremath{\triangleq} \ensuremath{\mathtt{wait}}$. In particular,
$\matchcomp{\ensuremath{\mathtt{fail}}}{\ensuremath{\mathtt{wait}}} = \ensuremath{\mathtt{fail}}$. The \emph{disjoint union}
$\matchunion{\mu}{\mu'}$ of matches is defined as follows:
\begin{inparaenum}
  \item if $\mu = \ensuremath{\mathtt{fail}}$ or $\mu' = \ensuremath{\mathtt{fail}}$, then
  $\matchunion{\mu}{\mu'} \ensuremath{\triangleq} \ensuremath{\mathtt{fail}}$; else
  \item if $\mu = \ensuremath{\mathtt{wait}}$ or $\mu' = \ensuremath{\mathtt{wait}}$, then
  $\matchunion{\mu}{\mu'} \ensuremath{\triangleq} \ensuremath{\mathtt{wait}}$; otherwise
  \item both $\mu$ and $\mu'$ are substitutions and if $\dom{\mu} \cap
  \dom{\mu'} \neq \emptyset$, then $\matchunion{\mu}{\mu'} \ensuremath{\triangleq} \ensuremath{\mathtt{fail}}$,
  else: \[\subsapply{(\matchunion{\mu}{\mu'})}{x} \ensuremath{\triangleq}
  \begin{cases}
  \subsapply{\mu}{x}  & \text{if $x \in \dom{\mu}$} \\
  \subsapply{\mu'}{x} & \text{if $x \in \dom{\mu'}$} \\
  x                   & \text{otherwise}
  \end{cases}\]
\end{inparaenum}
Disjoint union is used to guarantee that the matching operation is
deterministic.

\medskip
Before introducing the matching operation it is necessary to motivate the
concept of \emph{matchable form}. The pattern
$\termapp{\termmatch{x}}{\termmatch{y}}$ allows, at first, to decompose
arbitrary applications, which may lead to the loss of confluence. For
instance: \[
\begin{array}{llllll}
\termapp{(\termabs[\lista{x,y}]{\termapp{\termmatch{x}}{\termmatch{y}}}{\termvar{y}})}{(\termapp{(\termabs[\lista{w}]{\termmatch{w}}{\termapp{\termmatch{z_0}}{\termmatch{z_1}}})}{\termmatch{z_0}})} & \reduce & \termapp{(\termabs[\lista{x,y}]{\termapp{\termmatch{x}}{\termmatch{y}}}{\termvar{y}})}{(\termapp{\termmatch{z_0}}{\termmatch{z_1}})} & \reduce & \termmatch{z_1} \\
\termapp{(\termabs[\lista{x,y}]{\termapp{\termmatch{x}}{\termmatch{y}}}{\termvar{y}})}{(\termapp{(\termabs[\lista{w}]{\termmatch{w}}{\termapp{\termmatch{z_0}}{\termmatch{z_1}}})}{\termmatch{z_0}})} & \reduce & \termmatch{z_0}
\end{array}
\] This issue arises when allowing to match the pattern
$\termapp{\termmatch{x}}{\termmatch{y}}$ with an application that may still be
reduced, like the argument
$\termapp{(\termabs[\lista{w}]{\termmatch{w}}{\termapp{\termmatch{z_0}}{\termmatch{z_1}}})}{\termmatch{z_0}}$
of the outermost redex in the example above. To avoid this situation it is
required for the match to be decided only if the argument is sufficiently
evaluated. An analogous issue occurs if the pattern is reducible. Thus, both
the pattern and the argument must be in matchable form for the match to be
decided. The set of \emph{data structures} $\TermData{\ensuremath{\mathsf{PPC}}}$ and
\emph{matchable forms} $\Matchable{\ensuremath{\mathsf{PPC}}}$ are given by the following
grammar: \[
\begin{array}{c@{\qquad}c}
\begin{array}{rrcl}
\textbf{Data structures}  & d & \ensuremath{:\coloneq}  & \termmatch{x} \mid \termapp{d}{t}
\end{array}
&
\begin{array}{rrcl}
\textbf{Matchable forms}  & m & \ensuremath{:\coloneq}  & d \mid \termabs[\theta]{t}{t}
\end{array}
\end{array} \]

The \emph{matching operation} $\match[\theta]{p}{u}$ of a pattern $p$ against a
term $u$ relative to a list of symbols $\theta$ is defined as the application,
in order, of the following equations: \[
\begin{array}{rcl@{\qquad}l}
\match[\theta]{\termmatch{x}}{u}                & \ensuremath{\triangleq}  & \subs{\termvar{x}}{u}                                   & \text{if $x \in \theta$} \\
\match[\theta]{\termmatch{x}}{\termmatch{x}}    & \ensuremath{\triangleq}  & \ensuremath{{\color{metacolor}\{\}}}                                                 & \text{if $x \notin \theta$} \\
\match[\theta]{\termapp{p}{q}}{\termapp{t}{u}}  & \ensuremath{\triangleq}  & \matchunion{\match[\theta]{p}{t}}{\match[\theta]{q}{u}} & \text{if $\termapp{t}{u}, \termapp{p}{q} \in \Matchable{\ensuremath{\mathsf{PPC}}}$} \\
\match[\theta]{p}{u}                            & \ensuremath{\triangleq}  & \ensuremath{\mathtt{fail}}                                              & \text{if $u, p \in \Matchable{\ensuremath{\mathsf{PPC}}}$} \\
\match[\theta]{p}{u}                            & \ensuremath{\triangleq}  & \ensuremath{\mathtt{wait}}                                             & \text{otherwise}
\end{array}
\] An additional check is imposed, namely $\dom{\match[\theta]{p}{u}} =
\theta$. Otherwise, $\match[\theta]{p}{u} \ensuremath{\triangleq} \ensuremath{\mathtt{fail}}$. This last
condition is necessary to prevent bound symbols from going out of scope when
reducing. It can be easily guaranteed though by requesting, for each
abstraction $\termabs[\theta]{p}{t}$, that $\theta \subseteq \fm{p}$.
For instance, consider the term
$\termapp{(\termabs[\lista{x,y}]{\termmatch{x}}{\termvar{y}})}{u}$. Without
this final check, matching the argument $u$ against the pattern
$\termmatch{x}$ would yield a substitution $\subs{\termvar{x}}{u}$ and no
term would be assigned to the variable $\termvar{y}$ in the body of the
abstraction.

\medskip
Finally, the reduction relation $\reduce[\ensuremath{\mathtt{PPC}}]$ of $\ensuremath{\mathsf{PPC}}$ is given by the
closure by contexts of the rewriting rule: \[
\termapp{(\termabs[\theta]{p}{s})}{u} \rrule{\ensuremath{\mathtt{PPC}}} \matchapply{\match[\theta]{p}{u}}{s}
\] whenever $\match[\theta]{p}{u}$ is a decided match. To illustrate the
operational semantics of $\ensuremath{\mathsf{PPC}}$ consider the term $\mathsf{elim}$
introduced above, applied to the function
$\termabs[\lista{z}]{\termmatch{z}}{\termapp{\termapp{\termmatch{c}}{\termvar{z}}}{\termmatch{n}}}$
where the free matchables $\termmatch{c}$ and $\termmatch{n}$ can be seen as
constructors for lists $\mathsf{cons}$ and $\mathsf{nil}$ respectively: \[
\termapp{(\termabs[\lista{x}]{\termmatch{x}}{(\termabs[\lista{y}]{\termapp{\termvar{x}}{\termmatch{y}}}{\termvar{y}})})}{(\termabs[\lista{z}]{\termmatch{z}}{\termapp{\termapp{\termmatch{c}}{\termvar{z}}}{\termmatch{n}}})}
\quad\reduce[\ensuremath{\mathtt{PPC}}]\quad
\termabs[\lista{y}]{\termapp{(\termabs[\lista{z}]{\termmatch{z}}{\termapp{\termapp{\termmatch{c}}{\termvar{z}}}{\termmatch{n}}})}{\termmatch{y}}}{\termvar{y}}
\quad\reduce[\ensuremath{\mathtt{PPC}}]\quad
\termabs[\lista{y}]{\termapp{\termapp{\termmatch{c}}{\termmatch{y}}}{\termmatch{n}}}{\termvar{y}}
\] In the first step,
$\termabs[\lista{z}]{\termmatch{z}}{\termapp{\termapp{\termmatch{c}}{\termvar{z}}}{\termmatch{n}}}$
is substituted for $\termvar{x}$ into the pattern
$\termapp{\termvar{x}}{\termmatch{y}}$. In the second step, the resulting
application, which resides in the pattern, is reduced. The resulting term, when
applied to an argument, will yield a successful matching only if this argument
is a compound data of the form
$\termapp{\termapp{\termmatch{c}}{t}}{\termmatch{n}}$.

This relation is shown to be \emph{confluent} (CR) based on the matching
operation introduced above.

\begin{theorem}[\cite{JayK09}]
The reduction relation $\reduce[\ensuremath{\mathtt{PPC}}]$ is confluent (CR).
\label{t:preliminaries:ppc:cr}
\end{theorem}

\subsection{de Bruijn indices}
\label{s:preliminaries:indices}

We introduce next de Bruijn indices for the $\ensuremath{\lambda}$-calculus. Among the
many presentations of de Bruijn indices in the literature, we will follow that
of~\cite{KamareddineR95} as our development builds upon their ideas. In
particular, we choose to work with the presentation where indices are partially
updated as the term is being traversed by the substitution operation (details
below). We refer the reader to~\cite{KamareddineR95} for the equivalent version
where the update is performed once at the end of the substitution process. We
introduce now the \emph{$\ensuremath{\lambda}$-calculus with de Bruijn indices}
($\ensuremath{\lambda}_\mathtt{dB}$ for short).

\medskip
The sets of \emph{terms} $\Term{\ensuremath{\lambda}_\mathtt{dB}}$ and \emph{contexts} are given by
the following grammar: \[
\begin{array}{c@{\qquad}c}
\begin{array}{rrcl}
\textbf{Terms}    & t         & \ensuremath{:\coloneq}  & \termidxv{i} \mid \termapp{t}{t} \mid \termabsi{t} \\
\end{array}
&
\begin{array}{rrcl}
\textbf{Contexts} & \ctxt{C}  & \ensuremath{:\coloneq}  & \Box \mid \termapp{\ctxt{C}}{t} \mid \termapp{t}{\ctxt{C}} \mid \termabsi{\ctxt{C}}
\end{array}
\end{array}
\] where $\termidxv{i} \in \ensuremath{{\mathbb{N}}}_{\geq 1}$ is called an \emph{index}.
Indices are place-holders indicating the distance to the binding abstraction.
In the context of the $\ensuremath{\lambda}_\mathtt{dB}$-calculus, indices are also called
\emph{variables}. Thus, the \emph{free variables} of a term are inductively
defined as: $\fv{\termidxv{i}} \ensuremath{\triangleq} \set{\termidx{i}}$; $\fv{\termapp{t}{u}}
\ensuremath{\triangleq} \fv{t} \cup \fv{u}$; and $\fv{\termabsi{t}} \ensuremath{\triangleq} \fv{t} - 1$, where
$X - k$ stands for subtracting $k$ from each element of the set $X$, removing
those that result in a non-positive index.

In order to define $\ensuremath{\beta}$-reduction \emph{\`{a} la} de Bruijn, the
substitution of an index $\termidxv{i}$ for a term $u$ in a term $t$ must be
defined. Therefore, it is necessary to identify among the indices of the term
$t$, those corresponding to $\termidx{i}$. Furthermore, the indices of $u$
should be updated in order to preserve the correct bindings after the
replacement of the variable by $u$. To that end, the \emph{increment at depth
$k$} for variables in a term $t$, written $\fincv[k]{t}$, is inductively
defined as follows: \[
\begin{array}{c@{\qquad\qquad}c}
\begin{array}{rcll}
\fincv[k]{\termidxv{i}}   & \ensuremath{\triangleq}  & \begin{cases}
                                      \termidxv{i+1}  & \text{if $i > k$} \\
                                      \termidxv{i}    & \text{if $i \leq k$}
                                      \end{cases}
\end{array}
&
\begin{array}{rcll}
\fincv[k]{\termapp{t}{u}} & \ensuremath{\triangleq}  & \termapp{\fincv[k]{t}}{\fincv[k]{u}} \\
\fincv[k]{\termabsi{t}}   & \ensuremath{\triangleq}  & \termabsi{\fincv[k+1]{t}}
\end{array}
\end{array}
\] Then, the \emph{substitution at level $i$} of a term $u$ in a term $t$,
denoted $\subsapply{\subs{\termidx{i}}{u}}{t}$, is defined as a partial
function mapping free variables at level $i$ to terms, performing the
appropriate updates as it traverses the substituted term, to avoid undesired
captures. \[
\begin{array}{c@{\qquad\qquad}c}
\begin{array}{rcl@{\quad}l}
\subsapply{\subs{\termidxv{i}}{u}}{\termidxv{i'}}     & \ensuremath{\triangleq}  & \begin{cases}
                                                                  \termidxv{i'-1} & \text{if $i' > i$} \\
                                                                  u               & \text{if $i' = i$} \\
                                                                  \termidxv{i'}   & \text{if $i' < i$}
                                                                  \end{cases}
\end{array}
&
\begin{array}{rcl@{\quad}l}
\subsapply{\subs{\termidxv{i}}{u}}{(\termapp{t}{s})}  & \ensuremath{\triangleq}  & \termapp{\subsapply{\subs{\termidxv{i}}{u}}{t}}{\subsapply{\subs{\termidxv{i}}{u}}{s}} \\
\subsapply{\subs{\termidxv{i}}{u}}{\termabsi{t}}      & \ensuremath{\triangleq}  & \termabsi{\subsapply{\subs{\termidxv{i+1}}{\fincv[0]{u}}}{t}}
\end{array}
\end{array} \] It is worth noticing that this substitution should be
interpreted in the context of a redex, where a binder is removed and its bound
index substituted. This forces to update the free indices, that might be
captured by an outermost abstraction, as done by the first case of the
substitution over a variable $\termidxv{i'}$. Hence, preserving the correct
bindings.

Finally, the reduction relation $\reduce[\ensuremath{\mathtt{dB}}]$ of the
$\ensuremath{\lambda}_\mathtt{dB}$-calculus is given by the closure by contexts of the rewriting
rule: \[
\termapp{(\termabsi{s})}{u} \rrule{\ensuremath{\mathtt{dB}}} \subsapply{\subs{\termidxv{1}}{u}}{s}
\]

Also, embeddings between the $\ensuremath{\lambda}$-calculus and $\ensuremath{\lambda}_\mathtt{dB}$ are
defined: $\toLambdaX{\_} : \Term{\ensuremath{\lambda}} \to \Term{\ensuremath{\lambda}_\mathtt{dB}}$ and
$\toLambda{\_} : \Term{\ensuremath{\lambda}_\mathtt{dB}} \to \Term{\ensuremath{\lambda}}$, in such a way
that they are the inverse of each other and they allow to simulate one
calculus into the other:

\begin{theorem}[\cite{KamareddineR95}]
Let $t \in \Term{\ensuremath{\lambda}}$ and $s \in \Term{\ensuremath{\lambda}_\mathtt{dB}}$. Then,
\begin{enumerate}
  \item \label{t:preliminaries:indices:simulation:lambdax} If $t
  \reduce[\ensuremath{\beta}] t'$, then $\toLambdaX{t} \reduce[\ensuremath{\mathtt{dB}}] \toLambdaX{t'}$.

  \item \label{t:preliminaries:indices:simulation:lambda} If $s
  \reduce[\ensuremath{\mathtt{dB}}] s'$, then $\toLambda{s} \reduce[\ensuremath{\beta}] \toLambda{s'}$.
\end{enumerate}
\label{t:preliminaries:indices:simulation}
\end{theorem}

This shows that both formalisms ($\ensuremath{\lambda}$-calculus and $\ensuremath{\lambda}_\mathtt{dB}$)
have exactly the same operational semantics.

As an example to illustrate both reduction in the $\ensuremath{\lambda}_\mathtt{dB}$-calculus and
its equivalence with the $\ensuremath{\lambda}$-calculus, consider the following terms:
$\termapp{\termapp{(\termabs{z}{\termabs{y}{z}})}{(\termabs{x}{x})}}{(\termabs{x}{\termapp{x}{x}})}$
and
$\termapp{\termapp{(\termabsi{\termabsi{\termidxv{2}}})}{(\termabsi{\termidxv{1}})}}{(\termabsi{\termapp{\termidxv{1}}{\termidxv{1}}})}$.
The reader can verify that both expressions encode the same function in its
respective calculus. As expected, their operational semantics coincide \[
\begin{array}{c@{\quad}c@{\quad}c@{\quad}c@{\quad}c}
\termapp{\termapp{(\termabs{z}{\termabs{y}{z}})}{(\termabs{x}{x})}}{(\termabs{x}{\termapp{x}{x}})}
& \reduce[\ensuremath{\beta}] &
\termapp{(\termabs{y}{\termabs{x}{x}})}{(\termabs{x}{\termapp{x}{x}})}
& \reduce[\ensuremath{\beta}] &
\termabs{x}{x} \\
\termapp{\termapp{(\termabsi{\termabsi{\termidxv{2}}})}{(\termabsi{\termidxv{1}})}}{(\termabsi{\termapp{\termidxv{1}}{\termidxv{1}}})}
& \reduce[\ensuremath{\mathtt{dB}}] &
\termapp{(\termabsi{\termabsi{\termidxv{1}}})}{(\termabsi{\termapp{\termidxv{1}}{\termidxv{1}}})}
& \reduce[\ensuremath{\mathtt{dB}}] &
\termabsi{\termidxv{1}} \\
\end{array} \]

\section{Translation}
\label{s:translation}

This section introduces translations between $\ensuremath{\mathsf{PPC}}$ and $\ensuremath{\mathsf{PPC}_\mathtt{dB}}$ (back
and forth). The goal is to show that these interpretations are suitable to
simulate one calculus into the other. Moreover, the proposed translations turn
out to be the inverse of each other (modulo $\alpha$-conversion) and, as we
will see in Sec.~\ref{s:bisimulation}, they allow to formalise a strong
bisimulation between the two calculi.

\medskip
We start with the translation from $\ensuremath{\mathsf{PPC}}$ to $\ensuremath{\mathsf{PPC}_\mathtt{dB}}$. It takes the
term to be translated together with two lists of lists of symbols that dictate
how the variables and matchables of the terms should be interpreted
respectively. We use lists of lists since the first dimension indicates the
distance to the binder, while the second identifies the symbol among the
multiple bound ones.

Given the lists of lists $X$ and $Y$, we denote by $\listconc{X}{Y}$ their
concatenation. To improve readability, when it is clear from context, we also
write $\listconc{\theta}{X}$ with $\theta$ a list of symbols to denote
$\listconc{\lista{\theta}}{X}$ where $\lista{\_}$ denotes the list constructor.
We use set operations like union and intersection over lists to denote the
union/intersection of its underlying sets.

\begin{definition}
Given a term $t \in \Term{\ensuremath{\mathsf{PPC}}}$ and lists of lists of symbols $V$ and $M$
such that $\fv{t} \subseteq \bigcup_{V' \in V}{V'}$ and $\fm{t} \subseteq
\bigcup_{M' \in M}{M'}$, the \emph{translation of $t$ relative to $V$ and $M$},
written $\toPPCX[V][M]{t}$, is inductively defined as follows: \[
\begin{array}{rcl@{\quad}l}
\toPPCX[V][M]{\termvar{x}}            & \ensuremath{\triangleq}  & \termidxv{i}[j] & \text{where $i = \min\set{i' \mid x \in V_{i'}}$ and $j = \min\set{j' \mid x = V_{ij'}}$} \\
\toPPCX[V][M]{\termmatch{x}}          & \ensuremath{\triangleq}  & \termidxm{i}[j] & \text{where $i = \min\set{i' \mid x \in M_{i'}}$ and $j = \min\set{j' \mid x = M_{ij'}}$} \\
\toPPCX[V][M]{\termapp{t}{u}}         & \ensuremath{\triangleq}  & \termapp{\toPPCX[V][M]{t}}{\toPPCX[V][M]{u}} \\
\toPPCX[V][M]{\termabs[\theta]{p}{t}} & \ensuremath{\triangleq}  & \termabs[\fsize{\theta}]{\toPPCX[V][\listconc{\theta}{M}]{p}}{\toPPCX[\listconc{\theta}{V}][M]{t}}
\end{array}
\] Let $x_1, x_2, \ldots$ be an enumeration of $\ensuremath{{\mathbb{V}}}$. Then, the
\emph{translation} of $t$ to $\ensuremath{\mathsf{PPC}_\mathtt{dB}}$, written simply $\toPPCX{t}$, is
defined as $\toPPCX[X][X]{t}$ where $X = \lista{\lista{x_1}, \ldots,
\lista{x_n}}$ such that $\fv{t} \cup \fm{t} \subseteq \set{x_1, \ldots, x_n}$.
\label{d:translation:to-ppcx}
\end{definition}

For example, consider the term $s_0 =
\termapp{(\termabs[\lista{x}]{\termapp{\termmatch{y}}{\termmatch{x}}}{\termvar{x}})}{(\termapp{\termmatch{y}}{s'_0})}$
with $\fv{s'_0} = \set{y}$ and $\fm{s'_0} = \set{y}$. Then,
$\toPPCX[\lista{\lista{y}}][\lista{\lista{y}}]{s_0} =
\termapp{(\termabs[1]{\termapp{\toPPCX[\lista{\lista{y}}][\lista{\lista{x},\lista{y}}]{\termmatch{y}}}{\toPPCX[\lista{\lista{y}}][\lista{\lista{x},\lista{y}}]{\termmatch{x}}}}{\toPPCX[\lista{\lista{x},\lista{y}}][\lista{\lista{y}}]{\termvar{x}}})}{(\termapp{\toPPCX[\lista{\lista{y}}][\lista{\lista{y}}]{\termmatch{y}}}{\toPPCX[\lista{\lista{y}}][\lista{\lista{y}}]{s'_0}})}
=
\termapp{(\termabs[1]{\termapp{\termidxm{2}[1]}{\termidxm{1}[1]}}{\termidxv{1}[1]})}{(\termapp{\termidxm{1}[1]}{\toPPCX[\lista{\lista{y}}][\lista{\lista{y}}]{s'_0}})}$.
Note that the inicialisation of $V$ and $M$ with singleton elements implies
that each free variable/matchable in the term will be assigned a distinct
primary index (when interpreted at the same depth), following de Bruijn's
original ideas: let $s_1 =
\termapp{(\termabs[\lista{x}]{\termapp{\termmatch{y}}{\termmatch{x}}}{\termvar{x}})}{(\termapp{\termmatch{y}}{\termvar{z}})}$,
then $\toPPCX[\lista{\lista{y},\lista{z}}][\lista{\lista{y},\lista{z}}]{s_1} =
\termapp{(\termabs[1]{\termapp{\termidxm{2}[1]}{\termidxm{1}[1]}}{\termidxv{1}[1]})}{(\termapp{\termidxm{1}[1]}{\termidxv{2}[1]})}$.

\medskip
Our main goal is to prove that $\ensuremath{\mathsf{PPC}_\mathtt{dB}}$ simulates $\ensuremath{\mathsf{PPC}}$ via this
embedding. For this purpose we need to state first some auxiliary lemmas that
prove how the translation behaves with respect to the substitution and the
matching operation. We start with a technical result concerning the increment
functions for variable and matchable indices. Notation $\fincv[k]{t}[n]$ stands
for $n$ consecutive applications of $\fincv[k]{\_}$ over $t$ (similarly for
$\fincm[k]{t}[n]$).

\begin{lemma}
Let $t \in \Term{\ensuremath{\mathsf{PPC}}}$, $k \geq 0$, $i \geq 1$ and $n \geq k + i$ such
that $X_l \cap (\fv{t} \cup \fm{t}) = \emptyset$ for all $l \in [k+1,k+i-1]$.
Then,
\begin{enumerate}
  \item\label{l:translation:to-ppcx-upd:var}
  $\toPPCX[\listconc{\listconc{X_1}{\ldots}}{X_n}][M]{t} =
  \fincv[k]{\toPPCX[\listconc{\listconc{\listconc{X_1}{\ldots}}{X_k}}{\listconc{\listconc{X_{k+i}}{\ldots}}{X_n}}][M]{t}}[i-1]$.

  \item\label{l:translation:to-ppcx-upd:match}
  $\toPPCX[V][\listconc{\listconc{X_1}{\ldots}}{X_n}]{t} =
  \fincm[k]{\toPPCX[V][\listconc{\listconc{\listconc{X_1}{\ldots}}{X_k}}{\listconc{\listconc{X_{k+i}}{\ldots}}{X_n}}]{t}}[i-1]$.
\end{enumerate}
\label{l:translation:to-ppcx-upd}
\end{lemma}

\input{proofs/translation/to-ppcx-upd}

The translation of a substitution $\sigma$ requires an enumeration $\theta$
such that $\dom{\sigma} \subseteq \theta$ to be provided. It is then defined as
$\toPPCX[V][M]{\sigma}[\theta] \ensuremath{\triangleq}
\subs{\termidxv{1}[j]}{\toPPCX[V][M]{\subsapply{\sigma}{x_j}}}_{x_j \in \dom{\sigma}}$.
Note how substitutions from $\ensuremath{\mathsf{PPC}}$ are mapped into substitutions at level 1 in
the $\ensuremath{\mathsf{PPC}_\mathtt{dB}}$ framework. This suffices since substitutions are only meant to
be created in the context of a redex. When acting at arbitrary depth on a term,
substitutions are shown to behave properly.

\begin{lemma}
Let $s \in \Term{\ensuremath{\mathsf{PPC}}}$, $\sigma$ be a substitution,
$\theta$ be an enumeration such that $\dom{\sigma}
\subseteq \theta$ and $Y$ be a list of $i-1$ lists of symbols such that
$(\bigcup_{Y' \in Y}{Y'}) \cap \theta = \emptyset$ and
$(\bigcup_{Y' \in Y}{Y'}) \cap
(\bigcup_{x_j \in \theta}{\fv{\subsapply{\sigma}{\termvar{x_j}}}}) =
\emptyset$. Then,
$\toPPCX[\listconc{Y}{X}][M]{\subsapply{\sigma}{s}} =
\fdecv[i-1]{\subsapply{\subs{\termidxv{i}[j]}{\fincv[i-1]{\toPPCX[\listconc{Y}{X}][M]{\subsapply{\sigma}{\termvar{x_j}}}}}_{x_j \in \dom{\sigma}}}{\toPPCX[\listconc{\listconc{Y}{\theta}}{X}][M]{s}}}$.
\label{l:translation:to-ppcx-subs}
\end{lemma}

\input{proofs/translation/to-ppcx-subs}

In the case of a match, its translation is given by
$\toPPCX[V][M]{\match[\theta]{p}{u}} \ensuremath{\triangleq}
\match[\fsize{\theta}]{\toPPCX[V][\listconc{\theta}{M}]{p}}{\toPPCX[V][M]{u}}$.
Note how $\theta$ is pushed into the matchable symbol list of the pattern, in
accordance with the translation of an abstraction. This is crucial for the
following result of preservation of the matching output.

First, note that matchable forms are preserved by the translation as well.

\begin{lemma}
Let $t \in \Term{\ensuremath{\mathsf{PPC}}}$. Then,
\begin{enumerate}
  \item \label{l:appendix:to-ppcx-mf:data} $t \in \TermData{\ensuremath{\mathsf{PPC}}}$ iff
  $\toPPCX[V][M]{t} \in \TermData{\ensuremath{\mathsf{PPC}_\mathtt{dB}}}$.
  \item \label{l:appendix:to-ppcx-mf:match} $t \in \Matchable{\ensuremath{\mathsf{PPC}}}$ iff
  $\toPPCX[V][M]{t} \in \Matchable{\ensuremath{\mathsf{PPC}_\mathtt{dB}}}$.
\end{enumerate}
\label{l:appendix:to-ppcx-mf}
\end{lemma}

\begin{proof}
Both items follow by straightforward induction on $t$, using
(\ref{l:appendix:to-ppcx-mf:data}) to prove (\ref{l:appendix:to-ppcx-mf:match}).
\end{proof}

Then, the result of preservation of the matching output states:

\begin{lemma}
Let $p, u \in \Term{\ensuremath{\mathsf{PPC}}}$.
\begin{enumerate}
  \item\label{l:translation:to-ppcx-match:subs} If $\match[\theta]{p}{u} =
  \sigma$, then $\toPPCX[V][M]{\match[\theta]{p}{u}} =
  \toPPCX[V][M]{\sigma}[\theta]$.

  \item\label{l:translation:to-ppcx-match:fail} If $\match[\theta]{p}{u} =
  \ensuremath{\mathtt{fail}}$, then $\toPPCX[V][M]{\match[\theta]{p}{u}} = \ensuremath{\mathtt{fail}}$.

  \item\label{l:translation:to-ppcx-match:wait} If $\match[\theta]{p}{u} =
  \ensuremath{\mathtt{wait}}$, then $\toPPCX[V][M]{\match[\theta]{p}{u}} = \ensuremath{\mathtt{wait}}$.
\end{enumerate}
\label{l:translation:to-ppcx-match}
\end{lemma}

\input{proofs/translation/to-ppcx-match}

These previous results will allow to prove the simulation of $\ensuremath{\mathsf{PPC}}$ into
$\ensuremath{\mathsf{PPC}_\mathtt{dB}}$ via the translation $\toPPCX{\_}$. We postpone this result to
Sec.~\ref{s:bisimulation} (\emph{cf.}~ Thm.~\ref{t:bisimulation:ppc-ppcx}).

\medskip
Now we focus on the converse side of the embedding, \emph{i.e.}~ the translation of
$\ensuremath{\mathsf{PPC}_\mathtt{dB}}$ terms into $\ensuremath{\mathsf{PPC}}$ terms. As before, this mapping requires two
lists of lists of symbols from which names of the free indices of the term
will be selected: one for variable indices and the other for matchable indices.

\begin{definition}
Given a term $t \in \Term{\ensuremath{\mathsf{PPC}_\mathtt{dB}}}$ and lists of lists of distinct symbols
$V$ and $M$ such that $V_{ij}$ is defined for every $\termidx{i}[j] \in \fv{t}$
and $M_{ij}$ is defined for every $\termidx{i}[j] \in \fm{t}$, the
\emph{translation of $t$ relative to $V$ and $M$}, written $\toPPC[V][M]{t}$,
is inductively defined as follows: \[
\begin{array}{rcl@{\quad}l}
\toPPC[V][M]{\termidxv{i}[j]}    & \ensuremath{\triangleq}  & \termvar{V_{ij}} \\
\toPPC[V][M]{\termidxm{i}[j]}    & \ensuremath{\triangleq}  & \termmatch{M_{ij}} \\
\toPPC[V][M]{\termapp{t}{u}}     & \ensuremath{\triangleq}  & \termapp{\toPPC[V][M]{t}}{\toPPC[V][M]{u}} \\
\toPPC[V][M]{\termabs[n]{p}{t}}  & \ensuremath{\triangleq}  & \termabs[\theta]{\toPPC[V][\listconc{\theta}{M}]{p}}{\toPPC[\listconc{\theta}{V}][M]{t}}  & \text{$\theta = \lista{x_1, \ldots, x_n}$ fresh symbols}
\end{array}
\] Let $x_1, x_2, \ldots$ be the same enumeration of $\ensuremath{{\mathbb{V}}}$ as in
Def.~\ref{d:translation:to-ppcx}. Then, the \emph{translation} of $t$ to
$\ensuremath{\mathsf{PPC}}$, written simply $\toPPC{t}$, is defined as $\toPPC[X][X]{t}$ where
$X = \lista{\lista{x_1}, \ldots, \lista{x_n}}$ such that $\fv{t} \cup \fm{t}
\subseteq \set{\termidxv{1}[1], \ldots, \termidxv{n}[1]}$. Note that
well-formedness of terms guarantees that $X$ satisfies the conditions above.
\label{d:translation:to-ppc}
\end{definition}

To illustrate the translation, consider the term $t_1 =
\termapp{(\termabs[1]{\termapp{\termidxm{2}[1]}{\termidxm{1}[1]}}{\termidxv{1}[1]})}{(\termapp{\termidxm{1}[1]}{\termidxv{2}[1]})}$
where $\fv{t_1} = \set{\termidx{2}[1]}$ and $\fm{t_1} =
\set{\termidx{1}[1]}$. Then,
$\toPPC[\lista{\lista{y},\lista{z}}][\lista{\lista{y},\lista{z}}]{t_1} =
\termapp{(\termabs[\lista{x}]{\toPPC[\lista{\lista{y},\lista{z}}][\lista{\lista{x},\lista{y},\lista{z}}]{\termapp{\termidxm{2}[1]}{\termidxm{1}[1]}}}{\toPPC[\lista{\lista{x},\lista{y},\lista{z}}][\lista{\lista{y},\lista{z}}]{\termidxv{1}[1]}})}{\toPPC[\lista{\lista{y},\lista{z}}][\lista{\lista{y},\lista{z}}]{\termapp{\termidxm{1}[1]}{\termidxv{2}[1]}}}
=
\termapp{(\termabs[\lista{x}]{\termapp{\termmatch{y}}{\termmatch{x}}}{\termvar{x}})}{(\termapp{\termmatch{y}}{\termvar{z}})}$.
Note that $t_1 = \toPPCX{s_1}$ from the example after
Def.~\ref{d:translation:to-ppcx} and, with a proper initialisation of the lists
$V$ and $M$, we get $\toPPC{t_1} = s_1$.

\medskip
Once again, we start with some technical lemmas for substitutions and the
matching operations with respect to the embedding $\toPPC{\_}$. In this case,
the increment functions for variable and matchable indices behave as follows:

\begin{lemma}
Let $t \in \Term{\ensuremath{\mathsf{PPC}_\mathtt{dB}}}$, $k \geq 0$, $i \geq 1$ and $n \geq k+i$ such
that $\fv{t} \cup \fm{t} \subseteq
\set{\termidx{i'}[j] \mid i' \leq n-(i-1), j \leq \fsize{X_{i'}}}$. Then,
\begin{enumerate}
  \item\label{l:translation:to-ppc-upd:var}
  $\toPPC[\listconc{\listconc{X_1}{\ldots}}{X_n}][M]{\fincv[k]{t}[i-1]} \ensuremath{=_{\alpha}}
  \toPPC[\listconc{\listconc{\listconc{X_1}{\ldots}}{X_k}}{\listconc{\listconc{X_{k+i}}{\ldots}}{X_n}}][M]{t}$.

  \item\label{l:translation:to-ppc-upd:match}
  $\toPPC[V][\listconc{\listconc{X_1}{\ldots}}{X_n}]{\fincm[k]{t}[i-1]} \ensuremath{=_{\alpha}}
  \toPPC[V][\listconc{\listconc{\listconc{X_1}{\ldots}}{X_k}}{\listconc{\listconc{X_{k+i}}{\ldots}}{X_n}}]{t}$.
\end{enumerate}
\label{l:translation:to-ppc-upd}
\end{lemma}

\input{proofs/translation/to-ppc-upd}

As for the converse, the translation is only defined for substitution at level
$1$ and requires to be provided a list of symbols $\theta$ such that
$\fsize{\theta} \geq \max\set{j \mid \termidx{1}[j] \in \dom{\sigma}}$. Then,
$\toPPC[V][M]{\sigma}[\theta] \ensuremath{\triangleq}
\subs{\theta_j}{\toPPC[V][M]{\subsapply{\sigma}{\termidxv{1}[j]}}}_{\termidxv{1}[j] \in \dom{\sigma}}$.
The application of a substitution at an arbitrary level $i$ is shown to
translate properly.

\begin{lemma}
Let $s \in \Term{\ensuremath{\mathsf{PPC}_\mathtt{dB}}}$, $\sigma$ be a substitution at level $i$,
$\theta$ be a list of fresh symbols such that $\fsize{\theta} \geq
\max\set{j \mid \termidx{i}[j] \in \dom{\sigma}}$ and $Y$ be a list of $i-1$
lists of symbols. Then,
$\toPPC[\listconc{Y}{X}][M]{\fdecv[i-1]{\subsapply{\subs{\termidx{i}[j]}{\fincv[i-1]{\subsapply{\sigma}{\termidx{i}[j]}}}_{\termidx{i}[j] \in \dom{\sigma}}}{s}}}
\ensuremath{=_{\alpha}}
\subsapply{\subs{\theta_j}{\toPPC[\listconc{Y}{X}][M]{\subsapply{\sigma}{\termidxv{i}[j]}}}_{\termidx{i}[j] \in \dom{\sigma}}}{\toPPC[\listconc{\listconc{Y}{\theta}}{X}][M]{s}}$.
\label{l:translation:to-ppc-subs}
\end{lemma}

\input{proofs/translation/to-ppc-subs}

Similarly to the substitution case, the translation of a match
$\match[n]{p}{u}$ requires to be supplied with a list of $n$ fresh symbols
$\theta$. Then, it is defined as $\toPPC[V][M]{\match[n]{p}{u}}[\theta] \ensuremath{\triangleq}
\match[\theta]{\toPPC[V][\listconc{\theta}{M}]{p}}{\toPPC[V][M]{u}}$. The newly
provided list of symbols is used both as the parameter of the resulting match
and to properly translate the pattern, obtaining the following expected
results.

\begin{lemma}
Let $t \in \Term{\ensuremath{\mathsf{PPC}_\mathtt{dB}}}$. Then,
\begin{enumerate}
  \item \label{l:appendix:to-ppc-mf:data} $t \in \TermData{\ensuremath{\mathsf{PPC}_\mathtt{dB}}}$ iff
  $\toPPC[V][M]{t} \in \TermData{\ensuremath{\mathsf{PPC}}}$.
  \item \label{l:appendix:to-ppc-mf:match} $t \in \Matchable{\ensuremath{\mathsf{PPC}_\mathtt{dB}}}$ iff
  $\toPPC[V][M]{t} \in \Matchable{\ensuremath{\mathsf{PPC}}}$.
\end{enumerate}
\label{l:appendix:to-ppc-mf}
\end{lemma}

\begin{proof}
Both items follow by straightforward induction on $t$, using
(\ref{l:appendix:to-ppc-mf:data}) to prove (\ref{l:appendix:to-ppc-mf:match}).
\end{proof}

\begin{lemma}
Let $p, u \in \Term{\ensuremath{\mathsf{PPC}_\mathtt{dB}}}$.
\begin{enumerate}
  \item\label{l:translation:to-ppc-match:subs} If $\match[n]{p}{u} =
  \sigma$, then $\toPPC[V][M]{\match[n]{p}{u}}[\theta] =
  \toPPC[V][M]{\sigma}[\theta]$.

  \item\label{l:translation:to-ppc-match:fail} If $\match[n]{p}{u} =
  \ensuremath{\mathtt{fail}}$, then $\toPPC[V][M]{\match[n]{p}{u}}[\theta] =
  \ensuremath{\mathtt{fail}}$.

  \item\label{l:translation:to-ppc-match:wait} If $\match[n]{p}{u} =
  \ensuremath{\mathtt{wait}}$, then $\toPPC[V][M]{\match[n]{p}{u}}[\theta] =
  \ensuremath{\mathtt{wait}}$.
\end{enumerate}
\label{l:translation:to-ppc-match}
\end{lemma}

\begin{proof}
By straightforward induction on $p$ using Lem.~\ref{l:appendix:to-ppc-mf}.
Similar to the proof for Lem.~\ref{l:translation:to-ppcx-match}.
\end{proof}

Now we are in conditions to prove the simulation of $\ensuremath{\mathsf{PPC}_\mathtt{dB}}$ into $\ensuremath{\mathsf{PPC}}$
via the translation provided in Def.~\ref{d:translation:to-ppc}.

\medskip
Before proceeding to the next section, one final result concerns the
translations. It turns out that each translation is the inverse of the other,
as shown in Thm.~\ref{t:translation:inverse}. In case of $\ensuremath{\mathsf{PPC}}$ terms
we should work modulo $\alpha$-conversion, while for $\ensuremath{\mathsf{PPC}_\mathtt{dB}}$ terms we may
use equality (modulo secondary indices permutations, \emph{cf.}~ last paragraph in
Sec.~\ref{s:ppcx}). This constitutes the main result of this section and is the
key to extend our individual simulation results (\emph{cf.}~
Thm.~\ref{t:bisimulation:ppc-ppcx} and~\ref{t:bisimulation:ppcx-ppc} resp.)
into a strong bisimulation between the two calculi, as shown in
Sec.~\ref{s:bisimulation}.

\begin{lemma}
Let $t \in \Term{\ensuremath{\mathsf{PPC}_\mathtt{dB}}}$. Then, $\toPPCX[V][M]{\toPPC[V][M]{t}} = t$.
\label{l:translation:inverse-ppcx}
\end{lemma}

\input{proofs/translation/inverse-ppcx}

\begin{lemma}
Let $t \in \Term{\ensuremath{\mathsf{PPC}}}$. Then, $\toPPC[V][M]{\toPPCX[V][M]{t}} \ensuremath{=_{\alpha}} t$.
\label{l:translation:inverse-ppc}
\end{lemma}

\input{proofs/translation/inverse-ppc}

\begin{theorem}[Invertibility]
Let $t \in \Term{\ensuremath{\mathsf{PPC}_\mathtt{dB}}}$ and $s \in \Term{\ensuremath{\mathsf{PPC}}}$. Then,
\begin{inparaenum}
  \item \label{t:translation:inverse:ppcx} $\toPPCX{\toPPC{t}} = t$; and
  \item \label{t:translation:inverse:ppc} $\toPPC{\toPPCX{s}} \ensuremath{=_{\alpha}} s$.
\end{inparaenum}
\label{t:translation:inverse}
\end{theorem}

\begin{proof}
Both items are immediate by Lem.~\ref{l:translation:inverse-ppcx}
and~\ref{l:translation:inverse-ppc} respectively, taking $V = M = X$ as given
in Def.~\ref{d:translation:to-ppcx} and Def.~\ref{d:translation:to-ppc}.
\end{proof}

redpajama_set_name: RedPajamaArXiv


Kid Friendly: Yes. Perfect excursion for the all Family, Kid, Youth or Travelers who enjoy the nature and like to take great photos of the Volcanoes, Lakes, Rivers and the Forest. Also is a great tour for who want to spend good time in cities and markets.
Shore excursion special for who want enjoy the nature and walk around cities.
We'll depart from Puerto Montt pier and travel through to the Vicente Perez Rosales National which is part of the Temperate Rain Forests of the Austral Andes and it was declared a Biosphere Reserve by UNESCO In 2007. Our excursion takes us along the skirt of the volcano, where we will enjoy the native plant and wonderful views around to the Llanquihue lake . We will visit the three main areas of this National Park: The Osorno Volcano (Green lagoon and LLanquihue lake areas), Petrohue Waterfalls and Todos los Santos Lake. After that, we will visit the cozy town of Puerto Varas. Walking around and time for lunch or coffee with "Kuchen" (optional). Later, we will drive to Puerto Montt and visit the most famous Market in Southern Chile, Angelmo. Take photos and enjoy the "Local's life" at the Fish & Fruit Market and get handmade souvenirs from the Art & Craft Market in Angelmo. Back to the pier.
*This tour is priced for 4 travelers, but I can guide large groups. Get a Quote!
- We will drive through the Llanquihue lake. Stop at the viewpoint for pictures of Osorno and Calbuco volcano and lake.
- After that, we will visit the "Petrohue Waterfalls". Photos and walk.
- We will drive up to the Osorno Volcano area visit the Green Lagoon and Lake shore LLanquihue(Optional coffee or lunch Amazing photos from the top. View of 6 volcanoes, lakes and Andes Mountain Range.
-Back to Puerto Varas. We will visit and walk around this city. Time for lunch or coffee (optional). Photos and back to Puerto Montt.
- Walk and photos around Angelmo Market & Craft village.
- Back to the Pier and End of our Services.
Today, also we are finding lots of work on the route, so you will have to consider a couple stops on the route.
Other: -Professional Local Private guide (Bilingual).
-Wilderness First Responder accreditation guide.
25000 CLP - Between 30 to 50 dollars per person. This money will be enough for lunch, coffee with "Kuchen" or buy souvenirs in Puerto Varas or Puerto Montt. Most shops and restaurants accept credit card. Also in Puerto Varas you will find Money Exchange houses and cash machine for dollars.
Other: Optional Coffee & Lunch in Ensenada Village or Puerto Varas . Option available at additional cost. Consider a 1 hour extra time for lunch or coffee.
Souvenirs in Ensenada Village, Puerto Varas and Puerto Montt area.
Banks and Post Office in Puerto Varas and Puerto Montt.
Internet conexion in all restaurants in Puerto Montt, Puerto Varas and Osorno Volcano. Free Zone Internet in Puerto Varas, main square area.
GUEST PROVIDES: Comfortable warm clothes according to the activity (overlanding & hiking), rain jacket, windbreaker jacket, trekking boots or tennis shoes, walking sticks (optional), 1 day backpack, camera, water, cap or hat, sunscreen and sunglasses.


text:
The Prescription for Content Marketing Success? Freelance Writers Who Can Write Medical Copy
Just because your wife majored in English doesn't mean she can write good content for your medical practice. Chances are, neither can you. Instead, you need a writer who can generate medical-related copy that engages potential patients, especially if your practice offers retail services.
Content writers for hire who are well-versed in health and medical writing know how to target consumers who are researching elective treatments that address perceived flaws or imperfections. That's why cosmetic surgeons, dermatologists, ophthalmologists, cosmetic dentists, Medspas, orthodontists and similar practices should seek writers who are knowledgeable about these unique buyers.
Before you hire a writer, make sure he or she understands these very basic principals about writing for medical consumers.
It's All About the Benefits
Medical services fall into two basic categories: those patients must have to save or improve their lives and elective procedures patients don't necessarily need, but want. With the former, patients don't have an option—tumors must be removed, hips replaced and arteries unclogged. But when patients have a choice, the medical treatment becomes less like a service and more like a product. Good writers know how to treat it as such.
Madison Avenue execs and successful salespeople the world over know that marketing efforts focus on the product's benefits, rather than its features. That concept holds true in content marketing efforts for retail medical services. Instead of simply providing an explanation of how a procedure is performed and a list of possible effects, content should use an emotional appeal to drive consumers to action.
How will you look after liposuction or chemical peel or orthodontic treatment?
What types of clothes will you be able to wear following body lift surgery or laser vein treatment or breast augmentation?
Will you be more comfortable following laser eye correction, a tummy tuck or laser hair removal?
Approaching content from these angles will improve your chances of converting casual readers to profit centers.
Physician, Restrain Thyself
There's no question that physicians are experts when it comes to the inner workings of the human body, but sharing your vast knowledge with the masses won't impress anyone. In fact, presenting information that's too advanced or too technical will only intimidate consumers.
That's one reason why medical content often fails to resonate with its target audience. Yes, consumers want specific information about procedures or conditions, but they want it in a way they can easily understand. Wait until the patient is actually in the exam room before regurgitating your amassed knowledge of anatomy and physiology.
Physicians and medical professionals who offer elective, retail services must take pains to provide content for medical consumers instead of traditional patients who seek care for a medical condition. The right content writer can help you reach the audience that influences your practice's bottom line.
Chelsea A is a freelance writer available on WriterAccess, a marketplace where clients and expert writers connect for assignments.
Freelancer Chelsea A

redpajama_set_name: RedPajamaCommonCrawl


text:
Inside Apple Inc.'s iPhone X Compromise
Ashraf Eassa, The Motley Fool
Motley Fool October 16, 2017
According to The Korea Herald, Apple (NASDAQ: AAPL) is working on a brand-new iPhone that has support for a digital pen. The new phone, the publication says, could start shipping to customers as soon as 2019 -- or about two iPhone generations from now.
Unlike Samsung (NASDAQOTH: SSNLF), which the report says implements the S-Pen functionality in its Galaxy Note lineup by way of "electro-magnetic resonance technology that requires additional panels under the screen," Apple is apparently trying to implement what is called a supercapacitor stylus "for price benefits."
Apple's iPhone X tilted back with water splashing around it.
While this news is neat, the most interesting tidbit came near the end of the report. One of the sources said that Apple will need to significantly improve the performance of its mobile processor technology to support a digital pen. The source also added that Apple "had to compromise on some touch performance of the latest iPhone X largely due to the less advanced chipset." This is a curious claim that I think is worth exploring further.
What does the A10X have that the A11 Bionic doesn't?
We know that Apple successfully supports a digital pen -- known as the Apple Pencil -- with the latest iPad Pro tablets. With the latest iPad Pro tablets, according to the company, when a user writes on the screen using the Apple Pencil, the screen begins to scan for input at a rate of 240Hz, or cycles per second. This is twice the peak refresh rate of the display (which is 120Hz).
An Apple iPad Pro tilting back on the left, and another iPad Pro tilting backward on the right.
I suspect that upping the rate at which the system scans for touch input requires a fast processor. Since the Apple A10X successfully powers the iPad Pro can clearly handle pen input at an extremely fast rate, we know that A10X-level performance is good enough to handle high-speed touch input.
What's interesting is that the only area where the A10X is faster than the A11 Bionic is in the graphics processing unit or GPU.
I don't think the GPU would directly impact the touch performance of a device, though. It's not as though the GPU in an iPad Pro suddenly starts running at full blast whenever somebody writes on it with an Apple Pencil -- that'd be ludicrous.
So, here's what I think the source cited is really talking about.
Remember the ProMotion display?
Apple reportedly tested a high-refresh rate display on the iPhone X (Apple calls such displays ProMotion displays) but ultimately chose not to ship the device with such a display. Instead, the iPhone X shipped with a display that could only refresh its contents at 60Hz -- half that of the current iPad Pros.
Although I originally thought that Apple scrapped the technology because it may have been too tough to manufacture, another factor could've been that the GPU in the A11 Bionic couldn't keep up with the processing demands a high-refresh rate display without dropping frames.
Indeed, the extra GPU performance that the A11 Bionic chip delivers (Apple claims a 30% boost over the GPU performance in the A10 Fusion) is already offset by the fact that the iPhone X must render a screen with about 30% more pixels than the prior-generation iPhone 7 Plus. Or perhaps the GPU could handle the extra pixels and having to render twice as many frames in each second, but to do so, the GPU would consume too much power for Apple to achieve its desired battery life goals.
Since a faster refresh rate would dramatically improve the smoothness of the user experience, and since a faster display refresh rate would require that touch input be faster to keep up, I think this is what The Korea Herald's source is referring to.
More From The Motley Fool
5 Expected Social Security Changes in 2018
Why You're Smart to Buy Shopify Inc. (US) -- Despite Citron's Report
6 Years Later, 6 Charts That Show How Far Apple, Inc. Has Come Since Steve Jobs' Passing
Here's My Top Stock to Buy in October
Ashraf Eassa has no position in any of the stocks mentioned. The Motley Fool owns shares of and recommends Apple. The Motley Fool has the following options: long January 2020 $150 calls on Apple and short January 2020 $155 calls on Apple. The Motley Fool has a disclosure policy.


I couldn't help myself. Normally, I wouldn't care. But I blame two, maybe three, little old ladies in a Louisville coffee shop.
There are certain words and phrases that my brain listens for, even if I'm not actively listening.
Somehow, and I couldn't tell you how, Britney Spears made it into the mental queue. Maybe it had something to do with the Dr. Phil visit to her psych ward room, which thrust her name into the headlines and news broadcasts for what seemed like the dozenth time in three days.