数理解析研究所講究録 1217 巻 2001 年 158-164

158
Strong Normalization of Second
Order Symmetric Lambda-mu Calculus
Yoriyuki Yamagata

山形頼之

Department of Mathematical Science, University of Tokyo
yoriyuki@ms.u-tokyo.ac.jP

東京大学数理科学研究科

Abstract. Parigot suggested symmetric structural reduction rules forapplication to -abstraction in [7] to ensure unique representation of-calculus
data type. We prove strong normalization of second orderwith these rules.
$\mu$$\mathrm{A}/\mathrm{i}$1Introduction
Originally, -calculus was defined to clarify correspondence between classicallogic and control operators in functional programming languages. In this respect, -calculus seems quite successful [3] [4] [5] [10]. In addition, Parigot wasalso motivated in [6] by possibility of witness extraction from classical proofsof -sentences. Unfortunately, reduction rules of -calculus seems not sufficient for this purpose. For example, let $A(x)$ be an atomic formula of arithmeticasand $A’(x)$ be its code in second order predicate logic. We represent$X$
is avariable over$\forall X.\forall x(A(x)arrow X)arrow X$ in second order language, where
somehowofdeduction
normalpropositions. We expect that aclosed
contains aunique first order term such that $A(t)$ holds. However, consider thefollowing situation. Suppose that $A(t)$ holds but $A(u)$ does not hold. Let $M$ beis.
adeduction of $A’(t)$ represented
terms
two
apparently
contains
but
aclosed and normal deduction of. This suggests that we need addi$t,u$ . Moreover,is not awitness offact,
Parigot proposed addition of new
tional reduction to extract the witness. In
to solve similar problem on normal
reduction rules
is defined by inductively replacing
forms of the natural number type.
in $N$ to $[\alpha]M(L[M^{l}/\alpha])$ . We will prove that adding these
all occurrence offor an atomic
rules suffices to ensure that aclosed normal term of type$A(t)$
holds. Non-confluency$A(x)$ contains one and only one first order term andin classical logic.
analyze
non-determinismof this calculus could be used to
Obviously, to use such calculus for witness extraction, we need normalization
property of it. In addition, if we expect that reduction rules represent extraction
algorithm of witness, strong normalization is desirable. However, symmetric nature of reduction of application to -abstraction seems to prevent obvious adaption of the proof of strong normalization of original -calculus[8]. Luke Ong
and Charles Stewart addressed strong normalization of call-by-value restricti on$\mathrm{A}/\mathrm{i}$$\mathrm{A}/\mathrm{i}$$\mathrm{A}/\mathrm{i}$$\Sigma_{1}^{0}$$\exists x.A(x)$$\exists x.A’(x)$$t$$\mathrm{a}\mathrm{e}$$\Lambda X.\lambda\alpha.\mu\beta.[\beta]\alpha u(\mu\gamma.[\beta]\alpha tM)$$\lambda\mu-\mathrm{t}\mathrm{e}\mathrm{m}\mathrm{s}$$\exists xA’(x)$$\exists xA(x)$$u$$M(\mu\alpha.N)\Rightarrow\mu\beta.N[M^{l}/\alpha]$$N[M^{\cdot}/\alpha]$$[\alpha]L$$\exists xA(x)$

$t$

$\mu$

$\lambda\mu$159Lemma 5. Assume that $(t:):\in:$ , $(A:):\in I$ is defined as Definition 6. If $M\in$, $Mt:\in A_{:}$ . Simil arly, for $(Tj)j\in J$ anddefined as Definition, $MTj\in A_{j}$ .
6, if$(A\mathrm{j})j\in J$$\bigwedge_{\dot{l}\in I}^{1}A:$$M \in\bigwedge_{j\in J}^{2}Aj$

Proof. The proof goes on the sameof that of Lemma 4. We concentrate the. Assume that is the least ordinalsecond order case. Let, $L\in A_{j}$. We will prove that for all such thatsuch that
holds, by induction on and $w(M)$ .
induction hypothesis of
The case where $L\equiv M’Tj$ and $M\Rightarrow 1M’$ .
$w(M’)$ , the thesis follows.
. Since $M\in\Pi_{j\in Jj}^{2}A$ , weandThe case where
have the thesis.
. Let
and
The case where:. By induction hypothesis on , we have $KT\in A_{:}$ . Fromandarbitrariness of $K$ and , it follows$\mathrm{l}\mathrm{i}\cdot \mathrm{e}$$D^{\omega_{1}}(S)= \bigwedge_{:\in I}A:$$\kappa$$L$$t\in D^{\kappa}(S)$$MT\mathrm{j}\Rightarrow 1L$$\kappa$$\mathrm{R}\mathrm{o}\mathrm{m}$$M\equiv\lambda X.M_{1}$$L\equiv M_{1}[T\mathrm{j}/X]$$M\equiv\mu\alpha.M_{1}$$L\equiv\mu\beta.M_{1}[\mu\gamma.[\beta](\gamma T_{})/\alpha]$$K\in D^{\kappa_{1}}(S)$$J\in\bullet A$$\kappa_{1}$$\kappa_{1}$.

$\mu\gamma.[J](\gamma T_{})\in\bullet\cup D^{\kappa_{1}}(S)\kappa_{1}<\kappa$

Since $M$ has a -form, Af. Hence we have$\mu$

. We can infer$\in\bullet\bullet\bigcup_{\kappa_{1}<\kappa}D^{\kappa_{1}}(S)$$L\in\bullet\bullet$ $A_{:}$$[perp]$.

$M_{1}[\mu\gamma.[J](\gamma T_{\dot{1}})/\alpha]\in$

The rest of the proof runs similarly to the usual method of reducibilty candidenotes the set of all functions
dates. Let be the set of all first order tems.
From
to R. Suppose that is amap sending first order variables to first orderto n-ary function from the set of first order terms
terms, apredicate variable
theto R. We extend $xi$ to be amap on the whole types using
following clauses.
$F^{n}$$\mathcal{T}$$\mathcal{T}^{n}$$\xi$$X^{n}$$\xi([perp])=[perp] \mathrm{a}\mathrm{n}\mathrm{d}$

(7)
(8)

$\xi(\bullet A)=\bullet\xi(A)$$\xi(Aarrow B)=\xi(A)arrow\xi(B)$$\xi(\forall xA)=\wedge^{1}\xi[t/x](A)$(9)$t\in \mathcal{T}$(10)$\xi(\forall X^{n}A)=\wedge\xi[f/X^{n}](A)f\in \mathcal{F}^{\mathrm{n}}2$where $\xi[a/b]$ is defined as amap $\xi[a/b](b)=a$ and for $c\neq b$ , $\xi[a/b](c)=\xi(c)$ .
Proposition 2. $Lei$ $M$ be a term of tyPe A. Assume that free first order vari,and ffeeables of $M$ are ,’,first orderofto k-ary function fromvariables to first order terms, a predicate variable,
the set of first order terms to R. For each $1\leq i\leq n$ and ,. Let
is the arity offor$X_{n}$$x_{1}$$Mare..\alpha_{1}^{A_{1}}.,x_{m}$$\ldots p_{ee_{X_{l}^{redicatevat\dot{\mathrm{t}}ablesofMareX_{1}}}},\alpha_{l}.Supposethat\xi isamapse’ nd\cdots ing$

$var\dot{\mathrm{v}}ables$$X^{k}$$t_{1}$$\xi(X:))\xi(X_{\dot{l}})t_{1}\cdots$ $t_{n}\in \mathrm{R}_{B_{j}[t_{1}/x_{1},\cdots,t_{\mathrm{n}}/x_{k}]}$$\cdots$$t_{k}\in \mathcal{T}(k$$N_{j}\in\xi(A\mathrm{j})$160
7. Xx.M is a term of typefor a term $M$ of type and a first order variable$M$. Variables of do not contain as a free variable.
8. $Mt$ is a term of type $A[t/x]$ for a term $M$ of tyPe and a first order terrn$A$$\forall xA$

$x$

$x$

$A$

$t$

.

9. Xx.M is a term of typeand a $tem$ $M$
for a predicate variable$M$
as a free variable.
of type A. Variables of do not contain$A[T/X^{n}]$$M\{T\}$a10.
is a term of a $twe$and anfor term $M$ of type$\forall X^{n}A$$X^{n}$$X^{n}$$\forall X^{n}A$

abstraction term

$T\equiv\lambda x_{1}\cdots$ $x_{n}.B$.

Definition 3. Reduction rules are the followings. Let
variables.
$(\lambda_{1})(\lambda\alpha.M)N$$\Rightarrow M[N/\alpha]$$(\lambda_{2})(\lambda x.M)t$$\Rightarrow Af[t/x]$$\beta,\gamma,\delta$

and y, Y be fresh$(\lambda_{3})(\lambda X^{n}.M)T\Rightarrow M[T/X^{n}]$$(\mu)[M]\mu\alpha.N$$\mathrm{C}\mathrm{G})$$M\cdot M]N$$\Rightarrow N[M/\alpha]$$(\mu\alpha.M)N$$\Rightarrow M[N/\alpha]$$\Rightarrow\mu\beta.M[\mu\gamma.[\beta](\gamma N)/\alpha]M(\mu\alpha.N)\Rightarrow\mu\beta.N[\mu\gamma.[\beta](M\gamma)/\alpha]$$(\zeta_{2})(\mu\alpha.M)t$$\Rightarrow\mu\beta.M[\mu\gamma.[\beta](\gamma t)/\alpha]$(&) $(\mu\alpha.M)T$$\Rightarrow\mu\beta.M[\mu\gamma.[\beta](\gamma T)/\alpha]$

As usual, compatible closure of the rules above is called one-step reduction) and reflexive and transitive closure of one-step reduction isrelation (denoted
caUed reduction relation (denoted ). $w(t)$ is the maximal length of sequences
if the maximum exists. Otherwise $w(t)$ is undefined, isstrongly normalizable if and only if $w(t)$ is defined.
Using and (-rules, Parigot’s structural reduction [6] and symmetric one [7]mentioned in Section 1can be derived.
$\Rightarrow 1$$\Rightarrow$$t$$t\Rightarrow 1t_{1}\cdots\Rightarrow 1t_{n}$$\mu$$(\mu\alpha.

\ldots[\alpha]u\ldots)v\Rightarrow\zeta\mu\beta$$u(\mu\alpha.

\ldots[\alpha]v\ldots)\Rightarrow\zeta\mu\beta$

.

.

.

$\ldots \mathrm{M}\cdot[\beta](xv)]u\ldots\Rightarrow_{\mu}\mu\beta$.

$\ldots \mathrm{M}\cdot[\beta](ux)]v\ldots\Rightarrow_{\mu}\mu\beta$$\ldots[\beta](uv)\ldots$$\ldots[\beta](uv)\ldots$

If we understand ae the usual negation symbol, our -rules resemble to Andou’s.
reduction for
By induction on aterm, it is easy to prove the following lemma.
$\zeta$$\bullet$$[perp]_{e}[1]$Lemma 1. If M is a normal$M\equiv\lambda\alpha$.

$\lambda\mu$

term,$\cdots$ $\lambda X$.

$\cdots$ $\lambda x.\alpha M_{1}\cdots$$M_{m}$

or$M\equiv\lambda\alpha.\cdots\lambda X.\cdots\lambda x.\mu\beta.[\gamma]M_{1}$where$\lambda\alpha$.

$\cdots$ $\lambda X$.

$\cdots$

Ax. is an arbitrary sequence of X-abstraction.

We assume that predicates and function symbols for primitive recursive arithmetic are included in our language. Then we can code second order Peano arithis coded
metic in second order predicate logic. In particular, a -sentence$\forallX^{1}.X^{1}0arrow\forally(X^{1}yarrowX^{1}Sy)arrow$as
A $A(x)$ , where $N(x)$ is defined as
ffom $\exists x.N(x)\wedge A(x)$ , weand $A(x)$ is atomic. Since we can deduce.
extract witness from afomula$\Sigma_{1}^{0}$$\exists x.N(x)$$X^{1}y$$\exists x.A(x)$$\exists x.A(x)$$3\mathrm{x}.\mathrm{A}$161
Proposition 1. Let
be an atomic formula and M be a normal closed term
type.
M contains one and only one first order term t and $A(t)$ holds.
of$A(\mathrm{z}$$\mathit{3}x.A(z)$Proof By Lemma 1, $M$ has thewhereconsists ofabstraction and [ ] . By consideration on type, we have that has atype$X)$ ,
is afirst orderandis aof type $A(t)$ . Since $A(t)$ is atomic$X$and does not contain , we can see thatconsists of axioms alone. We havethe thesis.
$\cdot$$\mathrm{f}\mathrm{o}\mathrm{m}E[\alpha M_{1}\cdots M_{m}]$$\cdot$$E[\cdot]$$\forall x.(Aarrow$$\alpha$$M_{1}$$M_{2}$$\mathrm{t}\mathrm{e}\mathrm{m}$$\mathrm{t}\mathrm{e}\mathrm{m}$$M_{2}$

3Strong normalization
Definition 4. First we prepare several notations.
7. A term beginning with is called a fi-form.
2. For a set of terms of type , $Cl(S)$ is defined as the smallest set which
satisfies clauses(a) $S\subset Cl(S)$ and contains all variables of type .
(b) $MN\in Cl(S)$ if $L\in Cl(S)$ for all such that.
(c) $Mt\in Cl(S)fL\in Cl(S)$ for all such thatfor a first rder
term .
(d) $MT\in Cl(S)$ if $L\in Cl(S)$ for all such that $MT\Rightarrow 1v$ for an abstraction term .
3. The set of strong normalizable tems of typealso denoted .
,4. For a set S of terms of type C
$\mu$

$C$

$S$

$C$

$L$

$MN\Rightarrow_{1}L$$L$$Mt\Rightarrow_{1}v$$\mathit{0}$

$t$

$L$

$T$

$[perp] is$$[perp]$$\neq[perp]$$\bullet S:=\{\mu\alpha.M|\forall N\in S, M[N/x]\in[perp]\}$where$\alpha$.
. Note thatis a variable of type C and M has a type

5. the operator
is defined as
are monotone operators. For ordinal ,$Cl(\mathcal{X}\cup\bullet\bullet X)$$D(\mathcal{X})$$[perp]$$\bullet\bullet$

and hence $D$$\kappa$$D^{\kappa}(\mathcal{X}):=D(\cup D^{\tau}(\mathcal{X}))\tau<\kappa$.

Definition 5(Reducibility candidates). Let
be the first uncountable ordinal andbe a proposition. Let
be a set of strong normalizable terms oftype A. Suppose
does not contain a $\mu- fom[]$ and is closed under reduction
relation. Then, a set
is called a reducibility candidate of the proposition
A. Note that from monotonicity of $D$ , a reducibility candidate is a fixed point of
D. The set of candidates of the proposition is denoted by. is the union.
allof$\omega_{1}$

$A$

$S$

$S$

$S$

$D^{5d_{1}}(S)$$A$$\mathrm{R}_{A}$$\mathrm{R}$$\mathrm{R}_{A}$Lemma 2. Let 72 be a candidate$D^{\omega_{1}}(S)$.

$Il=Cl(S\cup\bullet\bullet \mathcal{R})$Proof Since 7? is fixed point of D, we have

while$D^{\kappa}(S)\subset Cl(S$

Lemma 3. For‘u\bullet \bullet$M\in\bullet \mathcal{R}$$\mathcal{R})$$N\in \mathcal{R}$,$\mathcal{R}=Cl(\mathcal{R}\cup\bullet\bullet \mathcal{R})\supset Cl(S\cup\bullet\bullet \mathcal{R})$

.

and

.

, $[M]N\in[perp]$ .

162such that $[M]N\Rightarrow 1L$ are strong normalizable. We consider each possibilities of the reduction of $[M]N$ .
. The
The case where has the form $[M’]N’$ and $M\Rightarrow M’$ andthesis follows from induction hypothesis on $w(M)+w(N)$ .
and $L\equiv M_{1}[N/\alpha]$ . By the hypothesis.
The case where$N$$L\equiv
N_{1}[M/\alpha]$. By Lemma 2, should be
andThe case where. We have the thesis.
an element of

Proof. It suffices to prove that all$L$$N\Rightarrow N’$$L$$M\equiv\mu\alpha.M_{1}$$M\in\bullet \mathcal{R}$$N\equiv\mu\alpha.N_{1}$$\mathcal{R}$$\bullet\bullet$. Assume that $(t:):\in I$ is a non-empty
andDefinition 6. Letfamily of first order terms and $(Tj)j\in J$ is a non-empty family of $abs$ rraction
is a candidate of the proposition $A1^{t}:/x$] for each $i\in I$ andterms. Farther,is a candidate of the proposition $A[Tj/X]$ for each $i\in J$ . Candidates $Aarrow B$,
are defined by the following steps.
$B\in \mathrm{R}_{B}$$A\in \mathrm{R}_{A}$$A_{:}$$A_{\mathrm{j}}$$\bigwedge_{j\in J}^{2}A_{j}$$\bigwedge_{\in \mathit{1}}^{1}.\cdot A:$

(1)
(2)
(3)
(4)

$L(A,B)$ $:=\{\lambda\alpha^{A}.M|\forall N\in A,M[N/\alpha^{A}]\in B\}$$\Pi_{1\in I:}!A:=\{\lambda x.M|\forall i\in I,M1^{t}:/x]\in A_{i}\}$$\Pi_{j\in Jj}^{2}A:=\{\lambda X.M|\forall j\in J, M1^{T}j/X]\in A_{j}\}$$Aarrow B$ $:=D^{w_{1}}(L(A,B))$

Lemma 4. let$.\cdot\wedge^{1}A::=D^{w_{1}}(\Pi_{1\in::}\in:!A)$(5)$j\in J\wedge A::=D^{w_{1}}(\Pi_{\mathrm{j}\in J:}^{2}2A)$

(6)

and

$A\in \mathrm{R}_{A}$$B\in \mathrm{R}_{B}$. If $M\in Aarrow B$ and $N\in A$, $MN\in B$ .

. Assume thatis the least ordinal such that $M\in$and is the least ordinal such that $N\in D^{\tau}(S)$ . By induction onprove that if $MN\Rightarrow 1L$ ,and $w(M)+w(N)$ , wethe natural sum$L\in B$ , which is the exact condition of $MN\in B$ .
The case $L\equiv M’N’$ and either $M\Rightarrow 1M’$ and $N\equiv N’$ or $M\equiv M’$ and. The thesis follows from induction hypothesis on $w(M)+w(N)$ .
and $L\equiv M_{1}[N/\alpha]$ . Since $M\in L(A,B)$ , we have the
The casethesis.
and is obtained from reduction of
The case where $M$ has aform,. Let
the outermost redex. Then, has a$K\in D^{\kappa_{1}}(.L(A,B))$ for. By induction hypothesis on , we have $KN\in$$[J](KN)\in[perp]$. Prom arbitrariness of $K$ and ,. It follows.
follows. Since $M$ is a form
Now,
, we have.
. Since
We can infer, the thesis follows.
fromand is obtained from reduction of the
The case where $N$ has aform. Let $J\in B$ andoutermost redex. has aformfor. Rom induction hypothesis on , we have $MK\in B$ . Similarly as. Since $N$ has a form $N\in$Proof. Let$A=D^{\omega_{1}}(S)$$D^{\kappa}(L(A,B))$$\kappa$$\tau$$\mathrm{w}\mathrm{i}\mathrm{u}$$\kappa\oplus\tau$$N\Rightarrow_{1}N’$$M\equiv \mathrm{p}\mathrm{a}.\mathrm{M}\mathrm{i}$$L$$\mu\alpha.M_{1}$$L$$\kappa_{1}<\kappa$$\kappa_{1}$$B$$\bullet$$\kappa_{1}$$\bigcup_{\kappa_{1}<\kappa}D^{\kappa_{1}}(L(A,B))$$\mu\gamma.[J](\gamma N)\in$$M \in\bullet\bullet\bigcup_{\kappa_{1}<\kappa}D^{\kappa_{1}}(L(A,B))$$\mu$$M_{1}[\mu\gamma.[J](\gamma N)/\alpha]\in[perp]$$\bullet\bullet$$J\in\bullet B$$\mathrm{f}\mathrm{o}\mathrm{m}\mu\beta.M_{1}[\mu\gamma.[\beta](\gamma N)/\alpha]$$J\in\bullet B$$L\in\bullet\bullet$$B$$B\subset B$$\mu\alpha.N_{1}$$L$$\tau_{1}<\tau$$L$$K\in D^{\tau_{1}}(S)$$\mu\beta.N_{1}[\mu\gamma.[\beta](M\gamma)/\alpha]$$\tau_{1}$$D^{\tau_{1}}(S)$$\mathrm{a}\mathrm{b}\mathrm{o}\mathrm{v}\mathrm{e},\mathrm{i}\mathrm{t}\mathrm{f}\mathrm{o}11\mathrm{o}\mathrm{w}\mathrm{s}\mu\gamma.[J](M\gamma)\in\bullet\cup\bullet\bullet\bigcup_{\tau_{1}<\tau}D^{\tau_{1}}(S).\mathrm{W}\mathrm{e}\mathrm{h}\mathrm{a}\mathrm{v}\mathrm{e}N_{1}[\mu\gamma.[\beta]7^{<\tau}M\gamma)/\alpha]\in[perp] \mathrm{a}\mathrm{n}\mathrm{d}$$\mu$hence,$L\in B$.

163
is confluent, hence useful as aprogramof this calculus [5]. Their calculus
ming language. However, imposing reduction strategy seems to be an alien idea
in alogical calculus, and non-determinism is lost.
Barbanera and Berardi proved strong nomalization of anon-deterministic
calculus for propositional classical logic using fixed point construction for reducibility candidates [2]. We will prove strong nomah.zation of second order-calculus with the rules above based on this method.
$\lambda\mu_{v}$$\lambda\mu$

2Symmetric $A/x$-calculus
calculus
Our formalization is exactly asecond order extension of symmetricin [9]. Usually, aterm of -calculus is understood as aproof with multiple-term as aproof with asinconclusions. On the contrary, we consider agle conclusion but two kinds of hypothesis, ordinary hypothesis and denials of$\lambda\mu$$\mathrm{A}/\mathrm{i}$$\mathrm{A}/\mathrm{i}$propositions, which correspond conclusions other than aprincipal formula inusual -calculus. Moreover, we do not distinguish A-variables and -variables.
,
stand for first order variables and terms.
and $t,u,t_{1}$ ,$x,y,x_{1}$ ,denotes n-ary predicate variables and constants.
$\lambda\mu$$\mu$$X^{n}$$\cdots$$\cdots$$\mathrm{Y}^{n},X^{n}.\cdot$

proposition is that of second order predicate logic built up by
Definition 1.
and logical connectives , . Formally,
predicate variables$A$$\forall$$arrow$$X_{}^{n}$$A::=X_{}^{n}t_{1}\cdots$ $t_{n}|Aarrow A|\forall x:A|\forall X_{\dot{1}}^{n}$ $A$.

formula is a proposition or a denialof proposition or contradiction .
Note that 1is not counted as a proposition. Other connectives are defined by usis defined as
ing second order construct. For example,
$A$

$A$

$\bullet A$$[perp]$$\forall X^{0}.\forall x(A(x)arrow$$\exists x.A(x)$$X^{0})arrow X^{0}$.

We assume axioms of our calculus is limited to those for atomic propositions
for atomic proposition . Weor formulae with aform$A_{1}arrow A_{2}$$arrow\cdotsarrow A_{n}$denote axioms and variable by Greek letters$\alpha,\beta$$A_{:}$,$\cdots$.

Definition 2. For each formula A, Ajz-terms of tyPe A are defined inductively

as follows.

1. A variable or an axiom
is a term of tyPe C. We assume that there is novariable of $type[perp]$ .
2. $[M]N$ is a term of type 1 for a term M of type \bullet A and a tem N of type A.
and a term $M$ of type3. pa.M is a term of type for a variable of type$\alpha^{C}.\cdot$$A$$[perp]$$\bullet A$$\alpha$.

4. pa.M is a term of tyPe for a variable of tyPe and a term $M$ of tyPe
1.
5. Aa.M is a term of type $Aarrow B$ for variable of type and a term $M$ oftype .
6. $MN4$ is a term of type B for a term M of type A $arrow B$ and a term N of type$\bullet A$$A$$\alpha$$\alpha$

$B$

$A$

164
15 j

I. We define M by simultaneous substitution. $>Ng$ into ,into.\rangleinto,og on M. Then$\ovalbox{\tt\small REJECT}:(\mathrm{z}_{\ovalbox{\tt\small REJECT}})_{\mathrm{t}}\ovalbox{\tt\small REJECT}\ovalbox{\tt\small REJECT}\ovalbox{\tt\small REJECT}$$\ovalbox{\tt\small REJECT}$$@_{\mathrm{b}^{\ovalbox{\tt\small REJECT}}Ftt\ovalbox{\tt\small REJECT}}.\ovalbox{\tt\small REJECT} B_{1_{\rangle}}\ovalbox{\tt\small REJECT}$eoe have ME $((A)$ .

$B_{n}$$Xg_{\rangle z}^{\ovalbox{\tt\small REJECT}}.X_{r\ovalbox{\tt\small REJECT}}Ng_{\rangle}\ovalbox{\tt\small REJECT}$$0_{1}$$\ovalbox{\tt\small REJECT}\ovalbox{\tt\small REJECT}\ovalbox{\tt\small REJECT}$$\mathrm{t}4(\mathrm{x}_{\mathrm{m}})$

Proof. By induction on the construction of M.
As aspecial case, t $\in\xi(A)$ holds. Rom Lemma 2, we have the following
theorem.
Theorem 1. All terms are strongly normalizable.
Acknowledgement. Iam grateful to Ken-etsu Fujita, Ryu Hasegawa andCharles Stewart for their helpful comments and discussion.

References
1. Yuuki Andou. Anormalization-procedure for the first order classical natural dedudion with full symbols. Tsukuba Journal of Mathematics, 19(1):153-162, 1995.
2. F. Barbanera and S. Berardi. Astrong normalzation result for classical logic. Ann.
,1995.
Pure Appl.
-calculus. In Trees in algebra and-translation of the
3. Ph. de Groote. A
programming, CAAP ‘94, number 787 in Lect. Notes Comput. Sci, pages 85-99.
Springer-Verlag, 1994.
4. Ph. de Groote. On the relation between -calculus and the syntactic theory of
sequential control. In Logic programming and automated reasoning, volume 822 ofLect. Notes Comput. Sci pages 31-43. Springer-Verlag, 1994.
5. G.-H. L. Ong and C. A. Stewart. Acurry-howard foundation for functional compuAnnual ACM SIGPLAN-SIGACT
tation with control. In Proceedings of the
Symposium on Principles of Programming Languages. ACM press, .J muary 1997.
6. M. Parigot.
-calculus:an algorithmic interpretation of classical natural deduction. In A. Voronkov, editor, Logic Programming and Automated $Re.u$ $onng$, volume 624 of Lecture Notes in Artificial Intelligence, pages 190-201. Springer-Verlag,
1992.
7. M. Parigot. Classical proofs as programs. In Computational logic and proof theory,
pages 263-276. Springer-Verlag, 1993.
volume 713 of Lect. Notes Comput
8. M. Parigot. Strong normalzation for second order classical natural deduction. J.
Symb. Log., 62(4):1461-1479,1997.
9. M. Parigot. On the computational interpretation of negation. In P. Clote and
H. Schwichtenberg, editors, Computer Science Logic, volume 1862 of Lect. Notes
pages $472_{-}484$ . Springer-Verlag, 2000.
Comput.
10. Th. Streicher and B. Reus. Classical logic, continuation semantics and abstract
machines. Journal of Functional Programming, $8(6):543-572$ ,1995.
$L\dot{\varphi}\mathrm{q}76:99-116$$\mathrm{A}/\mathrm{i}$$\mathrm{c}\mathrm{p}\triangleright$$\lambda/\iota$$\ell \mathit{4}fl$$\mathrm{A}/\mathrm{i}$$Sc\backslash \cdot$$Scc\dot{\backslash }$