Strong normalization of lambda-Sym-Prop- and lambda-bar-mu-mu-tilde-star- calculi

TL;DR

This paper provides an arithmetical proof of strong normalization for lambda-Sym-Prop and establishes a translation to lambda-bar-mu-mu-tilde-star-calculus, introducing the concept of zoom-in sequences of redexes.

Contribution

It offers a new arithmetical proof of strong normalization for lambda-Sym-Prop and connects it to lambda-bar-mu-mu-tilde-star-calculus using a novel method involving zoom-in sequences.

Findings

Proved strong normalization of lambda-Sym-Prop

Established translation to lambda-bar-mu-mu-tilde-star-calculus

Introduced the concept of zoom-in sequences of redexes

Abstract

In this paper we give an arithmetical proof of the strong normalization of lambda-Sym-Prop of Berardi and Barbanera [1], which can be considered as a formulae-as-types translation of classical propositional logic in natural deduction style. Then we give a translation between the lambda-Sym-Prop-calculus and the lambda-bar-mu-mu-tilde-star-calculus, which is the implicational part of the lambda-bar-mu-mu-tilde-calculus invented by Curien and Herbelin [3] extended with negation. In this paper we adapt the method of David and Nour [4] for proving strong normalization. The novelty in our proof is the notion of zoom-in sequences of redexes, which leads us directly to the proof of the main theorem.

Equations

$$A:=\alpha \mid {\alpha }^{\perp }\mid A\wedge A\mid A\vee A$$

$$C:=A\mid \perp .$$

$$var\frac{}{\Gamma ,x:A⊢x:A}\text{vspace}.1cm$$

$$\mathcal{A}=\{M|M⪯U\text{ and }M\text{ is proper}\},$$

$$\mathcal{B}=\{V|V⪯\sigma (b)\text{ for some }b\in dom(\sigma )\text{ and }V\text{ is proper}\}.$$

$$\begin{array}[]{ccccccccc}p&::=&\lfloor t,e\rfloor&&&&&&\\ t&::=&x&\mid&\lambda xt&\mid&\mu\alpha p&&\\ e&::=&\alpha&\mid&(t.e)&\mid&\tilde{\mu}xp&&\end{array}$$

$$\begin{array}[]{ll}\begin{minipage}[t]{180.0pt} $Var_{1}\;\;\;\displaystyle\frac{}{\Gamma,x:A\;\rhd\;x:A\;|\;\triangle}$\\ \end{minipage}&\begin{minipage}[t]{180.0pt} $Var_{2}\;\;\;\displaystyle\frac{}{\Gamma\;|\;\alpha:A\;\rhd\;\alpha:A,\triangle}$\\ \end{minipage}\\ \begin{minipage}[t]{180.0pt} $\lambda\;\;\;\displaystyle\frac{\Gamma,x:A\;\rhd\;t:B\;|\;\triangle}{\Gamma\;\rhd\;\lambda xt:A\rightarrow B\;|\;\triangle}$\\ \end{minipage}&\begin{minipage}[t]{180.0pt} $(.)\;\;\;\displaystyle\frac{\Gamma\;\rhd\;t:A\;|\;\triangle\;\;\;\Gamma\;|\;e:B\;\rhd\;\triangle}{\Gamma\;|\;(t.e):A\rightarrow B\;\rhd\;\triangle}$\\ \end{minipage}\end{array}$$

$$\lfloor ,\rfloor \frac{\Gamma ⊳t:A|△\Gamma |e:A⊳△}{\lfloor t,e\rfloor :(\Gamma ⊳△)}$$

$$\begin{array}[]{ll}\begin{minipage}[t]{180.0pt} $\mu\;\;\;\displaystyle\frac{p:(\Gamma\;\rhd\;\alpha:A,\triangle)}{\Gamma\;\rhd\;\mu\alpha p:A\;|\;\triangle}$\\ \end{minipage}&\begin{minipage}[t]{180.0pt} $\tilde{\mu}\;\;\;\displaystyle\frac{p:(\Gamma,x:A\;\rhd\;\triangle)}{\Gamma\;|\;\tilde{\mu}xp:A\;\rhd\;\triangle}$\\ \end{minipage}\end{array}$$

$$\begin{array}[]{ccccccccc}p&::=&\lfloor t,e\rfloor&&&&&&\\ t&::=&x&\mid&\lambda x\,t&\mid&\mu\alpha\,p&\mid&\overline{e}\\ e&::=&\alpha&\mid&(t.e)&\mid&\tilde{\mu}x\,p&\mid&\widetilde{t}\end{array}$$

$$\begin{array}[]{ll}\begin{minipage}[t]{180.0pt} $\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\overline{.}\;\;\;\displaystyle\frac{\Gamma\;|\;e:A\rhd\triangle}{\Gamma\rhd\overline{e}:A^{\bot}\;|\;\triangle}$\\ \end{minipage}&\begin{minipage}[t]{180.0pt} $\widetilde{.}\;\;\;\displaystyle\frac{\Gamma\rhd t:A\;|\;\triangle}{\Gamma\;|\;\widetilde{t}:A^{\bot}\rhd\triangle}$\\ \end{minipage}\end{array}$$

$$p^{\mathfrak{e}}=(u^{\mathfrak{e}}\star v^{\mathfrak{e}})\text{ if p=⌊v,u⌋}.$$

$$t^{\mathfrak{e}}=\left\{\begin{array}[]{ll}x&\;\;\;\textrm{ if $\;\;t=x$},\\ \lambda y(\lambda x({\pi}_{2}(y)\star u^{\mathfrak{e}})\star{\pi}_{1}(y))&\;\;\;\textrm{ if $\;\;t=\lambda xu$},\\ \lambda x(e^{\mathfrak{e}}\star t^{\mathfrak{e}})&\;\;\;\textrm{ if $\;\;t=\tilde{\mu}x\lfloor t,e\rfloor$},\\ u^{\mathfrak{e}}&\;\;\;\textrm{ if $\;\;t=\overline{u}$}.\end{array}\right.$$

$$e^{\mathfrak{e}}=\left\{\begin{array}[]{ll}\overline{\alpha}&\;\;\;\textrm{ if $\;\;e=\alpha$},\\ \langle t^{\mathfrak{e}},h^{\mathfrak{e}}\rangle&\;\;\;\textrm{ if $\;\;e=t.h$},\\ \lambda\overline{\alpha}(e^{\mathfrak{e}}\star t^{\mathfrak{e}})&\;\;\;\textrm{ if $\;\;e=\mu\alpha\lfloor t,e\rfloor$},\\ h^{\mathfrak{e}}&\;\;\;\textrm{ if $\;\;e=\widetilde{h}$}.\end{array}\right.$$

$$\frac{\Gamma ,x:A⊳u:B|△}{\Gamma ⊳\lambda xu:A\to B|△}.$$

$${\Gamma }^{\mathfrak{e}},({△}^{\mathfrak{e}}{)}^{\perp },x:A^{\mathfrak{e}},y:A^{\mathfrak{e}}\wedge (B^{\mathfrak{e}}{)}^{\perp }⊢u^{\mathfrak{e}}:B^{\mathfrak{e}},$$

$${\Gamma }^{\mathfrak{e}},({△}^{\mathfrak{e}}{)}^{\perp },y:A^{\mathfrak{e}}\wedge (B^{\mathfrak{e}}{)}^{\perp }⊢{\pi }_1(y):A^{\mathfrak{e}},$$

$${\Gamma }^{\mathfrak{e}},({△}^{\mathfrak{e}}{)}^{\perp },y:A^{\mathfrak{e}}\wedge (B^{\mathfrak{e}}{)}^{\perp }⊢{\pi }_2(y):(B^{\mathfrak{e}}{)}^{\perp }.$$

$${\Gamma }^{\mathfrak{e}},({△}^{\mathfrak{e}}{)}^{\perp },x:A^{\mathfrak{e}},y:A^{\mathfrak{e}}\wedge (B^{\mathfrak{e}}{)}^{\perp }⊢({\pi }_2(y)\star u^{\mathfrak{e}}):\perp ,$$

$${\Gamma }^{\mathfrak{e}},({△}^{\mathfrak{e}}{)}^{\perp },y:A^{\mathfrak{e}}\wedge (B^{\mathfrak{e}}{)}^{\perp }⊢\lambda x({\pi }_2(y)\star u^{\mathfrak{e}}):(A^{\mathfrak{e}}{)}^{\perp }.$$

$${\Gamma }^{\mathfrak{e}},({△}^{\mathfrak{e}}{)}^{\perp }⊢\lambda y(\lambda x({\pi }_2(y)\star u^{\mathfrak{e}})\star {\pi }_1(y)):(A^{\mathfrak{e}}{)}^{\perp }\vee B^{\mathfrak{e}}.$$

$$\frac{\Gamma ⊳t:A|△\Gamma |e:B⊳△}{\Gamma |t.e:A\to B⊳△}.$$

$$\frac{{\Gamma }^{\mathfrak{e}},({△}^{\mathfrak{e}}{)}^{\perp }⊢t^{\mathfrak{e}}:A^{\mathfrak{e}}{\Gamma }^{\mathfrak{e}},({△}^{\mathfrak{e}}{)}^{\perp }⊢e^{\mathfrak{e}}:(B^{\mathfrak{e}}{)}^{\perp }}{{\Gamma }^{\mathfrak{e}},({△}^{\mathfrak{e}}{)}^{\perp }⊢⟨t^{\mathfrak{e}},e^{\mathfrak{e}}⟩:A^{\mathfrak{e}}\wedge (B^{\mathfrak{e}}{)}^{\perp }}.$$

$$\frac{\Gamma ⊳t:A|△\Gamma |e:A⊳△}{\lfloor t,e\rfloor :(\Gamma ⊳△)},$$

$$\frac{{\Gamma }^{\mathfrak{e}},({△}^{\mathfrak{e}}{)}^{\perp }⊢t^{\mathfrak{e}}:A^{\mathfrak{e}}{\Gamma }^{\mathfrak{e}},({△}^{\mathfrak{e}}{)}^{\perp }⊢e^{\mathfrak{e}}:(A^{\mathfrak{e}}{)}^{\perp }}{{\Gamma }^{\mathfrak{e}},({△}^{\mathfrak{e}}{)}^{\perp }⊢(e^{\mathfrak{e}}\star t^{\mathfrak{e}}):\perp }.$$

$$M^{\mathfrak{f}}=\left\{\begin{array}[]{ll}x&\;\;\;\textrm{ if $\;\;M=x$},\\ \lfloor Q^{\mathfrak{f}},\widetilde{P^{\mathfrak{f}}}\rfloor&\;\;\;\textrm{ if $\;\;M=(P\star Q)$},\\ \overline{\tilde{\mu}xN^{\mathfrak{f}}}&\;\;\;\textrm{ if $\;\;M=\lambda xN$},\\ \overline{(P^{\mathfrak{f}}.\widetilde{Q^{\mathfrak{f}}})}&\;\;\;\textrm{ if $\;\;M=\langle P,Q\rangle$},\\ \lambda x\mu\beta\lfloor N^{\mathfrak{f}},\widetilde{x}\rfloor&\;\;\;\textrm{ if $\;\;M=\sigma_{1}(N)$, $x\notin Fv(N^{\mathfrak{f}})$ and $\beta\notin Fv(\lfloor N^{\mathfrak{f}},\widetilde{x}\rfloor)$},\\ \lambda xN^{\mathfrak{f}}&\;\;\;\textrm{ if $\;\;M=\sigma_{2}(N)$ and $x\notin Fv(N^{\mathfrak{f}})$}.\end{array}\right.$$

$$\frac{\Gamma ,x:A⊢u:\perp }{\Gamma ⊢\lambda xu:A^{\perp }}.$$

$$\frac{\frac{u^{\mathfrak{f}}:({\Gamma }^{\mathfrak{f}},x:A^{\mathfrak{f}}⊳)}{{\Gamma }^{\mathfrak{f}}|\tilde{\mu }x{u}^{\mathfrak{f}}:A^{\mathfrak{f}}⊳}}{{\Gamma }^{\mathfrak{f}}⊳\overline{\tilde{\mu }x{u}^{\mathfrak{f}}}:(A^{\mathfrak{f}}{)}^{\perp }}.$$

$$\frac{\Gamma ⊢u:A}{\Gamma ⊢{\sigma }_1(u):A\vee B},$$

$$\frac{\frac{\frac{\frac{}{{\Gamma }^{\mathfrak{f}},x:(A^{\mathfrak{f}}{)}^{\perp }⊳u^{\mathfrak{f}}:A^{\mathfrak{f}}|\beta :B^{\mathfrak{f}}}\frac{{\Gamma }^{\mathfrak{f}},x:(A^{\mathfrak{f}}{)}^{\perp }⊳x:(A^{\mathfrak{f}}{)}^{\perp }|\beta :B^{\mathfrak{f}}}{{\Gamma }^{\mathfrak{f}},x:(A^{\mathfrak{f}}{)}^{\perp }|\tilde{x}:A^{\mathfrak{f}}⊳\beta :B^{\mathfrak{f}}}}{\lfloor u^{\mathfrak{f}},\tilde{x}\rfloor :({\Gamma }^{\mathfrak{f}},x:(A^{\mathfrak{f}}{)}^{\perp }⊳\beta :B^{\mathfrak{f}})}}{{\Gamma }^{\mathfrak{f}},x:(A^{\mathfrak{f}}{)}^{\perp }⊳\mu \beta \lfloor u^{\mathfrak{f}},\tilde{x}\rfloor :B^{\mathfrak{f}}}}{{\Gamma }^{\mathfrak{f}}⊳\lambda x\mu \beta \lfloor u^{\mathfrak{f}},\tilde{x}\rfloor :(A^{\mathfrak{f}}{)}^{\perp }\to B^{\mathfrak{f}}}.$$

Full text

Introduction

It was revealed by the works of Murthy [Mur91] and Griffin [Gri90] that the Curry-Howard isomorphism, which establishes a correspondence between natural deduction style proofs in intuitionistic logic and terms of the typed $\lambda$-calculus, can be extended to the case of classical logic, as well. Since their discovery many calculi appeared aiming to give an encoding of proofs formulated either in classical natural deduction or in classical sequent calculus.

The $\lambda\mu$-calculus presented by Parigot in [Par90] finds its origin in the so called Free Deduction (FD). Parigot resolves the deterministic nature of intuitionistic natural deduction: unlike in the case of intuitionistic natural deduction, when eliminating an instance of a cut in FD, there can be several choices for picking out the subdeductions to be transformed. By introducing variables of a new kind, the so called $\mu$-variables, Parigot distinguishes formulas that are not active at the moment but the current continuation can be passed over to them. Besides the usual $\beta$-reduction, Parigot introduces a new reduction rule called the $\mu$-rule corresponding to structural cut eliminations made necessary by the occurrence of new forms of cuts due to the rule in connection with the $\mu$-variables. The result is a calculus, the $\lambda\mu$-calculus (Parigot [Par92]), which is in relation with classical natural deduction. The $\mu^{\prime}$-rule is the symmetric counterpart of the $\mu$-rule. It was introduced by Parigot [Par93] with the intention of keeping the unicity of representation of data (Nour [Nou97]), the price was, however, that confluence had been lost. In the presence of other simplification rules besides $\mu$ and $\mu^{\prime}$, even the strong normalization property is lost (Battyányi [Bat07]).

Historically, the first calculus reflecting the symmetry of classical propositional logic was the $\ls$-calculus of Berardi and Barbanera [BB96] establishing a formulae-as-types connection with natural deduction in classical logic. The calculus $\ls$ uses an involutive negation which is not defined as $A\rightarrow\bot$. There are negated and non-negated atomic types, and the main connective is not the arrow but the classical $\wedge$ and $\vee$. Berardi and Barbanera make use of the natural symmetry of classical logic expressed by the de Morgan laws in defining negated types. In their paper, Berardi and Barbanera proved that $\ls$ is strongly normalizable with a symmetric version of the Tait-Girard reducibility method (Tait [Tai67]). In this paper, leaning on the combinatorial proof applied by David and Nour in [DN07], we prove that $\ls$ is strongly normalizing. The novelty in our proof is the application of so-called zoom-in sequences of redexes, which was inspired by the work in Raamsdonk et al. [RSSX99]. We prove strong normalizability by verifying that it is closed under substitution. From the assumption that $U[x:=V]$ is strongly normalizing and $U$, $V$ are strongly normalizing, we can identify a subterm $U^{\prime}$ of a reduct of $U$ such that $U^{\prime}[x:=V]$ also is strongly normalizing. The reduction sequence leading to $U^{\prime}$ is a so-called zoom-in sequence of redexes: each subsequent element is a subterm of the one-step reduct of the preceding one. We prove that zoom-in sequences have useful invariant properties, which makes it relatively easy for us to set the stage for the main theorem. Due to its intrinsic symmetry in dealing with the typing relation, the $\ls$-calculus also proves to be very close to the calculus named by Nour as classical combinatory logic (CCL). Nour [Nou06] defined a calculus of combinators which is equivalent to the full classical propositional logic in natural deduction style. Then a translation is given in both directions between $\ls$ and CCL.

Curien and Herbelin introduced the $\overline{\lambda}\mu\tilde{\mu}$-calculus (Curien et al. [CH00]), which established a correspondence, via the Curry-Howard isomorphism, between classical Gentzen-style sequent calculus and a logical calculus. The $\overline{\lambda}\mu\tilde{\mu}$-calculus possesses a rather strong symmetry: it has right-hand side and left-hand side terms (also referred to as environments). The strong normalization of the calculus was proved by Polonovski [Pol04], and a proof formalizable in first order Peano arithmetic was found by David and Nour [DN05].

As to the connection between the $\lambda\mu$ and the $\overline{\lambda}\mu\tilde{\mu}$-calculus, Curien and Herbelin [CH00] defined a translation both for the call-by-value and the call-by-name part of the $\lambda\mu$-calculus into the $\overline{\lambda}\mu\tilde{\mu}$-calculus. Rocheteau [Roc05] finished this work by defining simulations between the two calculi in both directions. In this paper we define the $\lmts$-calculus, which is the $\overline{\lambda}\mu\tilde{\mu}$-calculus extended with negation, and we describe translations between the $\lmts$-calculus and the $\ls$-calculus. As a consequence, we obtain that, if one of the calculi is strongly normalizable, then the other one necessary admits this property.

The proof applied in the paper is an adaptation of that of David and Nour [DN05]. David and Nour [DN05] gave arithmetic proofs, that is, proofs formalizable in first-order Peano arithmetic, for the strong normalizability of the $\overline{\lambda}\mu\tilde{\mu}$- and Parigot’s symmetric $\lambda\mu$-calculus. It is demonstrated that the set of strongly normalizable terms are closed under substitution. The goal is achieved by applying implicitly an alternating substitution to find out which part of the substitution would be responsible for being not strongly normalizable provided the basis of the substitution and the terms written in are strongly normalizable. In this paper we reach the same goal by identifying a minimal non strongly normalizing sequence of redexes provided an infinite reduction sequence is given. We call this sequence of redexes a minimal zoom-in reduction sequence. The idea of zoom-in sequence was inspired by Raamsdonk et al. [RSSX99], where perpetual reduction strategies are defined in order to locate the minimal non strongly normalizing subterms of the elements of an infinite reduction sequence. Again, alternating substitutions are defined inductively starting from two sets of terms, and it is proven that zoom-in reduction sequences do not lead out of these substitutions. With this in hand, the method of David and Nour [DN05] can be applied.

We prove the strong normalization of the $\ls$-calculus, though our proof works with some slight modification in the case of the $\overline{\lambda}\mu\tilde{\mu}$-calculus, as well (Battyányi [Bat07]). However, instead of repeating the proof here, we give a translation of the $\ls$-calculus into the $\overline{\lambda}\mu\tilde{\mu}$-calculus, and vice versa. In fact, to make the connection more visible we define the $\lmts$-calculus, which is the $\overline{\lambda}\mu\tilde{\mu}$-calculus extended with terms expressing negated types. Hence, we also obtain a new proof of strong normalization of the $\overline{\lambda}\mu\tilde{\mu}$-calculus.

The paper is organized as follows. In the first section we introduce the $\ls$-calculus of Berardi and Barbanera, and, as the first step towards strong normalization, prove that the permutation rules can be postponed. In the next section we show that the $\beta$, $\beta^{\bot}$, $\pi$ and $\pi^{\bot}$ rules together are strongly normalizing. Section 3 introduces the $\overline{\lambda}\mu\tilde{\mu}$-calculus defined by Curien and Herbelin, and we augment the calculus with negation in order to make the comparison of the $\ls$- and the $\overline{\lambda}\mu\tilde{\mu}$-calculi simpler. Section 4 provides translations between the $\ls$- and the $\lmts$-calculi such that the strong normalization of one of the calculi implies that of the other. The last section contains conclusions with regard to the results of the paper.

1. The $\ls$-calculus

The ${\lambda}^{{\tiny\textit{Sym}}}$-calculus was introduced by Berardi and Barbanera [BB96]. It is organized entirely around the duality in classical logic. It has a negation “built-in”: the negation of $A$ is not defined as $A\rightarrow\bot$. Each type is rather related to its natural negated type by the notion of duality introduced by negation in classical logic. In fact, Berardi and Barbanera defined a calculus equivalent to first order Peano arithmetic. However, we only consider here its propositional part, denoted by $\ls$, since all the other calculi treated by us in this work are concerned with propositional logic.

{defi}

The set of types are built from two sets of base types $\mathcal{A}=\{a,b,\ldots\}$ (atomic types) and ${\mathcal{A}}^{\bot}=\{a^{\bot},b^{\bot},\ldots\}$ (negated atomic types).

1. (1)

The set of m-types is defined by the following grammar

[TABLE]

where $\alpha$ ranges over $\mathcal{A}$ and ${\alpha}^{\bot}$ over ${\mathcal{A}}^{\bot}$. 2. (2)

The set of types is defined by the following grammar

[TABLE] 3. (3)

We define the negation of an m-type as follows

[TABLE]

In this way we get an involutive negation, i.e. for every $m$-type $A$, $(A^{\bot})^{\bot}=A$. 4. (4)

The complexity of a type is defined inductively as follows.

• $cxty(A)=0$, if $A\in\mathcal{A}\cup\mathcal{A}^{\bot}\cup\{\bot\}$.
• $cxty(A_{1}\wedge A_{2})=cxty(A_{1}\vee A_{2})=cxty(A_{1})+cxty(A_{2})+1$.

Then, for every $m$-type $A$, $cxty(A)=cxty(A^{\bot})$.

{defi}

1. (1)

We denote by $Var$ the set of term-variables. The set of terms ${\mathcal{T}}$ of the $\ls$-calculus together with their typing rules are defined as follows. In the definition below the type of a variable must be an $m$-type and $\Gamma$ denotes a context (the set of declarations of variables).

[TABLE]

[TABLE] 2. (2)

We say that $M$ has type $A$, if there is a context $\Gamma$ such that $\Gamma\;\vdash\;M:A$. We consider $A$ as fixed for a certain element $\Gamma\;\vdash\;M:A$ of the typability relation. 3. (3)

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

The complexity of a term of ${\mathcal{T}}$ is defined as follows.

• $cxty(x)=0$,
• $cxty(\langle P_{1},P_{2}\rangle)=cxty((P_{1}\star P_{2}))=cxty(P_{1})+cxty(P_{2})$,
• $cxty(\lambda xP)=cxty(\sigma_{i}(P))=cxty(P)+1$, for $i\in\{1,2\}$.

{defi}

1. (1)

The reduction rules are enumerated below.

[TABLE]

(*) If $E[-]$ is a context with type $\bot$ and $E[-]\neq[-]$, $P$ has type $\bot$ and $E[-]$ does not bind any free variables in $P$. 2. (2)

Let us take the union of the above rules. Let $\rightarrow$ stand for the compatible closure of this union and, as usual, $\rightarrow^{*}$ denote the reflexive, symmetric and transitive closure of $\rightarrow$. The notions of reduction sequence, normal form and normalization are defined with respect to $\rightarrow$. 3. (3)

Let $M,N$ be terms. Assume $M\rightarrow^{*}N$. The length (i.e. the number of steps) of the reduction $\rightarrow^{*}$ is denoted by $lg(M\rightarrow^{*}N)$.

We enumerate below some theoretical properties of the $\ls$-calculus following Berardi and Barbanera [BB96] and de Groote [Gro01].

Proposition 1** (Type-preservation property).**

If $\Gamma\;\vdash\;P:A$ and $P\rightarrow^{*}Q$, then $\Gamma\;\vdash\;Q:A$.

Proposition 2** (Subformula property).**

If $\Pi$ is a derivation of $\Gamma\;\vdash\;P:A$ and $P$ is in normal form, then every type occurring in $\Pi$ is a subformula of a type occurring in $\Gamma$, or a subformula of $A$.

Theorem 3** (Strong normalization).**

If $\Gamma\;\vdash\;P:A$, then $P$ is strongly normalizable, i.e. every reduction sequence starting from $P$ is finite.

Berardi and Barbanera proved Theorem 3 for the extension of the $\ls$-calculus equivalent to first-order Peano-arithmetic. The proof of this result by Berardi and Barbanera [BB96] is based on reducibility candidates, but the definition of the interpretation of a type relies on non-arithmetical fixed-point constructions.

We present a syntactical and arithmetical proof of the strong normalization of the $\ls$-calculus in Section 3. The proof was inspired by a method of David and Nour [DN05]. First we establish that the permutation rules $\eta$, $\eta^{\bot}$ and $Triv$ can be postponed so that we can restrict our attention uniquely to the rules $\beta$, $\beta^{\bot}$, $\pi$, and $\pi^{\bot}$.

1.1. Permutation rules

First of all, we prove that the $\eta$- and $\eta^{\bot}$-reductions can be postponed w.r.t. $\beta$, $\beta^{\bot}$, $\pi$, and $\pi^{\bot}$.

{defi}

1. (1)

Let $\lambda_{\beta\pi}$-calculus denote the calculus with only the reduction rules $\rightarrow_{\beta}$, $\rightarrow_{\beta^{\bot}}$, $\rightarrow_{\pi}$, and $\rightarrow_{\pi^{\bot}}$. 2. (2)

Let $\rightarrow_{\beta\pi}$ stand for the union of $\rightarrow_{\beta},\rightarrow_{\beta^{\bot}},\rightarrow_{\pi},\rightarrow_{\pi^{\bot}}$ and let $M\rightarrow_{e}N$ denote the fact that $M\rightarrow_{\eta}N$ or $M\rightarrow_{\eta^{\bot}}N$. 3. (3)

We denote by $\rightarrow_{\beta_{0}}$ (resp. by $\rightarrow_{\beta^{\bot}_{0}}$) the $\beta$-reduction $(\lambda xM\star N)\rightarrow_{\beta}M[x:=N]$ (resp. the $\beta^{\bot}$-reduction $(N\star\lambda xM)\rightarrow_{\beta^{\bot}}M[x:=N]$), where $x$ occurs at most once in $M$. 4. (4)

We use the standard notation $\rightarrow^{+}$ and $\rightarrow^{*}$ for the transitive and reflexive, transitive closure of a reduction, respectively.

We examine the behaviour of a $\rightarrow_{e}$ rule followed by a $\rightarrow_{\beta}$ and a $\rightarrow_{\beta_{0}}$ rule in Lemmas 4 and 5.

Lemma 4**.**

If $U\rightarrow_{e}V\rightarrow_{\beta}W$, then $U\rightarrow_{\beta}V^{\prime}\rightarrow^{*}_{e}W$ or $U\rightarrow_{\beta_{0}}V^{\prime}\rightarrow_{\beta}W$ for some $V^{\prime}$.

Proof 1.1**.**

We assume $\rightarrow_{e}$ is an $\eta$-reduction, the proof of the case of $\rightarrow_{\beta}$ is similar. The proof is by induction on $cxty(U)$. The only interesting case is $U=(U_{1}\star U_{2})$. We consider only some of the subcases.

1. (1)

$U_{1}=\lambda x(U_{3}\star x)$, with $x\notin Fv(U_{3})$, and $V=(U_{3}\star U_{2})\rightarrow_{\beta}U_{4}[y:=U_{2}]=W$, where $U_{3}=\lambda yU_{4}$. In this case $U=(\lambda x(U_{3}\star x)\star U_{2})\rightarrow_{\beta_{0}}(U_{3}\star U_{2})\rightarrow_{\beta}U_{4}[y:=U_{2}]=W$, so $\rightarrow_{\eta}\rightarrow_{\beta}$ turns into $\rightarrow_{\beta_{0}}\rightarrow_{\beta}$. 2. (2)

$U_{1}=\lambda xU_{3}$, $U_{3}\rightarrow_{\eta}U_{4}$ and $V=(\lambda xU_{4}\star U_{2})\rightarrow_{\beta}U_{4}[x:=U_{2}]=W$. Then $U\rightarrow_{\beta}V^{\prime}=U_{3}[x:=U_{2}]\rightarrow_{\eta}U_{4}[x:=U_{2}]=W$. 3. (3)

$U_{1}=\lambda xU_{3}$, $U_{2}\rightarrow_{\eta}U_{4}$ and $V=(\lambda xU_{3}\star U_{4})\rightarrow_{\beta}U_{3}[x:=U_{4}]=W$. Then $U\rightarrow_{\beta}V^{\prime}=U_{3}[x:=U_{2}]\rightarrow^{*}_{\eta}U_{3}[x:=U_{4}]$.

Lemma 5**.**

If $U\rightarrow_{e}V\rightarrow_{\beta_{0}}W$, then $U\rightarrow_{\beta_{0}}W$ or $U\rightarrow_{\beta_{0}}V^{\prime}\rightarrow_{e}W$ or $U\rightarrow_{\beta_{0}}V^{\prime}\rightarrow_{\beta_{0}}W$ for some $V^{\prime}$.

Proof 1.2**.**

By induction on $cxty(U)$. We assume $U=(U_{1}\star U_{2})$ and we consider some of the more interesting cases.

1. (1)

$U_{1}=\lambda x(U_{3}\star x)$, with $x\notin Fv(U_{3})$, and $V=(U_{3}\star U_{2})\rightarrow_{\beta_{0}}U_{4}[y:=U_{2}]=W$, where $U_{3}=\lambda yU_{4}$. In this case $U=(\lambda x(U_{3}\star x)\star U_{2})\rightarrow_{\beta_{0}}(U_{3}\star U_{2})\rightarrow_{\beta_{0}}U_{4}[y:=U_{2}]=W$, thus $\rightarrow_{\eta}\rightarrow_{\beta_{0}}$ turns into $\rightarrow_{\beta_{0}}\rightarrow_{\beta_{0}}$. 2. (2)

$U_{1}=\lambda xU_{3}$, $U_{3}\rightarrow_{\eta}U_{4}$ and $V=(\lambda xU_{4}\star U_{2})\rightarrow_{\beta_{0}}U_{4}[x:=U_{2}]=W$. Then $U\rightarrow_{\beta_{0}}V^{\prime}=U_{3}[x:=U_{2}]\rightarrow_{\eta}U_{4}[x:=U_{2}]=W$. 3. (3)

$U_{1}=\lambda xU_{3}$, $U_{2}\rightarrow_{\eta}U_{4}$ and $V=(\lambda xU_{3}\star U_{4})\rightarrow_{\beta_{0}}U_{3}[x:=U_{4}]=W$. Then $U\rightarrow_{\beta_{0}}V^{\prime}=U_{3}[x:=U_{2}]\rightarrow_{\eta}U_{3}[x:=U_{4}]$ provided $x$ occurs in $U_{3}$. Otherwise $U\rightarrow_{\beta_{0}}U_{3}=W$.

We obtain easily the following lemma on the behaviour of several $\rightarrow_{e}$ rules followed by a $\rightarrow_{\beta}$ or a $\rightarrow_{\beta_{0}}$ rule.

Lemma 6**.**

*If $U{\rightarrow^{*}_{e}}V\rightarrow_{\beta_{0}}W$, then $U{\rightarrow_{\beta_{0}}}^{+}V^{\prime}{\rightarrow^{*}_{e}}W$ for some $V^{\prime}$, and

$lg(U{\rightarrow_{\beta_{0}}}^{+}V^{\prime}{\rightarrow^{*}_{e}}W)\leq lg(U{\rightarrow^{*}_{e}}V\rightarrow_{\beta_{0}}W)$.*

Proof 1.3**.**

By induction on $lg(U\rightarrow^{*}_{e}V\rightarrow_{\beta_{0}}W)$, using Lemma 5.

Lemma 7**.**

If $U{\rightarrow^{*}_{e}}V\rightarrow_{\beta}W$, then $U{\rightarrow_{\beta}}^{+}V^{\prime}\rightarrow^{*}_{e}W$ for some $V^{\prime}$.

Proof 1.4**.**

By induction on $lg(U{\rightarrow^{*}_{e}}V\rightarrow_{\beta}W)$. Use Lemmas 4 and 6.

Lemma 8**.**

If $U{\rightarrow^{*}_{e}}V\rightarrow_{\beta^{\bot}}W$, then $U{\rightarrow_{\beta^{\bot}}}^{+}V^{\prime}{\rightarrow^{*}_{e}}W$ for some $V^{\prime}$.

Proof 1.5**.**

Similar to that of the previous lemma.

We investigate now how a $\rightarrow_{e}$ rule behaves when followed by a $\rightarrow_{\pi}$ or $\rightarrow_{\pi^{\bot}}$ rule.

Lemma 9**.**

If $U\rightarrow_{e}V\rightarrow_{\pi}W$ (resp. $U\rightarrow_{e}V\rightarrow_{\pi^{\bot}}W$), then $U\rightarrow_{\pi}V^{\prime}\rightarrow_{e}W$ or $U\rightarrow_{\pi}W$ (resp. $U\rightarrow_{\pi^{\bot}}V^{\prime}\rightarrow_{e}W$ or $U\rightarrow_{\pi^{\bot}}W$) for some $V^{\prime}$.

Proof 1.6**.**

Observe that in case of $U\rightarrow_{e}V\rightarrow_{\pi}W$ the following possibilities can occur: either $U=\lambda x(V\star x)$ and $V\rightarrow_{\pi}W$ or $U=(\langle P_{1},P_{2}\rangle\star\sigma(Q))$ and $V=(\langle P_{1}^{\prime},P_{2}^{\prime}\rangle\star\sigma(Q^{\prime}))$, where exactly one of $P_{i}\rightarrow_{e}P_{i}^{\prime}$, $Q\rightarrow_{e}Q^{\prime}$ holds, the other two terms are left unchanged. From this, the statement easily follows.

Lemma 10**.**

If $U\rightarrow^{*}_{e}V\rightarrow_{\beta\pi}W$, then $U\rightarrow^{+}_{\beta\pi}V^{\prime}\rightarrow_{e}W$ for some $V^{\prime}$.

Proof 1.7**.**

By Lemmas 7, 8 and 9.

Lemma 11**.**

If $U\rightarrow^{*}_{e}V\rightarrow^{*}_{\beta\pi}W$, then $U\rightarrow^{+}_{\beta\pi}V^{\prime}\rightarrow^{*}_{e}W$ for some $V^{\prime}$.

Proof 1.8**.**

Follows from the previous lemma.

We are now in a position to prove the main result of the section.

Lemma 12**.**

The $\eta$- and the $\eta_{\bot}$-reductions are strongly normalizing.

Proof 1.9**.**

The $\eta$- and $\eta_{\bot}$-reductions on $M$ reduce the complexity of $M$.

{defi}

1. (1)

Let $\lambda_{\beta\pi\eta}$-calculus denote the calculus obtained from the $\lambda_{\beta\pi}$-calculus by adding the $\eta$- and $\eta^{\bot}$-reductions to it. 2. (2)

Let $\rightarrow_{\beta\pi\eta}$ denote the union of $\rightarrow_{\beta}$, $\rightarrow_{\beta^{\bot}}$, $\rightarrow_{\pi}$, $\rightarrow_{\pi^{\bot}}$, $\rightarrow_{\eta}$ and $\rightarrow_{\eta^{\bot}}$. 3. (3)

Assume $M$ is a term strongly normalizable in the $\lambda_{\beta\pi}$-calculus. Then we denote by $\eta_{\beta\pi}(M)$ the length of the longest reduction sequence $\rightarrow^{*}_{\beta\pi}$ starting from $M$.

Corollary 13**.**

If the $\lambda_{\beta\pi}$-calculus is strongly normalizing, then the $\lambda_{\beta\pi\eta}$-calculus is also strongly normalizing.

Proof 1.10**.**

Let $M$ be a term, we prove by induction on $\eta_{\beta\pi}(M)$ that $M$ is strongly normalizable in the $\lambda_{\beta\pi\eta}$-calculus. Assume $S$ is an infinite ${\beta\pi\eta}$-reduction sequence starting from $M$. If $S$ begins with a $\rightarrow_{\beta\pi}$, then the induction hypothesis applies. In the case when $S$ contains only $\rightarrow_{e}$-reductions, we are done by Lemma 12. Otherwise there is an initial subsequent $M\rightarrow_{e}^{+}M^{\prime}\rightarrow_{\beta\pi}N$. By Lemma 10, we have $M\rightarrow^{+}_{\beta\pi}M^{\prime\prime}\rightarrow^{*}_{e}N$. Thus, we can apply the induction hypothesis to $M^{\prime\prime}$.

In the rest of the section we deal with the rule $Triv$. For strong normalization, it is enough to show that $\rightarrow_{Triv}$ can be postponed w.r.t. $\rightarrow_{\beta\pi\eta}$.

Lemma 14**.**

If $U\rightarrow^{*}_{Triv}V\rightarrow_{\beta\pi\eta}W$, then $U\rightarrow_{\beta\pi\eta}^{+}V^{\prime}\rightarrow^{*}_{Triv}W$ for some $V^{\prime}$.

Proof 1.11**.**

It is enough to prove that if $U\rightarrow_{Triv}V\rightarrow_{\beta\pi\eta}W$, then $U\rightarrow_{\beta\pi\eta}V^{\prime}\rightarrow_{Triv}W$ for some $V^{\prime}$. Observe that if $U=E[V]\rightarrow_{Triv}V\rightarrow_{\beta\pi\eta}W$, then $V:\bot$ and $W:\bot$, from which the statement follows.

Lemma 15**.**

The reduction $\rightarrow_{Triv}$ is strongly normalizing.

Proof 1.12**.**

The reduction $\rightarrow_{Triv}$ on $M$ reduces the complexity of $M$.

Corollary 16**.**

If the $\lambda_{\beta\pi}$-calculus is strongly normalizing, then the ${\lambda}^{\tiny{\textit{Sym}}}_{Prop}$-calculus is also strongly normalizing.

Proof 1.13**.**

By Corollary 13 and Lemmas 14 and 15.

2. Strong normalization of the $\lambda_{\beta\pi}$-calculus

In this section, we give an arithmetical proof for the strong normalization of the $\lambda_{\beta\pi}$-calculus. In the sequel we detail the proofs for the $\beta$- and $\pi$-reductions only, all the proofs below can be extended with the cases of the $\beta^{\bot}$- and $\pi^{\bot}$-reduction rules in a straightforward way. We intend to examine how substitution behaves with respect to strong normalizability. The first milestone in this way is Lemma 20. Before stating the lemma, we formulate some auxiliary statements.

{defi}

1. (1)

Let $SN_{\beta\pi}$ denote the set of strongly normalizable terms of the $\lambda_{\beta\pi}$-calculus. 2. (2)

Let $M\in SN_{\beta\pi}$, then $\eta c(M)$ stands for the pair $\langle\eta_{\beta\pi}(M),cxty(M)\rangle$.

Lemma 17**.**

Let us suppose $M\in SN_{\beta\pi}$, $N\in SN_{\beta\pi}$ and $(M\star N)\notin SN_{\beta\pi}$. Then there are $P\in SN_{\beta\pi}$, $Q\in SN_{\beta\pi}$ such that $M\rightarrow^{*}_{\beta\pi}P$ and $N\rightarrow^{*}_{\beta\pi}Q$ and $(P\star Q)\notin SN_{\beta\pi}$ is a redex.

Proof 2.1**.**

By induction on $\eta c(M)+\eta c(N)$. Assume $M\in SN_{\beta\pi}$, $N\in SN_{\beta\pi}$ and $(M\star N)\notin SN_{\beta\pi}$. When $(M\star N)\rightarrow(M^{\prime}\star N)$ or $(M\star N)\rightarrow(M\star N^{\prime})$, then the induction hypothesis applies. Otherwise $(M\star N)\rightarrow P\notin SN_{\beta\pi}$, and we have the result.

{defi}

1. (1)

A proper term is a term differing from a variable. 2. (2)

For a type $A$, $\Sigma_{A}$ denotes the set of simultaneous substitutions of the form $[x_{1}:=N_{1},\ldots,x_{k}:=N_{k}]$ where $N_{i}$ ($1\leq i\leq n$) is proper and has type $A$. 3. (3)

A simultaneous substitution $\sigma\in\Sigma_{A}$ is said to be in $SN_{\beta\pi}$, if, for every $x\in dom(\sigma)$, $\sigma(x)\in SN_{\beta\pi}$ holds.

Lemma 18**.**

Let $M,N$ be terms such that $M\rightarrow^{*}_{\beta\pi}N$.

1. (1)

If $N=\lambda xP$, then $M=\lambda xP_{1}$ with $P_{1}\rightarrow^{*}_{\beta\pi}P$. 2. (2)

If $N=\langle P,Q\rangle$, then $M=\langle P_{1},Q_{1}\rangle$ with $P_{1}\rightarrow^{*}_{\beta\pi}P$ and $Q_{1}\rightarrow^{*}_{\beta\pi}Q$. 3. (3)

If $N=\sigma_{i}(P)$, then $M=\sigma_{i}(P_{1})$ with $P_{1}\rightarrow^{*}_{\beta\pi}P$, for $i\in\{1,2\}$.

Proof 2.2**.**

Straightforward.

We remark that in the presence of the $\rightarrow_{\eta}$ and $\rightarrow_{\eta}^{\bot}$ rules the above lemma would not work. For example, $\lambda x(y\star x)\rightarrow_{\eta}y$.

Lemma 19**.**

If $M\in SN_{\beta\pi}$ and $x\in Var$, then $(M\star x)\in SN_{\beta\pi}$ (resp. $(x\star M)\in SN_{\beta\pi}$).

Proof 2.3**.**

Let us suppose $M\in SN_{\beta\pi}$ and $(M\star x)\notin SN_{\beta\pi}$. By Lemma 17, we must have $M\rightarrow^{*}_{\beta\pi}\lambda yM_{1}\in SN_{\beta\pi}$ such that $(M\star x)\rightarrow^{*}_{\beta\pi}(\lambda yM_{1}\star x)\rightarrow_{\beta\pi}M_{1}[y:=x]$ and $M_{1}[y:=x]\notin SN_{\beta\pi}$. Being a subterm of a reduct of $M\in SN_{\beta\pi}$, we also have $M_{1}\in SN_{\beta\pi}$. Moreover, $M_{1}[y:=x]$ is obtained from $M_{1}$ by $\alpha$-conversion, hence $M_{1}[y:=x]\in SN_{\beta\pi}$, a contradiction.

{defi}

1. (1)

Let $M,N$ be terms.

1. (a)

We denote by $M\leq N$ (resp. $M<N$) the fact that $M$ is a sub-term (resp. a strict sub-term) of $N$. 2. (b)

We denote by $M\prec N$ the fact that $M\leq P$ for some $N\rightarrow^{+}_{\beta\pi}P$ or $M<N$. We denote by $\preceq$ the reflexive closure of $\prec$. 3. (c)

Let $R$ be a ${\beta\pi}$-redex. We write $M\rightarrow^{R}N$ if $N$ is the term $M$ after the reduction of $R$. 2. (2)

Let ${\mathcal{R}}=[R_{1},\dots,R_{n}]$ where $R_{i}$ is a ${\beta\pi}$-redex $(1\leq i\leq n)$. Then ${\mathcal{R}}$ is called zoom-in if, for every $1\leq i<n$, $R_{i}\rightarrow^{R_{i}}R_{i}^{\prime}$ and $R_{i+1}\leq R_{i}^{\prime}$. Moreover, ${\mathcal{R}}$ is minimal, if, for each $R_{i}=(P_{i}\star Q_{i})$, we have $P_{i}$, $Q_{i}\in SN_{\beta\pi}$ and $(P_{i}\star Q_{i})\notin SN_{\beta\pi}$. We write $M\rightarrow^{\mathcal{R}}N$, if $M\rightarrow^{R_{1}}...\rightarrow^{R_{n}}N$.

For the purpose of proving the strong normalization of the calculus, it is enough to show that the set of strongly normalizable terms is closed under substitution. To this end, we show that, if $U$, $S\in SN_{\beta\pi}$ and $U[x:=S]\notin SN_{\beta\pi}$, then there is a term $W\leq U$ of a special form such that $W\in SN_{\beta\pi}$ and $W[x:=S]\notin SN_{\beta\pi}$. Moreover, we show that the sequence of redexes leading to $W$ is not completely general, this is a zoom-in sequence defined below. Reducing the outermost redexes of a zoom-in sequence preserve some useful properties, which is the statement of Lemma 21.

Lemma 20**.**

Let $U$, $S\in SN_{\beta\pi}$ and suppose $U[x:=S]\notin SN_{\beta\pi}$. Then there are terms $P,V\preceq U$ and a zoom-in minimal ${\mathcal{R}}$ such that $U[x:=S]\rightarrow^{\mathcal{R}}V[x:=S]$, $(x\star P)\leq V$ (or $(P\star x)\leq V$), $P[x:=S]\in SN_{\beta\pi}$ and $(x\star P)[x:=S]\notin SN_{\beta\pi}$ (or $(P\star x)[x:=S]\notin SN_{\beta\pi}$).

Proof 2.4**.**

The proof goes by induction on $\eta c(U)$. If $U$ is other than an application, we can apply the induction hypothesis. Assume $U=(U_{1}\star U_{2})$ with $U_{i}[x:=S]\in SN_{\beta\pi}$ $(i\in\{1,2\})$ and $U[x:=S]\notin SN_{\beta\pi}$. By Lemma 17 and the induction hypothesis we may assume that $(U_{1}\star U_{2})[x:=S]\rightarrow_{\rho}U^{\prime}\notin SN_{\beta\pi}$, where $\rho\in\{\beta,\beta^{\bot},\pi,\pi^{\bot}\}$. Let us suppose $\rho=\beta$, the other cases can be treated similarly. If $U_{1}=\lambda yU_{1}^{\prime}$, then the induction hypothesis applies to $U_{1}^{\prime}[y:=U_{2}]$. Otherwise $U_{1}=x$, and we have obtained the result.

Next we define an alternating substitution: we start from two sets of terms of complementary types and the substitution is defined in a way that we keep track of which newly added sets of substitutions come from which of the two sets. The reason for this is that Lemma 20 in itself is not enough for proving the strong normalizability of $\ls$ even if we would consider the $\beta$ and $\beta^{\bot}$ rules alone. We have to show that, if we start from a term $(U_{1}\star U_{2})$, where $U_{1}$ and $U_{2}\in SN_{\beta\pi}$ and we assume that $U_{1}[x:=U_{2}]\notin SN_{\beta\pi}$, then there are no deep interactions between the terms which come from $U_{1}$ and from $U_{2}$. We can identify a subterm of a reduct of $U_{1}$ which is the cause for being non $SN_{\beta\pi}$, when performing a substitution with $U_{2}$.

{defi}

1. (1)

A set $\mathcal{A}$ of proper terms is called $\preceq$-closed from below if, for all terms $U,U^{\prime}$, if $U^{\prime}\preceq U$, $U\in\mathcal{A}$ and $U^{\prime}$ is proper, then $U^{\prime}\in\mathcal{A}$. 2. (2)

Let $\mathcal{A},\mathcal{B}$ be sets $\preceq$-closed from below and $A$ a type. We define simultaneously two sets of substitutions

1. (a)

$\Pi_{A}(\mathcal{B})\subseteq\Sigma_{A}$ and $\Theta_{A^{\bot}}(\mathcal{A})\subseteq\Sigma_{A^{\bot}}$ as follows.

• • –

$\emptyset\in\Pi_{A}(\mathcal{B})$,

• –

$[y_{1}:=V_{1}\tau_{1},\dots,y_{m}:=V_{m}\tau_{m}]\in\Pi_{A}(\mathcal{B})$ if $V_{i}\in\mathcal{B}$ such that $type(V_{i})=A$ and $\tau_{i}\in\Theta_{A^{\bot}}(\mathcal{A})$ $(1\leq i\leq m)$.

• • –

$\emptyset\in\Theta_{A^{\bot}}(\mathcal{A})$.

• –

$[x_{1}:=U_{1}\rho_{1},\dots,x_{m}:=U_{m}\rho_{m}]\in\Theta_{A^{\bot}}(\mathcal{A})$ if $U_{i}\in\mathcal{A}$ such that $type(U_{i})=A^{\bot}$ and $\rho_{i}\in\Pi_{A}(\mathcal{B})$ $(1\leq i\leq m)$. 2. (b)

Let $\mathcal{S}_{A}(\mathcal{A},\mathcal{B})=\{U\rho\;|\;U\in\mathcal{A}\textrm{ and }\rho\in\Pi_{A}(\mathcal{B})\}\cup\{V\tau\;|\;V\in\mathcal{B}\textrm{ and }\tau\in\Theta_{A^{\bot}}(\mathcal{A})\}$. It is easy to see that, from $U\leq V$ and $V\in\mathcal{S}_{A}(\mathcal{A},\mathcal{B})$, it follows $U\in\mathcal{S}_{A}(\mathcal{A},\mathcal{B})$.

Lemma 21**.**

Let $n$ be an integer, $A$ a type of length $n$ and ${\mathcal{R}}=[R_{1},\dots,R_{m}]$ a zoom-in minimal sequence of redexes. Assume the property $H$ “if $U$, $V\in SN_{\beta\pi}$ and $cxty(type(V))<n$, then $U[x:=V]\in SN_{\beta\pi}$” holds. If $R_{1}\in\mathcal{S}_{A}(\mathcal{A},\mathcal{B})$ for some sets $\mathcal{A}$ and $\mathcal{B}$ $\preceq$-closed from below, then $R_{m}\in\mathcal{S}_{A}(\mathcal{A},\mathcal{B})$.

Proof 2.5**.**

The proof goes by induction on $m$. We prove the induction step from $m=1$ to $m=2$, the proof is the same when $m\in\mathbb{N}$ is arbitrary. We only treat the more interesting cases. Assume $R_{1}\in\mathcal{S}_{A}(\mathcal{A},\mathcal{B})$.

1. (1)

$R_{1}=(\lambda xQ\star S)\rightarrow_{\beta}R_{1}^{\prime}=Q[x:=S]$* and $R_{2}\leq R_{1}^{\prime}$.*

1. (a)

Suppose $R_{1}=U\rho$ for some $U\in\mathcal{A}$ and $\rho\in\Pi_{A}(\mathcal{B})$. Then $U=(U_{1}\star U_{2})$ with $U_{1}\rho=\lambda xQ$ and $U_{2}\rho=S$, and, since $\rho\in\Sigma_{A}$, $U_{1}$ must be proper. Then we have $U_{1}=\lambda xU_{1}^{\prime}$ and $U_{1}^{\prime}\rho=Q$ for some $U_{1}^{\prime}$. Now, $R_{1}^{\prime}=U_{1}^{\prime}[x:=U_{2}]\rho\in\mathcal{S}_{A}(\mathcal{A},\mathcal{B})$, which yields $R_{2}\in\mathcal{S}_{A}(\mathcal{A},\mathcal{B})$. 2. (b)

Assume now $R_{1}=V\tau$. Then $V=(V_{1}\star V_{2})$ with $V_{1}\tau=\lambda xQ$ and $V_{2}\tau=S$, and, since $\tau\in\Sigma_{A^{\bot}}$, $V_{2}$ must be proper. If $V_{1}$ is proper, then, as before, we obtain the result. Otherwise $V_{1}\tau=U\rho=\lambda xQ$. Since $U\in\mathcal{A}$ is proper, $U=\lambda xU_{1}$ and $U_{1}\rho=Q$ for some $U_{1}$. Then $U_{1}\rho_{1}\in\mathcal{S}_{A}(\mathcal{A},\mathcal{B})$ with $\rho_{1}=\rho+[x:=V_{2}\tau]$, since $type(V_{2}\tau)=type(S)=A$. This implies $R_{2}\in\mathcal{S}_{A}(\mathcal{A},\mathcal{B})$. 2. (2)

$R_{1}=(\langle Q_{1},Q_{2}\rangle\star\sigma_{1}(S))\rightarrow_{\pi}(Q_{1}\star S)=R_{1}^{\prime}$* and $R_{2}\leq R_{1}^{\prime}$.*

1. (a)

Assume $R_{1}=U\rho$ for some $U\in\mathcal{A}$ and $\rho\in\Pi_{A}(\mathcal{B})$. Then $U_{1}\rho=\langle Q_{1},Q_{2}\rangle$ and $U_{2}\rho=\sigma_{1}(S)$.

Let $U_{1}$ and $U_{2}$ be proper. Then $U_{1}=\langle U_{1}^{\prime},U_{1}^{\prime\prime}\rangle$ and $U_{2}=\sigma_{1}(U_{2}^{\prime})$ such that $U_{1}^{\prime}\rho=Q_{1}$, $U_{1}^{\prime\prime}\rho=Q_{2}$ and $U_{2}^{\prime}\rho=S$. We have $R_{1}^{\prime}=(U_{1}^{\prime}\star U_{2}^{\prime})\rho\in\mathcal{S}_{A}(\mathcal{A},\mathcal{B})$, which yields the result.

• -

Assume $U_{2}\in Var$. Then $V\tau=\sigma(S)$, and $cxty(type(S))<$

$cxty(type(\sigma S))=n$. Then assumption $H$ and the fact that $\langle Q_{1},Q_{2}\rangle\in SN_{\beta\pi}$, together with Lemma 19, lead to $(Q_{1}\star S)\in SN_{\beta\pi}$, which is not possible. Since $\rho\in\Sigma_{A}$, $U_{1}\in Var$ is impossible. 2. (b)

Assume $R_{1}=V\tau$ for some $V\in\mathcal{B}$ and $\tau\in\Theta_{A^{\bot}}(\mathcal{A})$. Then $V_{1}\tau=\langle Q_{1},Q_{2}\rangle$ and $V_{2}\tau=\sigma_{1}(S)$, where $V=(V_{1}\star V_{2})$.

Let $V_{1}$ and $V_{2}$ be proper. Then $V_{1}=\langle V_{1}^{\prime},V_{1}^{\prime\prime}\rangle$ and $V_{2}=\sigma_{1}(V_{2}^{\prime})$ such that $V_{1}^{\prime}\tau=Q_{1}$, $V_{1}^{\prime\prime}\tau=Q_{2}$ and $V_{2}^{\prime}\tau=S$. We have $R_{1}^{\prime}=(V_{1}^{\prime}\star V_{2}^{\prime})\tau\in\mathcal{S}_{A}(\mathcal{A},\mathcal{B})$.

• -

Assume $V_{1}\in Var$. Then $U\rho=\langle Q_{1},Q_{2}\rangle$, where $cxty(type(Q_{1}))<$

$cxty(type(\langle Q_{1},Q_{2}\rangle))=n$. Then assumption $H$ and the fact that $S\in SN_{\beta\pi}$, together with Lemma 19, lead to $(Q_{1}\star S)\in SN_{\beta\pi}$, which is not possible. Since $\tau\in\Sigma_{A^{\bot}}$, the case of $V_{2}\in Var$ is impossible.

The next lemma identifies the subterm of $U$ being responsible for the non strong normalizability of $U[x:=V]$.

Lemma 22**.**

Let $n$ be an integer and $A$ a type of length $n$. Assume the property $H$ “if $U$, $V\in SN_{\beta\pi}$ and $cxty(type(V))<n$, then $U[x:=V]\in SN_{\beta\pi}$” holds.

1. (1)

Let $U$ be a proper term, $\sigma\in\Sigma_{A}$ and $a\notin Im(\sigma)$. If $U\sigma,P\in SN_{\beta\pi}$ and $U\sigma[a:=P]\notin SN_{\beta\pi}$, then there exists $U^{\prime}$ such that $(U^{\prime}\star a)\preceq U$ and $\sigma^{\prime}\in\Sigma_{A}$ such that $U^{\prime}\sigma^{\prime}\in SN_{\beta\pi}$ and $(U^{\prime}\sigma^{\prime}\star a)[a:=P]\notin SN_{\beta\pi}$. 2. (2)

Let $U$ be a proper term, $\sigma\in\Sigma_{A^{\bot}}$ and $a\notin Im(\sigma)$. If $U\sigma,P\in SN_{\beta\pi}$ and $U\sigma[a:=P]\notin SN_{\beta\pi}$, then there exists $U^{\prime}$ such that $(a\star U^{\prime})\preceq U$ and $\sigma^{\prime}\in\Sigma_{A^{\bot}}$ such that $U^{\prime}\sigma^{\prime}\in SN_{\beta\pi}$ and $(a\star U^{\prime}\sigma^{\prime})[a:=P]\notin SN_{\beta\pi}$.

Proof 2.6**.**

Let us consider only case (1). We identify the reason of $U\sigma[a:=P]$ being non strongly normalizable, we find a subterm $(U^{\prime}\star a)$ of a reduct of $U$ such that, for a substituted instance of $(U^{\prime}\star a)$, $(U^{\prime}\star a)\sigma^{\prime}\in SN_{\beta\pi}$ and $(U^{\prime}\star a)\sigma^{\prime}[a:=P]\notin SN_{\beta\pi}$. This will contradict by some minimality assumption concerning $U$ in the next lemma. For this we define two sets of substitutions as in Definition 2 with the sets $\mathcal{A}$ and $\mathcal{B}$ as below. We note that Property H of the previous lemma implicitly ensures that the type of $U$ and the type of the elements in $\sigma$ can be of the same lengths.

Let

[TABLE]

[TABLE]

Then $U\sigma\in\mathcal{S}_{A}(\mathcal{A},\mathcal{B})$. By Lemma 20, there exists a minimal zoom-in ${\mathcal{R}}=[R_{1},\dots,R_{n}]$ and there are terms $U^{*}$ and $V\preceq U\sigma$ such that $U\sigma[a:=P]\rightarrow^{\mathcal{R}}V[a:=P]$ and $(U^{*}\star a)\leq V$ and $(U^{*}\star a)\in SN_{\beta\pi}$ and $(U^{*}\star a)[a:=P]\notin SN_{\beta\pi}$ or $(a\star U^{*})\leq V$ and $(a\star U^{*})\in SN_{\beta\pi}$ and $(a\star U^{*})[a:=P]\notin SN_{\beta\pi}$. Assume the former. By Lemma 21, $(U^{*}\star a)\in\mathcal{S}_{A}(\mathcal{A},\mathcal{B})$. Then $(U^{*}\star a)=S\rho$ for some $S\in\mathcal{A}$ or $(U^{*}\star a)=W\tau$ for some $W\in\mathcal{B}$. Since $a\notin Im(\sigma)$, the latter is impossible. The former case, however, yields $S=(U^{\prime}\star a)$ with $U^{\prime}\rho=U^{*}$ for some $U^{\prime}\in\mathcal{A}$, which proves our assertion.

The next lemma states closure of strong normalizability under substitution.

Lemma 23**.**

If $M,N\in SN_{\beta\pi}$, then $M[x:=N]\in SN_{\beta\pi}$.

Proof 2.7**.**

We are going to prove a bit more general statement. Suppose $M,N_{i}\in SN_{\beta\pi}$ are proper, $type(N_{i})=A$ $(1\leq i\leq k)$. Let $\tau_{i}\in\Sigma_{A^{\bot}}$ are such that $\tau_{i}\in SN_{\beta\pi}$ $(1\leq i\leq k)$ and let $\rho=[x_{1}:=N_{1}\tau_{1},\ldots,x_{k}:=N_{k}\tau_{k}]$. Then we have $M\rho\in SN_{\beta\pi}$. The proof is by induction on $(cxty(A),\eta_{\beta\pi}(M),cxty(M)$, $\Sigma_{i}\;\eta_{\beta\pi}(N_{i}),\Sigma_{i}\;cxty(N_{i}))$ where, in $\Sigma_{i}\;\eta_{\beta\pi}(N_{i})$ and $\Sigma_{i}\;cxty(N_{i})$, we count each occurrence of the substituted variable. For example if $k=1$ and $x_{1}$ has $n$ occurrences, then $\Sigma_{i}\;\eta_{\beta\pi}(N_{i})=n\cdot\eta_{\beta\pi}(N_{1})$.

The only nontrivial case is when $M=(M_{1}\star M_{2})$ and $M\rho\notin SN_{\beta\pi}$. By the induction hypothesis $M_{i}\rho\in SN_{\beta\pi}$ $(i\in\{1,2\})$. We select some of the typical cases.

1. (A)

$M_{1}\rho\rightarrow_{\beta\pi}\lambda zM^{\prime}$* and $M^{\prime}[z:=M_{2}]\notin SN_{\beta\pi}$.*

$M_{1}$* is proper, then there is an $M_{3}$ such that $M_{1}=\lambda zM_{3}$ and $M_{3}\rho\rightarrow_{\beta\pi}M^{\prime}$. In this case $(M_{3}[z:=M_{2}])\rho\notin SN_{\beta\pi}$ and since $\eta_{\beta\pi}(M_{3}[z:=M_{2}])<\eta_{\beta\pi}(M)$, the induction hypothesis gives the result.* 2. 2.

$M_{1}\in Var$. Then $M_{1}=x\in dom(\rho)$, $\rho(x)=N_{j}\tau_{j}\rightarrow_{\beta\pi}\lambda zM^{\prime}$ for some $(1\leq j\leq k)$. Since $N_{j}$ is proper, there is an $N^{\prime}$ such that $N_{j}=\lambda zN^{\prime}$, $N^{\prime}\tau_{j}\rightarrow_{\beta\pi}M^{\prime}$. Then $N^{\prime}\tau_{j}[z:=M_{2}\rho]\notin SN_{\beta\pi}$ and $type(z)={type({N_{j}})}^{\bot}=type(\tau_{j})$, so, by the previous lemma, we have $N^{\prime\prime}\prec N^{\prime}$ and $\tau^{\prime}$ such that $(N^{\prime\prime}\tau^{\prime}\star M_{2}\rho)\notin SN_{\beta\pi}$. Now we have $(N^{\prime\prime}\tau^{\prime}\star M_{2}\rho)=(y\star M_{2}\rho)[y:=N^{\prime\prime}\tau^{\prime}]$, $type(N^{\prime\prime})={type(\tau^{\prime})}^{\bot}=A$ and $\eta_{\beta\pi}cxty(N^{\prime\prime})<\eta c(N_{j})$, which contradicts the induction hypothesis. 2. (B)

$M_{1}\rho\rightarrow_{\beta\pi}\langle M^{\prime},M^{\prime\prime}\rangle$* and either $(M^{\prime}\star M_{2})\notin SN_{\beta\pi}$ or $(M^{\prime\prime}\star M_{2})\notin SN_{\beta\pi}$. Suppose the former.*

$M_{1},M_{2}$* are proper, then there are $M_{3},M_{4}$ such that $M_{1}=\langle M_{3},M_{4}\rangle$ and $M_{3}\rho\rightarrow_{\beta\pi}M^{\prime}$, or $M_{4}\rho\rightarrow_{\beta\pi}M^{\prime\prime}$. Assume the former. Then we have $(M_{3}\star M_{2})\rho\notin SN_{\beta\pi}$ and $\eta_{\beta\pi}((M_{3}\star M_{2}))<\eta_{\beta\pi}(M)$, a contradiction.* 2. 2.

$M_{1}=x\in dom(\rho)$, then $\rho(x)=N_{j}\tau_{j}\rightarrow_{\beta\pi}\langle M^{\prime},M^{\prime\prime}\rangle$, $N_{j}$ is proper and $N_{j}=\langle U,V\rangle$, $U\tau_{j}\rightarrow_{\beta\pi}M^{\prime}$ or $V\tau_{j}\rightarrow_{\beta\pi}M^{\prime\prime}$. Now $(U\tau_{j}\star M_{2})=(y\star M_{2})[y:=U\tau_{j}]\notin SN_{\beta\pi}$, but $cxty(type(U))<cxty(type(N_{j}))$, a contradiction again. 3. 3.

$M_{2}\in Var$. This is similar to the previous case. By the same argument as in part (A)-2.-(a) of the proof of the previous lemma, $M_{1}$ and $M_{2}$ cannot be both variables. This completes the proof of the lemma.

Theorem 24**.**

The $\lambda_{\beta\pi}$-calculus is strongly normalizing.

Proof 2.8**.**

It is enough to show that, for every term, $M$, $N\in SN_{\beta\pi}$ implies $(M\star N)\in SN_{\beta\pi}$. Supposing $M,N\in SN_{\beta\pi}$, Lemma 19 gives $(M\star x)\in SN_{\beta\pi}$, which yields, by the previous lemma, $(M\star N)=(M\star x)[x:=N]\in SN_{\beta\pi}$.

3. The $\overline{\lambda}\mu\tilde{\mu}$- and the $\lmts$-calculus

In this section, we introduce the $\overline{\lambda}\mu\tilde{\mu}$-calculus together with one of its extensions, the $\lmts$-calculus, by which we establish a translation of the $\ls$-calculus and thus obtain the strong normalization of the $\lmts$-calculus as a consequence.

3.1. The $\overline{\lambda}\mu\tilde{\mu}$-calculus

The $\overline{\lambda}\mu\tilde{\mu}$-calculus was introduced by Curien and Herbelin ([Her95] and [CH00]). We examine here the calculus defined by Curien et al. [CH00], which is a simply typed one. The $\overline{\lambda}\mu\tilde{\mu}$-calculus was invented for representing proofs in classical Gentzen-style sequent calculus: under the Curry-Howard correspondence a version of Gentzen-style sequent calculus is obtained as a system of simple types for the $\overline{\lambda}\mu\tilde{\mu}$-calculus. Moreover, the system presents a clear duality between call-by-value and call-by-name evaluations.

{defi}

There are three kinds of terms, defined by the following grammar, and there are two kinds of variables. We assume that we use the same set of variables in the $\lmts$-calculus, too. In the literature, different authors use different terminology. Here, we will call them either $c$-terms, or $l$-terms or $r$-terms. Similarly, the variables will be called either $l$-variables (and denoted as $x,y,...$) or $r$-variables (and denoted as $a,b,...$).

[TABLE]

As usual, we denote by $Fv(u)$, the set of the free variables of the term $u$.

{defi}

The types are built from atomic formulas (or, in other words, atomic types) with the connector $\rightarrow$. We assume that the same set of type variables ${\mathcal{A}}$ is used in the $\lmts$-calculus, also. The typing system is a sequent calculus based on judgements of the following form.

$p:(\Gamma\;\rhd\;\triangle)$           $\Gamma\;\rhd\;t:A\;|\;\triangle$           $\Gamma\;|\;e:A\;\rhd\;\triangle$

where $\Gamma$ (resp. $\triangle$) is a set of declarations of the form $x:A$ (resp. $a:A$), $x$ (resp. $a$) denoting a $l$-variable (resp. an $r$-variable) and $A$ representing a type, such that $x$ (resp. $a$) occurs at most once in an expression of $\Gamma$ (resp. $\triangle$) of the form $x:A$ (resp. $a:A$). We say that $\Gamma$ an $l$-context and $\triangle$ is an $r$-context, respectively. The typing rules are as follows

[TABLE]

[TABLE]

[TABLE]

{defi}

The cut-elimination procedure (on the logical side) corresponds to the reduction rules (on the terms) given below.

[TABLE]

Let us take the union of the above rules. Let $\hookrightarrow$ stand for the compatible closure of this union and, as usual, $\hookrightarrow^{*}$ denote the reflexive, symmetric and transitive closure of $\hookrightarrow$. The notions of reduction sequence, normal form and normalization are defined with respect to $\hookrightarrow$.

We present below some theoretical properties of the $\overline{\lambda}\mu\tilde{\mu}$-calculus (Herbelin [Her95], Curien and Herbelin [CH00], de Groote [Gro01], Polonovski [Pol04] and David and Nour [DN07]).

Proposition 25** (Type-preservation property).**

If $\Gamma\;\rhd\;t:A\;|\;\triangle$ (resp. $\Gamma\;|\;e:A\;\rhd\;\triangle$, resp. $p:(\Gamma\;\rhd\;\triangle)$) and $t\hookrightarrow^{*}t^{\prime}$ (resp. $e\hookrightarrow^{*}e^{\prime}$, resp. $p\hookrightarrow^{*}p^{\prime}$), then $\Gamma\;\rhd\;t^{\prime}:A\;|\;\triangle$ (resp. $\Gamma\;|\;e^{\prime}:A\;\rhd\;\triangle$, resp. $p^{\prime}:(\Gamma\;\rhd\;\triangle)$).

Proposition 26** (Subformula property).**

If $\Pi$ is a derivation of $\Gamma\;\rhd\;t:A\;|\;\triangle$ (resp. $\Gamma\;|\;e:A\;\rhd\;\triangle$, resp. $p:(\Gamma\;\vdash\;\triangle)$) and $t$ (resp. $e$, resp. $p$) is in normal form, then every type occurring in $\Pi$ is a subformula of a type occurring in $\Gamma\cup\triangle$, or a subformula of $A$ (only for $t$ and $e$).

Theorem 27** (Strong normalization property).**

If $\Gamma\;\rhd\;t:A\;|\;\triangle$ (resp. $\Gamma\;|\;e:A\;\rhd\;\triangle$, resp. $p:(\Gamma\;\rhd\;\triangle)$), then $t$ (resp. $e$, resp. $p$) is strongly normalizable, i.e. every reduction sequence starting from $t$ (resp. $e$, resp. $p$) is finite.

The proof of Theorem 27 can be found in the thesis of Polonovski [Pol04], as well as in the work of David and Nour [DN07], where an arithmetical proof is presented.

3.2. The $\lmts$-calculus

Since we work in a sequent calculus, where negation is implicitly built in the rules, the typing rules of the $\overline{\lambda}\mu\tilde{\mu}$-calculus do not handle negation. However, for a full treatment of propositional logic we found it more convenient to introduce rules concerning negation. Since $c$-terms, which could have been candidates for objects of type $\bot$, are distinctly separated from terms, adding new term- and type-forming operators seems to be the easiest way to define negation.

{defi}

1. (1)

The terms of the $\lmts$-calculus are defined by the following grammar.

[TABLE]

As an abuse of terminology, in the sequel when speaking about the syntactic elements of the $\lmts$-calculus, we may not distinguish $l$-, $r$- and $c$-terms, we may speak about terms in general. We denote by $\mathfrak{T}$ the set of terms of the $\lmts$-calculus. 2. (2)

The complexity of a term of $\mathfrak{T}$ is defined as follows.

• $cxty(x)=cxty(\alpha)=0$,
• $cxty(\lambda xt)=cxty(\widetilde{t})=cxty(t)+1$,
• $cxty(\overline{e})=cxty(e)+1$,
• $cxty(\mu\alpha p)=cxty(\tilde{\mu}x\,p)=cxty(p)+1$,
• $cxty(\lfloor t,e\rfloor)=cxty((t.e))=cxty(t)+cxty(e)$.

{defi}

The type inference rules are the same as in the $\overline{\lambda}\mu\tilde{\mu}$-calculus with two extra rules added for the types of the complemented terms. Moreover, we introduce an equation between types (for all types $A$, $(A^{\bot})^{\bot}=A$) to ensure that our negation is involutive.

[TABLE]

We also define the complexity of types in the $\lmts$-calculus.

1. $cxty(A)=0$ for atomic types,
2. $cxty(A\rightarrow B)=cxty(A)+cxty(B)+1$,
3. $cxty(A^{\bot})=cxty(A)$.

That is, the complexity of a type $A$ provides us with the number of arrows in $A$. The presence of negation makes it necessary for us to introduce new rules handling negation.

{defi}

Besides the reduction rules already present in $\overline{\lambda}\mu\tilde{\mu}$, we endow the calculus with some more new rules to handle the larger set of terms. In what follows $cl$ stands for the name: complementer rule. We shall refer to the $cl_{1,l}$- and $cl_{1,r}$-rules by a common notation as the $cl_{1}$-rules.

[TABLE]

In the sequel, we continue to apply the notation $\hookrightarrow$ and $\hookrightarrow^{*}$ in relation with this new calculus.

Obviously, the statements analogous to Propositions 25 and 26 are still valid.

4. Relating the $\ls$-calculus to the $\lmts$-calculus

Rocheteau [Roc05] defined a translation between the $\overline{\lambda}\mu\tilde{\mu}$-calculus and the $\lambda\mu$-calculus, treating both a call-by-value and a call-by-name aspect of $\overline{\lambda}\mu\tilde{\mu}$. In this subsection, we give a translation (in both directions) between the $\ls$-calculus and the $\lmts$-calculus, which is a version of the $\overline{\lambda}\mu\tilde{\mu}$-calculus extended with negation. The translations are such that strong normalization of one calculus follows from that of the other in both directions. We omit issues of evaluation strategies, however. In the end of the section we give an exact description of the correspondence between the two translations. Preparatory to presenting the translations, let us introduce some definitions and notation below. We assume that the two calculi have the same sets of variables and atomic types. Moreover, as an abuse of notation, if $\overline{{\alpha}}:A^{\bot}$ stems from the $r$-variable $\alpha:A$ in the $\lmts$-calculus, then we suppose that in the $\ls$-calculus $\overline{{\alpha}}$ denotes a variable with type $A^{\bot}$.

4.1. A translation of the

$\lmts$-calculus into the $\ls$-calculus

{defi}

1. (1)

Let us consider the $\ls$-calculus. For $i\in\{1,2\}$, we write ${\pi}_{i}(y)=\lambda z(y\star{\sigma}_{i}(z))$. Then, we can observe that $y:A_{1}\wedge A_{2}\vdash{\pi}_{i}(y):A_{i}$, for $i\in\{1,2\}$. 2. (2)

We define a translation $.^{\mathfrak{e}}:\mathfrak{T}\longrightarrow\mathcal{T}$ as follows.

[TABLE]

[TABLE]

[TABLE] 3. (3)

The translation $.^{\mathfrak{e}}$ also applies to types.

• •

$A^{\mathfrak{e}}=A$, where $A$ is an atomic type,

• •

$(A^{\bot})^{\mathfrak{e}}=(A^{\mathfrak{e}})^{\bot}$,

• •

$(A\rightarrow B)^{\mathfrak{e}}=(A^{\mathfrak{e}})^{\bot}\vee B^{\mathfrak{e}}$. 4. (4)

Let $\Gamma$, $\triangle$ be $l$- and $r$-contexts, respectively. Then $\Gamma^{\mathfrak{e}}=\{x:A^{\mathfrak{e}}\;|\;x:A\in\Gamma\}$ and similarly for $\triangle$. Furthermore, for any $r$-context $\triangle$, let $\triangle^{\bot}=\{\overline{\alpha}:A^{\bot}\;|\;\alpha:A\in\triangle\}$.

Lemma 28**.**

1. (1)

If $\Gamma\;{\rhd}\;t:A\;|\;\triangle$, then $\Gamma^{\mathfrak{e}},(\triangle^{\mathfrak{e}})^{\bot}\;{\vdash}\;t^{\mathfrak{e}}:A^{\mathfrak{e}}$. 2. (2)

If $\Gamma\;|\;e:A\;{\rhd}\;\triangle$, then $\Gamma^{\mathfrak{e}},(\triangle^{\mathfrak{e}})^{\bot}\;{\vdash}\;e^{\mathfrak{e}}:(A^{\mathfrak{e}})^{\bot}$. 3. (3)

If $p:(\Gamma\;{\rhd}\;\triangle)$, then $\Gamma^{\mathfrak{e}},(\triangle^{\mathfrak{e}})^{\bot}\;{\vdash}\;p^{\mathfrak{e}}:\bot$.

Proof 4.1**.**

The above statements are proved simultaneously according to the length of the $\lmts$-deduction. We remark that $.^{\mathfrak{e}}$ is defined in Definition 4.1 exactly in the way to make the assertions of the lemma true. Let us examine some of the more interesting cases.

1. (1)

Suppose

[TABLE]

Then we have, by the induction hypothesis and Notation 4.1,

[TABLE]

[TABLE]

[TABLE]

Thus we can conclude

[TABLE]

[TABLE]

From which, we obtain

[TABLE] 2. (2)

Assume now

[TABLE]

Then we have

[TABLE] 3. (3)

From

[TABLE]

we obtain

[TABLE]

Our next aim is to prove that $\lmts$ can be simulated by the $\ls$-calculus. To this end we introduce a new notion of equality in the $\ls$-calculus.

{defi}

We define an equivalence relation $\sim$ on $\mathcal{T}$, which is the smallest relation compatible with the term forming rules and containing $((M\star N),(N\star M))$.

• •

$x\sim x$,

• •

if $M\sim M^{\prime}$, then $\lambda xM\sim\lambda xM^{\prime}$ and $\sigma_{i}(M)\sim\sigma_{i}(M^{\prime})$ for $i\in\{1,2\}$,

• •

if $M\sim M^{\prime}$ and $N\sim N^{\prime}$, then $\langle M,N\rangle\sim\langle M^{\prime},N^{\prime}\rangle$ and $(M\star N)\sim(M^{\prime}\star N^{\prime})$ and $(M\star N)\sim(N^{\prime}\star M^{\prime})$.

We say that $M$ and $N$ are equal up to symmetry provided $M\sim N$.

Lemma 29**.**

Let $M,M^{\prime},N,N^{\prime}\in\mathcal{T}$.

1. (1)

If $M\sim M^{\prime}$ and $N\sim N^{\prime}$, then $M[x:=N]\sim M^{\prime}[x:=N^{\prime}]$. 2. (2)

If $M\sim M^{\prime}$ and $M^{\prime}\rightarrow N$, then there is $N^{\prime}$ for which $M\rightarrow N^{\prime}$ and $N\sim N^{\prime}$.

Proof 4.2**.**

1. By induction on $cxty(M)$. 2. By 1.

Lemma 30**.**

Let $u,t,e\in\mathfrak{T}$. Then $(u[x:=t])^{\mathfrak{e}}=u^{\mathfrak{e}}[x:=t^{\mathfrak{e}}]$ and $(u[a:=e])^{\mathfrak{e}}=u^{\mathfrak{e}}[a:=e^{\mathfrak{e}}]$.

Proof 4.3**.**

By induction on $cxty(u)$.

Now we can formulate our assertion about the simulation of the $\lmts$-calculus by the $\ls$-calculus.

Theorem 31**.**

Let $v,w\in\mathfrak{T}$.

1. (1)

If $v\hookrightarrow_{r}w$ and $r\in\{\beta\,,\,\mu\,,\,{\tilde{\mu}}\,,\,{s_{l}}\,,\,{s_{r}}\}$, then $\;v^{\mathfrak{e}}\rightarrow^{+}w^{\mathfrak{e}}$. 2. (2)

If $v\hookrightarrow_{r}w$ and $r\in\{{cl_{1,l}}\,,\,{cl_{1,r}}\,,\,{cl_{2}}\}$, then $v^{\mathfrak{e}}\sim w^{\mathfrak{e}}$.

Proof 4.4**.**

1. (1)

Let us only treat the typical cases.

1. (a)

If $v=\lfloor\lambda xu,(t.e)\rfloor\hookrightarrow_{\beta}\lfloor t,\tilde{\mu}x\lfloor u,e\rfloor\rfloor=w$, then $v^{\mathfrak{e}}=(\langle t^{\mathfrak{e}},e^{\mathfrak{e}}\rangle\star\lambda y(\lambda x({\pi}_{2}(y)\star u^{\mathfrak{e}})\star{\pi}_{1}(y)))\rightarrow_{\beta^{\bot}}{}(\lambda x({\pi}_{2}(\langle t^{\mathfrak{e}},e^{\mathfrak{e}}\rangle)\star u^{\mathfrak{e}})\star{\pi}_{1}(\langle t^{\mathfrak{e}},e^{\mathfrak{e}}\rangle))\rightarrow^{*}{}(\lambda x(e^{\mathfrak{e}}\star u^{\mathfrak{e}})\star t^{\mathfrak{e}})=w^{\mathfrak{e}}$. 2. (b)

If $v=\lfloor\mu ap,e\rfloor\hookrightarrow_{\mu}p[a:=e]=w$, then, by Lemma 30, $v^{\mathfrak{e}}=(e^{\mathfrak{e}}\star\lambda ap^{\mathfrak{e}})\rightarrow_{\beta^{\bot}}p^{\mathfrak{e}}[a=e^{\mathfrak{e}}]=w^{\mathfrak{e}}$. 3. (c)

If $v=\mu a\lfloor w,a\rfloor\hookrightarrow_{s_{l}}w$, $a\notin w$, then $v^{\mathfrak{e}}=\lambda a(a\star w^{\mathfrak{e}})\rightarrow_{\eta^{\bot}}w^{\mathfrak{e}}$. 2. (2)

1. (a)

If $v=\overline{\widetilde{u}}\hookrightarrow_{cl_{1,l}}u=w$, then $v^{\mathfrak{e}}=(\overline{\widetilde{u}})^{\mathfrak{e}}=u^{\mathfrak{e}}=w^{\mathfrak{e}}$. 2. (b)

If $v=\lfloor\overline{v},\widetilde{u}\rfloor\hookrightarrow_{cl_{2}}\lfloor u,v\rfloor=w$, then $v^{\mathfrak{e}}=\lfloor\overline{v},\widetilde{u}\rfloor^{\mathfrak{e}}=(u^{\mathfrak{e}}\star v^{\mathfrak{e}})\sim w^{\mathfrak{e}}$.

Corollary 32**.**

The $\lmts$-calculus is strongly normalizable.

Proof 4.5**.**

Let $\sigma$ be a reduction sequence in the $\lmts$-calculus, assume $\sigma$ is $v_{0}\hookrightarrow v_{1}\ldots\hookrightarrow v_{n}$ and $\sigma$ contains $k\geq 0$ number of $\beta$-, $\mu$-, $\tilde{\mu}$-, $s_{l}$- or $s_{r}$-reductions. By Theorem 31, $v_{0}^{\mathfrak{e}}$, $v_{1}^{\mathfrak{e}},\ldots$, $v_{n}^{\mathfrak{e}}$ forms a sequence of $\ls$-terms, where either $v_{i}^{\mathfrak{e}}\rightarrow v_{i+1}^{\mathfrak{e}}$ or $v_{i}^{\mathfrak{e}}\sim v_{i+1}^{\mathfrak{e}}$ $(0\leq i\leq n-1)$ and, for every $\beta$-, $\mu$-, $\tilde{\mu}$-, $s_{l}$- or $s_{r}$-reduction, there corresponds a reduction step in the $\ls$-calculus. By Lemma 29, we obtain that $\sim$ can be postponed, that is, there are $w_{0}$, $w_{1},\ldots$, $w_{k+1}$ in $\mathcal{T}$ such that $w_{0}=v_{0}^{\mathfrak{e}}$, $w_{k+1}=v_{n}^{\mathfrak{e}}$ and $w_{0}\rightarrow\ldots\rightarrow w_{k}\sim w_{k+1}$. This means that we can establish a reduction sequence of length $k$ starting from $v_{0}^{\mathfrak{e}}$ in the $\ls$-calculus. Hence, by Theorem 24 and Corollary 16, an infinite reduction sequence starting from $v_{0}$ can contain only a finite number of $\beta$-, $\mu$-, $\tilde{\mu}$-, $s_{l}$- or $s_{r}$-reductions. Thus there would exist an infinite reduction sequence in the $\lmts$-calculus consisting entirely of $cl_{1,l}$-, $cl_{1,r}$- and $cl_{2}$-reductions, which is impossible.

4.2. A translation of the $\ls$-calculus into the $\lmts$-calculus

Now we are going to deal with the converse relation. That is we will present a translation of the $\ls$-calculus into the $\lmts$-calculus which faithfully reflects the typability relations of one calculus in the other one. Then we prove that our translation is in fact a simulation of the $\ls$-calculus in the $\lmts$-calculus.

{defi}

1. (1)

The translation $.^{\mathfrak{f}}:\mathcal{T}\longrightarrow\mathfrak{T}$ is defined as follows.

[TABLE] 2. (2)

The translation $.^{\mathfrak{f}}$ applies to the types as follows.

• •

${\alpha}^{\mathfrak{f}}=\alpha$,

• •

${({\alpha}^{\bot})}^{\mathfrak{f}}={\alpha}^{\bot}$,

• •

$(A\wedge B)^{\mathfrak{f}}=(A^{\mathfrak{f}}\rightarrow(B^{\mathfrak{f}})^{\bot})^{\bot}$,

• •

$(A\vee B)^{\mathfrak{f}}=(A^{\mathfrak{f}})^{\bot}\rightarrow B^{\mathfrak{f}}$.

We remark that $.^{\mathfrak{f}}$ maps the terms of the $\ls$-calculus with type $\bot$ to $c$-terms of the $\lmts$-calculus, which have no types. We also have, for all types $A$, ${(A^{\bot})}^{\mathfrak{f}}=(A^{\mathfrak{f}})^{\bot}$. Therefore the translation $.^{\mathfrak{f}}$ maps equal types to equal types.

Lemma 33**.**

1. (1)

If $\Gamma\;{\vdash}\;M:A$ and $A\neq\bot$, then $\Gamma^{\mathfrak{f}}\;{\rhd}\;M^{\mathfrak{f}}:A^{\mathfrak{f}}$. 2. (2)

If $\Gamma\;{\vdash}\;M:\bot$, then $M^{\mathfrak{f}}:(\Gamma^{\mathfrak{f}}\;{\rhd}\;)$.

Proof 4.6**.**

The proof proceeds by a simultaneous induction on the length of the derivation in the $\ls$-calculus. We can observe again that the notion of $.^{\mathfrak{f}}$ in Definition 4.2 is conceived in a way to make the statements of the lemma true. Let us only examine some of the typical cases of the first assertion.

1. (1)

Suppose

[TABLE]

Then, applying the induction hypothesis,

[TABLE] 2. (2)

If

[TABLE]

then, we obtain

[TABLE] 3. (3)

From

[TABLE]

we obtain

[TABLE]

Now we turn to the proof of the simulation of the $\ls$-calculus in the $\lmts$-calculus.

Lemma 34**.**

Let $M,N\in\mathcal{T}$. Then ${(M[x:=N])}^{\mathfrak{f}}=M^{\mathfrak{f}}[x:=N^{\mathfrak{f}}]$.

Proof 4.7**.**

By induction on $cxty(M)$.

Theorem 35**.**

Let $M,N\in\mathcal{T}$. If $M\rightarrow N$, then $M^{\mathfrak{f}}\hookrightarrow^{+}N^{\mathfrak{f}}$.

Proof 4.8**.**

Let us prove some of the more interesting cases.

1. (1)

If $M=(\lambda xP\star Q)\rightarrow_{\beta}P[x:=Q]=N$, then, applying Lemma 34,

$M^{\mathfrak{f}}=\lfloor Q^{\mathfrak{f}},\widetilde{\overline{\tilde{\mu}xP^{\mathfrak{f}}}}\rfloor\hookrightarrow_{cl_{1}}{}\lfloor Q^{\mathfrak{f}},\tilde{\mu}xP^{\mathfrak{f}}\rfloor\hookrightarrow_{\tilde{\mu}}{}P^{\mathfrak{f}}[x:=Q^{\mathfrak{f}}]=N^{\mathfrak{f}}$. 2. (2)

If $M=(Q\star\lambda xP)\rightarrow_{\beta_{\bot}}P[x:=Q]=N$, then

$M^{\mathfrak{f}}=\lfloor\overline{\tilde{\mu}xP^{\mathfrak{f}}},\widetilde{Q^{\mathfrak{f}}}\rfloor\hookrightarrow_{cl_{2}}{}\lfloor Q^{\mathfrak{f}},\tilde{\mu}xP^{\mathfrak{f}}\rfloor\hookrightarrow_{\tilde{\mu}}{}P^{\mathfrak{f}}[x:=Q^{\mathfrak{f}}]=N^{\mathfrak{f}}$. 3. (3)

If $M=(\langle P,Q\rangle\star\sigma_{1}(R))\rightarrow_{\pi}(P\star R)=N$, then

$M^{\mathfrak{f}}=\lfloor\lambda x\mu b\lfloor R^{\mathfrak{f}},\widetilde{x}\rfloor,\widetilde{\overline{(P^{\mathfrak{f}}.\widetilde{Q^{\mathfrak{f}}})}}\rfloor\hookrightarrow_{cl_{1}}{}\lfloor\lambda x\mu b\lfloor R^{\mathfrak{f}},\widetilde{x}\rfloor,(P^{\mathfrak{f}}.\widetilde{Q^{\mathfrak{f}}},)\rfloor\hookrightarrow_{\lambda}$**

$\lfloor P^{\mathfrak{f}},\tilde{\mu}x\lfloor\mu b\lfloor R^{\mathfrak{f}},\widetilde{x}\rfloor,\widetilde{Q^{\mathfrak{f}}}\rfloor\rfloor\hookrightarrow_{\tilde{\mu}}{}\lfloor\mu b\lfloor R^{\mathfrak{f}},\widetilde{P^{\mathfrak{f}}}\rfloor,\widetilde{Q^{\mathfrak{f}}}\rfloor\hookrightarrow_{\mu}{}\lfloor R^{\mathfrak{f}},\widetilde{P^{\mathfrak{f}}}\rfloor=N^{\mathfrak{f}}$.

We could have as well demonstrated that the $\lmts$-calculus is strongly normalizable by applying the method presented in Section 3 as accomplished by Battyányi [Bat07]. The following result states that in this case the strong normalizability of the $\ls$-calculus would arise as a direct consequence of that of the $\lmts$-calculus.

Corollary 36**.**

If the $\lmts$-calculus is strongly normalizable, then the same is true for the $\ls$-calculus as well.

Proof 4.9**.**

By Theorem 35.

4.3. The connection between the two translations

In this subsection we examine the connection between the two transformations. We prove that both compositions $.^{\mathfrak{e}^{\mathfrak{f}}}:\mathfrak{T}\longrightarrow\mathfrak{T}$ and $.^{\mathfrak{f}^{\mathfrak{e}}}:\mathcal{T}\longrightarrow\mathcal{T}$ are such that we can get back the original terms by performing some steps of reduction on $u^{\mathfrak{e}^{\mathfrak{f}}}$ or on $M^{\mathfrak{f}^{\mathfrak{e}}}$, respectively. That is, the following theorems are valid. The case of $.^{\mathfrak{f}^{\mathfrak{e}}}$ is the easier one.

First we describe the effect of $.^{\mathfrak{f}^{\mathfrak{e}}}$ on the typing relations.

Lemma 37**.**

If $\Gamma\;{\vdash}\;M:A$, then $\Gamma\;{\vdash}\;{M^{\mathfrak{f}}}^{\mathfrak{e}}:A$.

Proof 4.10**.**

Combining Lemmas 33 and 28.

Theorem 38**.**

Let $M\in\mathcal{T}$. Then ${M^{\mathfrak{f}}}^{\mathfrak{e}}\rightarrow^{*}M$.

Proof 4.11**.**

By induction on $cxty(M)$. We consider only the more interesting cases.

1. (1)

If $M=(P\star Q)$, then ${(P\star Q)^{\mathfrak{f}}}^{\mathfrak{e}}=\lfloor Q^{\mathfrak{f}},\widetilde{P^{\mathfrak{f}}}\rfloor^{\mathfrak{e}}=({P^{\mathfrak{f}}}^{\mathfrak{e}}\star{Q^{\mathfrak{f}}}^{\mathfrak{e}})\rightarrow^{*}(P\star Q)$. 2. (2)

If $M=\langle P,Q\rangle$, then ${\langle P,Q\rangle^{\mathfrak{f}}}^{\mathfrak{e}}=\overline{({P^{\mathfrak{f}}.\widetilde{Q^{\mathfrak{f}}}})}^{\mathfrak{e}}=\langle{P^{\mathfrak{f}}}^{\mathfrak{e}},{Q^{\mathfrak{f}}}^{\mathfrak{e}}\rangle\rightarrow^{*}\langle P,Q\rangle$. 3. (3)

If $M=\sigma_{1}(N)$, then

${\sigma_{1}(N)^{\mathfrak{f}}}^{\mathfrak{e}}={\lambda x\mu\beta\lfloor N^{\mathfrak{f}},\widetilde{x}\rfloor}^{\mathfrak{e}}=\lambda y(\lambda x({\pi}_{2}(y)\star{(\mu\beta\lfloor N^{\mathfrak{f}},\widetilde{x}\rfloor)}^{\mathfrak{e}})\star{\pi}_{1}(y))=\\ \lambda y(\lambda x({\pi}_{2}(y)\star\lambda\overline{\beta}(x\star{N^{\mathfrak{f}}}^{\mathfrak{e}}))\star{\pi}_{1}(y))\rightarrow_{\beta^{\bot}}\lambda y(\lambda x(x\star{N^{\mathfrak{f}}}^{\mathfrak{e}})\star{\pi}_{1}(y))\rightarrow_{\eta^{\bot}}\\ \lambda y({N^{\mathfrak{f}}}^{\mathfrak{e}}\star{\pi}_{1}(y))\rightarrow_{\beta}\lambda y(y\star\sigma_{1}({N^{\mathfrak{f}}}^{\mathfrak{e}}))\rightarrow_{\eta^{\bot}}\sigma_{1}({N^{\mathfrak{f}}}^{\mathfrak{e}})\rightarrow^{*}\sigma_{1}(N)$.

We begin to examine the composition ${.^{\mathfrak{e}}}^{\mathfrak{f}}:\mathfrak{T}\rightarrow\mathfrak{T}$ for an arbitrary $u$. First we make the following observation.

Lemma 39**.**

1. (1)

If $\Gamma\;{\rhd}\;t:A\;|\;\triangle$, then $\Gamma,\triangle^{\bot}\;{\rhd}\;{t^{\mathfrak{e}}}^{\mathfrak{f}}:A$. 2. (2)

If $\Gamma\;|\;e:A\;{\rhd}\;\triangle$, then $\Gamma,\triangle^{\bot}\;{\rhd}\;{e^{\mathfrak{e}}}^{\mathfrak{f}}:A^{\bot}$. 3. (3)

If $p:(\Gamma\;{\rhd}\;\triangle)$, then ${p^{\mathfrak{e}}}^{\mathfrak{f}}:(\Gamma,\triangle^{\bot}\;{\rhd})$.

Proof 4.12**.**

Combining Lemmas 28 and 33.

Theorem 38 states that, if $M$ is an $\ls$-term, then $M$ can be related to ${M^{\mathfrak{f}}}^{\mathfrak{e}}$ by the reductions in the $\ls$-calculus. We note that we are not able to obtain $u$ from ${{u^{\mathfrak{e}}}}^{\mathfrak{f}}$ in such a way. We can find a term $T$ instead such that ${{u^{\mathfrak{e}}}}^{\mathfrak{f}}\hookrightarrow^{*}T(u)$. The function $T$ can intuitively be considered as the description how $\ls$-connectives can be embedded into the $\lmts$-calculus. It turns out that the $\lmts$-calculus translates the ${\ls}$-terms not so smoothly as it was the case with the other direction.

{defi}

We define a function $T$ assigning a $\lmts$-term to a $\lmts$-term.

•

$T(x)=x$,

•

$T(\lambda xu)=\overline{\tilde{\mu}y\lfloor T(u)[x:=p_{1}(y)],\widetilde{p_{2}(y)}\rfloor}$,

•

$T(\mu\alpha p)=\overline{\tilde{\mu}\overline{\alpha}T(p)}$,

•

$T(\overline{u})=T(u)$,

•

$T(\alpha)=\overline{\alpha}$,

•

$T((u.v))=\langle T(u),T(v)\rangle$,

•

$T(\tilde{\mu}xp)=\overline{\tilde{\mu}xT(p)}$,

•

$T(\widetilde{h})=T(h)$,

•

$T(\lfloor t,e\rfloor)=\lfloor T(t),\widetilde{T(e)}\rfloor$.

Theorem 40**.**

Let $u\in\mathfrak{T}$. We have ${u^{\mathfrak{e}}}^{\mathfrak{f}}\hookrightarrow^{*}T(u)$.

Proof 4.13**.**

By induction on $cxty(u)$. We consider only some of the cases.

1. (1)

If $u=\lambda xv$, then

${u^{\mathfrak{e}}}^{\mathfrak{f}}=(\lambda y(\lambda x({\pi}_{2}(y)\star u^{\mathfrak{e}})\star{\pi}_{1}(y)))^{\mathfrak{f}}=\overline{\tilde{\mu}y\lfloor p_{1}(y),\widetilde{\overline{\tilde{\mu}x\lfloor{v^{\mathfrak{e}}}^{\mathfrak{f}},\widetilde{p_{2}(y)}\rfloor}}\rfloor}\hookrightarrow_{cl_{1,r}}$* *

$\overline{\tilde{\mu}y\lfloor p_{1}(y),\tilde{\mu}x\lfloor{v^{\mathfrak{e}}}^{\mathfrak{f}},\widetilde{p_{2}(y)}\rfloor\rfloor}\hookrightarrow_{\tilde{\mu}}\overline{\tilde{\mu}y\lfloor{v^{\mathfrak{e}}}^{\mathfrak{f}}[x:=p_{1}(y)],\widetilde{p_{2}(y)}[x:=p_{1}(y)]\rfloor}\hookrightarrow^{*}T(u)$. 2. (2)

If $u=\tilde{\mu}x\lfloor t,v\rfloor$, then

${u^{\mathfrak{e}}}^{\mathfrak{f}}=(\lambda x(v^{\mathfrak{e}}\star t^{\mathfrak{e}}))^{\mathfrak{f}}=\overline{\tilde{\mu}x\lfloor{t^{\mathfrak{e}}}^{\mathfrak{f}},\widetilde{{v^{\mathfrak{e}}}^{\mathfrak{f}}}\rfloor}\hookrightarrow^{*}\overline{\tilde{\mu}x\lfloor T(t),\widetilde{T(v)}\rfloor}=\overline{\tilde{\mu}xT(\lfloor t,v\rfloor)}=T(u)$.

Remark 41**.**

We remark that we cannot expect $T(u)$ to be expressible with the help of $\mathfrak{T}$. Namely, we can show that, if $=_{\tiny{\lmts}}$ denotes the reflexive, transitive closure of the compatible union of the reduction relations in the $\lmts$-calculus, then none of the assertions below are valid.

1. (1)

There exists a a $\lmts$-term $\Phi$ such that, for every $c$-term $c$, $T(c)=_{\tiny{\lmts}}\Phi(c)$. 2. (2)

There exists a a $\lmts$-term $\Phi_{1}$ such that, for every $l$-term $t$, $T(t)=_{\tiny{\lmts}}\Phi_{1}(t)$. 3. (3)

There exists a a $\lmts$-term $\Phi_{2}$ such that, for every $r$-term $e$, $T(e)=_{\tiny{\lmts}}\Phi_{2}(e)$.

5. Conclusion

The paper is mainly devoted to an arithmetical proof of the strong normalization of the $\ls$-calculus introduced by Berardi and Barbanera [BB96]. The proof is an adaptation of the work of David and Nour [DN05]. The novelty of our paper is the application of the method of zoom-in sequences of redexes: we achieve the main theorem by identifying the minimal non-strongly normalizing redexes of an infinite reduction sequence, which we call a zoom-in sequence of redexes. The idea of zoom-in sequences was inspired by the notion of perpetual reduction strategies introduced by Raamsdonk et al. [RSSX99]. Following the proof of the strong normalization of the $\ls$-calculus, the $\overline{\lambda}\mu\tilde{\mu}$-calculus is introduced, which was defined by Curien and Herbelin [CH00]. The same proof of strong normalization as we have presented for the $\ls$-calculus would also work for the calculus of Curien and Herbelin as was shown by Battyányi [Bat07]. However, instead of adapting the proof method for the $\overline{\lambda}\mu\tilde{\mu}$-calculus, we designed a translation of the $\ls$-calculus in the $\lmts$-calculus and vice versa, where the $\lmts$-calculus is the $\overline{\lambda}\mu\tilde{\mu}$-calculus augmented with terms explicitly expressing negation and with rules handling them. The translation allows us to assert strong normalization for the $\lmts$- and, hence, for the $\overline{\lambda}\mu\tilde{\mu}$-calculus.

On the technical side, we remark that there were two main difficulties that rendered the proof a little more involved. First, we had to work with an alternating substitution defined inductively starting from two sets of terms. The reason was that we had to prove a more general statement to locate the supposedly non strongly normalizing part of a term emerging as a result of a substitution. Simple substitutions would not have been enough for our purpose. The second difficulty was that in order to establish a key property of zoom-in sequences in Lemma 21 we had to move forward the Hypothesis “H” from the main theorem, thus making the application of the hypothesis implicit in the sequel. We think that the elimination of both problems would considerably enhance the paper’s intelligibility.

It seems promising to investigate whether the present method of verifying strong normalization can be applied to systems other than simple typed logical calculi, for example, proof nets (Laurent [Lau13]). Another fields of interest could be intuitionistic and classical typed systems with explicit substitutions (Rose [Ros96]). To handle these systems, the present proof must be simplified, we have to pay attention in our proof, for example, that the substitutions are defined by two sets of terms of different types. Finally, we remark that it is a natural requirement of a proof formalizable in first order arithmetic to enable us to find an upper bound for the lengths of the reduction sequences. At its present form, our proof does not make it possible, this raises another demand for the simplification of the results.

Acknowledgment

We wish to thank René David and the anonymous referees for helpful discussions and remarks.