数理解析研究所講究録
918 巻 1995 年 206-223

206

Extracting a reduction systemfrom a conjunction calculus
Akefumi Kumeta*

July 1995

1

Introduction

The purpose of this paper is to show that we can obtain a strongly norsystem from a variant of Lawvere
malizing and confluent abstract
style deductive system [Lambek 94] for a propositional calculus with conjunctions. The deductive system is reminiscent of a sequent calculus, andconsists of Lawvere style deductions, namely each of which has exactly one
input and one output, and inference rules that includes, initial deduction,
composition rule, and also left and right rules for conjunctions. It enjoys
the composition rule elimination theorem, which is thought of as a kind of
cut elimination theorem. In order to analyze the computationaI aspects, inparticular the operational semantics, we introduce a -term algebra whose
sorts are the deductions and operation symbols correspond to the inference
rules. Then each -term corresponds to the unique derivation of a deduction, and vice versa. First we show that we can eliminate operation symbols
corresponding to composition rule. This result, the weak normalization theorem, amounts to the composition rule elimination theorem of the deductive
system. Next, from the proof of the theorem, we extract a binary relation on
the -terms so that the -terms and the relation form an abstract reduction
system, which is not a term rewriting system by some reason. Finally weshow that it is strongly normalizing and confluent. As an application theword problem for the equivalence relation generated by it is thus decidable
as expected.
$\mathrm{r}\mathrm{e}\mathrm{d}_{11\mathrm{c}\mathrm{t}}\mathrm{i}_{0}\mathrm{n}$$\Sigma$$\Sigma$$\Sigma$$\mathrm{H}\mathrm{i}\mathrm{t}\mathrm{a}\mathrm{c}1_{1}\mathrm{i}$$\Sigma$

Software Engineering Co., Ltd. E–mail: akeoori. hitachi-sk.

$\mathrm{c}\mathrm{o}$

. jp

207

The underlying motivation of this study is to investigate the connection
between reduction systems and deductive systems. For a given deductive
system , we would like to find an abstract reduction system $(T,R)$ , withbeing a set of terms in which each term interprets a proof of , andis desired tobeing a binary relation on . As a computational model,
is tobe strongly normalizing and confluent. An application of such ( $T,$show that the word problem for the equivalence relation generated byis decidable by means of confluence method. The reduction system.
might also be used as a basis of constructive
betweencorrespondence
As a special case, we can think of the following-term algebras and sequent calculi, which is called $sequent_{S- a}s- So\Gamma ts$ interpretation. Let be a given sequent calculus that enjoys cut-elimination.
Let be a signature whose sorts are the sequents and operations correspond, the set of -terms, is a sound and comto the inference rules. Then
plete interpretation of derivations of . Since enjoys cut-elimination,
extracted from theis weakly normalizing. Let be a binary relation on
may have further
weak normalization. Then the reduction systemproperties like strong normalization and confluence.
$D$

$D$

$T$

$R$

$R$

$T$

$R\rangle$$R$$\langle T, R\rangle$$\mathrm{p}\mathrm{r}\mathrm{o}\mathrm{g}\mathrm{r}\mathrm{a}\mathrm{m}\dot{\min}\mathrm{g}$$\Sigma$$S$$\Sigma$$\Sigma$$\tau_{\Sigma}$

$S$

$S$

$\tau_{\Sigma}$$R$$\tau_{\Sigma}$$\langle\tau_{\Sigma}, R\rangle$

2

A conjunction calculus

In this section we introduce a variant of Lawvere style deductive system fora propositional calculus with conjunctions. Then we introduce a -term
algebra whose sorts are the deductions and operation symbols correspondto inference rules. For each deduction, there is a bijection between -termsof the deduction and derivation of the deduction.
$\Sigma$$\Sigma$be some set of propositional symbols. The set ofDefinition 1 Let
propositional conjunction formulae, notation , is defined inductively
as follows$7^{\mathit{2}}S$$\mathcal{F}$$::=$$\mathcal{F}$Definition 2$T\sim he$$7^{\mathit{2}}S|(F\wedge \mathcal{F})$.

set of Lawvere style deductions over
$D$

$::=$

$\mathcal{F}-arrow F$$\mathcal{F}$is defined by.

,
Definition 3 A deduction $A-arrow B\in D$ is derivable,
produced
is derivation of the deduction, in other words if it can be
ifusing the following rules.
$notati_{\mathit{0}}n\vdash A-arrow B$$tl\iota ere$

$a$

208

$\bullet$

The identity axiom and the composition rule
$Carrow B$$A-arrow C$$Aarrow A$

ID

–COMP
$A-arrow B$

call the composition formula.
The rules for conjunctions$C$$\nu Ve$$\bullet$$Carrow A$$Barrow C$$A-arrow C$$A\wedge Barrow C$$A$$Carrow B$$-\wedge- \mathrm{R}$$Carrow A$ A $B$

A-L’

A-L
A $Barrow C$

Definition 4 (Signature of Proof Terms) The signature-indexed familysists of and a$(\Sigma_{w,s}|w\in D^{*},$$setS_{J}$

over

$D$

con-

$D^{*}\cross D$

$D$

of

$\Sigma$where for any $A,$ $B,$
$1_{A}$$\in$$\sigma_{A,B}^{C}$$\in$$\pi_{A,B,C}$$\in$$\pi_{A,B,C}’$$\in$$C\in \mathcal{F}$$s\in D\rangle$,( is the empty word) (identity),$\Sigma_{Aarrow ccarrow}B,$ $Aarrow B$( . position),(projection),(projection),(product),$\Sigma_{\lambda,Aarrow A}$$’\backslash$$\mathrm{c}\mathrm{o}_{\vee}\mathrm{m}$$\Pi_{C,A_{\mathrm{t}}}w,S$$=\in$$\Sigma_{Aarrow C},$

$A\wedge Barrow C$$\Sigma_{B-arrow c,A\wedge}Barrow C$$\emptyset otherwise\Sigma_{Carrow Ac}arrow B.’ Crightarrow A\wedge B$

Definition 5 (Proof Terms over 7) The set of proof terms over.
notation , is defined as the set of ground -terms that is$)$

Below the notation : $A-arrow B$ stands for
The following proposition obviously holds.
$f$$\mathrm{P}\mathrm{r}o$$T=T_{\Sigma}$$\Sigma$$\mathcal{T}$$f\in \mathcal{T}_{Aarrow B}$.

position 6 (Subformula Property of Operation Symbols)

1. $1_{A}:A-arrow A$ ,2. if $\sigma_{A,B}^{C}(f,g):Aarrow B$ then$f$

: $A-arrow C$ and $g:C-arrow B$ ,3. if $\pi_{A,B,C}(f):$$A$

A $B-arrow C$ then $f$ : $Aarrow C$ ,

4. if

$A$

A $B-arrow C$ then$\pi_{A,B,C}’(f):$$f$: $Barrow C$ ,

$D$

,

209

5. if $\Pi_{C,A,B}(f,g)$ : $Carrow A$ A

$B$

then

: $Carrow A$ and $g:Carrow B$ .

$f$

This property permits us to omit subscripts of operation symbols of a term
except composition formula of composition symbols provided that the sortof the term is known.
It is clear that the next proposition holds, which says that the derivationsof deductions can be interpreted soundly and completely by the -term
interpretation,
algebra. We call this interpretation the-sorts interpretation.
which is a kind of$\Sigma$$\mathrm{d}\mathrm{e}\mathrm{d}\mathrm{u}\mathrm{c}\mathrm{t}\mathrm{i}_{\mathrm{o}\mathrm{n}}\mathrm{s}- \mathrm{a}S- \mathrm{s}\mathrm{o}\mathrm{r}\mathrm{t}_{\mathrm{S}}$$\mathrm{s}\mathrm{e}\mathrm{q}\mathrm{u}\mathrm{e}\mathrm{n}\mathrm{t}\mathrm{s}arrow \mathrm{a}\mathrm{s}$Interpretation) For each deducProposition 7 ($A-arrowB$
there exists a bijection between the derivations of $Aarrow B$ andtion$\mathrm{D}\mathrm{e}\mathrm{d}\mathrm{u}\mathrm{c}\mathrm{t}\mathrm{i}\mathrm{o}\mathrm{n}\mathrm{S}^{-}\mathrm{a}\mathrm{S}-\mathrm{s}_{0}\mathrm{r}\mathrm{t}\mathrm{S}$$T_{Aarrow B}$.

A reduction system

3

In the process of proving the weak normalization theorem in the -term
algebra, which amounts to the composition rule elimination theorem in the
deductive system, we extract a reduction relation, which turns out to bestrongly normalizing and confluent.
$\Sigma$,
Definition 8 The set of nornlal forms of sort $Aarrow B$ , notation$AarrowB$which contains no occurrencesis the set of ground -terms of sort
$N_{A-arrow B}$$\Sigma$of composition symbols.

Definition 9 The degree of$a$formula$A$, notation

follows$\bullet$$\partial(P)=1$$\partial$$\bullet$

(A A

$B$

)

,

$\partial(A)$, is defined aswhere $P\in PS$ ;$= \max(\partial(A), \partial(B))+1$

where $A,$ $B\in F$ .

,, is defined to, notation
The degree of a composition symbol.
be the degree of the composition formula that is, is thethe degrees ofof term , notation
The degree of aits composition symbols, so $\partial(f)=0$ iff is a normal form.
notation $h(f)$ , is that of its associated tree.
The height of a proof term$\sigma^{C}$$\partial(\sigma^{C})$$C$$\mathrm{p}\mathrm{r}o$$f$$\partial(\sigma^{C})=\partial(C)$$\sup\dot{o}f$$\partial(f)$$f$$f_{f}$. Let : $Aarrow C$ and $g:Carrow B$
Definition 10 (Redex) Let $A,$ $B,$
. Then a proof term being of the form
such that$C\in \mathcal{F}$$\partial(f),$$\partial(g)<\partial(C)$$\sigma^{C}(f,g)$

is called$a$redex.

$f$

210

Note that the degree of a redex
is the degree of the composition
formula . Then next lemma and proposition can be shown in a usual
constructive manner as in [Girard 89] for example.
$\sigma^{C}(f,g)$$C$

Lemma 11 (Principal lemma) Let
that$\sigma^{C}(f,g)$$C$

be a formula of degree$d$. Suppose: $Aarrow B$

is a redex. Then we can make a proof term$h$

: $A-arrow B$

such that $\partial(h)<d$ .

See appendix A for the proof of the principal lemma. Precise trace of theproof of this lemma suggests a one-step reduction relation as follows. The
resulting relation is somewhat cumbersome, since we do not ignore the degrees of terms. But the degree information ensures that the degree of a term
decreases as reduction proceeds. The relation and the terms form an ARS(abstract reduction system) but not a TRS.
Definition 12 (Principal$\mathrm{R}\mathrm{e}\mathrm{d}\mathrm{u}\mathrm{c}\mathrm{t}\mathrm{i}\mathrm{o}\mathrm{n}arrow_{p}$) We define a $relationarrow_{p}$ by,$arrow_{p}=arrow 1\cuparrow 2^{\cup}arrow 3\cuparrow 4\cuparrow\epsilon\cuparrow_{7}\cuparrow 8^{\cuparrow}9^{\cup}arrow 10$, which are extracted from the proof of the principal lemma, areis thedenotes
defined as follows. Below the notation$wherearrow_{i}’ s$$\sigma^{C}(f, g)arrow ih$$D$$thatarrow_{i}$-indexed family of relations$\{(\sigma^{C}(f,g), h)\in \mathcal{T}_{Aarrow B}\cross \mathcal{T}_{Aarrow B}|\partial(f), \partial(g)<\partial(C)\}$$\sigma^{A}(1, f)arrow 1f$,$\sigma^{B}(f, 1)arrow 2f$,$h)arrow_{3}\sigma^{D}(f, \sigma C(g, h))$,$\sigma^{C}(f, \sigma^{D}(g, h))arrow 4\sigma^{D}(\sigma^{c}(f,g),$ $h)$,$\sigma^{C}(\sigma^{D}(f,g),$$\sigma^{C}(\mathcal{T}1(f),g)arrow 6\pi(\sigma^{c_{(f,g)}})$,$g)arrow\tau\pi’(\sigma(f,g))$ ,$\sigma^{c_{(\pi’(f}c}),$$\sigma^{c_{(f,())}c}\Pi g1,g2arrow 8\mathrm{n}(\sigma(f,g1),$ $\sigma^{c}(f,g_{2}))$$\sigma^{C_{1}\wedge}(c2\Pi(f1, f2),$ $\pi(g))arrow_{9}\sigma(c_{1}f_{1},g)$,$\sigma^{C_{1^{\wedge}}C}2(\Pi(f1,f2),\pi’(g))arrow 10\sigma^{C_{2}}(f_{2}, g)$

.

,

.

211

Definition 13 (One-stepible relation generated$\mathrm{D}\mathrm{e}\mathrm{f}\mathrm{i}\mathrm{n}\mathrm{i}\mathrm{t}\mathrm{i}\mathrm{o}\backslash \mathrm{n}14$$\mathrm{R}\mathrm{e}\mathrm{d}\mathrm{u}\mathrm{c}\mathrm{t}\mathrm{i}\mathrm{o}\mathrm{n}arrow$$byarrow_{p},$

$i.e$

.

) The $relationarrow is$ the compat-$arrow$$g$$\sigma^{C}(f_{1}, f_{2})$$arrow$$\sigma^{C}(g_{1}, f_{2})$$\sigma^{C}(f_{1}, f_{2})$$arrow$$\sigma^{C}(f_{1},g_{2})$$\pi(f)$$arrow$$\pi(g)$$\pi’(f)$$arrow$$\pi’(g)$$\Pi(f1, f_{2})$$arrow$$\Pi(g_{1},f_{2})$$\Pi(f_{1}, f_{2})$$arrow$$\Pi(f_{1},g_{2})$The $ARSC$ is defined by

,
if
,
if
,
if
if $farrow g$ ,if $farrow g$ ,
,
if
.
if
.
$farrow_{p}g$$f$$f_{1}arrow g_{1}$$f_{2}arrow g_{2}$$f_{1}arrow g_{1}$$f_{2}arrow g_{2}$$C=\langle \mathcal{T}, arrow\rangle$

By using the principal lemma we have the following proposition. See appendix for the proof of this proposition.
$\mathrm{B}$

Proposition 15 Let : $A-arrow B$ such that $\partial(f)>0$ . Then we can conand $farrow^{*}g$ .
struct a proof term $g:Aarrow B$ such that$f$$\partial(f)>\partial(g)$By iterating the above proposition we have the next result.

Theorem 16 (Weak Normalization) For every proof term.
such that
there is a normal form

: $A-arrow B$ ,$farrow^{*}\mathrm{n}\mathrm{f}(f)$$\mathrm{n}\mathrm{f}(f)\in N_{Aarrow B}$

We have the following results. See appendix$\mathrm{T}1_{1}\mathrm{e}\mathrm{o}\mathrm{r}\mathrm{e}\mathrm{m}17$$f$$\mathrm{C}$for the proof of this theorem.

(Strong Normalization) Every term is strongly normaliz-ing.
locally confluent we need to introduce the next congruence
To show
relation. This relation cannot be extracted from the principal lemma since
it does not involve any composition symbols.
$\mathrm{t}\mathrm{h}\mathrm{a}\mathrm{t}arrow \mathrm{i}\mathrm{s}$on) We define the relation
Definition 18 (Congruence relation
proof terms as the -indexed family of the congruence relations generated$=\Pi$$=\mathrm{n}$$D$by the union of the relations$\{(l, r)\in TA_{1}\wedge A_{2^{arrow}}B_{1^{\wedge}}B_{2}\cross \mathcal{T}_{A_{1^{\wedge}}A_{2^{-}}B_{1}\wedge B_{2}}|$$l=\Pi(\pi(f), \pi(g)),$ $r=\pi(\Pi(f,g))$for some$f$:$A_{1}-arrow B_{1},$ $g:A_{1}-arrow B_{2}$

}

212

and
$\{(l,r)\in\tau A_{1^{\wedge}}A_{2}arrow B_{1}\wedge B_{2}\cross \mathcal{T}_{A_{1}\wedge A_{2-B}}1\mathrm{A}B_{2}|$$l=\Pi(\pi(\prime f),\pi^{J}(g)),$ $r=\pi’(\Pi(f,g))$for some :$f$$A_{2}-arrow B_{1,g}$:$A_{2}arrow B_{2}$}.

By checking all the critical situations we get the following result. See appendix for the proof of this proposition.
$\mathrm{D}$Proposition 19 (Local Confluence) The $relationarrow is$ locally confiuent
modulo the congruence.
$=\Pi$As a corollary we have the following theorem by the Newman’s lemma.
Theorem 20 The $ARSC$ is strongly normalizing and confluent modulo thecongruence.
$=\Pi$As an application the word problem for the equivalence relation generated
by the ARS is thus decidable as expected.
$C$

4

Related Work

5

Conclusion

We havea method to investigate operational semantics of deductive systems although the target deductive system was quite simple. Firstly,$\mathrm{a}\tilde{\mathrm{t}}\mathrm{t}\mathrm{e}\mathrm{m}\mathrm{p}\mathrm{t}\mathrm{e}\mathrm{d}$213

we introduced a -term algebra corresponding to a variant of conjunction
interpretation. This interpretation is
calculus by means ofclearly sound and complete. Secondly, after having showed the weak normalization theorem, we extracted a reduction relation from the principal
lemma. Finally the reduction system was shown to be strongly normalizing
and confluent modulo a congruence relation.
-sortsWhat we have shown in this paper indicates that theinterpretation is an effective way to investigate the operational semantics
of sequent calculi. There do not seem any significant obstacles to obtain-term algebra interpretations of other sequent calculi, including substructural logics [Ono 90], or even Gentzen’s . To extract strongly normalizing
and confluent reduction relations, we may, however, need to invent sometechnique to handle structural rules. This issue will be a future work.
$\Sigma$$\mathrm{s}\mathrm{e}\mathrm{q}\mathrm{u}\mathrm{e}\mathrm{n}\mathrm{t}_{\mathrm{S}\mathrm{a}}- \mathrm{s}- \mathrm{s}\mathrm{o}\mathrm{r}\mathrm{t}_{\mathrm{S}}$$\mathrm{s}\mathrm{e}\mathrm{q}\mathrm{u}\mathrm{e}\mathrm{n}\mathrm{t}_{\mathrm{S}-}\mathrm{a}\mathrm{s}$$\underline{\nabla}$$\mathrm{L}\mathrm{J}$

References[Girard 89] Girard, J. Y., Taylor, P., and Lafont, Y.: Proofs and Types,
Cambridge, 1989.
[Lambek 68] Lambek, J.: Deductive Systems and Categories I, Mathematical Systems Theory, vol. 2, Springer, 1968, pp.287-318.
[Lambek 93] Lambek, J.: Logic without Structural Rules (Another Look
, K. ed., Subat Cut Elimination), In Schroeder-IIeister, P. andstructural Logics, Oxford, 1993, pp.179-206.
$\mathrm{D}_{0\dot{\mathrm{S}}_{\backslash }}\mathrm{e}\mathrm{n}$[Lambek 94] Lambek, J.: What is a Deductive System, In Gabbay, DOV
M., ed., What is a Logical System, Oxford, 1994, pp.141-159.

[Ono 90]. Ono, H.: Structural rules and logical hierarchy, In Petkov, P. P.
ed., Mathematical Logic, Plenum, 1990, pp.95-104.
[Szabo 74] Szabo, M. E.: A categorical equivalence of proofs, Notre Dame
Journal of Formal Logic, Vol. 15, 1974, pp.177-191.
[Szabo 78] Szabo, M. E.: Algebra of proofs, North-Holland, 1978.

A

Proof of Principal lemma: A $arrow B$ is a redex.
Let C be a formula of degree d. Suppose that
We construct a proof term h by induction on $h(f)+h(g)$ .
$\sigma^{C}(f,g)$

214

1. Suppose that $C=A$ and that $f=1:A-arrow A$ and $g:Aarrow B$ . Then
is .
$h$

$g$

2. Suppose that $C=B$ and that
is .
$h$

$f$

: $Aarrow B$ and $g=1:Barrow B$ . Then$f$

3. Suppose that$f=\sigma^{D}(f_{1},f_{2}):Aarrow C$

such that
where : $Aarrow D$ and : $Darrow C$ for some
. Then by the induction hypothesis for and , we have a proof term
. And so we obtain a proof term
: $D-arrow B$ such thatas follows$d$$f_{2}$$g$$\partial(h_{1})<d$$h_{1}$$h$$h=\sigma^{D}(f_{1})h_{1}):A-arrow B$

4.

$\partial(D)<$$D\in \mathcal{F}$$f_{2}$$f_{1}$$\mathrm{S}\dot{\iota}_{\mathrm{P}\mathrm{p}_{0}\mathrm{s}\mathrm{e}}1$

.

that

: $C-arrow B$: $Darrow B$ for some

$g=\sigma^{D}(g_{1},g2)$

where : $Carrow D$ and. Then by the induction hypothesis for: $A-arrow D$ such that $\partial(h_{1})<d$ .
term
term as$g_{2}$$g_{1}$$d$$h_{1}$$h$such that $\partial(D)<$and , we have a proof
so we obtain a proof$D\in \mathcal{F}$$f$$g_{1}$$\mathrm{A}\mathrm{I}\tilde{\mathrm{t}}\mathrm{d}$$\mathrm{f}\mathrm{o}\mathrm{U}\mathrm{o}\mathrm{w}\mathrm{S}$$h=\sigma^{D}(h_{1,g):}2Aarrow B$

6 . Suppose that $A=A_{1}$ A$\beta^{1}$$A_{2}$.

and that$f=\pi(f_{1})$:$A_{1}$

A $A_{2}-arrow C$ ,where
: $A_{1}-arrow C$ . Then by the induction hypothesis for and ,: $A_{1}arrow B$ such that $\partial(h_{1})<d$ . And so we
we have a proof term
obtain a proof term as follows$f_{1}$$f_{1}$$g$$h_{1}$$h$$h=\pi(h_{1})$/7 $l$. Suppose that $A=A_{1}$ A$A_{2}$:$A_{1}\wedge A_{2}-arrow B$.

and that$f=\pi’(f_{1})$:$A_{1}$

A $A_{2}-arrow C$ ,where
: $A_{2}-arrow C$ . Then by the induction hypothesis for and ,. And so we: $A_{2}-arrow B$ such that
we have a proof term
obtain a proof term as follows$f_{1}$$f_{1}$$\partial(h_{1})<d$$h_{1}$$h$$h=\pi’(h_{1})$:$A_{1}$

A $A_{2}-arrow B$ .

$g$

215

$\mathrm{f}t$. Suppose that $B=B_{1}$ A$B_{2}$and that$g=\Pi(g_{1},g2):Carrow B_{1}$ A $B_{2}$,: $Carrow B_{1}$ and : $Carrow B_{2}$ . Then by the induction hywhere: $Aarrow B_{1}$potheses for and and for and , we have aproof terms$\partial(h_{2})<d$. And so we obtain a: $Aarrow B_{2}$ such that
andproof term as follows$g_{2}$$g_{1}$$f$$f$$g_{1}$$h_{1}$$g_{2}$$\partial(h_{1}),$$h_{2}$$h$$h=\Pi(h_{1},h_{2})$$\mathfrak{q}\text{ノ}S$. Suppose that $C=C_{1}$ A$C_{2}$$f=\mathrm{n}(f_{1},f_{2}):Aarrow C_{1}$:.

$A-arrow B_{1}\wedge B_{2}$and tha.tA$C_{2}$

and $g=\pi(g_{1}):c_{1}$ A $C_{2}arrow B$ ,where
: $A-arrow C_{1},$ : $A-arrow C_{2}$ , and : $C_{1}-arrow B$ . Since
we obtain a proof term as follows$f_{1}$$f_{2}$$g_{1}$$h$$\partial(C)$.

$h=\sigma^{C}(f_{1},g_{1}):Aarrow B$$l^{\mathit{0}}q$$\partial(C_{1})<$. Suppose that $C=C_{1}$ A$C_{2}$and that$f=\Pi(f_{1}, f_{2})$where$f_{1}$$g_{1}$$C_{2}$,: $A-arrow C$ , and also that
: $A-arrow C_{1}$ and $f_{22}$$g=\pi’(g_{1})$wherefollows: $Aarrow C_{1}$ A: $C_{2}-arrow B$ . Since:$c_{1}$

A $C_{2}-arrow B$ ,$\partial(C_{2})<\partial(C)$we obtain a proof term

$h=\sigma^{C_{2}}(f_{2},g_{1}):A-arrow B$

$h$

as

.

$\square$

Proof of Proposition 15$\mathrm{B}$Let : $A-arrow B$ such that $\partial(f)>0$ . By induction on $h(f)$ we show thatand $farrow^{*}g$ .
such that
there is a proof term$f$$g:\mathit{4}1-arrow B$$\partial(f)>\partial(g)$1. Suppose that $A=B$ and $f=1$ : $A-arrow A$ . Then $\partial(f)=0$ , and so theclaim holds vacuously.

216

2. Suppose that$f=\sigma^{c_{(f1}},f2):Aarrow B$: $A-arrow C$ andfor some
There are several cases.
$f_{1}$$f_{2}$,: $Carrow B$ .

$\partial(f2)\leq\partial(C)=d$ . Then by the induction hy(a) Suppose that
: $A-arrow C$ and : $Carrow B$
and , there exist
pothesis for. Thenandsuch that-. is a redex, and so we obtain a proof
term by the above lemma.
$\partial(f2)>\partial(C)$ .
Then by the induction hy(b) Suppose that
: $Aarrow C$ andwe have proof terms
andpotheses for.
and: $C-arrow B$ such that
And so we obtain a proof term as follows$\partial(f_{1}),$$f_{2}$$f_{1}$$\partial(f_{1}’),$$f_{2}’$$f_{1}’$$\partial(f_{2}’)<\partial(C),$$f_{2}arrow^{*}f_{2}’$$f_{1}arrow^{*}f_{1}’$$\psi^{-c}(f_{\acute{\mathrm{J}},\mathrm{r}_{\mathit{1}}}\partial\prime\prime,\ovalbox{\tt\small REJECT}’-$$g$$\partial(f_{1}),$$f_{2}$$f_{1}$$g_{1}$$\partial(g_{1}),$$g_{2}$$\partial(g_{2})<d,$$f_{2}arrow^{*}g_{2}$$f_{1}arrow^{*}g_{1}$$g$:$A-arrow$$g=\sigma^{C}(g_{1_{)}g_{2})B}$.

3. Suppose that $A=A_{1}$ A

and that$A_{2}$$f=\pi(f_{1}):A_{1}$A $A_{2}-arrow B$ ,. Then by the induction hywhere: $A_{1}arrow B$ such that
$A_{1}-arrow
B$ such thatpothesis for , we have a proof term :. And so we obtain a proof term as follows
and$\partial(f_{1})=d$$f_{1}$$f_{1}$$\partial(g_{1})<d$$g_{1}$$f_{1}arrow^{*}g_{1}$$g$$g=\pi(g_{1}):A_{1}$4. Suppose that $A=A_{1}$ A: $A_{2}arrow B$ such that

$A_{2}$$f_{1}$

A $A_{2}arrow B$ .

and that $f=\pi’(f_{1})$ : $A_{1}\wedge A_{2}-arrow B$ , where. Same as the above case.

$\partial(f_{1})=d$

and that $f=\Pi(f_{1},f2):A-arrow B1$ A
5. Suppose that $B=B_{1}$ A
orwhere : $A-arrow B_{1}$ and : $Aarrow B_{2}$ such that
. Same as the above case.
$B_{2}$$f_{2}$$f_{1}$$\partial(f_{1})=d$$B_{2}$,$\partial(f_{2})=$$d$$\square$$\mathrm{C}$

Proof of Strong Normalization

are strongly normalizing, then $\pi(f),$ $\pi’(f)$ and
It is clear that if $f,$ and$\Pi(f1,f_{2})$ are. Below we implicitly use this fact.
$f_{2}$$f_{1}$

Proposition 21 Let
normalizing, then$f$

: $Aarrow C$ and $g:C-arrow B$ . If$\sigma^{C}(f,g)$

is strongly normalizing.

$f$

and

$g$

are strongly

217

Proof Let : $A-arrow C$ and $g:C-arrow B$ . Suppose that and are strongly
is strongly normalizing it is sufficient tonormalizing. To show thatshow that whenever $\sigma^{C}(f,g)arrow h,$ is strongly normalizing. Induction on$\nu(f)+\nu(g)$ , where $\nu(f)$ is a upper bound of length of every normalization
sequence beginning with .
$f$

$f$

$g$

$\sigma^{C}(f,g)$

$h$

$f$

1.

. Thenis a redex. Suppose that is theresult of the reduction. By induction on the degree of the composition. Notewe show that $h:Aarrow B$ is strongly
formulais a redex.
since
that
$\partial(f),$$\partial(g)<\partial(C)$$h$$\sigma^{C}(f,g)$$C$$\partial(f),$$\mathrm{n}\mathrm{o}\mathrm{r}\mathrm{m}\mathrm{a}\mathrm{J}\mathrm{i}_{\mathrm{Z}\mathrm{i}\mathrm{n}}\mathrm{g}$$\sigma^{C}(f,g)$$\partial(g)<\partial(C)$. By induction on the sum of the lengths(a) Suppose thatof and , we show that is strongly normalizing. Note thatcannot be of the form $\Pi(f1, f_{2})$ for some and , and also bothof and are normal forms since $\partial(f)=\partial(g)=0$ . And so there
are next five cases.
. $C=A$ and $f=1$ . Then $\sigma^{C}(f,g)=\sigma^{A}(1,g)$ , and so $h=g$ .
By assumption is strongly normalizing.
above case.
. $C=B$ ancl $g=1$ . Same as, and $f=\pi(f_{1})$ . Thenandfor some. $A=A_{1}$ A$C\in \mathcal{P}S$

$f$

$f$

$h$

$g$

$f_{2}$$f_{1}$$f$$g$$\mathrm{i}$$g$$\mathrm{t}\mathrm{l}\mathrm{l}\mathrm{e}$$\mathrm{i}\mathrm{i}$$A_{2}$$A_{1}$$A_{2}$$\mathrm{i}\mathrm{i}\mathrm{i}$$\sigma^{C}(f,g)=\sigma c(\pi(f_{1}),g)$and so$h=\pi(\sigma^{c_{(f1,g)}})$

Since is strongly normalizing,andhypothesis for
Therefore is.
andfor some. $A=A_{1}$ A
is same as the above case.
andfor some. $B=B_{1}$ A$f$$f_{1}$,.

is, and so by the induction
is strongly normalizing.

$f_{1}$$\sigma^{C}(f_{1},g)$

$g,$

$h$

$\mathrm{i}\mathrm{v}$$\mathrm{v}$, and $f=\pi’(f_{1})$ . This case

$A_{2}$$A_{1}$$A_{2}$$B_{2}$$B_{1}$$B_{2}$, and $g=\Pi(g_{1},g_{2})$ . Then$\sigma^{C}(f,g)=\sigma^{c}(f,\Pi(g1,g2))$,$h=\mathrm{I}\mathrm{I}(\sigma^{c}(f, g1),\sigma^{C}(f,g_{2}))$.

and soare, and so, by theandis strongly normalizing,
induction hypotheses for and and for andare strongly normalizing. Therefore is.
and

Since

$g_{1}$$g$$f$$\sigma^{C}(f,g_{2})$$g_{1}$$g_{2}$$f$$g_{2},$$\sigma^{C}(f, g_{1})$

$h$

218

(b) $C=C_{1}\wedge C_{2}$ for someand . Note that.
By induction on the sum of the lengths of and we show thatis strongly normalizing. We consider the next four cases sinceother cases are same as the base step.
$C_{1}$$\partial(f),\partial(g)<\partial(C)$$C_{2}$

$f$

$g$

)

$h$

$\mathrm{i}$.

$f=\sigma^{D}(f_{1},f_{2})$for some $D,$$f_{1}$

and$f_{2}$. Then$\sigma(cf,g)=\sigma(c\sigma D(f1, f2),g)$and so$h=\sigma^{D}(f1,$ $\sigma^{c_{(f_{2},g))}}$,.

Since is strongly normalizing, is, and so, by the induction
hypothesis forandis strongly normalizing.
Note thatis strongly normalizing since is, andsince. Therefore, by the induction hypothesis for $D,$ is.
.
for some $D,$and . Same as the abovecase.
. $f=\Pi(f_{1}.’ f_{2})$ for some and , and $g=\pi(g_{1})$ for some .
Then
$f$

$f_{2}$$f_{2}$$g,$$\sigma^{C}(f_{2},g)$$\partial(C)$$\partial(D)<$$f$$f_{1}$$\partial(f)<\partial(C)$$h$$\mathrm{i}\mathrm{i}$$\mathrm{i}\mathrm{i}\mathrm{i}$$g=\sigma^{D}(g_{1}, g_{2})$$g_{1}$$f_{1}$$g_{2}$$f_{2}$$g_{1}$$\sigma(Cf,g)=\sigma C_{1}\wedge c2(\Pi(f1,f_{2}),\pi(g1))$and so$h=\sigma^{C_{1}}(f1,g_{1})$.

, and that
Note thatandare strongly
normalizing since and are. And so, by the induction
hypothesis foris strongly normalizing.
. $f=\Pi(f_{1},f_{2})$ , for some and , and $g=\pi’(g_{1})$ for some
. Same as the above case.
$\partial(C_{1})<\partial(C)$$f$$C_{1},$$\mathrm{i}\mathrm{v}$,$f_{1}$$g_{1}$$g$$h$$f_{1}$$f_{2}$$g_{1}$

2. $farrow f’$ . Then $\sigma^{C}(f,g)arrow\sigma^{C}(f’,g)$ . Note that $f’$ is strongly normalizing since is. And so, by the induction hypothesis for $f’$ and ,is strongly normalizing.
$f$$\sigma^{C},(f’, g)$

3. $garrow g’$ . This case is same as the above.
$\square$

$g$

219

Proof of Theorem 17 Let : $Aarrow B$ be an arbitrary term. By the
induction on , we show that is strongly normalizing.
$f$

$f$

$f$

1. $A=B$ and $f=1$ . Then clearly$f$is strongly normalizing.

and . Then by the induction
and
2. $f=\sigma^{C}(f_{1}, f_{2})$ for somehypotheses forand , they are strongly normalizing. Hence isby the above proposition.
$C$$f_{2}$$f_{1}$$f$$f_{2}$$f_{1}$

3. $f=\pi(f_{1})$ for some . Then, by the induction hypothesis forstrongly normalizing, and so is.
$f_{1}$$f_{1}$, it is$f$

4. $f=\pi’(f_{1})$ for some$f_{1}$. Same as above case.

and . Then, by the induction hypotheses
5. $f=\Pi(f_{1}, f_{2})$ for someand , they are strongly normalizing, and so is.
for$f_{1}$$f_{1}$$f_{2}$$f$$f_{2}$$\square$

Proof of Local Confluence$\mathrm{D}$For : $A-arrow C$ and $g:Carrow B$ , we introduce a notation. Below we implicitly use Theorem 17.
stands for$f$$f\triangleright^{C}g$

which$\sigma^{C}(f,g)$Lemma 22 Let : $A-arrow B,$ $g:Barrow C$ and $h:C-arrow D$ , where $\partial(B)=$and, be normal forms. And let $m$ and be normal forms of$k:Aarrow
D$
that
such
respectively. Then there exists a term
.
and
$f$

$f\triangleright^{B}g$$n$$\partial(C)$$m\triangleright^{C}harrow^{*}$$g\triangleright^{C}h$$k$$f\triangleright^{B}narrow^{*}k$

We can prove this leInma by induction on the sum of lengths $f,$
Proof of Proposition 19 Let $f,$$farrow k$ . Then we need to show that there exists. We check t.hc critical situations.
and$h,$ $k\in \mathcal{T}_{Aarrow B}$$karrow^{*}g$

$g$

and

$h$

.

. Assume that $farrow h$ and$g\in \mathcal{T}_{Aarrow B}$

such that$harrow^{*}g$$.\mathrm{a}11$. Since $\partial(1)=0<\partial(A)$ , we have
1. Suppose that $B=A$ and$farrow_{1}h$ and $farrow_{2}k$ , where $h=k=1$ . We set $g=1$ .
$f=1\triangleright^{A}1$

2. Suppose that
$f=1\triangleright^{A}(f_{1^{\triangleright}’}.Df_{2})$220

for some : $Aarrow D$ and : $Darrow B$ such that
Then $farrow_{1}h$ and $farrow_{4}k$ , where$f_{2}$$f_{1}$

and$h=f_{1}\triangleright^{D}f_{2}$But since$\partial(f_{1})<\partial(A)$$g=h$ .

3. Suppose that $B=B_{1}$ A

we have$B_{2}$$\partial(f_{1}\triangleright^{D}f_{2})<\partial(A)$$k=(1\triangleright^{A}f_{1})\triangleright^{D}f_{2}$$1\triangleright^{A}f_{1}arrow 1f_{1}$.

.

, and so $karrow h$ . We set

and$f=1\triangleright^{A}\Pi(f_{1}, f_{2})$for some: $A-arrow B_{1}$ and: $A-arrow B2$ such that$farrow_{8}k$$farrow_{1}h$. Thenandwhere$f_{1}$$f_{2}$$\partial(\mathrm{I}\mathrm{I}(f_{1}, f_{2}))<$$\partial(A)$and$h=\mathrm{n}(f_{1}, f_{2})$But sinceso

4.

$\mathrm{S}$$\partial(f_{1}))\partial(f2)<\partial(A)$$karrow+_{h}$. We set $g=h$ .

$k=\Pi(1\triangleright^{A}f_{1},1\triangleright^{A}f_{2})$we have$1\triangleright^{A}f_{i}arrow 1f_{i}$upp ose that$f=(f_{1^{\triangleright^{D}}}f2)\triangleright 1B$for some
Then .
$f$$f_{1}$: $A-arrow D$ and$arrow_{2}h$$f_{2}$$g=h$

for $i=1,2$ , and.

: $D-arrow B$ such that$\partial(f_{1}\triangleright^{D}f_{2})<\partial(B)$.

and $farrow_{3}k$ whereand$h=f_{1}\triangleright^{D}f_{2}$But since.

$\partial(f_{2})<\partial(B)$.

5. Suppose that $A=A_{1}$ A

we have$A_{2}$$k=f_{1}\triangleright^{D}(f_{2}\triangleright^{B}1)$$f_{2}\triangleright^{B}1arrow 2f_{2}$.

, and so $karrow h$ . We set

and$f=\pi(f_{1}\rangle\triangleright^{B}1$

for some: $A_{1}arrow B$ such that$farrow_{6}k$ where$f_{1}$$h=\pi(f_{1})$But since$g=h$ .

$\partial(f_{1})<\partial(B)$$\partial(\pi(f_{1}))<\partial(B)$and, we have. Then $farrow 2h$ and$k=\pi(f_{1}\triangleright^{B}1)$$f_{1}\triangleright^{B}1arrow_{2}f_{1}$.

and so $karrow h$ . We set

221

for some
and$\partial(\pi’(f1))<\partial(B)$ . Same as the above case.

6. Suppose that $A=A_{1}$ A
such that
7.

$\mathrm{S}$$f=\pi’(f_{1})\triangleright^{B}1$$A_{2}$

upp ose that$f=(f_{1}\triangleright^{D}f_{2})\triangleright c_{(}f_{3^{\triangleright}}Ef_{4})$for somesuch thatwhere$f_{1}$: $Aarrow D,$$\partial(f_{1}\triangleright^{D}f_{2}),$$f_{2}$: $Darrow C,$$f_{3}$$f_{4}$$\partial(f3\triangleright^{E}f_{4})<\partial(B)$,$k=((f1\triangleright^{Dc}f2)\triangleright f_{3})\triangleright fE4$$h$$\partial(f_{1}.),$$arrow$$\partial(D),$,: $Earrow B$: $C-arrow E$ , and. Then $f\sim_{3}h$ and $f\sim_{4}k$$h=f1^{\triangleright^{D}(f2}\triangleright^{c_{(}E}f_{3}\triangleright f4))$

But since: $A_{2}arrow B$$f_{1}$$\partial(E)<\partial(C)$.

we have$f_{1}\triangleright^{D}((f2^{\triangleright}fc)3\triangleright f_{4})E$$arrow^{*}$$n_{1}\triangleright^{D}(n_{2}\triangleright^{E}n3)=h’$,$(f_{1}\triangleright^{D}(f_{2^{\triangleright^{C}}}f3))\triangleright^{E}f4$$arrow^{*}$$(n_{1^{\triangleright^{D}n_{2})=}}\triangleright n_{3}k’E$

,

and
$k$

$arrow$

are normal forms of
and
where
tively. There are three cases.
$n_{1},$..

$f_{1},$$n_{3}$$n_{2}$$f_{2}\triangleright^{C}f_{3}$and$f_{4}$

respec-, thereby we set $g=k’$ .
. Then we have $h’arrow k’$ , thereby we set $g=h’$ .
and$\partial(D)=\partial(E)$ .
Let and be normal forms ofexistslemma,
there
respectively. Then, by the above$harrow^{*}r$ and
.
so
And
and
such that. Thereby we set $g=r$ .
$\partial(D)<\partial(E)$. Then we have$k’arrow h’$$\partial(E)<\partial(D)$$n_{2}\triangleright^{E}n_{3}$$\bullet$

$p$

$q$

$r$

$n_{1}\triangleright^{D}n_{2}$$n_{1}\triangleright^{D}parrow^{*}r$$q\triangleright^{E}n_{3}arrow^{*}r$$karrow^{*}r$8.

.pose that$\mathrm{S}\mathrm{u}\mathrm{p}$$B=B_{1}$ A $B_{2}$and$f=(f_{1^{\triangleright}}Df2)\triangleright^{C_{\Pi}}(f3, f_{4})$for somesuch thatwhere$f_{1}$,: $A-arrow D,$ $f2:D-arrow c,$ $f3:c-arrow B_{1}$ , and$\partial(f_{1}\triangleright^{D}f_{2}),$$\partial(\Pi(f_{3}, f_{4}))<\partial(B)$. Then$f_{4}$$farrow_{3}\mathit{1}\iota$

,

$h$

$=$

$f_{1}\triangleright^{D}(f_{2}\triangleright\Pi C(f_{3,f4}))$

$k$

$=$

$\Pi((f_{1^{\triangleright^{D}}}f_{2})\triangleright^{C}f3, (f_{1}\triangleright^{D}f2)\triangleright^{c}f4)$: $C-arrow B_{2}$and $farrow_{8}k$222

But since$h$we have$\partial(D)<\partial(C)$$\partial(f_{i}),$$arrow$$f_{1} \triangleright^{D}\prod(f_{2}\triangleright^{G}f_{3}, f_{2^{\triangleright}}Cf_{4})arrow^{*}f_{1}\triangleright^{D}\prod(n_{1}, n_{2})$$arrow$$\prod(f_{1}\triangleright^{D}n_{1}, f_{1^{\triangleright^{D}n}2})$$k$$arrow$,$\prod(f_{1}\triangleright^{B_{1}}(f_{2}\triangleright^{C}f_{3}), f_{1}\triangleright^{B_{2}}(f_{2}\triangleright^{C}f_{4}))arrow^{*}\prod(f_{1}\triangleright^{D}n_{1}, f_{1}\triangleright^{D}n_{2})$are normal forms of
where and
Thereby we set$n_{2}$$n_{1}$$f_{2}\triangleright^{C}f_{3}$$g=\Pi(f_{1}\triangleright^{D}n_{1},f_{1}\triangleright^{D}n_{2})$9. Suppose that $A=A_{1}$ A$A_{2}$.

and$f_{2}\triangleright^{C}f_{4}$respectively.

and$f=\pi(f_{1})\triangleright(cf2\triangleright^{D}f_{3})$for some: $A_{1}arrow C,$$f_{1}$$f_{2}$: $Carrow D$ and : $Darrow B$ such that
. Then $farrow_{4}h$ and $farrow_{6}k$ , where$f_{3}$$\partial(\pi(f_{1})),$ $\partial(f_{2}\triangleright^{D}f_{3})<\partial(B)$But since

$h$

$=$

$(\pi(f_{1})\triangleright f_{2}c)\triangleright^{D}f3$

,

$k$

$=$

$\pi(f_{1^{\triangleright^{C}}}(f_{2^{\triangleright}}Df_{3}))$.

$h$$arrow$$\pi(f_{1^{\triangleright^{C}}}f2)\triangleright fD3arrow\pi((f_{1}\triangleright^{cD}f2)\triangleright f_{3})$$k$$arrow$$\pi((f_{1}\triangleright^{cD}f2)\triangleright f_{3})$Thereby we set:$A_{2^{-}}arrow C,$$f_{2}$,.

$g=\pi((f_{1}\triangleright^{C}f_{2})\triangleright^{D}f_{3})$.

and: $c–D$ and : $Darrow B$ such that
. Same as the above case.

10. Suppose that $A=A_{1}$ A$f_{1}$

we have$\partial(D)<\partial(B)$$\partial(f_{1}),$$f=\pi’(f_{1})\triangleright^{C}(f_{2}\triangleright^{D}f_{3})$$A_{2}$

for some$f_{3}$$\partial(\pi(f_{1})),$ $\partial(f_{2}\triangleright^{D}f_{3})<\partial(B)$

11. Suppose that $A=A_{1}$ A $A_{2)}B=B_{1}$ A$B_{2}$

and$f=\pi(f_{1})\triangleright^{C}(\Pi(f_{2},f_{3}))$: $A_{1}arrow c,$: $Carrow B_{1}$ andfor some$f_{1}$$\partial(\pi(\prime f_{1})),$$\partial(\Pi(f2,f_{3}))<\partial(B)$$f_{2}$$f_{3}$.

: $Carrow B_{2}$ such that

Then $farrow_{6}h$ and $farrow_{8}k$ , where

,

$h$

$=$

$\pi(f_{1^{\triangleright^{C}\Pi}}(f2, f_{3}))$

$k$

$=$

$\Pi(\pi(f_{1})\triangleright^{c}f2, \pi(f1)\triangleright^{C}f3)$

.

,

223

But since$\partial(f_{1}),$$\partial(f2),\partial(f3)<\partial(B)$we have,$h$$arrow$$\pi(\Pi(f_{1^{\triangleright^{c}}}f2,f_{1^{\triangleright}}Cf_{3}))=h’$$k$$arrow$$\Pi(\pi(f_{1^{\triangleright}f_{2}}c),\pi(f_{1^{\triangleright}}Cf3))=k’$.

Thereby we set $g=h’=\Pi k’$ .

12. Suppose that $A=A_{1}$ A$A_{2},$$B=B_{1}$A$B_{2}$

and$f=\pi’(f1)\triangleright\Pi c(f_{2},f_{3})$for some$f_{1}$: $A_{2}arrow C,$$f_{2}$: $c-arrow B_{1}$ and. Then$\partial(\pi’(f1)),$ $\partial(\Pi(f_{2},f_{3}))<\partial(B)$$farrow\tau^{h}$: $Carrow B_{2}$ such thatand $farrow_{8}k$ , where

,

$h$

$=$

$\pi’(f1^{\triangleright}c_{\Pi}(f2, f_{3}))$

$k$

$=$

$\Pi(\pi’(f1)\triangleright fC2, \pi’(f1)\triangleright^{c_{f3}})$This case is same as the above case.
$\square$$f_{3}$.