Milner's Lambda-Calculus with Partial Substitutions

Delia Kesner     Shane Ó Conchúir

PPS, CNRS and Université Paris 7     Trinity College Dublin

France      Ireland

We study  Milner's lambda-calculus with  partial substitutions.
Particularly,  we  show  confluence  on  terms  and  metaterms,
preservation     of     $\beta$-strong    normalisation     and
characterisation   of  strongly   normalisable  terms   via  an
intersection typing  discipline. The results  on terms transfer
to  Milner's  bigraphical  model  of the  calculus.  We  relate
Milner's  calculus  to calculi  with  definitions,
to calculi with  explicit
substitutions, and to MELL Proof-Nets.

§ INTRODUCTION

The  $\lm$-calculus  was  introduced  by  Milner as  a  means  to
modelling   the   $\l$-calculus  in   bigraphs [28]. However, the  $\lm$-calculus is  interesting apart  from the
model; it enjoys confluence  on terms, step-by-step simulation of
$\beta$-reduction [32],   and  preservation  of
$\beta$-strong    normalisation     (PSN)    i.e.    every
$\l$-calculus term which  is $\beta$-strongly normalising is also
$\lm$-strongly normalising  [31].

In this paper we study many remaining open questions about the
The first  of them concerns confluence  on metaterms which
are terms containing  metavariables usually used to denote
incomplete  programs  and/or   proofs  in  higher-order
frameworks [17].   To obtain  a  confluent
reduction  relation  on metaterms  we  need  to extend  the
existing notion of reduction  on terms. We develop a proof
of confluence  for this extended  new relation by using Tait
and  Martin-Löf's  technique.  This  proof  includes  a  formal
argument  to show  that the  calculus of  substitution  itself is

Our main  contribution lies  in studying the  connections between
the $\lm$-calculus and other formalisms.  We start by considering calculi with
definitions,       namely,      the       partial
$\l$-calculus [12, 30], which we call $\lpar$, and
the  $\l$-calculus  with  definitions [35],
which we call $\ldef$.  We distinguish arbitrary terms of
the   calculi   with    definitions,   which   we   call
$\mterms$-terms,  from  (pure) terms   without  definition,  which  are
ordinary   $\l$-terms.     We   show   that    the   sets   of
strongly-normalising  $\l$-terms  in $\lm$  and  $\lpar$ are  the
same.  Similarly,  we show that the  sets of strongly-normalising
$\mterms$-terms in $\lm$ and $\ldef$ are equal.  Thus, we demonstrate
that partial substitutions and definitions are similar notions.

We also relate  $\lm$-strongly normalising terms
to  typed $\mterms$-terms.
For that, we start by introducing an
intersection type discipline for  $\mterms$-terms.
We  then give a simple
(and    constructive)   argument   to    prove   $\lpar$-strong
normalisation for   typed  $\l$-terms.  This  argument turns
out to be sufficient  to conclude $\lm$-strong normalisation for
intersection typed $\mterms$-terms.
By proving
the converse i.e. $\lm$-strongly normalising $\mterms$-terms can be  typed
in the intersection type discipline, we also provide a characterisation
of $\lm$-strongly normalising $\mterms$-terms.

The relation between typable and $\lm$-strongly normalising
$\mterms$-terms also gives an alternative proof of PSN for the
$\lm$-calculus, which is self-contained, and which simplifies previous
work [31] considerably.
Indeed, the existing proof is quite
involved, and uses  a translation of $\lm$ into a rather complex calculus,
obtained by modifying a language with explicit resources
inspired from Linear Logic's Proof-Nets.

Another contribution of the paper
is the  study of the relation  between
partial   substitutions   and   explicit   substitutions.    More
precisely, we define a translation  from $\lm$ to a calculus with
explicit    substitutions    called   $\les$ [20].     This
translation preserves  reduction and  has at least  two important
consequences.  On one hand, we  obtain a simple proof of
for  simply typed  $\mterms$-terms.   A second
consequence is  that the existing simulation of  the simply typed
$\les$-calculus  into MELL  Proof-Nets [20] also gives a
natural interpretation for the simply typed $\lm$-calculus by composition.  As a
corollary, $\lm$-strong normalisation  for simply typed $\mterms$-terms can
also be inferred from strong normalisation of MELL Proof-Nets.

Finally, we transfer our confluence and strong normalisation proofs on $\mterms$-terms without metavariables
in $\lm$ to Milner's model using an existing result.

Road map.
<Ref>  introduces the $\lm$-calculus.
Metaterms are introduced in <ref>:
some preliminary properties are discussed in <ref>
and confluence on metaterms is proved
using     Tait      and     Martin-Löf's     technique
in <ref>.      In <ref>   we  relate  $\lm$   to
calculi     with     definitions,    $\lpar$     and     $\ldef$.
In <ref>,  we present  the translation  from  $\lm$ to
$\les$ and  prove that  reduction in the  former is  simulated by
non-empty  reduction  sequences   in  the  latter.  <ref>  presents a  neat characterisation
of  $\lm$-strongly  normalising  terms  using  intersection  type
systems   as  well   as   the  PSN   property   for  untyped
$\mterms$-terms of $\lm$.     We  conclude
$\lm$-strong  normalisation  for  simply typed  $\mterms$-terms  from
strong $\les$-normalisation  for simply typed  $\mterms$-terms.
but  not  least,  we  discuss a relation between  $\lm$  and  MELL
Proof-Nets  and transfer results to
the bigraphical setting
in <ref>.

§ THE $\LM$-CALCULUS

The $\lm$-calculus  was introduced by Milner to present a model of
the $\lambda$-calculus  in local bigraphs.   The    calculus   was
inspired by $\lambdasigma$ [1]
although  it is a  named calculus  and has  turned out  to have
stronger properties as we show in this paper.  Terms
of the $\lm$-calculus, called $\mterms$-terms, are  given by the following grammar:

\[ t ::= x \mid t\ t \mid \l x. t \mid t[x/t] \]

The set of terms includes variables, abstractions,
applications and closures respectively.  The piece of
syntax $[x/t]$, which is not a term itself, is called an
explicit substitution. A term $t$ is said to be pure if $t$
does not contain any explicit substitution.

Free and bound variables are defined as usual, by assuming
the terms $\l x. t$ and $t[x/u]$ bind $x$ in $t$. Formally,

\[ \begin{array}{llllll}
\fv(x) & = & \set{x}  & \bv(x) & = & \ems \\
\fv(t\ u) & = & \fv(t) \cup \fv(u) & \bv(t\ u) & = & \bv(t)
\cup \bv(u)\\
\fv(\l x. t) & = & \fv(t) \setminus \set{x} & \bv(\l x. t) & = &
\bv(t) \cup \set{x} \\
\fv(t[x/u]) & = & \fv(t) \setminus \set{x} \cup \fv(u) & \bv(t[x/u])
& = & \bv(t) \cup \set{x} \cup \bv (u) \\
\end{array} \]

We consider $\alpha$-conversion which is the congruence generated by
renaming of bound variables. Thus for example $(\l y. x)[x/y]
=_{\alpha} (\l z. x')[x'/y]$. We work with $\alpha$-equivalence
classes so that two bound variables of the same term are assumed to be
distinct, and no free and bound variable of the same term have the
same name. Thus, $\alpha$-conversion avoids capture of variables.
We use notation $\l \vec{y}.s$ for $\l y_1. \ldots. \l
y_n. s$, where $s$ is not a lambda abstraction.  Implicit
substitution on $\mterms$-terms can be defined modulo $\alpha$-conversion
in such a way that capture of variables is avoided:

\[ \begin{array}{llllll}
x\isubs{x}{v} & :=  & v \\
y\isubs{x}{v} & :=  & y & \mbox{ if } y \neq x \\
(\l y. t)\isubs{x}{v}  & := & \l y. t\isubs{x}{v} \\
(tu)\isubs{x}{v} & := & t\isubs{x}{v}u\isubs{x}{v} \\
t[y/u]\isubs{x}{v}& := &  t\isubs{x}{v}[y/u\isubs{x}{v}]\\
\end{array} \]

The set  of $\mterms$-contexts  can be  defined by the following grammar:

\[ C ::= \Box \mid C\ t \mid t\ C \mid \l x. C \mid C[x/t]
\mid t[x/C] \]

We use the notation $C\cwc{u}_\phi$
to mean that the hole $\Box$ in the context $C$ has been replaced
by the term $u$ without capture of the variables in the set
$\phi$. Thus for example, if $C = \l z. \Box$, then
with $x \in \phi$
means in particular that $z \neq x$.

The reduction rules  of  the $\lm$-calculus are given
in <ref>.

\[ \begin{array}{|lcll|}
\hline
%\mbox{{\bf Equations}}: &&&\\
%t[x/u][y/v]  & =_{\Com} &   t[y/v][x/u] &  \mbox{ if } y \notin \fv(u)\ \&\
%x \notin \fv(v)\\ % \&\ x \neq y \\
%\mbox{{\bf Reduction Rules}}: &&&\\
(\l x. t)\ u    &\Rew{\B}   & t[x/u] & \\
t[x/u]          &\Rew{\Gc}  & t      & \mbox{ if } x \notin \fv(t) \\
C\cwc{x}_\phi[x/u]   &\Rew{\us}   & C\cwc{u}_\phi[x/u] & \mbox{ if } \{x\} \cup \fv(u) \subseteq \phi\\
%C\cwc{\mX_\Del}_{x \cup \fv(u)} [x/u]   &\Rew{\usm}   & C\cwc{\mX_\Del[x/u]}_{x \cup \fv(u)}[x/u] & \mbox{ if } x \in \Del, C \neq \Box[y_1/v_1]\ldots[y_n/v_n], n \geq 0\\
\hline
\end{array} \]

Reduction Rules for $\mterms$-Terms

As Milner  describes, an explicit substitution
$[x/u]$ acts  `at  a distance' on each free occurrence
of $x$ in turn, rather than migrating a copy of itself towards
each such occurrence   the reduction step
$(\l x.  x\ (y\ y))[y/t] \Rew{\us}  (\l x. x\  (t\ y))[y/t]$
implements  a partial  substitution.
Partial substitution is atypical and therefore presents novel
challenges: traditional methods of proving simulation or normalisation
properties need to be adapted to this setting.  However, it also
exhibits interesting properties: the
$\lm$-calculus retains PSN whilst having full
composition of substitutions.  This is remarkable since Melliès'
counterexample of PSN [26] for $\lambdasigma$ was based
on full composition of substitutions.

Bloo and  Rose's subsequent  work [8]
led to the intuition that

“the   essential  property   for  losing   PSN   is  the
possibility of moving one  substitution from outside a second
substitution to the inside of the latter by means of a
composition of substitutions.” <cit.>

The composition  described in <cit.> is  given by a local reduction rule, by pushing  one  substitution
inside  the one appearing on its left-hand side  (see for example rules
$\Compi$ and $\Compii$ in <ref>). Composition  of  substitutions
in the  $\lm$-calculus is different in the sense that it is implicit via
the non-local substitution rule.

We denote by $\sm$ (resp. $\B\sm$)
the  reduction relation generated by
the reduction  rules $\us$ and $\Gc$ in <ref>
(resp. $\B$, $\us$ and $\Gc$)
and closed by all contexts.
The reduction relations  of the $\lm$-calculus for $\mterms$-terms,
defined on $\mterms$-terms,  are generated by the previous
reduction relations  $\sm$ (resp. $\B\sm$)  modulo the
equivalence relation
$\alpha$, they are denoted by  $\Rew{\m}$ (resp. $\Rew{\lm}$):

\[  \begin{array}{llll}
t \Rew{\m} t' & \mbox{ iff there are } s,s' \mbox{ s.t.}  & t
=_{\alpha} s \Rew{\sm}  s'=_{\alpha} t' \\
t \Rew{\lm} t' & \mbox{ iff there are } s,s' \mbox{ s.t.}  & t
=_{\alpha} s \Rew{\B\sm}  s'=_{\alpha} t'  \\
\end{array} \]

Thus, the reduction relation
acts on  $\alpha$-equivalence classes.
For any reduction relation $\R$, we use the notation $\Rewn{\R}$
(resp.  $\Rewplus{\R}$) to denote the reflexive (resp. reflexive
transitive) closure of $\Rew{\R}$. As a consequence if $t
\Rewn{\m} t'$ (resp, $t
\Rewn{\lm} t'$) in $0$ steps, then $t=_{\alpha} t'$ (and not $t = t'$).

Reduction enjoys   the  following   properties.

Let $t,t'$ be $\mterms$-terms. If $t \Rew{\lm} t'$, then  $\fv(t') \subseteq \fv(t)$.

By induction on $t \Rew{\lm} t'$.

Let $t,u$ be $\mterms$-terms. Then $t[x/u] \Rewplus{\lm} t \isubs{x}{u}$.

By induction on $t$.

Full composition   guarantees
that explicit substitution  implements the implicit one.  While
this  property seems reasonable/natural,  it is  worth noticing
that many calculi with  explicit substitutions do not enjoy it.

Let $t,u$ be $\l$-terms.
If $t \Rew{\beta} u$, then $t \Rewplus{\lm} u$.

By induction on $t \Rew{\beta} u$.

§ METATERMS

We now introduce
metaterms,  usually used to denote  incomplete programs/proofs
in   higher-order  frameworks [17].  Metavariables
come  with a minimal amount of  information to guarantee
that some  basic operations such  as instantiation (replacement
of metavariables  by metaterms) are sound in  a typing context.
An example can  be given by the (non  annotated) metaterm $t=\l
y. y\ \mX\  (\l z. \mX)$, for which  the instantiation of $\mX$
by a term containing a  free occurrence of $z$ would be unsound
(see [29, 14, 33] for details).
The  set   of  $\mterms$-metaterms  is  obtained   by  adding
annotated metavariables of  the form $\mX_\Del$ (where
$\Del$ is  a set of  variables) to the grammar
generating the
$\mterms$-terms introduced in <ref>.
The  notion of free
variable  is extended  to $\mterms$-metaterms by $\fv(\mX_\Del)= \Del$. As a
consequence, $\alpha$-conversion can also be defined on
$\mterms$-metaterms and thus for example $\l x. \mX_{x,y} =_{\alpha} \l z. \mX_{z,y}$.
We also extend the  standard notion of implicit substitution to $\mterms$-metaterms as follows:

\begin{array}{llll}
\mX_\Del \isubs{x}{v} & := & \mX_\Del & \mbox{if } x \notin \Del\\
\mX_\Del \isubs{x}{v} & := & \mX_\Del[x/v] & \mbox{if } x \in \Del\\
\end{array}

It is worth noticing that Milner's original presentation did
not consider metaterms, as  the bigraphical system did not model
them. However, all properties we prove here involving metaterms
hold also for terms.

Throughout  this section,  we include a new rule
in the reduction   relation  as   well   as  a new equation in the equivalence relation. Indeed, we add  the equation  $\Com$
and the reduction rule $\usm$, presented in <ref>,
to the ones in <ref>.

\[ \begin{array}{|llll|}
\hline
\mbox{{\bf Equation}}: &&&\\
t[x/u][y/v]  & =_{\Com} &   t[y/v][x/u] &  \mbox{ if } y \notin \fv(u)\ \&\
x \notin \fv(v)\\ &&&\\ % \&\ x \neq y \\
\mbox{{\bf Reduction Rule}}: &&&\\
C\cwc{\mX_\Del}_{\phi} [x/u]  & \Rew{\usm} &
C\cwc{\mX_\Del[x/u]}_{\phi}[x/u]\  & \mbox{ if }   x \in
\Del\ \&\  x \cup \fv(u) \subseteq \phi \\
&&& \;\;\;\;  \&\ C \neq \Box[y_1/v_1]\ldots[y_n/v_n]\ (n \geq 0) \\
\hline
\end{array} \]

Extra Equation and Reduction Rule for $\mterms$-Metaterms

Remark in particular that $\usm$ cannot be applied if the
context is  empty. Remark also that the equation $\Com$ can
always  be postponed w.r.t. reduction if only
terms (and not metaterms) are considered.

The equation $\C$ is not part of the original presentation
of Milner's  $\lambda$-calculus but we  include it here  for at
least two reasons. The first one is that in bigraphs as well as
in  proof-nets, which are  graphical representation  of $\mterms$-terms,
some  syntactic  details —such  as  for  example  the order  of
appearence  of independent substitutions—  is
extensionally  irrelevant.  The   second  reason  is  that  the
reduction   relation    on   $\mterms$-metaterms   we    study   in <ref>  turns out to  be confluent  only
with the  equation $\C$.

The equivalence  relation  generated  by  the conversions  $\alpha$  and
$\Com$ is denoted by $\EqEs$. We now   denote by $\sm$ (resp. $\B\sm$)
the  reduction relation generated by
the reduction  rules $\{\us, \Gc, \usm\}$ (resp. $\{\B, \us, \Gc, \usm \}$)
and closed by all contexts.
The reduction relations  of the $\lm$-calculus for $\mterms$-metaterms are generated by the
reduction relations  $\sm$ (resp. $\B\sm$)  modulo the
equivalence relation
$\Es$, always  denoted by  $\Rew{\m}$ (resp. $\Rew{\lm}$):

\[  \begin{array}{llll}
t \Rew{\m} t' & \mbox{ iff there are } s,s' \mbox{ s.t.}  & t
\EqEs s \Rew{\sm}  s' \EqEs t' \\
t \Rew{\lm} t' & \mbox{ iff there are } s,s' \mbox{ s.t.}  & t
\EqEs s \Rew{\B\sm}  s'\EqEs t'  \\
\end{array} \]

§.§ Preliminary Properties

In this section we prove some preliminary properties of $\mterms$-metaterms. First, full composition still holds for $\mterms$-metaterms:

Let $t, u$ be $\mterms$-metaterms. Then
$t[x/u] \Rewn{\m} t\isubs{x}{u}$.

By induction on the number $n_{x,t}$ of free occurrences of
$x$ in $t$.

* If $n_{x,t}=0$, then $t[x/u] \Rew{\Gc} t = t\isubs{x}{u}$.

* If $n_{x,t}>0$, then we have different cases.

* Suppose  $t$ can be written as $C\cwc{x}$, for some
context $C$. Then
$t[x/u] \Rew{\us} C\cwc{u}[x/u]$ and
$n_{x,C\cwc{u}} < n_{x,t}$. By the         $C\cwc{u}[x/u] \Rewn{\m} C\cwc{u}\isubs{x}{u}$.
Since $t\isubs{x}{u} = C\cwc{u}\isubs{x}{u}$,
then   $t[x/u] \Rewn{\m} t\isubs{x}{u}$.

* Otherwise, suppose  $t$ can  be written as
$t=C\cwc{\mX_{\Del}}\ (x \in \Del)$, for some context
$C \neq \Box[y_1/v_1]\ldots[y_n/v_n]\ (n \geq 0)$.
Then $t[x/u] \Rew{\usm} C\cwc{\mX_{\Del}[x/u]}[x/u]$ and
$n_{x,C\cwc{\mX_{\Del}[x/u]}} < n_{x,t}$. By the         $C\cwc{\mX_{\Del}[x/u]}[x/u] \Rewn{\m} C\cwc{\mX_{\Del}[x/u]}\isubs{x}{u}$.
Since $t\isubs{x}{u} = C\cwc{\mX_{\Del}[x/u]}\isubs{x}{u}$,
then   $t[x/u] \Rewn{\m} t\isubs{x}{u}$.

* Otherwise,  $t$ can only be written as
$\mX_{\Del}[y_1/u_1]..[y_n/u_n]\ (x \in \Del)$
for some $n \geq 0$.
Remark that $x \notin \fv(u_i)$ for all $1 \leq i \leq n$,
otherwise we would be in the previous case.
Then $t[x/u]= \mX_{\Del}[y_1/u_1]..[y_n/u_n][x/u] =_{\C}
\mX_{\Del}[x/u][y_1/u_1]..[y_n/u_n]
= \mX_{\Del}\isubs{x}{u}[y_1/u_1\isubs{x}{u}]..[y_n/u_n\isubs{x}{u}]
= \mX_{\Del}[y_1/u_1]..[y_n/u_n]\isubs{x}{u}$.

So here there is a  subtle problem since $t \Rewn{\m} t'$
means $t = t'$ and not $t =_{\C} t'$ when the number of steps
$t$ to $t'$ is $0$. I've just realised that I
have the same problem in  my $\les$-paper. The solution is just
to talk about the reflexive closure on equivalence classes. Do
you agree?

Yes,  I agree. We rewrite modulo the equation in the
transitive case so I think we should also do the same in the reflexive case (it's funny how it's always the outlying cases). Besides solving the problem, this seems the correct notion to me. I've added the definition in the syntax section but there is probably a nicer way to do it.

If there's space, explain $\m$...
system $\sm = \{ \us, \usm, \Gc\}$ modulo
$\Es$ can be used as a function on $\Es$-equivalence classes.

We now  remark that the system $\sm = \{ \us, \usm, \Gc\}$ modulo
$\Es$ can be used as a function on $\Es$-equivalence classes.

The $\m$-normal forms of $\mterms$-metaterms exist and are unique modulo $\Es$.

The reduction relation  $\Rew{\m}$ can be shown to be  terminating
by associating to each $\mterms$-metaterm
a measure
which does not change by $\Es$ but strictly decreases by
$\Rew{\sm}$ (<ref> in  <ref>).   Thus, $\m$-normal forms  of $\mterms$-metaterms exist.
Moreover,   $\Rew{\m}$  is
locally confluent and locally coherent
in <ref>).  Therefore, by [18],
$\Rew{\m}$  is  confluent  on $\mterms$-metaterms  and  hence $\m$-normal forms
of $\mterms$-metaterms are unique
modulo $\Es$-equivalence.

Moreover, the following properties are  straightforward:

Let $u$ and $v$ be metaterms. Then,

* $\m(u\ v) = \m(u)\ \m(v)$.

* $\m(\l x.u) = \l x.\m(u)$.

Let  $t=f(t_1,\ldots,t_n)$, where $f$  is a  $\l$-abstraction, an
application     or      a     substitution     operator.     Then
$\m(f(t_1,\ldots,t_n)[x/u]) = \m(f(t_1[x/u],\ldots,t_n[x/u]))$.

First of all remark that $t=f(t_1,\ldots,t_n)$
means either $t=\l x. t_1$ or $t = t_1\ t_2$ or $t= t_1[y/t_2]$.
We reason by induction on the number  $n_{x,t}$ of free occurrences of
$x$ in $t$.

* If $n=0$, then $\m(t[x/u]) =_{\Gc} \m(t) =_{\Gc}
\m(f(t_1[x/u],\ldots,t_n[x/u]))$.

* If $n_{x,t}>0$, then we have two cases.

* There is a reduction
$t[x/u] \Rew{\lm} t'[x/u]$ such that
$n_{x,t'} < n_{x,t}$ so that
$t_i = C\cwc{x}$ or $t_i = C\cwc{\mX_{\Del}}$ with $x
\in \Del$ and $C \neq \Box[y_1/v_1]\ldots[y_n/v_n], n
\geq 0 $
for some $i \in [1..n]$. As a consequence
$t' = f(t_1,\ldots,t'_i,\ldots,t_n)$ with
$t'_i = C\cwc{u}$ or $t'_i = C\cwc{\mX_{\Del}[x/u]}$. Thus

\[ \begin{array}{ll}
\m(f(t_1,\ldots,t_i,\ldots,t_n)[x/u]) & = \\
\m(f(t_1,\ldots,t'_i,\ldots,t_n)[x/u]) & =_{\ih} \\
\m(f(t_1[x/u],\ldots,t'_i[x/u],\ldots,t_n[x/u])) & =_{\ih} \\
\m(f(t_1[x/u],\ldots,t_i[x/u],\ldots,t_n[x/u])) & =_{\ih} \\
\end{array}\]

* There is no such reduction so that is of the form
$t = t_1[y/t_2]$ with $x \in
\fv(t_1)$ and $x \notin
\fv(t_2)$. We thus have

\[ \begin{array}{ll}
\m(f(t_1,t_2)[x/u]) & = \\
\m( t_1[y/t_2][x/u]) &   =_{\C} \\
\m(t_1[x/u][y/t_2]) & =_{\Gc} \\
\m(t_1[x/u][y/t_2[x/u]]) & = \\
\m(f(t_1[x/u], t_2[x/u]))\\
\end{array} \]

Let $t$ be a $\mterms$-metaterm in  $\m$-normal form.
Then it has one of the following forms:

* $t =x$, $t= t_1\ t_2$, or $t = \l y. t_1$ where $t_1$ and $t_2$ are in $\m$-normal form.

* $t = \mX_\Del [x_1/u_1]\ldots[x_n/u_n]$, where $n
\geq 0$ and every $u_i$ is in $\m$-normal form and $x_i \in
\Del$ and $x_i \notin \fv(u_j)$ for all $i, j \in [1,n]$ s.t. $i < j$.

Remark that metaterms   in  $\m$-normal  form   have  all  explicit
substitutions  directly  above  metavariables. Thus in particular   terms
without metavariables in $\m$-normal form have no explicit substitutions at all.
From now on, we write $\m(t)$ to denote the (unique)
$\m$-normal form of the $\mterms$-metaterm $t$.

§.§ Confluence

While confluence on terms    always holds for calculi  with   explicit
substitutions, confluence on metaterms is often based
some possible form of  interaction between   substitutions,   such  as  in
$\lambda\sigma$ [1]   or  $\lambda_{ws}$ [13].
To illustrate this requirement, let  us consider the typical diverging
example adapted to $\lm$-reduction:

\[  t\isubs{y}{v}[x/u\isubs{y}{v}]  \LRewn{\lm} ((\l x. t)\ u)[y/v] \Rew{\B} t[x/u][y/v] \]

This diagram can be closed using  full composition with the sequence
$t[x/u][y/v] \linebreak \Rewplus{\lm} t[x/u]\isubs{y}{v} =

However,  while  de  Bruijn   notation  for  $\l$-terms  allows  a
canonical  representation  of bound  variables   given by  a
certain  order  on  their  natural numbers,  calculi  with  named
variables  suffer  from the  following  (also typical)  diverging

\[  \mX_{x,y}[y/v][x/z]  \LRewn{\lm} ((\l x. \mX_{x,y})\ z)[y/v] \Rew{\B} \mX_{x,y}[x/z][y/v] \]

The $\mterms$-metaterms $\mX_{x,y}[y/v][x/z]$ and $\mX_{x,y}[x/z][y/v]$ are
equal modulo permutation of independent substitutions,
thus justifying the introduction of the equation $\C$ in the definition
of the calculus for metaterms.

One possible technical tool to show confluence for $\mterms$-metaterms
is the use of another confluent calculus well-related to the
$\lm$-calculus. We prefer to give a self-contained argument, and so
adapt a proof based on Tait and Martin-Löf's technique: define a
simultaneous reduction relation denoted $\paralp{\lm}$; prove that $\lm$
can be projected to $\paralp{\lm}$ on $\m$-normal forms; show that
$\paralnp{\lm}$ has the diamond property; and finally conclude.

The relation $\paralp{}$ on $\mterms$-metaterms in $\m$-normal form is
given by:

* $x \paralp{} x$

* If $t  \paralp{} t'$, then $\l x. t  \paralp{} \l x. t'$

* If $t  \paralp{} t'$ and
$u \paralp{} u'$, then $t\ u  \paralp{} t'\ u'$

* If $t  \paralp{} t'$ and
$u \paralp{} u'$, then $(\l x. t)\ u  \paralp{} \m(t'[x/u'])$

* If $u_i \paralp{} u'_i$ and $x_j \notin \fv(u_i)$ for all $i, j \in [1,n]$, then $\mX_\Del [x_1/u_1]\ldots[x_n/u_n] \paralp{} \mX_\Del [x_1/u'_1]\ldots[x_n/u'_n]$

The relation $\paralp{\lm}$ is defined by $t  \paralp{\lm} t' \mbox{ iff } \exists s,s' \mbox{ s.t. }
t=_{\Es} s \paralp{} s' =_{\Es} t'$.
We use  $\paralnp{\lm}$
denote the reflexive closure of $\paralp{\lm}$ and thus
$t \paralnp{\lm} t'$  in $0$ steps means  $t=_{\Es} t'$.
The following properties are straightforward.

The reduction relation $ \paralp{\lm}$
enjoys the following properties:

(Reflexivity) $t \paralp{\lm} t$ for every $\mterms$-metaterm $t$ in $\m$-normal form.
Induct on  the structure of $t$, using the second two cases in the definition of $\paralp{}$ for the induction cases.

(Closure by contexts) if
$t \paralp{\lm} t'$, then
$u=C\cwc{t} \paralp{\lm} C\cwc{t'}=u'$
whenever $u$ and $u'$ are $\m$-normal forms.
Use your proof for $\les$ replacing $\es$ with $\s$.
I induct on  $n$, proving the base case $n=1$. The induction case is easier then since we are guaranteed to have an application or substitution where some $t_i$s are in one branch and the rest are in the other. We apply the induction hypothesis on both sides and then the third or fifth rule defining $\paralp{}$ to join the application/substitution. We then “build” the rest of the term $u'$ using the other cases in the definition of $\paralp{}$.

The reflexive and transitive closures
of $\paralp{\lm}$ and $\Rew{\lm}$ are the same relation.

To show $\paralnp{\lm} \subseteq\  \Rewn{\lm}$
we first show that $t \paralp{} t'$ implies $t \Rewn{\lm}
t'$ by induction on the definition of $\paralp{}$.

* $t = x \paralp{} x = t'$. Then $t \Rewn{\lm} t'$.

* $t = \lambda x. u \paralp{} \l x. u' = t'$ where $u
\paralp{} u'$. By the   $u \Rewn{\lm} u'$. Therefore, $\l x. u \Rewn{\lm} \l x. u'$.

* $t = u\ v \paralp{} u'\ v' = t'$ where $u \paralp{} u'$ and
$v \paralp{} v'$. By the   $u \Rewn{\lm} u'$ and $v \Rewn{\lm} v'$. Therefore, $u\ v \Rewn{\lm} u'\ v'$.

* $t  = (\l  x. u)  v \paralp{} \m(u'[x/v'])  = t'$  where $u
\paralp{} u'$ and $v \paralp{}  v'$. By   $u \Rewn{\lm} u'$
and $v \Rewn{\lm} v'$. Therefore,
$$(\l x. u) v \Rewn{\lm} (\l
x.  u')   v'  \Rew{\lm}  u'[x/v']   \Rewn{\lm}  \m(u'[x/v']).$$

* $t = \mX_\Del  [x_1/u_1]\ldots[x_n/u_n] \paralp{}
\mX_\Del   [x_1/u'_1]\ldots[x_n/u'_n]   =   t'$  where   $u_i
\paralp{} u'_i$ and  $x_i \notin \fv(u_j)$ for all  $i, j \in
[1,n]$.  By the    $u_i  \Rewn{\lm} u'_i$  for all  $i \in
[1,n]$ therefore $t \Rewn{\lm} t'$.

Now, suppose $t \paralp{\lm}^n t'$. We reason by
induction on  the number of
steps $n$.
For $n=0$, $t =_{\Es} t'$ so that $t \Rewn{\lm} t'$ and we are done.
Assume $n = k+1$ and $t \paralp{\lm} s \paralp{}^k t'$.
Then $t =_{\Es} t_1 \paralp{} s_1 =_{\Es} s \paralp{}^k t'$.
We have $t =_{\Es} t_1 \Rewn{\lm} s_1 =_{\Es} s  \Rewn{\lm} t'$
by the previous point and the
so we conclude $t \Rewn{\lm}

To show $\Rewn{\lm} \subseteq\ \paralnp{\lm}$
we first show that $t \Rew{\lm} t'$ implies $t \paralp{\lm} t'$ by
induction on $\Rew{\lm}$ using <ref>.
Now, suppose $t \Rewn{\lm} t'$ in $n$ steps. We conclude by
a simple  induction on  $n$.

A consequence of <ref> and the previous  lemma is that
$t \paralp{\lm} t'$ implies $\fv(t') \subseteq \fv(t)$.

Let $t,t',u,u'$ be $\mterms$-metaterms.
If $t \paralp{\lm} t'$ and $u \paralp{\lm} u'$,
then $\m(t[x/u]) \paralp{\lm} \m(t'[x/u'])$.

We have $t=_{\Es} s_1 \paralp{} s_2 =_{\Es}
t'$ so that it is sufficient to show that $s_1 \paralp{} s_2$
and $u \paralp{\lm} u'$
imply $\m(s_1[x/u]) \paralp{\lm} \m(s_2[x/u'])$ since then
$\m(t[x/u]) =_{\Es} \m(s_1[x/u])
\paralp{\lm} \m(s_2[x/u']) =_{\Es} \m(t'[x/u'])$.
We reason by induction on $s_1 \paralp{} s_2$.

* If $x \paralp{} x$, then
$\m(x[x/u]) = \m(u) = u \paralp{\lm} u' =
\m(u') = \m(x[x/u'])$.

* If $y \paralp{} y$, then
$\m(y[x/u]) = y  \paralp{\lm}
y = \m(y[x/u'])$ holds by definition.

* If $t_1\ t_2 \paralp{} t'_1\ t'_2$, where
$t_1 \paralp{} t'_1$ and $t_2 \paralp{} t'_2$,  then

\[ \begin{array}{ll}
\m((t_1\ t_2)[x/u]) & = (\mbox{\cref{l:es-application-lambda-composition}})\\
\m(t_1[x/u])\ \m(t_2[x/u]) &  \paralp{\lm} (\ih)\\
\m(t'_1[x/u'])\ \m(t'_2[x/u']) & = (\mbox{\cref{l:es-application-lambda-composition}})\\
\m((t'_1\ t'_2)[x/u'])
\end{array} \]

* If $\l y. v \paralp{} \l y. v'$, where
$v \paralp{} v'$, then

\[ \begin{array}{ll}
\m((\l y. v)[x/u]) & = (\mbox{\cref{l:es-application-lambda-composition},~\cref{l:s-distributes}}) \\
\l y. \m(v[x/u])   & \paralp{\lm} (\ih) \\
\l y. \m(v'[x/u']) & =(\mbox{\cref{l:es-application-lambda-composition},~\cref{l:s-distributes}}) \\
\m((\l y. v')[x/u'])
\end{array} \]

* If $(\l y. t_1)\ v \paralp{} \m(t'_1[y/v'])$, where
$t_1 \paralp{} t'_1$ and $v \paralp{} v'$, then

\[ \begin{array}{ll}
\m(((\l y. t_1)\ v)[x/u]) & = (\mbox{\cref{l:es-application-lambda-composition}}) \\
\m((\l y. t_1)[x/u])\ \m(v[x/u]) & = (\mbox{\cref{l:es-application-lambda-composition},~\cref{l:s-distributes}})\\
(\l y. \m(t_1[x/u]))\ \m(v[x/u]) & \paralp{\lm}
(\ih) \\
\m(\m(t'_1[x/u'])[y/\m(v'[x/u'])]) & = \\
\m( t'_1[x/u'][y/v'[x/u']]) & = (\mbox{\cref{l:es-application-lambda-composition}}) \\
\m( t'_1[y/v'][x/u']) & = \\
\m(\m( t'_1[y/v'])[x/u'])
\end{array} \]

* If $\mX_\Del [x_1/u_1]\ldots[x_n/u_n] \paralp{} \mX_\Del [x_1/u'_1]\ldots[x_n/u'_n]'$ where $u_i \paralp{} u'_i$ and $x_i \notin \fv(u_j)$ for all $i, j \in [1,n]$ then we reason by induction on $n$.

Note that $\m(u)=u$ and $\m(u')=u'$. We use <ref> throughout.

For $n=0$ we have two cases.

If $x \notin \Del$ then $\m(\mX_\Del[x/u]) = \mX_\Del \paralp{\lm} \mX_\Del = \m(\mX_\Del[x/u'])$.

If $x \in \Del$ then $\m(\mX_\Del[x/u]) = \mX_\Del[x/\m(u)] \paralp{\lm}  \mX_\Del[x/\m(u')] = \m(\mX_\Del[x/u'])$.

– For $n>0$ we consider the following cases.

If $x \notin \fv(\mX_\Del [x_1/u_1]\ldots[x_n/u_n])$ then $x \notin \fv(\mX_\Del [x_1/u'_1]\ldots[x_n/u'_n])$ and thus

\begin{array}{ccc}
\m(\mX_\Del [x_1/u_1]\ldots[x_n/u_n][x/u])\\
\mX_\Del [x_1/u_1]\ldots[x_n/u_n] & \paralp{\lm} & \mX_\Del [x_1/u'_1]\ldots[x_n/u'_n]\\
&&\m(\mX_\Del [x_1/u'_1]\ldots[x_n/u'_n][x/u'])
\end{array}

If $x \in \fv(\mX_\Del [x_1/u_1]\ldots[x_n/u_n])$ then

\begin{array}{ll}
\m(\mX_\Del [x_1/u_1]\ldots[x_n/u_n][x/u]) & = \mbox{\cref{l:es-application-lambda-composition} $n$ times}\\
\m(\mX_\Del [x/u] [x_1/u_1[x/u]]\ldots[x_n/u_n[x/u]]) & = \\
\m(\mX_\Del [x/u]) [x_1/\m(u_1[x/u])]\ldots[x_n/\m(u_n[x/u])] & \paralp{\lm} \mbox{\ih\  $n$ times}\\
\m(\mX_\Del [x/u']) [x_1/\m(u'_1[x/u'])]\ldots[x_n/\m(u'_n[x/u' ])] & = \\
\m(\mX_\Del [x/u'] [x_1/u'_1[x/u']]\ldots[x_n/u'_n[x/u']]) & = \mbox{\cref{l:es-application-lambda-composition} $n$ times}\\
\m(\mX_\Del [x_1/u'_1]\ldots[x_n/u'_n][x/u'])&
\end{array}

Let $s,s'$ be $\mterms$-metaterms.
If $s \Rew{\lm} s'$ then $\m(s) \paralp{\lm} \m(s')$.

If $s \Rew{\m}  s'$, then $\m(s) =  \m(s')$  holds  by <ref>.      Thus,  $\m(s)
\paralp{} \m(s')$ and $\m(s)
\paralp{\lm} \m(s')$ holds by definition.
If $s=_{\Es} s'$, then $\m(s) =_{\Es}  \m(s')$
by <ref>.
Then $\m(s) =_{\Es}  \m(s')\paralp{} \m(s')$
implies $\m(s)
\paralp{\lm} \m(s')$.
It remains to show that  $s \Rew{\B} s'$ implies
$\m(s) \paralp{\m(s)} \m(s')$.
We reason by induction on $s$.

* If $s = (\l x. t)\ u \Rew{\B} t[x/u] = s'$, then
$\m(s) = (\l x. \m(t))\ \m(u) \paralp{}
\m(\m(t)[x/\m(u)]) \EqEs \m(t[x/u])$.
Then $\m(s) \paralp{\m(s)} \m(s')$.

* If $s = t\ u \Rew{\B} t'\ u=s'$, where $t \Rew{\B} t'$,
then by the   we get $\m(t\ u) =_{\mbox{\cref{l:s-distributes}}} \m(t)\ \m(u) \paralp{\lm}  \m(t')\ \m(u) =_{\mbox{\cref{l:s-distributes}}}
\m(s')$.

* If $s = t\ u \Rew{\B} t\ u'$, where $u \Rew{\B} u'$,
then by the   we get
$\m(t\ u) =_{\mbox{\cref{l:s-distributes}}} \m(t)\ \m(u) \paralp{\lm}  \m(t')\ \m(u)
\m(s')$.

* If $s = t\ u \Rew{\B} t\ u'$, where $u \Rew{\B} u'$,
then by the   we get
$\m(t\ u) =_{\mbox{\cref{l:s-distributes}}} \m(t)\ \m(u) \paralp{\lm} \m(t)\ \m(u') =_{\mbox{\cref{l:s-distributes}} }
\m(s')$.

* If $s = \l x. t \Rew{\B} \l x. t'$, where $t \Rew{\B} t'$, then
by the   we get
$\m( \l x. t) =_{\mbox{\cref{l:s-distributes}}} \l x. \m(t) \paralp{\lm} \l x. \m(t') =_{\mbox{\cref{l:s-distributes}} }
\m(s')$.

* If $s = t[x/u] \Rew{\B} t'[x/u]$, where $t \Rew{\B} t'$, then
$\m(t) \paralp{\lm} \m(t')$ by the  and
$\m(u) \paralp{\lm} \m(u)$ by definition.
By <ref>
$\m(s) \EqEs \m(\m(t)[x/\m(u)]) \paralp{\lm}
\m(\m(t')[x/\m(u)])  \EqEs \m(s')$.

* If $s = t[x/u] \Rew{\B} t[x/u']$, where $u \Rew{\B} u'$, then
$\m(u) \paralp{\lm}  \m(u')$ by the  and
$\m(t) \paralp{\lm} \m(t)$ by definition.
By <ref> we conclude
$\m(s)  \EqEs  \m(\m(t)[x/\m(u)]) \paralp{\lm}
\m(\m(t)[x/\m(u')])  \EqEs  \m(s')$.

Finally, one concludes that $s \Rew{\lm}  s'$ implies
$\m(s) \paralp{ \lm } \m(s')$.

From <ref>, we
conclude  that   $\m$    projects   $\Rew{\lm}$  into

The relation $\paralp{\lm}$ has the diamond property,  if $t_1 \lparalp{\lm} t \paralp{\lm} t_2$, then there is
$t_3$ such that $t_1 \paralp{\lm} t_3  \lparalp{\lm} t_2$.

By  induction on the definition of $\paralp{\lm}$. We organize the proof as follows.

* We first prove that $t \lparalp{} u =_{\Es} u'$
implies $t =_{\Es} t' \lparalp{} u'$ by induction on the
definition of  $t \lparalp{} u$.

*  We then conclude  that $t \lparalp{\lm} u =_{\Es} u'$
implies $t =_{\Es} t' \lparalp{} u'$ using the previous point.

*  We now prove that $t_1 \lparalp{} t \paralp{} t_2$
implies $t_1 \paralp{\lm} t \lparalp{\lm} t_2$.

* Let us consider

\[ (\l x. t_1)\  u_1 \lparalp{} (\l x. t)\ u \paralp{} \m(t_2[x/u_2]) \]

where $t \paralp{} t_1$ and $t \paralp{} t_2$ and
$u \paralp{} u_1$ and $u \paralp{} u_2$. By the   we
know there are $t_3$ and $u_3$ such that
$t_1 \paralp{\lm} t_3$ and $t_2 \paralp{\lm} t_3$ and
$u_1 \paralp{\lm} u_3$ and $u_2 \paralp{\lm} u_3$ so that
in particular
$t_1 =_{\Es} w_1 \paralp{} w_3 =_{\Es} t_3$ and
$u_1 =_{\Es} w'_1 \paralp{} w'_3 =_{\Es} u_3$.
We have

\[ (\l x. t_1)\  u_1 =_{\Es}
(\l x. w_1)\  w'_1 \paralp{}
\m(w_3[x/w'_3 ])  =_{\Es}
\m(t_3[x/u_3]) \]

and <ref> gives

\[ \m(t_2[x/u_2]) \paralp{\lm}
\m(t_3[x/u_3]) \]

* Let us consider

\[ \m(t_1[x/u_1]) \lparalp{} (\l x. t)\ u \paralp{} \m(t_2[x/u_2]) \]

where $t \paralp{} t_1$ and $t \paralp{} t_2$ and
$u \paralp{} u_1$ and $u \paralp{} u_2$. By the   we
know there are $t_3$ and $u_3$ such that
$t_1 \paralp{\lm} t_3$ and $t_2 \paralp{\lm} t_3$ and
$u_1 \paralp{\lm} u_3$ and $u_2 \paralp{\lm} u_3$.
Then, <ref> gives

\[ \m(t_1[x/u_1]) \paralp{\lm} \m(t_3[x/u_3]) \lparalp{\lm} \m(t_2[x/u_2])  \]

* All the other cases are straightforward
using <ref>.

* We finally prove the diamond property as follows.
Let $t_1 \lparalp{\lm} t =_{\Es} u \paralp{} u' =_{\Es}  t_2$.
By point (<ref>) there is $u_1$ such that
$t_1 =_{\Es} u_1 \lparalp{}  u$ and by  point (<ref>) there is
$t_3$ such that $u_1 \paralp{\lm}  t_3 \lparalp{\lm} u'$.
We conclude
$t_1 \paralp{\lm}  t_3 \lparalp{\lm} t_2$.

The $\lm$-reduction relation  is confluent on $\mterms$-terms and $\mterms$-metaterms.

Take any  $\mterms$-metaterms $t, t_1, t_2$
such that $t \Rewn{\lm} t_i$ for $i=1,2$.
gives  $\m(t) \paralnp{} \m(t_i)$.
Since   the  diamond  property  implies
confluence [7], then <ref>
implies   confluence of $\paralp{}$.
Therefore, there is
a metaterm $s$ s.t. $\m(t_i) \paralnp{} s$.
By <ref> the (unique) $\m$-normal forms
of $t_i$ exist, so that
$t_i \Rewn{\m} \m(t_i)$.
We can then  close the
diagram by $t_i \Rewn{\m} \m(t_i) \Rewn{\lm} s$ using <ref>
to obtain $\m(t_i) \Rewn{\lm} s$ from $\m(t_i) \paralnp{} s$.

§ RELATING PARTIAL SUBSTITUTIONS TO DEFINITIONS

Partial substitution can be  related to calculi with definitions.
A definition can be understood as an abbreviation given
by a name for a larger term which can be used several times
in a program or a proof. A definition mechanism
is essential for practical use; current implementations of
proof assistants provide such a facility.

We  consider two  calculi,  the  first  one, which  we  call
$\lpar$,  appears  in [12]  and  uses  a  notion  of
partial  substitution on  $\l$-terms, while  the second  one, which  we call
$\ldef$,  uses  partial substitutions  on $\mterms$-terms to  model definitions  and
combines  standard  $\beta$-reduction   with  the  rules  of the
substitution calculus $\m$. The general result of this section is
that normalisation  in $\lpar$ and  $\lm$ are equivalent  on $\l$-terms and normalisation in  $\ldef$ and $\lm$ are equivalent
on $\mterms$-terms. More precisely,  for every  $\l$-term $t$, $t
\in \SN{\lpar}$ if  and only if $t \in \SN{\lm}$  and for every
$\mterms$-term  $t$,  $t  \in  \SN{\ldef}$  if and  only  if  $t  \in
\SN{\lm}$.   Thus,  the $\lm$-calculus  can  be  understood as  a
concise  and simple  language implementing  partial  and ordinary
substitution,  both in implicit  and explicit  style at  the same

§.§ The partial $\lpar$-calculus

Terms of the partial $\lpar$-calculus are $\l$-terms. The operational
semantics of the $\lpar$-calculus is given by the following rules:

\[ \begin{array}{|llll|}
\hline
(\l x. C\cwc{x}_\phi)\ u    &\Rew{\bp}  & (\l x. C\cwc{u}_\phi)\ u & \mbox{ if } \{x\} \cup \fv(u) \subseteq \phi\\
(\l x. t)\ u    &\Rew{\BGc}   & t & \mbox{ if } x \notin \fv(t) \\
\hline
\end{array} \]

We consider the following translation from  $\l$-terms to

\[ \begin{array}{lclll}
\begin{array}{lll}
\parlm{x} & := & x \\
\parlm{\l x. t} & := & \l x. \parlm{t}
\end{array}
\parlm{t\ u} & := & \left \{ \begin{array}{ll}
\parlm{t}\ \parlm{u} & \mbox{ if } t
\mbox{ is not a $\l$-abstraction} \\
\parlm{v}[x/\parlm{u}] & \mbox{ if } t=
\l x. v  \\
\end{array} \right .
\end{array} \]

Let $t,t'$ be $\l$-terms.
If $t \Rew{\lpar} t'$, then $\parlm{t} \Rewplus{\lm} \parlm{t'}$.

By induction on $\Rew{\lpar}$.

Let $t$ be a  $\l$-term.
If $t \in \SN{\lm}$, then $t \in \SN{\lpar}$.

Let  $t \in \SN{\lm}$ and suppose $t \notin \SN{\lpar}$.
Then, from an infinite $\lpar$-reduction sequence starting
at $t$ we can construct, by <ref>,
an infinite $\lm$-reduction sequence starting at $\parlm{t}$.
Since $t \Rewn{\lm} \parlm{t}$, then $t \notin \SN{\lm}$,  which
leads to a contradiction. We thus conclude $t \in \SN{\lpar}$.

The  converse reasoning also works. Define a
translation from $\mterms$-terms  to $\l$-terms:

\[ \begin{array}{lll@{\hspace{2cm}}lll}
\lmpar{x} & := & x &
\lmpar{\l x. t} & := & \l x. \lmpar{t}\\
\lmpar{t\ u} & := & \lmpar{t}\ \lmpar{u} &
\lmpar{t[x/u]} & := & (\l x. \lmpar{t})\ \lmpar{u} \\
\end{array} \]

Remark that $\lmpar{t}\isubs{x}{\lmpar{u}} =
\lmpar{t\isubs{x}{u}}$.

Let $t,t'$ be $\mterms$-terms
such that $t \Rew{\lm} t'$.
If $t \Rew{\B} t'$, then $\lmpar{t} = \lmpar{t'}$.
If  $t \Rew{\m} t'$, then $\lmpar{t} \Rewplus{\lpar} \lmpar{t'}$.

By induction on $\Rew{\lm}$.

Let $t$ be a  $\l$-term.
Then $t \in \SN{\lpar}$ if and only if $t \in \SN{\lm}$.

If   $t \in \SN{\lm}$, then $t \in \SN{\lpar}$
by <ref>.
For the converse, let  $t \in \SN{\lpar}$ and suppose $t \notin \SN{\lm}$.
Consider an infinite $\lm$-reduction sequence starting
at $t$. Since $\Rew{\B}$ is terminating,  such
infinite reduction sequence must contain an infinite
number of  $\Rew{\m}$ steps. By <ref>
this gives  an infinite $\lpar$-reduction sequence starting at
$\lmpar{t}$. Since $t$ is a $\l$-term, then $\lmpar{t} = t$,
thus $t \notin \SN{\lpar}$ which leads to a contradiciton.
We conclude $t \in \SN{\lm}$.

§.§ The $\l$-calculus with definitions $\ldef$

The syntax         of          the         $\l$-calculus         with
definitions $\ldef$ [35],  is isomorphic to
that of the $\lm$-calculus, where the use of a definition $x:=u$ in a term $v$,
denoted ${\tt let}\ x:=u\ {\tt in}\ v$, can be thought
as the term $v[x/u]$ in          $\lm$.          The         original
presentation [35]    of   the   operational
semantics of $\ldef$ is given  by a reduction system which is not
a (higher-order) term rewriting system.   This is due to the fact
that given a  definition $x:=u$, the term $x$  can be reduced to
the term $u$, so that  reduction creates new free variables since
$\fv(u)$  does  not necessarily  belong  to  $\set{x}$. Here,  we
present $\ldef$ by  a set of reduction rules  which preserve free
variables  of  terms.   Moreover,  we  consider  a  more  general
reduction   system  where   any  $\beta$-redex   can   be  either
$\beta$-reduced  or  transformed   to  a  definition,  while  the
calculus  appearing in [35] does  not allow
dynamic creation of definitions.

\[ \begin{array}{|llll|}
\hline
(\l x. t)\ u    &\Rew{\beta}  & t \isubs{x}{u} & \\
(\l x. t)\ u    &\Rew{\B}   & t[x/u] & \\
t[x/u]          &\Rew{\Gc}  & t      & \mbox{ if } x \notin \fv(t) \\
C\cwc{x}_\phi[x/u]   &\Rew{\us}   & C\cwc{u}_\phi[x/u] & \mbox{ if } \{x\} \cup \fv(u) \subseteq \phi\\
\hline
\end{array} \]

The following relations between $\ldef$ and $\lm$ holds:

Let $t,t'$ be $\mterms$-terms.

* If $t \Rew{\ldef} t'$, then $t \Rewplus{\lm} t'$.

* If $t \Rew{\lm} t'$, then $t \Rewplus{\ldef} t'$.

The first point can be shown by induction on $\Rew{\ldef}$ using the fact that
any $\beta$ step can be simulated by $\B$ followed
by several $\us$ steps and one $\Gc$ step.
The second point is straightforward.

We can then conclude that normalisation for
the $\ldef$-calculus and the  $\lm$-calculus are  equivalent:

Let $t$ be a $\mterms$-term.
Then $t \in \SN{\lm}$ if and only if  $t \in \SN{\ldef}$.

§ RELATING PARTIAL TO EXPLICIT SUBSTITUTIONS

We now relate $\lm$ to a calculus with  explicit (local)
substitutions called $\les$ [20], summarised below. We then give
a (dynamic) translation from $\lm$ to $\les$,
showing that each
$\lm$-reduction step can be simulated by a non-empty reduction
sequence in $\les$. This result  will
be used in particular in the forthcoming <ref>
and <ref>
to obtain different normalisation theorems.

Terms of the $\les$-calculus are   $\mterms$-terms.
Besides $\alpha$-conversion, we consider the equations and reduction
rules in <ref>.
Remark that  working modulo $\alpha$-conversion  allows us
to assume implicitly some conditions to avoid capture of
variables such as  for example $x \neq y$ and $y \notin
\fv(v)$ in the reduction rule $\Lamb$.

\[ \begin{array}{|lcll|}
\hline
\mbox{{\bf Equations}}: &&&\\
t[x/u][y/v]  & =_{\Com} &   t[y/v][x/u] &  \mbox{ if } y \notin \fv(u)\ \&\
x \notin \fv(v)\\ % \&\ x \neq y \\
\mbox{{\bf Reduction Rules}}: &&&\\
(\l x. t)\ u    &\Rew{\B}   & t[x/u] & \\
x[x/u]          &\Rew{\Var}& u & \\
t[x/u]          & \Rew{\Gc} & t & \mbox{ if } x \notin \fv(t) \\
(t\ u)[x/v]     &\Rew{\Appi} &(t[x/v]\ u[x/v]) & \mbox{ if } x \in \fv(t)\ \&\  x \in \fv(u)\\
(t\ u)[x/v]     &\Rew{\Appii} &(t\ u[x/v])& \mbox{ if } x \notin \fv(t)\ \&\  x \in \fv(u)\\
(t\ u)[x/v]     &\Rew{\Appiii} &(t[x/v]\ u)& \mbox{ if } x \in \fv(t)\ \&\  x \notin \fv(u)\\
(\l y.t)[x/v]   &\Rew{\Lamb} &  \l y . t[x/v] & \\
t[x/u][y/v]   &\Rew{\Compi}& t[y/v][x/u[y/v]] & \mbox{ if } y \in
\fv(u)\ \&\ y \in \fv(t)\\ % \&\ x \notin \fv(v)\ \&\ x \neq y \\
t[x/u][y/v]   &\Rew{\Compii}& t[x/u[y/v]] & \mbox{ if } y \in \fv(u)\ \&\ y
\notin \fv(t)\\
\hline
\end{array} \]

Equations and reduction rules for $\les$

We  consider the equivalence  relation $\Es$
generated   by  $\alpha$   and  $\Com$.
The  rewriting   system  containing
all the reduction rules except $\B$
is denoted
by $\s$. We write $\B\s$
for $\B  \cup \s$.
We note $\Rew{\ALC}$, the reduction
relation  generated by the rules  $\{ \Appi,$
$\Appii,$ $\Appiii,$ $\Lamb,$ $\Compi,$ $\Compii \}$,
closed by all contexts, and taken
modulo the equivalence relation  $\Es$.
The  reduction
relations of the $\les$-calculus are  generated by  $\s$ (resp.
$\B\s$) modulo $\Es$, and  is denoted
by  $\Rew{\es}$  (resp.  $\Rew{\les}$),  where  e  means
equational and s means substitution.
As expected, reduction  preserves free variables.

Let $t,t'$ be $\mterms$-terms.
If $t \Rew{\les} t'$, then  $\fv(t') \subseteq \fv(t)$. More precisely,
$t \Rew{\Gc} t'$ implies $\fv(t') \subseteq \fv(t)$, in
all other cases $\fv(t') = \fv(t)$.

We write $t [\vec{x}/\vec{u}]$ for $t [x_1/u_1] \ldots [x_n/u_n]$
where $\vec{x} = x_1, \ldots, x_n$, $\vec{u} = u_1, \ldots, u_n$,
and $x_i \notin \fv(u_j)$  where $i,j \in [1,\ldots,n]$. We write
$x_i$ to  denote an  arbitrary member of  $x_1, \ldots,  x_n$ and
similarly for  $u_i$. The concatenation of  two vectors $\vec{x}$
and   $\vec{y}$   is   written    as   $\vv{xy}$.   We   let   $t
[\vec{x}/\vec{u}]$ denote the  $=_\Com$-equivalence class which
arises by the reordering of the independent substitutions.

We extend the set  of variables with marked variables $\fresh{x},
\fresh{y}$, etc.   This will be used to  denote binders of
certain garbage substitutions which  will be fresh i.e. if
$t = v[\fresh{x}/u]$ then $\fresh{x} \notin \fv(v)$.

Remark that $\Rew{\ALC}$ may only propagate
garbage substitutions  through
abstractions  and  not through  applications  or inside  explicit

The reduction relation $\Rew{\ALC}$ is locally confluent and locally coherent.

See <ref>.

The $\ALC$-normal forms of terms exist and are unique modulo $\Es$.

The system $\Rew{\es}$ is terminating [20] and so
in particular $\Rew{\ALC}$
turns out to be  terminating.
By <ref>, $\Rew{\ALC}$ is locally confluent and locally coherent.
Therefore by [18], $\Rew{\ALC}$ is confluent and hence $\ALC$-normal
forms are unique modulo $\Es$-equivalence.

From now on, we can assume the existence
of a function $\ALC$ computing
the (unique) $\ALC$-normal form
of a $\mterms$-term, modulo $\Es$.
This allows us in particular
to define   the following     translation $\nombretra$  from  $\mterms$-terms  to
$\ALC$-normal forms:

\begin{array}{lcll}
\tra{x} & :=& x\\
\tra{\l x. t} & :=& \l x. \tra{t}\\
\tra{t\ u} & :=& (\tra{t}\ \tra{u})[\fresh{y}/\tra{u}] & \mbox{ where } \fresh{y} \mbox{ is fresh}\\
\tra{t[y/u]} & :=& \ALC(\tra{t}[y/\tra{u}]) & \mbox{ if $y \notin \fv(t)$}\\
\tra{t[y/u]} & :=& \ALC(\tra{t}[y/\tra{u}][\fresh{y}/\tra{u}]) & \mbox {
if $y \in \fv(t)$ where $\fresh{y}$ is fresh}
\end{array}

Remark that the translation $\tra{\_}$ preserves free variables.  Remark also
that the translation of a closure $\tra{t[y/u]}$ with $y \in \fv(t)$
introduces a garbage substitution with binder $\fresh{y}$. The
translation of $\tra{t\ u}$ similarly introduces garbage. Intuitively,
this should not interfere with the PSN property as: i) the body of the
garbage is strongly normalising exactly when the body of the regular
substitution is; and ii) the garbage substitution can only interact
with substitutions above it as can the regular substitution so that
any resulting infinite sequences can occur in the regular substitution
as well.  We call these garbage substitutions which are introduced by
the translation idle substitutions whilst the other
substitutions are called mobile substitutions.

The  translation  $\tra{\_}$  duplicates  all non-garbage  substitutions  and
function arguments, creating idle copies as garbage substitution.
The reasoning is as follows.

To    simulate     the   partial   substitution
$\Rew{\us}$ of the  $\lm$-calculus, we use the  (local) subcalculus $\ALC$.

$\ALC$-normal forms are required in order
to prove a simulation (otherwise the reduction $((x\ x)\ x)[x/y] \Rew{\us}
((y\ x)\ x)[x/y]$ cannot be simulated).

Now  consider the (partial)  reduction $x[x/z]  \Rew{\us} z[x/z]$
versus  the  (local) reduction  $x[x/z]  \Rew{\Var} z$.   Partial
reduction does  not remove the explicit  substitution $[x/z]$ but
local reduction  will correctly do  so as no free  occurrences of
the bound variable  $x$ lie beneath the body  of the substitution
$z$.   Therefore,   we   cannot  immediately   simulate   partial
substitution.   A   naive  solution  would  be   to  compose  the
translation with a reduction  to the garbage-free normal form but
this clearly  fails in the  general case; we should  instead keep
the garbage.

Finally,    consider    the     sequence    $(x\    x\    x)[x/y]
\Rewn{\lm} (y\ y\  y)[x/y]$. From the discussion above,
the  translation needs  to  both push  the explicit  substitution
inside  the  term  and  also  keep it  outside  awaiting  garbage
collection. Our solution is  to simply duplicate the substitution
in such a way as to solve this problem.

In  short, the  mobile substitutions  allow us  to  simulate most
$\Rew{\us}$   reductions  but   idle   substitutions  are
required to  simulate $\Rew{\us}$  reductions where the  last free
occurrence of the bound variable is replaced.

The reader should notice that
if $t$ is pure then $t = \Gc(\tra{t})$.
Also, if $t$ is in $\Rew{\lm}$-normal form, then $\Gc(\tra{t})$
is in $\Rew{\les}$-normal form so that $\tra{t}$ turns out to be
in $\SN{\les}$.

If $t$ is pure then:

* $t = \Gc(\tra{t})$;

* If $t$ is in $\Rew{\lm}$-normal form then $\Gc(\tra{t})$ is in $\Rew{\les}$-normal form; and

* If $t$ is in $\Rew{\lm}$-normal form then $\tra{t} \in \SN{\les}$.

* Induction on the structure of $t$.

* Prove that $\tra{t}$ only has $\Gc$-redexes by induction on the structure of $t$. As $\Gc$-reductions do not create new redexes, any $\Rewn{\Gc}$-reduct of $\tra{t}$ has only $\Gc$-redexes. The result follows by $\Rew{\Gc}$ SN.

* Follows from (2).

* We prove by induction on the structure of $t$.

* $t = x$. Trivial.

* $t = \l x.t'$.

By , $t' = \Gc(\tra{t'})$. Therefore, $t = \l x.t' = \l x.\Gc(\tra{t'}) = \Gc(\tra{t})$.

* $t = (u\ v)$.

By , $u = \Gc(\tra{u})$ and $v = \Gc(\tra{v})$.  Therefore, $t = (u\ v) = (\Gc(\tra{u})\  \Gc(\tra{v})) = \Gc(\tra{u}\  \tra{v}) = \Gc((\tra{u}\  \tra{v})[z/\tra{u}]) = \Gc(\tra{t})$.

* We first show that $\tra{t}$ has no $\B$-redexes by inducting over the structure of $t$.

* $t = x$. Trivial.

* $t = \l x.t'$. $\tra{t} = \l x.\tra{t'}$. By , $\tra{t'}$ has no $\B$-redexes and so neither has $\tra{t}$.

* $t = (u\ v)$. $\tra{t} = (\tra{t}\ \tra{u})[z/\tra{u}]$.  By , $\tra{u}$ and $\tra{v}$ have no $\B$-redexes. Since $t = (u\ v)$ has no $\B$-redexes, $u \neq \l x.u'$ so $\tra{u} \neq \l x.\tra{u'}$. Therefore, $\tra{t}$ has no $\B$-redexes.

We now argue about what other redexes $\tra{t}$ does have. All substitutions are garbage so there are no $\Var$ redexes. As the substitutions also lie above applications, there are no $\ALC$ redexes. Therefore $\tra{t}$ can only have $\Gc$ redexes and the same holds for any $\Rewn{\Gc}$-reduct of $\tra{t}$. The result follows by $\Rew{\Gc}$ SN.

* Follows from (2).

Let $t,t',v$ be $\mterms$-terms.
If $t \Rew{\les} t'$ then $t\isubs{z}{v} \Rew{\les} t'\isubs{z}{v}$.

By induction on the definition of $t  \Rew{\les}  t'$.

By induction on the recursive  definition of $t
\Rew{\les}  t'$.  By $\alpha$-equivalence,  we can  assume that
$\fv(v)$  and $\bv(t)$  are distinct  sets and  that  $z \notin
\bv(t)$.  We  first  consider  the  base  case  of  the
induction  where reductions  $t \Rew{\les}  t'$ occur  at the root.

* $t = (\l x. u_1)\ u_2 \Rew{\les} u_1[x/u_2] = t'$.

$t\isubs{z}{v} = (\l x. u_1\isubs{z}{v})\ u_2\isubs{z}{v} \Rew{\les} u_1\isubs{z}{v}[x/u_2\isubs{z}{v}]$.

* $t = x[x/u] \Rew{\les} u = t'$.

$t\isubs{z}{v} = (x[x/u])\isubs{z}{v} = x[x/u\isubs{z}{v}] \Rew{\les} u\isubs{z}{v}$.

* $t = u_1[x/u_2] \Rew{\les} u_1 = t'$.

$t\isubs{z}{v} = (u_1[x/u_2])\isubs{z}{v} = u_1\isubs{z}{v}[x/u_2\isubs{z}{v}] \Rew{\les} u_1\isubs{z}{v}$.

* $t = (u_1\ u_2)[x/u_3] \Rew{\les} (u_1[x/u_3]\ u_2[x/u_3]) = t'$.

$t\isubs{z}{v} = (u_1\isubs{z}{v}\

$\Rew{\les} (u_1\isubs{z}{v}[x/u_3\isubs{z}{v}]\ u_2\isubs{z}{v}[x/u_3\isubs{z}{v}])$.

* $t = (u_1\ u_2)[x/u_3] \Rew{\les} (u_1[x/u_3]\ u_2) = t'$. Similar.

* $t = (u_1\ u_2)[x/u_3] \Rew{\les} (u_1\ u_2[x/u_3]) = t'$. Similar.

* $t = (\l y.u_1)[x/u_2] \Rew{\les} \l y.u_1[x/u_2] = t'$.

$t\isubs{z}{v} = (\l y.u_1\isubs{z}{v})[x/u_2\isubs{z}{v}] \Rew{\les} (\l y.u_1\isubs{z}{v}[x/u_2\isubs{z}{v}])$.

* $t = u_1[x/u_2][y/u_3] \Rew{\les} u_1[y/u_3][x/u_2[y/u_3]] = t'$.

$t\isubs{z}{v} = u_1\isubs{z}{v}[x/u_2\isubs{z}{v}][y/u_3\isubs{z}{v}]$

$\Rew{\les} u_1\isubs{z}{v}[y/u_3\isubs{z}{v}][x/u_2\isubs{z}{v}[y/u_3\isubs{z}{v}]]$.

* $t = u_1[x/u_2][y/u_3] \Rew{\les} u_1[x/u_2[y/u_3]] = t'$. Similar.

The inductive cases are the following:

* $t = (u_1\ u_2) \Rew{\les} (u'_1\ u_2) = t'$.

$t\isubs{z}{v} = (u_1\isubs{z}{v}\ u_2\isubs{z}{v}) \Rew{\les}$ ()  $(u'_1\isubs{z}{v}\ u_2\isubs{z}{v})$.

* $t = (u_1\ u_2) \Rew{\les} (u_1\ u'_2) = t'$. Similar.

* $t = \l y.u_1 \Rew{\les} \l y.u'_1 = t'$. Similar.

* $t = u_1[x/u_2] \Rew{\les} u'_1[x/u_2] = t'$. Similar.

* $t = u_1[x/u_2] \Rew{\les} u_1[x/u_2'] = t'$. Similar.

Let $t,t',v$ be $\mterms$-terms.
If $t \Rew{\les}^n t'$ then $t\isubs{z}{v} \Rew{\les}^n
t'\isubs{z}{v}$, for $n \geq 0$.

Remark that if $t = t_1[x/u_1][y/u_2] =_{\Es} t_2[y/u_2][x/u_1] = t'$ then $t\isubs{z}{v}  =_{\Es} t'\isubs{z}{v}$ and use <ref> to conclude.

As a particular case of the previous corollary, we have
$t\isubs{z}{v} \Rewn{\ALC} \ALC(t)\isubs{z}{v}$.

Let $t,v$ be $\mterms$-terms.
Then $\ALC(t)\isubs{z}{\fresh{z}[\fresh{z}/v]}  = \ALC(t[z/v])$  if $z
\in \fv(t)$ and $v$ in $\ALC$-normal form.

By induction on  the structure of $t$.

By induction on  the structure of $t$.
By $\alpha$-equivalence, we can assume that $\fv(v)$ and $\bv(t)$ are distinct sets.

* $t = z$. $\ALC(t)\isubs{z}{\fresh{z}[\fresh{z}/v]} = \fresh{z}[\fresh{z}/v] = \ALC(z[z/v])$.

* $t = t_1\ t_2$. There are three cases depending on whether $z \in \fv(t_1)$, $z \in \fv(t_2)$, or both. We treat the case where $z \in \fv(t_1)$ and $z \notin \fv(t_2)$.

$\ALC(t)\isubs{z}{\fresh{z}[\fresh{z}/v]} = (\ALC(t_1)\isubs{z}{\fresh{z}[\fresh{z}/v]}\ \ALC(t_2)\isubs{z}{\fresh{z}[\fresh{z}/v]})$
$=$ () $\:(\ALC(t_1[z/v])\ \ALC(t_2)) = \ALC((t_1\ t_2)[z/v])$.

* $t = \l y.t_1$.
$\ALC(t)\isubs{z}{\fresh{z}[\fresh{z}/v]} = \l y.\ALC(t_1)\isubs{z}{\fresh{z}[\fresh{z}/v]}$

$=$ () $\:\l y. \ALC(t_1[z/v]) = \ALC((\l y. t_1)[z/v])$.

* $t = t_1[x/t_2]$. There are three cases depending on whether $z \in \fv(t_1)$, $z \in \fv(t_2)$, or both. We treat the case where $z \in \fv(t_1)$ and $z \notin \fv(t_2)$. Note that $\ALC$ preserves free names.

$\ALC(t[z/v])  =    \ALC(t_1[x/t_2][z/v])  = \ALC(t_1[z/v][x/t_2])\\
=\ALC(\ALC(t_1[z/v])[x/t_2])         =         \mbox{(\ih)         }
\:\ALC(\ALC(t_1)\isubs{z}{\fresh{z}[\fresh{z}/v]}[x/t_2])\\
=\ALC(t_1\isubs{z}{\fresh{z}[\fresh{z}/v]}[x/t_2])                 =
\ALC(t_1[x/t_2])\isubs{z}{\fresh{z}[\fresh{z}/v]}.$

Let $t,t',v$ be $\mterms$-terms in $\ALC$-normal form.
If $t \Rewplus{\les} t'$  then:

*  if $z \notin \fv(t)$ then $\ALC(t[z/v]) \Rewplus{\les} \ALC(t'[z/v])$;

*  if $z \in \fv(t)$ and $z \in \fv(t')$ then $\ALC(t[z/v]) \Rewplus{\les} \ALC(t'[z/v])$;

*  if $z \in \fv(t)$ and $z \notin \fv(t')$ then $\ALC(t[z/v]) \Rewplus{\les} t'$.

Note that by our conventions, $z \notin \bv(t)$.

* Let $z  \notin \fv(t)$. Write $t$ as  $\l \vec{y}.s$, where
$s$ is not a $\l$-abstraction.  As $t \Rewplus{\les} t'$ and $t
= \l \vec{y}.s$, it must be that $s \Rewplus{\les} \l
\vec{x}.s'$ with  $t' = \l \vec{y}. \l  \vec{x}.s'$, where $s'$
is not  a $\l$-abstraction and  $s,s'$ in $\ALC$-normal
form.     Therefore,   $\ALC(t[z/v])   =    \l   \vec{y}.s[z/v]
\Rewplus{\les} \l   \vec{y}.(\l   \vec{x}.s')[z/v]
\Rewn{\les}   \l   \vec{y}.\l   \vec{x}.s'[z/v]   =
\ALC(t'[z/v])$.

We define $\U(p)  = p\isubs{z}{\fresh{z}[\fresh{z}/v]}$ for any
$p$ in the sequence  $t \Rewplus{\les} t'$.
Then, from the sequence
$t = t_1 \Rew{\les} t_2 \Rew{\les} \ldots  \Rew{\les} t'$
we can build by <ref>
a sequence of the form
$\U(t_1) \Rew{\les} \U(t_2) \Rew{\les}\ldots  \Rew{\les} \U(t')$.

We have now two cases:

If $z \in \fv(t')$ then
$\U(t_1) = t\isubs{z}{\fresh{z}[\fresh{z}/v]} = \ALC(t[z/v]) \Rewplus{\les} \U(t') = t'\isubs{z}{\fresh{z}[\fresh{z}/v]} = \ALC(t'[z/v])$, using <ref> twice.

If $z \notin \fv(t')$ then $\U(t_1) = t\isubs{z}{\fresh{z}[\fresh{z}/v]} = \ALC(t[z/v]) \Rewplus{\les} \U(t') = t'\isubs{z}{\fresh{z}[\fresh{z}/v]} = t'$ using <ref> once.

Let $t,u,u'$ be $\mterms$-terms.
Let $u$ be in $\ALC$-normal form.
If $u \Rew{\les} u'$  then
$\ALC(t[z/u]) \Rewplus{\les} \ALC(t[z/u'])$.

Details in <ref>.

Let $t,u,u'$ be $\mterms$-terms. Let $u$ be in $\ALC$-normal form.
If $u \Rewplus{\les} u'$   then

$$\ALC(t[z/u]) \Rewplus{\les} \ALC(t[z/u']).$$

Let $t,u,u'$ be $\mterms$-terms.
If $\fresh{x}$ is fresh for $t$ and $t'$ and
$\ALC(t[\fresh{x}/u]) \Rewplus{\les} \ALC(t'[\fresh{x}/u])$
then  $\ALC(t) \Rewplus{\les} \ALC(t')$. pareceria ser *

The garbage substitution $[\fresh{x}/u]$ may not be copied during the sequence$\ALC(t[\fresh{x}/u]) \Rewplus{\les} \ALC(t'[\fresh{x}/u])$.
Moreover, $\ALC(t'[\fresh{x}/u])$
does not erase any substitution,
then this same sequence cannot discard $[\fresh{x}/u]$. It occurs exactly once in each term of the sequence. For any such term $p$, we define $\Er(p)$ as the term obtained by dropping the substitution $[\fresh{x}/u]$.

The proof  follows from the diagram  below where the  top line is
the       sequence      $t_1= \ALC(t[\fresh{x}/u])      \Rewplus{\les}
\ALC(t'[\fresh{x}/u])=t_n$.  The  squares   in  the  diagram  can  be
completed as either $\mbox{i) } t_i = \l \vec{z}.v_i[\fresh{x}/u]
\Rew{\les} \l \vec{z}.v_{i+1}[\fresh{x}/u]  = t_{i+1} \mbox{ with
}  v_i \Rew{\les}  v_{i+1}$ so  that $\Er(t_i)  =  \l \vec{z}.v_i
\Rew{\les}  \l  \vec{z}.v_{i+1}$;  or   $\mbox{ii)  }  t_i  =  \l
\vec{z}.(\l  w.  v_i)[\fresh{x}/u]  \Rew{\les} \l  \vec{z}.\l  w.
v_i[\fresh{x}/u] = t_{i+1}$   so  that $\Er(t_i) = \l \vec{z}.\l w.
v_i = \Er(t_{i+1})$.

\[ \begin{array}{lllllllllllllll}
t_1 & \Rew{\les} & t_2 & \Rew{} & \ldots & \Rew{} & t_n\\
\\
\Er(t_1) & \Rewn{\les} & \Er(t_2) & \Rewn{\les} & \ldots & \Rewn{\les} & \Er(t_n)\\
\end{array} \]

Let $t, t'$ be $\mterms$-terms.
If $t =_{\Es} t'$ then $\tra{t} =_{\Es} \tra{t'}$.

By induction on the definition of  $t =_{\Es} t'$.

* $t = t_1[x/t_3][y/t_2] =_{\Es} t_1[y/t_2][x/t_3] = t'$ with $y \notin \fv(t_3), x \notin \fv(t_2)$. We treat the case where $x,y \in \fv(t_1)$. We have

\begin{array}{ll}
= & \ALC(\tra{t_1}[x/\tra{t_3}][\fresh{x}/\tra{t_3}][y/\tra{t_2}][\fresh{y}/\tra{t_2}]).
\end{array}

As $\ALC$ has unique normal forms up to $_{\Es}$, we have

\begin{array}{ll}
& \ALC(\tra{t_1}[x/\tra{t_3}][\fresh{x}/\tra{t_3}][y/\tra{t_2}][\fresh{y}/\tra{t_2}])\\
=_{\cref{l:same-variables-tra}} & \ALC(\tra{t_1}[y/\tra{t_2}][\fresh{y}/\tra{t_2}][x/\tra{t_3}][\fresh{x}/\tra{t_3}])\\
= & \tra{t_1[y/t_2][x/t_3]}.
\end{array}

* $t = x =_{\Es} x = t'$.

* $t = \l x.t_1 =_{\Es} \l x.t'_1  = t'$ with $t_1 =_{\Es} t'_1$. Then $\tra{\l x.t_1} = \l x. \tra{t_1} =_{\ih} \l x. \tra{t'_1} = \tra{\l x.t'_1}$.

* $t = t_1\ t_2 =_{\Es} t'_1\ t'_2 = t'$ with $t_1 =_{\Es} t'_1$ and $t_2 =_{\Es} t'_2$. Then $\tra{t_1\ t_2} = \tra{t_1}\ \tra{t_2} =_{\ih} \tra{t'_1}\ \tra{t'_2} = \tra{t'_1\ t'_2}$.

* $t = t_1[y/t_2] =_{\Es} t'_1[y/t'_2] = t'$ with $t_1 =_{\Es} t'_1$ and $t_2 =_{\Es} t'_2$. We will consider the case where $y \in \fv(t_1)$. We have $\tra{t_1[y/t_2]} = \ALC(\tra{t_1}[y/\tra{t_2}][\fresh{y}/\tra{t_2}])$. As $\ALC$ has unique normal forms up to $_{\Es}$, we have $\ALC(\tra{t_1}[y/\tra{t_2}][\fresh{y}/\tra{t_2}]) =_{\ih} \ALC(\tra{t'_1}[y/\tra{t'_2}][\fresh{y}/\tra{t'_2}]) = \tra{t'_1[y/t'_2]}$.

[$\les$ simulates $\lm$]propositionlessimulateslm
Let $t, t'$ be $\mterms$-terms.
If $t \Rew{\lm} t'$ then $\tra{t} \Rewplus{\les} \tra{t'}$.

By induction on  $t \Rew{\lm} t'$.
Details can be found in  [32].

This property will be used in <ref>
to give an alternative
proof of $\lm$-strong normalisation
of simply typable terms, and in <ref> to relate simply
typable $\mterms$-terms to MELL proof-nets.

Let $t$ be a $\mterms$-term.
If $t \in \SN{\les}$,  then $t\in \SN{\lm}$.

Let $t \in \SN{\les}$ and suppose $t\notin \SN{\lm}$.
Then, there is an infinite $\lm$-reduction sequence starting at
$t$, which projects, by <ref>,
to an infinite $\les$-reduction sequence
starting at $\tra{t}$. RELACIONAR
$t \in \SN{\les}$ con $\tra{t} \in \SN{\les}$.

§ NORMALISATION PROPERTIES

Intersection   type   disciplines [9, 10]   are   more
flexible  than simple  type systems  in the  sense that  not only are
typed  terms strongly  normalising,  but  the converse  also
holds,  thus giving  a characterisation  of the  set  of strongly
normalising     terms.     Intersection    types
for calculi with explicit substitutions not enjoying
full composition have been
studied in [24, 21]. Here, we apply this
technique to   $\lm$,
and  obtain  a characterisation  of the  set of
strongly-normalising terms by means of intersection types.

Moreover, we study PSN. The
PSN  property  received a  lot  of  attention  in calculi  with
explicit            substitutions            (see           for
example [1, 5, 8]),   starting   from  an
unexpected  result given  by  Melliès [26] who
has shown that there are $\beta$-strongly normalisable terms in
$\l$-calculus  that are  not strongly  normalisable  in calculi
such as $\lambda\sigma$ [1].  Since then, there was a
challenge to  define calculi with  explicit substitutions being
confluent on metaterms and enjoying PSN at the same time.  Many
formalisms     such    as for example
$\lambda_{ws}$ [13]
and  $\les$ [20]  have been  shown to
enjoy   both   properties: confluence on metaterms and PSN.    In   particular,   $\lm$   enjoys
PSN [31].   However,  the   first  proof  of  this
result [31]    is    quite   involved.     Indeed,
$\lm$-reduction is simulated by  another  calculus enjoying
PSN,   called  $\lambda_{{\tt  blxr}}$,   which  is   a  slight
modification of $\llxr$ [22],  a formalism with explicit
ressources  (weakening,  contraction,  substitution)  based  on
proof-nets  for  the  multiplicative  exponential  fragment  of
Linear  Logic [15].   The  proof  in [31]
consists  of two  main  steps: first  prove  that the  modified
calculus $\lambda_{{\tt blxr}}$ has the PSN property (this is a
long proof  although it is  made easier by  adapting Lengrand's
techniques [23]),    then    prove   that    any
$\lm$-reduction   step  can   be  simulated   by   a  non-empty
$\lambda_{{\tt  blxr}}$-reduction   sequence. In this section we
also give an alternative proof of PSN
for the $\lm$-calculus.

§.§ Types

Types are built over a countable set of atomic symbols
(base types) and the type constructors $\>$ (for functional types)
and $\cap$ (for intersection types).
An environment $\Gam$  is a
partial function from variables to types.  We denote by
$\dom(\Gam)$ the domain of $\Gam$.
environments $\Gam$ and $\Del$ are said to be compatible iff
for all
$x \in \dom(\Gam) \cap
\dom(\Del)$
we have $\Gam(x)  = \Del(x)$.  We denote the
union  of  compatible contexts  by  $\Gam  \uplus  \Del$.  Thus  for
example $(x:A, y:B) \uplus (x:A, z:C) =$ $(x:A,$ $y:B,$ $z:C)$.

Typing  judgements have the form  $\Gam \vdash
t:A$ where $t$ is  a term, $A$ is a type and  $\Gam$ is an
environment. Derivations of typing  judgements
in a certain type discipline system are obtained by application of
the typing rules of the system. We consider several systems.

The  additive  simply  type  system  for
$\l$-terms  (resp. for  $\mterms$-terms), written $\saddl$
(resp. $\saddls$),  is  given  by the
rules , , and
(resp.        ,
,          ,          and
) in <ref>.

\[<EMAIL_ADDRESS>\hline
\irule{}
{\mathsmall{\Gam, x:A \vd x:A}}  \mathsmall{(\aaxiom)}  &
\irule{\mathsmall{\Gam \vd  t:A \> B} \sep
\mathsmall{\Gam \vd u:A}}
{\mathsmall{\Gam \vd  t\;u :B}}   \mathsmall{(\aapp)}  \\[.4cm]
\irule{\mathsmall{\Gam, x:A \vd t:B}}
{\mathsmall{\Gam \vd \l x. t: A\> B}}   \mathsmall{(\aabs)}  &
\irule{\mathsmall{\Gam \vd u:B \sep \Gam, x:B \vd t:A }}
{\mathsmall{\Gam  \vd t[x/u]:A}}  \mathsmall{(\asubstr)} \\
\hline
\end{array} \]

System $\saddl$ for $\l$-Terms and System  $\saddls$ for $\mterms$-Terms

The multiplicative simple type system  for
$\l$-terms  (resp. for $\mterms$-terms), written $\smultl$ (resp. $\smultls$), is given by the
rules , , and
(resp. , ,
, and )
in <ref>.

\[<EMAIL_ADDRESS>\hline
\irule{}
{\mathsmall{x:A \vd x:A}}   \mathsmall{(\maxiom)}   &
\irule{\mathsmall{\Gam \vd  t:A \> B \sep  \Del \vd u:A}}
{\mathsmall{\Gam \uplus \Del \vd  t\;u:B}}
\mathsmall{(\mapp)} \\[.4cm]
\irule{\mathsmall{\Gam  \vd t:B}}
{\mathsmall{\Gam \setminus \{ x:A\}  \vd \l x. t: A\> B}}  \mathsmall{(\mabs)} \sep &
\irule{\mathsmall{\Gam \vd u:B \sep \Del \vd t:A}}
{\mathsmall{\Gam \uplus ( \Del \setminus \{ x:B \} ) \vd t[x/u]:A}} \mathsmall{(\msubstr)}  \\
\hline
\end{array} \]

System $\smultl$ for $\l$-Terms and System  $\smultls$ for $\mterms$-Terms

Let $t$ be a $\mterms$-term. Then
$\Gam \vd_{\saddls} t:A$
iff  $\Gam \cap \fv(t) \vd_{\smultls} t:A$. Moreover,
if $t$ is a  $\l$-term, then $\Gam \vd_{\saddl} t:A$
iff  $\Gam \cap \fv(t) \vd_{\smultl} t:A$.

For the intersection type systems,
we also consider the additional rules in <ref>.

\[ \begin{array}{|cccc|}
\hline
\irule{\mathsmall{\Gam \vd t:A \sep \Gam \vd t:B}}
{\mathsmall{\Gam \vd t: A \cap  B}} & \mathsmall{(\ini)} &
\irule{\mathsmall{\Gam \vd t: A_1 \cap  A_2}}
{\mathsmall{\Gam \vd t:A_i}} & \mathsmall{(\ine)} \\
\hline
\end{array} \]

Additional Rules for Intersection Types

The additive intersection type system for $\l$-terms
(resp. for $\mterms$-terms), written $\addl$ (resp. $\addls$)
and  given in <ref>, is
obtained by adding the rules $\ini$ and $\ine$ in <ref> to those of $\saddl$
(resp. $\saddls$) in <ref>.

\[ \begin{array}{|cccc|}
\hline
\irule{}
{\Gam, x:A \vd x:A} &  (\aaxiom)  &
\irule{\Gam \vd u:B \sep \Gam, x:B \vd t:A }
{\Gam  \vd t[x/u]:A} & (\asubstr)   \\ &&&\\
\irule{\Gam \vd  t:A \> B \sep
\Gam \vd u:A}
{\Gam \vd  t\;u:B} &  (\aapp) &
\irule{\Gam, x:A \vd t:B}
{\Gam \vd \l x. t: A\> B} &  (\aabs)  \\ &&&\\
\irule{\Gam \vd t:A \sep \Gam \vd t:B}
{\Gam \vd t: A \cap  B} & (\ini) &
\irule{\Gam \vd t: A_1 \cap  A_2}
{\Gam \vd t:A_i} & (\ine) \\
\hline
\end{array} \]

System $\addl$ for $\l$-Terms and
System $\addls$ for  $\mterms$-terms

The multiplicative intersection type system for $\l$-terms
(resp. for $\mterms$-terms), written $\multl$ (resp. $\multls$)
and given in <ref>, is
obtained by adding the rules $\ini$ and $\ine$ in <ref> to those of $\saddl$
(resp. $\saddls$) in <ref>.
For technical reasons we specify  rule $\mabs$ (resp. $\msubstr$)
by using two different
instances  $\mabsi$ and $\mabsii$ (resp. $\msubsi$ and $\msubsii$).

\[ \begin{array}{|cccc|}
\hline
\irule{}
{x:A \vd x:A} &  (\maxiom)  &
\irule{\Gam \vd  t:A \> B \sep
\Del \vd u:A}
{\Gam \uplus \Del \vd  t\;u:B} &  (\mapp) \\ & & & \\
\irule{\Gam, x:A \vd t:B}
{\Gam \vd \l x. t: A\> B} &  (\mabsi) &
\irule{\Gam \vd t:B\ \mbox{ and } x \notin \Gam}
{\Gam \vd \l x. t: A\> B} & (\mabsii) \\  & & & \\
\irule{\Gam \vd u:B \sep
\Del, x:B \vd t:A }
{\Gam \uplus \Del \vd t[x/u]:A} &(\msubsi)  &
\irule{\Gam \vd u:B \sep
\Del \vd t:A \mbox{ and }\sep x \notin \Del}
{\Gam \uplus \Del \vd t[x/u]:A}  & (\msubsii)  \\& & & \\
\irule{\Gam \vd t:A \sep \Gam \vd t:B}
{\Gam \vd t: A \cap  B} & (\ini) &
\irule{\Gam \vd t: A_1 \cap  A_2}
{\Gam \vd t:A_i} & (\ine) \\
\hline
\end{array} \]

System $\multl$ for  $\l$-terms
and System $\multls$  for   $\mterms$-terms

A term $t$ is said to be typable  in system $\TST$,
written  $\Gam \vd_\TST t:A$ iff
there is $\Gam$ and $A$ s.t. the judgement $\Gam \vd t:A$ is derivable
from the set of typing rules of system $\TST$.

Remark that for any  $\l$-term  $t$
we have $\Gam \vd_{\addl} t:A$  iff
$\Gam \vd_{\addls} t:A$
and $\Gam \vd_{\multl} t:A$  iff
$\Gam \vd_{\multls} t:A$.

The relation $\ll$ on types is defined by the following axioms
and rules

* $A \ll A$

* $A \cap B \ll A$

* $A \cap  B \ll B$

* $A \ll B\ \&\  B \ll C$ implies $A \ll C$

* $A \ll B\ \&\  A \ll C$ implies $A \ll B \cap  C$

We use  $\un{n}$ for  $\set{1 \ldots n}$  and $\capp{n}  A_i$ for
$A_1 \cap \ldots  \cap A_n$. The following property  can be shown
by induction on the definition of $\ll$.

Let $\capp{n} A_i \ll \capp{m} B_j$, where none of the
$A_i$ and $B_j$ is an intersection type.  Then
for each $B_j$ there is $A_i$ s.t. $B_j = A_i$.

By an induction on the definition of $\capp{n} A_i \ll \capp{m}
B_j$. Let $\capp{p} C_k$ be some
type where no $C_k$ is an intersection type.

Case $\capp{n} A_i \ll \capp{n} A_i$. Trivial.

Case $\capp{n} A_i \cap \capp{p} C_k \ll \capp{n} A_i$. Trivial.

Case $\capp{p} C_k \cap \capp{n} A_i \ll \capp{n} A_i$. Trivial.

Case  $\capp{n} A_i  \ll  \capp{p} C_k,  \capp{p} C_k  \ll
\capp{m}  B_j$. Applying    once,  we have  for  each $B_j$
there is $C_k$  s.t. $B_j = C_k$. Applying    again, we have
for each $C_k$ there is $A_i$ s.t. $C_k = A_i$.

Case $\capp{n} A_i \ll  B_1 \cap \ldots \cap B_k, \capp{n}
A_i \ll  B_{k+1} \cap \ldots  \cap B_m$.
Applying the
to $\capp{n} A_i \ll  B_1 \cap \ldots \cap B_k$
and $\capp{n}
A_i \ll  B_{k+1} \cap \ldots  \cap B_m$
we have for each $B_j, 1 \leq j \leq k$ there is $A_i$ s.t. $B_j =
A_i$ and for each $B_j, k+1 \leq j \leq
m$ there is $A_i$ s.t. $B_j = A_i$.

§.§ Basic Properties of the Type Systems

We show some basic properties of the type systems.

If $\Gam \vd_\TST  t:A$ and $A \ll B$, then
$\Gam \vd_\TST t:B$ for all $\TST \in \{ \addl, \addls,
\multl, \multls\}$.

Let $\Gam \vd_\TST  t:A$. We
reason by induction on the definition of $A \ll B$.

Case $A=B, A \ll A$. Trivial.

Case $A=B \cap C \ll B$. Use $\ine$.

Case $A=C \cap B \ll B$. Use $\ine$.

Case $A \ll C, C \ll B$. Use  once to get $\Gam \vd_\TST  t:C$ and a second time to get $\Gam \vd_\TST  t:B$.

Case $A \ll  B_1, A \ll B_2, B = B_1  \cap B_2$. Use
twice to  get $\Gam  \vd_\TST  t:B_1$ and  $\Gam \vd_\TST  t:B_2$  and then
apply $\ini$.

The proofs of the following lemmas can be found in <ref>.

[Environments are Stable by $\ll$]
If $\Gam, x:B \vd_\TST  t:A$ and $C \ll B$, then $ \Gam, x:C
\vd_\TST t:A$ for all $\TST \in \{ \addl, \addls,
\multl, \multls\}$.

If $\Del \cap \fv(t) = \emptyset$,
$\Gam \vd_{\addls} t:A$ iff $\Gam, \Del \vd_{\addls} t:A$.

[Additive  Generation Lemma]lemmaadditivegenerationlemma
Let $\TST$ be an additive system. Then

* $\Gam \vd_\TST x:A$ iff there is $x:B \in \Gam$ and $B \ll A$.

* $\Gam \vd_\TST t\ u:A$ iff  there exist $A_i, B_i, i \in \un{n}$ s.t.
$\capp{n} A_i \ll A$ and $\Gam \vd_\TST t: B_i \> A_i$ and
$\Gam \vd_\TST u:B_i$.

* $\Gam \vd_\TST t[x/u]:A$ iff there exist $A_i, B_i, i \in \un{n}$ s.t.
$\capp{n} A_i \ll A$ and  $\forall i \in
\un{n}$ $\Gam \vd_\TST u:B_i$ and $\Gam, x:B_i \vd_\TST t: A_i$.

*   $\Gam \vd_\TST\l x. t:A$ iff   there exist $A_i, B_i, i \in
\un{n}$ s.t. $\capp{n} (A_i \> B_i) \ll A$
and   $\forall i \in
\un{n}$   $\Gam, x:A_i \vd_\TST t:B_i$.

*  $\Gam \vd_\TST\l x. t:B \> C$ iff   $\Gam, x:B \vd_\TST t:C$.

[Multiplicative Generation Lemma]lemmamultiplicativegenerationlemma
Let $\TST$ be a multiplicative system. Then

*  $\Gam \vd_\TST x:A$ iff $\Gam = x:B$ and $B \ll A$.

*  $\Gam \vd_\TST t\ u:A$ iff $\Gam = \Gam_1 \uplus \Gam_2$,
where $\Gam_1 = \fv(t)$ and $\Gam_2 = \fv(u)$
and there exist $A_i, B_i, i \in \un{n}$ s.t.
$\capp{n} A_i \ll A$ and  $\forall i \in \un{n}$, $\Gam_1 \vd_\TST t: B_i \> A_i$ and
$\Gam_2 \vd_\TST u:B_i$.

*  $\Gam \vd_\TST t[x/u]:A$ iff $\Gam = \Gam_1 \uplus \Gam_2$,
where $\Gam_1 = \fv(t) \setminus \set{x}$ and $\Gam_2 = \fv(u)$
and there exist $A_i, B_i, i \in \un{n}$ s.t.
$\capp{n} A_i \ll A$ and  $\forall i \in
\un{n}$, $\Gam_2 \vd_\TST u:B_i$ and
either $x \notin \fv(t)\ \&\ \Gam_1 \vd_\TST t: A_i$ or
$x \in \fv(t)\ \&\ \Gam_1, x:B_i \vd_\TST t: A_i$.

$\Gam \vd_\TST \l x. t:A$ iff  $\Gam = \fv(\l x.t)$ and there exist $A_i, B_i, i \in
\un{n}$ s.t. $\capp{n} (A_i \> B_i) \ll A$
and l $\forall i \in
\un{n}$, either $x \notin \fv(t)\ \&\ \Gam \vd_\TST t:B_i$ or
$x \in \fv(t)\ \&\ \Gam, x:A_i \vd_\TST t:B_i$.

*  $\Gam \vd_\TST \l x. t:B \> C$ iff $\Gam = \fv(\l x.t)$ and  $\Gam, x:B \vd_\TST
t:C$ or $\Gam \vd_\TST t:C$.

We can now state  a
correspondence between the multiplicative
and additive systems with intersection types.

Let $t$ be a $\mterms$-term. Then
$\Gam \vd_{\addls} t:A$
iff  $\Gam \cap \fv(t) \vd_{\multls} t:A$. Moreover,
if $t$ is a  $\l$-term, then $\Gam \vd_{\addl} t:A$
iff  $\Gam \cap \fv(t) \vd_{\multl} t:A$.

The right to left implication is by induction on $t$ using both
generation  lemmas and <ref>.   The left  to
right implication  is by induction on $t$  using the generation

Since  systems $\saddl$ and $\smultl$ (resp. $\saddls$  and $\smultls$)
type the same sets of $\l$-terms (resp. $\mterms$-terms) (<ref>), and
systems $\addl$ and $\multl$ (resp. $\addls$  and $\multls$) type
the same sets of  $\l$-terms (resp. $\mterms$-terms) (<ref>), then, from now on,
simply typable  $\l$-term means typable in
$\saddl$ or  $\smultl$, intersection  typable  $\l$-term means typable in
$\addl$ or  $\multl$,
simply typable  $\mterms$-term means typable in
$\saddls$ or $\smultls$ and
intersection  typable $\mterms$-term means typable in
$\addls$ or  $\multls$.

§.§ Simply typable  $\mterms$-terms are $\lm$-strongly normalising

The goal of this section is to show that simply typable $\mterms$-terms
are $\lm$-strongly normalising. This result turns out to be a
consequence of strong normalisation of simply typable $\l$-terms
in the partial  $\lpar$-calculus; a result
which can be shown using a simple  arithmetical proof [36, 11].
This proof is constructive as it only uses induction and
intuitionistic reasoning.

Let  $t,u$ be  a simply typable  $\l$-terms.
If $t,u\in \SN{\lpar}$, then $t\isubs{x}{u}
\in \SN{\lpar}$.

By  induction on  $\langle \type(u),   \eta_{\lpar}(t),  |t|
\rangle$, where $|t|$ is the number of constructors in $t$. We treat the interesting cases.

* If  $t =   \lambda  y.  v$,  then  $v\isubs{x}{u}  \in
\SN{\lpar}$  by  the     and   thus $t\isubs{x}{u}    = \l
x.      v\isubs{x}{u}    \in   \SN{\lpar}$.

* $t  = y  \ov{v_n}$
with $x \neq  y$. The  gives
$v_i\isubs{x}{u} \in \SN{\lpar}$
since $\eta_{\lpar}(v_i)$ decreases  and
$|v_i|$ strictly decreases. Then we conclude

* $t =x $. Then $x \isubs{x}{u} =u\in \SN{\lpar}$ by the hypothesis.

* $t  =  x  v   \ov{v_n}$. The
gives  $V = v \isubs{x}{u}$ and  $V_i =
v_i\isubs{x}{u}$ in $\SN{\lpar}$.
To show $t\isubs{x}{u}=u V \ov{V_n} \in \SN{\lpar}$
it is sufficient to show that all its reducts are
in $\SN{\lpar}$. We reason by induction on
$\eta_{\lpar}(u) + \eta_{\lpar}(V) + \Sigma_{i \in 1
\ldots n}\ \eta_{\lpar}(V_i)$.

* If  the reduction takes place  in $u$,
$V$ or $V_i$,  then the   property holds  by  the
* Suppose $u = \l y . U$ and $(\l y  . U)\ V\ \ov{V_n} \Rew{\BGc}
U\   \ov{V_n}$.   We  write     $U\    \ov{V_n}$  as      $(z\
\ov{V_n})\isubs{z}{U}$, where $z$ is a fresh variable.  Since
every  $V_i   \in  \SN{\lpar}$,   then  $z\   \ov{V_n}    \in
\SN{\lpar}$.  Also, $u    \in  \SN{\lpar}$   implies $U   \in
\SN{\lpar}$.  Thus,   $\type(U)   < \type(u)$   implies   $(z\
\ov{V_n}) \isubs{z}{U} \in \SN{\lpar}$ by the
* Suppose  $u = \l y . C\cwc{y}$ and $(\l y . C\cwc{y})\ V\ \ov{V_n}
\Rew{\bp} (\l y. C\cwc{V})\ V\  \ov{V_n}$.
We write $\l y. C\cwc{V}$ as $(\l y. C\cwc{z})\isubs{z}{V}$, where
$z$ is a fresh variable. Since $u \in \SN{\lpar}$, then
$C\cwc{y} \in \SN{\lpar}$. The change of free occurrences of
variables preserve normalisation so that
$C\cwc{z} \in \SN{\lpar}$ and thus $\l y. C\cwc{z} \in \SN{\lpar}$.
We also  have $\type(V) = \type(v)
< \type(u)$     so     that we get
$(\l y. C\cwc{z})\isubs{z}{V} \in  \SN{\lpar}$ by the

* $t =
(\l y. s) v  \ov{v_n}$.  The   gives $S = s\isubs{x}{u}$
and    $V = v    \isubs{x}{u}$   and $V_i =  v_i
\isubs{x}{u}$ are in $\SN{\lpar}$. These terms  are  also  typable.
To show
$t\isubs{x}{u}        =   (\l y.       S)  V  \ov{V_n} \in \SN{\lpar}$
it is sufficient to show that all its reducts are in $\SN{\lpar}$.
We reason by induction on
$\eta_{\lpar}(S) + \eta_{\lpar}(V) + \Sigma_{i \in 1
\ldots n}\ \eta_{\lpar}(V_i)$.

* If  the reduction takes place  in $S$,
$V$ or $V_i$,  then the   property holds  by  the

* Suppose $(\l y  . S)\ V\ \ov{V_n} \Rew{\BGc}
S\   \ov{V_n}$.   We  write     $S\    \ov{V_n}$  as      $(s\
\ov{v_n})\isubs{x}{u}$.  Since
$(\l y. s)\ v\ \ov{v_i} \Rew{\lpar} s\ \ov{v_n}$, then
$\eta_{\lpar}(s\ \ov{v_n}) < \eta_{\lpar}((\l y. s)\ v\ \ov{v_n})$
and thus we conclude
$S\   \ov{V_n}    \in
\SN{\lpar}$ by the
* Suppose  $u = \l y . C\cwc{y}$ and $(\l y . C\cwc{y})\ V\ \ov{V_n}
\Rew{\bp} (\l y. C\cwc{V})\ V\  \ov{V_n}$.
We write $\l y. C\cwc{V}$ as $(\l y. C\cwc{v})\isubs{x}{u}$.
Since $(\l y . C\cwc{y})\ v\ \ov{v_n}
\Rew{\bp} (\l y. C\cwc{v})\ v\  \ov{v_n}$, then
$\eta_{\lpar}((\l y. C\cwc{v})\ v\  \ov{v_n}) <
\eta_{\lpar}((\l y. C\cwc{v})\ v\  \ov{v_n})$ and thus
we conclude  $(\l y. C\cwc{V})\ V\  \ov{V_n} \in \SN{\lpar}$
by the

Let $t$ be a $\l$-term.
If $t$ is  simply typable,  then $t\in \SN{\lpar}$.

By induction  on the structure  of $t$. The cases $t=x$  and $t=\l x. u$
are  straightforward.   If $t  = u v$,   then write   $t=(z\
v)\isubs{z}{u}$. By  the  $u,v \in  \SN{\lpar}$  and  thus <ref>   gives  $t  \in  \SN{\lpar}$.

Let $t$ be  a $\mterms$-term.
If $t$ is simply typable,   then $t\in \SN{\lm}$.

Take  $t$ typable  in  $\saddls$. Then,   $\lmpar{t}$ (defined in <ref>) is a
$\l$-term. One shows by induction on $t$ that
$\lmpar{t}$ is typable in $\saddl$,   and that $\lmpar{t} \Rewplus{\B} t$.
Since $\lmpar{t}$ is a simply typable  $\l$-term, then
by <ref>
$\lmpar{t} \in \SN{\lpar}$ and by <ref>
$\lmpar{t} \in \SN{\lm}$ . Thus $t$ is also in $\SN{\lm}$.

This same result admits
an alternativa proof.

Let $t$ be  a $\mterms$-term.
If $t$ is simply typable,   then $t\in \SN{\lm}$.

Let $\Gam \vd_{\smultls}  t:A$.
It is not difficult
to  show that  $\tra{t}$ is also typable in
$\smultls$, by induction on $t$. Then $\tra{t} \in \SN{\les}$ by [20].
Now, suppose  $t \notin \SN{\lm}$. Then given an infinite
$\lm$-reduction sequence starting at $t$
we can construct, by <ref>,
an infinite $\les$-reduction sequence
starting at $\tra{t}$. This leads to a contradiction with $\tra{t} \in \SN{\les}$.
Thus  $t \in \SN{\lm}$.

§.§ Intersection Typable  $\mterms$-terms are $\lm$-strongly normalising

The goal of this section is to show that intersection
typable $\mterms$-terms
are $\lm$-strongly normalising.
We make use of the functions $\lmpar{\_}$
and $\tra{\_}$, respectively
defined in <ref> and <ref>.

Let $t$ be  a $\mterms$-term.
Then $t$ is typable in $\multls$ if and only if
$\lmpar{t}$ is typable in $\multl$.

By induction on the typing derivation of

Let $t$ be  a $\mterms$-term.
If $t$ is intersection  typable,  then $t\in \SN{\les}$.

Let $t$ be intersection  typable,
so that in particular
$t$ is typable in $\multls$.
<Ref> gives
$\lmpar{t} $ typable in $\multl$
and <ref> gives
$\lmpar{t} $ typable in $\addl$.
Thus $\lmpar{t} $ is $\beta$-strongly normalising [34].
As a consequence, $\lmpar{t}  \in \SN{\les}$
by PSN [20].
Since $\lmpar{t} \Rewn{\les} t$,
then we  conclude also $t \in \SN{\les}$.

Let $t$ be  a $\mterms$-term.
Then $t$ is typable in $\multls$ if and only if
$\tra{t}$ is typable in $\multls$.

By induction on the typing derivation of

Let $t$ be  a $\mterms$-term.
If $t$ is intersection  typable,  then $t\in \SN{\lm}$.

Let $t$ be intersection  typable,
so that in particular
$t$ is typable in $\multls$.
By <ref> also
$\tra{t}$ is  typable in $\multls$.
Thus, $\tra{t} \in \SN{\les}$ by <ref>.
Suppose $t \notin \SN{\lm}$, so that there is
an infinite
$\lm$-reduction sequence starting at $t$,
which projects,
by <ref>, to an infinite $\les$-reduction
sequence starting at $\tra{t}$. This leads to a contradiction
with $\tra{t} \in \SN{\les}$.
Thus we conclude $t \in \SN{\lm}$ as required.

§.§ $\lm$-strongly normalising terms are intersection typable  $\mterms$-terms

We now complete the picture  by showing that the intersection
type discipline for $\mterms$-terms gives a characterisation of
$\lm$-strongly normalising terms. To do this, we use the
translation $\lmpar{\_}$ introduced in <ref>
to relate $\mterms$-terms to $\l$-terms.

Let $t,u$ be  $\mterms$-terms.
Then $\lmpar{t}\isubs{x}{\lmpar{u}} = \lmpar{t\isubs{x}{u}}$.

By induction on $t$.

* If $t = y$ and $y = x$ then $x\isubs{x}{\lmpar{u}} = \lmpar{u} = \lmpar{x\isubs{x}{u}}$. If $y \neq x$ then $y\isubs{x}{\lmpar{u}} = y = \lmpar{y\isubs{x}{u}}$.

* If $t = \l y.t'$ then $\lmpar{t}\isubs{x}{\lmpar{u}} = (\l y.\lmpar{t'}\isubs{x}{\lmpar{u}}) = (\l y.\lmpar{t'\isubs{x}{u}})$ by the . Then, $(\l y.\lmpar{t'\isubs{x}{u}}) = \lmpar{\l y.t'\isubs{x}{u}} = \lmpar{(\l y.t')\isubs{x}{u}}$.

* If $t = u\ v$ then the proof is similar.

* If $t  = t_1[y/t_2]$  then  $\lmpar{t}\isubs{x}{\lmpar{u}} =
((\l  y.\lmpar{t_1})\lmpar{t_2})\isubs{x}{\lmpar{u}}  =$$(\l                           y.\lmpar{t_1}\isubs{x}{\lmpar{u}})\
(\lmpar{t_2}\isubs{x}{\lmpar{u}})$. Applying   twice we get

\begin{eqnarray*}
&&(\l y.\lmpar{t_1}\isubs{x}{\lmpar{u}})\ (\lmpar{t_2}\isubs{x}{\lmpar{u}})\\
&=&(\l y.\lmpar{t_1\isubs{x}{u}})\ \lmpar{t_2\isubs{x}{u}}\\
\end{eqnarray*}

Let $t$ be a $\mterms$-term.
If $\lmpar{t} \Rew{\beta} t'$, then  $\exists\ u$ s.t.
$t  \Rewplus{\lm} u$ and $t' = \lmpar{u}$.

By induction on the reduction step $\lmpar{t}
\Rew{\beta} t'$.

If the step is external, then we have two possibilites.

* If $\lmpar{(\l x. t_1)\ t_2} = (\l x. \lmpar{t_1})\ \lmpar{t_2}
\Rew{\beta} \lmpar{t_1}\isubs{x}{\lmpar{t_2}}$, then
$(\l x. t_1)\ t_2 \Rew{\B} t_1[x/t_2] \Rewplus{\lm}
t_1\isubs{x}{t_2}$ by <ref>.
We conclude by <ref>.

* If $\lmpar{t_1[x/t_2]} =  (\l x. \lmpar{t_1})\ \lmpar{t_2}
\Rew{\beta}\lmpar{t_1}\isubs{x}{\lmpar{t_2}}$, then
$t_1[x/t_2] \Rewplus{\lm}
t_1\isubs{x}{t_2}$ by <ref>.
We conclude again by <ref>.

If the step is internal, then we reason by cases.

* If $\lmpar{t_1\ t_2} = \lmpar{t_1}\ \lmpar{t_2} \Rew{\beta}
t'_1\ \lmpar{t_2}$, then $t_1 \Rewplus{\lm} u_1$ and $t'_1=
\lmpar{u_1}$ by the   so that
$ t_1\ t_2 \Rewplus{\lm} u_1\ t_2$
and $t'_1\ \lmpar{t_2} = \lmpar{u_1\ t_2}$.

* If $\lmpar{t_1\ t_2} = \lmpar{t_1}\ \lmpar{t_2} \Rew{\beta}
\lmpar{t'_1}\ t'_2$, then this case is similar to the previous one.

* If $\lmpar{\l x. t_1} = \l x. \lmpar{t_1}\Rew{\beta}\l
x. t'_1$, then $t_1 \Rewplus{\lm} u_1$ and $t'_1=
\lmpar{u_1}$ by the   so that
$\l x. t_1 \Rewplus{\lm} \l x. u_1$
and $\l x. t'_1 = \lmpar{\l x. u_1}$.

* If $\lmpar{t_1[x/t_2]} =  (\l x. \lmpar{t_1})\ \lmpar{t_2}
\Rew{\beta} (\l x. t'_1)\ \lmpar{t_2}$, then
$t_1 \Rewplus{\lm} u_1$ and $t'_1=
\lmpar{u_1}$ by the   so that
$t_1[x/t_2]  \Rewplus{\lm} u_1[x/t_2]$
and $(\l x. t'_1)\ \lmpar{t_2} = \lmpar{u_1[x/t_2]}$.

* If $\lmpar{t_1[x/t_2]} =  (\l x. \lmpar{t_1})\ \lmpar{t_2}
\Rew{\beta} (\l x. \lmpar{t_1})\ t'_2$, then this case is
similar to the previous one.

Let $t$ be a $\mterms$-term.
If $t \in \SN{\lm}$, then $t$ is an intersection typable  $\mterms$-term.

Let $t \in  \SN{\lm}$.
Suppose $\lmpar{t} \notin \SN{\beta}$.  Then, there is an infinite
$\beta$-reduction  sequence starting  at $\lmpar{t}$,
which can be projected, by <ref>, to an infinite
$\lm$-reduction sequence starting at $t$.  Thus $t
\notin  \SN{\lm}$, which leads  to a

Therefore $\lmpar{t}\in \SN{\beta}$, so that $\lmpar{t}$ is
typable in $\addl$ by [34].  By <ref>
$\lmpar{t}$ is also typable in $\multls$,
and by <ref> $t$ is typable in

§.§ PSN

We now  show  the PSN property
stating that  $\lm$-reduction preserves  $\beta$-strong
normalisation. A proof of this result
already exists [31]. We reprove this property in a more simple way.

Let $t$ be a $\l$-term.
If $t \in \SN{\beta}$,  then $t\in \SN{\lm}$.

If $t \in \SN{\beta}$, then $t$ is typable
in $\addl$ by [34], so that
$t$ is also typable
in $\addls$ (which contains $\addl$).
We conclude
$t \in \SN{\lm}$ by <ref>.

We finally conclude with the following equivalences:

Let $t$ be a $\mterms$-term. Then  $t$ is typable in $\addls$ iff
$t$ is typable in $\multls$ iff
$t \in \SN{\lm}$ iff $t \in \SN{\ldef}$. Furthermore,
let $t$ be a  $\l$-term. Then  $t$ is typable in $\addl$ iff
$t$ is typable in $\multl$ iff
$t \in \SN{\lm}$ iff $t \in \SN{\lpar}$ iff $t \in \SN{\beta}$.

The statement $t$ is typable in $\addls$ iff $t$ is typable in
$\multls$ holds by <ref>.  The statement
$t$ intersection typable iff $t\in \SN{\lm}$ holds
by <ref> and <ref>.
The statement $t \in \SN{\lm}$ iff $t \in \SN{\ldef}$ holds
by <ref>.  The statement $t$ is typable in $\addl$
iff $t$ is typable in $\multl$ holds
by <ref>.  The statement $t$ is typable in
$\addl$ iff $t \in \SN{\beta}$ holds by [34].  The
statement $t \in \SN{\lm}$ iff $t \in \SN{\lpar}$ holds
by <ref>.  <Ref> gives $t \in \SN{\beta}$ implies $t
\in \SN{\lm}$. And $t \in \SN{\lm}$ implies $t \in \SN{\beta}$ is a
consequence of <ref>.

§ RELATING PARTIAL SUBSTITUTIONS TO GRAPHICAL FORMALISMS

§.§ MELL Proof-nets

Calculi  with explicit substitutions
enjoy a nice relation with the multiplicative exponential fragment
of linear logic (MELL). This is done by interpreting terms into
a graphical formalism which represent
MELL proofs in natural deduction style.
In order  to obtain this interpretation,  one first  defines a
(simply)  typed version  of the  term calculus.    The translation
from  $\mterms$-terms to  proof-nets gives  a simulation  of  the reduction
rules   for  explicit  substitutions   via  cut   elimination  in
proof-nets.    As  an   immediate  consequence   of  this
simulation, one  proves that a  simply typed version of  the term
calculus is strongly normalizing.  Also, an important property of
the  simulation is  that each  step in  the calculus  with  ES is
simulated  by a  constant number  of steps  in proof-nets:
this  shows that  the two  systems  are very  close, unlike  what
happens  when simulating  the  $\l$-calculus. This  gives also  a
powerful    tool   to    reason   about    the    complexity   of

We apply this idea to the $\lm$-calculus  by
using previous work based on an interpretation of $\les$-terms into
MELL proof-nets [20] and our translation in <ref>. We thus

Let $t$ be a $\mterms$-term which is simply typable.
Then $t$ is in particular typable in  the
multiplicative simple typed system $\smultls$
given in <ref>. Then the  translation
of $t$ into a MELL proof-net can be  given by
$\pntra{t} = \pnlestra{\tra{t}}$, where $\tra{\_}$ is the
translation from $\lm$ to $\les$ introduced in <ref>,
while  $\pnlestra{\_}$ is the translation from $\les$ to MELL
proof-nets given in [20].
Call $R/E$ the strongly normalising reduction relation on MELL proof-nets. Then:

Let $t$ be a $\mterms$-term.
If $t$ is typable in $\smultls$
and $t \Rew{\lm} t'$, then $\pntra{t} \Rewplus{R/E} {\cal C}[\pntra{t'}]$, where
${\cal C}[\pntra{t'}]$ denotes a proof-net
containing $\pntra{t'}$ as a sub proof-net.

Let $t \Rew{\lm} t'$.
<Ref> gives $\tra{t} \Rewplus{\les}
\tra{t'}$.
Moreover, by a simple inspection of the proof of this proposition we
know that there is  at least one $\{\B, \Var, \Gc\}$-step in the reduction
sequence $\tra{t} \Rewplus{\les}
\tra{t'}$. This together with Theorem 8.2 in [20] gives
$\pntra{t} = \pnlestra{\tra{t}} \Rewplus{R/E} {\cal
C}[\pnlestra{\tra{t'}}]= {\cal C}[\pntra{t'}]$.

If $t$ is typable in $\smultls$, then $t\in \SN{\lm}$.

As $R/E$ is strongly normalising, we conclude $t \in \SN{\lm}$ using <ref>.

§.§ Local bigraphs

Milner,    Leifer,     and    Jensen's    bigraphical    reactive
systems [27, 25, 19] have been proposed  as a framework for modelling  the mobility of
distributed  agents able  to  manipulate their  own linkages  and
nested  locations. Milner  has  presented  an
encoding  of  $\lm$ as  a  bigraphical
reactive system $\lamBig$ as a means to study confluence in bigraphs [28].
This  encoding  may  also  be  understood  as  a  formalism  with
partial  substitutions.

The $\lm$-calculus   is  close   to  $\lamBig$  both
statically  and dynamically;  $\alpha$-equivalent terms  have the
same  encoding  and   one-step reduction  in  the  former matches
one-step reaction in  the latter. Thus,  any properties proved for
$\lm$ hold for the image of the encoding in $\lamBig$.

There is a close operational correspondence between $\lm$ and $\lamBig$:

Let $t$ be a $\mterms$-term.  Then $t \Rew{\lm} t'$
iff the
encoding of $t$ in $\lamBig$ can react in one step to  the encoding of $t'$ in $\lamBig$.

Thus, the image $\lamBig^e$ of the encoding is closed under reaction.
We  can  reason  about   reaction  in  $\lamBig^e$  by  considering
reduction of $\lm$ terms without   metavariables:

$\lamBig^e$ is confluent and satisfies PSN. Encodings of intersection typed terms are strongly normalising.

§ CONCLUSIONS

We  answer some  fundamental remaining questions  concerning the  adequacy of
Milner's $\l$-calculus with partial substitutions. In particular,
we  prove  that the  $\lm$-calculus  is  confluent  on terms  and
metaterms, that it  enjoys PSN, and that it allows a characterisation of $\lm$-strongly normalising
terms by using intersection type disciplines.

We relate $\lm$ to the  calculi with definitions $\lpar$ and $\ldef$,
thus obtaining a certain number of interesting results concerning
normalisation.   We also  relate the  $\lm$-calculus  to
classical calculi  with explicit  substitutions.  Thus,  the $\lm$-calculus
can be  understood as a concise and  simple language implementing
partial and ordinary substitution,  both in implicit and explicit
style at the same time.

Last but not least, we establish a clear
connection   between  simply   typed   $\lm$-calculus  and   MELL
proof-nets,  thus  injecting  again  a  graph  representation  to
$\mterms$-terms  which   were  inspired  from   bigraphical  reactive

In  related    work,     Bundgaard    and
Hildebrandt [6]  use  partial   substitution similar to   $\lm$   in  their extension of Higher-Order  Mobile  Embedded  Resources (Homer), a higher-order  process calculus. Partial substitution
is also used  in different frameworks such as  for example Ariola
and  Felleisen's [2]  call-by-need  lambda
calculus and   Ariola    and   Klop's [3]   cyclic

Grohmann  and  Miculan   have  modelled  the  call-by-name  and
call-by-value       $\lambda$-calculi       with      bigraphs
[16]  by adapting  Milner's  model. While
they concentrate on encodings  of $\l$-terms, the model is
still   based  on  $\lm$ and   reduction  matches   reaction
Therefore,   our  results   can   be  used   to  reason   about
normalisation properties  of encodings of  $\mterms$-terms in their

We are grateful to  V. van  Oostrom who
pointed out to us references to calculi with
partial notions of substitutions such
as $\lpar$ and $\ldef$.

[1]
Martín Abadi, Luca Cardelli, Pierre Louis Curien, and Jean-Jacques Lévy.
Explicit substitutions.
Journal of Functional Programming, 4(1):375–416, 1991.

[2]
Zena M. Ariola and Matthias Felleisen.
The call-by-need lambda calculus.
Journal of Functional Programming, 7(3):265–301, 1997.

[3]
Zena M. Ariola and Jan Willem Klop.
Lambda calculus with explicit recursion.
Information and Computation, 139(2):154–233, 1997.

[4]
Franz Baader, editor.
Term Rewriting and Applications, 18th International Conference,
RTA-07, volume 4533 of Lecture Notes in Computer Science.
Springer-Verlag, June 2007.

[5]
Zine-El-Abidine Benaissa, Daniel Briaud, Pierre Lescanne, and Jocelyne
$\lambda\upsilon$, a calculus of explicit substitutions which
preserves strong normalisation.
Journal of Functional Programming, 6(5):699–722, 1996.

[6]
Mikkel Bundgaard and Thomas T. Hildebrandt.
Bigraphical semantics of higher-order mobile embedded resources with
local names.
Electronic Notes in Theoretical Computer Science, 154(2):7–29,

[7]
Franz Baader and Tobias Nipkow.
Term Rewriting and All That.
Cambridge University Press, 1998.

[8]
Roel Bloo and Kristoffer Rose.
Preservation of strong normalization in named lambda calculi with
explicit substitution and garbage collection.
In Computer Science in the Netherlands (CSN), pages 62–72,

[9]
Mario Coppo and Mariangiola Dezani-Ciancaglini.
A new type assignment for lambda-terms.
Archiv für mathematische Logik und Grundlagenforschung,
(19):139–156, 1978.

[10]
Mario Coppo and Mariangiola Dezani-Ciancaglini.
An extension of the basic functionality theory for the
Notre-Dame Journal of Formal Logic, 4(21):685–693, 1980.

[11]
René David.
A short proof of the strong normalization of the simply typed lambda
Available as <http://www.lama.univ-savoie.fr/ david/>.

[12]
Nicolaas G. de Bruijn.
Generalizing Automath by Means of a Lambda-Typed Lambda
In Mathematical Logic and Theoretical Computer Science, number
106 in Lecture Notes in Pure and Applied Mathematics, pages 71–92, New York,
1987. Marcel Dekker.

[13]
René David and Bruno Guillaume.
A $\lambda$-calculus with explicit weakening and explicit
Mathematical Structures in Computer Science, 11:169–206, 2001.

[14]
Gilles Dowek, Thérèse Hardin, and Claude Kirchner.
Higher-order unification via explicit substitutions.
Information and Computation, 157:183–235, 2000.

[15]
Jean-Yves Girard.
Linear logic.
Theoretical Computer Science, 50(1):1–101, 1987.

[16]
Davide Grohmann and Marino Miculan.
Directed bigraphs.
Electronic Notes in Theoretical Computer Science, 173:121–137,

[17]
Gérad Huet.
Résolution d'équations dans les langages d'ordre $1,2,
\ldots, \omega$.
Thèse de doctorat d'état, Université Paris VII, 1976.

[18]
Jean-Pierre Jouannaud and Hélène Kirchner.
Completion of a set of rules modulo a set of equations.
SIAM Journal on Computing, 15(4):1155–1194, 1986.

[19]
Ole Høgh Jensen and Robin Milner.
Bigraphs and mobile processes (revised).
Technical Report UCAM-CL-TR-580, Computer Laboratory, University of
Cambridge, February 2004.

[20]
Delia Kesner.
The theory of calculi with explicit substitutions revisited.
In Jacques Duparc and Thomas Henzinger, editors, Proceedings of
the 16th Annual Conference of the European Association for Computer Science
Logic (CSL), volume 4646 of Lecture Notes in Computer Science, pages
238–252. Springer-Verlag, September 2007.

[21]
Kentaro Kikuchi.
Simple proofs of characterizing strong normalization for explicit
substitution calculi.
In Baader [4], pages 257–272.

[22]
Delia Kesner and Stéphane Lengrand.
Extending the explicit substitution paradigm.
In Jürgen Giesl, editor, 16th International Conference on
Rewriting Techniques and Applications (RTA), volume 3467 of Lecture
Notes in Computer Science, pages 407–422. Springer-Verlag, April 2005.

[23]
Stéphane Lengrand.
Induction principles as the foundation of the theory of
normalisation: Concepts and techniques.
Technical report, PPS laboratory, Université Paris 7, March 2005.
available at http://hal.ccsd.cnrs.fr/ccsd-00004358.

[24]
Stéphane Lengrand, Pierre Lescanne, Dan Dougherty, Mariangiola
Dezani-Ciancaglini, and Steffen van Bakel.
Intersection types for explicit substitutions.
Information and Computation, 189(1):17–42, 2004.

[25]
James J. Leifer and Robin Milner.
Deriving bisimulation congruences for reactive systems.
In Catuscia Palamidessi, editor, CONCUR, volume 1877 of Lecture Notes in Computer Science, pages 243–258. Springer, 2000.

[26]
Paul-André Melliès.
Typed $\lambda$-calculi with explicit substitutions may not
In Mariangiola Dezani-Ciancaglini and Gordon Plotkin, editors, Proceedings of the 2nd International Conference on Typed Lambda Calculus and
Applications (TLCA), volume 902 of Lecture Notes in Computer Science,
pages 328–334. Springer-Verlag, April 1995.

[27]
Robin Milner.
Computational flux.
In POPL '01: Proceedings of the 28th ACM SIGPLAN-SIGACT
symposium on Principles of programming languages, pages 220–221, New York,
NY, USA, 2001. ACM Press.

[28]
Robin Milner.
Local bigraphs and confluence: two conjectures.
In Roberto Amadio and Iain Phillips, editors, Proceedings of the
13th International Workshop on Expressiveness in Concurrency (EXPRESS
'06). Electronic Notes in Theoretical Computer Science, 2006.

[29]
César Muñoz.
Un calcul de substitutions pour la représentation de preuves
partielles en théorie de types.
PhD thesis, Université Paris 7, November 1997.

[30]
Robert. P. Nederpelt.
The fine-structure of lambda calculus.
Technical Report Computing Science Notes 92/07, Eindhoven University
of Technology, Department of Mathematics and Computer Science, 1992.

[31]
Shane Ó Conchúir.
Proving PSN by simulating non-local substitution with local
In Delia Kesner, Mark-Oliver Stehr, and Femke van Raamsdonk, editors,
Proceedings of the Third International Workshop on Higher-Order
Rewriting (HOR), pages 37–42, August 2006.

[32]
Shane Ó Conchúir.
${\Lambda_{\mathrm{sub}}}$ as an explicit substitution calculus.
Technical Report TR-2006-95, IT-Universitetet, København,
September 2006.

[33]
Frank Pfenning.
On a logical foundation for explicit substitutions.
In Baader [4], pages 257–272.

[34]
Garrell Pottinger.
A type assignment for the strongly normalizable $\lambda$-terms.
In To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus,
and Formalism, pages 561–577. Academic Press, New York, 1980.

[35]
Paula Severi and Erik Poll.
Pure type systems with definitions.
In Logical Foundations of Computer Science'94, volume 813 of
Lecture Notes in Computer Science, pages 316–328. Springer-Verlag,

[36]
Diederik Ton van Daalen.
The language theory of automath.
PhD thesis, Technische Hogeschool Eindhoven, 1977.

§ PROOFS OF <REF>

§ PROOFS OF <REF>

To check local confluence of $\Rew{\ALC}$ we have to check that

\[ t_1 \LRew{\ALC}  t \Rew{A} t_2 \mbox{ implies }
t_1 \Rewn{\ALC}  t_3 =_{\Es} t_4 \LRewn{\ALC} t_2 \]

where  $A = \{ \Appi, \Appii, \Appiii, \Lamb, \Compi, \Compii \}$

To check local coherence  of $\Rew{\ALC}$ we have to check that

\[ t_1 \LRew{\ALC}  t =_{\Es}  t_2
\mbox{ implies }
t_1 \Rewn{\ALC}  t_3 =_{\Es} t_4 \LRewn{\ALC} t_2 \]

By [18] it is sufficient to show that for every critical
pair $\langle c_1, c_2 \rangle$ there exist two $\ALC$-normal forms $c_1!$ and $c_2!$ of $c_1$ and $c_2$ respectively such that $c_1! =_{\Es} c_2!$. We thus check this property, remarking that in some cases we find a common reduct
before arriving at an $\ALC$-normal form so that in particular
the desired property holds.

* $\Compii$ and $\Appi$:

We have $y \in \fv(u)\ \&\ y \notin \fv(t_1\ t_2)\ \&\ x \in
\fv(t_1)\ \&\ x \in \fv(t_2)$ so that

$(t_1\ t_2)[x/u][y/v] \Rew{\Compii} (t_1\ t_2)[x/u[y/v]]$

$(t_1\ t_2)[x/u][y/v] \Rew{\Appi} (t_1[x/u]\ t_2[x/u])[y/v] $

can be closed by

$(t_1\ t_2)[x/u[y/v]] \Rew{\Appi} t_1[x/u[y/v]] \ t_2[x/u[y/v]]$

$(t_1[x/u]\ t_2[x/u])[y/v] \Rew{\Appi}
t_1[x/u][y/v]\ t_2[x/u][y/v] \Rewn{\Compii}t_1[x/u[y/v]] \

* $\Compii$ and $\Appii$:

We have $y \in \fv(u)\ \&\ y \notin \fv(t_1\ t_2)\ \&\ x \notin
\fv(t_1)\ \&\ x \in \fv(t_2)$ so that

$(t_1\ t_2)[x/u][y/v] \Rew{\Compii} (t_1\ t_2)[x/u[y/v]]$

$(t_1\ t_2)[x/u][y/v] \Rew{\Appii} (t_1\ t_2[x/u])[y/v] $

can be closed by

$(t_1\ t_2)[x/u[y/v]] \Rew{\Appii} t_1\ t_2[x/u[y/v]]$

$(t_1\ t_2[x/u])[y/v] \Rew{\Appii}
t_1\ t_2[x/u][y/v] \Rewn{\Compii} t_1\ t_2[x/u[y/v]]$

* $\Compii$ and $\Appiii$: Similar.

* $\Compii$ and $\Lamb$:

We have $y \in \fv(u)\ \&\ y \notin \fv(\l z. t)$ so that

$(\l z. t)[x/u][y/v] \Rew{\Compii} (\l z. t)[x/u[y/v]]$

$(\l z. t)[x/u][y/v] \Rew{\Lamb} (\l z. t[x/u])[y/v]$

can be closed by

$(\l z. t)[x/u[y/v]] \Rew{\Lamb} \l z. t[x/u[y/v]]$

$(\l z. t[x/u])[y/v] \Rew{\Lamb}\l z. t[x/u][y/v] \Rew{\Compii} \l
z. t[x/u[y/v]]$

* $\Compi$ and $\Appi$:

We have $y \in \fv(u)\ \&\ y \in \fv(t_1\ t_2)\ \&\ x \in
\fv(t_1)\ \&\ x \in \fv(t_2)$ so that

$(t_1\ t_2)[x/u][y/v] \Rew{\Compi} (t_1\ t_2)[y/v][x/u[y/v]]$

$(t_1\ t_2)[x/u][y/v] \Rew{\Appi} (t_1[x/u]\ t_2[x/u])[y/v]$

If $y \in \fv(t_1)\ \&\ y \in \fv(t_2)$, then we close by

$(t_1\ t_2)[y/v][x/u[y/v]] \Rew{\Appi}
(t_1[y/v]\ t_2[y/v])[x/u[y/v]] \Rew{\Appi}
t_1[y/v][x/u[y/v]]\ t_2[y/v][x/u[y/v]]$

$(t_1[x/u]\ t_2[x/u])[y/v] \Rew{\Appi}
t_1[x/u][y/v]\ t_2[x/u][y/v]\Rewn{\Compi}
t_1[y/v][x/u[y/v]]\ t_2[y/v][x/u[y/v]]$

If $y \notin \fv(t_1)\ \&\ y \in \fv(t_2)$, then we close by

$(t_1\ t_2)[y/v][x/u[y/v]] \Rew{\Appii}
(t_1\ t_2[y/v])[x/u[y/v]] \Rew{\Appi}
t_1[x/u[y/v]]\ t_2[y/v][x/u[y/v]]$

$(t_1[x/u]\ t_2[x/u])[y/v] \Rew{\Appi}
(t_1[x/u][y/v]\ t_2[x/u][y/v]\Rew{\Compi}
t_1[x/u][y/v]\ t_2[y/v][x/u[y/v]] \\ \Rew{\Compii}
t_1[x/u[y/v]]\ t_2[y/v][x/u[y/v]]$

If $y \in \fv(t_1)\ \&\ y \notin \fv(t_2)$, then is similar to the
previous case.

Remark that the case  $y \notin \fv(t_1)\ \&\ y \notin \fv(t_2)$
is not possible.

* $\Compi$ and $\Appii$

We have $y \in \fv(u)\ \&\ y \in \fv(t_1\ t_2)\ \&\ x \notin
\fv(t_1)\ \&\ x \in \fv(t_2)$ so that

$(t_1\ t_2)[x/u][y/v] \Rew{\Compi} (t_1\ t_2)[y/v][x/u[y/v]]$

$(t_1\ t_2)[x/u][y/v] \Rew{\Appii} (t_1\ t_2[x/u])[y/v]$

If $y \in \fv(t_1)\ \&\ y \in \fv(t_2)$, then we close by

$(t_1\ t_2)[y/v][x/u[y/v]] \Rew{\Appi}
(t_1[y/v]\ t_2[y/v])[x/u[y/v]] \Rew{\Appii}
t_1[y/v]\ t_2[y/v][x/u[y/v]]$

$(t_1\ t_2[x/u])[y/v] \Rew{\Appi}
t_1[y/v]\ t_2[x/u][y/v]\Rewn{\Compi}
t_1[y/v]\ t_2[y/v][x/u[y/v]]$

If $y \notin \fv(t_1)\ \&\ y \in \fv(t_2)$, then we close by

$(t_1\ t_2)[y/v][x/u[y/v]] \Rew{\Appii}
(t_1\ t_2[y/v])[x/u[y/v]] \Rew{\Appii}
t_1\ t_2[y/v][x/u[y/v]]$

$(t_1\ t_2[x/u])[y/v] \Rew{\Appii}
t_1\ t_2[x/u][y/v]\Rew{\Compi}
t_1\ t_2[y/v][x/u[y/v]]$

If $y \in \fv(t_1)\ \&\ y \notin \fv(t_2)$, then is similar to the
previous case.

Remark that the case  $y \notin \fv(t_1)\ \&\ y \notin \fv(t_2)$
is not possible.

* $\Compi$ and $\Appiii$: this case is similar to the
previous one.

* $\Compi$ and $\Lamb$:

We have $y \in \fv(u)\ \&\ y \in \fv(\l z.t)$ so that

$(\l z. t)[x/u][y/v] \Rew{\Compi} (\l z. t)[y/v][x/u[y/v]]$

$(\l z. t)[x/u][y/v] \Rew{\Lamb} (\l z. t[x/u])[y/v]$

can be closed by

$(\l z. t)[y/v][x/u[y/v]] \Rewn{\Lamb} \l z. t[y/v][x/u[y/v]]$

$(\l z. t[x/u])[y/v] \Rew{\Lamb} \l z. t[x/u][y/v]\Rew{\Compi} \l z. t[y/v][x/u[y/v]]$

* $\Compii$ and $\Compii$:

We have $z \in \fv(v)\ \&\ z \notin \fv(t[x/u])\ \&\ y \in
\fv(u)\ \&\ y \notin \fv(t)$ so that

$t[x/u][y/v][z/w] \Rew{\Compii} t[x/u][y/v[z/w]]$

$t[x/u][y/v][z/w] \Rew{\Compii} t[x/u[y/v]][z/w]$

can be closed by

$t[x/u][y/v[z/w]] \Rew{\Compii} t[x/u[y/v[z/w]]]$

$t[x/u[y/v]][z/w] \Rew{\Compii} t[x/u[y/v][z/w]] \Rew{\Compii}  t[x/u[y/v[z/w]]]$

* $\Compi$ and $\Compii$:

We have $z \in \fv(t[x/u])\ \&\ z \in \fv(v)\ \&\
y \in \fv(u)\ \&\ y \notin \fv(t)$ so that

$t[x/u][y/v][z/w] \Rew{\Compi} t[x/u][z/w][y/v[z/w]]$

$t[x/u][y/v][z/w] \Rew{\Compii} t[x/u[y/v]][z/w]$

If $z \in \fv(u)\ \&\ z \in \fv(t)$, we close by

$t[x/u][z/w][y/v[z/w]]  \Rew{\Compi} t[z/w][x/u[z/w]][y/v[z/w]]$

$t[x/u[y/v]][z/w] \Rew{\Compi} t[z/w][x/u[y/v][z/w]]
\Rew{\Compi}  t[z/w][x/u[z/w][y/v[z/w]]]$

If $z \in \fv(u)\ \&\ z \notin \fv(t)$, we close by

$t[x/u][z/w][y/v[z/w]]  \Rew{\Compii} t[x/u[z/w]][y/v[z/w]]$

$t[x/u[y/v]][z/w] \Rew{\Compii} t[x/u[y/v][z/w]]
\Rew{\Compi}  t[x/u[z/w][y/v[z/w]]]$

If $z \notin \fv(u)\ \&\ z \in \fv(t)$, we close by

$t[x/u][z/w][y/v[z/w]]  =_{\C}  t[z/w][x/u][y/v[z/w]]
\Rew{\Compii} t[z/w][x/u[y/v[z/w]]] $

$t[x/u[y/v]][z/w] \Rew{\Compi} t[z/w] [x/u[y/v][z/w] ]
\Rew{\Compii}  t[z/w] [x/u[y/v[z/w]]]$

* $\Compii$ and $\Compi$:

We  have $z \in \fv(v)\ \&\ z \notin \fv(t[x/u])\ \&\
y \in \fv(u)\ \&\ y \in \fv(t)$ so that

$t[x/u][y/v][z/w] \Rew{\Compii} t[x/u][y/v[z/w]]$

$t[x/u][y/v][z/w] \Rew{\Compi} t[y/v][x/u[y/v]][z/w]$

can be closed by

$t[x/u][y/v[z/w]] \Rew{\Compi} t[y/v[z/w]][x/u[y/v[z/w]]]$

$t[y/v][x/u[y/v]][z/w] \Rew{\Compi} t[y/v][z/w][x/u[y/v][z/w]]
\Rew{\Compii} t[y/v[z/w]][x/u[y/v][z/w]] \\
\Rew{\Compii} t[y/v[z/w]][x/u[y/v[z/w]]]$

* $\Compi$ and $\Compi$

We  have $z \in \fv(v)\ \&\ z \in \fv(t[x/u])\ \&\
y \in \fv(u)\ \&\ y \in \fv(t)$ so that

$t[x/u][y/v][z/w] \Rew{\Compi} t[x/u][z/w][y/v[z/w]]$

$t[x/u][y/v][z/w] \Rew{\Compi} t[y/v][x/u[y/v]][z/w]$

If $z \in \fv(u)\ \&\ z \notin \fv(t)$, then we close by

$t[x/u][z/w][y/v[z/w]] \Rew{\Compii}

$t[y/v][x/u[y/v]][z/w] \Rew{\Compi}
t[y/v][z/w][x/u[y/v][z/w]] \Rew{\Compi}
t[y/v][z/w][x/u[z/w][y/v[z/w]]]  \\ \Rew{\Compii}

If $z \notin \fv(u)\ \&\ z \in \fv(t)$, then we close by

$t[x/u][z/w][y/v[z/w]] =_{\C}
t[z/w][x/u][y/v[z/w]] \Rew{\Compi}

$t[y/v][x/u[y/v]][z/w] \Rew{\Compi}
t[z/w][y/v[z/w]][x/u[y/v][z/w]] \\ \Rew{\Compii}

* $\Appi$ and $\C$:

We have $y \notin \fv(u)\ \&\ x \notin \fv(v)\ \&\ x \in
\fv(t_1)\ \&\ x \in \fv(t_2)$ so that

$(t_1\ t_2)[x/u][y/v] =_{\C} (t_1\ t_2)[y/v] [x/u]$

$(t_1\ t_2)[x/u][y/v] \Rew{\Appi} (t_1[x/u]\ t_2[x/u])[y/v]$

If $y \in \fv(t_1)\ \&\ y \in \fv(t_2)$, we close by

$(t_1\ t_2)[y/v] [x/u] \Rew{\Appi} (t_1[y/v] \ t_2[y/v] )[x/u]
\Rew{\Appi} t_1[y/v][x/u] \ t_2[y/v][x/u]$

$(t_1[x/u]\ t_2[x/u])[y/v]\Rew{\Appi}
t_1[x/u][y/v]\ t_2[x/u][y/v] =_{\C} t_1[y/v][x/u]\ t_2[y/v][x/u]$

If $y \notin \fv(t_1)\ \&\ y \in \fv(t_2)$, we close by

$(t_1\ t_2)[y/v] [x/u] \Rew{\Appii} (t_1 \ t_2[y/v] )[x/u]
\Rew{\Appi} t_1[x/u] \ t_2[y/v][x/u]$

$(t_1[x/u]\ t_2[x/u])[y/v]\Rew{\Appii}
t_1[x/u]\ t_2[x/u][y/v] =_{\C} t_1[x/u]\ t_2[y/v][x/u]$

The case  $y \in \fv(t_1)\ \&\ y \notin \fv(t_2)$ is similar to
the previous one.

If $y \notin \fv(t_1)\ \&\ y \notin \fv(t_2)$, we close by

$(t_1\ t_2)[y/v] [x/u] \Rew{\Gc} (t_1 \ t_2)[x/u]
\Rew{\Appi} t_1[x/u] \ t_2[x/u]$

$(t_1[x/u]\ t_2[x/u])[y/v]\Rew{\Gc}
t_1[x/u]\ t_2[x/u]$

* $\Appii$ and $\C$:

We have $y \notin \fv(u)\ \&\ x \notin \fv(v)\ \&\ x \notin
\fv(t_1)\ \&\ x \in \fv(t_2)$ so that

$(t_1\ t_2)[x/u][y/v] =_{\C} (t_1\ t_2)[y/v] [x/u]$

$(t_1\ t_2)[x/u][y/v] \Rew{\Appii} (t_1\ t_2[x/u])[y/v]$

If $y \in \fv(t_1)\ \&\ y \in \fv(t_2)$, we close by

$(t_1\ t_2)[y/v] [x/u] \Rew{\Appi} (t_1[y/v] \ t_2[y/v] )[x/u]
\Rew{\Appii} t_1[y/v]\ t_2[y/v][x/u]$

$(t_1\ t_2[x/u])[y/v]\Rew{\Appi}
t_1[y/v]\ t_2[x/u][y/v] =_{\C} t_1[y/v]\ t_2[y/v][x/u]$

If $y \notin \fv(t_1)\ \&\ y \in \fv(t_2)$, we close by

$(t_1\ t_2)[y/v] [x/u] \Rew{\Appii} (t_1 \ t_2[y/v] )[x/u]
\Rew{\Appii} t_1\ t_2[y/v][x/u]$

$(t_1\ t_2[x/u])[y/v]\Rew{\Appii}
t_1\ t_2[x/u][y/v] =_{\C} t_1\ t_2[y/v][x/u]$

The case  $y \in \fv(t_1)\ \&\ y \notin \fv(t_2)$ is similar to
the previous one.

If $y \notin \fv(t_1)\ \&\ y \notin \fv(t_2)$, we close by

$(t_1\ t_2)[y/v] [x/u] \Rew{\Gc} (t_1 \ t_2)[x/u]
\Rew{\Appii} t_1\ t_2[x/u]$

$(t_1\ t_2[x/u])[y/v]\Rew{\Gc}
t_1\ t_2[x/u]$

* $\Appiii$ and $\C$: similar to the previous one.

* $\Lamb$ and $\C$:

We have $y \notin \fv(u)\ \&\ x \notin \fv(v)$ so that

$(\l z. t)[x/u][y/v] =_{\C} (\l z. t)[y/v] [x/u]$

$(\l z. t)[x/u][y/v] \Rew{\Lamb} (\l z. t[x/u])[y/v]$

can be closed by

$(\l z. t)[y/v] [x/u] \Rewn{\Lamb}\l z. t[y/v] [x/u]$

$(\l z. t[x/u])[y/v] \Rew{\Lamb} \l z. t[x/u][y/v] =_{\C} \l z. t[y/v][x/u]$

* $\Compii$ and $\C$:

We have $z \notin \fv(v)\ \&\ y \notin \fv(w)\ \&\ y \in
\fv(u)\ \&\ y \notin \fv(t)$ so that

$t[x/u][y/v][z/w] =_{\C} t[x/u][z/w][y/v]$

$t[x/u][y/v][z/w] \Rew{\Compii} t[x/u[y/v]][z/w]$

If $z \in \fv(t)\ \&\  z \in \fv(u)$, then

$t[x/u][z/w][y/v] \Rew{\Compi}
t[z/w][x/u[z/w]][y/v] \Rew{\Compii}

$t[x/u[y/v]][z/w] \Rew{\Compi}
t[z/w] [x/u[y/v][z/w] ] =_{\C} t[z/w] [x/u[z/w][y/v]]$

If $z \notin \fv(t)\ \&\ z \in \fv(u)$, then

$t[x/u][z/w][y/v] \Rew{\Compii}
t[x/u[z/w]][y/v] \Rew{\Compii}

$t[x/u[y/v]][z/w] \Rew{\Compi}
t[x/u[y/v][z/w] ] =_{\C} t[x/u[z/w][y/v]]$

If $z \notin \fv(u)$, then

$t[x/u][z/w][y/v] =_{\C} t[z/w][x/u][y/v] \Rew{\Compii} t[z/w][x/u[y/v]]$

$t[x/u[y/v]][z/w] =_{\C} t[z/w][x/u[y/v]]$

* $\Compi$ and $\C$:

We have $z \notin \fv(v)\ \&\ y \notin \fv(w)\ \&\ y \in
\fv(u)\ \&\ y \in \fv(t)$ so that

$t[x/u][y/v][z/w] =_{\C} t[x/u][z/w][y/v]$

$t[x/u][y/v][z/w] \Rew{\Compi} t[y/v][x/u[y/v]][z/w]$

If $z \in \fv(t)\ \&\ z \in \fv(u)$, then

$t[x/u][z/w][y/v] \Rew{\Compi} t[z/w][x/u[z/w]][y/v] \Rew{\Compi}

$t[y/v][x/u[y/v]][z/w]\Rew{\Compi} t[y/v][z/w][x/u[y/v][z/w]] =_{\C}

If $z \notin \fv(t)\ \&\ z \in \fv(u)$, then

$t[x/u][z/w][y/v] \Rew{\Compii} t[x/u[z/w]][y/v] \Rew{\Compi}

$t[y/v][x/u[y/v]][z/w]\Rew{\Compii} t[y/v][x/u[y/v][z/w]] =_{\C}

If $z \notin \fv(u)$, then

$t[x/u][z/w][y/v] =_{\C} t[z/w][x/u][y/v] \Rew{\Compi} t[z/w][y/v] [x/u[y/v]]$

$t[y/v][x/u[y/v]][z/w]  =_{\C} t[z/w][y/v][x/u[y/v]]$

* $\Compii$ and $\C$:

We have $y \notin \fv(u)\ \&\ x \notin \fv(v)\ \&\
z \in \fv(v)\ \&\ z \notin \fv(t[x/u])$ so that

$t[x/u][y/v][z/w] =_{\C} t[y/v][x/u][z/w]$

$t[x/u][y/v][z/w] \Rew{\Compii} t[x/u][y/v[z/w]]$

can be closed by

$t[y/v][x/u][z/w] =_{\C} t[y/v][z/w][x/u] \Rew{\Compii} t[y/v[z/w]][x/u]$

$t[x/u][y/v[z/w]]=_{\C} t[y/v[z/w]][x/u]$

* $\Compi$ and $\C$:

We have $y \notin \fv(u)\ \&\ x \notin \fv(v)\ \&\
z \in \fv(v)\ \&\ z \in \fv(t[x/u])$ so that

$t[x/u][y/v][z/w] =_{\C} t[y/v][x/u][z/w]$

$t[x/u][y/v][z/w] \Rew{\Compi} t[x/u][z/w][y/v[z/w]]$

If $z \in \fv(t)\ \&\ z \in \fv(u)$, then

$t[y/v][x/u][z/w] \Rew{\Compi} t[y/v][z/w][x/u[z/w]] \Rew{\Compi}

$t[x/u][z/w][y/v[z/w]] \Rew{\Compi} t[z/w][x/u[z/w]][y/v[z/w]]
=_{\C} t[z/w][y/v[z/w]][x/u[z/w]]$

If $z \notin \fv(t)\ \&\ z \in \fv(u)$, then

$t[y/v][x/u][z/w]\Rew{\Compi} t[y/v][z/w][x/u[z/w]]\Rew{\Compii}t[y/v[z/w]][x/u[z/w]]$

$t[x/u][z/w][y/v[z/w]]\Rew{\Compii} t[x/u[z/w]][y/v[z/w]]
=_{\C} t[y/v[z/w]][x/u[z/w]]$

If $z \in \fv(t)\ \&\ z \notin \fv(u)$, then

$t[y/v][x/u][z/w] =_{\C} t[y/v][z/w][x/u] \Rew{\Compi} t[z/w][y/v[z/w]][x/u]$

$t[x/u][z/w][y/v[z/w]]=_{\C} t[z/w][y/v[z/w]][x/u]$

If $z \notin \fv(t)$ then  $\ALC(t[z/u]) = \l \vec{y}.\ALC(t')[z/u]$
with $t=\l  \vec{y}.t'$ and    $t'   \neq  \l y'.t''$.   Then    $\l
\vec{y}.\ALC(t')[z/u]    \Rew{\les}   \l      \vec{y}.\ALC(t')[z/u']
\Rewn{\les} \l \vec{y}.\ALC(t')[z/\ALC(u')] = \ALC(t[z/u'])$.

Otherwise,  $z \in \fv(t)$, and  we
reason by induction on  the structure of $t$.

* $t = z$.
$\ALC(t[z/u]) = z[z/u] \Rew{\les} z[z/u'] \Rewn{\les} z[z/\ALC(u')] = \ALC(t[z/u'])$.

* $t = \l y. t_1$.

$\ALC(t[z/u]) = \ALC((\l y. t_1)[z/u]) = \l y.\ALC(t_1[z/u])$

$\Rewplus{\les} $ () $\:\l y.\ALC(t_1[z/u']) = \ALC((\l y.t_1)[z/u'])$.

* $t = (t_1\ t_2)$.

There are three subcases.

* $z \in \fv(t_1)$, $z \in \fv(t_2)$.

$\ALC(t[z/u]) = \ALC((t_1\ t_2)[z/u]) = (\ALC(t_1[z/u])\ \ALC(t_2[z/u]))$

$\Rewplus{\les}$ ( twice) $(\ALC(t_1[z/u'])\ \ALC(t_2[z/u']))$

$ = \ALC(t_1[z/u']\ t_2[z/u']) = \ALC((t_1\ t_2)[z/u'])$.

* $z \in \fv(t_1)$, $z \notin \fv(t_2)$. Similar.

* $z \notin \fv(t_1)$, $z \in \fv(t_2)$. Similar.

* $t =  t_0[\vec{x}/\vec{t}]$ with  $\vec{x} =  x_1, \ldots,
x_n$,  $\vec{t}  =  t_1,  \ldots,  t_n$, $n  >  0$,  $t_0  \neq
v_1[y/v_2]$,   $x_j  \notin  \fv(t_i)$   for  all   $i,j \in [1..n]$ (the
substitutions are independent).

Since  we are rewriting  modulo $\Es$  and the  substitutions are
independent, we choose an order for them in the proofs below. For
convenience,    we   write    $[x_i\ldots   x_j]$    instead   of

We now reason by cases on $t_0$.

* $t_0 = y$. Let $z \in \fv(t_i)$, $i \in [1..k]$, $z \notin
\fv(t_{j})$, $j \in [k+1..n]$.  Let $y = z$. We have

\begin{eqnarray*}
=&z[z/u][x_1/\ALC(t_1[z/u])]\cdots[x_k/\ALC(t_k[z/u])][x_{k+1}\ldots x_n]\\
\mbox{(\ih)} \Rewplus{\les} &z[z/u][x_1/\ALC(t_1[z/u'])]\cdots[x_k/\ALC(t_k[z/u'])][x_{k+1}\ldots x_n]\\
\Rewplus{\les}&z[z/\ALC(u')][x_1/\ALC(t_1[z/u'])]\cdots[x_k/\ALC(t_k[z/u'])][x_{k+1}\ldots x_n]\\
\end{eqnarray*}

W.l.o.g., the remaining  cases are $y = x_i$ for $i \in [1..k]$,
$y = x_{i}$
for $i \in [k+1..n]$, and
$y \neq z,x_i$ for all $i \in [1..n]$ and they are similar.

* $t_0 = \l y. v$.

$\ALC(t[z/u]) = \ALC((\l y. v)[\vec{x}/\vec{t}][z/u]) = \l y.\ALC(v[\vec{x}/\vec{t}][z/u])\: \mbox{ (\ih)}$

$\Rewplus{\les} \l y. \ALC(v[\vec{x}/\vec{t}][z/u']) =\ALC((\l y. v)[\vec{x}/\vec{t}][z/u']) = \ALC(t[z/u'])$.

* $t_0 = (v_1\ v_2)$.
We partition the set of substitutions $\{[x_1/t_1],\ldots,[x_n/t_n]\}$ as follows:

* $x_1 \ldots x_{k_1} \in \fv(v_1)$, $x_1 \ldots x_{k_1} \notin \fv(v_2)$;

* $x_{k_1+1} \ldots x_{k_2} \in \fv(v_1)$, $x_{k_1+1} \ldots x_{k_2} \in \fv(v_2)$;

* $x_{k_2+1} \ldots x_{k_3} \notin \fv(v_1)$, $x_{k_2+1} \ldots x_{k_3} \in \fv(v_2)$;

* $x_{k_3+1} \ldots x_{k_4} \notin \fv(v_1) \cup \fv(v_2)$, $z \in \fv(t_{k_3+1}),\ldots, \fv(t_{k_4})$;

* $x_{k_4+1} \ldots x_{k_n} \notin \fv(v_1) \cup \fv(v_2)$, $z \notin \fv(t_{k_4+1}),\ldots, \fv(t_{k_n})$.

There are three  cases depending on whether $z  \in \fv(v_1) \cup
\bigcup_{i  \in  [1..k_2]}\fv(t_i)$   or  $z  \in  \fv(v_2)  \cup
\bigcup_{i \in [k_1..k_3]}\fv(t_i)$. We treat the case where both
conditions are true. The other cases are similar.

The       use  of     below    does    not  follow directly   from
$\ALC(v_1[\vec{x}/\vec{t}][z/u])                        \Rewplus{\les}
\ALC(v_1[\vec{x}/\vec{t}][z/u'])$   but   can   be  derived  from  the
hypothesis by  considering  the structure of   $v_1$ as  $\l  \vec{y}.
v_1'$ and using $x_{k_2+1}\ldots  x_n \notin \fv(v_1)$ (similarly  for

\begin{eqnarray*}
=&\ALC((v_1\ v_2)[\vec{x}/\vec{t}][z/u])\\
=&(\ALC(v_1[x_1\ldots x_{k_2}][z/u])\ \ALC(v_2[x_{k_1+1}\ldots x_{k_3}][z/u]))\\
&[x_{k_3+1}/\ALC(t_{k_3+1}[z/u])]\cdots[x_{k_4}/\ALC(t_{k_4}[z/u])][x_{k_4+1}\ldots x_{k_n}]\\
\mbox{(\ih)} \Rewplus{\les}&(\ALC(v_1[x_1\ldots x_{k_2}][z/u'])\ \ALC(v_2[x_{k_1+1}\ldots x_{k_3}][z/u']))\\
&[x_{k_3+1}/\ALC(t_{k_3+1}[z/u])]\cdots[x_{k_4}/\ALC(t_{k_4}[z/u])][x_{k_4+1}\ldots x_{k_n}]\\
\mbox{(\ih)} \Rewplus{\les}
&(\ALC(v_1[x_1\ldots x_{k_2}][z/u'])\ \ALC(v_2[x_{k_1+1}\ldots x_{k_3}][z/u']))\\
&[x_{k_3+1}/\ALC(t_{k_3+1}[z/u'])]\cdots[x_{k_4}/\ALC(t_{k_4}[z/u'])][x_{k_4+1}\ldots x_{k_n}]\\
\end{eqnarray*}

* $t = t_0[\vec{x}/\vec{t}]$ with  $\vec{x} =  x_1, \ldots, x_n$,
$\vec{t} = t_1,  \ldots, t_n$, $n  > 0$, $t_0 \neq v_1[y/v_2]$, $x_j
\in    \fv(t_i)$ for   some   $i<j$   (the   substitutions are   not
independent). This case degenerates into the previous case:

\begin{eqnarray*}
=&\ALC((v_1\ v_2)[\vec{x}/\vec{t}][z/u])\\
=&\ALC((v_1\ v_2)[\vec{y}/\vec{s}][z/u])\\
&\mbox{such that the substitutions $[\vec{y}/\vec{s}]$ are independent}\\
\mbox{previous case }  \Rewplus{\les} &\ALC((v_1\ v_2)[\vec{y}/\vec{s}][z/u'])\\
=&\ALC((v_1\ v_2)[\vec{x}/\vec{t}][z/u'])\\
\end{eqnarray*}

By induction on the definition of $t \Rew{\lm} t'$. By <ref> (twice), it is
sufficient to prove that $t \Rew{\B\sm} t'$
implies $\tra{t}
\Rew{\B\sm} \tra{t'}$. First we consider the base case of the induction
where reductions occur at the root.

* $t=(\lambda x.u)\ v \Rew{\B} u[x/v]=t'$.

If $x \in \fv(u)$, then
$\tra{(\lambda x.u)\ v}
=  ((\lambda x.\tra{u})\ \tra{v}) [z/\tra{v}]
\Rew{\B}  \tra{u}[x/\tra{v}][z/\tra{v}]
\Rewn{\ALC}  \ALC(\tra{u}[x/\tra{v}][z/\tra{v}])
=  \tra{u[x/v]}$.

If $x \notin \fv(u)$, then
$\tra{(\lambda x.u)\ v}
=  ((\lambda x.\tra{u})\ \tra{v}) [z/\tra{v}]
\Rew{\B}  \tra{u}[x/\tra{v}][z/\tra{v}]
\Rew{\Gc}  \tra{u}[x/\tra{v}]
\Rewn{\ALC}  \ALC(\tra{u}[x/\tra{v}])=  \tra{u[x/v]}

* $t=C\cwc{x}[x/u] \Rew{\us} C\cwc{u}[x/u]=t'$.
We reason by  induction on the context  $C$.

* $C = \Box$.
Then $t=x[x/u] \Rew{\us} u[x/u]=t'$ and
$\tra{t}=x[x/\tra{u}][\fresh{x}/\tra{u}] \Rew{\Var}
\tra{u}[\fresh{x}/\tra{u}] \Rewn{\ALC} \ALC(\tra{u}[\fresh{x}/\tra{u}])
= \tra{u[x/u]}$.

* $C = D\ v$.

We treat the case where $x \notin \fv(v)$. By the , $\tra{D\cwc{x}[x/u]} = $$\ALC(\tra{D\cwc{x}}[x/\tra{u}][\fresh{x}/\tra{u}]) \Rewplus{\les} \tra{D\cwc{u}[x/u]}$. We have

\begin{array}{rcll}
\tra{D\cwc{u}[x/u]}& =& \ALC(\tra{D\cwc{u}}[x/\tra{u}]) & x \notin \fv(D\cwc{u})\\
\tra{D\cwc{u}[x/u]}& =& \ALC(\tra{D\cwc{u}}[x/\tra{u}][\fresh{x}/\tra{u}]) & x \in \fv(D\cwc{u})
\end{array}

so by <ref>,

\begin{array}{ll}
\ALC(\tra{D\cwc{x}}[x/\tra{u}]) \Rewplus{\les} \ALC(\tra{D\cwc{u}}) & x \notin \fv(D\cwc{u})\\
\ALC(\tra{D\cwc{x}}[x/\tra{u}]) \Rewplus{\les} \ALC(\tra{D\cwc{u}}[x/\tra{u}]) & x \in \fv(D\cwc{u}).
\end{array}

When $x \in \fv(D\cwc{u})$ then

\begin{eqnarray*}
&\tra{(D\cwc{x}\ v)[x/u]}\\
=& \ALC((\tra{D\cwc{x}}\ \tra{v})[z/\tra{v}][x/\tra{u}][\fresh{x}/\tra{u}])\\
=& (\ALC(\tra{D\cwc{x}}[x/\tra{u}])\ \ALC(\tra{v}))[z/\tra{v}][\fresh{x}/\tra{u}]\\
\Rewplus{\les} & (\ALC(\tra{D\cwc{u}}[x/\tra{u}])\ \ALC(\tra{v}))[z/\tra{v}][\fresh{x}/\tra{u}]\\
=& (\ALC(\tra{D\cwc{u}}[x/\tra{u}]\ \tra{v}))[z/\tra{v}][\fresh{x}/\tra{u}]\\
=& \ALC((\tra{D\cwc{u}}\ \tra{v})[z/\tra{v}][x/\tra{u}][\fresh{x}/\tra{u}])\\
=&\tra{(D\cwc{u} v)[x/u]}.
\end{eqnarray*}

Otherwise, if $x \notin \fv(D\cwc{u})$ then

\begin{eqnarray*}
&\tra{(D\cwc{x}\ v)[x/u]}\\
=& \ALC((\tra{D\cwc{x}}\ \tra{v})[z/\tra{v}][x/\tra{u}][\fresh{x}/\tra{u}])\\
=& (\ALC(\tra{D\cwc{x}}[x/\tra{u}])\ \ALC(\tra{v}))[z/\tra{v}][\fresh{x}/\tra{u}]\\
\Rewplus{\les} & (\ALC(\tra{D\cwc{u}})\ \ALC(\tra{v}))[z/\tra{v}][\fresh{x}/\tra{u}]\\
=& \ALC((\tra{D\cwc{u}}\ \tra{v})[z/\tra{v}][\fresh{x}/\tra{u}])\\
=&\tra{(D\cwc{u} v)[x/u]}
\end{eqnarray*}

The case where $x \notin \fv(D\cwc{u})$ follows similarly as do the cases where $x \in \fv(v)$.

The cases where $x \in \fv(v)$ follow similarly.

* $C = v\ D$.

We treat the case where $x \notin \fv(v)$. Again we have

\begin{array}{ll}
\ALC(\tra{D\cwc{x}}[x/\tra{u}]) \Rewplus{\les} \ALC(\tra{D\cwc{u}}) & x \notin \fv(D\cwc{u})\\
\ALC(\tra{D\cwc{x}}[x/\tra{u}]) \Rewplus{\les} \ALC(\tra{D\cwc{u}}[x/\tra{u}]) & x \in \fv(D\cwc{u}).
\end{array}

When $x \in \fv(D\cwc{u})$ we have the following.

\begin{eqnarray*}
&\tra{(v\ D\cwc{x})[x/u]}\\
=& \ALC((\tra{v}\ \tra{D\cwc{x}})[z/\tra{D\cwc{x}}][x/\tra{u}][\fresh{x}/\tra{u}])\\
=& (\ALC(\tra{v})\ \ALC(\tra{D\cwc{x}}[x/\tra{u}]))[z/\ALC(\tra{D\cwc{x}}[x/\tra{u}])][\fresh{x}/\tra{u}]\\
\Rewplus{\les} & (\ALC(\tra{v})\ \ALC(\tra{D\cwc{u}}[x/\tra{u}]))[z/\ALC(\tra{D\cwc{u}}[x/\tra{u}])][\fresh{x}/\tra{u}]\\
= & \ALC(\tra{v}\ \tra{D\cwc{u}}[x/\tra{u}])[z/\ALC(\tra{D\cwc{u}}[x/\tra{u}])][\fresh{x}/\tra{u}]\\
= & \ALC((\tra{v}\ \tra{D\cwc{u}})[z/\tra{D\cwc{u}}][x/\tra{u}][\fresh{x}/\tra{u}])\\
=&\tra{(v\ D\cwc{u})[x/u]}
\end{eqnarray*}

The case where $x \notin \fv(D\cwc{u})$ follows similarly as do the cases where $x \in \fv(v)$.

* $C = \l z. D$.

When $x \in \fv(D\cwc{u})$ we have:

\begin{eqnarray*}
& \tra{C\cwc{x}[x/u]}\\
=& \ALC((\l z. \tra{D\cwc{x}})[x/\tra{u}][\fresh{x}/\tra{u}]) \\
=& \l z.\ALC(\tra{D\cwc{x}}[x/\tra{u}][\fresh{x}/\tra{u}])\\
=& \l z. \tra{D\cwc{x}[x/u]}\\
\Rewplus{\les} (\ih)& \l z. \tra{D\cwc{u}[x/u]} \\
=& \l z.\ALC(\tra{D\cwc{u}}[x/\tra{u}][\fresh{x}/\tra{u}])\\
=& \ALC((\l z. \tra{D\cwc{u}})[x/\tra{u}][\fresh{x}/\tra{u}]) \\
=& \tra{C\cwc{u}[x/u]}
\end{eqnarray*}

When $x \notin \fv(D\cwc{u})$ we have:

\begin{eqnarray*}
& \tra{C\cwc{x}[x/u]}\\
=& \ALC((\l z. \tra{D\cwc{x}})[x/\tra{u}][\fresh{x}/\tra{u}]) \\
=& \l z.\ALC(\tra{D\cwc{x}}[x/\tra{u}][\fresh{x}/\tra{u}])\\
=& \l z. \tra{D\cwc{x}[x/u]}\\
\Rewplus{\les} (\ih)& \l z. \tra{D\cwc{u}[x/u]} \\
=& \l z.\ALC(\tra{D\cwc{u}}[x/\tra{u}])\\
=& \ALC((\l z. \tra{D\cwc{u}})[x/\tra{u}]) \\
=& \tra{C\cwc{u}[x/u]}
\end{eqnarray*}

* $C = D[z/v]$.

The case is further broken down depending on whether $z \in \fv(D\cwc{x})$, $x \in \fv(D\cwc{u})$, and $x \in \fv(v)$.

$\tra{D\cwc{x}[x/u]} = \ALC(\tra{D\cwc{x}}[x/\tra{u}][\fresh{x}/\tra{u}]) \Rewplus{\les} \tra{D\cwc{u}[x/u]}$ by the  . We have

\begin{array}{rcll}
\tra{D\cwc{u}[x/u]}& =& \ALC(\tra{D\cwc{u}}[x/\tra{u}]) & x \notin \fv(D\cwc{u})\\
\tra{D\cwc{u}[x/u]}& =& \ALC(\tra{D\cwc{u}}[x/\tra{u}][\fresh{x}/\tra{u}]) & x \in \fv(D\cwc{u})
\end{array}

so by <ref>,

\begin{array}{ll}
\ALC(\tra{D\cwc{x}}[x/\tra{u}]) \Rewplus{\les} \ALC(\tra{D\cwc{u}}) & x \notin \fv(D\cwc{u})\\
\ALC(\tra{D\cwc{x}}[x/\tra{u}]) \Rewplus{\les} \ALC(\tra{D\cwc{u}}[x/\tra{u}]) & x \in \fv(D\cwc{u})
\end{array}

As $z \in \fv(D\cwc{x})$ and $z\neq x$ implies
$z \in \fv( \tra{D\cwc{x}}[x/\tra{u}])$ and $z \in \fv(\tra{D\cwc{u}})$,
by <ref>.<ref> and <ref>.<ref> we have

\begin{array}{ll}
\ALC(\tra{D\cwc{x}}[x/\tra{u}][z/v']) \Rewplus{\les} \ALC(\tra{D\cwc{u}}[z/v'])\\
\hfill x \notin \fv(D\cwc{u})\\
\ALC(\tra{D\cwc{x}}[x/\tra{u}][z/v']) \Rewplus{\les} \ALC(\tra{D\cwc{u}}[x/\tra{u}][z/v']) \\
\hfill x \in \fv(D\cwc{u}).
\end{array}

We take the case where $x \in \fv(D\cwc{u})$, $z \in \fv(D\cwc{x})$, $x \notin \fv(v)$. We assume below that $D\cwc{x} \neq \l y.s$ for some $s$ – the alternative case can be similarly proved.

\begin{eqnarray*}
& \tra{C\cwc{x}[x/u]}\\
= & \ALC(\tra{D\cwc{x}}[z/\tra{v}][\fresh{z}/\tra{v}][x/\tra{u}][\fresh{x}/\tra{u}])\\
= & \ALC(\tra{D\cwc{x}}[x/\tra{u}][z/\tra{v}])[\fresh{z}/\tra{v}][\fresh{x}/\tra{u}]\\
\Rewplus{\les} &
\ALC(\tra{D\cwc{u}}[x/\tra{u}][z/\tra{v}])[\fresh{z}/\tra{v}][\fresh{x}/\tra{u}]\\
= & \ALC(\tra{D\cwc{u}}[z/\tra{v}][\fresh{z}/\tra{v}][x/\tra{u}][\fresh{x}/\tra{u}])\\
= & \tra{C\cwc{u}[x/u]}
\end{eqnarray*}

We assume below that $D\cwc{x} \neq \l y.s$ for some $s$ – the alternative case can be similarly proved.

Let $x \in \fv(D\cwc{u})$, $z \in \fv(D\cwc{x})$, $x \in \fv(v)$.

\begin{eqnarray*}
& \tra{C\cwc{x}[x/u]}\\
= & \ALC(\tra{D\cwc{x}}[z/\tra{v}][\fresh{z}/\tra{v}][x/\tra{u}][\fresh{x}/\tra{u}])\\
= & \ALC(\tra{D\cwc{x}}[x/\tra{u}][z/\tra{v}[x/\tra{u}]])[\fresh{z}/\tra{v}[x/\tra{u}]][\fresh{x}/\tra{u}]\\
\Rewplus{\les} &         \ALC(\tra{D\cwc{u}}[x/\tra{u}][z/\tra{v}[x/\tra{u}]])[\fresh{z}/\tra{v}[x/\tra{u}]][\fresh{x}/\tra{u}]\\
= & \ALC(\tra{D\cwc{u}}[z/\tra{v}][\fresh{z}/\tra{v}][x/\tra{u}][\fresh{x}/\tra{u}])\\
= & \tra{C\cwc{u}[x/u]}
\end{eqnarray*}

Let $x \in \fv(D\cwc{u})$, $z \in \fv(D\cwc{x})$, $x \notin \fv(v)$.

\begin{eqnarray*}
& \tra{C\cwc{x}[x/u]}\\
= & \ALC(\tra{D\cwc{x}}[z/\tra{v}][\fresh{z}/\tra{v}][x/\tra{u}][\fresh{x}/\tra{u}])\\
= & \ALC(\tra{D\cwc{x}}[x/\tra{u}][z/\tra{v}])[\fresh{z}/\tra{v}][\fresh{x}/\tra{u}]\\
\Rewplus{\les} &
\ALC(\tra{D\cwc{u}}[x/\tra{u}][z/\tra{v}])[\fresh{z}/\tra{v}][\fresh{x}/\tra{u}]\\
= & \ALC(\tra{D\cwc{u}}[z/\tra{v}][\fresh{z}/\tra{v}][x/\tra{u}][\fresh{x}/\tra{u}])\\
= & \tra{C\cwc{u}[x/u]}
\end{eqnarray*}

Let $x \notin \fv(D\cwc{u})$, $z \notin \fv(D\cwc{x})$, $x \in \fv(v)$.

\begin{eqnarray*}
& \tra{C\cwc{x}[x/u]}\\
= & \ALC(\tra{D\cwc{x}}[z/\tra{v}][x/\tra{u}][\fresh{x}/\tra{u}])\\
= & \ALC(\tra{D\cwc{x}}[x/\tra{u}][z/\tra{v}[x/\tra{u}]])[\fresh{x}/\tra{u}]\\
\Rewplus{\les} &         \ALC(\tra{D\cwc{u}}[z/\tra{v}[x/\tra{u}]])[\fresh{x}/\tra{u}]\\
= & \ALC(\tra{D\cwc{u}}[z/\tra{v}][x/\tra{u}][\fresh{x}/\tra{u}])\\
= & \tra{C\cwc{u}[x/u]}
\end{eqnarray*}

Let $x \notin \fv(D\cwc{u})$, $z \notin \fv(D\cwc{x})$, $x \notin \fv(v)$.

\begin{eqnarray*}
& \tra{C\cwc{x}[x/u]}\\
= & \ALC(\tra{D\cwc{x}}[z/\tra{v}][x/\tra{u}][\fresh{x}/\tra{u}])\\
= & \ALC(\tra{D\cwc{x}}[x/\tra{u}][z/\tra{v}])[\fresh{x}/\tra{u}]\\
\Rewplus{\les} &
\ALC(\tra{D\cwc{u}}[z/\tra{v}])[\fresh{x}/\tra{u}]\\
= & \ALC(\tra{D\cwc{u}}[z/\tra{v}][\fresh{x}/\tra{u}])\\
= & \tra{C\cwc{u}[x/u]}
\end{eqnarray*}

The remaining four cases are similar.

* $C = v[z/D]$.

$\tra{D\cwc{x}[x/u]} = \ALC(\tra{D\cwc{x}}[x/\tra{u}][\fresh{x}/\tra{u}]) \Rewplus{\les} \tra{D\cwc{u}[x/u]}$ by the . We assume below that $v \neq \l y.s$ for some $s$ – the alternative is similarly explained.

The  case is further broken down  depending on whether $z \in \fv(v)$,
$x \in \fv(D\cwc{u})$,  and $x  \in \fv(v)$.  For the  cases where  $x
\notin \fv(D\cwc{u})$, we use  the    equations and reductions    from <ref>.    For   the    cases    where   $x   \in
\fv(D\cwc{u})$,  we   use     the equations  and     reductions   from <ref>.

\begin{eqnarray}
\nonumber  &\tra{D\cwc{u}[x/u]}\\
\nonumber  &=\ALC(\tra{D\cwc{u}}[x/\tra{u}]).\\
\nonumber  & \mbox{Thus, by~\cref{l:non-interfering-garbage},}\\
\nonumber  &\ALC(\tra{D\cwc{x}}[x/\tra{u}])\\
\nonumber  &\Rewplus{\les} \ALC(\tra{D\cwc{u}}).\\
\nonumber  & \mbox{Thus, by~\cref{c:reduce-copies-of-subs},}\\
\nonumber  &\ALC(\tra{v}[z/\ALC(\tra{D\cwc{x}}[x/\tra{u}])])\\
&\Rewplus{\les}  \ALC(\tra{v}[z/\ALC(\tra{D\cwc{u}})]) \label{EqSimproof1}\\
\nonumber  & \mbox{and}\\
\nonumber  &\ALC(\tra{v}[x/\tra{u}])][z/\ALC(\tra{D\cwc{x}}[x/\tra{u}])])\\
&\Rewplus{\les}  \ALC(\tra{v}[x/\tra{u}])][z/\ALC(\tra{D\cwc{u}})])~\label{EqSimproof2}\\
\nonumber  & \mbox{Let $\fresh{z}$ be fresh for the equations above. Then:}\\
\nonumber  &\ALC(\tra{v}[z/\ALC(\tra{D\cwc{x}}[x/\tra{u}])][\fresh{z}/\ALC(\tra{D\cwc{x}}[x/\tra{u}])])\\
\nonumber =&\ALC(\tra{v}[z/\ALC(\tra{D\cwc{x}}[x/\tra{u}])])[\fresh{z}/\ALC(\tra{D\cwc{x}}[x/\tra{u}])]\\
\nonumber \Rewplus{\les} &
\ALC(\tra{v}[z/\ALC(\tra{D\cwc{u}})])[\fresh{z}/\ALC(\tra{D\cwc{x}}[x/\tra{u}])]\\
\nonumber \Rewplus{\les} &
\ALC(\tra{v}[z/\ALC(\tra{D\cwc{u}})])[\fresh{z}/\ALC(\tra{D\cwc{u}})]\\
= &\ALC(\tra{v}[z/\ALC(\tra{D\cwc{u}})][\fresh{z}/\ALC(\tra{D\cwc{u}})])~\label{EqSimproof3}\\
\nonumber  & \mbox{and}\\
\nonumber  &\ALC(\tra{v}[x/\tra{u}][z/\ALC(\tra{D\cwc{x}}[x/\tra{u}])][\fresh{z}/\ALC(\tra{D\cwc{x}}[x/\tra{u}])])\\
\nonumber =&\ALC(\tra{v}[x/\tra{u}][z/\ALC(\tra{D\cwc{x}}[x/\tra{u}])])[\fresh{z}/\ALC(\tra{D\cwc{x}}[x/\tra{u}])]\\
\nonumber \Rewplus{\les} &
\ALC(\tra{v}[x/\tra{u}][z/\ALC(\tra{D\cwc{u}})])[\fresh{z}/\ALC(\tra{D\cwc{x}}[x/\tra{u}])]\\
\nonumber \Rewplus{\les} &
\ALC(\tra{v}[x/\tra{u}][z/\ALC(\tra{D\cwc{u}})])[\fresh{z}/\ALC(\tra{D\cwc{u}})]\\
\ALC(\tra{v}[x/\tra{u}][z/\ALC(\tra{D\cwc{u}})][\fresh{z}/\ALC(\tra{D\cwc{u}})])~\label{EqSimproof4} \\
\end{eqnarray}

Equations for the cases where $x$ is not free in $\fv(D{\cwc{u}})$

\begin{eqnarray}
\nonumber &\tra{D\cwc{u}[x/u]}\\
\nonumber &= \ALC(\tra{D\cwc{u}}[x/\tra{u}][\fresh{x}/\tra{u}]).\\
\nonumber & \mbox{Thus, by~\cref{l:non-interfering-garbage},}\\
\nonumber &\ALC(\tra{D\cwc{x}}[x/\tra{u}])\\
\nonumber &\Rewplus{\les} \ALC(\tra{D\cwc{u}}[x/\tra{u}]).\\
\nonumber & \mbox{Thus, by~\cref{c:reduce-copies-of-subs},}\\
\nonumber &\ALC(\tra{v}[z/\ALC(\tra{D\cwc{x}}[x/\tra{u}])])\\
&\Rewplus{\les} \ALC(\tra{v}[z/\ALC(\tra{D\cwc{u}}[x/\tra{u}])]) \label{EqSimproof5}\\
\nonumber  & \mbox{and}\\
\nonumber &\ALC(\tra{v}[x/\tra{u}])][z/\ALC(\tra{D\cwc{x}}[x/\tra{u}])])\\
&\Rewplus{\les} \ALC(\tra{v}[x/\tra{u}])][z/\ALC(\tra{D\cwc{u}}[x/\tra{u}])])~\label{EqSimproof6}\\
\nonumber  & \mbox{Let $\fresh{z}$ be fresh for the equations above. Then:}\\
\nonumber  &\ALC(\tra{v}[z/\ALC(\tra{D\cwc{x}}[x/\tra{u}])][\fresh{z}/\ALC(\tra{D\cwc{x}}[x/\tra{u}])])\\
\nonumber =&\ALC(\tra{v}[z/\ALC(\tra{D\cwc{x}}[x/\tra{u}])])[\fresh{z}/\ALC(\tra{D\cwc{x}}[x/\tra{u}])]\\
\nonumber \Rewplus{\les} &
\ALC(\tra{v}[z/\ALC(\tra{D\cwc{u}}[x/\tra{u}])])[\fresh{z}/\ALC(\tra{D\cwc{x}}[x/\tra{u}])]\\
\nonumber \Rewplus{\les} &
\ALC(\tra{v}[z/\ALC(\tra{D\cwc{u}}[x/\tra{u}])])[\fresh{z}/\ALC(\tra{D\cwc{u}}[x/\tra{u}])]\\
= &\ALC(\tra{v}[z/\ALC(\tra{D\cwc{u}}[x/\tra{u}])][\fresh{z}/\ALC(\tra{D\cwc{u}}[x/\tra{u}])])~\label{EqSimproof7}\\
\nonumber  & \mbox{and}\\
\nonumber  &\ALC(\tra{v}[x/\tra{u}][z/\ALC(\tra{D\cwc{x}}[x/\tra{u}])][\fresh{z}/\ALC(\tra{D\cwc{x}}[x/\tra{u}])])\\
\nonumber =&\ALC(\tra{v}[x/\tra{u}][z/\ALC(\tra{D\cwc{x}}[x/\tra{u}])])[\fresh{z}/\ALC(\tra{D\cwc{x}}[x/\tra{u}])]\\
\nonumber \Rewplus{\les} & \ALC(\tra{v}[x/\tra{u}][z/\ALC(\tra{D\cwc{u}}[x/\tra{u}])])[\fresh{z}/\ALC(\tra{D\cwc{x}}[x/\tra{u}])]\\
\nonumber \Rewplus{\les} &
\ALC(\tra{v}[x/\tra{u}][z/\ALC(\tra{D\cwc{u}}[x/\tra{u}])])[\fresh{z}/\ALC(\tra{D\cwc{u}}[x/\tra{u}])]\\
=& \ALC(\tra{v}[x/\tra{u}][z/\ALC(\tra{D\cwc{u}}[x/\tra{u}])][\fresh{z}/\ALC(\tra{D\cwc{u}}[x/\tra{u}])])~\label{EqSimproof8}
\end{eqnarray}

Equations for the cases where $x$ is free in $D{\cwc{u}}$

The structure of the proofs is the same. Depending on $z \in \fv(v)$,  $x \notin \fv(v)$, or $x \in \fv(D\cwc{u})$, we use a different equation from the figures as follows:

$x \notin \fv(D\cwc{u})$     $x \in \fv(D\cwc{u})$

$z \notin \fv(v)$ and $x \notin \fv(v)$     Use (<ref>)     Use (<ref>)

$z \notin \fv(v)$ and $x \in \fv(v)$     Use (<ref>)     Use (<ref>)

$z \in \fv(v)$ and $x \notin \fv(v)$     Use (<ref>)     Use (<ref>)

$z \in \fv(v)$ and $x \in \fv(v)$     Use (<ref>)     Use (<ref>)

For example, we take the case where $z \in \fv(v)$,  $x \notin \fv(v)$, and $x \in \fv(D\cwc{u})$.

\begin{eqnarray*}
& \tra{C\cwc{x}[x/u]}\\
= & \ALC(\tra{v}[z/\tra{D\cwc{x}}][\fresh{z}/\tra{D\cwc{x}}][x/\tra{u}][\fresh{x}/\tra{u}])\\
= & \ALC(\tra{v}[z/\ALC(\tra{D\cwc{x}}[x/\tra{u}])][\fresh{z}/\ALC(\tra{D\cwc{x}}[x/\tra{u}])][\fresh{x}/\tra{u}])\\
\Rewplus{\les} &
\ALC(\tra{v}[z/\ALC(\tra{D\cwc{u}}[x/\tra{u}])][\fresh{z}/\ALC(\tra{D\cwc{u}}[x/\tra{u}])][\fresh{x}/\tra{u}])\\
= & \ALC(\tra{v}[z/\tra{D\cwc{u}}][\fresh{z}/\tra{D\cwc{u}}][x/\tra{u}][\fresh{x}/\tra{u}])\\
= & \tra{C\cwc{u}[x/u]}
\end{eqnarray*}

Thus for example,
let $z \in \fv(v)$,  $x \notin \fv(v)$, and $x \in \fv(D\cwc{u})$. Then,

\begin{eqnarray*}
& \tra{C\cwc{x}[x/u]}\\
= & \ALC(\tra{v}[z/\tra{D\cwc{x}}][\fresh{z}/\tra{D\cwc{x}}][x/\tra{u}][\fresh{x}/\tra{u}])\\
= & \ALC(\tra{v}[z/\ALC(\tra{D\cwc{x}}[x/\tra{u}])][\fresh{z}/\ALC(\tra{D\cwc{x}}[x/\tra{u}])][\fresh{x}/\tra{u}])\\
&\mbox{(use (\ref{EqSimproof7}) and~\cref{l:adding-independent-subsi}.\ref{l:adding-independent-subsia})}\\
\Rewplus{\les} & \ALC(\tra{v}[z/\ALC(\tra{D\cwc{u}}[x/\tra{u}])][\fresh{z}/\ALC(\tra{D\cwc{u}}[x/\tra{u}])][\fresh{x}/\tra{u}])\\
= & \ALC(\tra{v}[z/\tra{D\cwc{u}}][\fresh{z}/\tra{D\cwc{u}}][x/\tra{u}][\fresh{x}/\tra{u}])\\
= & \tra{C\cwc{u}[x/u]}
\end{eqnarray*}

Let $z \notin \fv(v)$,  $x \notin \fv(v)$, and $x \notin \fv(D\cwc{u})$.

\begin{eqnarray*}