Strong normalizability of the non-deterministic catch/throw calculi.
The catch/throw mechanism in Common Lisp provides a simple control mechanism for non-local exits. We study typed calculi by Nakano and Sato which formalize the catch/throw mechanism. These calculi correspond to classical logic through the Curry-Howard isomorphism, and one of their characteristic points is that they have non-deterministic reduction rules. These calculi can represent various computational meaning of classical proofs. This paper is mainly concerned with the strong normalizability of these calculi. Namely, we prove the strong normalizability of these calculi, which was an open problem. We first formulate a non-deterministic variant of Parigot's -calculus, and show it is strongly normalizing. We then translate the catch/throw calculi to this variant. Since the translation preserves typing and reduction, we obtain the strong normalization of the catch/throw calculi. We also briefly consider second-order extension of the catch/throw calculi. Copyright 2002 Elsevier Science B.V
Introduction
The catch and throw mechanism provides a means to implement non-local exits. The
following simple example written in Common Lisp [19] shows how to use the catch and
throw mechanism:
(defun multiply (x)
(catch 'zero (multiply2 x)))
(defun multiply2 (x)
(if (null x) 1
(if (= (car x)
(* (car x) (multiply2 (cdr x))))))
The rst function multiply sets up the catch-point with the tag zero, and immediately
calls the second function. The second one multiply2 performs the actual computation by
recursion. Given a list of integers, it calculates the multiplication of the members in the
list. If 0 is found in the list, then the result must be 0 without computing any further, so
it returns 0 by the throw-expression. The catch/throw mechanism is useful if one wants
to escape from nested function calls at a time, especially in run-time errors.
Nakano [11{14] proposed calculi with inference rules which give logical interpretations
of the catch/throw constructs in Lisp. His calculi dier from the actual catch/throw-
constructs in Common Lisp in the following two ways.
(1) He changed the scope rule of the catch-construct from a dynamic one to a lexical
one. In the above example, the expression (throw 'zero 0) is not lexically in the scope
of the corresponding catch-expression, which indicates that the catch-expression has
dynamic scope in Common Lisp. 1 In Nakano's calculi, tags are variables rather than
constants, and the correspondence between throw and catch is represented as the ordinary
variable binding mechanism, in which the scope of binders is lexical.
(2) He introduced the tag-abstraction and tag-application mechanisms which do not
exist in Common Lisp. 2 The motivation of this was to recover the expressivity which was
lost by changing the scope rule of the catch-construct.
Let us see how the above example can be written in Nakano's style:
(defun multiply (x)
(catch 'zero (multiply2 x 'zero)))
(defun multiply2 (x u)
(if (null x) 1
(if (= (car x) (throw u
(* (car x) (multiply2 (cdr x) u)))))
In this modied program, the catch-construct has lexical scope so that the scope of
the tag zero is (multiply2 x 'zero) only. To throw an object from another function
multiply2, the function is abstracted by the tag variable u. When using the function
multiply2 we must provide the tag zero as the second parameter.
Nakano also introduced a new type constructor  (called \otherwise") for the tag
abstraction mechanism; if a is a term of type A, and u is a tag-variable of type B, then
the abstraction of a by u has type A B.
The characteristic points in Nakano's formulation were (1) L c=t has restriction (side-
condition) in the implication-introduction rule, and it excludes terms which corresponds
to classical proofs. Actually L c=t corresponds to an intuitionistic calculus through the
Curry-Howard isomorphism. (2) L c=t allows as many reductions as possible, hence it is
non-deterministic (not con
uent). These two features may look strange, since classical
logic is said to be essentially non-con
uent, while intuitionistic logic is con
uent. 3 We
consider that the classical version of L c=t , which is obtained by removing the restriction, is
a more natural calculus, and is suitable for extracting algorithmic meaning from classical
proofs. We call L K
c=t as the classical version of L c=t .
1 Similarly the exception mechanism in the Standard ML has dynamic scope.
2 The exception mechanism in the Standard ML has abstraction/application.
3 We refer to Girard [6] and Parigot [15] for the discussion on the con
uence and the classical logic.
A few years later than Nakano, the second author (Sato) proposed another formulation
for the catch/throw mechanism [17]. His motivation was to eliminate the type of the
tag abstraction (\otherwise") in L c=t , since it is equivalent to disjunction. By unifying
the throw-expression and the tag-abstraction mechanism, he obtained a simpler calculus
NJ c=t . He also showed that L c=t can be interpreted in NJ c=t . NJ c=t has essentially the
same restriction in the implication-introduction rule, hence it corresponds to intuitionistic
logic. He also dened NK c=t by throwing away the restriction, and showed that it corresponds
to classical logic. In summary, there are proposed four calculi for the catch/throw
mechanism:
Author Intuitionistic Logic Classical Logic
Nakano L c=t L K
c=t
Sato NJ c=t NK c=t
In this paper, we investigate the strong normalizability (SN) of the above four calculi,
in particular, L K
c=t and NK c=t . The SN of L c=t was proved by Nakano [14], but his proof
was based on complex model-theoretic arguments. In our previous works, we proved the
SN of NJ c=t in [8], and the SN of a large fragment of L K
c=t in [9], but the SN of the full
fragments of classical calculi L K
c=t and NK c=t was an open problem. This paper solves this
problem in an armative way.
We rst formulate a non-deterministic variant of Parigot's -calculus by adding several
reduction rules, and prove its strong normalizability using the reducibility method. We
then translate the catch/throw calculi to this variant. Since this translation preserves
typing as well as reduction, we obtain a proof of the strong normalizability of all the four
calculi. We nally brie
y discuss second-order extension of them.
2. The Catch/Throw Calculi
2.1. Nakano's Formulation
Nakano proposed several calculi for the catch/throw mechanism. Among them, L c=t
given in [14] is the strongest one. In this paper we also study L K
c=t , an extension of
L c=t . Although Nakano himself did not present L K
c=t in published papers, the latter can be
obtained from L c=t by simply throwing away the restriction in the implication introduction
rule, therefore we regard L K
c=t as one of Nakano's calculi.
In the following, we shall dene L K
c=t and mention the dierence of L K
c=t and L c=t .
We assume that there are nitely many atomic types (we use K as a metavariable for
atomic including ? (falsity).
Denition 2.1 (Type)
In this denition, !, ^, _ are the types for the function space, product, and sum. By the
Curry-Howard isomorphism, we may identify them with logical connectives implication,
conjunction, and disjunction. The connective  was introduced to give a type to tag
abstraction. As usual, we abbreviate A !? as :A.
We assume that, for each type A, there are innitely many individual variables x A of
type A and innitely many tag variables u A of type A. We use x A ; y A ; z A for individual
variables and u A ; v A ; w A for tag variables. We regard u A and u B as dierent tag variables
if A 6 B. This implies that we may sometimes use the same variable-name for dierent
entities (dierent types).
Preterms of L c=t and L K
c=t are dened as follows.
Denition 2.2 (Preterm)
Among the preterms above, the constructs catch, throw, , and tapp were introduced
by Nakano to represent the catch and throw mechanism. We refer to the following table
for the correspondence to similar constructs in Common Lisp and Standard ML.
c=t Common Lisp Standard ML
As noted in the introduction, tags in Common Lisp (exception names in Standard ML) are
represented as tag-variables rather than constants. The preterm u:t is the tag-abstraction
mechanism like the -abstraction x:t, and the preterm tapp(t; u) is the tag-application
mechanism 4 like the functional application apply(t; u).
We sometimes omit the types in variables. We also write apply(a; b) as ab. An individual
variable is bound by the -construct and the case-construct, and a tag variable
is bound by the catch-construct and the -construct. We identify two terms which are
equivalent under renaming of bound individual/tag variables. FV(t) and FTV(t) denote
the set of free individual variables and the set of free tag variables in t, respectively.
The type inference rules are given in the natural deduction style, and listed in Table 1.
The inference rules are used to derive a judgment of the form ' a : A ;  where
is a nite set in the form fx g, and  is a nite set in the form
g. In both sets we understand each variable appears only once. is
a context of individual variables, and  is a context of tag variables.
In L c=t , the implication-introduction rule (marked (*)) has a restriction on free tag variables
in b. L K
c=t has no restriction. In the intuitionistic calculus L c=t , a preterm x A :b is
well-typed only when x A does not essentially occur in the scope of any throw-construct
in b. One of Nakano's main results was that, this restriction neatly corresponds to intuitionistic
propositional calculus through the Curry-Howard isomorphism. The actual
Actually, Nakano did not use the word tapp. Rather, he simply wrote tu for tapp(t; u). In this paper,
we use dierent function symbols for dierent term-construction to clarify the syntax.
Table
Type Inference Rules of L c=t and L K
c=t
' a :? ;
restriction is complex due to the existence of the case-construct. In this paper we do not
give the precise denition of \essential occurrence". We refer to [11] and [14] for details.
Among the inference rules, the rst ten are standard. The rules for throw and catch
re
ect their intended semantics, namely, aborts the current context so that
this term can be any type regardless of the type of b, and the type of catch(u
a) is the
same as a and also the same as the type of possibly thrown terms. The term u B :a is
tag-abstraction, and it is assigned a new type A  B. Conversely, if a is of type A  B,
then applying a tag variable u B to it generates a term of type A.
An example of the type inference is as follows (which corresponds to the double negation
Ag. The above one is
a type inference gure in L K
c=t , but not in L c=t . This is because, in the formation of
x A :throw(u A ; x A ), the abstracted variable x A occurs free in throw(u
does not t into Nakano's restriction.
Let a; b; c;    be metavariables for terms. If ' a : A ;  is derived by the inference
rules, we say a is a term of type A under contexts and .
One-step reduction rules of L c=t and L K
c=t are given by Table 2.

Table
One-Step Reduction Rules of L c=t and L K
c=t
a 6 x and x 2 FV (a))
In this denition, C[ ] represents a context with a hole [ dened as usual. Also substitution
a[b=x] and a[v=u] are dened as usual.
As an instance, we have the following reductions:
tapp((v:(throw(v;
Instead of having a one-step reduction like catch(u; a[throw(u; b)=x]) ; 1 b, the catch/throw
mechanism splits into two steps as follows:
Since we did not restrict any evaluation strategy, the reduction in L K
c=t is non-deterministic,
moreover it is not con
uent. For instance, we have the following reduction sequences where
we put t  catch(u
We dene a ; b (zero or more step reduction), and a ;+ b (one or more step reduction)
as usual.
Theorem 2.1 (Nakano)
The subject reduction property holds for L c=t and L K
c=t .
2.2. Sato's Formulation
In [17], Sato proposed another formulation of the catch/throw mechanism. His primary
motivation was to get rid of the logical connective  from L K
c=t , yet to obtain a system
which is as powerful as L K
c=t . From the logical point of view,  is redundant, since it is
equivalent to disjunction. Sato successfully eliminated  from the calculus by unifying
the two binders of tag variables, catch and .
We shall give the denition of NK c=t in the following. NJ c=t is obtained from NK c=t by
restricting the !-introduction rule in the same way as L c=t from L K
c=t . Types are those of
L c=t with  deleted. Preterms are dened as follows.
Denition 2.3 (Preterm)
Individual variables are bound by the - and the case-constructs, and tag variables are
bound by the ?-constructs. The ?-construct replaces catch and  in L c=t , the !-construct
replaces throw in L c=t , and the tapply-construct replaces tapp in L c=t .
The type inference rules for the new constructs are given by Table 3.

Table
Type Inference Rules of NJ c=t and NK c=t
The inference rule for the !-construct is the same as that of throw in L c=t . The term ?u
may be constructed even if the type of a diers from B. The meaning of ?u B :a is that,
if the computation of a ends normally and returns a 0 , then it returns inj 1
(a 0 ), and if a
term b is thrown during the computation of a, then it returns inj 2
(b). Hence ?u B :a has
type A _ B if a is of type A. The tapply-construct may be dicult to understand, but
it is an inverse operation of tag abstraction. So tapply(?u B reduces to a[v B =u B ].
Type inference rules of other constructs are the same as before. The calculus with
the restriction in the implication introduction rule is called NJ c=t , and the one without
the restriction is NK c=t . The former corresponds to intuitionistic logic and the latter to
classical logic.
One-step reduction rules for the new constructs are given as follows:
(a) (if u 62 FTV(a))
The last reduction may look strange, but it is useful in writing concise proofs [17], and
necessary to simulate the reduction tapp(v:a; u) ; 1 a[u=v] in L c=t /L K
c=t .
Theorem 2.2 (Sato)
The subject reduction property holds for NJ c=t and NK c=t .
2.3. Non-determinism and Classical Logic
All the four calculi for the catch/throw mechanism have non-deterministic reduction
rules, and are not con
uent. We do not think that this is defect because: (1) as far
as the strong normalizability is concerned, it is good to have as many reduction rules
as possible. As a corollary of the strong normalizability of the strongest calculus, we
obtain the strong normalizability of any subcalculus, and (2) classical logic is said to be
inherently non-deterministic. In order to express all possible computations in classical
proofs, our calculus should be non-deterministic. Later we can choose one answer by
xing an evaluation strategy. Murthy gave examples which show classical proofs may
contain multiple computational meanings [10]. The second author showed in [18] that
Murthy's example can be expressed in in the NK c=t -style calculus.
3. A Non-deterministic Variant of Parigot's
In this section, we give a non-deterministic variant of Parigot's  as a target of translation
from the catch/throw calculi.
Parigot's -calculus [16] is a second-order propositional calculus for classical logic. It
is a natural-deduction system whose sequents have multiple consequents. The -calculus
is a quite nice formulation of classical logic, and at the same time, it is computationally
interesting, since various control structures can be represented by the -construct whose
typing is given as follows:
The most important reduction rule for the -construct (called structural reduction) is:
where af[]c := [](cb)g is the term obtained from a by substituting [](cb) for every
subterm in the form []c where this  is free in a. We refer to [16] for the denition of
the -calculus.
We can simulate a simplied version of the catch/throw mechanism in L K
c=t by the -
construct as follows:
catch(u; a) as u:[u]a
throw(u; a) as v:[u]a (where v does not appear in [u]a)
However, the catch/throw calculi we consider are not con
uent. Moreover, one term
reduces to dierent variables x A and y A as we saw in the previous section. Since the
calculus is a con
uent calculus, direct simulation of the catch/throw calculi by  is not
possible.
A possible solution is to add more reductions to , for instance, the call-by-value
version of the structural reduction (the symmetric structural reduction). However, it is
not known that a system which has both the structural reduction and the symmetric
structural reduction is strongly normalizing or not 5 . Instead of naively adding reduction
rules, we slightly modify the -calculus, then add non-deterministic reductions. Namely,
we classify uses of  into three cases:
(1) u:[u]a
(2) u:[v]a with u 62 FTV([v]a)
(3) u:[v]a with u 6 v and u 2 FTV(a)
We need (1) and (2) to simulate the catch-construct and the throw-construct, respec-
tively. We only need to extend the reduction rules for (2), and the reduction rules for (1)
remain the same. We do not need (3) to simulate the catch/throw calculi, so such a term
construction will be excluded.
Another modication to the -calculus is that we no longer have distinction of individual
variables and tag variables. The named term [u]a will be represented by ordinary
application ua. By this modication, we can directly -abstract over variables which
correspond to names such as []. This is the key to simulate the tag-abstraction/tag-
application mechanism in L K
c=t . This representation is essentially due to de Groote [3],
who formalized the exception mechanism for ML. Fujita [4] recently studied a similar
calculus for the exception mechanism.
As notational convenience, we write u:a for the term u:[u]a, and abort(va) for
the term u:[v]a. We also extend reduction rules for the abort-construct to have non-deterministic
features. We call the resulting system  ND .
3.1. A Non-deterministic Calculus  ND
The types of  ND are dened as follows:
Denition 3.1 (Type)
Recently, Fujita[5] indicated that such a system is shown to be strongly normalizing by translating it to
Barbanera and Berardi's symmetric -calculus if we restrict the system to rst-order. However, we need
the second-order version in this paper.
Since  ND is second-order, the type ? is redundant from the logical point of view. We,
however, include ? as a primitive type, since we want to interpret ? dierently from
8X:X. The type variable X is bound by the type abstraction 8X, and we identify two
types which are identical modulo renaming of bound type variables. We abbreviate A !?
as :A.
The preterms are as follows. Note that we adopt the Curry-style (implicit typing) for
ND as in the -calculus. 6 Hence we do not attach types to variables, and consider
reduction rules.
Denition 3.2 (Preterm)
Contrary to the original , we have only one sort of variables. A variable x may be used
for an ordinary variable and also for a name (a tag-variable in our sense). Also we have
no distinction between ordinary terms and named terms. Variables are bound by  and
constructs, and we again identify two terms which diers only in the bound variables.
The preterm abort(t) is new to  ND as we explained above.
A judgment in  ND is in the form ' a : A where is a nite set in the form
g. The type inference rules which derive judgments are shown in

Table

Table
Type Inference Rules of  ND
' a :?
In the 8-introduction rule (marked (*)), X may not occur freely in .
If ' a : A is derived using the above rules, we say a is a (typable) term of type A
(sometimes written as a : A).
The reduction rules are derived from the -calculus, but we added several rules for
abort which makes  ND non-deterministic. Since we shall use the substitution in the
6 In [16], Parigot also denes a Church-style system.
Table
One-Step Reduction Rules of  ND
form [x:u(xb)=u] many times, it is abbreviated as [b=  u]. When using this notation, we
always assume that x is a fresh variable. We also abbreviate composition of substitutions
We often write  b for the sequence hb 1 ;    ; b n i. Hence
successive application (   (ab 1 )    b n ) is abbreviated as a  b and successive substitution
In the last case we assume that b 1 ;    ; b n do not contain u
free. We also use simultaneous substitution [b 1 =x
um are mutually distinct and c do not contain u
As before, we use the notation a ; b and a ;+ b.
The following lemma can be proved easily.
Lemma 3.1
Let  be the substitution [b 1 =x
um ]. If a ; b, then a ; b.
3.2. Strong Normalizability of  ND
In this subsection, we prove the strong normalizability (SN) of  ND . The proof is a
slight modication of Parigot's original proof of the SN of . Nevertheless, we give the
proof here for completeness.
Let T be the set of preterms in  ND , and SN be the set of strongly normalizing
preterms in  ND . Note that we do not restrict T and  ND be subsets of typable terms,
following [16]. (a) is the maximum length of reduction sequences starting from a if
a 2 SN , and is undened if a 62 SN .
For F  T , let F <! be the set of nite sequences of elements of F . Namely,
In particular, F <! contains the empty sequence hi.
Let F and G be subsets of T , and S be a subset of T <! . Then we introduce the
following notations:
As a special case, we have G.
Denition 3.3 (Reducibility Candidate)
A reducibility candidate is a subset of T , and is inductively dened as follows:
1. SN is a reducibility candidate.
2. If F and G are reducibility candidates, so is F ! G.
3. If fF i g i2I is a family of reducibility candidates for a non-empty set I, then
is a reducibility candidate. (Note that the index set I may be innite.)
The set of the reducibility candidates is denoted as RC.
Lemma 3.2
For any F 2 RC, the following four clauses hold.
1. F  SN .
2. All variables are contained in F .
3. If a 2 SN , then abort(a) 2 F .
4. There exists a set S such that S  SN <! and
The clause 3 was added from Parigot's original proof. It means that abort(a) with
a strongly normalizing term a is contained in any reducibility candidate. The main
dierence of our proof and Parigot's is that, in our case, a term in the form C[abort(a)]
may reduce to abort(a), so we should always consider abort(a) as a reduct. However
such a term is contained in any reducibility candidate if a is strongly normalizing by this
lemma, and therefore we can always handle this term easily.
Proof. We prove all the four clauses simultaneously by induction on \F 2 RC".
(Case: F is SN ) Clause 4 is proved by taking fhig as S, and other clauses are trivial.
(Case: F is G induction hypothesis (abbreviated as IH),
we have x proves Clause 1.
By IH, G  SN , and there exists a set S 0  SN <! such that
by taking
G;
we have G which proves Clause 4.
Let x be a variable, a 2 SN , b
since all its reducts are in the form xb 0
n or abort(d)bk+1    b 0
proving Clause 2. We
also have abort(a)b proving Clause 3.
(Case: F is T
are easily proved from IH. Also by IH, for each
I there is an S i  SN <! such that G
then we have
which proves Clause 4. ut
From Clause 4 in the above lemma, we put F ? as the largest such S. Namely, for any
A preterm a is neutral if it is either a variable or in the form bc.
Lemma 3.3
For any F 2 RC, the following two clauses hold.
1. For any a 2 F , if a ; 1 a 0 then a 0 2 F .
2. If a is neutral, and a 0 2 F for any a 0 such that a ; 1 a 0 , then a 2 F .
Proof. This lemma is proved by induction on \F 2 RC". The key case is F  G ! H.
We shall prove Clause 2 only. Suppose a is neutral, and a 0 2 G ! H for any a 0 such
that a ; 1 a 0 . Take an arbitrary preterm b 2 G. We shall prove ab 2 H by induction on
(a) (b) (since a and b are SN). The preterm ab reduces in one step to either one of
a 0 b (with a ; 1 a 0 ), ab (with a  a 00 [abort(c)=x]), or abort(d)
(with b  b 00 [abort(d)=x]). We can easily prove that all the four terms belong to H, and
by IH, we have ab 2 H. Consequently a 2 G ! H. ut
Denition 3.4 (Interpretation of Types)
An interpretation  is a map from type variables to reducibility candidates.
Note that there exists an interpretation which maps all the type variables to SN .
An interpretation is naturally extended to any types in the following way:
where an interpretation [F=X] is dened as
for Y 6= X.
Lemma 3.4
Let A; B be types, and  be an interpretation. Then
This lemma can be proved by induction on the structure of A.
Lemma 3.5
Let F 2 RC, x; u be variables, a; b be terms, and  c be a sequence of terms.
1. If a[b=x] 2 F and b is SN, then (x:a)b 2 F .
2. If (u: (a[d=  u])d)c 2 SN and c
3. If  c
4. If a 2 SN , then u: a 2 SN .
Proof. 1. We can prove this clause by induction on (a[b=x]) + (b) using Lemma
3.1 and Lemma 3.3. We must take care that the reducts of (x:a)b may be of the form
abort(c), but this case can be treated using Clause 3 of Lemma 3.2.
2. We can prove this clause by induction on ((u: (a[d=  u])d)c)
3. From Clause 1 above, all we have to prove is u(bc) 2 SN for any b 2 F . Since
4. This can be proved by analyzing reduction rules. ut
Theorem 3.1
Assume is derived in  ND .
Assume also that  is an interpretation, b
then we have
At rst look, the statement of the theorem looks ambiguous. For instance, given a
proof of x C ; y :D ' a : A, we may split the lefthand side of ' in two ways, each of which
results in the following conclusion:
holds for any b 1 2 (C) and b 2 2 (:D).
holds for any b 2 (C) and  c 2 (D) ? .
Actually the theorem implies that both hold, so no ambiguity arises. We now state the
proof of the theorem.
Proof. The theorem is proved by induction on the type inference of a. Let  be
a substitution [b 1 =x
as .
(Case: Assumption-Rule) In this case a  x. We have to prove x 2 (A). There are two
subcases. (i) x  x i for some i. Then A  C i and x  b i . By the assumption b i 2 (C i ),
so x 2 (A). (ii) x  u i for some i. Then A  :D i and x  z:u i (zc). From Lemma
3.5, we have x 2 (D
(Case: !-introduction) In this case a  x: c. We have A  B ! C and c is a term
of type C. By a suitable renaming, we have a  x: c. Take any d 2 (B). By IH,
Hence by Lemma 3.5, we have (x: c)d 2 (C), hence
C).
(Case: !-elimination) In this case, we have a  bc,
Hence a  (b)(c) 2 (A).
(Case: 8-introduction) In this case, A  8X: B and a : B is derivable. Let F 2 RC
and  0  [F=X]. Since the type variable X does not occur freely in , b
m. Hence, by IH, we have a 2  0 (B). Finally
a 2 (8X: B).
(Case: 8-elimination) In this case, a : 8X: B and A  B[C=X]. We have a 2 (8X: B)
from IH, hence a 2 [(C)=X](B). By Lemma 3.4, a 2 (B[C=X]).
(Case: -introduction) In this case, a  u:b, and b : A. By a suitable renaming, we
have a  u: b. We have By IH, we have
Hence (b 0 )c 2 SN , therefore by Clause 4 of Lemma 3.5,
we have u: (b 0 )c 2 SN . By Clause 2 of Lemma 3.5, (u: b)c 2 SN . Consequently,
(Case: ?-elimination) In this case, a  abort(b). By IH, b 2
3.2, we have a  abort(b) 2 (A). ut
By choosing x m) in
the theorem above, we obtain a 2 (A) for any term a of type A and an interpretation .
Since there exists an interpretation , and (A)  SN , we have the following theorem:
Corollary 3.1
ND is strongly normalizing.
4. Translation from the Catch/Throw Calculi to  ND
This section gives translations from the catch/throw calculi to  ND . In the following
we give only translations from the classical catch/throw calculi L K
c=t and NK c=t , but the
translations work also for L c=t and NJ c=t , since they are subcalculi.
4.1. Translation of Nakano's Calculus
We shall translate L K
c=t to  ND . The translation is the same as the standard encoding
of propositional logic in second-order logic except the catch/throw-constructs.
First, we translate types. (other than ?) in L K
c=t , and
variables in  ND .
The point here is that the type AB is translated to :B ! A. This translation re
ects
our intention that the -abstraction is translated to the -abstraction.
We then translate preterms in L K
c=t to  ND . We assume that, for each individual
variable x A in L K
c=t , x is a variable in  ND , and for each tag variable u A in L K
c=t , u is a
variable in  ND . We also assume that this mapping on variables are injective.
Preterms are translated as follows:
x A  x
abort(a)  abort(a)
x A :a  x:a
ab  ab
(a)  a(xy:x)
(a)  xy:xa
tapp(a;
The translation is extended to contexts for variables in the following way. Let be
a context for individual variables fx A 1: A
and  be a context for tag
variables
in L K
c=t . Then we dene:
Note that the types of tag variables are negated through the translation.
The translation preserves typing and reduction as we shall see.
Lemma 4.1 (Preservation of Type Assignment)
If ' a : A ;  is derived in L K
c=t , then ;  ' a : A is derived in  ND .
Proof. Since the translation for propositional connectives are standard, we verify the
other cases only.
From IH, we have ;  ' a : A. Since  fu : Ag is  fu : :Ag, and
a) is u:a, we can derive ;  fu A : Ag ' catch(u A ; a) : A by the
-introduction rule.
(throw) From IH, we have ;  ' a : A. Since  [ fu A : Ag is
a) is abort(ua), we can derive by the
!-elimination rule and the ?-elimination rule.
From IH, we have ;  ' a : A. Since
and A  B is :B ! A, we can derive ;  by the
!-introduction rule.
(tapp) From IH, we have
by the !-elimination rule, we can derive
Lemma 4.2
The translation is compatible with substitution. Namely, a[b=x A ]  a[b=x], and a[v B
a[v=u].
This lemma is proved by straightforward induction on the construction of a, and is
omitted.
Lemma 4.3 (Preservation of Reduction)
If a and b are typable terms and a ; 1 b in L K
c=t , then a ;+ b in  ND .
Proof.
This lemma is proved by induction on the structure of the term a. We prove the key
cases only.
1. a 6 x and x 2 FV(a)
By Lemma 4.2, we have a[throw(u A ; b)=x]  a[abort(ub)=x]. By induction on the
term a, we have a[abort(c)=x] ;+ abort(c) for any c, so we have a[abort(ub)=x] ;+
abort(ub).
2. catch(u A ; a) ; 1 a with u A 62 FTV(a)
Since u 62 FV (a), we have catch(u A ; a)  u:a ; 1 a.
3. catch(u A ; throw(u A ;
We have catch(u A ; throw(u A ; a))  u:abort(ua), and u 62 FV(a).
4. tapp(u:a;
We have tapp(u:a; v)  (u:a)v, and it reduces to a[v=u]. By Lemma 4.2, a[v=u]
a[v=u], hence we are done. ut
From the above lemmas, we have the following theorem.
Theorem 4.1
The system L K
c=t is strongly normalizing. Hence L c=t is strongly normalizing.
Remark. The translation from L K
c=t to  ND does not really need the second order
quantier. Namely, if we eliminate 8, and add ^ and _ to  ND , then we can translate
c=t to this modied calculus. Since we can prove the SN of this modied calculus by an
elementary method as in [16], we can also prove the SN of L K
c=t by an elementary method.
However, we need the second order quantier 8 in translating NK c=t as we shall see in
the next section. We therefore proved the SN of L K
c=t based on the reducibility method.
4.2. Translation of Sato's Calculus
In this subsection we translate NK c=t to  ND .
Before dening the translation, we try to give a naive translation from NK c=t to L K
c=t ,
and explains why it fails. A natural candidate of the translation is:
A  A for any type A
tapply(a;
where the type C will be supplied from the type inference of each term. At this moment
let us ignore how to obtain this C. By the above translation we can interpret all but one
reduction rules in NK c=t . The only exception is the following one:
The lefthand side is interpreted as
tapply(?u:a; v)  case(catch(u; inj 1
which does not necessarily reduce to a[v=u]. Hence the naive translation from NK c=t to
c=t fails. Moreover, it seems very dicult to nd a suitable extension of L K
c=t which is
strongly normalizing and which can reduce the above term to a[v=u].
However, the situation changes if we consider the second-order calculus where the disjunctive
type is no more primitive, but is dened as A _ B
As we shall see later, the term tapply(?u:a; v) reduces to a[v=u] through this
encoding.
Now let us dene the translation from NK c=t to  ND . The translation of types are
the same as the translation from L K
c=t to  ND . The translation of preterms except
are the same. The translation of the new constructs
is dened as follows:
tapply(a;
where we assume x; y are not used in the term a. This translation may look complex, but
it is the result of the second-order encoding of the above naive translation from NK c=t to
c=t .
The translation is extended to a context for individual variables in the same way as
before.
For a context for tag variables , we need to change the translation, since a tag variable
of type B should be translated to a variable of type C _ B where C is the type of the
body of enclosing ?-expression. In other words, we cannot determine the type C until
we reach the enclosing ?-expression. To solve this problem, we introduce a mapping
from a set of tag variables (in NK c=t ) to a set of types in  ND , and we make the
translation of contexts for tag variables dependent on . Let  be a context for tag
variables fu B1:
g, and be a mapping from fu B1
n g to types in
ND . We dene
In this denition _ 0 is an abbreviation dened as C _ 0 D  8X:
the same as the result of the translation of _).
Lemma 4.4 (Preservation of Type Assignment)
If ' a : A ;  is derivable in NK c=t , then, for any mapping whose domain contains all
the tag variables in , we have ;  ' a : A is derivable in  ND .
Proof. This is proved by induction on the derivation of ' a : A ; . We only verify
the key cases.
We have to derive ;  any . Fix a mapping
. Suppose (otherwise the proof is shorter), and  0   Bg. Let
0 be a mapping such that 0 (v)  (v) for v 6 u and 0 (u)  A. From IH, we
can derive ;  0 ' a : A. We have  0 is B)g. Also we have
From these
facts, we can derive the desired type inference by the -introduction rule.
We have to derive for any . Fix any . From IH,
we can derive ;  ' a : B. We have
is abort(u(xy:ya)). We can derive the desired type inference by the ?-elimination
rule.
We have to derive for any .
From IH, we can derive ;  ' a : A _ B. We have
B)g, and tapply(a; u B ) is a(x:x)(y:abort(u(zw:wy))). By calculating the type
of this term, we can derive the desired type inference. ut
The next lemma is used in proving the preservation of reduction through the translation.
Lemma 4.5
Let a be a typable term in NK c=t . Let  be a substitution [x:v(xt 1 t 2 )=v] where v
is the result of the translation of a tag variable v B in NK c=t , t 1 is x:x, and t 2 is
y:abort(u(zw:wy)). Then we have a ; a[u=v] in  ND .
Proof. We prove this lemma by induction on the structure of the term a. We state
here the key cases only.
(Case a  !v
We have the following reduction sequence:
(Case a  tapply(b; v B We have the following reduction sequence:
Lemma 4.6 (Preservation of Reduction)
If a and b are typable terms and a ; 1 b in  ND , then a ;+ b in  ND .
Proof.
We only check the key cases (the tapply-expression). In the following we put t 1  x:x,
and t 2  y:abort(u(zw:wy)).
1. tapply(inj 1
We have tapply(inj 1
2. tapply(inj 2
We have tapply(inj 2 (a); abort(u(zw:wa)). The
last term is !u B :a.
3. tapply(?v:a; u)
We have:
tapply(?v:a; u)  (v:zw:za)t 1 t 2
a[u=v]
Hence we have the desired property. ut
From the lemmas we have the following theorem.
Theorem 4.2
The system NK c=t (and hence NJ c=t ) is strongly normalizing.
Remark. In our proof, the use of the second order quantier 8 is indispensable to
give a translation of NK c=t . Since NK c=t is a rst-order system, one may think that our
proof used too strong a method, and that the SN of NK c=t could be proved by a more
elementary method. At present, we do not have an answer to this question. Our trial to
apply an elementary method to NK c=t was not successful.
5. Extension of the Catch/Throw Calculi
Having given the translation to  ND , it is easy to introduce the second-order quantier
to the four catch/throw calculi without loss of the nice properties such as the strong
normalization. Since the catch/throw calculi are formulated in the Church-style (variables
are explicitly labeled with their types), we should introduce term-constructs for type
abstraction/application. As usual we let X:a denote the former and aX for the latter.
The typing rules are given as follows:
In the 8-introduction rule (marked (*)), X may not occur freely in nor .
Also the reduction rule (X:a)B ; 1 a[B=X] is added. By adding these rules to L K
c=t ,
we obtain a second-order catch/throw calculus L K2
c=t . Similarly we can obtain NK 2
c=t .
The calculi L K2
c=t and NK 2
c=t enjoy nice properties such as the subject reduction and the
strong normalization. Here we brie
y mention the expressivity of these calculi.
structures such as the integers and the binary trees can be encoded by the second-order
quantier [6], we can dene functions with the catch/throw mechanism over various data
types in the extended calculi.
For instance the function multiply mentioned before is typed as follows:
It Int  U:uft:tUuf
It IntList  W:wft:tWwf
Here Times(a; b) is the multiplication of two integers a and b and dened as usual. It Int
and It IntList are iterators on the type Int and IntList. The term It Int (a; z:b; x)
with x 62 FV (b) is the if-then-else expression, namely it reduces to a if x is 0, and b
otherwise. It is easily seen that the above function multiply does the same computation
as one given in the introduction.
Since the above representation of free structures is not so good in computation [6], we
may consider another direction of extension. Namely, we may add inductive data types.
In [8], the rst author already proposed to add inductive data types to NJ c=t without
loss of the SN of the calculus, and showed that higher-order functions which use the
catch/throw mechanism can be represented in the extended calculus. However, we have
not fully studied this direction for the classical catch/throw calculi, so it is left for future
work.
6. Concluding Remarks
We have investigated the four catch/throw calculi by Nakano and Sato, in particular,
the calculi which correspond to classical logic through the Curry-Howard isomorphism.
We dene a non-deterministic variant of Parigot's -calculus, and proved the strong
normalizability of this variant. We gave faithful translations from the catch/throw calculi
to this variant, and as a corollary, we obtained the strong normalizability of the four
calculi. We also discussed their extension brie
y.
Recently, Fujita [4] studied  exc , a call-by-name variant of de Groote's formulation of the
exception mechanism in Standard ML. His calculus is a subcalculus of the rst-order version
of -calculus. Since the catch/throw mechanism and the exception mechanism are
essentially the same, his motivation and ours are similar. The main dierences of his calculus
and our  ND is that (1) his calculus is con
uent, while ours are non-deterministic,
so we have more computations, (2) he uses the rst-order version (actually, the implicational
while we use the second-order version, and (3) his calculus has two sorts
of variables (reminiscent of individual variables and tag variables), while we use one sort
of variables, thus we can directly abstract over tags.
Crolard [2] also studied a con
uent calculus for the catch/throw mechanism. Since his
calculus can be translated to Parigot's -calculus, it is similar to Fujita's formulation,
thus diers from the calculi studied in this paper.
Extracting algorithmic contents from classical proofs is now a quite active research
area. Many researchers in this area aim at obtaining con
uent calculi for classical logic.
However, classical logic is said to be inherently non-deterministic, namely, classical proofs
may contain multiple computational meanings. Therefore, if we want to represent as
many computational meanings as possible, it is natural to begin with non-deterministic
calculi. Our approach is to design and study non-deterministic calculi rst, then to study
con
uent subcalculi. We believe that the catch/throw calculi presented in this paper can
be good basis for this approach. Barbanera and Berardi's calculus [1] is another non-deterministic
calculus for classical proofs, so their calculus could be also a good basis.
Further studies on extracting computational meaning from classical proofs are left for
future work.

Acknowledgement

We would like to express our heartful thanks to Hiroshi Nakano, Makoto Tatsuta, and
Izumi Takeuti for helpful comments on earlier works. We also thank to Ken-etsu Fujita
for pointing out references and errors, and to anonymous referees for valuable comments
for improvement. The author is supported in part by Grant-in-Aid for Scientic Research
from the Ministry of Education, Science and Culture of Japan, No. 09780266 and No.
10143105.



--R






Proofs and Types (Cambridge University Press


"A Classical Catch/Throw Calculus with Tag Abstractions and its Strong Normalizability"










--TR
Common LISP: the language
Proofs and types
A formulae-as-type notion of control
Intuitionistic and classical natural deduction systems with the catch and the throw rules
Lambda-My-Calculus
Extracting Constructive Content from Classical Logic via Control-like Reductions
A Simple Calculus of Exception Handling
Classical Brouwer-Heyting-Kolmogorov Interpretation

--CTR
Emmanuel Beffara , Vincent Danos, Disjunctive normal forms and local exceptions, ACM SIGPLAN Notices, v.38 n.9, p.203-211, September
catch and throw;classical logic;type system;strong normalizability