1–LABEL:LastPageMar. 20, 2017Jun. 22, 2018

# An estimation for the lengths of reduction sequences of the
$\lambda\mu\rho\theta$-calculus

Péter Battyányi  Department of Computer Science, Faculty of Informatics,
University of Debrecen, Kassai út 26, 4028 Debrecen, Hungary
<EMAIL_ADDRESS>and  Karim Nour  Univ. Grenoble Alpes, Univ.
Savoie Mont Blanc, CNRS, LAMA, 73000 Chambéry, France<EMAIL_ADDRESS>
###### Abstract.

Since it was realized that the Curry-Howard isomorphism can be extended to the
case of classical logic as well, several calculi have appeared as candidates
for the encodings of proofs in classical logic. One of the most extensively
studied among them is the $\lambda\mu$-calculus of Parigot [Par.92]. In this
paper, based on the result of Xi presented for the $\lambda$-calculus [Xi.99],
we give an upper bound for the lengths of the reduction sequences in the
$\lambda\mu$-calculus extended with the $\rho$\- and $\theta$-rules.
Surprisingly, our results show that the new terms and the new rules do not add
to the computational complexity of the calculus despite the fact that
$\mu$-abstraction is able to consume an unbounded number of arguments by
virtue of the $\mu$-rule.

###### Key words and phrases:

classical logic ; $\lm$-calculus ; standardization ; length of reduction
sequence

##  1\. Introduction

###  1.1. The Curry-Howard isomorphism for classical logic

In the early nineties it was realized that the Curry-Howard isomorphism can be
extended to the case of classical logic [Gri.90, Mur.91]. Since then several
calculi have appeared aiming to give an encoding of proofs formulated either
in classical natural deduction or in classical sequent calculus [BaBe.96,
CuHe.00, Par.92, ReSo.94].

A noteworthy example of a calculus establishing a correspondence between terms
and natural deduction proofs is the $\lambda\mu$-calculus presented by Parigot
[Par.90], which stands very close in nature to the $\lambda$-calculus itself.
Besides the usual variables a new type of variables is introduced, the so-
called classical- or $\mu$-variables. The calculus enriched with the
$\mu$-variables is capable of representing proofs in classical natural
deduction by terms via the Curry-Howard isomorphism. The reduction rules
corresponding to the new $\lambda\mu$-terms are defined in [Par.92]. In
addition, further simplification rules, for example the $\rho$\- and
$\theta$-rules, and the symmetric counterpart of the $\mu$-rule, which is the
$\mu^{\prime}$-rule, were defined for the $\lambda\mu$-calculus [Par.92,
Par.93]. The motivation for introducing the $\mu^{\prime}$-rule, and the
simplification rules $\rho$ and $\theta$, was the following. In the typed
$\lambda$-calculus we are able to define integers by Church’s numerals and
other data types in the usual manner [Kri.91]. For the Church numerals and the
data types the unicity of representation of data holds. This means that, if we
talk about the Church numerals only, every term of type $N$, where $N$ is a
type of a Church numeral, is $\beta$-equal to a Church numeral. This is no
more true for the $\lambda\mu$-calculus: we can find normal terms of type $N$
that are not Church numerals. The problem is resolved by introducing a
symmetric equivalent of the $\mu$-rule and some more reduction rules, namely
the $\rho$\- and the $\theta$-rules [Par.93]. We should remark that the price
for adding more rules to the calculus other than the $\beta$\- and $\mu$-rules
was the disappearance of the usual proof theoretical properties, like
confluence, in case of the $\lambda\mu\mu^{\prime}$-calculus. Even strong
normalization is lost, when we consider the symmetric $\lambda\mu$-calculus
together with the $\rho$-rule [Bat.07]. Parigot has already showed in [Par.97]
that the $\lambda\mu$-calculus, i.e. when we consider the $\beta$\- and the
$\mu$-rules only, is strongly normalizing: his proof was based on the Tait-
Girard reducibility method [Tai.67]. An arithmetical proof of the same result
was presented by David and Nour [DaNo.03].

###  1.2. The work of Xi

Prior to presenting the work of Xi, we give an example which shows that the
length of a reduction sequence can be exponential in terms of the complexity
of a term even in the case of the simply typed $\lambda$-calculus. We define a
sequence of simple types with recursion. Let $N_{0}=(X\rightarrow
X)\rightarrow(X\rightarrow X)$, where $X$ is a type variable and, for every
$i\in\mathbb{N}$, $N_{i+1}=(N_{i}\rightarrow
N_{i})\rightarrow(N_{i}\rightarrow N_{i})$. For every $n\in\mathbb{N}$ we
denote by $\underline{n}$ the $n$-th Church numeral. Let
$n_{1},...,n_{m}\in\mathbb{N}$ and
$P=(\underline{n_{m}}\;(...\;(\underline{n_{3}}\;\;(\underline{n_{2}}\;\;\underline{n_{1}}))\;...))$.
It is easy to check that $P$ is of type $N_{m-1}\rightarrow N_{m-1}$ and
reduces to the Church numeral $\underline{{n_{m}}^{.^{.^{.^{{\scriptstyle
n_{2}}^{{{\scriptstyle n_{1}}}}}}}}}$ in ${n_{m}}^{.^{.^{.^{{\scriptstyle
n_{2}}^{{{\scriptstyle n_{1}}}}}}}}$ steps of $\beta$-reductions.

In his paper [Xi.99], Xi obtains an upper bound for the lengths of reduction
sequences of the simply typed $\lambda$-calculus. First of all, he finds a
bound for the leftmost reduction sequences of the $\lambda$I-calculus. Since
any reduction sequence of a $\lambda$I-term is at most as long as the leftmost
one, he has immediately found a bound for the $\lambda$I-calculus. Next, he
maps the set of $\lambda$-terms into the set of $\lambda$I-terms such that,
for any reduction sequence of a $\lambda$-term, he can find a reduction
sequence of the corresponding $\lambda$I-term which is at least as long. As
our starting example shows, it is inevitable that this bound will be
exponential in relation to the complexity (the number of symbols) of the term
and/or the rank (the number of arrows) of the type of the term. In our
treatment we chose to develop Xi’s method further, since, when aiming to find
the terms with longest reduction sequences, $\lambda\mu$I-terms appeared to be
promising candidates and, among their reduction sequences, the standard ones
turned out to be the ones with longest reduction paths.

An improvement of Xi’s method appeared in the work of Asperti and Lévy
[AsLe.13]. They gave a refinement of Xi’s result which proved to be a
considerable strengthening of the bound especially in the cases when the
computation leads to normal forms of a sufficiently simple structure (e.g. a
variable or booleans). They showed that in these cases the length of the
longest reduction sequence is at most a factorial of that of the shortest one.

###  1.3. The motivations of our work

First of all, we note that the motivation for the introduction of the
$\lambda\mu$-calculus was not the enhancement of the expressive power of the
$\lambda$-calculus but rather the need for representing program constructs,
like $exit$, $call/CC$, which were missing from the simply typed
$\lambda$-calculus. The power of the new calculus stems from the fact that a
$\mu$-abstraction can consume any number of arguments through subsequent
reductions.

Interestingly, our results show that the upper bound for the number of
reduction steps of a term in the $\lambda\mu$-calculus stays close to the
expression giving an upper bound for the $\lambda$-calculus. One expects that
this bound should increase in comparison with the $\lambda$-calculus, since
the $\lambda\mu$-calculus properly contains the $\lambda$-calculus.

Intuitively, one should try to simulate the $\lambda\mu$-calculus with the
help of the $\lambda$-calculus and hence obtain a bound for the lengths of the
reduction sequences. This type of simulation has two defects: first of all,
the upper bound for the lengths would grow considerably and, secondly,
additional difficulties would come up when we want to simulate the
simplification rules (for a detailed explanation see Section 5). Hence, in
spite of the expected difficulties with respect to the handling of critical
pairs and, consequently, with relation to the choice of the definition of
standard reduction sequences, we have voted for the adaptation of Xi’s method.

There are several works concerning the standardization of the
$\lambda\mu$-calculus [Bat.07, DaNo1.05, Py.98, Sau.10]. David and Nour
[DaNo1.05] consider standardization of the $\lambda\mu$-calculus without
simplification rules, while Py [Py.98] chooses simplification rules by which
the confluence is retained in the extended calculi. This eliminates the
difficulties imposed on the treatment of the critical pairs. A different
aspect is that of Saurin [Sau.10]. He works with essentially the same
calculus: basically, he considers the rules $\beta$, $\mu$, $\rho$ and
$\theta$, which are sufficient to obtain confluency in the calculus. In his
calculus, he also applies some other- local and global- simplification rules
besides the already mentioned ones. In spite of the complexity of this
calculus, Saurin succeeds in defining the notion of a standard reduction
sequence and he also obtains a standardization theorem. His definition follows
the traditional way: he uses the notion of residuals (one cannot reduce the
residual of a redex lying to the left of a redex reduced). This results in a
rather technical proof. However, none of the works mentioned contain
estimations for the lengths of standard reduction sequences. Instead of the
traditional way, we chose to define the notion of a standard reduction
sequence following the style of David [DaNo1.05] so that the proofs can be
carried out by recursion on the lengths of the reduction sequences.

###  1.4. Outline of the present work

In this paper, following the reasoning of Xi [Xi.99] for the simply typed
$\lambda$-calculus, we present an upper bound for the lengths of the reduction
sequences in the $\lambda\mu\rho\theta$-calculus in terms of the complexity
and the rank of the term $M$, where the rank of $M$ is the maximum of its
redex ranks and the complexity of a term is the number of symbols in $M$. We
base our treatment on [Bat.07]. First we prove a standardization theorem for
the $\lambda\mu$-calculus with the additional assertion that, in the case of
the $\lambda\mu$I-calculus the length of a reduction sequence is majorized by
that of its standardization, which is, in turn, bounded from above by a
certain measure defined in the paper. In addition, we show that, if $M$ is a
$\lambda\mu$I-term, then a standard reduction sequence leading to the normal
form of $M$ is the leftmost reduction sequence, which is necessarily unique.
This fits our intuition, as a matter of fact. Thus it makes no difference in
which way we are able to find the standard reduction sequence leading to the
normal form of $M$: it is by all means the longest reduction sequence
normalizing $M$. Thus, as our first task, we find an appropriate, normalizing
reduction sequence for $\lambda\mu$I-terms such that its standardization
provides us with a measure which is a super-exponential number theoretic
function and an upper bound for the length of the standard reduction sequence.
This is accomplished in Section 4. Hence, our strategy for a general term $M$
is to define a translation $[\\![M]\\!]_{k}$ of $M$ into the
$\lambda\mu$I-calculus such that the longest reduction sequence of $M$ is not
longer than the longest reduction sequence of $[\\![M]\\!]_{k}$. Since we have
already obtained a bound for the reduction sequences of $[\\![M]\\!]_{k}$, we
also have one for those of $M$.

###  1.5. Some difficulties and our proposed solutions

The new redexes, and especially the critical pairs, impose additional
difficulties: we reformulated the notion of a standard reduction sequence in
the $\lambda\mu\rho\theta$-calculus in line with the definition of standard
$\beta$-reduction sequences according to David [Dav.01]. The resulting notion
proved to be vastly different in appearance from that for the
$\lambda$-calculus. With the presence of the new rules overlapping redexes can
occur: performing a $\theta$-redex can make a $\mu$-redex to vanish and
executing a $\theta$-redex can make a $\rho$-redex to disappear and vice
versa. Our definition of a standard reduction sequence excludes these
situations: overlapping $\theta$\- and $\mu$-redexes are always considered
$\mu$-redexes. Likewise, in the case overlapping $\theta$\- and
$\rho$-redexes, a $\theta$-redex in not allowed to destroy the containing
$\rho$-redex and vice versa. We show that our choice is appropriate: we can
always find standard reduction sequences respecting these constraints. Due to
the presence of other reduction rules, finding the bound and proving that the
lengths of the reduction sequences obey that bound is more difficult even in
the case of $\lambda\mu$I-terms. Instead of treating as candidates every
possible $\lambda\mu$I-sequences of reductions for the estimation like Xi does
for the $\lambda$I-calculus, we compute the bound only by starting from a
special kind of $\lambda\mu$I-reduction sequence which we call good
$k$-normalization sequence. We evaluate the bound for the general case by
assigning a $\lambda\mu$I-term $[\\![M]\\!]_{k}$ with a certain $k$ to the
$\lambda\mu$-term $M$ such that the length of the longest reduction paths of
$[\\![M]\\!]_{k}$ is greater than or equal to that of $M$. Concerning the
general case, our transformation of $M$ into $[\\![M]\\!]_{k}$ is in fact a
correction of Xi’s argument [Xi.99], the original idea of Xi contained a
slight impreciseness. Namely, when $M$ is a $\lambda$-abstraction, we have to
apply case distinction deciding whether $M$ is the left hand side of a
$\beta$-redex or not. Otherwise the size of the corresponding
$\lambda\mu$I-term, $[\\![M]\\!]_{k}$, could not be estimated correctly.

As a general remark, we can observe that the bound obtained for the
$\lambda\mu$-calculus is exactly the same as the one obtained by Xi [Xi.99]
for the $\lambda$-calculus, except for the fact that the ranks of the redexes
and hence the measures of the reduction sequences are generalizations of the
corresponding notions for the $\lambda$-calculus. Perhaps, this surprising
result could be interpreted as an informal statement saying that the
computational complexity of the $\lambda\mu$-calculus has not been increased
by introducing the classical variables in the $\lambda$-calculus.

##  2\. The $\lambda\mu\rho\theta$-calculus

###  2.1. The syntax of calculus

The $\lambda\mu\rho\theta$-calculus was introduced by Parigot [Par.92].
Instead of his original calculus, we use a modified version owing to de Groote
[deG.98]: we apply the term formation rules in a more flexible way, that is,
we do not assume that a $\mu$-abstraction $(\mu\alpha.M)$ must be of the form
$(\mu\alpha.([\beta]M_{1}))$ for some $\beta$ and $M_{1}$. In what follows, we
give the appropriate definitions.

[Terms]

  1. (1)

There are two kinds of variables : the set of $\lambda$-variables
$\mathcal{V}=\\{x,y,z,\dots\\}$ and the set of $\mu$-variables
$\mathcal{W}=\\{\alpha,\beta,\gamma,\dots\\}$. The set of terms is denoted by
$\mathcal{T}$ and the term formation rules are:

$\mathcal{T}\;:=\;\mathcal{V}\;\mid\;({\lambda}\mathcal{V}.\mathcal{T})\;\mid\;(\mu\mathcal{W}.\mathcal{T})\;\mid\;([\mathcal{W}]\mathcal{T})\;\mid\;(\mathcal{T}\;\mathcal{T}).$

  2. (2)

The complexity of a term is defined as follows:

     * •

$comp(x)=1$,

     * •

$comp([\alpha]M)=comp(\lambda x.M)=comp(\mu\alpha.M)=comp(M)+1$,

     * •

$comp(M\,N)=comp(M)+comp(N)$.

  3. (3)

As usual we denote by $Fv(M)$ the set of variables ooccuring free in the term
$M$.

  4. (4)

Let $M$ and $N$ be terms. We write $N\leq M$ if $N$ is a subterm of $M$ and
$N<M$, if $N\leq M$ and $N\neq M$.

In brief, the complexity of a term is the number of symbols in the term. By
the formation of terms we apply the usual stipulations: the scope of the
$\lambda$\- and $\mu$-abstractions extend to the right as far as possible,
moreover, the abstractions are right associative, whereas the term application
is left associative. The calculus examined by us is the simply typed one, the
typing relation is presented in the next definition.

[Type system]

  1. (1)

The types are built from atomic formulas (or, in other words, atomic types)
and the constant symbol $\bot$ with the connector $\rightarrow$. As usual for
every type $A$, $\neg A$ is an abbreviation for $A\rightarrow\bot$.

  2. (2)

The length of a type $A$ (denoted by $lh(A)$) is defined as the number of
arrows of $A$.

  3. (3)

In the definition below, $\Gamma$ denotes a (possibly empty) context, that is,
a finite set of declarations of the form $x:A$ (resp. $\alpha:\neg A$) for a
$\lambda$-variable $x$ (resp. a $\mu$-variable $\alpha$) and type $A$ such
that a $\lambda$-variable $x$ (resp. a $\mu$-variable $\alpha$) occurs at most
once in an expression $x:A$ (resp. $\alpha:\neg A$) of $\Gamma$. The typing
rules are:

$\displaystyle\frac{}{\Gamma,x:A\;\vdash\;x:A}\;ax$

$\;\;\;\;\;\;\;\;\;\;\displaystyle\frac{\Gamma,x:A\;\vdash\;M:B}{\Gamma\;\vdash\;\lambda x.M:A\rightarrow B}\;{\rightarrow}_{i}$ | $\;\;\;\;\;\;\;\;\displaystyle\frac{\Gamma\;\vdash\;M:A\rightarrow B\;\;\;\;\;\Gamma\;\vdash\;N:A}{\Gamma\;\vdash\;M\,N:B}\;{\rightarrow}_{e}$
---|---

$\;\;\;\;\;\;\;\;\;\;\displaystyle\frac{\Gamma,\alpha:\neg A\vdash\;M:A}{\Gamma,\alpha:\neg A\;\vdash\;[\alpha]M:\bot}\;{\bot}$ | $\;\;\;\;\;\;\;\;\displaystyle\frac{\Gamma,\alpha:\neg A\;\vdash\;M:\bot}{\Gamma\vdash\;\mu\alpha.M:A}\;{\mu}$
---|---

  4. (4)

We will say that a term $M$ is typable with $A$, if there is a set of
declarations $\Gamma$ such that $\Gamma\;\vdash\;M:A$ holds.

[Reduction rules]

  1. (1)

We have four kinds of redexes

     * •

a $\beta$-redex : term of the form $(\lambda x.M)N$,

     * •

a $\mu$-redex : term of the form $(\mu\alpha.M)N$,

     * •

a $\rho$-redex : term of the form $[\alpha]\mu\beta.M$,

     * •

a $\theta$-redex : term of the form $\mu\alpha.[\alpha]M$ and $\alpha\not\in
Fv(M)$.

We denote by $NF$ the set of normal forms i.e. terms without redex.

  2. (2)

The reduction rules are as follows:

     * •

The $\beta$-reduction rule is $(\lambda x.M)N\rightarrow_{\beta}M[x:=N]$

where $M[x:=N]$ is obtained from $M$ by replacing every $x$ in $M$ by $N$.

     * •

The $\mu$-reduction rule is
$(\mu\alpha.M)N\rightarrow_{\mu}\mu\alpha.M[\alpha:{=}_{r}N]$

where $M[\alpha:{=}_{r}N]$ is obtained from $M$ by replacing every subterm in
$M$ of the form $[\alpha]U$ by $[\alpha](U\;N)$.

     * •

The $\rho$-reduction is $[\alpha]\mu\beta.M\rightarrow_{\rho}M[\beta:=\alpha]$

where $M[\beta:=\alpha]$ is obtained by exchanging in $M$ every free
occurrence of $\beta$ for $\alpha$.

     * •

The $\theta$-reduction is $\mu\alpha.[\alpha]M\rightarrow_{\theta}M$ provided
$\alpha\not\in Fv(M)$.

  3. (3)

Let $R$ be a redex of $M$. We write $M\rightarrow^{R}N$ if $N$ is the term $M$
after the reduction of $R$. If
$M=M_{1}\rightarrow^{R_{1}}M_{2}\rightarrow^{R_{2}}\dots\rightarrow^{R_{n}}M_{n+1}=N$,
then $\sigma=[R_{1},\dots,R_{n}]$ denotes this reduction sequence,
$n=|\sigma|$ and we write $M\mapsto^{\sigma}N$.

  4. (4)

Let $\sigma$, $\nu$ be (possibly empty) sequences of reductions. Then
$\sigma\\#\nu$ denotes their concatenation. Let $\sigma=[R_{1},\dots,R_{n}]$.
We denote by $\sigma[x:=M]$ (resp. $\sigma[\alpha:=_{r}M]$) the reduction
sequence $[R_{1}[x:=M],\dots,R_{n}[x:=M]]$ (resp.
$[R_{1}[\alpha:=_{r}M],\dots,R_{n}[\alpha:=_{r}M]]$). Moreover, let
$\sigma[\alpha:=\beta]$ denote the reduction sequence
$[R_{1}[\alpha:=\beta],\dots,R_{n}[\alpha:=\beta]]$.

  5. (5)

As it is customary, by a reduction step we mean the closure of the reduction
relation compatible with respect to the term formation rules. In general
$\rightarrow$ denotes the compatible closure of a reduction relation, or that
of the union of some set of relations, while by $\mapsto$ we mean the
reflexive, transitive closure of $\rightarrow$. Sometimes we write
$M\mapsto^{n}N$ if $M$ is reduced with $n$ steps of reductions to $N$.

  6. (6)

If $M$ is strongly normalizing i.e. $M$ has no infinite reduction sequences,
then, by König’s infinity lemma, $\eta(M)$ will denote the length of the
longest reduction sequence starting from $M$.

We present below some theoretical properties of the
$\lambda\mu\rho\theta$-calculus.

######  Theorem 1 (Church-Rosser property).

Let $M_{1}$, $M_{2}$ and $M_{3}$ be terms such that $M_{1}\mapsto M_{2}$ and
$M_{1}\mapsto M_{3}$. Then there exists an term $M_{4}$ for which
$M_{2}\mapsto M_{4}$ and $M_{3}\mapsto M_{4}$.

A proof of the above assertion can be found in the papers of Parigot [Par.92],
Py [Py.98] or Rozière [Roz.03]. Py [Py.98] expounded the question to a greater
extent together with the results belonging to the topic.

######  Proposition 2 (Type preservation property).

Let $M$, $N$ and $A$, $\Gamma$ be such that $\Gamma\;\vdash\;M:A$ and
$M\mapsto N$. Then $\Gamma\;\vdash\;N:A$.

The property can be verified by double induction on the length of the
reduction sequence $M\mapsto N$ and the complexity of $M$.

######  Theorem 3 (Strong normalization).

If $M$ is a typable term, then $M$ is strongly normalizing i.e. every
reduction sequence starting from $M$ is finite.

There are several proofs of this result in the literature. Consider, for
example, Parigot [Par.97], David and Nour [DaNo.03]. In [deG.01], de Groote
proves the strong normalization of the simply typed $\lambda\mu$-calculus
extended with terms of conjunctive and disjunctive types, respectively. He
does not consider the $\rho$\- and $\theta$-reduction rules in his calculus.
Albeit, we aim to find an upper bound for the reduction sequences of the
$\lambda\mu$-calculus enriched with the $\rho$\- and $\theta$-rules, as a by-
product we also obtain a proof for the strong normalization of the
$\lambda\mu\rho\theta$-calculus. We consider fewer simplification rules than
Saurin [Sau.10], however, our notion of standardness is formulated in a
different form which enables us to prove statements concerning standard
reduction sequences by induction on the complexity of terms.

In this paper we consider only simply typed $\lambda\mu$-terms. The typing
relations involve that a $\mu$-variable cannot have but one argument, that is,
we are not allowed to formulate terms of the form $(([\alpha]M)\;N)$, where
$\alpha$ is a $\mu$-variable and $M$, $N$ are arbitrary terms.

###  2.2. Head and leftmost reductions

In order to proceed to the standardization theorem, we define the notions of
head- and leftmost reduction sequences. Both are special cases of the standard
reduction sequences discussed in the next section.

  1. (1)

Let $M$ be a term and $\overrightarrow{P}$ a possibly empty sequence of terms
$P_{1},\dots,P_{n}$. We write $(M\;\overrightarrow{P})$ for the term
$(\dots((M\;P_{1})\;P_{2})\;\dots P_{n})$, which also is denoted by
$(M\;P_{1}\dots P_{n})$.

  2. (2)

Let $M=(P_{1}\dots P_{n})=(P_{1}\;\overrightarrow{P})$, with a possibly empty
sequence of terms $\overrightarrow{P}$. Then, for $2\leq i\leq n$, we write
$P_{i}\in\overrightarrow{P}$ and we call $P_{i}$ $(2\leq i\leq n)$ the
components of $\overrightarrow{P}$ or the arguments of $P_{1}$.

  3. (3)

Let $\overrightarrow{P}=P_{1}\ldots P_{n}$. We write
$\overrightarrow{P}\mapsto^{\sigma}\overrightarrow{P^{\prime}}$, where
$\sigma=\sigma_{1}\\#\ldots\\#\sigma_{n}$ is such that
$P_{i}\mapsto^{\sigma_{i}}P_{i}^{\prime}$ $(1\leq i\leq n)$.

######  Lemma 4.

Every term $M$ of the simply typed $\lambda\mu\rho\theta$-calculus can be
written uniquely in one of the following forms.

  1. (1)

$M$ is a variable,

  2. (2)

$M=\lambda x.M_{1}$, or $M=\mu\alpha.M_{1}$ and $M$ is not a $\theta$-redex,
or $M=[\alpha]M_{1}$ and $M$ is not a $\rho$-redex,

  3. (3)

$M=(x\;M_{1}\overrightarrow{P})$,

  4. (4)

$M=(\lambda x.M_{1})M_{2}\overrightarrow{P}$, or
$M=(\mu\alpha.M_{1})M_{2}\overrightarrow{P}$,

  5. (5)

$M=[\alpha]\mu\beta.M_{1}$, or $M=\mu\alpha.[\alpha]M_{1}$ and $\alpha\notin
Fv(M_{1})$.

######  Proof 2.1.

By induction on $comp(M)$.

In the following definitions the functions $hr$ and $lr$ are undefined in the
cases not mentioned explicitly.

  1. (1)

The head-redex of a term $M$, in notation $hr(M)$, is defined as follows.

     * •

$hr(\lambda x.M)=hr(M)$,

     * •

$hr(\mu\alpha.M)=\mu\alpha.M$ if $\mu\alpha M$ is a $\theta$-redex, and
$hr(\mu\alpha.M)=hr(M)$ otherwise,

     * •

$hr([\alpha]M)=[\alpha]M$ if $[\alpha]M$ is a $\rho$-redex, and
$hr([\alpha]M)=hr(M)$ otherwise,

     * •

$hr((\mu\alpha.M_{1})M_{2}\overrightarrow{P})=(\mu\alpha.M_{1})M_{2}$,

     * •

$hr((\lambda x.M_{1})M_{2}\overrightarrow{P})=(\lambda x.M_{1})M_{2}$.

If $M=(\mu\alpha.M_{1})M_{2}\overrightarrow{P}$, then a critical pair of
redexes can emerge provided $(\mu\alpha.M_{1})$ is a $\theta$-redex as well.
In this situation we always choose the $\mu$-redex $(\mu\alpha.M_{1})M_{2}$ as
the head-redex of $M$.

  2. (2)

Let
$M_{1}\rightarrow^{R_{1}}M_{2}\rightarrow^{R_{2}}\dots\rightarrow^{R_{n}}M_{n+1}$.
Then $\sigma=[R_{1},\dots,R_{n}]$ is a head-reduction sequence, if, for each
$1\leq i\leq n$, $R_{i}$ is the head-redex of $M_{i}$. We denote by
$M\mapsto_{hd}N$ the fact that $M$ reduces to $N$ via a head-reduction
sequence.

  1. (1)

The leftmost-redex of a term $M$, in notation $lr(M)$, is defined as follows.

     * •

$lr(\lambda x.M)=lr(M)$,

     * •

$lr(\mu\alpha.M)=\mu\alpha.M$ if $\mu\alpha M$ is a $\theta$-redex, and
$lr(\mu\alpha.M)=lr(M)$ otherwise,

     * •

$lr([\alpha]M)=[\alpha]M$ if $[\alpha]M$ is a $\rho$-redex, and
$lr([\alpha]M)=lr(M)$ otherwise,

     * •

$lr((\mu\alpha.M_{1})M_{2}\overrightarrow{P})=(\mu\alpha.M_{1})M_{2}$,

     * •

$lr((\lambda x.M_{1})M_{2}\overrightarrow{P}))=(\lambda x.M_{1})M_{2}$,

     * •

$lr(x\;M_{1}\;M_{2}\dots M_{n})=lr(M_{i})$ provided $M_{i}\notin NF$ and
$M_{j}\in NF$ $(1\leq j\leq i-1)$.

  2. (2)

A reduction sequence
$M_{1}\rightarrow^{R_{1}}M_{2}\rightarrow^{R_{2}}\dots\rightarrow^{R_{n}}M_{n+1}$
is the leftmost-reduction sequence from $M_{1}$ to $M_{n+1}$ if $R_{i}$ is the
leftmost-redex of $M_{i}$ $(1\leq i\leq n)$. We denote by $M\mapsto_{lrs}N$
the fact that $M$ reduces to $N$ via a leftmost-reduction sequence. Then the
reduction sequence itself is denoted by $lrs(M\mapsto N)$. If
$M\mapsto^{\sigma}N$ and $\sigma$ is a leftmost reduction sequence, then
$\sigma$ is unique.

Following the tradition of relating head reduction sequences to leftmost
reduction sequences in the case of the $\lambda$-calculus [Bar.85], we compare
briefly the two notions of reductions.

######  Lemma 5.

Every head-reduction sequence is a leftmost-reduction sequence.

######  Proof 2.2.

A straightforward induction on the complexity of the term, comparing the
various subcases of Definitions 2.2 and 2.2.

We give a sketch of the proof that every leftmost-reduction sequence is the
concatenation of head-reduction sequences, however. To this end, we first
settle what we mean by a term being in head-normal form.

A term $M$ is in head-normal form (in notation $M\in HNF$), if one of the
following cases is valid.

  1. (1)

$M=\lambda x.M_{1}$ and $M_{1}\in HNF$,

  2. (2)

$M=(x\;M_{1}\ldots M_{k})$,

  3. (3)

$M=\mu\alpha.M_{1}$, $M$ is not a $\theta$-redex and $M_{1}\in HNF$,

  4. (4)

$M=[\alpha]M_{1}$, $M$ is not a $\rho$-redex and $M_{1}\in HNF$.

We say that $M^{\prime}\in HNF$ is a head-normal form of $M$, if
$M\mapsto_{hd}M^{\prime}$. Observe that, since the typed
$\lambda\mu\rho\theta$-calculus is strongly normalizing, every term has a
unique head-normal form.

Prior to detailing the connection between leftmost reduction and head
reduction, we introduce a new notion.

Let $M\in HNF$.

  1. (1)

The core of $M$, in notation $core(M)$, is defined as follows.

     * •

If $M=\lambda x.M_{1}$, or $M=\mu\alpha.M_{1}$, or $M=[\alpha]M_{1}$, then
$core(M)=core(M_{1})$.

     * •

If $M=x$, or $M=(M_{1}\;M_{2})$, then $core(M)=M$.

Observe that, if $M\in HNF$, $core(M)$ can be obtained from $M$ if we omit the
initial $\lambda$-, $\mu$-prefixes or $\mu$-variables standing in front of
$M$.

  2. (2)

Assume $core(M)=(x\;\overrightarrow{P})$ with a possibly empty
$\overrightarrow{P}$. Then we call the components of $\overrightarrow{P}$ the
components of $M$, as well.

Intuitively, a leftmost reduction sequence is a head reduction sequence until
the term reaches a head normal form. At this point, the leftmost reduction
sequence is the concatenation of leftmost reduction sequences of the
components. This is the content of the lemma below.

######  Lemma 6.

Let $M\mapsto^{\sigma}M^{\prime\prime}$ be a leftmost reduction sequence and
assume $M^{\prime\prime}\in NF$. Then there exists $M^{\prime}\in HNF$ and
$\sigma^{\prime}$, $\sigma^{\prime\prime}$ such that
$M\mapsto^{\sigma^{\prime}}M^{\prime}\mapsto^{\sigma^{\prime\prime}}M^{\prime\prime}$,
where $\sigma^{\prime}$ is a head reduction sequence and, if
$core(M^{\prime})=(x\;M_{1}^{\prime}\ldots M_{k}^{\prime})$, then
$\sigma^{\prime\prime}=\nu_{1}\\#\ldots\\#\nu_{k}$ such that
$core(M^{\prime\prime})=(x\;M_{1}^{\prime\prime}\ldots M_{k}^{\prime\prime})$,
$M_{i}^{\prime}\mapsto^{\nu_{i}}M_{i}^{\prime\prime}$ and $\nu_{i}$ are
leftmost reduction sequences $(1\leq i\leq k)$.

######  Proof 2.3.

By induction on $comp(M)$ taking into account the subcases of Definition 2.2.
Let $M\mapsto_{lrs}^{\sigma}M^{\prime\prime}$ and assume
$\sigma=[R]\\#\widehat{\sigma}$. A straightforward observation of the points
of Definitions 2.2 and 2.2 gives that, if $M^{\prime\prime}\notin HNF$, then
$R$ is the head redex of $M$. Hence we may assume
$M\mapsto^{\sigma^{\prime\prime}}M^{\prime\prime}$, where $M\in HNF$. Then, by
induction on $comp(M)$, we obtain that we may suppose that $M=x$ or
$M=(x\;M_{1}\ldots M_{n})$. By Definition 2.2, both assumptions immediately
yield the result.

###  2.3. Other definitions

We define in this subsection the notion of a $\lambda\mu$I-term and a
$\lambda\mu$I-redex, together with some main properties of the
$\lambda\mu$I-calculus.

  1. (1)

The set of $\lambda\mu I$-terms is defined inductively as follows:

     * •

$x$ is a $\lambda\mu I$-term,

     * •

$\lambda x.M$ is a $\lambda\mu I$-term provided $M$ is a $\lambda\mu I$-term
and $x\in Fv(M)$,

     * •

$(M\;N)$ is a $\lambda\mu I$-term if $M$ and $N$ are $\lambda\mu I$-terms,

     * •

$\mu\alpha.M$ is a $\lambda\mu I$-term provided $M$ is a $\lambda\mu I$-term
and $\alpha\in Fv(M)$,

     * •

$[\alpha]M$ is a $\lambda\mu I$-term provided $M$ is a $\lambda\mu I$-term.

  2. (2)

If $M=(\lambda x.M_{1})M_{2}$ (resp. $M=(\mu\alpha.M_{1})M_{2}$, where
$\lambda x.M_{1}$ (resp. $\mu\alpha.M_{1}$) and $M_{2}$ are
$\lambda\mu$I-terms, then $M$ is called a $\lambda\mu$I-redex.

It is easy to see that, if $M$ is a $\lambda\mu$I-term and $M\mapsto
M^{\prime}$, then $M^{\prime}$ is a $\lambda\mu$I-term. Thus, it is clear that
this calculus also has the following three properties: Church-Rosser-property,
type preservation and strong normalization.

The next section is concerned with a standardization result in the
$\lambda\mu\rho\theta$-calculus. In the sequel, we are going to use the
notions of subterms, redexes, reduction sequences, residuals etc. in an
intuitive manner.

A reduction sequence
$M_{1}\rightarrow^{R_{1}}M_{2}\rightarrow^{R_{2}}\ldots\rightarrow^{R_{n}}M_{n+1}$
is a sequence of terms and redex occurrences, where $M_{i+1}$ is obtained by
reducing with $R_{i}$ in $M_{i}$ $(1\leq i\leq n)$. In what follows, by an
abuse of notation, a reduction sequence will be referred to without noting
explicitly the exact occurrences of the redexes in the terms, if they are
clear from the context. We give a short account of the intuitive notions for
residuals and involvement of redexes.

  1. (1)

Let $M\rightarrow^{R}M^{\prime}$ be a reduction step.

    1. (a)

If $R=(\lambda x.R_{1})R_{2}<M$, then $R$ and $\lambda x.R_{1}$ have no
residuals, otherwise, if $(\lambda x.R_{1})R_{2}<U\leq M$, we obtain the
residual of $U$ by exchanging $(\lambda x.R_{1})R_{2}$ for $R_{1}[x:=R_{2}]$
in $U$. When $U\leq R_{1}$, then we obtain the residual by substituting each
occurrence of $x$ by $R_{2}$ in $U$. In the case of $U\leq R_{2}$, the
residual of $U$ is the same, only its position changes in $M^{\prime}$: its
index will be one of the indices of a former occurrence of $x$ in $R_{1}$. If
$R$ and $U$ are disjoint, then the residual of $U$ is $U$ itself.

    2. (b)

The situations are analogous in the cases of the other redexes: if
$R=(\mu\alpha.R_{1})R_{2}$, then $R$ has no residual, if
$R=[\alpha]\mu\beta.R_{1}$, then $R$ and $\mu\beta.R_{1}$ have no residuals,
and, finally, if $R=\mu\alpha.[\alpha]R_{1}$, then $R$ and $[\alpha]R_{1}$
have no residuals. Besides these afore-said cases, if $R<U\leq M$, then we
obtain the residual of $U$, if we execute the redex $R$ in $U$. When $U<R$ and
$U$ has a residual: if $R=(\mu\alpha.R_{1})R_{2}$ and $U\leq R_{1}$, we obtain
the residual by recursively exchanging every subterm $[\alpha]P$ of $U$ by
$[\alpha](P\;R_{2})$. If $U\leq R_{2}$, then the residual is $U$ only its
index changes in $M^{\prime}$. Otherwise, for $U\leq R_{1}$ and
$R=[\alpha]\mu\beta.R_{1}$, the residual is $U[\beta:=\alpha]$. If $U\leq
R_{1}$ and $R=\mu\alpha.[\alpha]R_{1}$, then the residual is $U$ just the
index is modified in $M^{\prime}$.

  2. (2)

Residuals of terms with respect to reduction sequences are defined in a
recursive way: we obtain the residuals with respect to a reduction sequence if
we compute the residuals of the residuals with respect to subsequences of the
reduction sequence.

  3. (3)

Let $\sigma$ be the reduction sequence
$M_{1}\rightarrow^{R_{1}}M_{2}\rightarrow^{R_{2}}\ldots\rightarrow^{R_{n}}M_{n+1}$,
assume $R\leq M_{1}$ is a redex. Then we say that $R$ is involved in $\sigma$,
if there is an $1\leq i\leq n$ such that $R=R_{i}$ and $R_{i}$ is a residual
of $R$ with respect to
$M_{1}\rightarrow^{R_{1}}\ldots\rightarrow^{R_{i-1}}M_{i}$.

In what follows, most of the proofs will follow an induction on
lexicographically ordered tuples of integers. Ordering of tuples is understood
in the usual lexicographic manner: $(n,m)\leq(n^{\prime},m^{\prime})$ iff
either $n<n^{\prime}$ or $n=n^{\prime}$ and $m\leq m^{\prime}$.

##  3\. Standardization for the $\lambda\mu\rho\theta$-calculus

Our results concerning the standardization of the $\lambda\mu$-calculus are
not the strongest ones. In fact, some of our statements are valid for the
$\lambda\mu$I-calculus only. A standardization result can be found in the
paper of Saurin [Sau.10], where, besides the rules mentioned in our article,
some other rules are taken into account. Our only concern with the
standardization is our aim to find an upper bound for the reduction sequences
of the $\lambda\mu$-calculus. In the present subsection we define a notion of
a standard reduction sequence for the $\lambda\mu\rho\theta$-calculus and find
some assertions concerning their lengths. Many of the proofs are adaptations
of the ones related to the simply typed $\lambda$-calculus in [Xi.99]. The
result itself, however, is not a simple generalization of Xi’s method. In the
presence of $\mu$-, $\rho$\- and $\theta$-reductions overlapping redexes mean
the greatest obstacle to a straightforward formulation of standardness. We
suggest the following solution to this problem. We define the notion of a
standard reduction sequence such that every standard reduction sequence should
obey the following properties: when a redex, which is simultaneously a $\mu$\-
and a $\theta$-redex, is involved in a standard reduction sequence, we
stipulate that the redex should be understood only as a $\mu$-redex. Likewise,
when a $\theta$-redex would destroy a containing $\rho$-redex we prohibit
reducing the $\theta$-redex, and when a $\rho$-redex would make a containing
$\theta$-redex disappear, we forbid the $\rho$-redex until the $\theta$-redex
exists. These raise additional issues in the estimation of the lengths of
standard reduction sequences: we must take into account the numbers of
arguments of such $\theta$-redexes that are simultaneously $\mu$-redexes and
we must exclude some reduction sequences from the set of standard reduction
sequences in order to deal with the overlapping $\rho$\- and $\theta$-redexes.
These considerations are reflected in the definition of a standard reduction
sequence and in the measure for a term presented in Definition 3.3. We show
that our suggestion for a solution is appropriate: we can majorize every
reduction sequence by a standard reduction sequence of Definition 3.1.

We should remark that the widely known and intuitive definition requires of a
standard reduction sequence that no redex is a residual of a redex which lies
to the left of some other redex in the sequence [Bar.85]. Instead of this, we
use a definition of a standard reduction sequence similar to the one applied
in [Dav.01], which enables us to prove properties concerning standard
reduction sequences by induction on the complexity of terms.

###  3.1. Standard reduction sequences in the $\lambda\mu\rho\theta$-calculus

In this subsection we define the notion of a standard
$\beta\mu\rho\theta$-reduction sequence and present some elementary lemmas
concerning properties of standard reduction sequences. In the definition
below, we clarify what we mean by a standard $\beta\mu\rho\theta$-reduction
sequence. The definition is structured by induction on the lexicographically
ordered pair $(|\sigma|,comp(M))$. A reduction sequence $M\mapsto^{\sigma}N$
is standard if, either it is empty, or one of the following cases holds.

  1. (1)

$M=\lambda x.M_{1}$, $N=\lambda x.N_{1}$, $M_{1}\mapsto^{\sigma}N_{1}$ and
$\sigma$ is standard.

  2. (2)

If $M=\mu\alpha.M_{1}$, let $M\mapsto^{\sigma}N$ be $M=P_{1}\rightarrow
P_{2}\rightarrow\ldots\rightarrow P_{k+1}=N$.

    1. (a)

Either $N=\mu\alpha.N_{1}$, $M_{1}\mapsto^{\sigma}N_{1}$ and $\sigma$ is
standard and none of $P_{j}$ is a $\theta$-redex $(1\leq j\leq k+1)$,

    2. (b)

or let $M\mapsto^{\sigma^{\prime}}\mu\alpha.[\alpha]M^{\prime}=P_{j}$ such
that $P_{j}$ is the first term in the sequence which is a $\theta$-redex and
$\sigma^{\prime}$ is standard and

      1. (i)

either
$\mu\alpha.[\alpha]M^{\prime}=P_{j}\rightarrow_{\theta}M^{\prime}\mapsto^{\sigma^{\prime\prime}}N$,

      2. (ii)

or
$\mu\alpha.[\alpha]M^{\prime}=P_{j}\mapsto^{\sigma^{\prime\prime\prime}}\mu\alpha.[\alpha]N^{\prime}$
such that $M^{\prime}\mapsto^{\sigma^{\prime\prime\prime}}N^{\prime}$,

where $\sigma^{\prime\prime}$ and $\sigma^{\prime\prime\prime}$ are standard.

  3. (3)

If $M=[\alpha]M_{1}$, let $M\mapsto^{\sigma}N$ be $M=P_{1}\rightarrow
P_{2}\rightarrow\ldots\rightarrow P_{k+1}=N$.

    1. (a)

Either $N=[\alpha]N_{1}$, $M_{1}\mapsto^{\sigma}N_{1}$ and $\sigma$ is
standard and none of $P_{j}$ is a $\rho$-redex $(1\leq j\leq k+1)$,

    2. (b)

or let $M\mapsto^{\sigma^{\prime}}[\alpha]\mu\beta.M^{\prime}=P_{j}$ such that
$P_{j}$ is the first term in the sequence which is a $\rho$-redex and
$\sigma^{\prime}$ is standard and

      1. (i)

either
$[\alpha]\mu\beta.M^{\prime}=P_{j}\rightarrow_{\rho}M^{\prime}[\beta:=\alpha]\mapsto^{\sigma^{\prime\prime}}N$,

      2. (ii)

or
$[\alpha]\mu\beta.M^{\prime}=P_{j}\mapsto^{\sigma^{\prime\prime\prime}}[\alpha]\mu\beta.N^{\prime}$
such that $M^{\prime}\mapsto^{\sigma^{\prime\prime\prime}}N^{\prime}$,

where $\sigma^{\prime\prime}$ and $\sigma^{\prime\prime\prime}$ are standard.

  4. (4)

$M=(\lambda x.M_{1})M_{2}\ldots M_{n}$ and

    1. (a)

either $M\rightarrow_{\beta}(M_{1}[x:=M_{2}]\dots M_{n})\mapsto^{\sigma_{1}}N$
and $\sigma_{1}$ is standard,

    2. (b)

or $M\mapsto^{\sigma_{1}}(\lambda x.N_{1})M_{2}\dots
M_{n}\mapsto^{\sigma_{2}}(\lambda x.N_{1})N_{2}\dots
M_{n}\mapsto^{\sigma_{3}}\ldots\mapsto^{\sigma_{n}}$
$(\lambda x.N_{1})N_{2}\ldots N_{n}=N$ and $\sigma_{i}$ $(1\leq i\leq n)$ are
standard.

  5. (5)

$M=(\mu\alpha.M_{1})M_{2}\ldots M_{n}$ and

    1. (a)

either $M\rightarrow_{\mu}(\mu\alpha.M_{1}[\alpha:=_{r}M_{2}]\ldots
M_{n})\mapsto^{\sigma_{1}}N$ and $\sigma_{1}$ is standard,

    2. (b)

or $M\mapsto^{\sigma_{1}}(\mu\alpha.N_{1})M_{2}\ldots
M_{n}\mapsto^{\sigma_{2}}(\mu\alpha.N_{1})N_{2}\ldots
M_{n}\mapsto^{\sigma_{3}}\ldots\mapsto^{\sigma_{n}}$
$(\mu\alpha.N_{1})N_{2}\ldots N_{n}=N$ and $\sigma_{i}$ $(1\leq i\leq n)$ are
standard.

  6. (6)

$M=(x\;M_{1}\ldots M_{n})$, $M=(x\;M_{1}\ldots
M_{n})\mapsto^{\sigma_{1}}(x\;N_{1}\ldots
M_{n})\mapsto^{\sigma_{2}}\ldots\mapsto^{\sigma_{n}}$
$(x\;N_{1}\;N_{2}\ldots N_{n})=N$ and $\sigma_{i}$ $(1\leq i\leq n)$ are
standard.

In the rest of this paper, we may treat a reduction sequence $\sigma$ as a
list of the terms in $\sigma$ or sometimes as the list of the redex
occurrences of the reduction sequence. In accordance with this, given a
standard reduction sequence
$M_{1}\rightarrow^{R_{1}}M_{2}\rightarrow^{R_{2}}\ldots\rightarrow^{R_{n}}M_{n+1}$,
we may say that the sequence $M_{1},\ldots,M_{n+1}$ is standard (the redex
occurrences are implicitly understood in $M_{i}$), or we may talk about the
same thing by just saying that the sequence $\sigma=[R_{1},\ldots,R_{n}]$ is
standard. In notation: $\sigma\in St$.

We illustrate some of the difficulties in the example below, when we want to
assert statements about standard reduction sequences.

Let $M=(\mu\alpha.[\alpha]\lambda u.(\mu\beta.[\beta]\lambda y.x)[\alpha]x)x$.
Then, if we choose the $\theta$-redex $\mu\beta.[\beta]\lambda y.x$, we obtain
$M\rightarrow_{\theta}(\mu\alpha.[\alpha]\lambda u.(\lambda y.x)[\alpha]x)x$,
and, since we are not allowed to reduce the redex $(\lambda y.x)[\alpha]x$,
there are no more reductions provided we restrict ourselves to standard ones.
On the other hand, if we choose the $\mu$-redex $(\mu\beta.[\beta]\lambda
y.x)[\alpha]x$, then $M\rightarrow_{\mu}(\mu\alpha.[\alpha]\lambda
u.\mu\beta.[\beta](\lambda
y.x)[\alpha]x)x\rightarrow_{\beta}(\mu\alpha.[\alpha]\lambda
u.\mu\beta.[\beta]x)x$
$\rightarrow_{\mu}\mu\alpha.[\alpha](\lambda
u.\mu\beta.[\beta]x)x\rightarrow_{\theta}(\lambda
u.\mu\beta.[\beta]x)x\rightarrow_{\beta}\mu\beta[\beta]x\rightarrow_{\theta}x$
is standard.

The above definition prevents standard reduction sequences from having
overlapping $\theta$\- and $\rho$-redexes that could eliminate each other.
Moreover, our definition of standardness is such that it gives rise to the
following distinction between standard reduction sequences, at least in the
case of the $\lambda\mu$I-calculus: given a $\lambda\mu$I-term, if the head
redex exists, then a standard reduction sequence either begins with the head
redex or the head redex has a unique residual in the resulting term, which is
the head redex of the result itself. This will be demonstrated in Lemmas 11
and 12. On the other hand, in the general case, the situation is a little more
complicated as Examples 3.1 and 3.1 show. Example 3.1 even demonstrates that,
in the general case, in the presence of the $\theta$-rule, a standard
reduction sequence is not necessarily left to right, in contrast with the case
of the $\lambda$-calculus.

Our aim in this section is to obtain a standardization theorem for the
$\lambda\mu\rho\theta$-calculus, together with an upper bound on the lengths
of the standard reduction sequences. To this end, we state and prove some
auxiliary propositions first concerning the behaviour of standard reduction
sequences and then we present some lemmas providing upper bounds for the
lengths of reduction sequences starting from terms obtained as the results of
substitutions.

We state our first theorem saying that left-most reduction sequences are
special cases of standard reduction sequences.

######  Theorem 7.

Every leftmost reduction sequence is standard.

######  Proof 3.1.

Immediate from Definitions 2.2 and 3.1.

The following lemma states that a reduction sequence, which consists of a head
reduction sequence followed by a standard reduction sequence is itself
standard.

######  Lemma 8.

Let
$M\mapsto^{\sigma^{\prime}}M^{\prime}\mapsto^{\sigma^{\prime\prime}}M^{\prime\prime}$
such that $\sigma^{\prime}$ is a head-reduction sequence and
$\sigma^{\prime\prime}$ is standard. Then
$\sigma=\sigma^{\prime}\\#\sigma^{\prime\prime}$ is standard.

######  Proof 3.2.

Let $\sigma^{\prime}=[R]\\#\nu$. We prove the result by induction on
$(|\sigma^{\prime}|,comp(M))$, taking into account the various points of
Definition 2.2. Assume $|\nu|=0$. We deal with two of the cases only.

  1. (1)

$M=[\alpha]M_{1}$.

    1. (a)

Assume $M$ is a $\rho$-redex, then $M_{1}=\mu\beta.M_{2}$ and
$M\rightarrow_{\rho}M_{2}[\beta:=\alpha]\mapsto^{\sigma^{\prime\prime}}M^{\prime\prime}$
is standard by point 3 of Definition 3.1.

    2. (b)

If $R\leq M_{1}$, then the induction hypothesis applies.

  2. (2)

$M=(\mu\alpha.M_{1})M_{2}\dots M_{n}$. In this case the head redex of $M$ is
$(\mu\alpha.M_{1})M_{2}$. Thus
$M\rightarrow_{\mu}(\mu\alpha.M_{1}[\alpha:=_{r}M_{2}]\dots
M_{n})\mapsto^{\sigma^{\prime\prime}}M^{\prime\prime}$ and $\sigma$ is
standard by point 5 of Definition 3.1.

The cases when $|\nu|>0$ follow from the induction hypothesis.

The lemma below is a technical one, it will be useful for verifying that, if
we are given terms $M$, $M^{\prime}$ and $N$, $N^{\prime}$ such that
$M\mapsto_{st}M^{\prime}$ and $N\mapsto_{st}N^{\prime}$, then it is also true
that $M[x:=N]\mapsto_{st}M^{\prime}[x:=N^{\prime}]$ and
$M[\alpha:=_{r}N]\mapsto_{st}M^{\prime}[\alpha:=_{r}N^{\prime}]$,
respectively.

######  Lemma 9.

  1. (1)

Let
$M=(M_{1}\;M_{2})\mapsto^{\sigma}(\mu\alpha.M_{3})M_{2}\rightarrow_{\mu}(\mu\alpha.M_{3}[\alpha:=M_{2}])\mapsto^{\nu}N$
such that $\sigma$, $\nu\in St$ and suppose $\mu\alpha.M_{3}$ is the first
term of the reduction sequence $M_{1}\mapsto^{\sigma}\mu\alpha.M_{3}$ of the
form $\mu\beta.P$. Then $\xi=\sigma\\#[(\mu\alpha.M_{3})M_{2}]\\#\nu$ is
standard.

  2. (2)

Let $M=(M_{1}\;M_{2})\mapsto^{\sigma}(\lambda
x.M_{3})M_{2}\rightarrow_{\mu}M_{3}[x:=M_{2}]\mapsto^{\nu}N$ such that
$\sigma$, $\nu\in St$ and suppose $\lambda x.M_{3}$ is the first term of the
reduction sequence $M_{1}\mapsto^{\sigma}\lambda x.M_{3}$ of the form $\lambda
y.P$. Then $\xi=\sigma\\#[(\lambda x.M_{3})M_{2}]\\#\nu$ is standard.

######  Proof 3.3.

We deal only with case 1. We examine some of the interesting cases. The proof
goes by induction on $(|\sigma|,comp(M))$ taking into account the various
points of Definition 3.1.

  1. (1)

If $\sigma$ is standard by virtue of point 2 of Definition 3.1, that is,
$M=\mu\alpha.M_{1}$, the only possibility is when $R=\mu\alpha.[\alpha]R_{1}$
is the first $\theta$-redex in the sequence. But then $R$ is in fact $M$, and
$[R]\\#\nu$ is standard by definition.

  2. (2)

Let $\sigma$ be standard by reason of point 5 of Definition 3.1. By
assumption, the only possibility is $M=(\mu\alpha.P_{1})P_{2}\ldots P_{n}$ and
$\sigma=[(\mu\alpha.P_{1})P_{2}]\\#\sigma^{\prime}$. The induction hypothesis
can be applied to $\sigma^{\prime}$ and
$M^{\prime}=(\mu\alpha.P_{1}[\alpha:=_{r}P_{2}]\ldots P_{n})$.

The following lemma gives us some information on the form of a term which is a
reduct obtained by a standard reduction sequence.

######  Lemma 10.

Let $M\mapsto^{\sigma}M^{\prime}$ such that $\sigma$ is standard. Assume the
head-redex $hd(M)$ of $M$, if it exists, is not involved in $\sigma$. Then the
following statements are true.

  1. (1)

If $M=\lambda x.M_{1}$, then $M^{\prime}=\lambda x.M_{1}^{\prime}$, where
$M_{1}\mapsto^{\sigma}M_{1}^{\prime}$.

  2. (2)

If $M=[\alpha]M_{1}$, then $M^{\prime}=[\alpha]M_{1}^{\prime}$, where
$M_{1}\mapsto^{\sigma}M_{1}^{\prime}$.

  3. (3)

If $M=(M_{1}\dots M_{n})$, then there are standard
$\sigma_{1},\dots,\sigma_{n}$ and terms $M_{1}^{\prime},\dots,M_{n}^{\prime}$
such that $M_{i}\mapsto^{\sigma_{i}}M_{i}^{\prime}$ $(1\leq i\leq n)$,
$M^{\prime}=(M_{1}^{\prime}\dots M_{n}^{\prime})$ and
$\sigma=\sigma_{1}\\#\dots\\#\sigma_{n}$.

  4. (4)

If $M=\mu\alpha.M_{1}$ is a $\lambda\mu$I-term, then
$M^{\prime}=\mu\alpha.M_{1}^{\prime}$, where
$M_{1}\mapsto^{\sigma}M_{1}^{\prime}$.

######  Proof 3.4.

By induction on $(|\sigma|,comp(M))$. We consider some of the typical cases.

  1. (1)

$M=(\mu\alpha.M_{1})M_{2}\ldots M_{n}$. Since the head redex
$(\mu\alpha.M_{1})M_{2}$ is not involved in $\sigma$, point 5 of Definition
3.1 yields the result.

  2. (2)

$M=\mu\alpha.M_{1}$. If $M=\mu\alpha[\alpha]M_{2}$ is a $\theta$-redex, then,
since $M$ is not involved in $\sigma$, point 2 of Definition 3.1 yields that
$M_{2}\mapsto^{\sigma}N_{2}$ such that $N=\mu\alpha.[\alpha]N_{2}$. Assume now
$M$ is not a $\theta$-redex. Thus $M$ is either not of the form
$\mu\alpha.[\alpha]M_{2}$ such that $\alpha\notin Fv(M_{2})$ or
$M=\mu\alpha.[\alpha]M_{2}$ and $\alpha\in Fv(M_{2})$. Then $hd(M)=hd(M_{1})$
and, applying the induction hypothesis to $M_{1}$, it is straightforward to
check that either $M$ cannot reduce to a term of the form
$\mu\alpha.[\alpha]M^{\prime\prime}$, or
$M\mapsto\mu\alpha.[\alpha]M^{\prime\prime}$ and $\alpha\in
Fv(M^{\prime\prime})$. Again, by point 2 of Definition 3.1 we obtain the
result.

We remark that the assumption of $M$ being a $\lambda\mu$I-term is crucial in
Case 4 of Lemma 10 as the following example shows.

If $M=\mu\alpha.[\alpha](\lambda x.x)((\lambda y.x)[\alpha]x)$, then
$hd(M)=(\lambda x.x)((\lambda y.x)\;[\alpha]x)$. Consider the standard
reduction sequence $\sigma$: $M\rightarrow_{\beta}\mu\alpha.[\alpha](\lambda
x.x)x\rightarrow_{\theta}(\lambda x.x)x=M^{\prime}$. Then $hd(M)$ is not
involved in $\sigma$, on the other hand, $M^{\prime}$ is not of the form
$\mu\alpha.M_{1}^{\prime}$.

In the next two lemmas our common assumption is that $M$ is a
$\lambda\mu$I-term. The lemmas will serve as auxiliary statements when we
prove that a standard normalizing reduction sequence is unique in the case of
$\lambda\mu$I-terms.

######  Lemma 11.

Let $M$ be a $\lambda\mu$I-term. If $M\mapsto^{\sigma}M^{\prime}$ is standard
such that the head-redex $hd(M)$ of $M$ exists and is not involved in
$\sigma$, then the head-redex $hd(M^{\prime})$ of $M^{\prime}$ exists and it
is the unique residual of $hd(M)$ with respect to $\sigma$.

######  Proof 3.5.

By induction on $(|\sigma|,comp(M))$, taking into account the various cases of
Definition 2.2. Let $\sigma=[R]\\#\sigma^{\prime}$. We assume
$|\sigma^{\prime}|=0$. We examine some of the cases.

  1. (1)

$M=\mu\alpha.M_{1}$.

    1. (a)

$M=\mu\alpha.[\alpha]M_{2}$.

Assume $M$ is a $\theta$-redex. By assumption,
$M_{2}\mapsto^{R}M_{2}^{\prime}$ such that
$M^{\prime}=\mu\alpha.[\alpha]M_{2}^{\prime}$. Then our assertion follows. We
have also made use of point 2 (b) of Definition 3.1.

Assume now $M$ is not a $\theta$-redex, which implies $\alpha\in Fv(M_{2})$.
Then $hd(M_{1})=hd(M)$ is not $R$, we have $M_{2}\mapsto^{R}M_{2}^{\prime}$.
Since $M$ is a $\lambda\mu$I-term, $\alpha\in Fv(M_{2}^{\prime})$ holds. Thus,
if $M_{1}^{\prime}=[\alpha]M_{2}^{\prime}$,
$hd(M_{1}^{\prime})=hd(M^{\prime})$, by which, and the induction hypothesis,
we have the result.

    2. (b)

$M\neq\mu\alpha.[\alpha]M_{2}$. Let $M_{1}\rightarrow^{R}M_{1}^{\prime}$,
where $M^{\prime}=\mu\alpha.M_{1}^{\prime}$. By the induction hypothesis,
$hd(M_{1}^{\prime})$ exists and it is the unique residual of $hd(M_{1})$,
which is $hd(M)$. We prove that $hd(M^{\prime})=hd(M_{1}^{\prime})$, by which
our assertion follows. By Definition 2.2, it is enough to verify that
$M^{\prime}$ is not a $\theta$-redex. Lemma 10 shows that the only possibility
is $M=\mu\alpha.[\alpha]M_{2}$ for some $M_{2}$ provided $M^{\prime}$ is a
$\theta$-redex, but this was excluded by the assumption.

  2. (2)

$M=[\alpha]M_{1}$.

    1. (a)

$M=[\alpha]\mu\beta.M_{2}$. Then our assumption and point 3 of Definition 3.1
yields the statement.

    2. (b)

$M$ is not a $\rho$-redex. Then Lemma 10 ensures that $M^{\prime}$ is not a
$\rho$-redex either. If $M_{1}\mapsto^{R}M_{1}^{\prime}$, where
$M^{\prime}=[\alpha]M_{1}^{\prime}$, then $hd(M)=hd(M_{1})$ and
$hd(M^{\prime})=hd(M_{1}^{\prime})$, by which, together with the induction
hypothesis, our claim follows.

  3. (3)

$M=(\mu\alpha.M_{1})M_{2}\ldots M_{n}$. Since $hd(M)$ is not $R$, the only
possibility is $M_{i}\rightarrow^{R}M_{i}^{\prime}$ for some $1\leq i\leq n$.
Hence our assertion follows.

The case $|\sigma^{\prime}|>0$ follows by the induction hypothesis.

The assumption that $M$ is a $\lambda\mu$I-term is necessary in the above
lemma, too.

Let $M=\mu\alpha.[\alpha](\lambda x.x)((\lambda y.x)[\alpha]x)$, as in Example
3.1, then $hd(M)=(\lambda x.x)((\lambda y.x)[\alpha]x)$. Consider the
reduction sequence $M\rightarrow_{\beta}\mu\alpha.[\alpha](\lambda
x.x)x=M^{\prime}$. In this case $hd(M^{\prime})=M^{\prime}$ and it is not a
residual of $hd(M)$.

######  Lemma 12.

Let $M$ be a $\lambda\mu$I-term. If $M\mapsto^{\sigma}M^{\prime}$ is standard
and the head-redex $hd(M)$ of $M$ is involved in $\sigma$, then
$\sigma=[hd(M)]\\#\sigma^{\prime}$ for some $\sigma^{\prime}$.

######  Proof 3.6.

The proof goes by induction on $|\sigma|$, considering the cases of Definition
3.1. If $|\sigma|=1$, then the statement is trivial. Assume
$\sigma=[R]\\#\sigma^{\prime}$, where $|\sigma^{\prime}|>0$, and let $hd(M)$,
the head redex of $M$, be different from $R$. Let
$M\rightarrow^{R}M^{\prime\prime}\mapsto^{\sigma^{\prime}}M^{\prime}$. By
Lemma 11, the head redex $hd(M^{\prime\prime})$ of $M^{\prime\prime}$ exists
and it is the unique residual of $hd(M)$ with respect to $R$. Then
$hd(M^{\prime\prime})$ is involved in $\sigma^{\prime}$, thus, by the
induction hypothesis, we have
$\sigma^{\prime}=[hd(M^{\prime\prime})]\\#\sigma^{\prime\prime}$. Now, by
examining the various forms of $M$ according to Definition 2.2, we can easily
check that the above situation is impossible.

Again, $M\in\lambda\mu$I is necessary for the statement of the previous lemma.

Let $M=\mu\alpha.[\alpha](\lambda x.x)((\lambda y.x)[\alpha]x)$, as in Example
3.1, then $hd(M)=(\lambda x.x)((\lambda y.x)[\alpha]x)$. Consider the standard
reduction sequence $\sigma$,
$M\rightarrow_{\beta}\mu\alpha.[\alpha](\lambda
x.x)x\rightarrow_{\theta}(\lambda x.x)x\rightarrow_{\beta}x=M^{\prime}$. Then
$hd(M)$ is involved in $\sigma$ and, on the other hand, $\sigma$ is not of the
form $[hd(M)]\\#\sigma^{\prime}$ for some $\sigma^{\prime}$.

###  3.2. Calculating the bounds for substitutions

In the following lemmas we examine how standardization is related to
substitutions in relation to $\lambda$\- and $\mu$-variables. In addition, we
give estimations for the lengths of standard reduction sequences starting from
terms given in the form of substitutions. The lemmas in this subsection are
indispensable for proving Lemma 19, which is the standardization lemma.

The next lemma shows that the length of a standard reduction sequence is not
modified by a $\lambda$-substitution, i.e. we can find a standard reduction
sequence of the same length for the substitutions.

######  Lemma 13.

Let $M\mapsto^{\sigma}M^{\prime}$ be standard, then there exists a $\nu\in St$
such that
$M[x:=N]\mapsto^{\nu}M^{\prime}[x:=N]$ and $|\nu|=|\sigma|$.

######  Proof 3.7.

The proof goes by a straightforward induction on $(|\sigma|,comp(M))$
distinguishing the cases of Definition 3.1. We deal only with the case
$M=[\alpha]M_{1}$. We prove that the choice $\nu=\sigma[x:=N]$ is appropriate.

  1. (1)

If $M\mapsto^{\sigma}M^{\prime}$ with $M^{\prime}=[\alpha]M_{1}^{\prime}$ and
$M_{1}\mapsto^{\sigma}M_{1}^{\prime}$, then the induction hypothesis applies.

  2. (2)

    1. (a)

If
$M\mapsto^{\sigma_{1}}[\alpha]\mu\beta.P\rightarrow_{\rho}P[\beta:=\alpha]\mapsto^{\sigma_{2}}M^{\prime}$
such that $[\alpha]\mu\beta.P$ is the first $\rho$-redex in the sequence, then
the induction hypothesis implies that
$M[x:=N]\mapsto^{\sigma_{1}[x:=N]}[\alpha]\mu\beta.P[x:=N]$ and
$P[\beta:=\alpha][x:=N]\mapsto^{\sigma_{2}[x:=N]}M^{\prime}[x:=N]$ are
standard, moreover, $[\alpha]\mu\beta.P[x:=N]$ is the first $\rho$-redex in
the sequence. We obtain the result immediately from Definition 3.1.

    2. (b)

If
$M\mapsto^{\sigma_{1}}[\alpha]\mu\beta.P\mapsto^{\sigma_{2}}[\alpha]\mu\beta.Q=M^{\prime}$,
where $[\alpha]\mu\beta.P$ is the first $\rho$-redex in the sequence then, by
the induction hypothesis,
$M[x:=N]\mapsto^{\sigma_{1}[x:=N]}[\alpha]\mu\beta.P[x:=N]$ and
$[\alpha]\mu\beta.P[x:=N]\mapsto^{\sigma_{2}}[\alpha]\mu\beta.Q[x:=N]=M^{\prime}[x:=N]$
are standard, which, considering Definition 3.1, yields the result.

In the sequel, we make preparations for the estimation of the upper bound of
the length of a standard reduction sequence. To this aim, we introduce
quantitative notions in relation to reduction sequences.

  1. (1)

Let $M$ be a term and $x$ (resp. $\alpha$) be a $\lambda$-variable (resp.
$\mu$-variable). Denote by $|M|_{x}$ (resp. $|M|_{\alpha}$) the number of
occurrences of $x$ (resp. $\alpha$) in $M$.

  2. (2)

Let $\sigma$ be the reduction sequence
$M\rightarrow^{R_{1}}M_{1}\rightarrow^{R_{2}}\dots\rightarrow^{R_{n}}M_{n}$
and $\alpha\in Fv(M)$. Let $\langle\sigma\rangle_{(\rho,\alpha)}$ denote the
number of $\rho$-reductions of the form $(\alpha\;\mu\beta.P)$ in $\sigma$.
Furthermore, let $\langle\sigma\rangle_{\rho}$ be the number of $\rho$-redexes
in $\sigma$.

  3. (3)

If $M\mapsto^{\sigma}M^{\prime}$, let us denote by
$\langle\sigma\rangle_{\theta}$ the number of $\theta$-redexes in $\sigma$.

  4. (4)

If $x\in Fv(M)$, let us denote by $sumarg(M,x)$ the sum of the number of
arguments of each occurrence of $x$ in $M$. It is easy to see that
$sumarg(M,x)\leq comp(M)-1$.

Regarding the $\mu$-substitutions, the length of a standard reduction sequence
can increase. This is in connection with the standardization of reduction
sequences initially containing $\rho$-redexes.

######  Lemma 14.

If $M\mapsto^{\sigma}M^{\prime}$ is standard and $N_{1},\dots,N_{k}$ are terms
for which $\alpha\notin Fv(N_{i})$ $(1\leq i\leq k)$, then there exists a
standard reduction sequence $\nu$ such that
$M[\alpha:=_{r}N_{1}]\dots[\alpha:=_{r}N_{k}]\mapsto^{\nu}M^{\prime}[\alpha:=_{r}N_{1}]\dots[\alpha:=_{r}N_{k}]$
and $|\nu|=|\sigma|+k\cdot\langle\sigma\rangle_{(\rho,\alpha)}$.

######  Proof 3.8.

By induction on $(|\sigma|,comp(M))$. The case $|\sigma|=0$ is trivial. If
$\sigma=[R]\\#\sigma^{\prime}$, where
$M\rightarrow^{R}M^{\prime\prime}\mapsto^{\sigma^{\prime}}M^{\prime}$, the
only interesting case is
$M=[\gamma]\mu\beta.M_{1}\rightarrow_{\rho}M_{1}[\beta:=\gamma]=M^{\prime\prime}\mapsto^{\sigma^{\prime}}M^{\prime}$.
If $\alpha\neq\gamma$, then the result follows from the induction hypothesis.
Otherwise, we have the following reduction sequence denoted by (1) :
$M[\alpha:=_{r}N_{1}]\dots[\alpha:=_{r}N_{k}]=[\alpha](\mu\beta.M_{1}[\alpha:=_{r}N_{1}]\dots[\alpha:=_{r}N_{k}])N_{1}\dots
N_{k}{}\mapsto_{\mu}^{k}[\alpha]\mu\beta.M_{1}[\alpha:=_{r}N_{1}]\dots[\alpha:=_{r}N_{k}][\beta:=_{r}N_{1}]\dots[\beta:=_{r}N_{k}]\rightarrow_{\rho}M_{1}[\beta:=\alpha][\alpha:=_{r}N_{1}]\dots[\alpha:=_{r}N_{k}]$,
from which the estimation for the length of $\nu$ follows. Assume $\sigma$ is
standard, we prove by induction on $(|\sigma|,comp(M))$ that $\nu$ is
standard. We examine the cases of Definition 3.1. We consider only the case
when $\sigma$ is standard by reason of point 3 of Definition 3.1. Let
$M=[\gamma]M_{1}$. If $M_{1}\mapsto^{\sigma}M_{1}^{\prime}$, the induction
hypothesis applies. Otherwise, there are standard $\sigma^{\prime}$,
$\sigma^{\prime\prime}$ such that
$M\mapsto^{\sigma^{\prime}}[\gamma]\mu\beta.M^{\prime\prime}\mapsto^{\sigma^{\prime\prime}}M^{\prime}$
and $[\gamma]\mu\beta.M^{\prime\prime}$ is the first term in the sequence
which is a $\rho$-redex and either
$\sigma^{\prime\prime}=[[\gamma]\mu\beta.M^{\prime\prime}]\\#\sigma^{\prime\prime\prime}$
for some $\sigma^{\prime\prime\prime}\in St$ or
$M^{\prime}=[\gamma]\mu\beta.M^{\prime\prime\prime}$ and
$M^{\prime\prime}\mapsto^{\sigma^{\prime\prime}}M^{\prime\prime\prime}$.
Assume $\gamma=\alpha$. Then, by the induction hypothesis,
$M[\alpha:=_{r}N_{1}]\dots[\alpha:=_{r}N_{k}]\mapsto^{\nu^{\prime}}[\alpha](\mu\beta.M^{\prime\prime}[\alpha:=_{r}N_{1}]\dots[\alpha:=_{r}N_{k}])N_{1}\ldots
N_{k}$ is standard and
$(\mu\beta.M^{\prime\prime}[\alpha:=_{r}N_{1}]\dots[\alpha:=_{r}N_{k}])N_{1}\ldots
N_{k}$ is the first $\mu$-redex in the sequence. Then we apply the head
reduction sequence of (1), hence Lemma 8 involves that $\nu$ is standard. If
$\gamma\neq\alpha$, then
$M[\alpha:=_{r}N_{1}]\dots[\alpha:=_{r}N_{k}]=[\gamma]M_{1}[\alpha:=_{r}N_{1}]\dots[\alpha:=_{r}N_{k}]\mapsto[\gamma]\mu\beta.M^{\prime\prime}[\alpha:=_{r}N_{1}]\dots[\alpha:=_{r}N_{k}]$.
If
$\sigma^{\prime\prime}=[[\gamma]\mu\beta.M^{\prime\prime}]\\#\sigma^{\prime\prime\prime}$,
then Lemma 9 applies. Otherwise we obtain the result by the induction
hypothesis.

The situation in the lemma below is more complicated when we assume that we
are provided a term together with a standard reduction sequence emanating from
that and we substitute the term in place of a variable of another term. This
is in relation with the possibility of creating new redexes. As we have seen
earlier, sometimes we only obtain an estimation for the lengths of the new
standard reduction sequences.

######  Lemma 15.

  1. (1)

If $N\mapsto^{\sigma}N^{\prime}$ is standard, then there exists a standard
reduction $\nu$ such that
$M[x:=N]\mapsto^{\nu}M[x:=N^{\prime}]$ and
$|\nu|\leq|\sigma|\cdot|M|_{x}+sumarg(M,x)\cdot(\langle\sigma\rangle_{\theta}+\langle\sigma\rangle_{\rho})$.

  2. (2)

If $N\mapsto^{\sigma}N^{\prime}$ is standard, then there exists a standard
reduction $\nu$ such that
$M[\alpha:=_{r}N]\mapsto^{\nu}M[\alpha:=_{r}N^{\prime}]$ and
$|\nu|=|\sigma|\cdot|M|_{\alpha}$.

######  Proof 3.9.

Let us only deal with case 1. The proof goes by a straightforward induction on
$comp(M)$. We lean on the points of Definition 2.2. For example, let us
consider two of the cases.

  1. (1)

$M=(x\;M_{1}\ldots M_{n})$. Let $\tau_{i}$ be the reduction sequences obtained
for $M_{i}[x:=N]$ by the induction hypothesis. Let
$\tau=\tau_{1}\\#\ldots\\#\tau_{n}$. By induction on $|\sigma|$, we define the
following transformation $\sigma^{\circ}$. We eliminate the outermost
$\theta$-redexes from $\sigma$, that is, redexes $R$, where
$N\mapsto^{\sigma^{\prime}}R\rightarrow_{\theta}R^{\prime}\mapsto^{\sigma^{\prime\prime}}N^{\prime}$.
Observe that an outermost $\theta$-redex appears in $\sigma$ iff $\sigma$ is
standard by reason of point 2. (a) of Definition 3.1. Let $\sigma$ be such
that
$N=\mu\alpha.P\mapsto^{\sigma_{1}}\mu\alpha.[\alpha]R\rightarrow_{\theta}R\mapsto^{\sigma_{2}}N^{\prime}$,
where $\sigma=\sigma_{1}\\#\sigma_{2}$ and $R$ is the first $\theta$-redex in
$\sigma_{1}$. Let $\xi$ be $(\mu\alpha.P)M_{1}[x:=N]\ldots
M_{n}[x:=N]\rightarrow_{\mu}^{n}\mu\alpha.P[\alpha:=_{r}M_{1}[x:=N]]\ldots[\alpha:=_{r}M_{n}[x:=N]]\mapsto^{\sigma_{1}^{\prime}}\mu\alpha.[\alpha](R\;M_{1}[x:=N]\ldots
M_{n}[x:=N])\rightarrow_{\theta}(R\;M_{1}[x:=N]\ldots M_{n}[x:=N])$, where
$\sigma_{1}^{\prime}$ is obtained from $\sigma_{1}$ by Lemma 14. Then let
$\sigma^{\circ}=\xi\\#(\sigma_{2})^{\circ}$ where
$\sigma=[R]\\#\sigma^{\prime}$. The reduction sequence
$M[x:=N]\mapsto^{\sigma^{\circ}}(N^{\prime}\;M_{1}[x:=N]\dots
M_{n}[x:=N])\mapsto^{\tau}(N^{\prime}\;M_{1}[x:=N^{\prime}]\dots
M_{n}[x:=N^{\prime}])$ is appropriate. We prove by induction on $|\sigma|$
that $|\sigma^{\circ}|\leq
n+n\cdot(\langle\sigma\rangle_{\rho}+\langle\sigma\rangle_{\theta})$:
$|\sigma^{\circ}|=|\xi|+|\sigma_{2}^{\circ}|=1+n+|\sigma_{1}|+n\cdot\langle\sigma_{1}\rangle_{(\rho,\alpha)}+|\sigma_{2}^{\circ}|\leq
1+n+|\sigma_{1}|+n\cdot\langle\sigma_{1}\rangle_{\rho}+|\sigma_{2}^{\circ}|\leq
1+n+|\sigma_{1}|+n\cdot\langle\sigma_{1}\rangle_{\rho}+|\sigma_{2}|+n\cdot(\langle\sigma_{2}\rangle_{\theta}+\langle\sigma_{2}\rangle_{\rho})=|\sigma|+n\cdot(\langle\sigma\rangle_{\theta}+\langle\sigma\rangle_{\rho})$.
Then
$|\sigma^{\circ}+\tau|=|\sigma^{\circ}|+\smash{\sum_{i=1}^{i=n}|\tau_{i}|}\leq|\sigma|+n\cdot(\langle\sigma\rangle_{\theta}+\langle\sigma\rangle_{\rho})+|\tau_{i}|\cdot\smash{\sum_{i=1}^{i=n}}|M_{i}|_{x}+\smash{\sum_{i=1}^{i=n}}sumarg(M_{i},x)\cdot(\langle\sigma\rangle_{\theta}+\langle\sigma\rangle_{\rho})=|\sigma|\cdot|M|_{x}+sumarg(M,x)\cdot(\langle\sigma\rangle_{\theta}+\langle\sigma\rangle_{\rho})$.

  2. (2)

$M=(\lambda y.M_{1})M_{2}\overrightarrow{P}$. The induction hypothesis gives
$\tau_{i}$ such that $M_{i}[x:=N]\mapsto^{\tau_{i}}M_{i}[x:=N^{\prime}]$
$(1\leq i\leq,k)$. Then we can choose $\tau=\tau_{1}\\#\ldots\\#\tau_{k}$.

Lemmas 16 and 17 combine the results of the preceding lemmas: we substitute in
place of a variable common in the members of a standard reduction sequence a
new term such that we are also equipped with a standard reduction sequence
starting from it. In the case of the $\lambda$-substitution we obtain an
inequality for the length of the new standard reduction sequence, whereas in
the case of the $\mu$-substitution we have an exact estimation.

######  Lemma 16.

Let $M\mapsto^{\sigma}M^{\prime}$ and $N\mapsto^{\nu}N^{\prime}$ be standard.
Then there is a standard reduction $\tau$ such that
$M[x:=N]\mapsto^{\tau}M^{\prime}[x:=N^{\prime}]$ and
$|\tau|\leq|\sigma|+|M^{\prime}|_{x}\cdot|\nu|+sumarg(M^{\prime},x)\cdot(\langle\nu\rangle_{\theta}+\langle\nu\rangle_{\rho})$.

######  Proof 3.10.

The proof goes by induction on $(|\sigma|,comp(M))$, taking into account the
various points of Definition 3.1. The case $|\sigma|=0$ is treated by Lemma
15. Let $\sigma=[R]\\#\sigma^{\prime}$. We treat some of the typical cases.

  1. (1)

$M=\mu\alpha.M_{1}$. If $M_{1}\mapsto^{\sigma}M_{1}^{\prime}$, then the
induction hypothesis applies. Let $\sigma$ be standard by reason of point 2
(a) of Definition 3.1. Let
$M\mapsto^{\sigma_{1}}\mu\alpha.[\alpha]M_{2}\rightarrow_{\theta}M_{2}\mapsto^{\sigma_{2}}M^{\prime}$.
Lemma 13 and the induction hypothesis give standard $\nu_{1}$ and $\nu_{2}$
such that
$M[x:=N]\mapsto^{\nu_{1}}\mu\alpha.[\alpha]M_{2}[x:=N])\rightarrow_{\theta}M_{2}[x:=N]\mapsto^{\nu_{2}}M^{\prime}[x:=N^{\prime}]$.
Moreover, since $\mu\alpha.[\alpha]M_{2}[x:=N]$ is the first $\theta$-redex in
the sequence, $\nu=\nu_{1}\\#[\mu\alpha.[\alpha]M_{2}[x:=N]]\\#\nu_{2}$ is
standard by virtue of Definition 3.1. The case of point 2. (b) of Definition
3.1 follows from the induction hypothesis.

  2. (2)

$M=(\mu\alpha.M_{1})M_{2}\ldots M_{n}$. Assume
$M\rightarrow_{\mu}(\mu\alpha.M_{1}[\alpha:=_{r}M_{2}]\ldots
M_{n})\mapsto^{\sigma^{\prime}}M^{\prime}$. Then
$((\mu\alpha.M_{1})M_{2})[x:=N]$ is the head redex of $M[x:=N]$ and Lemma 8
together with the induction hypothesis yield the result. If
$(\mu\alpha.M_{1})M_{2}$ is not involved in $\sigma$, then the induction
hypothesis applies.

  3. (3)

$M=(x\;M_{2}\ldots M_{n})$. The proof is analogous to that of Lemma 15. We
define, by induction on $\nu$, a standard reduction sequence $\nu^{\circ}$ in
the same way as in Lemma 15. We let
$\tau=\nu^{\circ}\\#\tau_{2}\\#\ldots\\#\tau_{n}$, where $\tau_{i}$ is
obtained from $M_{i}[x:=N]$ $(2\leq i\leq n)$ by the induction hypothesis. By
examining the various cases of Definition 3.1, we prove by induction on
$|\nu|$ that $\tau\in St$. As to the length of $\tau$, we have
$|\tau|=|\nu^{\circ}|+|\tau_{2}|+\ldots+|\tau_{n}|\leq|\nu|+(n-1)\cdot(\langle\nu\rangle_{\theta}+\langle\nu\rangle_{\rho})+\smash{{\sum_{i=2}^{n}}}(|\sigma_{i}|+|M_{i}^{\prime}|_{x}\cdot|\nu|+sumarg(M_{i}^{\prime},x)\cdot(\langle\nu\rangle_{\theta}+\langle\nu\rangle_{\rho}))=|\sigma|+|M^{\prime}|_{x}\cdot|\nu|+sumarg(M^{\prime},x)\cdot(\langle\nu\rangle_{\theta}+\langle\nu\rangle_{\rho})$.

The remaining cases are proved analogously.

######  Lemma 17.

Let $M\mapsto^{\sigma}M^{\prime}$ and $N\mapsto^{\nu}N^{\prime}$ be standard.
Then there is standard sequence $\tau$ such that
$M[\alpha:=_{r}N]\mapsto^{\tau}M^{\prime}[\alpha:=_{r}N^{\prime}]$ and
$|\tau|=|\sigma|+\langle\sigma\rangle_{(\rho,\alpha)}+|M^{\prime}|_{\alpha}\cdot|\nu|$.

######  Proof 3.11.

The proof goes by induction on $(|\sigma|,comp(M))$, similarly to that of the
previous lemma. We consider some of the cases according to Definition 3.1. The
case $\sigma$=0 is treated in Lemma 15. Let $\sigma=[R]\\#\sigma^{\prime}$ for
some $\sigma^{\prime}$.

  1. (1)

$M=[\beta]M_{1}$. Assume $\beta=\alpha$. If
$M_{1}\mapsto^{\sigma}M_{1}^{\prime}$ with
$M^{\prime}=[\alpha]M_{1}^{\prime}$, then the induction hypothesis applies.
Otherwise, let
$M\mapsto^{\sigma_{1}}[\alpha]\mu\gamma.M_{2}\rightarrow_{\rho}M_{2}[\gamma:=\alpha]\mapsto^{\sigma_{2}}M^{\prime}$.
Similarly to the proof of Lemma 14, we have the standard reduction sequence
$\tau$:
$M[\alpha:=_{r}N]\mapsto^{\sigma_{1}[\alpha:=_{r}N]}[\alpha](\mu\gamma.M_{2}[\alpha:=_{r}N])\;N\rightarrow_{\mu}[\alpha]\mu\gamma.M_{2}[\alpha:=_{r}N][\gamma:=_{r}N])\rightarrow_{\rho}M_{2}[\gamma:=\alpha][\alpha:=_{r}N]\mapsto^{\tau_{2}}M^{\prime}[\alpha:=_{r}N^{\prime}]$,
where $\tau_{2}$ is obtained from $\sigma_{2}$ by the induction hypothesis and
the standardness follows from Lemma 9 and the induction hypothesis, where we
have made use of the fact that $[\alpha]\mu\gamma.M_{2}$ is the first
$\rho$-redex in $\sigma_{1}$. For the length of $\tau$ we have
$|\tau|=2+|\sigma_{1}|+|\tau_{2}|=2+|\sigma_{1}|+|\sigma_{2}|+\langle\sigma_{2}\rangle_{(\rho,\alpha)}+|M^{\prime}|_{\alpha}\cdot|\nu|=|\sigma|+\langle\sigma\rangle_{(\rho,\alpha)}+|M^{\prime}|_{\alpha}\cdot|\nu|$.
Assume now $\beta\neq\alpha$. The case when $M$ does not reduce to a
$\rho$-redex or it reduces to a $\rho$-redex but this is not involved in
$\sigma$ is again obvious. Let $M\mapsto^{\sigma_{1}}[\beta]\mu\gamma.M_{2}$.
Then
$M[\alpha:=_{r}N]\mapsto^{\sigma_{1}[\alpha:=_{r}N]}[\beta]\mu\gamma.M_{2}[\alpha:=_{r}N]\rightarrow_{\rho}M_{2}[\gamma:=\beta][\alpha:=_{r}N]\mapsto^{\tau^{\prime}}M^{\prime}[\alpha:=_{r}N^{\prime}]$
is standard, and $\tau^{\prime}$ is obtained by the induction hypothesis. The
equation for the length of $\tau$ is obviously valid in this case, too.

  2. (2)

$M=(\mu\beta.M_{1})M_{2}\ldots M_{n}$. If $(\mu\beta.M_{1})M_{2}$ is not
involved in $\sigma$, then the induction hypothesis applies. Otherwise, since
$hd(M)=hd(M[\alpha:=_{r}N])$, we have the result by Lemma 8, and again by the
induction hypothesis.

All the remaining cases are proved in a similar way.

###  3.3. The standardization theorem for the $\lambda\mu\rho\theta$-calculus

We are in a position now to state and prove the standardization theorem for
the $\lambda\mu\rho\theta$-calculus. As an additional result, we obtain an
upper bound for the lengths of the standard $\lambda\mu$I-reduction sequences.
First of all, we harvest the results of the previous subsection in a
definition: the definition below assigns values to pairs formed by redexes and
their containing terms. The definition is of technical interest: it makes us
possible to find an upper bound for the standardization of a reduction
sequence.

Let $R$ be a redex in a term $M$, the number $m(R,M)$ is defined as follows.

  1. (1)

If $R=(\mu\alpha.P)Q$, then $m(R,M)=|P|_{\alpha}$.

  2. (2)

If $R=(\lambda x.P)Q$, then $m(R,M)=2\cdot comp(M)-2$.

  3. (3)

If $R=[\alpha]\mu\beta.P$, then $m(R,M)=1$.

  4. (4)

If $R=\mu\alpha.[\alpha]P$ and $R$ has $n$ arguments in $M$, then
$m(R,M)=2n-1$.

The definition of $m(R,M)$ resembles the corresponding definition applied by
Xi [Xi.99], where $m(R)$ is the number of the occurrences of $x$ in $P$
provided $R=(\lambda x.P)Q$. The additional redexes, however, compel us to
change the value of $m(R,M)$ even for the case of the $\beta$-redex. The lemma
below will be used in the next subsection.

######  Lemma 18.

If $R$ is a redex in $M$, then $m(R,M)\leq 2\cdot(comp(M)-1)$.

######  Proof 3.12.

Immediate by Definition 3.3.

The following lemma is the main lemma for obtaining the standardization result
and the bound for the standard reduction sequences in Theorem 20. In what
follows, let $|\sigma|^{*}=max(|\sigma|,1)$, where $\sigma$ is a reduction
sequence.

######  Lemma 19.

Let $M\mapsto^{\sigma}M^{\prime}\rightarrow^{R}M^{\prime\prime}$ such that
${\sigma}$ is a standard reduction sequence. Then there exists a standard
reduction sequence $M\mapsto^{\tau}M^{\prime\prime}$ such that $|\tau|\leq
1+max(m(R,M^{\prime}),2)\cdot|\sigma|^{*}$. Furthermore, if $M$ is a
$\lambda\mu$I-term, then $1+|\sigma|\leq|\tau|$.

######  Proof 3.13.

The proof goes by induction $(|\sigma|,comp(M))$. The case of $|\sigma|=0$ is
obvious, thus we may assume $|\sigma|>0$. We examine the points of Definition
3.1. We treat some of the more interesting cases.

  1. (1)

$M=[\alpha]M_{1}$. If $M_{1}\mapsto^{\sigma}M_{1}^{\prime}$ such that
$M^{\prime}=[\alpha]M_{1}^{\prime}$ and there are no $\rho$-redexes as head
redexes in $\sigma$ including $M^{\prime\prime}$, then the induction
hypothesis applies. Assume $M\mapsto^{\sigma_{1}}[\alpha]\mu\beta.M_{2}$ such
that $\sigma_{1}\in St$ and $[\alpha]\mu\beta.M_{2}$ is the first $\rho$-redex
in the sequence. Let us suppose, according to point 3 (a) of Definition 3.1,
$[\alpha]\mu\beta.M_{2}\rightarrow_{\rho}M_{2}[\beta:=\alpha]\mapsto^{\sigma_{2}}M^{\prime}$,
where $\sigma=\sigma_{1}\\#[[\alpha]\mu\beta.M_{2}]\\#\sigma_{2}$ and
$\sigma_{i}\in St$ $(i\in\\{1,2\\})$. By the induction hypothesis applied to
$\sigma_{2}$, we obtain a $\tau^{\prime}\in St$ such that $|\tau^{\prime}|\leq
1+max(m(R,M^{\prime}),2)\cdot|\sigma_{2}|^{*}$. Then let
$\tau=\sigma_{1}\\#[[\alpha]\mu\beta.M_{2}]\\#\tau^{\prime}$. Hence
$|\tau|=1+|\sigma_{1}|+|\tau^{\prime}|\leq
1+|\sigma_{1}|+1+max(m(R,M^{\prime}),2)\cdot|\sigma_{2}|^{*}\leq
1+max(m(R,M^{\prime}),2)\cdot|\sigma|^{*}$. Assume we have
$[\alpha]\mu\beta.M_{2}\mapsto^{\sigma_{2}}[\alpha]\mu\beta.M_{2}^{\prime}$
with $M^{\prime}=[\alpha]\mu\beta.M_{2}^{\prime}$ and
$M_{2}\mapsto^{\sigma_{2}}M_{2}^{\prime}$, by reason of point 3 (b) of
Definition 3.1. If $R\leq M_{2}^{\prime}$, then we obtain the result by the
induction hypothesis. Assume $R=M^{\prime}$. Then
$\tau=\sigma_{1}\\#[[\alpha]\mu\beta.M_{2}]\\#\sigma_{2}^{\prime}$ is
appropriate, where $\sigma_{2}^{\prime}$ is
$M_{2}[\beta:=\alpha]\mapsto^{\sigma_{2}[\beta:=\alpha]}M_{2}^{\prime}[\beta:=\alpha]$.
The estimation for $|\tau|$ follows easily, since
$|\sigma_{2}^{\prime}|=|\sigma_{2}|$. Finally, if $M$ is a $\lambda\mu$I-term,
the result follows from the induction hypothesis by inspection of the various
subcases. For example, consider the case when
$[\alpha]\mu\beta.M_{2}\rightarrow_{\rho}M_{2}[\beta:=\alpha]\mapsto^{\sigma_{2}}M^{\prime}$,
where $\sigma=\sigma_{1}\\#[[\alpha]\mu\beta.M_{2}]\\#\sigma_{2}$, that is,
the case described by point 3 (a) of Definition 3.1. If $\tau^{\prime}$ is the
standard reduction sequence corresponding to $\sigma_{2}$ by the induction
hypothesis and $\tau=\sigma_{1}\\#[[\alpha]\mu\beta.M_{2}]\\#\tau^{\prime}$,
then $1+|\sigma_{2}|\leq|\tau^{\prime}|$ and we obtain the result.

  2. (2)

$M=(\mu\alpha.M_{1})M_{2}\ldots M_{n}$. Let $\sigma$ be standard by virtue of
point 5.(a) of Definition 3.1. Then $(\mu\alpha.M_{1})M_{2}\ldots
M_{n}\rightarrow_{\mu}(\mu\alpha.M_{1}[\alpha:=_{r}M_{2}]\ldots
M_{n})\mapsto^{\sigma^{\prime}}M^{\prime}$ with $\sigma^{\prime}\in St$. The
induction hypothesis applied to $\sigma^{\prime}$ provides us with a standard
$\tau^{\prime}$ with appropriate length such that
$(\mu\alpha.M_{1}[\alpha:=_{r}M_{2}]\ldots
M_{n})\mapsto^{\tau^{\prime}}M^{\prime\prime}$. By this the result follows.
Assume $\sigma$ is standard by reason of point 5.(b) of Definition 3.1. Then
$(\mu\alpha.M_{1})M_{2}\ldots
M_{n}\rightarrow^{\sigma_{1}}(\mu\alpha.M_{1}^{\prime})M_{2}\ldots
M_{n}\mapsto^{\sigma_{2}}\ldots\mapsto^{\sigma_{n}}(\mu\alpha.M_{1}^{\prime})M_{2}^{\prime}\ldots
M_{n}^{\prime}=M^{\prime}$, where $\sigma=\sigma_{1}\\#\ldots\\#\sigma_{n}$.
If $R\leq M_{i}^{\prime}$, then the induction hypothesis gives the result. Let
$R=(\mu\alpha.M_{1}^{\prime})M_{2}^{\prime}$. Then $\tau$ can be chosen as
$(\mu\alpha.M_{1})M_{2}\ldots
M_{n}\rightarrow_{\mu}(\mu\alpha.M_{1}[\alpha:=_{r}M_{2}]\ldots
M_{n})\mapsto^{\tau_{1}}(\mu\alpha.M_{1}^{\prime}[\alpha:=_{r}M_{2}^{\prime}]\ldots
M_{n})\mapsto^{\sigma_{3}}\ldots\mapsto^{\sigma_{n}}(\mu\alpha.M_{1}^{\prime}[\alpha:=_{r}M_{2}^{\prime}]\ldots
M_{n}^{\prime})$, where $\tau_{1}$ is obtained from Lemma 17. Moreover,
$|\tau|=1+|\tau_{1}|+\sum_{i=3}^{n}|\sigma_{i}|=1+|\sigma_{1}|+\langle\sigma_{1}\rangle_{(\rho,\alpha)}+|M_{1}^{\prime}|_{\alpha}\cdot|\sigma_{2}|+\sum_{i=3}^{n}|\sigma_{i}|\leq
1+2|\sigma_{1}|+|M^{\prime}|_{\alpha}\cdot|\sigma_{2}|+\sum_{i=3}^{n}|\sigma_{i}|\leq
1+max(m(R,M^{\prime}),2)\cdot|\sigma|^{*}.$ Assume
$R=\mu\alpha.[\alpha]M_{1}^{\prime\prime}$ is a $\theta$-redex. In this case
$\sigma_{1}$ is standard by virtue of point 2 (b) (ii) of Definition 3.1. Let
$\mu\alpha.[\alpha]M_{1}^{*}$ be the first $\theta$-redex such that an initial
segment $\sigma_{1}^{\prime}$ of $\sigma_{1}$ produces
$\mu\alpha.[\alpha]M_{1}^{*}$ starting from $\mu\alpha.M_{1}$. Let
$\sigma_{1}=\sigma_{1}^{\prime}\\#\sigma_{1}^{\prime\prime}$. Then
$(\mu\alpha.M_{1})M_{2}\ldots
M_{n}\rightarrow_{\mu}^{n-1}\mu\alpha.M_{1}[\alpha:=_{r}M_{2}]\ldots[\alpha:=_{r}M_{n}]\mapsto^{\tau_{1}}\mu\alpha.[\alpha](M_{1}^{*}\;M_{2}\ldots
M_{n})\rightarrow_{\theta}(M_{1}^{*}\;M_{2}\ldots
M_{n})\mapsto^{\sigma_{1}^{\prime\prime}}(M_{1}^{\prime}\;M_{2}\ldots
M_{n})\mapsto^{\sigma_{2}}\ldots\mapsto^{\sigma_{n}}(M_{1}^{\prime}\;M_{2}^{\prime}\ldots
M_{n}^{\prime})=M^{\prime}$ is standard, where $\tau_{1}$ is obtained from
$\sigma_{1}^{\prime}$ by Lemma 14. As to the length of $\tau$, we have
$|\tau|=1+(n-1)+|\tau_{1}|+|\sigma_{1}^{\prime\prime}|+\sum_{i=2}^{n}|\sigma_{i}|=1+(n-1)+|\sigma_{1}^{\prime}|+(n-1)\cdot\langle\sigma_{1}^{\prime}\rangle_{(\rho,\alpha)}+|\sigma_{1}^{\prime\prime}|+\sum_{i=2}^{n}|\sigma_{i}|\leq
1+|\sigma|+(n-1)\cdot(1+|\sigma|)=1+n\cdot|\sigma|+(n-1)\leq
1+max(m(R,M^{\prime}),2)\cdot|\sigma|^{*}$. When $M$ is a $\lambda\mu$I-term,
we obtain the result by the induction hypothesis. Let us only treat the last
case, where $(\mu\alpha.M_{1})M_{2}\ldots
M_{n}\rightarrow^{\sigma_{1}}(\mu\alpha.M_{1}^{\prime})M_{2}\ldots
M_{n}\mapsto^{\sigma_{2}}\ldots\mapsto^{\sigma_{n}}(\mu\alpha.M_{1}^{\prime})M_{2}^{\prime}\ldots
M_{n}^{\prime}=M^{\prime}$ and
$R=\mu\alpha.M_{1}^{\prime}=\mu\alpha.[\alpha]M_{1}^{\prime\prime}$. If
$\mu\alpha.[\alpha]M_{1}^{*}$ is the first $\theta$-redex in $\sigma_{1}$ such
that $\sigma_{1}=\sigma_{1}^{\prime}\\#\sigma_{1}^{\prime\prime}$ and
$\tau_{1}$ is obtained from $\sigma_{1}^{\prime}$ by Lemma 14 and $\tau$ is
defined as above, then
$1+|\sigma|=1+|\sigma_{1}^{\prime}|+|\sigma_{1}^{\prime\prime}|+\sum_{i=2}^{n}|\sigma_{i}|\leq|\tau|=(n-1)+|\tau_{1}|+1+|\sigma_{1}^{\prime\prime}|+\sum_{i=2}^{n}|\sigma_{i}|$,
where $|\sigma_{1}^{\prime}|\leq|\tau_{1}|$ by Lemma 14.

Let $\sigma$ be the reduction sequence
$M_{1}\rightarrow^{R_{1}}M_{2}\rightarrow^{R_{2}}\dots\rightarrow^{R_{n}}M_{n+1}$.
Denote by $\mathcal{M}(\sigma)$ (the measure of $\sigma$) the number
$\prod^{n}_{i=1}(1+max(m(R_{i},M_{i}),2))$.

######  Theorem 20.

Let $\sigma$ be the reduction sequence
$M=M_{1}\rightarrow^{R_{1}}M_{2}\rightarrow^{R_{2}}\dots\rightarrow^{R_{n}}M_{n+1}$.
Then there is a standard reduction sequence $st(\sigma)$ such that
$M_{1}\mapsto^{st(\sigma)}M_{n+1}$ and $|st(\sigma)|\leq\mathcal{M}(\sigma)$.
Moreover, if $M$ is a $\lambda\mu$I-term, then $|\sigma|\leq|st(\sigma)|$ also
holds.

######  Proof 3.14.

The statement of the theorem is proved by induction on $|\sigma|$.

  1. (1)

If $|\sigma|=1$, then our claim follows directly from Lemma 19.

  2. (2)

Let $\sigma=\sigma^{\prime}\\#[R_{n}]$, where $|\sigma^{\prime}|\geq 1$. By
the induction hypothesis, we can find a standard $st(\sigma^{\prime})$ with
appropriate length such that $M_{1}\mapsto^{st(\sigma^{\prime})}M_{n}$.
Moreover, $|st(\sigma^{\prime})|^{*}=|st(\sigma^{\prime})|$. Then, by Lemma
19, there is a standard $M_{1}\mapsto^{\tau}M_{n+1}$ such that $|\tau|\leq
1+max(m(R_{n},M_{n}),2)\cdot|st(\sigma^{\prime})|^{*}\leq(1+max(m(R_{n},M_{n}),2))\cdot|st(\sigma^{\prime})|^{*}$,
which yields the result.

######  Theorem 21.

If $M$ is a $\lambda\mu$I-term, then a standard reduction sequence starting
from $M$ and leading to the normal form of $M$ is the leftmost reduction
sequence and it is a reduction sequence of maximal length.

######  Proof 3.15.

Let $M$ be a $\lambda\mu$I-term. Assume $M\mapsto^{\sigma}M^{\prime}$ where
$M^{\prime}$ is the normal form of $M$. The proof goes by induction on
$(|\sigma|,comp(M))$. We may assume $M\in HNF$. Otherwise, by Lemma 11, the
head redex of $M$ is involved in $\sigma$, then Lemma 12 yields that
$\sigma=[hd(M)]\\#\sigma^{\prime}$. That is, if $M\notin HNF$, then the
induction hypothesis applies. Let $M=(x\;M_{2}\ldots M_{n})$. By Definition
3.1 there exist $\sigma_{i}\in St$ $(2\leq i\leq n)$ such that
$\sigma=\sigma_{2}\\#\ldots\\#\sigma_{n}$ and $(x\;M_{2}\ldots
M_{n})\mapsto^{\sigma_{2}}(x\;M_{2}^{\prime}\ldots
M_{n})\mapsto^{\sigma_{3}}\ldots\mapsto^{\sigma_{n}}(x\;M_{2}^{\prime}\ldots
M_{n}^{\prime})$. Then the induction hypothesis applied to $\sigma_{i}$
$(2\leq i\leq n)$ gives the result. The leftmost reduction has a maximal
length by Theorem 20.

##  4\. The estimation for the lengths of the reduction sequences of the
$\lambda\mu\rho\theta$-calculus

In this section we present an application of Theorem 20 which, through the
standardization, provides us with a bound for the length of the standard
reduction sequence. Making use of the fact that, by Theorem 21, the standard
reduction sequence for a $\lambda\mu$I-term is unique and the Church-Rosser
property is valid for the $\lambda\mu$I-calculus, it does not make a
difference which normalizing reduction sequence we start from and obtain its
standardization. Hence, we choose a normalization sequence $\sigma$ the
measure of which, $\mathcal{M}(\sigma)$, can easily be estimated, which is, at
the same time, an upper bound for the standardization of $\sigma$. By Theorem
20, we have thus obtained an upper bound for $|\sigma|$. We extend this result
to the general case by finding a translation $[\\![M]\\!]_{k}$ of $M$ with an
appropriate $k$, where $[\\![M]\\!]_{k}$ is a $\lambda\mu$I-term such that
lengths of the types of the redexes in $M$ is the same as those of
$[\\![M]\\!]_{k}$ and $\eta(M)\leq\eta([\\![M]\\!]_{k})$ and the complexity of
$[\\![M]\\!]_{k}$ is bounded by a linear function of the complexity of $M$.

###  4.1. The estimation the lengths of the reduction sequences of the
$\lambda\mu\rho\theta I$-calculus

In this subsection we give an estimation for the lengths of the reduction
sequences in the $\lambda\mu\rho\theta$I-calculus. To this end we define a
normalization strategy such that the lengths of reduction sequences obeying
that strategy can be assessed easily and we can even establish bounds for the
sizes of the developments. Prior to this, we need the rank of a redex.
Intuitively, the rank of a redex is the length of type of the $\lambda$\- or
$\mu$-abstraction of the redex. This is exactly the quantity that can decrease
by a reduction.

  1. (1)

The rank of a redex $R$ in a term $M$ is defined as follows.

     * •

If $R=(\lambda x.M_{1})M_{2}$, then $rank(R,M)=lh(type(\lambda x.M_{1}))$.

     * •

If $R=(\mu\alpha.M_{1})M_{2}$, then $rank(R,M)=lh(type(\mu\alpha.M_{1}))$.

     * •

If $R=[\alpha]\mu\beta.M$, then $rank(R,M)=lh(type(\mu\beta.M))$.

     * •

If $R=\mu\alpha.[\alpha]M$, then $rank(R,M)=lh(type(\mu\alpha.(\alpha\;M)))$.

  2. (2)

The rank of a term $M$ is $rank(M)=max\\{rank(R,M)\;|\;R\textrm{ is a redex in
}M\\}$.

  3. (3)

Define $NF_{k}=\\{M\;|\;rank(M)<k\\}$.

The following lemma states that reductions do not increase the rank.

######  Lemma 22.

Let $M$,$N$ be terms.

  1. (1)

We have $rank(M[x:=N])\leq max\\{rank(M),rank(N),lh(type(x))\\}$ and

$rank(M[\alpha:=_{r}N])\leq max\\{rank(M),rank(N),lh(type^{*}(\alpha))\\}$,
where $type^{*}(\alpha)=A$ if $type(\alpha)=\neg A$.

  2. (2)

If $M\mapsto M^{\prime}$, then $rank(M)\geq rank(M^{\prime})$.

######  Proof 4.1.

  1. (1)

By induction on $comp(M)$.

  2. (2)

It is enough to prove if $M\rightarrow^{R}M^{\prime}$, then $rank(M)\geq
rank(M^{\prime})$. The proof goes by induction on $comp(M)$ and we use the
first item.

We are now in a position to define the notion of a $k$-reduction sequence,
which will denote a specific normalization strategy in what follows.

  1. (1)

We say that a reduction sequence $\nu$ is a $k$-reduction sequence, if every
redex in $\nu$ is of rank $k$.

  2. (2)

A reduction sequence $M\mapsto^{\nu}M^{\prime}$ is a $k$-normalization for a
given term $M$, if it is a $k$-reduction sequence and $M^{\prime}\in NF_{k}$.

  3. (3)

A reduction sequence $\xi$ starting from a term is good, if, at each reduction
step, it chooses the leftmost, innermost redex of maximal rank, that is, the
redex containing no other redexes of maximal rank and stands in the leftmost
position among these redexes.

Let $\sigma$ be a good reduction sequence starting from $M$, assume
$rank(M)=k$. Then $\sigma$ starts with the leftmost, innermost redex of rank
$k$ and chooses the leftmost, innermost redex of maximal rank every time.
Since $M$ is strongly normalizable, $\sigma$ is necessarily finite. By Lemma
22, the ranks of the redexes involved in $\sigma$ form a monotone decreasing
sequence. Thus, if $\sigma$ is a good normalizing sequence, then the sequence
of redexes of rank $k$ in $\sigma$ comes to an end and $\sigma$ continues with
a leftmost, innermost redex of maximal rank, which is less than $k$. Hence,
$\sigma$ is the concatenation of $l_{i}$-normalization sequences ($1\leq i\leq
s$) with $l_{1}=k>l_{2}>...>l_{s}\geq 1$.

The next two lemmas show that good k-normalization sequences can be dissected
easily so that we are able to estimate their lengths in the proof of Lemma 25.

######  Lemma 23.

  1. (1)

Let $rank((\mu\alpha.P)Q)=k$ and $x\notin Fv(P)$. If
$(\mu\alpha.P)Q{\mapsto}^{\nu}U$ and $\nu$ is a good $k$-normalization
sequence, there are terms $P^{\prime},Q^{\prime},U^{\prime}$ and good
$k$-normalization sequences ${\nu}_{1},{\nu}_{2},\nu_{3}$ such that
$P{\mapsto}^{\nu_{1}}P^{\prime}$, $Q{\mapsto}^{\nu_{2}}Q^{\prime}$,
$(\mu\alpha.P^{\prime})x{\mapsto}^{\nu_{3}}U^{\prime}$,
$U=U^{\prime}[x=Q^{\prime}]$ and
$\nu=\nu_{1}\\#\nu_{2}\\#\nu_{3}[x:=Q^{\prime}]$.

  2. (2)

Let $rank((\lambda y.P)Q)=k$ and $x\notin Fv(P)$. If $(\lambda
y.P)Q{\mapsto}^{\nu}U$ and $\nu$ is a good $k$-normalization sequence, there
are terms $P^{\prime},Q^{\prime},U^{\prime}$ and good $k$-normalization
sequences ${\nu}_{1},{\nu}_{2}$ such that $P{\mapsto}^{\nu_{1}}P^{\prime}$,
$Q{\mapsto}^{\nu_{2}}Q^{\prime}$, $(\lambda
y.P^{\prime})x{\rightarrow}^{\nu_{3}}P^{\prime}[y:=x]=P^{\prime\prime}$,
$U=P^{\prime\prime}[x:=Q^{\prime}]$ and
$\nu=\nu_{1}\\#\nu_{2}\\#\nu_{3}[x:=Q^{\prime}]$.

######  Proof 4.2.

  1. (1)

The algorithm proceeds by eliminating the innermost $k$-redexes from left to
right, that is we have (possibly empty) $\nu_{1}$ and $\nu_{2}$\- both being
$k$-normalization sequences such that $\nu_{1}\\#\nu_{2}$ is an initial
subsequent of $\nu$ and $P\mapsto^{\nu_{1}}P^{\prime}\in{NF}_{k}$,
$Q\mapsto^{\nu_{2}}Q^{\prime}\in{NF}_{k}$. Then $\nu$ continues with reducing
$(\mu\alpha.P^{\prime})Q^{\prime}$ and the redexes created by this reduction.
It is immediate to check that when reducing
$(\mu\alpha.P^{\prime})Q^{\prime}$, the created $k$-redexes can only be
redexes of the form $(\lambda y.V[\alpha:=_{r}Q^{\prime}])Q^{\prime}$ for some
$\lambda y.V$ of rank $k$ such that $[\alpha]\lambda y.V\leq P^{\prime}$, so
for every $k$-redex $R$ in $\mu\alpha.P^{\prime}[\alpha:=_{r}Q^{\prime}]$
there is an $R^{\prime}$ in $\mu\alpha.P^{\prime}[\alpha:=_{r}x]$ such that
$R=R^{\prime}[x:=Q^{\prime}]$. Reducing with these $\beta$-redexes in
$\mu\alpha.P^{\prime}[\alpha:=_{r}Q^{\prime}]$, no more $k$-redexes are
created. This proves our assertion.

  2. (2)

Analogous to the first point.

######  Lemma 24.

Let $rank((\mu\alpha.P)x)=k$, $\mu\alpha.P\in{{NF}}_{k}$ and $x\notin Fv(P)$.
If $(\mu\alpha.P)x{\mapsto}^{\nu}U$, $\nu$ is a good $k$-normalization
sequence, and $U\in{{NF}}_{k}$, then $|\nu|\leq comp(P)$ and $comp(U)\leq
2\cdot comp(P)$.

######  Proof 4.3.

Since $\mu\alpha.P\in{{NF}}_{k}$, in $\mu\alpha.P[\alpha:=_{r}x]$ $k$-redexes
of the form $(\lambda y.Q[\alpha:=_{r}x])x$ can only occur, where
$[\alpha]\lambda y.Q\leq P$ and $rank(\lambda y.Q)=k$. Subsequently reducing
these redexes gives $U$, which means that $U$ can be obtained in at most
$|P|_{\alpha}+1\leq comp(P)$ steps. Considering the above argument, since $x$
is a variable, the $\beta$-reduction steps in $\nu$ does not increase the size
of the term, so $comp(U)\leq
comp(\mu\alpha.P[\alpha:=_{r}x])=1+comp(P)+|P|_{\alpha}\leq 2\cdot comp(P)$.

The lemma below gives estimations for good $k$-normalization sequences. We may
observe that the obtained bounds does not depend on $k$.

######  Lemma 25.

Let $M$ be a term such that $rank(M)=k$. If $M\mapsto^{\nu}M^{\prime}$ and
$\nu$ is a good $k$-normalization sequence, then $comp(M^{\prime})\leq
2^{comp(M)-1}$ and $|\nu|\leq 2^{comp(M)-1}$.

######  Proof 4.4.

The proof of $comp(M^{\prime})\leq 2^{comp(M)-1}$ goes by induction on
$comp(M)$.

  1. (1)

The case $M=x$ or $M=\lambda x.M_{1}$ is obvious.

  2. (2)

Let $M=\mu\alpha.M_{1}$.

    1. (a)

If $M=\mu\alpha.[\alpha]M_{1}$ is a $\theta$-redex of rank $k$, then, since
the algorithm eliminates $k$-redexes from bottom to up and from left to right,
we have a $\nu^{\prime}\leq\nu$ such that
$\mu\alpha.[\alpha]M_{1}\mapsto^{\nu^{\prime}}\mu\alpha.[\alpha]M_{1}^{\prime}\rightarrow^{R}M_{1}^{\prime}=M^{\prime}$.
But in this case $M\rightarrow_{\theta}M_{1}\mapsto^{\nu^{\prime}}M^{\prime}$
is valid as well, thus by the induction hypothesis $comp(M^{\prime})\leq
2^{comp((M_{1})-1)}<2^{comp(M)-1}$.

    2. (b)

If $\mu\alpha.M_{1}$ is not a $\theta$-redex, but reduces to a $\theta$-redex
of rank $k$ in the course of the process, then a reasoning analogous to the
above one works.

    3. (c)

If $\mu\alpha.M_{1}$ is not a $\theta$-redex and it neither reduces to a
$\theta$-redex, then the induction hypothesis applies.

  3. (3)

Let $M=(M_{1}\;M_{2})$.

    1. (a)

If $M$ is not a $k$-redex, then we prove that $M$ cannot reduce to a
$k$-redex.

Suppose on the contrary that there is some initial subsequent of $\nu$ such
that it reduces $M$ to a $k$-redex, take $\nu^{\prime}$ as the shortest such
reduction sequence. Suppose $M$ reduces to a $\mu$-redex (the case of a
$\beta$-redex is similar). In this case we have
$M\mapsto^{\nu^{\prime}}(\mu\beta.N_{1})N_{2}$, where
$M_{1}\mapsto\mu\beta.N_{1}$ and $M_{2}\mapsto N_{2}$. Then
$M\mapsto^{\nu^{\prime\prime}}(N_{3}\;N_{2})\rightarrow^{R^{\prime}}(\mu\beta.N_{1})N_{2}$
must hold for some $R^{\prime}$, $\nu^{\prime\prime}$ such that
$\nu^{\prime}=\nu^{\prime\prime}\\#[R^{\prime}]$ and for some $N_{3}$, $N_{3}$
not beginning with a $\mu$. This means $N_{3}=R^{\prime}$ would be again a
$k$-redex, but a straightforward examination of the possible cases shows it is
impossible.

Hence we have $M^{\prime}=(M_{1}^{\prime}\;M_{2}^{\prime})$,
$\nu=\nu_{1}\\#\nu_{2}$ for some $k$-reduction sequences sequences $\nu_{1}$,
$\nu_{2}$ and $M_{i}\mapsto^{\nu_{i}}M_{i}^{\prime}$ $(i\in\\{1,2\\})$. Thus
by the induction hypothesis
$comp(M^{\prime})=comp(M_{1}^{\prime})+comp(M_{2}^{\prime})\leq
2^{comp(M_{1})-1}+2^{comp(M_{2})-1}\leq 2^{comp(M)-1}$.

    2. (b)

If $M$ is a $k$-redex and $M=(\mu\alpha.M_{1})M_{2}$, then $M$ is involved in
$\nu$ as a $\mu$-redex. By Lemma 23, we have $M_{1}^{\prime}$,
$M_{2}^{\prime}$, $M^{\prime\prime}$ and $\nu_{1}$, $\nu_{2}$, $\nu_{3}$ such
that $M_{1}{\mapsto}^{\nu_{1}}M_{1}^{\prime}$,
$M_{2}{\mapsto}^{\nu_{2}}M_{2}^{\prime}$,
$(\mu\alpha.M_{1}^{\prime})x{\mapsto}^{\nu_{3}}M^{\prime\prime}$,
$M^{\prime}=M^{\prime\prime}[x:=M_{2}^{\prime}]$ and
$\nu=\nu_{1}\\#\nu_{2}\\#\nu_{3}[x:=M_{2}^{\prime}]$, provided $x\notin
Fv(M_{1})$. From this, by Lemma 24 and by the induction hypothesis,
$comp(M^{\prime})=comp(M^{\prime\prime}[x:=M_{2}^{\prime}])=comp(M^{\prime\prime})+|M^{\prime\prime}|_{x}\cdot(comp(M_{2}^{\prime})-1)<comp(M^{\prime\prime})\cdot
comp(M_{2}^{\prime})\leq 2\cdot comp(M_{1}^{\prime})\cdot
comp(M_{2}^{\prime})\leq 2\cdot 2^{comp(M_{1})-1}\cdot
2^{comp(M_{2})-1}<2^{comp(M)-1}$. The case $M=(\lambda x.M_{1})M_{2}$ is
similar.

  4. (4)

Let $M=[\alpha]M_{1}$.

    1. (a)

If $M$ does not reduce to a $k$-redex, then the result is obvious.

    2. (b)

If $M$ is either a $k$-redex, or reduces to a $k$-redex, then there is a
$\nu^{\prime}$ and a $\mu\beta.M_{2}\in{{NF}}_{k}$ such that
$[\alpha]M_{1}\mapsto^{\nu^{\prime}}[\alpha]\mu\beta.M_{2}\rightarrow^{R}M_{2}[\beta:=\alpha]$
and $\nu^{\prime}\\#[R]=\nu$. The induction hypothesis for $M_{1}$ gives the
result.

We prove $|\nu|\leq 2^{comp(M)-1}$ by induction on $comp(M)$. The only
interesting case is when $M$ is a redex of rank $k$. Let, for example,
$M=(\mu\alpha.M_{1})M_{2}$. Since $\nu$ is a $k$-normalization sequence we can
assume again that $M$ is involved in $\nu$. By Lemma 23, we have
$M_{1}^{\prime}$, $M_{2}^{\prime}$ and $k$-normalization sequences
${\nu}_{1},{\nu}_{2},\nu_{3}$ such that
$M_{1}{\mapsto}^{\nu_{1}}M_{1}^{\prime}$,
$M_{2}{\mapsto}^{\nu_{2}}M_{2}^{\prime}$,
$(\mu\alpha.M_{1})^{\prime}x{\mapsto}^{\nu_{3}}M^{\prime\prime}$,
$M^{\prime}=M^{\prime\prime}[x=M_{2}^{\prime}]$ and
$\nu=\nu_{1}\\#\nu_{2}\\#\nu_{3}[x:=M_{2}^{\prime}]$, provided $x\notin
Fv(M_{1})$. Then, using Lemma 24 and the induction hypothesis, we obtain
$|\nu|=|\nu_{1}|+|\nu_{2}|+|\nu_{3}[x:=M_{2}^{\prime}]|=|\nu_{1}|+|\nu_{2}|+|\nu_{3}|\leq
2^{comp(M_{1})-1}+2^{comp(M_{2})-1}+2^{comp(M_{1})-1}=2^{comp(M_{1})}+2^{comp(M_{2})-1}\leq
2^{comp(M)-1}.$

Let tower defined by $\emph{tower}(n,m)=\left\\{\begin{array}[]{ll}m&\textrm{
if }n=0,\\\ 2^{{\emph{tower}}(n-1,m)}&\textrm{ if }n>0.\end{array}\right.$

In other words, the integer $\emph{tower}(n,m)$ is
$2^{\cdot^{\cdot^{\cdot^{2^{m}}}}}$, where $2$ is repeated $n$ times.

######  Theorem 26.

Let $M$ be a term such that $rank(M)=k$. If $M\mapsto^{\sigma}N$, $\sigma$ is
a good reduction sequence and $N\in NF$, then
$\mathcal{M}(\sigma)<\emph{tower}(k+1,comp(M))$.

######  Proof 4.5.

We first prove by induction on $k$ that
$\mathcal{M}(\sigma)<{\textrm{tower}}(1,{\textrm{tower}}(1,comp(M))+\sum_{i=2}^{k}{\textrm{tower}}(i,comp(M)-1))$.

  1. (1)

If $k=1$, then $\sigma$ is a 1-normalization sequence. Suppose $\sigma$ is
$M=M_{1}\rightarrow^{R_{1}}M_{2}\rightarrow^{R_{2}}\dots\rightarrow^{R_{n-1}}M_{n}\rightarrow^{R_{n}}M_{n+1}$
for some $n\geq 1$. We have, by Lemmas 18 and 25, $1+max(m(R_{i},M_{i}),2)\leq
2\cdot comp(M_{i})-1\leq 2\cdot 2^{comp(M)-1}-1<2^{comp(M)}$, then
$\mathcal{M}(\sigma)=\prod^{n}_{i=1}(1+max(m(R_{i},M_{i}),2))\;<$
$\;\prod^{n}_{i=1}2^{comp(M)}=2^{n\cdot comp(M)}$. Again, by Lemma 25, we
obtain $n=|\sigma|\leq 2^{comp(M)-1}$, so $\mathcal{M}(\sigma)<2^{comp(M)\cdot
2^{comp(M)-1}}\leq 2^{2^{comp(M)}}=$
$\textrm{tower}(1,\textrm{tower}(1,comp(M)))$.

  2. (2)

Let $rank(M)=k+1$ and $k\geq 1$. Assume
$M\mapsto^{\sigma^{\prime}}M^{\prime}\mapsto^{\sigma^{\prime\prime}}N\in{NF}$,
where $\sigma^{\prime}$ is a $k+1$-normalization sequence starting from $M$.
By the induction hypothesis, we have
$\mathcal{M}(\sigma^{\prime\prime})<{\textrm{tower}}(1,{\textrm{tower}}(1,comp(M^{\prime}))+\sum_{i=2}^{k}{\textrm{tower}}(i,comp(M^{\prime})-1))$.
As above, we obtain again $\mathcal{M}(\sigma^{\prime})<2^{2^{comp(M)}}$.
Then, using the multiplicity of $\mathcal{M}$ and Lemma 25, we can assert
$\mathcal{M}(\sigma)=\mathcal{M}(\sigma^{\prime})\cdot\mathcal{M}(\sigma^{\prime\prime})<2^{2^{comp(M)}}\cdot{\textrm{tower}}\Big{(}1,{\textrm{tower}}(1,comp(M^{\prime}))\;+\;\sum_{i=2}^{k}{\textrm{tower}}(i,comp(M^{\prime})-1)\Big{)}<2^{2^{comp(M)}}\cdot{\textrm{tower}}\Big{(}1,{\textrm{tower}}(1,\textrm{tower}(1,comp(M)-1)){}+$
$\sum_{i=2}^{k}{\textrm{tower}}(i,\textrm{tower}(1,comp(M)-1))\Big{)}=$
$2^{2^{comp(M)}}\cdot
2^{\underbrace{{2^{2^{comp(M)-1}}+\dots+2^{\cdot^{\cdot^{\cdot^{2^{comp(M)-1}}}}}}}_{k}}=$
${\textrm{tower}}(1,{\textrm{tower}}(1,comp(M))+\sum_{i=2}^{k+1}{\textrm{tower}}(i,comp(M)-1))$.

Finally, we prove, by induction on $k$, that
${\textrm{tower}}(1,comp(M))+\sum_{i=2}^{k}{\textrm{tower}}(i,comp(M)-1)\leq\textrm{tower}(k,comp(M))$.
The case $k=1$ is obvious. Let $k=n+1$ and $n\geq 1$. Applying the induction
hypothesis, we obtain
${\textrm{tower}}(1,comp(M))+\sum_{i=2}^{n+1}{\textrm{tower}}(i,comp(M)-1){}=$
$\;\underbrace{{2^{comp(M)}+2^{2^{comp(M)-1}}+\dots+2^{\cdot^{\cdot^{\cdot^{2^{comp(M)-1}}}}}}}_{n+1}{}\leq$
$\textrm{tower}(n,comp(M))+\textrm{tower}(n+1,comp(M)-1){}<\;\textrm{tower}(n+1,comp(M))$.

######  Corollary 27.

Let $M$ be a $\lambda\mu I$-term of rank $k$. Every reduction sequence
starting from $M$ has length less than $\emph{tower}(k+1,comp(M))$.

######  Proof 4.6.

Let $N$ be the normal-form of $M$. By Definition 4.1 and Theorem 26, there
exists a $\sigma$ such that $M\mapsto^{\sigma}N$ and
$\mathcal{M}(\sigma)<\textrm{tower}(k+1,comp(M))$. By Theorem 20, there is a
standard $\sigma^{\prime}$ such that $M\mapsto^{\sigma^{\prime}}N$ and
$|\sigma^{\prime}|<\mathcal{M}(\sigma)$. The result follows now from Theorem
21.

###  4.2. Some properties of the function $\eta$

In the next subsection we undertake the task of estimating the lengths of
reduction sequences starting from an arbitrary term by transforming the
starting term into a $\lambda\mu$I-term and estimating an upper bound for the
reduction sequences of the $\lambda\mu$I-term. In order to make the estimation
work, we have to prove that the longest reduction sequences of the transformed
terms are at least as long as those of the original terms. To this end, we
perform some calculations concerning longest reduction sequences of terms and
their reducts. This subsection prepares the treatment of the general case. The
lemmas of the subsection compare the lengths of the longest reduction
sequences starting from a redex and from one of its reducts.

######  Lemma 28.

Let $M,N$ and $\overrightarrow{P}$ be $\lambda\mu I$-terms. If $\alpha\notin
Fv(N)$, then
$\eta((\mu\alpha.\langle
M,[\alpha]z\rangle)\overrightarrow{P})+\eta(N)\leq\eta((\mu\alpha.\langle
M,[\alpha](z\;N)\rangle)\overrightarrow{P})$.

######  Proof 4.7.

Let $U=(\mu\alpha.\langle M,[\alpha]z\rangle)\overrightarrow{P}$,
$V=(\mu\alpha.\langle M,[\alpha](z\;N)\rangle)\overrightarrow{P}$. If
$\overrightarrow{P}$ is empty, the result is trivial, so may assume
$\overrightarrow{P}$ is not empty and its components are $M_{1},\dots,M_{n}$.
We are going to prove if $U\mapsto^{\sigma_{1}}U^{\prime}$,
$N\mapsto^{\sigma_{2}}N^{\prime}$ for some $\sigma_{1}$, $\sigma_{2}$,
$U^{\prime}$, $N^{\prime}$, then we have a reduction sequence $\nu$ of $V$
such that $|\sigma_{1}|+|\sigma_{2}|\leq|\nu|$. By the second part of Theorem
20, it is enough to restrict our attention to the case when $\sigma_{1}$ and
$\sigma_{2}$ are standard. We may assume that the head-redex of $U$ is
involved in $\sigma_{1}$, otherwise the result is trivial. Furthermore, we may
suppose that $\mu\alpha.\langle M,[\alpha]z\rangle$ is reduced in
$|\sigma_{1}|$ with all of its arguments $M_{1},\dots,M_{n}$. Then
$\sigma_{1}$ is of the form
$U\mapsto^{\xi}\mu\alpha.\langle
M[\alpha:=_{r}M_{1}]\dots[\alpha:=_{r}M_{n}],[\alpha](z\;M_{1}\dots
M_{n})\rangle$
$\mapsto^{\zeta}\mu\alpha.\langle M^{\prime},[\alpha](z\;M_{1}\dots
M_{n})\rangle\;\mapsto^{\zeta^{*}}\;\mu\alpha.\langle
M^{\prime},[\alpha](z\;M_{1}^{\prime}\dots M_{n}^{\prime})\rangle$,
where $M[\alpha:=_{r}M_{1}]\dots[\alpha:=_{r}M_{n}]\mapsto^{\zeta}M^{\prime}$
and $\zeta^{*}=\zeta_{1}\\#\dots\\#\zeta_{n}$ with
$M_{i}\mapsto^{\zeta_{i}}M_{i}^{\prime}$ for $1\leq i\leq n$. Let
$\xi^{\prime}$ be $V\mapsto^{\xi^{\prime}}\mu\alpha.\langle
M[\alpha:=_{r}M_{1}]\dots[\alpha:=_{r}M_{n}],[\alpha](z\;N\;M_{1}\dots
M_{n})\rangle$, then choosing $\nu$ as
$\nu=\xi^{\prime}\\#\zeta\\#\sigma_{2}\\#\zeta^{*}$ is appropriate.

######  Lemma 29.

Let $M=(\lambda x.M_{1})M_{2}\overrightarrow{P}$ and
$N=(M_{1}[x:=M_{2}]\;\overrightarrow{P^{\prime}})$.

  1. (1)

If $x\in Fv(M_{1})$ and $N$ is strongly normalizable, then $M$ is also
strongly normalizable and $\eta(M)=\eta(N)+1$.

  2. (2)

If $x\notin Fv(M_{1})$ and $N,M_{2}$ are strongly normalizable, then $M$ is
also strongly normalizable and $\eta(M)=\eta(N)+\eta(M_{2})+1$.

######  Proof 4.8.

  1. (1)

Let $M\mapsto^{\sigma}U$ be an arbitrary reduction sequence, we are going to
show that $|\sigma|\leq\eta(N)+1$, from which the result follows. We may
suppose that $(\lambda x.M_{1})M_{2}$ is involved in $\sigma$. Then $\sigma$
is of the following form for some $\sigma_{1}$ and $\sigma_{2}$, $M=(\lambda
x.M_{1})M_{2}\overrightarrow{P}\mapsto^{\sigma_{1}}M^{\prime}=(\lambda
x.M_{1}^{\prime})M_{2}^{\prime}\overrightarrow{P^{\prime}}\rightarrow(M_{1}^{\prime}[x:=M_{2}^{\prime}]\;\overrightarrow{P^{\prime}})\mapsto^{\sigma_{2}}U$
where $M_{i}\mapsto^{\nu_{i}}M_{i}^{\prime}$ $(i\in\\{1,2\\})$,
$\overrightarrow{P}\mapsto^{\nu_{3}}\overrightarrow{P^{\prime}}$ and
$\sigma_{1}=\nu_{1}\\#\nu_{2}\\#\nu_{3}$. Let $\sigma^{\prime}$ denote the
reduction sequence $M=(\lambda x.M_{1})M_{2}\overrightarrow{P}\rightarrow
N=(M_{1}[x:=M_{2}]\overrightarrow{P})\mapsto^{\sigma^{*}}U$, where
$\sigma^{*}=\nu_{1}^{\prime}\\#\nu_{2}^{\prime}\\#\nu_{3}\\#\sigma_{2}$ and
$\nu_{1}^{\prime}$ is constructed from $\nu_{1}$ by Lemma 13 with
$M_{1}\mapsto^{\nu_{1}}M_{1}^{\prime}$ and $M_{2}$ and $\nu_{2}^{\prime}$ is
obtained by applying Lemma 15 to $M_{1}$ and
$M_{2}\mapsto^{\nu_{2}}M_{2}^{\prime}$. Then $|\sigma|\leq\eta(N)+1$, which is
the desired result.

  2. (2)

Let $M\mapsto^{\sigma}U$ be an arbitrary reduction sequence, it is enough to
show that $|\sigma|\leq\eta(N)+\eta(M_{2})+1$. We may suppose that $(\lambda
x.M_{1})M_{2}$ is involved in $\sigma$. Then $\sigma$ is of the form
$M=(\lambda
x.M_{1})M_{2}\overrightarrow{P}\mapsto^{\sigma_{1}}M^{\prime}=(\lambda
x.M_{1}^{\prime})M_{2}^{\prime}\overrightarrow{P^{\prime}}\rightarrow_{\beta}(M_{1}^{\prime}\;\overrightarrow{P^{\prime}})\mapsto^{\sigma_{2}}U$
where $M_{i}\mapsto^{\nu_{i}}M_{i}^{\prime}$ $(i\in\\{1,2\\})$,
$\overrightarrow{P}\mapsto^{\nu_{3}}\overrightarrow{P^{\prime}}$ and
$\sigma_{1}=\nu_{1}\\#\nu_{2}\\#\nu_{3}$. $\sigma$ can obviously be rearranged
as $M\mapsto^{\nu_{2}}(\lambda
x.M_{1})M^{\prime}_{2}\overrightarrow{P}\rightarrow_{\beta}N=(M_{1}\;\overrightarrow{P})\mapsto^{\nu_{1}\\#\nu_{3}}(M^{\prime}_{1}\;\overrightarrow{P^{\prime}})$,
which yields the result.

######  Lemma 30.

  1. (1)

Let $M=[\alpha]\mu\beta.M_{1}$ and $N=M_{1}[\beta:=\alpha]$. If $N$ is
strongly normalizable, then $M$ is also strongly normalizable and
$\eta(M)=\eta(N)+1$.

  2. (2)

Let $M=\mu\alpha.[\alpha]M_{1}$ be a $\theta$-redex. If $M_{1}$ is strongly
normalizable, then $M$ is also strongly normalizable and
$\eta(M)=\eta(M_{1})+1$.

######  Proof 4.9.

  1. (1)

Assume $\sigma$ is a reduction sequence starting from
$[\alpha]\mu\beta.M_{1}$. We prove $|\sigma|\leq\eta(N)+1$, from which the
result follows. Let $\sigma=[R]\\#\sigma^{\prime}$ for some $\sigma^{\prime}$.
We distinguish the various cases according to the form of $\sigma$.

    1. (a)

If
$[\alpha]\mu\beta.M_{1}\rightarrow^{R}_{\rho}M_{1}[\beta:=\alpha]\mapsto^{\sigma^{\prime}}M_{2}$,
where $\sigma=[R]\\#\sigma^{\prime}$, then the result obviously follows.

    2. (b)

If
$[\alpha]\mu\beta.M_{1})\rightarrow^{R}M_{2}\mapsto^{\sigma^{\prime}}M_{3}$,
where $M_{2}\neq N$ and $\mu\beta.M_{1}$ does not disappear in $\sigma$, then
$M_{3}=[\alpha]\mu\beta.M_{3}^{\prime}$ and
$M_{1}\mapsto^{\sigma}M_{3}^{\prime}$, which yields the result.

    3. (c)

If $[\alpha]\mu\beta.M_{1}\rightarrow^{R}M_{2}\mapsto^{\sigma^{\prime}}M_{3}$,
where $M_{2}\neq N$ and $\mu\beta.M_{1}$ disappears in $\sigma$. Then
$[\alpha]\mu\beta.M_{1}\mapsto^{\sigma^{\prime\prime}}[\alpha]\mu\beta.[\beta]M_{k}\rightarrow_{\theta}[\alpha]M_{k}\mapsto^{\sigma^{\prime\prime\prime}}M_{3}$,
where $\mu\beta.M_{1}$ does not disappear in $\sigma^{\prime\prime}$. We have
$[\alpha]\mu\beta.M_{1}\rightarrow_{\rho}M_{1}[\beta:=\alpha]\mapsto^{\sigma^{\prime\prime}[\beta:=\alpha]}([\beta]M_{k})[\beta:=\alpha]=[\alpha]M_{k}\mapsto^{\sigma^{\prime\prime\prime}}M_{3}$,
and the latter reduction sequence is equal in length to $\sigma$. By this the
result follows.

The reverse direction is obvious.

  2. (2)

Similar to the above one.

######  Lemma 31.

Let $M=(\mu\alpha.M_{1})M_{2}\overrightarrow{P}$ and
$N=(\mu\alpha.M_{1}[\alpha:=_{r}M_{2}])\overrightarrow{P^{\prime}}$.

  1. (1)

If $\alpha\in Fv(M_{1})$ and $N$ is strongly normalizable, then $M$ is also
strongly normalizable $\eta(M)=\eta(N)+1$.

  2. (2)

If $\alpha\notin Fv(M_{1})$ and $N,M_{2}$ are strongly normalizable, then $M$
is also strongly normalizable and $\eta(M)=\eta(N)+\eta(M_{2})+1$.

######  Proof 4.10.

  1. (1)

Let $M\rightarrow^{\sigma}M^{*}$. We prove $|\sigma|\leq\eta(N)+1$, from this
$\eta(M)\leq\eta(N)+1$ follows.

    1. (a)

The redex $R=(\mu\alpha.M_{1})M_{2}$ is involved in $\sigma$.

      1. (i)

If $\mu\alpha.M_{1}$ does not disappear in $\sigma$,
$(\mu\alpha.M_{1})M_{2}\overrightarrow{P}\rightarrow^{\sigma^{\prime}}(\mu\alpha.M_{1}^{\prime})M_{2}^{\prime}\overrightarrow{P^{\prime}}\rightarrow_{\mu}(\mu\alpha.M_{1}^{\prime}[\alpha:=_{r}M_{2}^{\prime}])\overrightarrow{P^{\prime}}\mapsto^{\sigma^{\prime\prime}}M^{*}$.
Then, since $\alpha\in Fv(M_{1})$, by Lemmas 15 and 14, the reduction sequence
$(\mu\alpha.M_{1})M_{2}\overrightarrow{P}\rightarrow^{r}(\mu\alpha.M_{1}[\alpha:=_{r}M_{2}])\overrightarrow{P}\mapsto(\mu\alpha.M_{1}[\alpha:=_{r}M_{2}^{\prime}])\overrightarrow{P}\mapsto(\mu\alpha.M_{1}^{\prime}[\alpha:=_{r}M_{2}^{\prime}])\overrightarrow{P^{\prime}}\mapsto^{\sigma^{\prime\prime}}M^{*}$
has length at least $|\sigma|$, by which the assertion follows.

      2. (ii)

If $\mu\alpha.M_{1}$ disappears in $\sigma$,
$(\mu\alpha.M_{1})M_{2}\overrightarrow{P}\rightarrow^{\sigma^{\prime}}(\mu\alpha.[\alpha]M_{1}^{\prime})M_{2}^{\prime}\overrightarrow{P^{\prime}}\rightarrow_{\theta}$
$(M_{1}^{\prime}\;M_{2}^{\prime}\overrightarrow{P^{\prime}})\mapsto^{\sigma^{\prime\prime}}M^{*}$.
Then, since $\alpha\in Fv(M_{1})$, by Lemmas 15 and 14, the sequence
$(\mu\alpha.M_{1})M_{2}\overrightarrow{P}\rightarrow_{\mu}(\mu\alpha.M_{1}[\alpha:=_{r}M_{2}])\overrightarrow{P}\mapsto(\mu\alpha.([\alpha]M_{1}^{\prime})[\alpha:=_{r}M_{2}^{\prime}])\overrightarrow{P^{\prime}}=(\mu\alpha.[\alpha](M_{1}^{\prime}\;M_{2}^{\prime}))\overrightarrow{P^{\prime}})\rightarrow_{\theta}(M_{1}^{\prime}\;M_{2}^{\prime}\overrightarrow{P^{\prime}})\mapsto^{\sigma^{\prime\prime}}M^{*}$
has length at least $|\sigma|$, which yields the result.

    2. (b)

The redex $R=(\mu\alpha.M_{1})M_{2}$ is not involved in $\sigma$.

      1. (i)

If $\mu\alpha.M_{1}$ does not disappear in $\sigma$, that is,
$(\mu\alpha.M_{1})M_{2}\overrightarrow{P}\mapsto M^{*}=$
$(\mu\alpha.M_{1}^{\prime})M_{2}^{\prime}\overrightarrow{P^{\prime}}$. Then,
since $\alpha\in Fv(M_{1})$, we can apply Lemmas 15 and 14 to assert that
$(\mu\alpha.M_{1})M_{2}\overrightarrow{P}\rightarrow^{R}(\mu\alpha.M_{1}[\alpha:=_{r}M_{2}])\overrightarrow{P}\mapsto(\mu\alpha.M_{1}^{\prime}[\alpha:=_{r}M_{2}^{\prime}])\overrightarrow{P}^{\prime}$
has length at least $|\sigma|+1$.

      2. (ii)

If $\mu\alpha.M_{1}$ disappears in $\sigma$,
$(\mu\alpha.M_{1})M_{2}\overrightarrow{P}\mapsto(\mu\alpha.[\alpha]M_{1}^{\prime})M_{2}^{\prime}\overrightarrow{P^{\prime}}\rightarrow_{\theta}$
$(M_{1}^{\prime}\;M_{2}^{\prime}\overrightarrow{P^{\prime}})\mapsto M^{*}$. By
Lemmas 14 and 15, the sequence
$(\mu\alpha.M_{1})M_{2}\overrightarrow{P}\rightarrow^{R}(\mu\alpha.M_{1}[\alpha:=_{r}M_{2}])\overrightarrow{P}\mapsto(\mu\alpha.([\alpha]M_{1}^{\prime})[\alpha:=_{r}M_{2}^{\prime}])\overrightarrow{P^{\prime}}=(\mu\alpha.[\alpha](M_{1}^{\prime}\;M_{2}^{\prime}))\overrightarrow{P^{\prime}}\rightarrow_{\theta}(M_{1}^{\prime}\;M_{2}^{\prime}\;\overrightarrow{P^{\prime}})\mapsto
M^{*}$ has length at least $|\sigma|+1$, which proves the assertion.

The reverse direction is obvious.

  2. (2)

The proof of $\eta(M)\leq\eta(N)+\eta(M_{2})+1$ is similar to the first part
of the proof of Lemma 31. In this case the verification is made easier by the
fact that, since $\alpha\notin Fv(M_{1})$, $\mu\alpha.M_{1}$ does not
disappear in a reduction sequence starting from $M$. For the converse, let
$N\mapsto^{\sigma}N^{\prime}$ and $M_{2}\mapsto^{\nu}M_{2}^{\prime}$. Then
$(\mu\alpha.M_{1})M_{2}\overrightarrow{P}\rightarrow^{\nu}(\mu\alpha.M_{1})M_{2}^{\prime}\overrightarrow{P}\rightarrow_{\mu}(\mu\alpha.M_{1})\overrightarrow{P}\rightarrow^{\sigma}N^{\prime}$
is a reduction sequence starting from $M$, which means that
$\eta(N)+\eta(M_{2})+1\leq\eta(M)$.

###  4.3. The general case

In what follows we transform every $\lambda\mu$-term $M$ into a $\lambda\mu
I$-term $[\\![M]\\!]_{k}$ with some $k\geq 0$ such that
$\eta(M)\leq\eta([\\![M]\\!]_{k})$, by which, using Corollary 27, we can
obtain a bound for $\eta(M)$.

At this point our presentation slightly differs from that of Xi [Xi.99]. We
have reformulated the translation in [Xi.99], hence we were able to avoid the
minor mistake of Xi when computing the complexity of the obtained
$\lambda\mu$I-terms. For a detailed explanation see [Bat.07]. The interesting
fact for Theorem 38, which is the main result of the paper, is, however, that
we get the same bound for the simply typed $\lambda\mu$-calculus as Xi
obtained for the $\lambda$-calculus, mutatis mutandis. Namely, if we restrict
the notion of the rank of a term in Definition 4.1 by taking into
consideration the $\beta$-redex only, we get the result of Xi for the
$\lambda$-calculus as a special case of Theorem 38. This suggests that the
addition of the classical variables, together with the new rules, does not
increase the computational complexity of the calculus. The idea of the
translation is to introduce new variables of appropriate types in order to
ensure that each bounded variable appears in the terms. The only difficult
case is that of the $\lambda$-abstraction. We explain below the difficulties
lying behind the definition for the case of the abstraction.

  1. (1)

Let $\mathcal{V}=\\{v_{(A,B)}\;|\;A,B\textrm{ are types}\\}$ be a set of
distinguished variables such that for all $A$, $B$ we have
$v_{(A,B)}:A\rightarrow(B\rightarrow A)$, where $v_{(A,B)}$ are either
constants or new variables. Let $M:A$ and $N:B$ be typed $\lambda\mu$-terms.
We denote the term $((v_{(A,B)}\;M)\;N)$ by $\langle M,N\rangle$.

  2. (2)

Let $M$ be a term and $k\geq 0$. The $\lambda\mu$-term $[\\![M]\\!]_{k}$
assigned to $M$ is defined as follows.

     * •

$[\\![M]\\!]_{k}=M$, if $M$ is a variable,

     * •

$[\\![M]\\!]_{k}=\lambda x.\lambda y_{1}.\dots\lambda
y_{m}.\langle([\\![M_{1}]\\!]_{k}\;y_{1}\dots y_{m}),x\rangle$, if $M=\lambda
x.M_{1}$ such that $lh(type(M))\leq k$ and
$type(M_{1})=A_{1}\rightarrow\dots\rightarrow A_{m}\rightarrow B$,
$type(y_{i})=A_{i}$ $(1\leq i\leq m)$ and $B$ is atomic,

     * •

$[\\![M]\\!]_{k}=\lambda x.\langle[\\![M_{1}]\\!]_{k},x\rangle$, if $M=\lambda
x.M_{1}$ and $lh(type(M))>k$,

     * •

$[\\![M]\\!]_{k}=\mu\alpha.\langle[\\![M_{1}]\\!]_{k},[\alpha]z\rangle$, if
$M=\mu\alpha.M_{1}$, where $\alpha\notin Fv(M_{1})$ and $z$ is a new variable
such that $type(M)=type(z)$,

     * •

$[\\![M]\\!]_{k}=\mu\alpha.[\\![M_{1}]\\!]_{k}$, if $M=\mu\alpha.M_{1}$ and
$\alpha\in Fv(M_{1})$,

     * •

$[\\![M]\\!]_{k}=[\alpha][\\![M_{1}]\\!]_{k}$, if $M=[\alpha]M_{1}$,

     * •

$[\\![M]\\!]_{k}=([\\![M_{1}]\\!]_{k}\;[\\![M_{2}]\\!]_{k})$, if
$M=(M_{1}\;M_{2})$.

  3. (3)

For each term $M$ and each $k\geq 0$, we define the contexte $\Gamma_{M,k}$
wich containes the constants $v_{(A,B)}$ of $[\\![M]\\!]_{k}$ with their type
$A\rightarrow(B\rightarrow A)$.

Observe that in the definition above the translations for $\lambda$\- and
$\mu$-abstractions differ. The underlying reason is the fact that in a
$\beta$-reduction the $\lambda$-abstraction disappears while this is not the
case concerning a $\mu$-reduction. Hence, in order to ensure the validity of
Lemma 37, we must make sure that the translation of a term with $\beta$-redex
as head redex can be continued even after the reduction with the head redex.
The main aim with the translation is to produce a $\lambda\mu$I-term
$[\\![M]\\!]_{k}$ from $M$ such that the relation
$\eta(M)\leq\eta([\\![M]\\!]_{k})$ should be valid, which is the statement of
Lemma 37. To achieve this, we reproduce the original $M$ inside its
translation $[\\![M]\\!]_{k}$ in a sense, since, in general, the translation
does not respect reduction, that is, if $M\rightarrow N$, then it is not
necessarily the case that $[\\![M]\\!]_{k}\rightarrow[\\![N]\\!]_{k}$.

The next four lemmas describe some intuitively clear properties of the
translation.

######  Lemma 32.

Let $M$ be a term and $k\geq 0$.

  1. (1)

$[\\![M]\\!]_{k}$ is a $\lambda\mu I$-term.

  2. (2)

$\alpha\in Fv(M)$ iff $\alpha\in Fv([\\![M]\\!]_{k})$ and if $x\in Fv(M)$,
then $x\in Fv([\\![M]\\!]_{k})$.

######  Proof 4.11.

By induction on $comp(M)$.

Observe that, in the case of $\lambda$-variables, $Fv(M)\subseteq
Fv([\\![M]\\!]_{k})$, since $M$ can contain free variables of the form
$v_{(A,B)}$ besides its original parameters.

######  Lemma 33.

If $M$ is a term and $k\geq 0$, then $rank([\\![M]\\!]_{k})=rank(M)$.

######  Proof 4.12.

By induction on $comp(M)$.

######  Lemma 34.

If $M$ be a term and $k\geq 0$, then $comp([\\![M]\\!]_{k})\leq(2k+3)\cdot
comp(M)$.

######  Proof 4.13.

The only nontrivial case is $M=\lambda x.M_{1}$. Let $lh(type(\lambda
xM_{1}))=l$. If $k<l$, then $comp([\\![M]\\!]_{k})=comp(\lambda
x.\langle[\\![M_{1}]\\!]_{k},x\rangle)=comp([\\![M_{1}]\\!]_{k})+3\leq(2k+3)\cdot
comp(M)$. If $k\geq l$, then, for some $m\leq l$, we obtain by the induction
hypothesis $comp([\\![M]\\!]_{k})=comp(\lambda x.\lambda y_{1}.\dots\lambda
y_{m}.\langle([\\![M_{1}]\\!]_{k}\;y_{1}\dots
y_{m}),x\rangle)=comp([\\![M_{1}]\\!]_{k})+2m+3\leq(2k+3)\cdot comp(M)$.

######  Lemma 35.

Let $M,N$ be terms and $k\geq 0$.

  1. (1)

If $\Gamma\vdash M:A$, then $\Gamma,\Gamma_{M,k}\vdash[\\![M]\\!]_{k}:A$.

  2. (2)

$[\\![M]\\!]_{k}[x:=[\\![N]\\!]_{k}]=[\\![M[x:=N]]\\!]_{k}$,

  3. (3)

$[\\![M]\\!]_{k}[\alpha:=_{r}[\\![N]\\!]_{k}]=[\\![M[\alpha:=_{r}N]]\\!]_{k}$,

  4. (4)

$[\\![M]\\!]_{k}[\beta:=\alpha]=[\\![M[\beta:=\alpha]]\\!]_{k}$.

######  Proof 4.14.

By induction on $comp(M)$.

Our aim is to prove $\eta(M)\leq\eta([\\![M]\\!]_{k})$. The assertions of
Subsection 4.2 and Lemma 36 prepare the proof of that statement, which is the
claim of Lemma 37.

######  Lemma 36.

If $M\rightarrow M^{\prime}$ and $rank(M)\leq k$, then
$\eta([\\![M^{\prime}]\\!]_{k})+1\leq\eta([\\![M]\\!]_{k})$.

######  Proof 4.15.

By induction on $comp(M)$.

  1. (1)

If $M=\lambda x.M_{1}$, the induction hypothesis applies.

  2. (2)

If $M=(\lambda x.M_{1})M_{2}\dots M_{n}$. We have $lh(type(\lambda
x.M_{1}))\leq k$ by virtue of the assumption $rank(M)\leq k$. Let
$type(M_{1})=A_{1}\rightarrow\dots A_{m}\rightarrow B$, where $B$ is atomic.
Let $M^{\prime}=(M_{1}[x:=M_{2}]\dots M_{n})$, otherwise the induction
hypothesis applies. Since $B$ is atomic, $m\geq n-2$ holds. Then
$[\\![M]\\!]_{k}\rightarrow\lambda y_{1}.\dots\lambda
y_{m}.\langle([\\![M_{1}]\\!]_{k}[x:=[\\![M_{2}]\\!]_{k}]\;y_{1}\dots
y_{m}),[\\![M_{2}]\\!]_{k}\rangle\dots[\\![M_{n}]\\!]_{k}$
$\mapsto\lambda y_{n-1}.\dots\lambda
y_{m}.\langle([\\![M_{1}]\\!]_{k}[x:=[\\![M_{2}]\\!]_{k}]\dots[\\![M_{n}]\\!]_{k}\;y_{n-1}\dots
y_{m}),[\\![M_{2}]\\!]_{k}\rangle$. Lemma 35 gives
$([\\![M_{1}]\\!]_{k}[x:=[\\![M_{2}]\\!]_{k}]\;[\\![M_{3}]\\!]_{k}\dots[\\![M_{n}]\\!]_{k})=([\\![M_{1}[x:=M_{2}]]\\!]_{k}\;[\\![M_{3}]\\!]_{k}\dots[\\![M_{n}]\\!]_{k})=$
$([\\![M_{1}[x:=M_{2}]\;M_{3}\dots M_{n}]\\!]_{k})=[\\![M^{\prime}]\\!]_{k}$,
by which the result follows.

  3. (3)

If $M=(\mu\alpha.M_{1})M_{2}\dots M_{n}$, we may assume again that
$M\rightarrow^{R}M^{\prime}$, where $R=(\mu\alpha.M_{1})M_{2}$.

    1. (a)

If $\alpha\in Fv(M_{1})$, let
$M^{\prime}=(\mu\alpha.M_{1}[\alpha:=_{r}M_{2}]\dots M_{n})$. We have, by
Lemma 35,
$[\\![M]\\!]_{k}=(\mu\alpha.[\\![M_{1}]\\!]_{k})[\\![M_{2}]\\!]_{k}\dots[\\![M_{n}]\\!]_{k}\;\rightarrow\;(\mu\alpha.[\\![M_{1}]\\!]_{k}[\alpha:=_{r}[\\![M_{2}]\\!]_{k}]\dots[\\![M_{n}]\\!]_{k})=(\mu\alpha.[\\![M_{1}[\alpha:=_{r}M_{2}]]\\!]_{k}\dots[\\![M_{n}]\\!]_{k})\;=\;[\\![M^{\prime}]\\!]_{k}$.

    2. (b)

If $\alpha\notin Fv(M_{1})$, then $M^{\prime}=(\mu\alpha.M_{1})M_{3}\dots
M_{n}$ and $[\\![M]\\!]_{k}\rightarrow$
$(\mu\alpha.\langle[\\![M_{1}]\\!]_{k},[\alpha](z\;[\\![M_{2}]\\!]_{k})\rangle)[\\![M_{3}]\\!]_{k}\dots[\\![M_{n}]\\!]_{k}$.
We may assume $\alpha\notin Fv(M_{i})$ $(1\leq i\leq k)$. Then Lemma 28 gives
$\eta((\mu\alpha.\langle[\\![M_{1}]\\!]_{k},[\alpha](z\;[\\![M_{2}]\\!]_{k})\rangle)[\\![M_{3}]\\!]_{k}\dots[\\![M_{n}]\\!]_{k})\geq$
$\eta((\mu\alpha.\langle[\\![M_{1}]\\!]_{k},[\alpha]z\rangle)[\\![M_{3}]\\!]_{k}\dots[\\![M_{n}]\\!]_{k})+\eta([\\![M_{2}]\\!]_{k})+1$.
Moreover, by induction on $n$, we obtain that
$\eta([\\![M^{\prime}]\\!]_{k})\leq$
$\eta((\mu\alpha.\langle[\\![M_{1}]\\!]_{k},[\alpha]z\rangle)[\\![M_{3}]\\!]_{k}\dots[\\![M_{n}]\\!]_{k})$,
by which the result follows.

  4. (4)

If $M=[\alpha]M_{1}$, the only interesting case is
$M=[\alpha]\mu\beta.M_{1}^{\prime}\rightarrow M_{1}^{\prime}[\beta:=\alpha]$.
If $\beta\in Fv(M_{1}^{\prime})$, then
$[\\![M]\\!]_{k}=(\alpha\;\mu\beta.[\\![M_{1}^{\prime}]\\!]_{k})$. Otherwise,
$[\\![M]\\!]_{k}=[\alpha]\mu\beta.\langle[\\![M_{1}^{\prime}]\\!]_{k},[\beta]z\rangle$.
Applying Lemma 35, in both cases we obtain the result.

  5. (5)

The case $M=\mu\alpha.M_{1}$ is analogous to the previous one.

  6. (6)

If $M=(x\;M_{1}\overrightarrow{P})$, the induction hypothesis applies.

Prior to proving the next lemma, we demonstrate with an example that the
hypothesis $rank(M)\leq k$ was indeed necessary for the validity of Lemma 36.

Let $M=(\lambda x.\lambda y.y\;x)\;y$. Then $M^{\prime}=(\lambda y.y)y$.
Assume $x,y:A$. Then $rank(\lambda x.\lambda y.y)=2$, which means $rank(M)=2$.
Let $k=1$. Then

$[\\![M]\\!]_{1}=((\lambda x.\langle[\\![\lambda y.y]\\!]_{1},x\rangle)x)y$,
and $[\\![M^{\prime}]\\!]_{1}=(\lambda y.\langle y,y\rangle)y$.

Since $[\\![\lambda y.y]\\!]_{1}=\lambda y.\langle y,y\rangle$ is not a redex,
we have $\eta([\\![M]\\!]_{1})=\eta([\\![M^{\prime}]\\!]_{1})=1$, thus the
statement of Lemma 36 is not valid for $M$.

######  Lemma 37.

If $M$ is a $\lambda\mu$-term such that $rank(M)\leq k$, then
$\eta(M)\leq\eta([\\![M]\\!]_{k})$.

######  Proof 4.16.

By induction on $(\eta([\\![M]\\!]_{k}),comp(M))$.

  1. (1)

If $M=\lambda x.M_{1}$, then, by the induction hypothesis we have the result.

  2. (2)

If $M=(x\;M_{1}\dots M_{n})$, then, by the induction hypothesis,
$\eta(M)=\eta(M_{1})+\dots+\eta(M_{n})\leq\eta([\\![M_{1}]\\!]_{k})+\dots+\eta([\\![M_{n}]\\!]_{k})=\eta([\\![M]\\!]_{k})$.

  3. (3)

If $M=(\lambda x.M_{1})M_{2}\dots M_{n}$, let
$M^{\prime}=(M_{1}[x:=M_{2}]\dots M_{n})$. If follows from Lemma 22 that
$rank(M^{\prime})\leq k$.

     * -

$x\in Fv(M_{1})$: By Lemmas 36 and 29 and the induction hypothesis,
$\eta(M)=\eta(M^{\prime})+1\leq\eta([\\![M^{\prime}]\\!]_{k})+1\leq\eta([\\![M]\\!]_{k})$.

     * -

$x\notin Fv(M_{1})$: $[\\![M]\\!]_{k}\rightarrow_{\beta}\lambda
y_{1}.\dots\lambda y_{m}.\langle([\\![M_{1}]\\!]_{k}\;y_{1}\dots
y_{m}),[\\![M_{2}]\\!]_{k}\rangle\ldots[\\![M_{n}]\\!]_{k}=U$. By Lemma 29, we
are ready, if we prove $\eta([\\![(M_{1}\;M_{3}\ldots
M_{n})]\\!]_{k}\leq\eta(U)$. By the choice of $m$, we have $m\geq n-2$, hence
$U\mapsto\langle([\\![M_{1}]\\!]_{k}\;[\\![M_{3}]\\!]_{k}\dots[\\![M_{m}]\\!]_{k}),[\\![M_{2}]\\!]_{k}\rangle\ldots[\\![M_{n}]\\!]_{k}$,
from which the conclusion follows.

  4. (4)

Let $M=(\mu\alpha.M_{1})M_{2}\dots M_{n}$.

     * -

If $\alpha\in Fv(M_{1})$, let
$M^{\prime}=(\mu\alpha.M_{1}[\alpha:=_{r}M_{2}]\dots M_{n})$. Then
$rank(M^{\prime})\leq k$ by Lemma 22 again. We have, by Lemmas 36, 31 and the
induction hypothesis,
$\eta(M)=\eta(M^{\prime})+1\leq\eta([\\![M^{\prime}]\\!]_{k})+1=\eta([\\![M]\\!]_{k})$.

     * -

If $\alpha\notin Fv(M_{1})$, let $M^{\prime}=(\mu\alpha.M_{1})M_{3}\dots
M_{n}$. We have
$[\\![M]\\!]_{k}\rightarrow(\mu\alpha.\langle[\\![M_{1}]\\!]_{k},[\alpha](z\;[\\![M_{2}]\\!]_{k})\rangle)[\\![M_{3}]\\!]_{k}\dots[\\![M_{n}]\\!]_{k}$,
which, together with Lemmas 31, 28, 22 and the induction hypothesis, yields
that
$\eta(M)\leq\eta(M^{\prime})+\eta(M_{2})+1\leq\eta([\\![M^{\prime}]\\!]_{k})+\eta([\\![M_{2}]\\!]_{k})+1\leq\eta([\\![M]\\!]_{k})$.

  5. (5)

Let $M=\mu\alpha.M_{1}$.

     * -

Assume $\alpha\in Fv(M_{1})$. If $\mu\alpha.M_{1}=\mu\alpha.[\alpha]M_{2}$ is
a $\theta$-redex, then, by Lemmas 30, 22 and the induction hypothesis,
$\eta(M)=\eta(M_{2})+1\leq\eta([\\![M_{2}]\\!]_{k})+1=\eta([\\![M]\\!]_{k})$.
Otherwise, let $\mu\alpha.M_{1}\rightarrow M^{\prime}$. Since
$\mu\alpha.M_{1}$ is not a $\theta$-redex, we have
$M^{\prime}=\mu\alpha.M_{1}^{\prime}$ together with $rank(M^{\prime})\leq k$.
By Lemma 36, we can apply the induction hypothesis to $M^{\prime}$, that is,
$\eta(\mu\alpha.M_{1}^{\prime})+1\leq\eta([\\![\mu\alpha.M_{1}^{\prime}]\\!]_{k})+1\leq\eta([\\![\mu\alpha.M_{1}]\\!]_{k})$.
But $M^{\prime}$ was arbitrary and
$\eta(M)=max\\{\eta(M^{\prime})+1\;|\;M\rightarrow M^{\prime}\\}$, which
proves our assertion.

     * -

If $\alpha\notin Fv(M_{1})$, then we can apply the induction hypothesis to
$M_{1}$.

  6. (6)

Let $M=[\alpha]\mu\beta.M^{\prime}$. Similar to the previous case by using
Lemma 30.

The following theorem is the main result of our paper. Interestingly, as
mentioned before, we obtain the same bound for the
$\lambda\mu\rho\theta$-calculus as that for the $\lambda$-calculus [Xi.99].

######  Theorem 38.

If $M$ is a $\lambda\mu$-term such that $rank(M)=k$, then every
$\beta\mu\rho\theta$-reduction sequence starting from $M$ is of length less
than $tower(k+1,(2k+3)\cdot comp(M))$.

######  Proof 4.17.

We obtain, by Lemma 34, $comp([\\![M]\\!]_{k})\leq(2k+3)\cdot comp(M)$ and, by
Lemma 33, $rank([\\![M]\\!]_{k})=rank(M)$. These, together with Corollary 27
and Lemma 37, imply
$\eta(M)\leq\eta([\\![M]\\!]_{k})<tower(k+1,comp([\\![M]\\!]_{k}))\leq
tower(k+1,(2k+3)\cdot comp(M))$.

##  5\. Concluding remarks

In what follows, we give a short account of the other possibilities for
obtaining bounds for the reduction sequences in the $\lambda\mu$-calculus. We
could have also begun our paper with these considerations, however the methods
below do not give such full-fledged results as the one discussed above (the
bounds are higher and, more importantly, we were unable to treat the
additional rules by the arguments presented below). By this reason, we decided
to deal with these discussions only after the main argument of the paper. We
could resort to the idea of translating the $\lambda\mu$-calculus into the
$\lambda$-calculus by a CPS-translation such that the sizes of the translated
terms and the lengths of their reduction sequences would depend on the sizes
and lengths of the original terms. Then the bound for the $\lambda$-calculus
would provide us with a bound for the $\lambda\mu$-calculus, too. By examining
this idea, we have come to the conclusion that we were not able to simulate
every reduction rule, if we apply the already existing translations, and even
the bound would be much worse than the one appearing in our result. We
investigate these questions in detail below.

###  5.1. A possible attempt to compute an upper bound for the
$\lambda\mu\rho$-calculus

In the following observations we confine our attention to the case of the
$\lambda\mu\rho$-calculus. In order to establish a bound for the lengths of
reduction sequences of the $\lambda\mu\rho$-calculus it seems to be a natural
idea to try to transform a reduction sequence of the $\lambda\mu\rho$-calculus
into a reduction sequence of the $\lambda$-calculus. We go round this approach
a little bit more detailed: we present the CPS-translation from the simply-
typed $\lambda\mu\rho$-calculus to the simply-typed $\lambda$-calculus
introduced by de Groote [deG.01], and then we give an account of the
possibilities of finding an appropriate bound with this method. The notation
for the CPS-translation is taken from de Groote [deG.01]. As to a bound for
the simply-typed $\lambda$-calculus we regard the one presented in Xi [Xi.99].

Let $o$ be some distinguished atomic type.

  1. (1)

For every type $A$, we define the three types $A^{o}$, $\sim A$ and
$\overline{A}$ by : $\sim A=A\rightarrow o$, $\overline{A}=\sim\sim A^{o}$,
${\perp}^{o}=o$, $X^{o}=X$, if $X$ is atomic, and $(B\rightarrow
C)^{o}=\overline{B}\rightarrow\overline{C}$.

  2. (2)

Let $\Gamma_{\lambda}$ (resp. $\Gamma_{\mu}$) denote a $\lambda$-context
(resp. $\mu$-context), that is, a finite (possibly empty) set of declarations
$x_{1}:A_{1},\dots,x_{n}:A_{n}$ (resp. $\alpha_{1}:\neg
B_{1},\dots,\alpha_{m}:\neg B_{m}$). We define $\overline{\Gamma_{\lambda}}$
(resp. $\sim\Gamma_{\mu}^{o}$) by
$x_{1}:\overline{A_{1}},\dots,x_{n}:\overline{A_{n}}$ (resp. $\alpha_{1}:\sim
B_{1}^{o},\dots,\alpha_{m}:\sim B_{m}^{o}$).

We suppose that the $\mu$ -variables of the $\lambda\mu\rho$-calculus are also
$\lambda$ -variables of the $\lambda$-calculus.

The CPS-translation $\overline{M}$ of a $\lambda\mu\rho$-term $M$ is defined
as follows.

  * •

$\overline{x}=\lambda k.(x\;k)$,

  * •

$\overline{\lambda x.M}=\lambda k.(k\;\lambda x.\overline{M})$,

  * •

$\overline{(M\;N)}=\lambda k.(\overline{M}\;\lambda m.(m\;\overline{N}\;k))$,

  * •

$\overline{\mu\alpha.M}=\lambda\alpha.(\overline{M}\;\lambda k.k)$,

  * •

$\overline{[\alpha]M}=\lambda k.(\overline{M}\;\alpha)$.

######  Lemma 39.

Let $M:A$ be a typable term with $\lambda$-context $\Gamma_{\lambda}$ and
$\mu$-context $\Gamma_{\mu}$. Then its CPS-translation, $\overline{M}$, is
typable with contexts $\overline{\Gamma_{\lambda}}$ and
$\sim\Gamma_{\mu}^{o}$.

Let $=_{\lambda}$ (resp. $=_{\mu}$) denote the relation defined as the
reflexive, symmetric, transitive closure of the $\beta$-reduction (resp. that
of the union of the $\beta$-, $\mu$\- and $\rho$-reductions). As usual, we
consider terms differing in renaming of bound variables as equals.

Then, in [deG.94], de Groote proves the following result.

######  Lemma 40.

Let $M,N$ be $\lambda\mu\rho$-terms. Then $M=_{\mu}N$ iff
$\overline{M}=_{\lambda}\overline{N}$.

Unfortunately, in Lemma 40, $\overline{M}\mapsto_{\lambda}\overline{N}$ does
not hold in general, even if $M\mapsto_{\mu}N$. So on one hand we cannot use
the CPS-translation to imitate the reduction sequences in the
$\lambda\mu\rho$-calculus by reduction sequences in the $\lambda$-calculus. On
the other hand there can be another drawback of this approach.
In general, we could make use of the CPS-translation for estimating bounds of
reduction sequences if, for any $M\mapsto_{\mu}^{\sigma}NF(M)$, we could find
a $\nu$ with $\overline{M}\mapsto_{\lambda}^{\nu}NF(\overline{M})$ such that
$|\sigma|\leq c.|\nu|$ with some constant $c$, where $NF(M)$ and
$NF(\overline{M})$ denote the (unique) normal form of $M$ in the
$\lambda\mu\rho$-calculus and of $\overline{M}$ in the $\lambda$-calculus,
respectively. In fact, we even know that
$NF(\overline{M})=\overline{\overline{NF(M)}}$, where
$\overline{\overline{M}}$ stands for the so called modified CPS-translation of
the term $M$ ( de Groote [deG.94]).