Logical Structures of the Catch and Throw Mechanism

Hiroshi Nakano

Logical Structures of the Catch and Throw Mechanism

Hiroshi Nakano

Department of Applied Mathematics and Informatics Ryukoku University

A Dissertation

Submitted to the Graduate School of

the University of Tokyo

in Partial Fulfillment of the Requirements for the Degree of Doctor of Science

February, 1995 (Revised May, 1995)

Abstract

The catch and throw mechanism is a programming construct for non-local exit. In practical programming, this mechanism plays an important role when programmers handle exceptional situations. In this thesis we give typing systems which capture the mechanism in the proofs-as-programs notion. The typing systems can be regarded as a constructive logic with facilities for exception handling, which includes inference rules corresponding to the operations of catch and throw. We show that we can actually regard their proofs as programs which make use of the catch and throw mechanism by a natural interpretation. On one hand the catch and throw mechanism provides only a restricted access to the current continuation, on the other hand its logic is still constructive, in contrast to the works due to Griffin and Murthy on more powerful facilities such as call/cc (call-with-current-continuation) of Scheme. We also capture the non-determinism introduced by the catch and throw mechanism in a consistent way.

Acknowledgements

I would like to thank Susumu Hayashi for a great number of helpful suggestions and invaluable encouragement on this work. This work has been deeply influenced by him in a number of aspects. He pointed out the connection between this work and the literature concerning variants of LJ and the treatment of goto in Hoare’s logic. I would like to thank Satoru Takasu, who enlightened me on the fundamental notions of constructive programming. I would like to thank Masami Hagiya for his valuable comments and helpful support on this thesis. I would also thank Takayasu Ito, Masahiko Sato, Makoto Tatsuta, Satoshi Kobayashi, and many other people who contributed directly or indirectly to the development of this thesis. Finally I wish to thank Hiromi Nakano, my wife, for her patient encouragement and support during this work.

Contents

1 Introduction 1 1.1 Backgrounds . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1 1.2 The catch and throw mechanism . . . . . . . . . . . . . . . . . . . . . . . . . . . 2 1.3 Overview of the thesis . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 1.4 Related works . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5

2 A typing system for the catch and throw mechanism 7

2.1 A calculus with the catch and throw mechanism . . . . . . . . . . . . . . . . . . 7 2.1.1 Syntax . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7 2.1.2 Operational semantics of the calculus . . . . . . . . . . . . . . . . . . . . 8

2.2 The typing system . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11 2.3 A realizability interpretation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14

2.3.1 The realizability . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15 2.3.2 Soundness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16

3 The conventional implementation 20 3.1 Definition of the machine . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20 3.2 Validity of the machine . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23 3.3 Realizability by the abstract machine . . . . . . . . . . . . . . . . . . . . . . . . . 39

4 The typing system as a logic 40 4.1 A sequent calculus style formulation . . . . . . . . . . . . . . . . . . . . . . . . . 40 4.2 The logical meaning of the new connective . . . . . . . . . . . . . . . . . . . . . . 42 4.3 The catch and throw mechanism as structural rules . . . . . . . . . . . . . . . . . 43 4.4 The restriction on the right implication rule . . . . . . . . . . . . . . . . . . . . . 43 4.5 The cut-elimination theorem . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44

5 A natural extension with a non-determinism 49 5.1 A non-determinism by the catch and throw mechanism . . . . . . . . . . . . . . . 49 5.2 A calculus with a non-determinism . . . . . . . . . . . . . . . . . . . . . . . . . 49

5.2.1 Operational semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 5.3 Basic properties of the calculus . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 5.4 The typing system L_{c/t} . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52

5.4.1 Syntax of typing judgements . . . . . . . . . . . . . . . . . . . . . . . . . 52 5.4.2 L_{c/t} . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53

5.4.3 Basic properties of L_{c/t} . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 5.5 The subject reduction property of L_{c/t} . . . . . . . . . . . . . . . . . . . . . . . . 57 5.6 L_{c/t} as a logic . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 60

6 A term model for the extended system 62 6.1 Term models . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 62 6.2 An admissible frame . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 73 6.3 Strong normalizability and normal forms . . . . . . . . . . . . . . . . . . . . . . . 84 6.4 Realizability interpretation of L_{c/t} . . . . . . . . . . . . . . . . . . . . . . . . . . 85

7 Concluding remarks 86

Chapter 1

Introduction

1.1 Backgrounds

It is well known that constructive proofs can be regarded as computer programs by a notion called “proofs as programs”. By this notion, we can extract executable programs from constructive proofs of sentences that correspond to the specifications of the programs by a “realizability interpretation” [16]. The same schema can be observed in the area of constructive type theories, in which types specify what programs do. The notion of “proofs as programs” is also called “formula as types”, “propositions as types” or the Curry-Howard isomorphism [14], and is summarized as the following correspondences.

Computer programming  Constructive logic or type theory
programs  proofs
specifications  formulas or types
program development  theorem proving
programmers  mathematicians or ...

This paradigm provides a theoretical basis for a formal method of computer programming, in which programmers construct formal proofs of theorems that specify what the programs do, and target programs in some form are automatically extracted from the formal proofs. The correctness of the programs relative to their specification, that is, the theorems, is defined by a certain interpretation of formulas of the formal system, and is assured by the soundness metatheorem for the formal system with respect to the interpretation. In other words, programmers simultaneously construct and verify the computer programs in this paradigm.

In the last decade, many works have been intensively done both in practical and in theoretical approaches [5, 6, 12, 13, 19, 26, 35, 36], in which the most of their attention has been concentrated on the area that can be regarded as an application of the standard constructive logic, because we had already have rich results on the constructive logic itself, and the conventional constructive logics really have enough strength with respect to the class of provable theorems, that is, the class of realizable specifications. However, from the viewpoint of practical programming, some aspects of the logical activities of programmers have not been captured in this paradigm. For example, the class of proofs, that is, the class of available programs is also important for the programmers as well as the class of provable theorems, but is not ever discussed intensively. Actually, many practical programming languages provide some additional programming facilities to programmers in order to extend the class of programs. Although these facilities do not extend the class of realizable specifications, that is, we can construct equivalent programs without such additional facilities, they have important roles for practical program development. The main aim of this thesis is to capture one of such programming facilities in the notion of “proofs as programs”.

1.2 The catch and throw mechanism

The catch and throw mechanism is a programming facility for non-local exit. We can find examples of the mechanism in some practical programming languages such as C [15] and Common Lisp [32]. We give some primary introduction about this mechanism by taking Common Lisp as an example. In the case of Common Lisp, (catch tag form) is a special form that serves as a target of transfer of control by another special form (throw tag form). At the evaluation of (catch tag form), a catcher marked with the tag is established, and the form is then evaluated. The result of the form is returned from the catch, except that if a throw special form with the same tag is executed during the evaluation, then the evaluation is immediately aborted and the catch returns a value specified by the form of the throw. For example, the evaluation process

of (+ (catch 'u (+ 2 (+ 3 5))) 8) proceeds as follows.
                    Eval: (+ (catch 'u (+ 2 (+ 3 5))) 8)
                     . . . . Eval: (catch 'u (+ 2 (+ 3 5)))

….  …. Eval: 'u
….  …. Return: u
….  …. Eval: (+ 2 (+ 3 5))
….  ….  …. Eval: 2
….  ….  …. Return: 2
….  ….  …. Eval: (+ 3 5)
….  ….  ….  …. Eval: 3
….  ….  ….  …. Return: 3
….  ….  ….  …. Eval: 5
….  ….  ….  …. Return: 5
….  ….  ….  …. Apply: + to 3 and 5
….  ….  …. Return: 8
….  ….  …. Apply: + to 2 and 8
….  …. Return: 10

…. Return: 10 …. Eval: 8 …. Return: 8 …. Apply: + to 10 and 8

Return: 18

On the other hand, the evaluation process of (+ (catch 'u (+ 2 (+ 3 (throw 'u 5)))) 8) proceeds as follows.

Eval: (+ (catch 'u (+ 2 (+ 3 (throw 'u 5)))) 8)
. . . . Eval: (catch 'u (+ 2 (+ 3 (throw 'u 5))))

….  …. Eval: 'u
….  …. Return: u

. . . .  . . . . Eval: (+ 2 (+ 3 (throw 'u 5)))

….  ….  …. Eval: 2
….  ….  …. Return: 2
….  ….  …. Eval: (+ 3 (throw 'u 5))
….  ….  ….  …. Eval: 3
….  ….  ….  …. Return: 3
….  ….  ….  …. Eval: (throw 'u 5)
….  ….  ….  ….  …. Eval: 'u
….  ….  ….  ….  …. Return: u
….  ….  ….  ….  …. Eval: 5
….  ….  ….  ….  …. Return: 5
….  ….  ….  ….  …. Apply: throw to u and 5

…. Return: 5 …. Eval: 8 …. Return: 8 …. Apply: + to 2 and 8

Return: 10

In practical programming, the catch and throw mechanism plays an important role when programmers handle exceptional situations. Suppose, for example, we have to construct a program P with a specification represented by a sequent Γ → C ∨ E of LJ combining three subprograms Q: Γ → A ∨ E, R: Γ A → B ∨ E and S: Γ B → C ∨ E, where C is the normal output for the input Γ, and E is an error signal which denotes that there is something wrong in the input. The specifications of Q, R and S say that such errors may be detected in the execution of these subprograms. In this situation, the construction of P in LJ would be as follows,

\begin{aligned}\begin{matrix}⋮ & Q \\ Γ → A ∨ E \end{matrix} & \begin{matrix}\begin{matrix}\begin{matrix}⋮ & R \\ Γ A → B ∨ E \end{matrix} & \begin{matrix}\begin{matrix}⋮ & S \\ Γ B → C ∨ E \end{matrix} & \begin{matrix}E → E & (init) \\ E → C ∨ E \end{matrix} ; (→ ∨) \\ Γ B ∨ E → C ∨ E \end{matrix} ; (∨ →) \\ Γ A → C ∨ E \end{matrix} ; (cut) & \begin{matrix}E → E & (init) \\ E → C ∨ E \end{matrix} ; (→ ∨) \\ Γ A ∨ E → C ∨ E \end{matrix} ; (∨ →) \\ & Γ → C ∨ E \end{aligned} ; (cut),

where applications of structural rules are omitted. The constructed program P would work as follows. The program P first calls the subprogram Q and gets its return value, then checks whether it denotes an error or not. If not, P calls the subprogram R with that value and gets its return value. P again checks the value and calls S if it does not denote an error. Eventually, P returns the value returned by S. If P detects an error in the values returned by Q or S, it immediately returns a value denoting an error. We can find an inefficiency that whenever P gets values from the subprograms it must check whether they denote an error or not. This is often found in practical programming without the catch and throw mechanism. If the mechanism is available, programmers can concentrate on the main stream of programming as if no exceptional situation can arise, since error signals are passed through ordinary language constructs. Following the proofs-as-programs notion in the opposite direction, we can find that the problem comes from the restriction of LJ that only one formula is admissible in the right-hand side of sequents. If the restriction is dropped as in LK, we can construct P′ of a specification Γ→C E from subprograms Q′: Γ → A E, R′: Γ A → B E and S′: Γ B → C E as follows,

\begin{aligned}\begin{matrix}⋮ & Q′ \\ Γ → A E \end{matrix} & \begin{matrix}\begin{matrix}⋮ & R′ \\ Γ A → B E \end{matrix} & \begin{matrix}⋮ & S′ \\ Γ B → C E \end{matrix} \\ Γ A → C E \end{matrix} (cut) \\ & Γ → C E \end{aligned} ; (cut),

where structural rules are again omitted. The proof is much simpler than the previous one and easy to develop. The point is that exceptional conclusions are admitted besides the main conclusion and we can proceed the proof construction as if they do not exist. It reflects the programmer’s reasoning behind the catch and throw mechanism well. Of course, we must justify such a logic constructively so that correct programs can be extracted from the proofs.

In this thesis, we present such an attempt to extract a logical structure from the programmer’s reasoning concerning exception handling by the catch and throw mechanism, and capture the mechanism in the notion of “proofs as programs” by constructive frame works and their realizability interpretations.

1.3 Overview of the thesis

Chapter 2 gives a typing system for a simple programming language equipped with the catch and throw mechanism. The aim of this chapter is to capture the mechanism with a fixed evaluation strategy, the call-by-value strategy. Section 2.1 introduces a calculus with the catch and throw mechanism, and gives its operational semantics by a set of reduction rules in the manner of Felleisen et al. [7]. This semantics should be a natural translation of the standard operational semantics of the mechanism in practical programming languages. Section 2.2 gives a typing system Lc/t^{CBV} of the calculus, and Section 2.3 gives a realizability interpretation of the typing system and shows how the catch and mechanism can be captured by proving the soundness theorem.

Chapter 3 introduces an abstract stack machine to imitate the standard implementation of the catch and throw mechanism in practical programming languages, and shows that the semantics defined by this machine is equivalent to the one given in Section 2.1. Another realizability interpretation of Lc/t^{CBV} defined directly by the abstract machine is also given.

Chapter 4 discusses the formal system regarding it as a logic. We show that Lc/t^{CBV} is a conservative extension of the propositional fragment of the standard intuitionistic logic such as Gentzen’s LJ or NJ. We reformulate Lc/t^{CBV} into a sequent calculus style formal system in order to clarify the difference between Lc/t^{CBV} and the standard formulations of classical and intuitionistic logic. The cut-elimination theorem of the sequent calculus style reformulation is also given.

Chapter 5 deals with the non-determinism introduced by the catch and throw mechanism. The reduction rules of the calculus given in Chapter 2 is naturally extended to capture this non-determinism, in which any evaluation strategy should be allowed. The typing system of the calculus is also extended. We show that although the well-typed terms of the system do not have the Church-Rosser property, they have the subject reduction property instead.

Chapter 6 is devoted to construction of a term model of the extended system introduced in the previous chapter. Unfortunately, the standard method is not enough to this construction, and a set of terms that has a certain property is required for the domain of interpretation. By this term model, we show the strong normalizability of the well-typed terms and the soundness of the extended typing system relative to an extended realizability interpretation.

1.4 Related works

From a computational point of view, the catch and throw mechanism is just a subcase of more powerful facilities for control such as call/cc of Scheme and Felleisen’s C operator [7], and the relation between such facilities and the computational meaning of classical logic has been investigated in various ways [3, 11, 21, 20, 22, 27, 28, 29, 31], where the computational behavior of the facilities is captured as translation processes of classical proofs into intuitionistic ones [8].

Murthy showed that classical formal proofs can be regarded as programs with such control facilities [21, 20], where Felleisen’s C operator corresponds to the following inference rule of classical logic.

{¬¬A \atop A} (C)

By a simple modification of Freidman’s work [8], he showed that classical proofs of a formula A can be translated into intuitionistic proofs of (A^{Φ} ⊃ Φ) ⊃ Φ for any formula Φ, where

A^{Φ} = A  (A is atomic)
(¬A)^{Φ} = A^{Φ} ⊃ Φ
(A ∧ B)^{Φ} = A^{Φ} ∧ B^{Φ}
(A ∨ B)^{Φ} = A^{Φ} ∨ B^{Φ}
(A ⊃ B)^{Φ} = A^{Φ} ⊃ (B^{Φ} ⊃ Φ) ⊃ Φ
(∀x.A)^{Φ} = ∀x.((A^{Φ} ⊃ Φ) ⊃ Φ)
(∃x.A)^{Φ} = ∃x.A^{Φ}.

Note that if Φ does not include any ¬, ⊃ or ∀, then we can translate classical proofs of Φ into intuitionistic ones since Φ^{Φ} = (Φ ⊃ Φ) ⊃ Φ in this case. This translation of formulas that maps A to A^{Φ} corresponds to the continuation-passing-style translation [30] of programs of type A, and the computational meaning of C operator can be regarded as a mechanism that transforms intuitionistic proofs of ((¬¬A)^{Φ} ⊃ Φ) ⊃ Φ into ones of (A^{Φ} ⊃ Φ) ⊃ Φ.

However, from the viewpoint of formal method for computer programming, only a restricted class of formulas, for example, Π_{2}^{0} sentences, are allowed for the specification of programs in order to assure the total correctness of the programs in these classical frameworks. On the other hand, any of such restrictions is not required for the frameworks presented in this thesis, that is, any formula is allowed as a specification of programs. More importantly, the main aim of our work is to capture the logic behind the use of such facilities in practical programming rather than to capture their computational behavior. We summarize the basic properties of our frameworks in comparison among others in the following table.

framework  logic  trick

proof as programs

non-determinism

Murthy [20]  classical  C operator  restricted  no
λμ-calculus [29]  classical  μ operator  restricted  no
LC [9]  classical  involutive negation restricted  no
λ_{P rop}^{Sym} [3]  classical  involutive negation restricted  yes
Lc/t^{CBV}  intuitionistic  catch/throw  yes  no
L_{c/t}  intuitionistic  catch/throw  yes  yes

A typing system for the catch and throw mechanism

2.1 A calculus with the catch and throw mechanism

In this section we introduce a simple programming language equipped with the catch and throw mechanism, and give its operational semantics.

2.1.1 Syntax

We first give the syntax of the language.

Definition 2.1.1 (Constants and variables) We assume that the following disjoint sets of individual constants, individual variables and tag variables are given. The syntax of the calculus is defined relatively to these three sets.

Const : a set of individual constants c, d, . . ..
Var  : a countably infinite set of individual variables x, y, z, . . ..
Tvar : a countably infinite set of tag variables u, v, w, . . ..

Definition 2.1.2 (Terms) We define a set Term of terms by

Term : : = Const | Var
| let Var=Term. Term
| throw Tvar Term | catch Tvar Term
| λ Var. Term^{∗} | Term Term
| <Term, Term> | proj1 Term | proj2 Term
| inj1 Term | inj2 Term | case Term Var. Term Var. Term
| κ Tvar. Term | Term Tvar ,

where Term^{∗} stands for the set of terms that have no free occurrence of tag variables. We use M, N, K, L, … to denote terms.

Free and bound occurrences of variables are defined in the standard manner. We regard a tag variable u as bound in catch u M and κ u. M. We denote the set of individual and tag variables occurring freely in M by F IV (M) and F T V (M), respectively.

Example 2.1.3 (Terms)

λ x. case x y.(inj2 y) z.(inj1 z)
catch u ((κ v. proj1 <x, throw v y>) u)

Note that we have a restriction on terms of the form λ x. M. For example, λ x. throw u x is not a term since it has a free occurrence of a tag variable u.

The terms of the forms throw Tvar Term and catch Tvar Term provide the catch and throw mechanism of the language. Roughly, these terms correspond to throw and catch of Common Lisp [32], respectively. The terms κ Tvar. Term and Term Tag are used for tag-abstraction and tag-instantiation, respectively. These terms provide a way of passing tags. Note that tags can not be passed by usual lambda-abstractions and applications since they are not terms.

We also define the alpha-convertibility in the standard manner where we allow renaming of bound tag variables as well as bound individual variables. Hereafter, we identify terms by this alpha-convertibility. We use M[N_{1}/x_{1}, …, N_{n}/x_{n}] to denote the term obtained from a term M by substituting N_{1}, …, N_{n} for each free occurrence of individual variables x_{1}, …, x_{n}, respectively, with alpha-conversion for avoiding capture of free variables. Similarly, we also use M[v_{1}/u_{1}, …, v_{n}/u_{n}] to denote the term obtained from M by substituting v_{1}, …, v_{n} for each free occurrence of tag variables u_{1}, …, u_{n}, respectively. Note that in the case that N_{1}, …, N_{n} have free tag variables, M[N_{1}/x_{1}, …, N_{n}/x_{n}] may not be a well-formed term, because N_{1}, …, N_{n} can introduce some free tag variables into lambda-abstractions.

Proposition 2.1.4 Let M be a term, and let x_{1}, …, x_{m} and u_{1}, …, u_{n} be sequences of distinct individual and tag variables, respectively. If N_{1}, …, N_{m} are closed terms and v_{1}, …, v_{n} are tag variables, then M[N_{1}/x_{1}, …, N_{m}/x_{m}, v_{1}/u_{1}, …, v_{n}/u_{n}] is a term.

Proof. Obvious from the definition of Term.

2.1.2 Operational semantics of the calculus

We define a call-by-value evaluator of terms to give an intuitive semantics of this calculus. The evaluator is defined in terms of evaluation contexts and a set of rewriting rules for terms. The basic idea is due to Felleisen et al. [7]. In Chapter 3 we will give another operational semantics by an abstract machine which imitates the standard implementation of the catch/throw mechanism in some practical programming languages.

Definition 2.1.5 (Values) We define a set Val of closed terms as follows.

Val : : = Const
| λ Var. Term | <Val, Val>
| inj1 Val | inj2 Val
| κ Tvar. Val | κ Tvar. throw Tvar Val .

Elements of Val are called values, and we use V, V′, W, W′, … to denote values.

Note that any value must be a closed term. Therefore any value of the form

κ Tvar. throw Tvar Val

must be κ u. throw u V for some tag variable u and some value V.

Example 2.1.6 (Values)

λ x. (λ y. y) x
<inj1 c_{1}, κ u. throw u c_{2}>

Definition 2.1.7 (Evaluation contexts) We define a set C of pseudo terms which have a hole, denoted by ∗, in them as follows.

C : : = ∗
| let Var=C. Term
| throw Tvar C | catch Tvar C
| C Term | Val C
| <C, Term> | <Val, C> | proj1 C | proj2 C
| inj1 C | inj2 C | case C Var. Term Var. Term
| κ Tvar. C | C Tag.

Elements of C are called evaluation contexts. We use C, C′, … to denote evaluation contexts. We use C[M] to denote the term obtained from C by replacing the hole ∗ by a term M.

By the definition, no evaluation context captures free individual variables placed at the hole, but it may capture free tag variables at the hole. For example, if C = catch u ∗ and M = throw u N, then C[M] = catch u (throw u N).

Example 2.1.8 (Evaluation contexts)

(λ y. M (proj1 y)) <∗, N>

catch u (inj1 (throw u ∗))

Proposition 2.1.9 If C and C′ are evaluation contexts, then C[C′] is also an evaluation context.

Proof. Obvious from the definition of evaluation contexts.

Proposition 2.1.10 If a term M can be written as M = C[throw u V], where V is a value and C does not capture u, then the combination of such C and throw u V is unique.

Proof. By induction on the structure of C. Note that no value has free occurrences of tag variables.

Definition 2.1.11 (Rewriting rules) The call-by-value rewriting ⟼_{CBV} is defined by the following rules, where C is an arbitrary evaluation context such that C ≠ ∗ and C does not capture u. Note that none of redexes is a value.

catch u V ⟼_{CBV} V
catch u C[throw u V] ⟼_{CBV} catch u (throw u V)
catch u (throw u V) ⟼_{CBV} V
let x=V. M ⟼_{CBV} M[V/x]
(λ x. M) V ⟼_{CBV} M[V/x]
κ u. C[throw u V] ⟼_{CBV} κ u. throw u V
(κ u. V) v ⟼_{CBV} V
(κ u. throw u V) v ⟼_{CBV} throw v V
proj1 <V, W > ⟼_{CBV} V
proj2 <V, W > ⟼_{CBV} W
case (inj1 V) x.M y.N ⟼_{CBV} M[V/x]
case (inj2 V) x.M y.N ⟼_{CBV} N[V/y]

Proposition 2.1.12 Let M be a term. If M ⟼_{CBV} N for some N, then N is unique.

Proof. Obvious from the definition of ⟼_{CBV}.

Definition 2.1.13 (Evaluation steps) A call-by-value evaluation step ⟶_{CBV} is defined by

C[M] ⟶_{CBV} C[N]  if and only if  M ⟼_{CBV} N.

Example 2.1.14 Let M be a term, and let V and V′ be values.

(catch u ((λ z. M) (throw u (λ x. x)))) V ⟶_{CBV} (catch u (throw u (λ x. x))) V
⟶_{CBV} (λ x. x) V
⟶_{CBV} V
catch u (proj2 <V, V′>) ⟶_{CBV} catch u V′
⟶_{CBV} V′
catch u (((λ x. κ v. throw v x) V) u) ⟶_{CBV} catch u ((κ v. throw v V) u)
⟶_{CBV} catch u (throw u V)
⟶_{CBV} V

Let ⟶_{CBV}^{∗} be the transitive and reflexive closure of the relation ⟶_{CBV}. We write M ≻_{CBV} N if N is a normal form of M w.r.t. ⟶_{CBV}, that is, M ⟶_{CBV}^{∗} N and N / ; ⟼_{CBV} K for any K.

Proposition 2.1.15 If M ⟶_{CBV} N, then C[M] ⟼_{CBV} C[N] for any evaluation context C.

Proof. Obvious from the definitions of ⟶_{CBV} and evaluation contexts.

Proposition 2.1.16 Let x_{1}, …, x_{n} and y_{1}, …, y_{n} be sequences of individual variables, and sup-

pose that x_{1}, …, x_{n} are distinct. If M ⟶_{CBV} N, then M[y_{1}/x_{1}, …, y_{n}/x_{n}] ⟶_{CBV} N[y_{1}/x_{1}, …,

y_{n}/x_{n}]. Similarly, let u_{1}, …, u_{n} and v_{1}, …, v_{n} be sequences of tag variables, and suppose that

u_{1}, …, u_{n} are distinct. If M ⟶_{CBV} N, then M[v_{1}/u_{1}, …, v_{n}/u_{n}] ⟶_{CBV} N[v_{1}/u_{1}, …, v_{n}/u_{n}].

Proof. Obvious from the definition of ⟶_{CBV}.

Proposition 2.1.17 If M is not a normal form, then M can be written in a unique way as M = C[N] for some evaluation context C and some redex N, i.e., N ⟼_{CBV} K for some K.

Proof. Since M is not normal, there exists at least one combination of such C and N. We can show the uniqueness by induction on the structure of C.

Therefore, if M ≻_{CBV} N, then N is unique. But note that N may not be a value even if M ≻_{CBV} N. For example, throw u V ≻_{CBV} throw u V, but throw u V is not a value.

Proposition 2.1.18 Every value is a normal form.

Proof. Obvious from the definition of ⟶_{CBV}.

Proposition 2.1.19 Let V be a value. Let u and C be a tag variable and an evaluation context, respectively. If C does not capture u, then C[throw u V] is a normal form.

Proof. By induction on the form of C. Note that C[throw u V] is not a value, because it is not a closed term.

2.2 The typing system

We introduce a typing system Lc/t^{CBV} of the language given in the previous section, which can be regarded as a logical system that captures the catch/throw mechanism.

Definition 2.2.1 (Type expressions) We have five kinds of type expressions in Lc/t^{CBV} as follows.

A : atomic type expression
A ∧ B : conjunction
A ∨ B : disjunction
A ⊃ B : implication
A ◁ B : exception

Type expressions are also called formulas.

The last one is introduced to handle the catch/throw mechanism and represents another kind of disjunction. It corresponds to the type of tag-abstractions, i.e., terms of the form κ Tvar. Term. We give a precise meaning to the connective ◁ by a realizability interpretation later.

Definition 2.2.2 (Type-contexts) An individual type-context, or an individual context for short, is a finite mapping which assigns a type expression, i.e., a formula, to each individual variable in its domain. We use {x_{1} : A_{1}, …, x_{m}: A_{m}} to denote an individual type-context whose domain is {x_{1}, …, x_{m}} and which assigns A_{i} to x_{i} for any i, where A_{1}, …, A_{m} are type expressions, and x_{1}, …, x_{m} are distinct individual variables. A tag type-context, or a tag context for short, is similarly defined as a finite mapping which assigns a type expression to each tag variable in its domain. We use {u_{1} : B_{1}, …, u_{n}: B_{n}} to denote a tag type-context, where u_{1}, …, u_{n} are distinct tag variables.

Definition 2.2.3 (Typing judgement) Let Γ be an individual type-context, and Δ a tag typecontext. Let M be a term, and C a type expression. Typing judgements have the following form.

Γ ⊢ M : C; Δ.

A typing judgement {x_{1} : A_{1}, …, x_{m}: A_{m}} ⊢ M : C; {u_{1} : E_{1}, …, u_{n}: E_{n}} roughly says that when we execute the program M supplying values of the types A_{1} … A_{m} for the corresponding free variables x_{1}, …, x_{m} of the program, it normally returns a value of the type C, otherwise the program exits with a value which belongs to one of the types E_{1} … E_{n}. Let us explain by example. If we have a derivation of a typing judgement {x: A, y: B} ⊢ M : C; {}, then

1. F IV (M) ⊂ {x, y}, and

2. if K and L satisfy the specifications A and B, respectively, then the evaluation of M[K/x, L/y] terminates with a value that satisfies the specification C.

Note that this corresponds to the standard interpretation of simply typed lambda calculus. On the other hand, {x: A, y: B} ⊢ M : C; {u: E} says that

1. F IV (M) ⊂ {x, y},

2. F T V (M) ⊂ {u}, and

3. if K and L satisfy the specifications A and B, respectively, then

a. the evaluation of M[K/x, L/y] terminates with a value that satisfies the specification

C, or b. the evaluation of M[K/x, L/y] causes a throw-operation of a value to the tag u, which is not caught by catch-terms, and the thrown value satisfies the specification E.

That is, there are two possible results of the evaluation of M in the second example. The precise meaning of typing judgements is given in the next section by a realizability interpretation.

Definition 2.2.4 (Typing rules) The inference rules of Lc/t^{CBV} are as follows.

Γ ∪ {x: A} ⊢ x: A; Δ (var)

Γ ⊢ N : A; Δ Γ ∪ {x: A} ⊢ M : C; Δ

Γ ⊢ let x=N. M : C; Δ (let)

Γ ⊢ M : E; Δ Γ ⊢ throw u M : A; Δ ∪ {u: E} (throw)  Γ ⊢ M : A; Δ ∪ {u: A} Γ ⊢ catch u M : A; Δ (catch)

\begin{matrix}Γ ⊢ M : A; Δ & Γ ⊢ N : B; Δ \\ Γ ⊢ <M, N>: A ∧ B; Δ \end{matrix} (∧-I )

Γ ⊢ M : A ∧ B; Δ Γ ⊢ proj1 M : A; Δ (∧_{1}-E )  Γ ⊢ M : A ∧ B; Δ Γ ⊢ proj2 M : B; Δ (∧_{2}-E )

{Γ ⊢ M : A; Δ \atop Γ ⊢ inj1 M : A ∨ B; Δ} (∨_{1}-I )  {Γ ⊢ M : B; Δ \atop Γ ⊢ inj2 M : A ∨ B; Δ} (∨_{2}-I )

Γ ⊢ L: A ∨ B; Δ Γ ∪ {x: A} ⊢ M : C; Δ Γ ∪ {y: B} ⊢ N : C; Δ

Γ ⊢ case L x.M y.N : C; Δ (∨-E )

{Γ ∪ \{x: A\} ⊢ M : B; \{\} \atop Γ ⊢ λ x. M : A ⊃ B; Δ} (⊃-I )  \begin{matrix}Γ ⊢ M : A ⊃ B; Δ & Γ ⊢ N : A; Δ \\ Γ ⊢ M N : B; Δ \end{matrix} (⊃-E )

{Γ ⊢ M : A; Δ ∪ \{u: E\} \atop Γ ⊢ κ u. M : A ◁ E; Δ} (◁-I )  {Γ ⊢ M : A ◁ E; Δ \atop Γ ⊢ M u: A; Δ ∪ \{u: E\}} (◁-E )

Example 2.2.5 (Derivations) Let Γ be as Γ = {x: A, f : A ⊃ A}.

\begin{matrix}Γ ∪ \{y: B\} ⊢ x: A; \{\} & (var) \\ Γ ⊢ λ y. x: B ⊃ A; \{u: A\} \end{matrix} ; (⊃-I ) \begin{matrix}Γ ⊢ f : A ⊃ A; \{\} (var) & Γ ⊢ x: A; \{\} (var) \\ Γ ⊢ f x: A; \{\} \end{matrix} ; (⊃-E )

Γ ⊢ throw u (f x) : B; {u: A} (throw)

Γ ⊢ (λ y. x) (throw u (f x)) : A; {u: A} (⊃-E )

Γ ⊢ catch u ((λ y. x) (throw u (f x))) : A;

(catch)
{x: A} ⊢ λ f. catch u ((λ y. x) (throw u (f x))) : (A ⊃ A) ⊃ A;

(⊃-I )
⊢ λ x. λ f. catch u ((λ y. x) (throw u (f x))) : A ⊃ (A ⊃ A) ⊃ A;

(⊃-I )

There is nothing special except for (throw), (catch), (⊃-I ), (◁-I ) and (◁-E ). If we have a term M of a type E, we can treat the term throw u M as if it belongs to an arbitrary type A, but in reality, the evaluation of throw u M causes a throw-operation of the result of M to the tag u instead of returning a value of A. On the other hand, if we have a term M of A which may throw a value of A to the tag u during the evaluation of M, then we can treat catch u M as a term of A which causes no throw-operation to u. Once we adopt the interpretation of typing judgements explained above, these rules for catch and throw are quite natural.

The most important point about our typing rules is a restriction on the rule (⊃-I ). We can introduce a λ-abstraction only if its body has no free tag variable, that is, the tag context of the premise must be empty. If we dropped this restriction, our intended interpretation of typing judgements would be affected. Consider the following example.

\begin{matrix}\{x: A\} ⊢ x: A; \{\} & (var) \\ \{x: A\} ⊢ throw u x: B; \{u: A\} \end{matrix} (throw)

{} ⊢ λ x. throw u x: A ⊃ B; {u: A} (⊃-I )

The derived judgement says that the evaluation of λ x. throw u x terminates with a value of A ⊃ B, or a value of A is thrown to the tag u during the evaluation. But the evaluation of λ x. throw u x immediately terminates with itself, which is not a value of A ⊃ B. Note that throw u x is not evaluated until λ x. throw u x is applied to some value of the type A. From the logical point of view, this restriction on (⊃-I ) is required to keep the system constructive. We shall discuss this point in Chapter 4.

The restriction on (⊃-I )-rule leads us to introduce the new connective ◁. We can not construct any function that may throw something to the outside of the function without the new connective, because the body of the λ-abstraction must not have any tag variable. We can construct such a function by the new connective as follows. Let Γ be as Γ = {x: A ∨ B}.

Γ ⊢ x: A ∨ B; \{u: B\} (var) Γ ∪ \{y: A\} ⊢ y: A; \{u: B\} (var) ; . . . . . . \begin{matrix}Γ ∪ \{z: B\} ⊢ z: B; \{\} & (var) \\ Γ ∪ \{z: B\} ⊢ throw u z: A; \{u: B\} \end{matrix} (throw)

Γ ⊢ case x y.y z.(throw u z) : A; {u: B}

(∨-E )

Γ ⊢ κ u. case x y.y z.(throw u z) : A ◁ B; {} (◁-I )

{} ⊢ λ x. κ u. case x y.y z.(throw u z) :(A ∨ B) ⊃(A ◁ B) ; {} (⊃-I )

Let M be as M = λ x. κ u. case x y.y z.(throw u z), and let N be a term of the type A ∨ B. The function M can be used as follows.

\begin{matrix}\begin{matrix}⋮ ; \{\} ⊢ M :(A ∨ B) ⊃(A ◁ B) ; \{\} & ⋮ ; \{\} ⊢ N : A ∨ B; \{\} \\ \{\} ⊢ M N : A ◁ B; \{\} \end{matrix} & (⊃-E ) \\ \{\} ⊢ (M N) v: A; \{v: B\} \end{matrix} ; (◁-E )

Normally the function M returns a value of A, otherwise it throws a value of B to the given tag v.

2.3 A realizability interpretation

In this section we give a realizability interpretation of Lc/t^{CBV} to show how the catch/throw mechanism can be captured in it.

2.3.1 The realizability

Let A be a mapping which assigns a subset of Const to each atomic type. The realizability is defined relatively to this mapping A.

Definition 2.3.1 (Realizability of types) Let V be a value, and A a type. We define a relation r between values and types as follows.

1. V r A iff V ∈ A(A), if A is an atomic type.

2. V r A_{1} ∧ A_{2} iff V = <V_{1}, V_{2}> for some V_{1} and V_{2} such that V_{1} r A_{1} and V_{2} r A_{2}.

3. V r A_{1} ∨ A_{2} iff V = inj_{i} W and W r A_{i} for some W and i (i = 1, 2).

4. V r A_{1} ⊃ A_{2} iff V = λ x. M for some term M such that for any value W, if W r A_{1}, then M[W/x] ≻_{CBV} V′ and V′ r A_{2} for some value V′.

5. V r A_{1} ◁ A_{2} iff V = κ u. M for some u and M such that

(a) M is a value and M r A_{1}, or

(b) M = throw u W and W r A_{2} for some value W.

If the relation holds between a term and a type, we say that the term realizes the type, and the term is a realizer of the type.

Definition 2.3.2 (Interpretation) We define the interpretation of typing judgements as follows. The relation

{x_{1} : A_{1}, …, x_{m}: A_{m}} ⊢ ⊢ M : C; {u_{1} : B_{1}, …, u_{n}: B_{n}}

holds if and only if for any closed terms K_{1}, …, K_{m} such that K_{i} ≻_{CBV} W_{i} and W_{i} r A_{i} for some W_{i} (1 ≤ i ≤ m),

1. M[K_{1}/x_{1}, …, K_{m}/x_{m}] ≻_{CBV} V and V r C for some V, or

2. M[K_{1}/x_{1}, …, K_{m}/x_{m}] ≻_{CBV} C[throw u_{j} V] and V r B_{j} for some j, V and C which does not capture u_{j}.

This interpretation is essentially the same as the standard realizability interpretation of NJ in the case that the type C does not include any occurrence of ◁ and n = 0. It should also be noted that the logical connective ◁ corresponds to the semicolon of a typing judgement as ⊃ corresponds to ⊢.

Lemma 2.3.3 Suppose that {x_{1} : A_{1}, …, x_{m}: A_{m}} ⊢ ⊢ M : C; {u_{1} : B_{1}, …, u_{n}: B_{n}} holds. and let y_{1} … y_{m} and v_{1} … v_{n} be a sequence of distinct individual variables and a sequence of distinct tag variables, respectively. Then

{y_{1} : A_{1}, …, y_{m}: A_{m}} ⊢ ⊢ M[y⃗/x⃗, v⃗/u⃗] ; {v_{1} : B_{1}, …, v_{n}: B_{n}}

also holds, where M[y⃗/x⃗, v⃗/u⃗] stands for M[y_{1}/x_{1}, …, y_{m}/x_{m}, v_{1}/u_{1}, …, v_{n}/u_{n}].

Proof. Since M[y⃗/x⃗, v⃗/u⃗][K⃗/y⃗] = M[K⃗/x⃗, v⃗/u⃗], straightforward from the definition of Γ ⊢ ⊢ M : C; Δ by Proposition 2.1.16.

2.3.2 Soundness

The following soundness theorem assures us that we can regard the proofs of the formal system as programs which satisfy the specification defined by the realizability interpretation of the conclusion.

Theorem 2.3.4 (Soundness) If Γ ⊢ M : C; Δ is derivable in Lc/t^{CBV}, then Γ ⊢ ⊢ M : C; Δ holds.

Proof. By induction on the structure of the derivation. Let Γ be as Γ = {x_{1} : A_{1}, …, x_{m}: A_{m}}, and let Δ be as Δ = {u_{1} : B_{1}, …, u_{n}: B_{n}}. Let K_{1}, …, K_{m} be closed terms such that K_{i} ≻_{CBV} W_{i} and W_{i} r A_{i} for some W_{i} (1 ≤ i ≤ m). Each induction step is done by cases according to the rule applied in the last step of the derivation.

Case 1: The last rule is (var). Trivial.

Case 2: The last rule is (let). Let Γ ⊢ M_{1} : D; Δ and Γ ∪ {z: D} ⊢ M_{2} : C; Δ be the premises, that is, M = let z=M_{1}. M_{2}. By the induction hypothesis, Γ ⊢ ⊢ M_{1} : D; Δ and Γ ∪ {z: D} ⊢ ⊢ M_{2} : C; Δ hold. Therefore for some V_{1},

1. M_{1}[K⃗/x⃗] ≻_{CBV} V_{1} and V_{1} r D, or

2. M_{1}[K⃗/x⃗] ≻_{CBV} C′[throw u_{j} V_{1}] and V_{1} r B_{j} for some j (1 ≤ j ≤ n) and C′ which does not capture u_{j}.

Let z′ be a fresh individual variable. In the first case,

(let z=M_{1}. M_{2})[K⃗/x⃗] = let z′=M_{1}[K⃗/x⃗]. M_{2}[z′/z][K⃗/x⃗]
⟶_{CBV}^{∗} let z′=V_{1}. M_{2}[z′/z][K⃗/x⃗]
⟶_{CBV} M_{2}[z′/z][K⃗/x⃗][V_{1}/z′]
= M_{2}[V_{1}/z][K⃗/x⃗].

Since Γ ∪ {z: D} ⊢ ⊢ M_{2} : C; Δ and V_{1} r D, for some V_{2},

M_{2}[V_{1}/z][K⃗/x⃗] ≻_{CBV} V_{2} and V_{2} r C, or

M_{2}[V_{1}/z][K⃗/x⃗] ≻_{CBV} C[throw v_{j} V_{2}] and V_{2} r B_{j}

for some j (1 ≤ j ≤ n) and C which does not capture v_{j}. Therefore, one of the two conditions of Definition 2.3.2 is satisfied. In the second case, let C be as C = let z′=C′. M_{2}[z′/z][K⃗/x⃗].

(let z=M_{1}. M_{2})[K⃗/x⃗] = let z′=M_{1}[K⃗/x⃗]. M_{2}[z′/z][K⃗/x⃗]
⟶_{CBV}^{∗} let z′=C′[throw u_{j} V_{1}]. M_{2}[z′/z][K⃗/x⃗]
= C[throw u_{j} V_{1}].

Since C does not capture u_{j}, the second condition of Definition 2.3.2 is satisfied in this case. Therefore Γ ⊢ ⊢ let z=M_{1}. M_{2} ; Δ holds.

Case 3: The last rule is (throw). Let Γ ⊢ M′: B_{k}; Δ′ be the premise, where Δ = Δ′ ∪ {u_{k}: B_{k}} and M = throw u_{k} M′. By the induction hypothesis, for some V′,

1. M′[K⃗/x⃗] ≻_{CBV} V′ and V′ r B_{k}, or

2. M[K⃗/x⃗] ≻_{CBV} C′[throw u_{j} V′] and V′ r B_{j} for some j (1 ≤ j ≤ n) and C′ which does not capture u_{j}.

In the first case,

(throw u_{k} M′)[K⃗/x⃗] = throw u_{k} M′[K⃗/x⃗] ⟶_{CBV}^{∗} throw u_{k} V′.

Therefore the second condition of Definition 2.3.2 is satisfied since V′ r B_{k}. In the second case, let C be as C = throw u_{k} C′.

(throw u_{k} M′)[K⃗/x⃗] = throw u_{k} M′[K⃗/x⃗]
⟶_{CBV}^{∗} throw u_{k} C′[throw u_{j} V′]
= C[throw u_{j} V′].

Since C does not capture u_{j}, the second condition of Definition 2.3.2 is satisfied also in this case. Therefore Γ ⊢ ⊢ throw u_{k} M′: C; Δ holds.

Case 4: The last rule is (catch). Let Γ ⊢ M′: C; Δ∪{v: C} be the premise, where M = catch v M′. By the induction hypothesis, for some V′,

1. M′[K⃗/x⃗] ≻_{CBV} V′ and V′ r C,

2. M′[K⃗/x⃗] ≻_{CBV} C′[throw v V′] and V′ r C for some C′ which does not capture v, or

3. M′[K⃗/x⃗] ≻_{CBV} C′[throw u_{j} V′], V′ r B_{j} and u_{j} ≠ v, for some j and C′ which does not capture u_{j}.

In the first case,

(catch v M′)[K⃗/x⃗] = catch v M′[K⃗/x⃗] ⟶_{CBV}^{∗} catch v V′ ⟶_{CBV} V′.

Therefore the first condition of Definition 2.3.2 is satisfied. In the second case, since C′ does not capture v,

(catch v M′)[K⃗/x⃗] = catch v M′[K⃗/x⃗]
⟶_{CBV}^{∗} catch v C′[throw v V′]
= or ⟶_{CBV} catch v (throw v V′)
⟶_{CBV} V′.

That is, the first condition is satisfied also in this case. In the last case, let C be as C = catch v C′.

(catch v M′)[K⃗/x⃗] = catch v M′[K⃗/x⃗]
⟶_{CBV}^{∗} catch v C′[throw u_{j} V′]
= C[throw u_{j} V′].

Since u_{j} ≠ v, C does not capture u_{j}. Therefore the second condition of Definition 2.3.2 is satisfied in this case. We now get Γ ⊢ ⊢ catch v M′; Δ.

Case 5: The last rule is (⊃-I ). Let Γ∪{z: C_{1}} ⊢ M′: C_{2} ; {} be the premise, where M = λ z. M′ and C = C_{1} ⊃ C_{2}. Let z′ be a fresh individual variable.

(λ z. M′)[K⃗/x⃗] = λ z′. M[z′/z][K⃗/x⃗] ∈ Val.

Assume that W r C_{1}. By the induction hypothesis,

M[z′/z][K⃗/x⃗][W/z′] = M[W/z][K⃗/x⃗] ≻_{CBV} V′ and V′ r C_{2}.

That is, (λ z. M′)[K⃗/x⃗] r C_{1} ⊃ C_{2}.

Case 6: The last rule is (⊃-E ). Let Γ ⊢ M_{1} : D ⊃ C; Δ and Γ ⊢ M_{2} : D; Δ be the premises, where M = M_{1} M_{2}. By the induction hypothesis on the first premise, for some V_{1},

1. M_{1}[K⃗/x⃗] ≻_{CBV} V_{1} and V_{1} r D ⊃ C, or

2. M_{1}[K⃗/x⃗] ≻_{CBV} C′[throw u_{j} V_{1}] and V_{1} r B_{j} for some j (1 ≤ j ≤ n) and C′ which does not capture u_{j}.

In the first case, since V_{1} r D ⊃ C, we can assume that V_{1} = λ z. N for some z and N. Therefore,

(M_{1} M_{2})[K⃗/x⃗] = M_{1}[K⃗/x⃗] M_{2}[K⃗/x⃗] ⟶_{CBV}^{∗} (λ z. N) M_{2}[K⃗/x⃗]

On the other hand, by induction hypothesis on the second premise, for some V_{2},

M_{2}[K⃗/x⃗] ≻_{CBV} V_{2} and V_{2} r C, or

M_{2}[K⃗/x⃗] ≻_{CBV} C′′[throw u_{j} V_{2}] and V_{2} r B_{j}

for some j (1 ≤ j ≤ n) and C′′ which does not capture u_{j}. Therefore, (M_{1} M_{2})[K⃗/x⃗] ⟶_{CBV}^{∗}

(λ z. N) V_{2} ⟶_{CBV} N[V_{2}/z] or (M_{1} M_{2})[K⃗/x⃗] ⟶_{CBV}^{∗} (λ z. N) C[throw u_{j} V_{2}]. Since λ z. N r D ⊃ C

and V_{2} r D, one of the two conditions of Definition 2.3.2 is satisfied. In the second case, let C be as C = C′ M_{2}[K⃗/x⃗].

(M_{1} M_{2})[K⃗/x⃗] ⟶_{CBV}^{∗} C′[throw u_{j} V_{1}] M_{2}[K⃗/x⃗] = C[throw u_{j} V_{1}]

Since C does not capture u_{j}, the second condition of Definition 2.3.2 is satisfied in this case. Therefore, Γ ⊢ ⊢ M_{1} M_{2} ; Δ holds.

Case 7: The last rule is (◁-I ). Let Γ ⊢ M′: C_{1} ; Δ ∪ {v: C_{2}} be the premise, where M = κ v. M′ and C = C_{1} ◁ C_{2}.

(κ v. M′)[K⃗/x⃗] = κ v. M′[K⃗/x⃗].

By the induction hypothesis, for some V′,

1. M′[K⃗/x⃗] ≻_{CBV} V′ and V′ r C_{1},

2. M′[K⃗/x⃗] ≻_{CBV} C′[throw v V′] and V′ r C_{2} for some C′ which does not capture v, or

3. M′[K⃗/x⃗] ≻_{CBV} C′[throw u_{j} V′], V′ r B_{j} and u_{j} ≠ v, for some j and C′ which does not capture u_{j}.

In the first case,

(κ v. M′)[K⃗/x⃗] = κ v. M′[K⃗/x⃗] ⟶_{CBV}^{∗} κ v. V′,

and since V′ r C_{1}, we get κ v. V′ r C_{1} ◁ C_{2}. Therefore, the first condition of Definition 2.3.2 is satisfied. In the second case,

(κ v. M′)[K⃗/x⃗] = κ v. M′[K⃗/x⃗]
⟶_{CBV}^{∗} κ v. C′[throw v V′]
= or ⟶_{CBV} κ v. throw v V′.

Since V′ r C_{2}, we get κ v. throw v V′ r C_{1} ◁ C_{2}. That is, the first condition is satisfied also in this case. In the third case, let C be as C = κ v. C′.

(κ v. M′)[K⃗/x⃗] = κ v. M′[K⃗/x⃗]
⟶_{CBV}^{∗} κ v. C′[throw u_{j} V′]
= C[throw u_{j} V′].

Since u_{j} ≠ v, C does not capture u_{j}. Therefore the second condition is satisfied. We now get Γ ⊢ ⊢ κ v. M′: C_{1} ◁ C_{2} ; Δ.

Case 8: The last rule is (◁-E ). Let Γ ⊢ M′: C ◁ B_{k}; Δ′ be the premise, where M = M′ u_{k} and Δ = Δ′ ∪ {u_{k}: B_{k}}.

(M′ u_{k})[K⃗/x⃗] = M′[K⃗/x⃗] u_{k}.

By the induction hypothesis, for some V′,

1. M′[K⃗/x⃗] ≻_{CBV} κ v. V′ and V′ r C for some v,

2. M′[K⃗/x⃗] ≻_{CBV} κ v. throw v V′ and V′ r B_{k} for some v, or

3. M′[K⃗/x⃗] ≻_{CBV} C′[throw u_{j} V′] and V′ r B_{j} for some j (1 ≤ j ≤ n) and C′ which does not capture u_{j}.

In the first case,

(M′ u_{k})[K⃗/x⃗] = M′[K⃗/x⃗] u_{k} ⟶_{CBV}^{∗} (κ v. V′) u_{k} ⟶_{CBV} V′

That is, the first condition of Definition 2.3.2 is satisfied in this case. In the second case,

(M′ u_{k})[K⃗/x⃗] = M′[K⃗/x⃗] u_{k} ⟶_{CBV}^{∗} (κ v. throw v V′) u_{k} ⟶_{CBV} throw u_{k} V′

Since V′ r B_{k}, the second condition is satisfied. In the third case, Let C be as C = C′ u_{k}.

(M′ u_{k})[K⃗/x⃗] = M′[K⃗/x⃗] u_{k} ⟶_{CBV}^{∗} C′[throw u_{j} V′] u_{k} = C[throw u_{j} V′]

Since C does not capture u_{j}, the second condition is satisfied in this case. We now get Γ ⊢ ⊢ M′ u_{k}: C; Δ.

Case 10: The last rule is one of the others. We get Γ ⊢ ⊢ M : C; Δ similarly.

Corollary 2.3.5 If {} ⊢ M : C; {} is derivable in Lc/t^{CBV}, then M ≻_{CBV} V for some value V.

Proof. Straightforward from Theorem 2.3.4.

The conventional implementation

In this section we imitate the standard implementation of the catch/throw mechanism by an abstract stack machine, and give a realizability interpretation of the formal system in terms of the abstract machine which is equivalent to the realizability defined in Section 2.3.

3.1 Definition of the machine

We design the machine only to illustrate how the catch/throw mechanism works. Other mechanisms required for the evaluation of terms remain abstract (cf. [17, 30]). First, we extend the syntax. The extended part is used by the machine internally.

Definition 3.1.1 (Tag constants) We assume that a set Tconst which is a representation of the set of natural numbers is given. Elements of Tconst are called tag constants. We use \overline{n} to denote the tag constant that represents a natural number n.

Definition 3.1.2 (Tag^{+}) We define a set Tag^{+} by

Tag^{+} : : = Tconst | Tvar .

Elements of Tag^{+} are called internal tags. We use t, t′, … to denote internal tags.

Definition 3.1.3 (Val^{+} and Term^{+}) We define two sets Val^{+} and Term^{+}, simultaneously, as follows.

Val^{+} : : = Const | λ Var. Term^{+} | <Val^{+}, Val^{+}>
| inj1 Val^{+} | inj2 Val^{+}
| κ Tvar. val Val^{+} | κ Tvar. throw Tvar (val Val^{+})
Term^{+} : : = Const | Var | val Val^{+} | let Var=Term^{+}. Term^{+}
| throw Tag^{+} Term^{+} | catch Tvar Term^{+}
| λ Var. Term^{+} | Term^{+} Term^{+}
| <Term^{+}, Term^{+}> | proj1 Term^{+} | proj2 Term^{+}
| inj1 Term^{+} | inj2 Term^{+} | case Term^{+} Var. Term^{+} Var. Term^{+}
| κ Tvar. Term^{+} | Term^{+} Tag^{+} ,

where every element of Val^{+} must be closed and must not have any occurrence of tag constants. Elements of Val^{+} are called internal values. We use Q, R, … to denote internal values. Elements of Term^{+} are called internal terms. We use e, f, g, … to denote internal terms. Note that if λ x. e is an internal value, then F IV (e) ⊂ {x} and F T V (e) = {} since every internal value must be closed.

Proposition 3.1.4 Val^{+} ⊂ Term^{+} and Term ⊂ Term^{+}.

Proof. Obvious from the definition.

We now have new terms such as val (λ x. e), throw \overline{3} e and e \overline{0}, as internal terms as well as ordinary terms.

Definition 3.1.5 Let e be an internal term which does not have any occurrence of tag constants. We assign a term \overline{e} to e as follows.

\overline{c} = c  \overline{x} = x
\overline{val e} = \overline{e}  \overline{let x=e_{1}. e_{2}} = let x=\overline{e}_{1}. \overline{e}_{2}
\overline{throw u e} = throw u \overline{e}  \overline{catch u e} = catch u \overline{e}
\overline{λ x. e} = λ x. \overline{e}  \overline{e_{1} e_{2}} = \overline{e}_{1} \overline{e}_{2}
\overline{<e_{1}, e_{2}>} = <\overline{e}_{1}, \overline{e}_{2}>  \overline{proj_{i} e} = proj_{i} \overline{e}
\overline{inj_{i} e} = inj_{i} \overline{e}  \overline{case e_{0} x.e_{1} y.e_{2}} = case \overline{e}_{0} x.\overline{e}_{1} y.\overline{e}_{2}
\overline{κ u. e} = κ u. \overline{e}  \overline{e u} = \overline{e} u

That is, \overline{e} is the term obtained from e by stripping all val’s occurring in e.

Proposition 3.1.6 Let e be a closed internal term. If e has no occurrence of tag constants, then \overline{e} is a closed term.

Proof. Straightforward induction on the structure of e.

Proposition 3.1.7 \overline{Q} ∈ Val for any internal value Q.

Proof. Straightforward induction on the structure of Q. Note that any internal value has no occurrence of tag constants.

Proposition 3.1.8 Let M be a term, x_{1}, …, x_{n} individual variables, and Q_{1}, …, Q_{n} internal values.

\overline{M[val Q_{1}/x_{1}, …, val Q_{n}/x_{n}]} = M[\overline{Q}_{1}/x_{1}, …, \overline{Q}_{n}/x_{n}].

Proof. Straightforward induction on the structure of M.

Definition 3.1.9 (Seg) We define a set Seg by

Seg : : = let Var=∗. Term^{+} | throw Tag^{+} ∗ | catch Tvar ∗
| ∗ Term^{+} | Val^{+} ∗
| <∗, Term^{+}> | <Val^{+}, ∗> | proj1 ∗ | proj2 ∗
| inj1 ∗ | inj2 ∗ | case ∗ Var. Term^{+} Var. Term^{+}
| κ Tvar. ∗ | κ Tvar. throw Tvar ∗ | ∗ Tag^{+} ,

where κ Tvar. throw Tvar ∗ must be closed, that is, the two tag variables are identical. Elements of Seg are called context segments. We use S, S′, … to denote context segments.

The abstract machine has a stack. The state of the machine is determined only by this stack state. We represent a stack state as follows.

bottom ←  → top
[ S_{1}, S_{2}, S_{3}, …, S_{n}, e ],

where S_{1}, …, S_{n} are context segments and e is a closed internal term.

Definition 3.1.10 A stack state [ S_{1}, S_{2}, S_{3}, …, S_{n}, e] is valid if S_{1} … S_{n} are context segments and e is a closed internal term.

Definition 3.1.11 (Transition rules) The abstract machine changes its state according to the following table, where S⃗ denotes a sequence of context segments.

[ S⃗, c ] ⇒ [ S⃗, val c]
[ S⃗, let x=e_{1}. e_{2} ] ⇒ [ S⃗, let x=∗. e_{2}, e_{1} ]
[ S⃗, let x=∗. e_{2}, val e_{1} ] ⇒ [ S⃗, e_{2}[val e_{1}/x] ]
[ S⃗, throw t e ] ⇒ [ S⃗, throw t ∗, e ]
[ S_{1}, …, S_{n}, S_{n+1}, …, S_{n+m},
throw \overline{n} ∗, val e ] ⇒ [ S_{1}, …, S_{n}, val e ]
[ S_{1}, …, S_{n}, catch u e ] ⇒ [ S_{1}, …, S_{n}, e[\overline{n}/u] ]
[ S⃗, λ x. e ] ⇒ [ S⃗, val (λ x. e) ]
[ S⃗, e_{1} e_{2} ] ⇒ [ S⃗, ∗ e_{2}, e_{1} ]
[ S⃗, ∗ e_{2}, val e_{1} ] ⇒ [ S⃗, e_{1} ∗, e_{2} ]
[ S⃗, (λ x. e_{1}) ∗, val e_{2} ] ⇒ [ S⃗, e_{1}[val e_{2}/x] ]
[ S⃗, <e_{1}, e_{2}> ] ⇒ [ S⃗, <∗, e_{2}>, e_{1} ]
[ S⃗, <∗, e_{2}>, val e_{1} ] ⇒ [ S⃗, <e_{1}, ∗>, e_{2} ]
[ S⃗, <e_{1}, ∗>, val e_{2} ] ⇒ [ S⃗, val <e_{1}, e_{2}> ]
[ S⃗, proj1 e ] ⇒ [ S⃗, proj1 ∗, e ]
[ S⃗, proj1 ∗, val <e_{1}, e_{2}> ] ⇒ [ S⃗, val e_{1} ]
[ S⃗, proj2 e ] ⇒ [ S⃗, proj2 ∗, e ]
[ S⃗, proj2 ∗, val <e_{1}, e_{2}> ] ⇒ [ S⃗, val e_{2} ]
[ S⃗, inj1 e ] ⇒ [ S⃗, inj1 ∗, e ]
[ S⃗, inj1 ∗, val e ] ⇒ [ S⃗, val (inj1 e) ]
[ S⃗, inj2 e ] ⇒ [ S⃗, inj2 ∗, e ]
[ S⃗, inj2 ∗, val e ] ⇒ [ S⃗, val (inj2 e) ]
[ S⃗, case e_{0} x.e_{1} y.e_{2} ] ⇒ [ S⃗, case ∗ x.e_{1} y.e_{2}, e_{0} ]
[ S⃗, case ∗ x.e_{1} y.e_{2}, val (inj1 e_{0}) ] ⇒ [ S⃗, e_{1}[val e_{0}/x] ]
[ S⃗, case ∗ x.e_{1} y.e_{2}, val (inj2 e_{0}) ] ⇒ [ S⃗, e_{2}[val e_{0}/y] ]
[ S_{1}, …, S_{n}, κ u. e ] ⇒ [ S_{1}, …, S_{n}, κ u. throw u ∗,
throw \overline{n} ∗, κ u. ∗, e[\overline{n+1}/u] ]

[ S⃗, κ u. ∗, val e ] ⇒ [ S⃗, val (κ u. val e) ]
[ S⃗, κ u. throw u ∗, val e ] ⇒ [ S⃗, val (κ u. throw u (val e)) ]
[ S⃗, e t ] ⇒ [ S⃗, ∗ t, e ]
[ S⃗, ∗ t, val (κ u. e) ] ⇒ [ S⃗, e[t/u] ]

Let ⇒^{∗} be the transitive and reflexive closure of the relation ⇒. Example 3.1.12

[ (catch u ((λ z. e) (throw u (λ x. x)))) c ]
⇒ [ ∗ c, catch u ((λ z. e) (throw u (λ x. x))) ]
⇒ [ ∗ c, (λ z. e) (throw \overline{1} (λ x. x)) ]
⇒ [ ∗ c, ∗ (throw \overline{1} (λ x. x)), λ z. e ]
⇒ [ ∗ c, ∗ (throw \overline{1} (λ x. x)), val (λ z. e) ]
⇒ [ ∗ c, (λ z. e) ∗, throw \overline{1} (λ x. x) ]
⇒ [ ∗ c, (λ z. e) ∗, throw \overline{1} ∗, λ x. x ]
⇒ [ ∗ c, (λ z. e) ∗, throw \overline{1} ∗, val (λ x. x) ]
⇒ [ ∗ c, val (λ x. x) ]
⇒ [ (λ x. x) ∗, c ]
⇒ [ (λ x. x) ∗, val c ]
⇒ [ val c ]

Note that when the stack is in a state [ S_{1}, S_{2}, …, S_{n−1}, S_{n}, e ], the composition S_{1}[S_{2}[… [S_{n−1}[S_{n}]] …]] of the context segments represents the evaluation contexts of the internal term e, i.e., the continuation after the evaluation of e. The catch/throw mechanism of the machine provides a restricted access to the continuation through tags. Observe that we need not any explicit copying of evaluation contexts to provide the mechanism.

Proposition 3.1.13 Let [ S_{1}, …, S_{m}, e ] be a valid stack state. If

[ S_{1}, …, S_{m}, e ] ⇒ [ S′_{1}, …, S′_{n}, e′ ],

then [ S′_{1}, …, S′_{n}, e′ ] is also valid.

Proof. Obvious from the definition of transition rules. Note that e is closed since the state is valid.

Definition 3.1.14 Let S⃗ and S⃗′ be sequences of context segments, and let e and e′ be internal terms. [ S⃗′, e′ ] is a final state of [ S⃗, e ], if [ S⃗, e ] ⇒^{∗} [ S⃗′, e′ ] and no transition rule is applicable to [ S⃗′, e′ ].

The rule applicable for a state is unique by the definition of the transition rules. Therefore, if [e] ⇒^{∗} [val Q], the internal value Q is unique.

3.2 Validity of the machine

In this subsection we discuss the validity of the abstract machine relative to the semantics given in Section 2.1.2. We show that 1. M ≻_{CBV} V implies [ M ] ⇒^{∗} [ val Q ] for some Q such that \overline{Q} = V, and

2. [ M ] ⇒^{∗} [ val Q ] implies M ≻_{CBV} \overline{Q}.

for any closed term M.

Definition 3.2.1 Let e and e′ be internal terms, and let S_{1}, …, S_{m} and S′_{1}, …, S′_{n} be sequences of context segments. Let l be a natural number. We define a relation ⇒_{l} by

[ S_{1}, …, S_{m}, e] ⇒_{l} [ S′_{1}, …, S′_{n}, e′] iff \{ \begin{matrix}[ S_{1}, …, S_{m}, e] ⇒ [ S′_{1}, …, S′_{n}, e′], \\ l ≤ m, n, and \\ S_{i} = S′_{i} (1 ≤ i ≤ l). \end{matrix}

Let ⇒_{l}^{∗} be the transitive and reflexive closure of the relation ⇒_{l}.

The relation ⇒ is equivalent to ⇒_{0}, and ⇒_{n} implies ⇒_{m} if m < n. Note that if [ S_{1}, …, S_{m}, e] ⇒_{l} [ S′_{1}, …, S′_{n}, e′], then this transition does not depend on S_{1}, …, S_{l}.

Definition 3.2.2 Let M be a term such that M ≻_{CBV} N for some N. The rewriting path from M to N is unique. We denote the length of the path by len(M).

Definition 3.2.3 Let M be a term. We define |M| by

|c| = |x| = 1
|let x=M. N| = 1 + max(|M|, |N|)
|throw u M| = |catch u M| = |λ x. M| = 1 + |M|
|M N| = |<M, N>| = 1 + max(|M|, |N|)
|proj_{i} M| = |inj_{i} M| = 1 + |M|
|case L x.M y.N| = 1 + max(|L|, |M|, |N|)
|κ x. M| = |M u| = 1 + |M|.

Theorem 3.2.4 Let S⃗ be a sequence of context segments whose lengths is l. Let x_{1}, …, x_{m} be individual variables, and R_{1}, …, R_{m} internal values. Let u_{1}, …, u_{n} be tag variables, and \overline{k}_{1}, …, \overline{k}_{n} tag constants such that k_{i} ≤ l for any i. Let M be a term such that F IV (M) ⊂ \{x_{1}, …, x_{m}\} and F T V (M) ⊂ \{u_{1}, …, u_{n}\}. Let M[\overline{R⃗}/x⃗] and M[val R⃗/x⃗,\overline{k⃗}/u⃗] be abbreviations for M[\overline{R}_{1}/x_{1}, …, \overline{R}_{m}/x_{m}] and M[val R_{1}/x_{1}, …, val R_{m}/x_{m}, \overline{k}_{1}/u_{1}, …, \overline{k}_{n}/u_{n}], respectively.

1. If M[\overline{R⃗}/x⃗] ≻_{CBV} V, then

[ S⃗, M[valR⃗/x⃗,\overline{k⃗}/u⃗] ] ⇒_{l}^{∗} [ S⃗, val Q ],

for some internal value Q such that \overline{Q} = V.

2. If M[\overline{R⃗}/x⃗] ≻_{CBV} C[throw u_{j} V] for some j and C which does not capture u_{j}, then

[ S⃗, M[valR⃗/x⃗,\overline{k⃗}/u⃗] ] ⇒_{l}^{∗} [ S⃗, S⃗′, throw \overline{k}_{j} ∗, val Q ],

for some sequence of context segments S⃗′ and some internal value Q such that \overline{Q} = V.

Proof. Induction on the lexicographic ordering of len(M[\overline{R⃗}/x⃗]) and |M[\overline{R⃗}/x⃗]|.

Case 1: M is an individual constant. In this case M[\overline{R⃗}/x⃗] = M. Therefore, we get V = M if M[\overline{R⃗}/x⃗] ≻_{CBV} V. By the definition of transition rules,

[ S⃗, M[valR⃗/x⃗,\overline{k⃗}/u⃗] ] = [ S⃗, M ] ⇒_{l} [ S⃗, val M ].

Let Q be as Q = M. Then we get \overline{Q} = V since M is an individual constant. Note that M[\overline{R⃗}/x⃗] / ; ≻_{CBV} C[throw u_{i} V].

Case 2: M is an individual variable. We get M[\overline{R⃗}/x⃗] = M or M[\overline{R⃗}/x⃗] = \overline{R}_{i} for some i. Therefore M[\overline{R⃗}/x⃗] / ; ≻_{CBV} C[throw u_{j} V]. Suppose that M[\overline{R⃗}/x⃗] ≻_{CBV} V, i.e., M = x_{i} and \overline{R}_{i} ≻_{CBV} V. Since \overline{R}_{i} is a value, we get \overline{R}_{i} = V. Let Q be as Q = R_{i}. Obviously [ S⃗, M[valR⃗/x⃗,\overline{k⃗}/u⃗] ] ⇒_{l}^{∗} [ S⃗, val R_{i} ] since M[valR⃗/x⃗,\overline{k⃗}/u⃗] = val R_{i}.

Case 3: M = let y=M_{1}. M_{2} for some y, M_{1} and M_{2}. We can assume y ≠ x_{i} for any i. First, suppose that M[\overline{R⃗}/x⃗] ≻_{CBV} V. By the definition of rewriting rules, M_{1}[\overline{R⃗}/x⃗] ≻_{CBV} V_{1} and M_{2}[\overline{R⃗}/x⃗][V_{1}/y] ≻_{CBV} V for some value V_{1}. Note that len(M_{1}[\overline{R⃗}/x⃗]), len(M_{2}[\overline{R⃗}/x⃗][V_{1}/y]) < len(M[\overline{R⃗}/x⃗]). Therefore, for some internal values Q_{1} and Q such that \overline{Q}_{1} = V_{1} and \overline{Q} = V,

[ S⃗, (let y=M_{1}. M_{2})[valR⃗/x⃗,\overline{k⃗}/u⃗] ]
⇒_{l} [ S⃗, let y=∗. M_{2}[valR⃗/x⃗,\overline{k⃗}/u⃗], M_{1}[valR⃗/x⃗,\overline{k⃗}/u⃗] ]
⇒_{l}^{∗} [ S⃗, let y=∗. M_{2}[valR⃗/x⃗,\overline{k⃗}/u⃗], val Q_{1} ]  (by ind. hyp.)
⇒_{l} [ S⃗, M_{2}[valR⃗/x⃗, val Q_{1}/y,\overline{k⃗}/u⃗] ]
⇒_{l}^{∗} [ S⃗, val Q ]  (by ind. hyp.).

Next suppose that M[\overline{R⃗}/x⃗] ≻_{CBV} C[throw u_{j} V]. By the definition of rewriting rules,

1. M_{1}[\overline{R⃗}/x⃗] ≻_{CBV} C′[throw u_{j} V] and C = let y=C′. M_{2} for some C′, or

2. M_{1}[\overline{R⃗}/x⃗] ≻_{CBV} V_{1} and M_{2}[\overline{R⃗}/x⃗][V_{1}/x] ≻_{CBV} C[throw u_{j} V] for some value V_{1}.

In the first case, len(M_{1}[\overline{R⃗}/x⃗]) = len(M[\overline{R⃗}/x⃗]) and |M_{1}[\overline{R⃗}/x⃗]| < |M[\overline{R⃗}/x⃗]|. Therefore by the induction hypothesis, for some S⃗′ and Q such that \overline{Q} = V,

[ S⃗, (let y=M_{1}. M_{2})[valR⃗/x⃗,\overline{k⃗}/u⃗] ]
⇒_{l} [ S⃗, let y=∗. M_{2}[valR⃗/x⃗,\overline{k⃗}/u⃗], M_{1}[valR⃗/x⃗,\overline{k⃗}/u⃗] ]
⇒_{l}^{∗} [ S⃗, let y=∗. M_{2}[valR⃗/x⃗,\overline{k⃗}/u⃗], S⃗′, throw \overline{k}_{j} ∗, val Q ].

In the second case, len(M_{1}[\overline{R⃗}/x⃗]), len(M_{2}[\overline{R⃗}/x⃗][V_{1}/x]) < len(M[\overline{R⃗}/y⃗]). Therefore, for some S⃗′, Q_{1} and Q such that \overline{Q}_{1} = V_{1} and \overline{Q} = V,

[ S⃗, (let y=M_{1}. M_{2})[valR⃗/x⃗,\overline{k⃗}/u⃗] ]
⇒_{l} [ S⃗, let y=∗. M_{2}[valR⃗/x⃗,\overline{k⃗}/u⃗], M_{1}[valR⃗/x⃗,\overline{k⃗}/u⃗] ]
⇒_{l}^{∗} [ S⃗, let y=∗. M_{2}[valR⃗/x⃗,\overline{k⃗}/u⃗], val Q_{1} ]  (by ind. hyp.)
⇒_{l} [ S⃗, M_{2}[valR⃗/x⃗, val Q_{1}/y,\overline{k⃗}/u⃗] ]
⇒_{l}^{∗} [ S⃗, S⃗′, throw \overline{k}_{j} ∗, val Q ]  (by ind. hyp.).

Case 4: M = throw v M′ for some v and M′. Since M[\overline{R⃗}/x⃗] / ; ≻_{CBV} V, suppose that M ≻_{CBV} C[throw u_{j} V]. By the definition of rewriting rules,

1. M′[\overline{R⃗}/x⃗] ≻_{CBV} C′[throw u_{j} V] and C = throw v C′ for some C′, or

2. M′[\overline{R⃗}/x⃗] ≻_{CBV} V and v = u_{j}.

In the first case, len(M′[\overline{R⃗}/x⃗]) = len(M[\overline{R⃗}/x⃗]) and |M′[\overline{R⃗}/x⃗]| < |M[\overline{R⃗}/x⃗]|. Therefore by the induction hypothesis, for some S⃗′ and Q such that \overline{Q} = V,

[ S⃗, (throw v M′)[valR⃗/x⃗,\overline{k⃗}/u⃗] ] = [ S⃗, throw v[\overline{k⃗}/u⃗] M′[valR⃗/x⃗,\overline{k⃗}/u⃗] ]
⇒_{l} [ S⃗, throw v[\overline{k⃗}/u⃗] ∗, M′[valR⃗/x⃗,\overline{k⃗}/u⃗] ]
⇒_{l}^{∗} [ S⃗, throw v[\overline{k⃗}/u⃗] ∗, S⃗′, throw \overline{k}_{j} ∗, val Q].

Similarly in the second case, for some Q such that \overline{Q} = V,

[ S⃗, (throw v M′)[valR⃗/x⃗,\overline{k⃗}/u⃗] ] = [ S⃗, throw \overline{k}_{j} M′[valR⃗/x⃗,\overline{k⃗}/u⃗] ]
⇒_{l} [ S⃗, throw \overline{k}_{j} ∗, M′[valR⃗/x⃗,\overline{k⃗}/u⃗] ]
⇒_{l}^{∗} [ S⃗, throw \overline{k}_{j} ∗, val Q ],

by the induction hypothesis.

Case 5: M = catch v M′ for some v and M′. We can assume that v ≠ u_{i} for any i. First, suppose that M[\overline{R⃗}/x⃗] ≻_{CBV} V. By the definition of rewriting rules,

1. M′[\overline{R⃗}/x⃗] ≻_{CBV} V, or

2. M′[\overline{R⃗}/x⃗] ≻_{CBV} C′[throw v V] for some C′ which does not capture v.

In the first case, since len(M′[\overline{R⃗}/x⃗]) < len(M[\overline{R⃗}/x⃗]), by the induction hypothesis, for some Q such that \overline{Q} = V,

[ S⃗, (catch v M′)[valR⃗/x⃗,\overline{k⃗}/u⃗] ] = [ S⃗, catch v M′[valR⃗/x⃗,\overline{k⃗}/u⃗] ]
⇒_{l} [ S⃗, M′[valR⃗/x⃗,\overline{k⃗}/u⃗, \overline{l}/v] ]
⇒_{l}^{∗} [ S⃗, val Q ].

Similarly in the second case, since len(M′[\overline{R⃗}/x⃗]) < len(M[\overline{R⃗}/x⃗]),

[ S⃗, (catch v M′)[valR⃗/x⃗,\overline{k⃗}/u⃗] ] = [ S⃗, catch v M′[valR⃗/x⃗,\overline{k⃗}/u⃗] ]
⇒_{l} [ S⃗, M′[valR⃗/x⃗,\overline{k⃗}/u⃗, \overline{l}/v] ]
⇒_{l}^{∗} [ S⃗, S⃗′, throw \overline{l} ∗, val Q ]
⇒_{l} [ S⃗, val Q ]

for some S⃗′ and Q such that \overline{Q} = V.

Next suppose that M[\overline{R⃗}/x⃗] ≻_{CBV} C[throw u_{j} V]. Since C[throw u_{j} V] is not a value, M′[\overline{R⃗}/x⃗] ≻_{CBV} C′[throw u_{j} V] and C = catch v C′ for some C′. Since len(M′[\overline{R⃗}/x⃗]) = len(M[\overline{R⃗}/x⃗]) and |M′[\overline{R⃗}/x⃗]| < |M[\overline{R⃗}/x⃗]|,

[ S⃗, (catch v M′)[valR⃗/x⃗,\overline{k⃗}/u⃗] ] = [ S⃗, catch v M′[valR⃗/x⃗,\overline{k⃗}/u⃗] ]
⇒_{l} [ S⃗, catch v ∗, M′[valR⃗/x⃗,\overline{k⃗}/u⃗, \overline{l}/v] ]
⇒_{l}^{∗} [ S⃗, catch v ∗, S⃗′, throw \overline{k}_{j} ∗, val Q ]

for some S⃗′ and Q such that \overline{Q} = V by the induction hypothesis.

Case 6: M = κ v. M′ for some v and M′. We can assume that v ≠ u_{i} for any i. First, suppose that M[\overline{R⃗}/x⃗] ≻_{CBV} V. By the definition of rewriting rules, for some V′,

1. M′[\overline{R⃗}/x⃗] ≻_{CBV} V′ and V = κ v. V′, or

2. M′[\overline{R⃗}/x⃗] ≻_{CBV} C′[throw v V′] and V = κ v. throw v V′ for some C′ which does not capture v.

In the first case, len(M′[\overline{R⃗}/x⃗]) = len(M[\overline{R⃗}/x⃗]) and |M′[\overline{R⃗}/x⃗]| < |M[\overline{R⃗}/x⃗]|. Therefore by the induction hypothesis, for some Q′ such that \overline{Q}′ = V′,

[ S⃗, (κ v. M′)[valR⃗/x⃗,\overline{k⃗}/u⃗] ]
= [ S⃗, κ v. M′[valR⃗/x⃗,\overline{k⃗}/u⃗] ]
⇒_{l} [ S⃗, κ v. throw v ∗, throw \overline{l} ∗, κ v. ∗, M′[valR⃗/x⃗,\overline{k⃗}/u⃗, \overline{l+1}/v] ]
⇒_{l}^{∗} [ S⃗, κ v. throw v ∗, throw \overline{l} ∗, κ v. ∗, val Q′ ]
⇒_{l} [ S⃗, κ v. throw v ∗, throw \overline{l} ∗, val (κ v. val Q′) ]
⇒_{l} [ S⃗, val (κ v. val Q′) ].

Let Q be as Q = κ v. val Q′, Then we get \overline{Q} = κ v. \overline{Q}′ = κ v. V′ = V. In the second case, len(M′[\overline{R⃗}/x⃗]) ≤ len(M[\overline{R⃗}/x⃗]) and |M′[\overline{R⃗}/x⃗]| < |M[\overline{R⃗}/x⃗]|. Therefore,

[ S⃗, (κ v. M′)[valR⃗/x⃗,\overline{k⃗}/u⃗] ]
⇒_{l} [ S⃗, κ v. throw v ∗, throw \overline{l} ∗, κ v. ∗, M′[valR⃗/x⃗,\overline{k⃗}/u⃗, \overline{l+1}/v] ]
⇒_{l}^{∗} [ S⃗, κ v. throw v ∗, throw \overline{l} ∗, κ v. ∗, S⃗′′, throw \overline{l+1} ∗, val Q′ ]
⇒_{l} [ S⃗, κ v. throw v ∗, val Q′ ]
⇒_{l} [ S⃗, val (κ v. throw v (val Q′)) ]

for some S⃗′′ and Q′ such that \overline{Q}′ = V′ by the induction hypothesis. Let Q be as Q = κ v. throw v (val Q′), Then we get \overline{Q} = κ v. throw v \overline{Q}′ = κ v. throw v V′ = V.

Next suppose that M[\overline{R⃗}/x⃗] ≻_{CBV} C[throw u_{j} V]. By the definition of rewriting rules, there exists some C′ such that M′[\overline{R⃗}/x⃗] ≻_{CBV} C′[throw u_{j} V] and C = κ v. C′. Note that C′ does not capture u_{j}. Since len(M′[\overline{R⃗}/x⃗]) = len(M[\overline{R⃗}/x⃗]) and |M′[\overline{R⃗}/x⃗]| < |M[\overline{R⃗}/x⃗]|,

[ S⃗, (κ v. M′)[valR⃗/x⃗,\overline{k⃗}/u⃗] ]
⇒_{l} [ S⃗, κ v. throw v ∗, throw \overline{l} ∗, κ v. ∗, M′[valR⃗/x⃗,\overline{k⃗}/u⃗, \overline{l+1}/v] ]
⇒_{l}^{∗} [ S⃗, κ v. throw v ∗, throw \overline{l} ∗, κ v. ∗, S⃗′′, throw \overline{k}_{j} ∗, val Q ]

for some S⃗′′ and Q such that \overline{Q} = V by the induction hypothesis.

Case 7: M = M′v for some M′ and v. First, suppose that M[\overline{R⃗}/x⃗] ≻_{CBV} V. By the definition of rewriting rules, for some w,

M′[\overline{R⃗}/x⃗] ≻_{CBV} κ w. V.

Since len(M′[\overline{R⃗}/x⃗]) < len(M[\overline{R⃗}/x⃗]), by the induction hypothesis, for some Q such that \overline{Q} = V,

[ S⃗, (M′v)[valR⃗/x⃗,\overline{k⃗}/u⃗] ] = [ S⃗, M′[valR⃗/x⃗,\overline{k⃗}/u⃗] v[\overline{k⃗}/u⃗] ]
⇒_{l} [ S⃗, ∗ v[\overline{k⃗}/u⃗], M′[valR⃗/x⃗,\overline{k⃗}/u⃗] ]
⇒_{l}^{∗} [ S⃗, ∗ v[\overline{k⃗}/u⃗], val (κ w. val Q) ]
⇒_{l} [ S⃗, (val Q)[v[\overline{k⃗}/u⃗]/w] ]
= [ S⃗, val Q ].

Next suppose that M[\overline{R⃗}/x⃗] ≻_{CBV} C[throw u_{j} V]. By the definition of rewriting rules,

1. M′[\overline{R⃗}/x⃗] ≻_{CBV} C′[throw u_{j} V] and C = C′v for some C′, or

2. M′[\overline{R⃗}/x⃗] ≻_{CBV} κ w. throw w V for some w and v = u_{j}. In the first case, len(M′[\overline{R⃗}/x⃗]) = len(M[\overline{R⃗}/x⃗]) and |M′[\overline{R⃗}/x⃗]| < |M[\overline{R⃗}/x⃗]|. Therefore,

[ S⃗, (M′v)[valR⃗/x⃗,\overline{k⃗}/u⃗] ]

⇒_{l} [ S⃗, ∗ v[\overline{k⃗}/u⃗], M′[valR⃗/x⃗,\overline{k⃗}/u⃗] ]
⇒_{l}^{∗} [ S⃗, ∗ v[\overline{k⃗}/u⃗], S⃗′, throw \overline{k}_{j} ∗, val Q ]

for some S⃗′ and Q such that \overline{Q} = V by the induction hypothesis. Similarly in the second case,

[ S⃗, (M′v)[valR⃗/x⃗,\overline{k⃗}/u⃗] ] = [ S⃗, M′[valR⃗/x⃗,\overline{k⃗}/u⃗] \overline{k}_{j} ]
⇒_{l} [ S⃗, ∗ \overline{k}_{j}, M′[valR⃗/x⃗,\overline{k⃗}/u⃗] ]
⇒_{l}^{∗} [ S⃗, ∗ \overline{k}_{j}, val (κ w. throw w (val Q)) ]
⇒_{l} [ S⃗, throw \overline{k}_{j} (val Q) ]
⇒_{l} [ S⃗, throw \overline{k}_{j} ∗, val Q ].

Case 8: M = λ y. M′ for some y and M′. Since M[\overline{R⃗}/x⃗] ≻_{CBV} λ y. (M′[\overline{R⃗}/x⃗]), we get M[\overline{R⃗}/x⃗] / ; ≻_{CBV} C[throw u_{j} V]. Suppose that M[\overline{R⃗}/x⃗] ≻_{CBV} V, i.e., V = λ y. (M′[\overline{R⃗}/x⃗]). Since F T V (λ y. M′) = \{\}, we get (λ y. M′)[val R⃗/x⃗,\overline{k⃗}/u⃗] = λ y. (M′[val R⃗/x⃗]). Therefore, [ S⃗, M[val R⃗/x⃗,\overline{k⃗}/u⃗] ] ⇒_{l} [ S⃗, val Q ], where Q = λ y. (M′[valR⃗/x⃗]), and \overline{Q} = λ y. (M′[\overline{R⃗}/x⃗]) by Proposition 3.1.8. Case 9: M has one of other forms. Similar. Lemma 3.2.5 Let S⃗ be a sequence of context segments whose length is l, and let e be an internal term. If [ S⃗, e ] ⇒_{l}^{∗} [ S⃗, S⃗′, e′ ] for some S⃗′ and e′, then for any tag constant \overline{m} occurring in S⃗′ or e′, m < l implies that \overline{m} occurs in e. Proof. By induction on the length of the path of [ S⃗, e ] ⇒_{l}^{∗} [ S⃗, S⃗′, e′ ]. Each step is obvious from the definition of transition rules.

Lemma 3.2.6 Let S⃗ be a sequence of context segments whose length is l. Let u_{1}, …, u_{n} be tag variables, and \overline{k}_{1}, …, \overline{k}_{n} tag constants. Let M be a term such that F IV (M) = \{\} and F T V (M) ⊂ {u_{1}, …, u_{n}}. If

[ S⃗, M[\overline{k}_{1}/u_{1}, …, \overline{k}_{n}/u_{n}] ] ⇒^{∗} [ S⃗′, e ]

for some S′ and e, then

1. [ S⃗, M[\overline{k}_{1}/u_{1}, …, \overline{k}_{n}/u_{n}] ] ⇒_{l}^{∗} [ S⃗′, e ],

2. [ S⃗, M[\overline{k}_{1}/u_{1}, …, \overline{k}_{n}/u_{n}] ] ⇒_{l}^{∗} [ S⃗, val Q ] for some Q, or

3. [ S⃗, M[\overline{k}_{1}/u_{1}, …, \overline{k}_{n}/u_{n}] ] ⇒_{l}^{∗} [ S⃗, …, throw \overline{k}_{j} ∗, val Q ] and k_{j} < l for some Q and j.

Proof. Assume that [ S⃗, M[\overline{k}_{1}/u_{1}, …, \overline{k}_{n}/u_{n}] ] / ⇒_{l}^{∗} [ S⃗′, e ], and let [ S⃗′′, e′ ] be the final state of [ S⃗, M[\overline{k}_{1}/u_{1}, …, \overline{k}_{n}/u_{n}] ] w.r.t. ⇒_{l}, which is not a final state w.r.t. ⇒ since [ S⃗, M[\overline{k}_{1}/u_{1}, …, \overline{k}_{n}/u_{n}] ] ⇒^{∗} [ S⃗′, e ]. Therefore, a transition rule is applicable to the state. By the definition of transition rules,

1. [ S⃗′′, e′ ] = [ S⃗, val Q ] for some Q, or

2. [ S⃗′′, e′ ] = [ S⃗, …, throw \overline{m} ∗, val Q ] for some Q and m such that m < l.

We get m = k_{j} for some j by Lemma 3.2.5 in the latter case.

Lemma 3.2.7 Let S⃗ and S⃗′ be sequences of context segments whose lengths are l and m, respectively. Let u_{1}, …, u_{n} be tag variables, and \overline{k}_{1}, …, \overline{k}_{n} tag constants. Let M be a term such that F IV (M) = {} and F T V (M) ⊂ {u_{1}, …, u_{n}}. If

[ S⃗, S⃗′, M[\overline{k}_{1}/u_{1}, …, \overline{k}_{n}/u_{n}] ] ⇒^{∗} [ S⃗, val Q ]

for some Q, then

1. [ S⃗, S⃗′, M[\overline{k}_{1}/u_{1}, …, \overline{k}_{n}/u_{n}] ] ⇒_{l+m}^{∗} [ S⃗, S⃗′, val Q′ ] for some Q′, or

2. [ S⃗, S⃗′, M[\overline{k}_{1}/u_{1}, …, \overline{k}_{n}/u_{n}] ] ⇒_{l+m}^{∗} [ S⃗, S⃗′, …, throw \overline{k}_{j} ∗, val Q′ ] and l ≤ k_{j} < l + m

for some Q′ and j.

Proof. Suppose that [ S⃗, S⃗′, M[\overline{k}_{1}/u_{1}, …, \overline{k}_{n}/u_{n}] ] ⇒^{∗} [ S⃗, val Q ]. By Lemma 3.2.6,

1. [ S⃗, S⃗′, M[\overline{k}_{1}/u_{1}, …, \overline{k}_{n}/u_{n}] ] ⇒_{l+m}^{∗} [ S⃗, val Q ],

2. [ S⃗, S⃗′, M[\overline{k}_{1}/u_{1}, …, \overline{k}_{n}/u_{n}] ] ⇒_{l+m}^{∗} [ S⃗, S⃗′, val Q′ ] for some Q′, or

3. [ S⃗, S⃗′, M[\overline{k}_{1}/u_{1}, …, \overline{k}_{n}/u_{n}] ] ⇒_{l+m}^{∗} [ S⃗, S⃗′, …, throw \overline{k}_{j} ∗, val Q′ ] and k_{j} < l + m for

some Q′ and j.

In the first case, we get m = 0 by the definition of ⇒_{l+m}^{∗}. Therefore, [ S⃗, val Q ] = [ S⃗, S⃗′, val Q ]. Trivial in the second case. In the third case, it is enough to show that l ≤ k_{j}. Since [ S⃗, val Q ] is a final state w.r.t. ⇒_{l}, we get that [ S⃗, S⃗′, …, throw \overline{k}_{j} ∗, val Q′ ] is not a final state w.r.t. ⇒_{l}. Therefore we get l ≤ k_{j}.

Lemma 3.2.8 Let S⃗ be a sequence of context segments whose length is l. Let u_{1}, …, u_{n} be tag variables, and \overline{k}_{1}, …, \overline{k}_{n} tag constants. Let M be a term such that F IV (M) = \{\} and

F T V (M) ⊂ \{u_{1}, …, u_{n}\}. If [ S⃗, M[\overline{k}_{1}/u_{1}, …, \overline{k}_{n}/u_{n}] ] ⇒^{∗} [ S⃗′, throw \overline{q} ∗, val Q ] for some

S⃗′, Q and q such that q < l, then

1. [ S⃗, M[\overline{k}_{1}/u_{1}, …, \overline{k}_{n}/u_{n}] ] ⇒_{l}^{∗} [ S⃗, val Q′ ] for some Q′, or

2. [ S⃗, M[\overline{k}_{1}/u_{1}, …, \overline{k}_{n}/u_{n}] ] ⇒_{l}^{∗} [ S⃗, …, throw \overline{q} ∗, val Q ].

Proof. Suppose that [ S⃗, M[\overline{k}_{1}/u_{1}, …, \overline{k}_{n}/u_{n}] ] ⇒^{∗} [ S⃗′, throw \overline{q} ∗, val Q ] and q < l. By Lemma 3.2.6,

1. [ S⃗, M[\overline{k}_{1}/u_{1}, …, \overline{k}_{n}/u_{n}] ] ⇒_{l}^{∗} [ S⃗′, throw \overline{q} ∗, val Q ],

2. [ S⃗, M[\overline{k}_{1}/u_{1}, …, \overline{k}_{n}/u_{n}] ] ⇒_{l}^{∗} [ S⃗, val Q′ ] for some Q′, or

3. [ S⃗, M[\overline{k}_{1}/u_{1}, …, \overline{k}_{n}/u_{n}] ] ⇒_{l}^{∗} [ S⃗, …, throw \overline{k}_{j} ∗, val Q′ ] and k_{j} < l for some Q′ and j.

In the first case, let m be the length of S⃗′. Trivial if l ≤ m. Otherwise we get [ S⃗′, throw \overline{q} ∗, val Q ] = [ S⃗, val Q ] from the definition of ⇒_{l}. Trivial in the the second case. In the third case, since k_{j} < l, [ S⃗, …, throw \overline{k}_{j} ∗, val Q′ ] is a final state w.r.t. ⇒_{l} as well as [ S⃗, …, throw \overline{q} ∗, val Q ]. Therefore, k_{j} = q and Q′ = Q.

Theorem 3.2.9 Let S⃗ be a sequence of context segments whose lengths is l. Let x_{1}, …, x_{m} be individual variables, and R_{1}, …, R_{m} internal values. Let u_{1}, …, u_{n} be tag variables, and \overline{k}_{1}, …, \overline{k}_{n} tag constants such that k_{i} ≤ l for any i. Let M be a term such that F IV (M) ⊂ \{x_{1}, …, x_{m}\} and F T V (M) ⊂ \{u_{1}, …, u_{n}\}. Let M[\overline{R⃗}/x⃗] and M[val R⃗/x⃗,\overline{k⃗}/u⃗] be abbreviations for M[\overline{R}_{1}/x_{1}, …, \overline{R}_{m}/x_{m}] and M[val R_{1}/x_{1}, …, val R_{m}/x_{m}, \overline{k}_{1}/u_{1}, …, \overline{k}_{n}/u_{n}], respectively. Let Q be an internal value.

1. If [ S⃗, M[valR⃗/x⃗,\overline{k⃗}/u⃗] ] ⇒_{l}^{∗} [ S⃗, val Q ], then

M[\overline{R⃗}/x⃗] ≻_{CBV} \overline{Q} or M[\overline{R⃗}/x⃗] ≻_{CBV} C[throw u_{j} \overline{Q}]

for some j and C such that k_{j} = l and C does not capture u_{j}.

2. If [ S⃗, M[valR⃗/x⃗,\overline{k⃗}/u⃗] ] ⇒_{l}^{∗} [ S⃗, …, throw \overline{q} ∗, val Q ] for some q such that q < l, then

M[\overline{R⃗}/x⃗] ≻_{CBV} C[throw u_{j} \overline{Q}]

for some j and C such that q = k_{j} and C does not capture u_{j}.

Proof. By induction on the lengths of the following transition paths.

[ S⃗, M[valR⃗/x⃗,\overline{k⃗}/u⃗] ] ⇒_{l}^{∗} [ S⃗, val Q ]  (3.1)
[ S⃗, M[valR⃗/x⃗,\overline{k⃗}/u⃗] ] ⇒_{l}^{∗} [ S⃗, …, throw \overline{q} ∗, val Q ]  (3.2)

By cases according to the form of M.

Case 1: M is an individual constant. Trivial since [ S⃗, M[val R⃗/x⃗,\overline{k⃗}/u⃗] ] = [ S⃗, M ] ⇒_{l} [ S⃗, val M ] and M ≻_{CBV} M = \overline{M}.

Case 2: M is an individual variable. Suppose that

[ S⃗, M[valR⃗/x⃗,\overline{k⃗}/u⃗] ] ⇒_{l}^{∗} [ S⃗, …, val Q ].

Since M = x_{i} for some i, we get M[val R⃗/x⃗,\overline{k⃗}/u⃗] = val R_{i}. That is, [ S⃗, M[val R⃗/x⃗,\overline{k⃗}/u⃗] ] is a final state w.r.t. ⇒_{l}. Therefore (3.2) does not hold. Suppose that (3.1) holds. In this case, Q = R_{i}. Therefore, M[\overline{R⃗}/x⃗] = \overline{R}_{i} ≻_{CBV} \overline{R}_{i} = \overline{Q}.

Case 3: M = let y=M_{1}. M_{2} for some y, M_{1} and M_{2}. We can assume that y ≠ x_{i} for any i. Let S_{l+1} be as S_{l+1} = let y=∗. M_{2}[valR⃗/x⃗,\overline{k⃗}/u⃗]. By the definition of transition rules,

[ S⃗, (let y=M_{1}. M_{2})[valR⃗/x⃗,\overline{k⃗}/u⃗] ]
= [ S⃗, let y=M_{1}[valR⃗/x⃗,\overline{k⃗}/u⃗]. M_{2}[valR⃗/x⃗,\overline{k⃗}/u⃗] ]
⇒_{l} [ S⃗, S_{l+1}, M_{1}[valR⃗/x⃗,\overline{k⃗}/u⃗] ].

First, suppose (3.1), i.e., [ S⃗, S_{l+1}, M_{1}[valR⃗/x⃗,\overline{k⃗}/u⃗] ] ⇒_{l}^{∗} [ S⃗, val Q ]. By Lemma 3.2.7,

1. [ S⃗, S_{l+1}, M_{1}[valR⃗/x⃗,\overline{k⃗}/u⃗] ] ⇒_{l+1}^{∗} [ S⃗, S_{l+1}, val Q′ ] for some Q′, or

2. [ S⃗, S_{l+1}, M_{1}[val R⃗/x⃗,\overline{k⃗}/u⃗] ] ⇒_{l+1}^{∗} [ S⃗, S_{l+1}, …, throw \overline{k}_{i} ∗, val Q′ ] and k_{i} = l for some

Q′ and i.

In the first case, since k_{j} < l + 1 for any j, we get M_{1}[\overline{R⃗}/x⃗] ≻_{CBV} \overline{Q}′ by the induction hypothesis. On the other hand,

[ S⃗, M[valR⃗/x⃗,\overline{k⃗}/u⃗] ] ⇒_{l} [ S⃗, S_{l+1}, M_{1}[valR⃗/x⃗,\overline{k⃗}/u⃗] ]
⇒_{l+1}^{∗} [ S⃗, S_{l+1}, val Q′ ]
⇒_{l} [ S⃗, M_{2}[valR⃗/x⃗, val Q′/y,\overline{k⃗}/u⃗] ].

Therefore, we get [ S⃗, M_{2}[val R⃗/x⃗, val Q′/y,\overline{k⃗}/u⃗] ] ⇒_{l}^{∗} [ S⃗, val Q ] by (3.1). By the induction hypothesis again, we get M_{2}[\overline{R⃗}/x⃗, \overline{Q}′/y] ≻_{CBV} \overline{Q} or M_{2}[\overline{R⃗}/x⃗, \overline{Q}′/y] ≻_{CBV} C[throw u_{j} \overline{Q}] for some j and C such that k_{j} = l and C does not capture u_{j}. That is,

M[\overline{R⃗}/x⃗] = let y=M_{1}[\overline{R⃗}/x⃗]. M_{2}[\overline{R⃗}/x⃗]
⟶_{CBV}^{∗} let y=\overline{Q}′. M_{2}[\overline{R⃗}/x⃗]
⟶_{CBV} M_{2}[\overline{R⃗}/x⃗, \overline{Q}′/y]
≻_{CBV}  \overline{Q} or C[throw u_{j} \overline{Q}].

In the second case,

[ S⃗, M[valR⃗/x⃗,\overline{k⃗}/u⃗] ] ⇒_{l} [ S⃗, S_{l+1}, M_{1}[valR⃗/x⃗,\overline{k⃗}/u⃗] ]
⇒_{l+1}^{∗} [ S⃗, S_{l+1}, …, throw \overline{l} ∗, val Q′ ]
⇒_{l} [ S⃗, val Q′ ].

Since [ S⃗, val Q′ ] is a final state w.r.t ⇒_{l}, we get Q′ = Q from (3.1). That is,

[ S⃗, S_{l+1}, M_{1}[valR⃗/x⃗,\overline{k⃗}/u⃗] ] ⇒_{l+1}^{∗} [ S⃗, S_{l+1}, …, throw \overline{l} ∗, val Q ].

By the induction hypothesis, we get M_{1}[\overline{R⃗}/x⃗] ≻_{CBV} C′[throw u_{j} \overline{Q}] for some j and C′ such that l = k_{j} and C′ does not capture u_{j}. Therefore,

M[\overline{R⃗}/x⃗] = let y=M_{1}[\overline{R⃗}/x⃗]. M_{2}[\overline{R⃗}/x⃗]
⟶_{CBV}^{∗} let y=C′[throw u_{j} \overline{Q}]. M_{2}[\overline{R⃗}/x⃗]
= C[throw u_{j} \overline{Q}],

where C = let y=C′. M_{2}[\overline{R⃗}/x⃗], which does not capture u_{j}.

Next suppose that q < l and (3.2), i.e.,

[ S⃗, M[valR⃗/x⃗,\overline{k⃗}/u⃗] ] ⇒_{l} [ S⃗, S_{l+1}, M_{1}[valR⃗/x⃗,\overline{k⃗}/u⃗] ]
⇒_{l}^{∗} [ S⃗, …, throw \overline{q} ∗, val Q ].

By Lemma 3.2.8,

1. [ S⃗, S_{l+1}, M_{1}[valR⃗/x⃗,\overline{k⃗}/u⃗] ] ⇒_{l+1}^{∗} [ S⃗, S_{l+1}, val Q′ ] for some Q′, or

2. [ S⃗, S_{l+1}, M_{1}[valR⃗/x⃗,\overline{k⃗}/u⃗] ] ⇒_{l+1}^{∗} [ S⃗, S_{l+1}, …, throw \overline{q} ∗, val Q ].

In the first case, since k_{j} < l + 1 for any j, we get M_{1}[\overline{R⃗}/x⃗] ≻_{CBV} \overline{Q}′ by the induction hypothesis. On the other hand,

[ S⃗, M[valR⃗/x⃗,\overline{k⃗}/u⃗] ] ⇒_{l}^{∗} [ S⃗, S_{l+1}, val Q′ ]
⇒_{l} [ S⃗, M_{2}[valR⃗/x⃗, val Q′/y,\overline{k⃗}/u⃗] ].

Therefore, [ S⃗, M_{2}[val R⃗/x⃗, val Q′/y,\overline{k⃗}/u⃗] ] ⇒_{l}^{∗} [ S⃗, …, throw \overline{q} ∗, val Q ] by (3.2). By the induction hypothesis, we get M_{2}[\overline{R⃗}/x⃗, \overline{Q}/y] ≻_{CBV} C[throw u_{j} \overline{Q}] for some j and C such that q = k_{j} and C does not capture u_{j}. Therefore,

M[\overline{R⃗}/x⃗] = let y=M_{1}[\overline{R⃗}/x⃗]. M_{2}[\overline{R⃗}/x⃗]
⟶_{CBV}^{∗} let y=\overline{Q}′. M_{2}[\overline{R⃗}/x⃗]
⟶_{CBV} M_{2}[\overline{R⃗}/x⃗, \overline{Q}′/y]
≻_{CBV} C[throw u_{j} \overline{Q}].

In the second case, we get M_{1}[\overline{R⃗}/x⃗] ≻_{CBV} C′[throw u_{j} \overline{Q}] for some j and C′ such that q = k_{j} and C′ does not capture u_{j}, by the induction hypothesis. Therefore,

M[\overline{R⃗}/x⃗] = let y=M_{1}[\overline{R⃗}/x⃗]. M_{2}[\overline{R⃗}/x⃗]
≻_{CBV} let y=C′[throw u_{j} \overline{Q}]. M_{2}[\overline{R⃗}/x⃗]
= C[throw u_{j} \overline{Q}],

where C = let y=C′. M_{2}[\overline{R⃗}/x⃗], which does not capture u_{j}.

Case 4: M = throw v M′ for some v and M′. Since F T V (M) ⊂ {u_{1}, …, u_{n}}, we get v = u_{p} for some p. Let S_{l+1} be as S_{l+1} = throw \overline{k}_{p} ∗. By the definition of transition rules,

[ S⃗, (throw v M′)[valR⃗/x⃗,\overline{k⃗}/u⃗] ] = [ S⃗, throw \overline{k}_{p} M′[valR⃗/x⃗,\overline{k⃗}/u⃗] ]
⇒_{l} [ S⃗, S_{l+1}, M′[valR⃗/x⃗,\overline{k⃗}/u⃗] ].

First, suppose (3.1), i.e., [ S⃗, S_{l+1}, M′[valR⃗/x⃗,\overline{k⃗}/u⃗] ] ⇒_{l}^{∗} [ S⃗, val Q ]. By Lemma 3.2.7,

1. [ S⃗, S_{l+1}, M′[valR⃗/x⃗,\overline{k⃗}/u⃗] ] ⇒_{l+1}^{∗} [ S⃗, S_{l+1}, val Q′ ] for some Q′, or

2. [ S⃗, S_{l+1}, M′[val R⃗/x⃗,\overline{k⃗}/u⃗] ] ⇒_{l+1}^{∗} [ S⃗, S_{l+1}, …, throw \overline{k}_{i} ∗, val Q′ ] and k_{i} = l for some

Q′ and i.

In the first case, since k_{j} < l + 1 for any j, we get M′[\overline{R⃗}/x⃗] ≻_{CBV} \overline{Q}′ by the induction hypothesis. Therefore,

M[\overline{R⃗}/x⃗] = throw u_{p} M′[\overline{R⃗}/x⃗] ≻_{CBV} throw u_{p} \overline{Q}′.

On the other hand, [ S⃗, S_{l+1}, val Q′ ] ⇒_{l}^{∗} [ S⃗, val Q ] by (3.1). Therefore, we get k_{p} = l and Q = Q′. In the second case, since k_{i} = l,

[ S⃗, M[valR⃗/x⃗,\overline{k⃗}/u⃗] ] ⇒_{l} [ S⃗, S_{l+1}, M′[valR⃗/x⃗,\overline{k⃗}/u⃗] ]
⇒_{l+1}^{∗} [ S⃗, S_{l+1}, …, throw \overline{l} ∗, val Q′ ]
⇒_{l} [ S⃗, val Q′ ].

Therefore, Q′ = Q by (3.1), i.e.,

[ S⃗, S_{l+1}, M′[valR⃗/x⃗,\overline{k⃗}/u⃗] ] ⇒_{l+1}^{∗} [ S⃗, S_{l+1}, …, throw \overline{l} ∗, val Q ].

By the induction hypothesis, we get M′[\overline{R⃗}/x⃗] ≻_{CBV} C′[throw u_{j} \overline{Q}] for some j and C′ such that l = k_{j} and C′ does not capture u_{j}. Therefore,

M[\overline{R⃗}/x⃗] = throw u_{p} M′[\overline{R⃗}/x⃗]
⟶_{CBV}^{∗} throw u_{p} C′[throw u_{j} \overline{Q}]
= C[throw u_{j} \overline{Q}],

where C = throw u_{p} C′, which does not capture u_{j}.

Next suppose that q < l and (3.2), i.e.,

[ S⃗, M[valR⃗/x⃗,\overline{k⃗}/u⃗] ] ⇒_{l} [ S⃗, S_{l+1}, M′[valR⃗/x⃗,\overline{k⃗}/u⃗] ]
⇒_{l}^{∗} [ S⃗, …, throw \overline{q} ∗, val Q ].

By Lemma 3.2.8,

1. [ S⃗, S_{l+1}, M′[valR⃗/x⃗,\overline{k⃗}/u⃗] ] ⇒_{l+1}^{∗} [ S⃗, S_{l+1}, val Q′ ] for some Q′, or

2. [ S⃗, S_{l+1}, M′[valR⃗/x⃗,\overline{k⃗}/u⃗] ] ⇒_{l+1}^{∗} [ S⃗, S_{l+1}, …, throw \overline{q} ∗, val Q ].

In the first case, since k_{j} < l + 1 for any j, we get M′[\overline{R⃗}/x⃗] ≻_{CBV} \overline{Q}′ by the induction hypothesis. Therefore,

M[\overline{R⃗}/x⃗] = throw u_{p} M′[\overline{R⃗}/x⃗] ≻_{CBV} throw u_{p} \overline{Q}′.

On the other hand, [ S⃗, S_{l+1}, val Q′ ] ⇒_{l}^{∗} [ S⃗, …, throw \overline{q} ∗, val Q ] by (3.2). Therefore we get q = k_{p} and Q′ = Q. In the second case, we get M′[\overline{R⃗}/x⃗] ≻_{CBV} C′[throw u_{j} \overline{Q}] for some j and C′ such that q = k_{j} and C′ does not capture u_{j}, by the induction hypothesis. Therefore,

M[\overline{R⃗}/x⃗] = throw u_{p} M′[\overline{R⃗}/x⃗]
≻_{CBV} throw u_{p} C′[throw u_{j} \overline{Q}]
= C[throw u_{j} \overline{Q}],

where C = throw u_{p} C′, which does not capture u_{j}.

Case 5: M = catch v M′ for some v and M′. We can assume that v ≠ u_{i} for any i. By the definition of transition rules,

[ S⃗, (catch v M′)[valR⃗/x⃗,\overline{k⃗}/u⃗] ] = [ S⃗, catch v M′[valR⃗/x⃗,\overline{k⃗}/u⃗] ]
⇒_{l} [ S⃗, M′[valR⃗/x⃗,\overline{k⃗}/u⃗, \overline{l}/v] ].

First, suppose (3.1), i.e., [ S⃗, M′[valR⃗/x⃗,\overline{k⃗}/u⃗, \overline{l}/v] ] ⇒_{l}^{∗} [ S⃗, val Q ]. By the induction hypothesis,

1. M′[\overline{R⃗}/x⃗] ≻_{CBV} \overline{Q},

2. M′[\overline{R⃗}/x⃗] ≻_{CBV} C′[throw u_{j} \overline{Q}] and k_{j} = l for some j and C′ which does not capture u_{j}, or

3. M′[\overline{R⃗}/x⃗] ≻_{CBV} C′[throw v \overline{Q}] for some C′ which does not capture v.

In the first case,

M[\overline{R⃗}/x⃗] ⟶_{CBV}^{∗} catch v \overline{Q} ≻_{CBV}  \overline{Q}.

In the second case,

M[\overline{R⃗}/x⃗] ≻_{CBV} catch v C′[throw u_{j} \overline{Q}] = C[throw u_{j} \overline{Q}],

where C = catch v C′, which does not capture u_{j}. In the third case,

M[\overline{R⃗}/x⃗] ⟶_{CBV}^{∗} catch v C′[throw v \overline{Q}] ⟶_{CBV}^{∗} catch v (throw v \overline{Q}) ⟶_{CBV}  \overline{Q}.

Next suppose that q < l and (3.2), i.e.,

[ S⃗, M[valR⃗/x⃗,\overline{k⃗}/u⃗] ] ⇒_{l} [ S⃗, M′[valR⃗/x⃗,\overline{k⃗}/u⃗, \overline{l}/v] ]
⇒_{l}^{∗} [ S⃗, …, throw \overline{q} ∗, val Q ].

By the induction hypothesis, M′[\overline{R⃗}/x⃗] ≻_{CBV} C′[catch u_{j} \overline{Q}] and k_{j} = q for some j and C′ which does not capture u_{j}. Therefore,

M[\overline{R⃗}/x⃗] ≻_{CBV} catch v C′[throw u_{j} \overline{Q}] = C[throw u_{j} \overline{Q}],

where C = catch v C′, which does not capture u_{j}.

Case 6: M = κ v. M′ for some v and M′. We can assume that v ≠ u_{i} for any i. By the definition of transition rules,

[ S⃗, (κ v. M′)[valR⃗/x⃗,\overline{k⃗}/u⃗] ]
= [ S⃗, κ v. M′[valR⃗/x⃗,\overline{k⃗}/u⃗] ]
⇒_{l} [ S⃗, κ v. throw v ∗, throw \overline{l} ∗, κ v. ∗, M′[valR⃗/x⃗,\overline{k⃗}/u⃗, \overline{l+1}/v] ].

Let S⃗′ be as S⃗′ = κ v. throw v ∗, throw \overline{l} ∗, κ v. ∗. First, suppose (3.1), i.e., [ S⃗, S⃗′, M′[valR⃗/x⃗,\overline{k⃗}/u⃗, \overline{l+1}/v] ] ⇒_{l}^{∗} [ S⃗, val Q ]. By Lemma 3.2.7,

1. [ S⃗, S⃗′, M′[valR⃗/x⃗,\overline{k⃗}/u⃗, \overline{l+1}/v] ] ⇒_{l+3}^{∗} [ S⃗, S⃗′, val Q′ ] for some Q′,

2. [ S⃗, S⃗′, M′[val R⃗/x⃗,\overline{k⃗}/u⃗, \overline{l+1}/v] ] ⇒_{l+3}^{∗} [ S⃗, S⃗′, …, throw \overline{k}_{i} ∗, val Q′ ] and k_{i} = l for

some Q′ and i, or

3. [ S⃗, S⃗′, M′[valR⃗/x⃗,\overline{k⃗}/u⃗, \overline{l+1}/v] ] ⇒_{l+3}^{∗} [ S⃗, S⃗′, …, throw \overline{l+1} ∗, val Q′ ] and for some Q′.

In the first case, since l + 1, k_{j} < l + 3 for any j, we get M′[\overline{R⃗}/x⃗] ≻_{CBV} \overline{Q}′ by the induction hypothesis. Therefore,

M[\overline{R⃗}/x⃗] = κ v. M′[\overline{R⃗}/x⃗] ≻_{CBV} κ v. \overline{Q}′.

On the other hand,

[ S⃗, S⃗′, val Q′ ] = [ S⃗, κ v. throw v ∗, throw \overline{l} ∗, κ v. ∗, val Q′ ]
⇒_{l} [ S⃗, κ v. throw v ∗, throw \overline{l} ∗, val (κ v. val Q′) ]
⇒_{l} [ S⃗, val (κ v. val Q′) ].

Therefore, we get Q = κ v. val Q′ by (3.1), i.e., \overline{Q} = κ v. \overline{Q}′. In the second case,

[ S⃗, M[valR⃗/x⃗,\overline{k⃗}/u⃗] ] ⇒_{l} [ S⃗, S⃗′, M′[valR⃗/x⃗,\overline{k⃗}/u⃗, \overline{l+1}/v] ]
⇒_{l+3}^{∗} [ S⃗, S⃗′, …, throw \overline{l} ∗, val Q′ ]
⇒_{l} [ S⃗, val Q′ ].

Therefore Q′ = Q by (3.1), and

[ S⃗, S⃗′, M′[valR⃗/x⃗,\overline{k⃗}/u⃗, \overline{l+1}/v] ] ⇒_{l+3}^{∗} [ S⃗, S⃗′, …, throw \overline{l} ∗, val Q ].

By the induction hypothesis, we get M′[\overline{R⃗}/x⃗] ≻_{CBV} C′[throw u_{j} \overline{Q}] for some j and C′ such that l = k_{j} and C′ does not capture u_{j}. That is,

M[\overline{R⃗}/x⃗] = κ v. M′[\overline{R⃗}/x⃗]
⟶_{CBV}^{∗} κ v. C′[throw u_{j} \overline{Q}]
= C[throw u_{j} \overline{Q}],

where C = κ v. C′, which does not capture u_{j}. In the third case, by the induction hypothesis, we get M′[\overline{R⃗}/x⃗] ≻_{CBV} C′[throw v \overline{Q}′] for some C′ which does not capture v. Therefore,

M[\overline{R⃗}/x⃗] = κ v. M′[\overline{R⃗}/x⃗]
⟶_{CBV}^{∗} κ v. C′[throw v \overline{Q}′]
≻_{CBV} κ v. throw v \overline{Q}′.

On the other hand,

[ S⃗, M[valR⃗/x⃗,\overline{k⃗}/u⃗] ]
⇒_{l} [ S⃗, S⃗′, M′[valR⃗/x⃗,\overline{k⃗}/u⃗, \overline{l+1}/v] ]
⇒_{l+3}^{∗} [ S⃗, κ v. throw v ∗, throw \overline{l} ∗, κ v. ∗, …, throw \overline{l+1} ∗, val Q′ ]
⇒_{l} [ S⃗, κ v. throw v ∗, val Q′ ]
⇒_{l} [ S⃗, val (κ v. throw v val Q′) ].

Therefore we get Q = κ v. throw v (val Q′) by (3.1), i.e., \overline{Q} = κ v. throw v \overline{Q}′.

Next, suppose that q < l and (3.2), i.e.,

[ S⃗, M[valR⃗/x⃗,\overline{k⃗}/u⃗] ] ⇒_{l} [ S⃗, S⃗′, M′[valR⃗/x⃗,\overline{k⃗}/u⃗, \overline{l+1}/v] ]
⇒_{l}^{∗} [ S⃗, …, throw \overline{q} ∗, val Q ].

By Lemma 3.2.8,

1. [ S⃗, S⃗′, M′[valR⃗/x⃗,\overline{k⃗}/u⃗, \overline{l+1}/v] ] ⇒_{l+3}^{∗} [ S⃗, S⃗′, val Q′ ] for some Q′, or

2. [ S⃗, S⃗′, M′[valR⃗/x⃗,\overline{k⃗}/u⃗, \overline{l+1}/v] ] ⇒_{l+3}^{∗} [ S⃗, S⃗′, …, throw \overline{q} ∗, val Q ].

We need not consider the first case, because in this case,

[ S⃗, M[valR⃗/x⃗,\overline{k⃗}/u⃗] ]
⇒_{l} [ S⃗, S⃗′, M′[valR⃗/x⃗,\overline{k⃗}/u⃗, \overline{l+1}/v] ]
⇒_{l+3}^{∗} [ S⃗, κ v. throw v ∗, throw \overline{l} ∗, κ v. ∗, …, throw \overline{l+1} ∗, val Q′ ]
⇒_{l} [ S⃗, κ v. throw v ∗, val Q′ ]
⇒_{l} [ S⃗, val (κ v. throw v (val Q′)) ],

and this contradicts (3.2). In the second case, we get M′[\overline{R⃗}/x⃗] ≻_{CBV} C′[throw u_{j} \overline{Q}] for some j and C such that q = k_{j} and C′ does not capture u_{j} by the induction hypothesis. Therefore,

M[\overline{R⃗}/x⃗] ≻_{CBV} κ v. C′[throw u_{j} \overline{Q}] = C[throw u_{j} \overline{Q}],

where C = κ v. C′, which does not capture u_{j}.

Case 7: M = M′v for some M′ and v. Since F T V (M) ⊂ {u_{1}, …, u_{n}}, we get v = u_{p} for some p. By the definition of transition rules,

[ S⃗, (M′v)[valR⃗/x⃗,\overline{k⃗}/u⃗] ] = [ S⃗, M′[valR⃗/x⃗,\overline{k⃗}/u⃗] \overline{k}_{p} ]
⇒_{l} [ S⃗, ∗ \overline{k}_{p}, M′[valR⃗/x⃗,\overline{k⃗}/u⃗] ].

First, suppose (3.1), i.e., [ S⃗, ∗ \overline{k}_{p}, M′[valR⃗/x⃗,\overline{k⃗}/u⃗] ] ⇒_{l}^{∗} [ S⃗, val Q ]. By Lemma 3.2.7,

1. [ S⃗, ∗ \overline{k}_{p}, M′[valR⃗/x⃗,\overline{k⃗}/u⃗] ] ⇒_{l+1}^{∗} [ S⃗, ∗ \overline{k}_{p}, val Q′ ] for some Q′, or

2. [ S⃗, ∗ \overline{k}_{p}, M′[valR⃗/x⃗,\overline{k⃗}/u⃗] ] ⇒_{l+1}^{∗} [ S⃗, ∗ \overline{k}_{p}, …, throw \overline{k}_{i} ∗, val Q′ ] and k_{i} = l for some Q′

and i.

In the first case, since k_{j} < l + 1 for any j, we get M′[\overline{R⃗}/x⃗] ≻_{CBV} \overline{Q}′ by the induction hypothesis. Therefore,

M[\overline{R⃗}/x⃗] = M′[\overline{R⃗}/x⃗] u_{p} ⟶_{CBV}^{∗} \overline{Q}′ u_{p}.

On the other hand, we get Q′ = κ w. e for some w and e from (3.1). Moreover, since Q′ is an internal value, for some Q′′,

1a. Q′ = κ w. val Q′′, or

1b. Q′ = κ w. throw w (val Q′′).

In the case of 1a,

[ S⃗, ∗ \overline{k}_{p}, val Q′ ] = [ S⃗, ∗ \overline{k}_{p}, val (κ w. val Q′′) ] ⇒_{l} [ S⃗, val Q′′ ].

We so get Q = Q′′ from (3.1). Therefore \overline{Q}′ = κ w. \overline{Q}, and

M[\overline{R⃗}/x⃗] ⟶_{CBV}^{∗} \overline{Q}′ u_{p} = (κ w. \overline{Q}) u_{p} ≻_{CBV}  \overline{Q}.

In the case of 1b,

[ S⃗, ∗ \overline{k}_{p}, val Q′ ] = [ S⃗, ∗ \overline{k}_{p}, val (κ w. throw w (val Q′′)) ]
⇒_{l} [ S⃗, throw \overline{k}_{p} (val Q′′) ]
⇒_{l} [ S⃗, throw \overline{k}_{p} ∗, val Q′′ ].

We so get k_{p} = l and Q′′ = Q from (3.1). Therefore \overline{Q}′ = κ w. throw w \overline{Q}, and

M[\overline{R⃗}/x⃗] ⟶_{CBV}^{∗} \overline{Q}′ u_{p}. = (κ w. throw w \overline{Q}) u_{p} ≻_{CBV} throw u_{p} \overline{Q}.

In the second case,

[ S⃗, M[valR⃗/x⃗,\overline{k⃗}/u⃗] ] ⇒_{l} [ S⃗, ∗ \overline{k}_{p}, M′[valR⃗/x⃗,\overline{k⃗}/u⃗] ]
⇒_{l+1}^{∗} [ S⃗, ∗ \overline{k}_{p}, …, throw \overline{l} ∗, val Q′ ]
⇒_{l} [ S⃗, val Q′ ].

We so get Q′ = Q from (3.1). Therefore,

[ S⃗, ∗ \overline{k}_{p}, M′[valR⃗/x⃗,\overline{k⃗}/u⃗] ] ⇒_{l+1}^{∗} [ S⃗, ∗ \overline{k}_{p}, …, throw \overline{l} ∗, val Q ].

By the induction hypothesis, we get M′[\overline{R⃗}/x⃗] ≻_{CBV} C′[throw u_{j} \overline{Q}] for some j and C′ such that l = k_{j} and C′ does not capture u_{j}. That is,

M[\overline{R⃗}/x⃗] = M′[\overline{R⃗}/x⃗] \overline{k}_{p}
⟶_{CBV}^{∗} C′[throw u_{j} \overline{Q}] \overline{k}_{p}
= C[throw u_{j} \overline{Q}],

where C = C′ \overline{k}_{p}, which does not capture u_{j}.

Next, suppose that q < l and (3.2), i.e.,

[ S⃗, M[valR⃗/x⃗,\overline{k⃗}/u⃗] ] ⇒_{l} [ S⃗, ∗ \overline{k}_{p}, M′[valR⃗/x⃗,\overline{k⃗}/u⃗] ]
⇒_{l}^{∗} [ S⃗, …, throw \overline{q} ∗, val Q ].

By Lemma 3.2.8,

1. [ S⃗, ∗ \overline{k}_{p}, M′[valR⃗/x⃗,\overline{k⃗}/u⃗] ] ⇒_{l+1}^{∗} [ S⃗, ∗ \overline{k}_{p}, val Q′ ] for some Q′, or

2. [ S⃗, ∗ \overline{k}_{p}, M′[valR⃗/x⃗,\overline{k⃗}/u⃗] ] ⇒_{l+1}^{∗} [ S⃗, ∗ \overline{k}_{p}, …, throw \overline{q} ∗, val Q ].

In the first case, since k_{j} < l + 1 for any j, we get M′[\overline{R⃗}/x⃗] ≻_{CBV} \overline{Q}′ by the induction hypothesis. Therefore,

M[\overline{R⃗}/x⃗] = M′[\overline{R⃗}/x⃗] u_{p} ⟶_{CBV}^{∗} \overline{Q}′ u_{p}.

On the other hand, [ S⃗, ∗ \overline{k}_{p}, val Q′ ] ⇒_{l}^{∗} [ S⃗, …, throw \overline{q} ∗, val Q ] by (3.2). Therefore, we get Q′ = κ w. throw w (val Q) for some w and q = k_{p}. That is, \overline{Q}′ = κ w. throw w \overline{Q} and

M[\overline{R⃗}/x⃗] ⟶_{CBV}^{∗} \overline{Q}′ u_{p}
= (κ w. throw w \overline{Q}) u_{p}
≻_{CBV} throw u_{p} \overline{Q}.

In the second case, we get M′[\overline{R⃗}/x⃗] ≻_{CBV} C′[throw u_{j} \overline{Q}] for some j and C such that q = k_{j} and C′ does not capture u_{j}, by the induction hypothesis. Therefore,

M[\overline{R⃗}/x⃗] = M′[\overline{R⃗}/x⃗] u_{p}
≻_{CBV} C′[throw u_{j} \overline{Q}] u_{p}
= C[throw u_{j} \overline{Q}],

where C = C′ u_{p}, which does not capture u_{j}.

Case 8: M = λ y. M′ for some y and M′. Note that M[\overline{R⃗}/x⃗] ≻_{CBV} λ y. (M′[\overline{R⃗}/x⃗]). Since F T V (λ x. M′) = \{\}, we get M[valR⃗/x⃗,\overline{k⃗}/u⃗] = λ y. (M[valR⃗/x⃗]). Therefore, by the definition of transition rules,

[ S⃗, M[valR⃗/x⃗,\overline{k⃗}/u⃗] ] ⇒_{l} [ S⃗, val (λ y. (M′[valR⃗/x⃗])) ].

So (3.2) does not hold. Suppose (3.1), i.e., Q = λ y. (M′[val R⃗/x⃗]). We get \overline{Q} = λ y. (M′[\overline{R⃗}/x⃗]) by Proposition 3.1.8.

Case 9: M has one of other forms. Similar.

Corollary 3.2.10 Let M be a closed term. Let V and Q be a value and an internal value, respectively.

1. M ≻_{CBV} V implies [ M ] ⇒^{∗} [ val Q ] for some Q such that \overline{Q} = V, and

2. [ M ] ⇒^{∗} [ val Q ] implies M ≻_{CBV} \overline{Q}.

Proof. Straightforward from Theorem 3.2.4 and Theorem 3.2.9.

3.3 Realizability by the abstract machine

We can give another realizability interpretation of the formal system in terms of the abstract machine. Theorem 3.3.1 The relation

{x_{1} : A_{1}, …, x_{m}: A_{m}} ⊢ ⊢ M : C; {u_{1} : B_{1}, …, u_{n}: B_{n}}

holds if and only if for any closed terms K_{1}, …, K_{m} such that [ K_{i} ] ⇒^{∗} [ val R_{i} ] and \overline{R}_{i} r A_{i} for some R_{i} (1 ≤ i ≤ m), for any context segments S_{1}, …, S_{l}, and for any tag constants \overline{k}_{1}, …, \overline{k}_{n} such that k_{j} < l for any j,

1. [ S_{1}, …, S_{l}, M[K⃗/x⃗,\overline{k⃗}/u⃗] ] ⇒_{l}^{∗} [ S_{1}, …, S_{l}, val Q ] and \overline{Q} r C for some Q, or

2. [ S_{1}, …, S_{l}, M[K⃗/x⃗,\overline{k⃗}/u⃗] ] ⇒_{l}^{∗} [ S_{1}, …, S_{l}, …, throw \overline{k}_{j} ∗, val Q] and \overline{Q} r B_{j} for

some j and Q, where the term M[K⃗/x⃗,\overline{k⃗}/u⃗] stands for M[K_{1}/x_{1}, …, K_{m}/x_{m}, \overline{k}_{1}/u_{1}, …, \overline{k}_{n}/u_{n}]. Proof. Straightforward from Theorem 3.2.4 and Theorem 3.2.9.

The typing system as a logic

In this chapter we discuss Lc/t^{CBV} considering it as a logic. We reformulate the typing system Lc/t^{CBV} into a sequent calculus since the logic can be easily understood when compared with LK and LJ.

4.1 A sequent calculus style formulation

We consider types as formulas. That is, we have atomic formulas, conjunctions, disjunctions, implications and exceptions. A sequent of the system is of the form

A_{1} … A_{m} → C; E_{1} … E_{n}

where m and n can be 0. It looks like a sequent of LK rather than LJ ignoring the semicolon “;” between C and E_{1} … E_{n}. Actually, its purely logical meaning is the same as LK. In this sense, the semicolon is unnecessary. But we saw that it plays a significant role for the constructive meaning of the sequent.

Definition 4.1.1 (Realizability of sequents) The sequents are interpreted as follows. Let <x_{1} … x_{m}, M, u_{1} … u_{n}> be a triple which consists of a sequence of distinct individual variables x_{1} … x_{m}, a term M and a sequence of distinct tag variables u_{1} … u_{n}. We assume that the free individual and tag variables of the term M are included in the two sequences. A triple <x_{1} … x_{m}, M, u_{1} … u_{n}> realizes A_{1} … A_{m} → C; B_{1} … B_{n} if and only if

{x_{1} : A_{1}, …, x_{m}: A_{m}} ⊢ ⊢ M : C; {u_{1} : B_{1}, …, u_{n}: B_{n}}.

Definition 4.1.2 (Inference rules) The inference rules and the corresponding realizers are as follows.

{A → A; \atop <x, x, >} (init)  {<x⃗, M_{1}, u⃗> \atop Γ_{1} → A; Δ_{1}} {<y⃗ z, M_{2}, v⃗> \atop Γ_{2} A → C; Δ_{2}} {Γ_{1} Γ_{2} → C; Δ_{1} Δ_{2} \atop <x⃗ y⃗, let z=M_{1}. M_{2}, u⃗ v⃗>} (cut)

{<x⃗ y_{1} y_{2} z⃗, M, u⃗> \atop Γ_{1} A B Γ_{2} → C; Δ} ; {Γ_{1} B A Γ_{2} → C; Δ \atop <x⃗ y_{2} y_{1} z⃗, M, u⃗>} (x→) {<x⃗, M, u⃗> \atop Γ → C; Δ} ; {Γ A → C; Δ \atop <x⃗ y, M, u⃗>} (w→) {<x⃗ y_{1} y_{2} z⃗, M, u⃗> \atop Γ_{1} A A Γ_{2} → C; Δ} ; {Γ_{1} A Γ_{2} → C; Δ \atop <x⃗ y z⃗, M[y/y_{1}, y/y_{2}], u⃗>} ; (c→)

{<x⃗, M, u⃗ v_{1} v_{2} w⃗> \atop Γ → A; Δ_{1} B C Δ_{2}} ; {Γ → A; Δ_{1} C B Δ_{2} \atop <x⃗, M, u⃗ v_{2} v_{1} w⃗>} (→x) {<x⃗, M, v⃗> \atop Γ → A; Δ} ; {Γ → A; E Δ \atop <x⃗, M, u v⃗>} (→w) {<x⃗, M, u_{1} u_{2} v⃗> \atop Γ → A; E E Δ} ; {Γ → A; E Δ \atop <x⃗, M[u/u_{1}, u/u_{2}], u v⃗>} ; (→c)

{<x⃗, M, v⃗> \atop Γ → E; Δ}

{Γ → A; E Δ \atop <x⃗, throw u M, u v⃗>}

(throw) {<x⃗, M, u v⃗> \atop Γ → A; A Δ}

{Γ → A; Δ \atop <x⃗, catch u M, v⃗>}

(catch)

{<x⃗ z, M, u⃗> \atop Γ A → C; Δ}

{Γ A ∧ B → C; Δ \atop <x⃗ y, M[proj1 y/z], u⃗>}

(∧_{1} →) {<x⃗ z, M, u⃗> \atop Γ B → C; Δ}

{Γ A ∧ B → C; Δ \atop <x⃗ y, M[proj2 y/z], u⃗>}

(∧_{2} →)

{<x⃗, M_{1}, u⃗> \atop Γ_{1} → A; Δ_{1}} {<y⃗, M_{2}, v⃗> \atop Γ_{2} → B; Δ_{2}} {Γ_{1} Γ_{2} → A ∧ B; Δ_{1} Δ_{2} \atop <x⃗ y⃗, <M_{1}, M_{2}>, u⃗ v⃗>} (→ ∧) {<x⃗ z_{1}, M_{1}, u⃗> \atop Γ_{1} A → C; Δ_{1}} {<y⃗ z_{2}, M_{2}, v⃗> \atop Γ_{2} B → C; Δ_{2}} Γ_{1} Γ_{2} A ∨ B → C; Δ_{1} Δ_{2} <x⃗ y⃗ z, case z z_{1}.M_{1} z_{2}.M_{2}, u⃗ v⃗> (∨ →)

{<x⃗, M, u⃗> \atop Γ → A; Δ} ; {Γ → A ∨ B; Δ \atop <x⃗, inj1 M, u⃗>} (→ ∨_{1})  {<x⃗, M, u⃗> \atop Γ → B; Δ} ; {Γ → A ∨ B; Δ \atop <x⃗, inj2 M, u⃗>} (→ ∨_{2})

{<x⃗, M_{1}, u⃗> \atop Γ_{1} → A; Δ_{1}} {<y⃗ z′, M_{2}, v⃗> \atop Γ_{2} B → C; Δ_{2}} {Γ_{1} Γ_{2} A ⊃ B → C; Δ_{1} Δ_{2} \atop <x⃗ y⃗ z, let z′=zM_{1} . M_{2}, u⃗ v⃗>} (⊃ →)  {<x⃗ y, M, > \atop Γ A → B;} ; {Γ → A ⊃ B; \atop <x⃗, λ y. M, >} (→ ⊃)
{<x⃗ z_{1}, M_{1}, v⃗> \atop Γ_{1} A → B; Δ_{1}} {<y⃗ z_{2}, M_{2}, w⃗> \atop Γ_{2} E → C; Δ_{2}}
Γ_{1} Γ_{2} A ◁ E → C; B Δ_{1} Δ_{2}
<x⃗ y⃗ z, let z_{2}=(catch u′ let z_{1}=zu′. throw u M_{1}). M_{2}, u v⃗ w⃗>

(◁ →)

{<x⃗, M, u v⃗> \atop Γ → A; E Δ} ; {Γ → A ◁ E; Δ \atop <x⃗, κ u. M, v⃗>} (→ ◁)

The typing system Lc/t^{CBV} is equivalent to the above sequent calculus as a logic.

Theorem 4.1.3 {x_{1} : A_{1}, …, x_{m}: A_{m}} ⊢ M : C; {u_{1} : B_{1}, …, u_{n}: B_{n}} is derivable in Lc/t^{CBV} for

some x_{1}, …, x_{m}, M, u_{1}, …, u_{n}, if and only if A_{1} … A_{m} → C; B_{1} … B_{n} is derivable in the sequent calculus.

Proof. Induction on the structure of the derivation.

If we ignore semicolons in the sequents, the inference rules are almost the same as the ones of LK. It should be noted that every right logical rule introduces a logical connective into the formula between the arrow and the semicolon, namely, the main conclusion. In the following sections we discuss the details.

4.2 The logical meaning of the new connective

First we consider the new logical connective ◁. From the logical point of view, the new connective ◁ is equivalent to ∨. The difference between them consists only in their implementations.

Definition 4.2.1 We use Ã to denote the formula obtained from a formula A by replacing every occurrence of the logical connective ◁ by ∨. If Ã = B̃, then we denote it by A ≃ B. If Γ = A_{0} … A_{n}, Δ = B_{0} … B_{n} and A_{i} ≃ B_{i} for any i (0 ≤ i ≤ n), then we denote it by Γ ≃ Δ.

Lemma 4.2.2 If A ≃ A′, then A → A′; is a derivable sequent.

Proof. Straightforward induction on the structure of the formula A. The basic idea comes from the following two derivations.

\begin{matrix}⋮ & ind. hyp. \\ A → A′; \end{matrix} ; A → A′ ∨ B′; ; (→ ∨_{1}) \begin{matrix}⋮ & ind. hyp. \\ B → B′; \end{matrix} ; B → A′ ∨ B′; ; (→ ∨_{2})

A ◁ B → A′ ∨ B′; A′ ∨ B′ (◁ →)

A ◁ B → A′ ∨ B′; (catch)

\begin{matrix}⋮ & ind. hyp. \\ A → A′; \end{matrix} \begin{matrix}⋮ & ind. hyp. \\ B → B′; \end{matrix} ; B → A′; B′ ; (throw)

A ∨ B → A′; B′ (∨ →)

A ∨ B → A′ ◁ B′; (→ ◁)

Theorem 4.2.3 If Γ → A; Δ is a derivable sequent. and if Γ ≃ Γ′, A ≃ A′ and Δ ≃ Δ′, then Γ′ → A′; Δ′ is also derivable.

Proof. Induction on the structure of the derivation of the sequent Γ → A; Δ. Apply Lemma 4.2.2 in the case that the last rule is (init).

If we identify A ◁ B with A ∨ B, the formal system can be regarded as a variant of the propositional fragment of LJ.

Theorem 4.2.4 A sequent A_{1} … A_{m} → C; is derivable in our sequent calculus if and only if Ã_{1} … Ã_{m} → C̃ is derivable in (the propositional fragment of) LJ.

Proof. The if part is trivial because the propositional fragment of LJ can be regarded as a subsystem of ours. For the only if part, prove the following lemma by induction on the structure of the derivation: If A_{1} … A_{m} → C; E_{1} … E_{n} is derivable, then Ã_{1} … Ã_{m} → C̃ ∨ Ẽ_{1} ∨ … ∨ Ẽ_{n} is derivable in (the propositional fragment of) LJ. The theorem is a corollary of the lemma.

As a corollary of the theorem, we get the disjunction property of the system.

Corollary 4.2.5 (Disjunction property) Let → A ∨ B; be a derivable sequent. Then we can derive → A; or → B; .

We should note that there is another possibility of formulation of (◁ →) as follows.

{<x⃗ z, M, v⃗> \atop Γ A → C; Δ} ; {Γ A ◁ E → C; E Δ \atop <x⃗ y, let z=y u. M, u v⃗>} ; (◁ →)

This formulation seems more natural than the original in Definition 4.1.2 from the viewpoint of realizer construction, and is equivalent to the original as long as we have (cut). But we could not get the cut-elimination theorem if we replaced the original rule by this rule.

4.3 The catch and throw mechanism as structural rules

The three right-structural rules of LK are divided into five rules, i.e., (→x), (→c), (→w), (catch) and (throw). The rules (catch) and (→c) correspond to the right-contraction rule of LK. The former introduces a catch-term. The latter means a sharing of one tag variable by two throw-terms, i.e., multiple throw-terms can be caught by one catch-term afterwards. The right-weakening rule of LK is divided into (throw) and (→w). The former corresponds to a throw-term. The latter means an introduction of a redundant tag variable. We note that the rule (→w) is a derived rule.

\begin{matrix}{<x⃗, M, v⃗> \atop Γ → A; Δ} ; Γ → E; A Δ & (throw) \\ Γ → A; E A Δ \end{matrix} ; (throw)

Γ → A; A E Δ (→x)

Γ → A; E Δ

<x⃗, catch w (throw w (throw u M)), u v⃗>

(catch)

But we adopt (→w) as a primitive rule because the realizer given above introduces a redundant throw-term, i.e., a throw-term never invoked.

We have no right-exchange rule over the semicolon, but it is also a derived rule as follows.

\begin{matrix}{<x⃗, M, u w⃗> \atop Γ → A; E Δ} ; Γ → E; A E Δ & (throw) \\ Γ → E; E A Δ \end{matrix} ; (→x)

Γ → E; A Δ

<x⃗, catch u (throw v M), v w⃗>

(catch)

In contrast to (→w), we leave it as a derived rule because there is no primitive programming construct corresponding to the rule.

4.4 The restriction on the right implication rule

As a logic, the only and significant difference from LK is that there must be exactly one formula on the right hand side of the sequent when we apply the right-implication rule (→ ⊃). This restriction is required to keep the system constructive. Roughly, our system can be regarded as the propositional fragment of LK with this restriction on the right-implication rule. If we dropped the restriction, the following anomaly would occur. Consider the following derivation of A ∨(A ⊃ B), which is not derivable in the constructive logic.

\begin{matrix}A → A; & (init) \\ A → A ∨(A ⊃ B) ; \end{matrix} ; (→ ∨_{1}) ; A → B; A ∨(A ⊃ B) ; (throw) ; → A ⊃ B; A ∨(A ⊃ B) ; (→ ⊃) ; → A ∨(A ⊃ B) ; A ∨(A ⊃ B) ; (→ ∨_{2}) ; → A ∨(A ⊃ B) ; ; (catch)

The realizer would be <, catch u (inj2 (λ x. throw u (inj1 x))), >. Note that the term is a normal form since λ x. throw u (inj1 x) is not a value. But it does not realize A ∨(A ⊃ B). The evaluation process of the term by the abstract machine would be as follows.

[ S_{1}, …, S_{l−1}, case ∗ y.e_{1} z.e_{2}, catch u (inj2 (λ x. throw u (inj1 x))) ]
⇒ [ S_{1}, …, S_{l−1}, case ∗ y.e_{1} z.e_{2}, inj2 (λ x. throw \overline{l} (inj1 x)) ]
⇒ [ S_{1}, …, S_{l−1}, case ∗ y.e_{1} z.e_{2}, inj2 ∗, λ x. throw \overline{l} (inj1 x) ]
⇒ [ S_{1}, …, S_{l−1}, case ∗ y.e_{1} z.e_{2}, inj2 ∗, val (λ x. throw \overline{l} (inj1 x)) ]
⇒ [ S_{1}, …, S_{l−1}, case ∗ y.e_{1} z.e_{2}, val (inj2 (λ x. throw \overline{l} (inj1 x))) ]
⇒ [ S_{1}, …, S_{l−1}, e_{2}[val (λ x. throw \overline{l} (inj1 x))/z] ]

Note that the tag constant \overline{l} in the last is meaningless because the corresponding evaluation context has been lost. From a computational point of view, this problem can be solved by introducing more powerful facilities for non-local exit such as call/cc of Scheme. But it affects the realizability interpretation of formulas. For example, although the realizers of disjunctions still have a certain constructive meaning, they do not always contain the information that specifies which of A ∨ B is realized by them. It should be noted that the system without the restriction becomes a classical one, and we do not have the soundness theorem or the disjunction property anymore.

LK with this kind of restriction on (→ ⊃) is known as a variant of LJ, which is essentially equivalent to LJ (cf.[18, 33, 34]). The same restriction is also required for (→ ∀)-rule in the case of predicate calculus.

4.5 The cut-elimination theorem

The (cut)-rule of our sequent calculus is redundant.

Theorem 4.5.1 (Cut-elimination) If a sequent is derivable, then we can derive it without (cut)-rule.

The proof becomes more complicated than the case of LJ/LK because there exists the special restriction to apply (→ ⊃)-rule and the new connective ◁ has been introduced. We call the following inference rules structural rules.

(x→) (c→) (w→) (→x) (→c) (→w) (throw) (catch)

Note that we count (throw) and (catch) as structural rules. Left-logical rules, right-logical rules and principal formulas of logical rules are defined in the standard manner. To prove Theorem 4.5.1, we first extend (cut)-rule as follows, and we call the extended rule (mix).

Γ_{1} → A; Δ_{1}  Γ_{2} → C; Δ_{2}

Γ_{1} (Γ_{2} − X) → C; (A Δ_{1} − X) Δ_{2} (mix)

where Γ_{1}−X stands for the sequence of formulas obtained from Γ_{1} by removing X, and A Δ_{1}−X stands for the sequence of formulas obtained from A Δ_{1} by removing X.

We now consider only derivations that involve (mix) instead of (cut) since we can use (mix) instead of (cut). It is enough to show that we can construct a derivation which does not include any (mix), i.e., a mix-free derivation. We prove the theorem by induction on the number of occurrences of (mix) in the derivation. Suppose we have a derivation Π such as

\begin{matrix}⋮ & Π_{1} \\ Γ_{1} → A; Δ_{1} \end{matrix} (r1) \begin{matrix}⋮ & Π_{2} \\ Γ_{2} → C; Δ_{2} \end{matrix} (r2)

Γ_{1} (Γ_{2} − X) → C; (A Δ_{1} − X) Δ_{2} (mix)

where Π_{1} and Π_{2} are mix-free derivations and (r1) and (r2) stand for some inference rules except (mix). We translate derivations of this form to mix-free derivations.

Definition 4.5.2 (Grades and heights) We define the grade of the (mix)-rule as the number of logical connectives such as ∧, ∨, ⊃ and ◁ occurring in X. The left height of the (mix)-rule is the maximum length of the derivation paths in Π_{1}. The right height of the (mix)-rule is the maximum length of the derivation paths in Π_{2}. The height of the (mix)-rule is the sum of the left and right heights.

Proof of the cut-elimination theorem. We translate derivations of the form of Π to mixfree derivations by induction on the lexicographic ordering of the grade and the height of the (mix)-rule. We divide the proof into the following four cases.

Case 1: The rule (r1) is not a right-logical rule whose principal formula is X. The only crucial is the subcase that (r1) is (→ ⊃) whose principal formula is not X. Since there exists a restriction to apply (→ ⊃), this case is not just a variant of other subcases. The derivation Π has the following form.

\begin{matrix}⋮ & Π_{1} \\ Γ_{1} A → B; \end{matrix} ; Γ_{1} → A ⊃ B; (→ ⊃) \begin{matrix}⋮ & Π_{2} \\ Γ_{2} → C; Δ_{2} \end{matrix} (r2)

Γ_{1} (Γ_{2} − X) → C; (A ⊃ B − X) Δ_{2} (mix)

The conclusion is identical to Γ_{1} (Γ_{2} − X) → C; A ⊃ B Δ_{2} since the principal formula A ⊃ B is not X. We can derive it applying structural rules to Γ_{1} → A ⊃ B; .

Case 2: The rule (r1) is a right-logical rule whose principal formula is X, and (r2) is (→ ⊃). This case is crucial.

Subcase 2-1: The rule (r1) is (→ ∧) whose principal formula is X, i.e., the derivation Π has the following form.

\begin{matrix}⋮ & Π_{11} \\ Γ_{11} → A_{1} ; Δ_{11} \end{matrix} \begin{matrix}⋮ & Π_{12} \\ Γ_{12} → A_{2} ; Δ_{12} \end{matrix} Γ_{11} Γ_{12} → A_{1} ∧ A_{2} ; Δ_{11} Δ_{12} (→ ∧) \begin{matrix}⋮ & Π_{2} \\ Γ_{2} C → D; \end{matrix} ; Γ_{2} → C ⊃ D; (→ ⊃)

Γ_{11} Γ_{12} (Γ_{2} − X) → C ⊃ D; (Δ_{11} Δ_{12} − X) (mix)

First, we consider the following derivation for each i (i = 1, 2).

\begin{matrix}⋮ & Π_{1i} \\ Γ_{1i} → A_{i}; Δ_{1i} \end{matrix} \begin{matrix}⋮ & Π_{2} \\ Γ_{2} C → D; \end{matrix} ; Γ_{2} → C ⊃ D; (→ ⊃)

Γ_{1i} (Γ_{2} − X) → C ⊃ D; (A_{i} Δ_{1i} − X) (mix)

Since the left height of the (mix)-rule is less than Π, we have a mix-free form of this derivation by the induction hypothesis. Let Π′_{1i} be the mix-free derivation. Next, we consider the following derivation.

\begin{matrix}\begin{matrix}\begin{matrix}A_{1} → A_{1} ; (init) & A_{2} → A_{2} ; (init) \\ A_{1} A_{2} → A_{1} ∧ A_{2} ; \end{matrix} ; (→ ∧) & \begin{matrix}⋮ & Π_{2} \\ Γ_{2} C → D; \end{matrix} \\ A_{1} A_{2} (Γ_{2} C − X) → D; \end{matrix} & (mix) \\ A_{1} A_{2} (Γ_{2} − X) C → D; \end{matrix} ; ^{(w→)^{∗}} ; A_{1} A_{2} (Γ_{2} − X) → C ⊃ D; ; (→ ⊃)

Since the left height of the (mix)-rule is equal to or less than Π and the right height is less than Π, we have a mix-free form of this derivation by the induction hypothesis. Let Π′_{2} be the mix-free derivation. Combining Π′_{11}, Π′_{12} and Π′_{2}, we get the following derivation, where Γ′_{2} and Δ′_{1i} are Γ_{2} − X and A_{i} Δ_{1i} − X, respectively.

\begin{matrix}⋮ & Π′_{12} \\ Γ_{12} Γ′_{2} → C ⊃ D; Δ′_{12} \end{matrix}

\begin{matrix}⋮ & Π′_{11} \\ Γ_{11} Γ′_{2} → C ⊃ D; Δ′_{11} \end{matrix}  \begin{matrix}⋮ & Π′_{2} \\ A_{1} A_{2} Γ′_{2} → C ⊃ D; \end{matrix}

Γ_{11} Γ′_{2} (A_{1} A_{2} Γ′_{2} − A_{1}) → C ⊃ D; (C ⊃ D Δ′_{11} − A_{1}) (mix)

⋮ structural rules
A_{2} Γ_{11} Γ′_{2} → C ⊃ D; Δ_{11} − X

Γ_{12} Γ′_{2} (A_{2} Γ_{11} Γ′_{2} − A_{2}) → C ⊃ D; (C ⊃ D Δ′_{12} − A_{2}) (Δ_{11} − X) (mix)

⋮ structural rules
Γ_{11} Γ_{12} Γ′_{2} → C ⊃ D; (Δ_{11} Δ_{12} − X)

Since the grades of the two (mix)-rules are both less than Π, we have a mix-free form of this derivation by the induction hypothesis.

Subcase 2-2: The rule (r1) is (→ ∨_{1}) or (→ ∨_{2}) whose principal formula is X. Similar to Case 2-1.

Subcase 2-3: The rule (r1) is (→ ⊃) whose principal formula is X. In this case, just similar to the proof for LK or LJ because Δ_{1} is empty.

Subcase 2-4: The rule (r1) is (→ ◁) whose principal formula is X, i.e., the derivation Π has the following form.

\begin{matrix}⋮ & Π_{1} \\ Γ_{1} → A_{1} ; A_{2} Δ_{1} \end{matrix} ; Γ_{1} → A_{1} ◁ A_{2} ; Δ_{1} (→ ◁) \begin{matrix}⋮ & Π_{2} \\ Γ_{2} C → D; \end{matrix} ; Γ_{2} → C ⊃ D; (→ ⊃)

Γ_{1} (Γ_{2} − X) → C ⊃ D; (Δ_{1} − X) (mix)

First, We consider the following derivation.

\begin{matrix}⋮ & Π_{1} \\ Γ_{1} → A_{1} ; A_{2} Δ_{1} \end{matrix} \begin{matrix}⋮ & Π_{2} \\ Γ_{2} C → D; \end{matrix} ; Γ_{2} → C ⊃ D; (→ ⊃)

Γ_{1} (Γ_{2} − X) → C ⊃ D; A_{1} A_{2} Δ_{1} − X (mix)

Since the left height of the (mix)-rule is less than Π, we have a mix-free form of this derivation by the induction hypothesis. Let Π′_{1} be the mix-free derivation. Next, we consider the following two derivations.

\begin{matrix}\begin{matrix}\begin{matrix}A_{1} → A_{1} ; & (init) \\ A_{1} → A_{1} ; A_{2} \end{matrix} ; (→w) ; A_{1} → A_{1} ◁ A_{2} ; ; (→ ◁) & \begin{matrix}⋮ & Π_{2} \\ Γ_{2} C → D; \end{matrix} \\ A_{1} (Γ_{2} C − X) → D; \end{matrix} & (mix) \\ A_{1} (Γ_{2} − X) C → D; \end{matrix} ; ^{(w→)^{∗}} ; A_{1} (Γ_{2} − X) → C ⊃ D; ; (→ ⊃) \begin{matrix}\begin{matrix}\begin{matrix}A_{2} → A_{2} ; & (init) \\ A_{2} → A_{1} ; A_{2} \end{matrix} ; (throw) ; A_{2} → A_{1} ◁ A_{2} ; ; (→ ◁) & \begin{matrix}⋮ & Π_{2} \\ Γ_{2} C → D; \end{matrix} \\ A_{2} (Γ_{2} C − X) → D; \end{matrix} & (mix) \\ A_{2} (Γ_{2} − X) C → D; \end{matrix} ; ^{(w→)^{∗}} ; A_{2} (Γ_{2} − X) → C ⊃ D; ; (→ ⊃)

Note that we need at least two steps to derive Γ_{1} → A_{1} ; A_{2} in Π_{1}. Therefore the left heights of the (mix)-rules are equal to or less than Π. Since the right heights are less than Π, we have mix-free forms of these derivations by the induction hypothesis. Let Π′_{21} and Π′_{22} be the mix-free derivations. Combining Π′_{1}, Π′_{21} and Π′_{22}, we get the following derivation, where Γ′_{2} is Γ_{2} − X.

\begin{matrix}⋮ & Π′_{1} \\ Γ_{1} Γ′_{2} → C ⊃ D; A_{1} A_{2} Δ_{1} − X \end{matrix} \begin{matrix}⋮ & Π′_{21} \\ A_{1} Γ′_{2} → C ⊃ D; \end{matrix}

Γ_{1} Γ′_{2} (A_{1} Γ′_{2} − A_{1}) → C ⊃ D; (A_{1} A_{2} Δ_{1} − X) − A_{1} (mix)

⋮ structural rules
Γ_{1} Γ′_{2} → C ⊃ D; A_{2} Δ_{1} − X

\begin{matrix}⋮ & Π′_{22} \\ A_{2} Γ′_{2} → C ⊃ D; \end{matrix}

Γ_{1} Γ′_{2} (A_{2} Γ′_{2} − A_{2}) → C ⊃ D; (A_{2} Δ_{1} − X) − A_{2} (mix)

⋮ structural rules
Γ_{1} Γ′_{2} → C ⊃ D; Δ_{1} − X

Since the grades of the two (mix)-rules are both less than Π, we have a mix-free form of this derivation by the induction hypothesis.

Case 3: The rule (r1) is a right-logical rule whose principal formula is X, and (r2) is neither (→ ⊃), nor a left-logical rule whose principal formula is X. The proof is just similar to the one for LK or LJ.

Case 4: The rule (r1) is a right-logical rule whose principal formula is X, and (r2) is a leftlogical rule whose principal formula is also X. The proof is also just similar to the cases of LJ and LK.

Unfortunately the computational behavior of the catch/throw mechanism is not captured by the cut-elimination process. Consider the following simple example.

\begin{matrix}A → A; & (init) \\ A → A; A \end{matrix} ; (throw)

A → A;

<x, catch u (throw u x), >

(catch)

This is a cut-free derivation, but the realizer includes a catch-throw pair. Another kind of proof transformation should be considered to explain the computational behavior of the mechanism. Roughly, the throw operation corresponds to the following form of non-local proof transformation.

\begin{matrix}\begin{matrix}⋮ & Π \\ Γ → E; Δ \end{matrix} ; Γ → A; E Δ ; . . . . . . & (throw) \\ Γ′ → E; E Δ′ \end{matrix} Γ′ → E; Δ′ (catch) ⟹  \begin{matrix}⋮ & Π \\ Γ → E; Δ \end{matrix} ; ⋮ (wxc → wxc) ; Γ′ → E; Δ′ ,

where Γ′ → E; Δ′ must be derivable from Γ → E; Δ by applying (→x), (→w), (→c), (x→), (w→) and (c→). We will discuss the details in Chapter 5.

A natural extension with a non-determinism

5.1 A non-determinism by the catch and throw mechanism

In the previous chapters, the author showed that the catch/throw mechanism corresponds to a variant formulation of Gentzen’s NJ following the Curry-Howard isomorphism in the opposite direction, and gave a correspondence with the conventional implementation by an abstract stack machine, in which the computational behavior of the mechanism was treated by a fixed evaluation strategy, the call-by-value strategy, and therefore the result of evaluation was unique. However, generally, the catch/throw mechanism introduces a non-determinism to evaluation processes, that is, the result of evaluation depends on the evaluation strategy. For example, let M be a term defined by

M = catch u ((λ x. λ y. 1) (throw u 2) (throw u 3)).

There are three possible results for the evaluation of M depending on the evaluation strategy as follows.

M → catch u ((λ y. 1) (throw u 3)) → catch u 1 → 1 M → catch u (throw u 2) → 2 M → catch u (throw u 3) → 3

In this chapter, we first extend the language to capture this non-deterministic feature of the catch and throw mechanism, and introduce its typing system, and show that the new typing system has the subject reduction property.

5.2 A calculus with a non-determinism

We first extend the calculus described in Chapter 2 by new reduction rules. The syntax of the terms used in the new calculus is the same as the one defined in Chapter 2, but we do not use let-expressions such as let x=M. N. That is, Term is now redefined as:

Term : : = Const | Var
| throw Tvar Term | catch Tvar Term
| λ Var. Term^{∗} | Term Term
| <Term, Term> | proj1 Term | proj2 Term
| inj1 Term | inj2 Term | case Term Var. Term Var. Term
| κ Tvar. Term | Term Tvar ,

We need not the notions of values or evaluation contexts in the new calculus.

5.2.1 Operational semantics

Now we define an operational semantics of the new calculus by a set of reduction rules on terms. The non-deterministic feature of the catch and throw mechanism is introduced by the following reduction rule.

Definition 5.2.1 (↦_{t}) A relation ↦_{t} on terms is defined as follows:

M[throw u N/x] ↦_{t} throw u N (x ∈ F IV (M) and x ≠ M) .

In other words,

C[throw u N] ↦_{t} throw u N,

where C ≠ ∗ and C does not capture any individual/tag variables occurring freely in throw u N. Note that N may not be a value.

Example 5.2.2

<inj1 (throw u M), throw v N> ↦_{t} throw u M
<inj1 (throw u M), throw v N> ↦_{t} throw v N
throw u M / ; ↦_{t} throw u M
case z x.(throw u x) y.y / ; ↦_{t} throw u x
catch u (throw u M) / ; ↦_{t} throw u M
catch v (throw u (M v)) / ; ↦_{t} throw u (M v)

The rest of reduction rules is defined by the following rules.

Definition 5.2.3 (↦_{n}) A relation ↦_{n} on terms is defined as follows:

catch u M ↦_{n} M  (u ∉ F T V (M))
catch u (throw u M) ↦_{n} M  (u ∉ F T V (M))
(λ x. M) N ↦_{n} M[N/x]
(κ u. M) v ↦_{n} M[v/u]
proj1 <M, N> ↦_{n} M
proj2 <M, N> ↦_{n} N
case (inj1 L) x.M y.N ↦_{n} M[L/x]
case (inj2 L) x.M y.N ↦_{n} N[L/y]

Definition 5.2.4 (Reduction rules) We define a relation ↦ by the union of ↦_{t} and ↦_{n}, that is,

M ↦ N iff M ↦_{t} N or M ↦_{n} N.

Definition 5.2.5 (→) We define a relation → as follows: M → N if and only if N is obtained from M by replacing an occurrence of M′ in M by N′ such that M′ ↦ N′. Let →^{∗} be the transitive and reflexive closure of the relation →.

Example 5.2.6 Let 1, 2 and 3 be distinct individual constants, and let M be as M = catch u ((λ x. λ y. 1) (throw u 2) (throw u 3)).

M → catch u ((λ y. 1) (throw u 3)) → catch u 1 → 1 M → catch u (throw u 2) → 2 M → catch u (throw u 3) → 3

Definition 5.2.7 (→^{sub}) We define a relation →^{sub} as follows:

M →^{sub} N iff M → N and M {/ \atop ↦} N,

and →^{sub∗} as the transitive and reflexive closure of →^{sub}.

5.3 Basic properties of the calculus

In this section, we consider about the basic properties of the calculus.

Proposition 5.3.1 (Extension of ⟶_{CBV}) Let M and N be terms of the new calculus, that is, M or N does not include any let-expressions. If M ⟶_{CBV}^{∗} N, then M →^{∗} N.

Proof. Obvious from the definitions of ⟶_{CBV} and →.

Proposition 5.3.2 Let L, M and N be terms and x an individual variable. Let u and v be tag variables. If M ↦ N, then

1. M[L/x] ↦ N[L/x], and

2. M[v/u] ↦ N[v/u].

Proof. Obvious from the definition of ↦.

Proposition 5.3.3 Let L, M and N be terms and x an individual variable. Let u and v be tag variables. If M → N, then

1. M[L/x] → N[L/x], and

2. M[v/u] → N[v/u].

Proof. We can assume that M →^{sub} N because it is obvious from Proposition 5.3.2 if M ↦ N. We show that M[L/x] → N[L/x] by induction on |M|. Suppose M →^{sub} N. Obviously, M must not be a variable. If M = catch u M′ for some u and M′, then we can assume that u is fresh, and that N = catch u N′ for some N′ such that M′ → N′. Since M′[L/x] →^{sub} N′[L/x] by the induction hypothesis, we get M[L/x] → N[L/x] in this case. We can similarly derive it even if M has one of the other forms. We can also get M[v/u] → N[v/u] by induction on |M|.

Proposition 5.3.4 Let M be a term, and let x and y be individual variables. Let u and v be tag variables. If M[y/x, v/u] ↦ N, then M ↦ N′ and N = N′[y/x, v/u] for some N′.

Proof. Obvious from the definition of ↦.

Proposition 5.3.5 If M[y/x, v/u] → N, then M → N′ and N = N′[y/x, v/u] for some N′.

Proof. Similar to the proof of Proposition 5.3.3.

5.4 The typing system L_{c/t}

5.4.1 Syntax of typing judgements

We introduce a new typing system for the new calculus which has the extended reduction rules.

Definition 5.4.1 (Type expressions) We use the same class of type expressions, or formulas, as Lc/t^{CBV}. That is, atomic types, conjunctions (A ∧ B), disjunctions (A ∨ B), implications (A ⊃ B) and exceptions (A ◁ B).

Definition 5.4.2 (Individual contexts) Individual contexts are also defined in the same way

as Lc/t^{CBV}.

Definition 5.4.3 (Tag contexts) We extend the definition of tag contexts as follows. A tag context is a finite mapping which assigns a pair of a type expression and a set of individual variables to each tag variable in its domain. We use Δ, Δ′, … to denote tag contexts. Let u_{1}, …, u_{n} be tag variables. Let B_{1}, …, B_{n} be type expressions, and let V_{1}, …, V_{n} be sets of individual variables such that if u_{i} = u_{j} then B_{i} = B_{j} and V_{i} = V_{j} for any i and j. We use {u_{1} : B_{1}^{V_{1}}, …, u_{n}: B_{n}^{V_{n}}} to denote a tag context whose domain is {u_{1}, …, u_{n}} and which assigns the pair < B_{i}, V_{i} > to u_{i} for each i. We denote the first and the second components of Δ(u) by Δ^{t}(u) and Δ^{v}(u), respectively. For example, Δ^{t}(u_{i}) = B_{i} and Δ^{v}(u_{i}) = V_{i} if Δ = {u_{1} : B_{1}^{V_{1}}, …, u_{n}: B_{n}^{V_{n}}}.

Definition 5.4.4 (Compatible contexts) Let Γ and Γ′ be individual contexts. Γ is compatible with Γ′ if and only if Γ(x) = Γ′(x) for any individual variable x ∈ Dom(Γ)∩Dom(Γ′). We denote it by Γ ∥ Γ′. Note that Γ ∪ Γ′ is also an individual context if Γ ∥ Γ′. The compatibility of tag contexts is also defined as follows: Δ is compatible with Δ′ if and only if Δ^{t}(u) = Δ^{′t}(u) for any individual variable u ∈ Dom(Δ) ∩ Dom(Δ′). We denote it by Δ ∥ Δ′. When Δ and Δ′ are compatible, we define a new tag context Δ ⊔ Δ′ as follows.

(Δ ⊔ Δ′)(u) = \{ \begin{matrix}(Δ^{t}(u), Δ^{v}(u) ∪ Δ^{′v}(u)) & if u ∈ Dom(Δ) ∩ Dom(Δ′) \\ Δ(u) & if u ∈ Dom(Δ) and u ∉ Dom(Δ′) \\ Δ′(u) & if u ∉ Dom(Δ) and u ∈ Dom(Δ′) \end{matrix}

Note that Dom(Δ ⊔ Δ′) = Dom(Δ) ∪ Dom(Δ′).

Definition 5.4.5 Let Δ be as Δ = {u_{1} : B_{1}^{V_{1}}, …, u_{n}: B_{n}^{V_{n}}}, and let u and v be tag variables. If {u, v} ⊂ Dom(Δ) implies Δ^{t}(u) = Δ^{t}(v), then we define a tag context Δ[v/u] as follows.

Δ[v/u] = {u_{1}[v/u] : B_{1}^{V_{1}}, …, u_{n}[v/u] : B_{n}^{V_{n}}}.

We define Γ[y/x] similarly for an individual context Γ and individual variables x and y.

5.4 The typing system L_{c/t}  53

Definition 5.4.6 Let V be a set of individual variables. We define a tag context Δ[V/{x}] as follows.

Dom(Δ[V/{x}]) = Dom(Δ)

Δ[V/{x}]^{t}(u) = Δ^{t}(u)

Δ[V/\{x\}]^{v}(u) = \{ \begin{matrix}(Δ^{v}(u) − \{x\}) ∪ V & if x ∈ Δ^{v}(u) \\ Δ^{v}(u) & otherwise. \end{matrix}

Definition 5.4.7 (Typing judgements) Let Γ and Δ be an individual context and a tag context, respectively, such that Δ^{v}(u) ⊂ Dom(Γ) for any u ∈ Dom(Δ). Let M be a term, and C a type expression. Typing judgements have the following form.

Γ ⊢ M : C; Δ

The intended meaning of a typing judgement {x_{1} : A_{1}, …, x_{m}: A_{m}} ⊢ M : C; {u_{1} : B_{1}^{V_{1}}, …, u_{n}: B_{n}^{V_{n}}} is roughly that when we execute the program M supplying values of the types A_{1} … A_{m} for the corresponding free variables x_{1}, …, x_{m} of M, it normally reduces to a value of the type C, otherwise the program throws a value of B_{j} with a tag u_{j} for some j (1 ≤ j ≤ n), and the thrown value depends on only the individual variables which belong to V_{j}.

5.4.2 L_{c/t}

We denote the typing system by L_{c/t}, which can be an extension of Lc/t^{CBV}.

Definition 5.4.8 (Typing rules) L_{c/t} is defined by the following set of typing rules.

Γ ∪ {x: A} ⊢ x: A; Δ (var)

Γ ⊢ M : A; Δ ⊔ {u: A^{V} }

Γ ⊢ catch u M : A; Δ (catch)

Γ_{1} ⊢ M : E; Δ Γ_{1} ∪ Γ_{2} ⊢ throw u M : A; Δ ⊔ {u: E^{Dom(Γ_{1})}}

(throw)

{Γ ∪ \{x: A\} ⊢ M : B; Δ \atop Γ ⊢ λ x. M : A ⊃ B; Δ} ^{(⊃-I ) (x ∉ Δ^{v}(u) for any u ∈ Dom(Δ))}
Γ_{1} ⊢ M : A ⊃ B; Δ_{1} Γ_{2} ⊢ N : A; Δ_{2}

Γ_{1} ∪ Γ_{2} ⊢ M N : B; Δ_{1} ⊔ Δ_{2} (⊃-E )

{Γ ⊢ M : A; Δ ⊔ \{u: E^{V} \} \atop Γ ⊢ κ u. M : A ◁ E; Δ} (◁-I )

{Γ_{1} ⊢ M : A ◁ E; Δ \atop Γ_{1} ∪ Γ_{2} ⊢ M u: A; Δ ⊔ \{u: E^{Dom(Γ_{1})}\}} (◁-E )
Γ_{1} ⊢ M : A; Δ_{1} Γ_{2} ⊢ N : B; Δ_{2}

Γ_{1} ∪ Γ_{2} ⊢ <M, N>: A ∧ B; Δ_{1} ⊔ Δ_{2} (∧-I )

Γ ⊢ M : A ∧ B; Δ Γ ⊢ proj1 M : A; Δ (∧_{1}-E )  Γ ⊢ M : A ∧ B; Δ Γ ⊢ proj2 M : B; Δ (∧_{2}-E )

{Γ ⊢ M : A; Δ \atop Γ ⊢ inj1 M : A ∨ B; Δ} (∨_{1}-I )  {Γ ⊢ M : B; Δ \atop Γ ⊢ inj2 M : A ∨ B; Δ} (∨_{2}-I )
Γ_{1} ⊢ L: A ∨ B; Δ_{1} Γ_{2} ∪ {x: A} ⊢ M : C; Δ_{2} Γ_{3} ∪ {y: B} ⊢ N : C; Δ_{3}
Γ_{1} ∪ Γ_{2} ∪ Γ_{3} ⊢ case L x.M y.N : C;
Δ_{1} ⊔ Δ_{2}[Dom(Γ_{1})/{x}] ⊔ Δ_{3}[Dom(Γ_{1})/{y}]

(∨-E )

The side condition for (⊃-I ) is necessary to keep the system constructive. Note that the following inference rule of Lc/t^{CBV} corresponds to (⊃-I ) of L_{c/t}.

{Γ ∪ \{x: A\} ⊢ M : B; \{\} \atop Γ ⊢ λ x. M : A ⊃ B; \{\}} (⊃-I )

As a logic, (⊃-I ) of Lc/t^{CBV} is equivalent to (⊃-I ) of Definition 5.4.8, but is too restrictive with respect to the variation of proofs, that is, typed programs. For example, the following typing judgement, which is derivable in L_{c/t}, would not be derivable if we replaced (⊃-I ) by the one of

Lc/t^{CBV}.

{} ⊢ catch u (λ x. throw u (λ y. y)) : A ⊃ A; {}

Moreover, the language would not have a subject reduction property, because

{} ⊢ catch u ((λ z. λ x. z) (throw u (λ y. y))) : A ⊃ A; {}

would be still derivable, but

catch u ((λ z. λ x. z) (throw u (λ y. y))) → catch u (λ x. throw u (λ y. y)).

This is the reason why we maintain the set of the relevant individual variables to each tag in tag contexts of typing judgements.

The following example of a derivation shows that the calculus does not have Church-Rosser property even if we consider only the well-typed terms. Let M be the term λ x. λ f. catch u ((λ y. x) (throw u (f x))). The well-typed term M has two normal forms as follows.

M → λ x. λ f. catch u (throw u (f x)) → λ x. λ f. f x
M → λ x. λ f. catch u x → λ x. λ f. x

Example 5.4.9 Let Γ be as Γ = {x: A, f : A ⊃ A}.

\begin{matrix}\{y: B\} ⊢ x: A; \{\} & (var) \\ \{\} ⊢ λ y. x: B ⊃ A; \{\} \end{matrix} ; (⊃-I ) \begin{matrix}Γ ⊢ f : A ⊃ A; \{\} (var) & Γ ⊢ x: A; \{\} (var) \\ Γ ⊢ f x: A; \{\} \end{matrix} ; (⊃-E )

Γ ⊢ throw u (f x) : B; {u: A^{{x,f}}}

(throw)
Γ ⊢ (λ y. x) (throw u (f x)) : A; {u: A^{{x,f}}}

(⊃-E )
Γ ⊢ catch u ((λ y. x) (throw u (f x))) : A; {}

(catch)

{x: A} ⊢ λ f. catch u ((λ y. x) (throw u (f x))) : (A ⊃ A) ⊃ A; {}

(⊃-I )

{} ⊢ λ x. λ f. catch u ((λ y. x) (throw u (f x))) : A ⊃ (A ⊃ A) ⊃ A; {} (⊃-I )

5.4.3 Basic properties of L_{c/t}

In this subsection, we presents a some basic properties of the system as a preparation for proving the subject reduction property of L_{c/t}. Proposition 5.4.10 If Γ ⊢ M : C; Δ is derivable, then F IV (M) ⊂ Dom(Γ) and F T V (M) ⊂ Dom(Δ). Proof. By induction on the derivation of Γ ⊢ M : C; Δ. Definition 5.4.11 Let Δ and Δ′ be tag contexts. We define a relation Δ ⊏ Δ′ as follows. The relation Δ ⊏ Δ′ holds if and only if

• Dom(Δ) ⊂ Dom(Δ′), and

• Δ^{t}(u) = Δ^{′t}(u) and Δ^{v}(u) ⊂ Δ^{′v}(u) for any u ∈ Dom(Δ). Note that Δ ⊏ (Δ ⊔ Δ′) if Δ ∥ Δ′. Definition 5.4.12 Let d be a natural number. We say a typing judgement is d-derivable if there exists a derivation of the judgement whose depth is less than or equal to d. Proposition 5.4.13 Let d be a natural number, and let Γ ⊢ M : C; Δ be a d-derivable typing judgement.

1. If Γ ⊂ Γ′ and Δ ⊏ Δ′, then Γ′ ⊢ M : C; Δ′ is also d-derivable.

2. If Γ[y/x] is well defined, then Γ[y/x] ⊢ M[y/x] : C; Δ[{y}/{x}] is also d-derivable.

3. If Δ[v/u] is well defined, then Γ ⊢ M[v/u] : C; Δ[v/u] is also d-derivable. Proof. By simultaneous inductions on d. Proposition 5.4.14 Let x and u be as x ∉ F IV (M) and u ∉ F T V (M).

1. If Γ ∪ {x: A} ⊢ M : C; Δ is derivable, then Γ ⊢ M : C; Δ[{}/{x}] is also derivable.

2. If Γ ⊢ M : C; Δ ⊔ {u: E^{V} } is derivable, then Γ ⊢ M : C; Δ is also derivable. Proof. Straightforward induction on the derivations.

Proposition 5.4.15 (Extension of Lc/t^{CBV}) Let M be a term of the new calculus, that is, M does not include any let-expressions. Let Γ be a tag context, and C a formula. Let u_{1}, …, u_{n} be a sequence of tag variables, and let B_{1}, …, B_{n} be a sequence of formulas. If Γ ⊢ M : C; {u_{1} : B_{1},

…, u_{n}: B_{n}} is derivable in Lc/t^{CBV}, then Γ ⊢ M : C; {u_{1} : B_{1}^{Dom(Γ)}, …, u_{n}: B_{n}^{Dom(Γ)}} is derivable

in L_{c/t}.

Proof. By induction on the depth of the derivation of Γ ⊢ M : C; {u_{1} : B_{1}, …, u_{n}: B_{n}}. Use Proposition 5.4.13.

Proposition 5.4.16 (Throw) Let M be term, and let u be a tag variable. If Γ ⊢ throw u M : C; Δ is derivable, then Γ ⊢ throw u M : A; Δ is also derivable for any type A.

Proof. Since Γ ⊢ throw u M : C; Δ is derivable, so is Γ ⊢ M : E; Δ′ for some E and Δ′ such that Δ = Δ′ ⊔ {u: E^{Dom(Γ)}}. Therefore, we can derive Γ ⊢ throw u M : A; Δ for any A by (throw).

Proposition 5.4.17 (Substitution) Let Γ_{1}, Γ_{2}, Δ_{1} and Δ_{2} be as Γ_{1} ∥ Γ_{2} and Δ_{1} ∥ Δ_{2}. If Γ_{1} ⊢ N : A; Δ_{1} and Γ_{2} ∪ {x: A} ⊢ M : C; Δ_{2} are derivable, then Γ_{1} ∪ Γ_{2} ⊢ M[N/x] : C; Δ_{1} ⊔ Δ_{2}[Dom(Γ_{1})/{x}] is also derivable.

Proof. By induction on the depth of the derivation of Γ_{2} ∪ {x: A} ⊢ M : C; Δ_{2}. Suppose that Γ_{1} ⊢ N : A; Δ_{1} and Γ_{2}∪{x: A} ⊢ M : C; Δ_{2} are derivable. First, suppose also that x ∉ F IV (M), that is, M[N/x] = M. Since Γ_{2} ∪ {x: A} ⊢ M : C; Δ_{2} is derivable, so is Γ_{2} ⊢ M : C; Δ_{2}[{}/{x}] by Proposition 5.4.14, and this implies that Γ_{1} ∪ Γ_{2} ⊢ M : C; Δ_{1} ⊔ Δ_{2}[Dom(Γ_{1})/{x}] is derivable by Proposition 5.4.13. Therefore, we now assume that x ∈ F IV (M). By cases on the last rule used in the derivation of Γ_{2} ∪ {x: A} ⊢ M : C; Δ_{2}.

Case 1: The last rule is (var). That is, M = x since x ∈ F IV (M). We can derive Γ_{1} ∪ Γ_{2} ⊢ M[N/x] : C; Δ_{1} ⊔ Δ_{2}[Dom(Γ_{1})/{x}] by applying Proposition 5.4.13 to the derivation of Γ_{1} ⊢ N : A; Δ_{1} since M[N/x] = N and C = A .

Case 2: The last rule is (catch). In this case, M = catch u M′ and the following judgement is derivable for some u, V and M′.

Γ_{2} ∪ {x: A} ⊢ M′: C; Δ_{2} ⊔ {u: C^{V} }

We can assume that u ∉ Dom(Δ_{1}) by Proposition 5.4.13. By the induction hypothesis, we have a derivation of

Γ_{1} ∪ Γ_{2} ⊢ M′[N/x] : C; Δ_{1} ⊔ (Δ_{2} ⊔ {u: C^{V} })[Dom(Γ_{1})/{x}].  (5.1)

Since u ∉ Dom(Δ_{1}), we get M[N/x] = catch u (M′[N/x]). By applying (catch) to (5.1), we get Γ_{1} ∪ Γ_{2} ⊢ M[N/x] : C; Δ_{1} ⊔ Δ_{2}[Dom(Γ_{1})/{x}].

Case 3: The last rule is (throw). In this case, M = throw u M′ and the following judgement is derivable for some u, M′, E, Γ′_{2} and Δ such that Γ′_{2} ⊂ Γ_{2} ∪ {x: A} and Δ_{2} = Δ ⊔ {u: E^{Dom(Γ′_{2})}}.

Γ′_{2} ⊢ M′: E; Δ

5.5 The subject reduction property of L_{c/t}  57

We get x ∈ F IV (M′), that is, x ∈ Dom(Γ′_{2}) from x ∈ F IV (M). Let Γ be as Γ = Γ′_{2} − {x: A}, that is, Γ′_{2} = Γ ∪ {x: A}. By the induction hypothesis, we have a derivation of

Γ_{1} ∪ Γ ⊢ M′[N/x] : E; Δ_{1} ⊔ Δ[Dom(Γ_{1})/{x}].

Since M[N/x] = throw u (M′[N/x]), by applying (throw),

Γ_{1} ∪ Γ ⊢ M[N/x] : C; Δ_{1} ⊔ Δ[Dom(Γ_{1})/{x}] ⊔ {u: E^{Dom(Γ_{1}∪Γ)}}.

Since Γ ⊂ Γ_{2}, by Proposition 5.4.13 again,

Γ_{1} ∪ Γ_{2} ⊢ M[N/x] : C; Δ_{1} ⊔ Δ[Dom(Γ_{1})/{x}] ⊔ {u: E^{Dom(Γ_{1}∪Γ)}}.

Note that

Δ[Dom(Γ_{1})/{x}] ⊔ {u: E^{Dom(Γ_{1}∪Γ)}} = Δ_{2}[Dom(Γ_{1})/{x}]

because Δ_{2} = Δ ⊔ {u: E^{Dom(Γ)∪{x}}} and x ∉ Dom(Γ).

Case 4: The last rule is (⊃-I ). In this case M = λ y. M′, C = C_{1} ⊃ C_{2} and the following judgement is derivable for some y, C_{1}, C_{2} and M′ such that y ∉ Δ_{2}^{v}(u) for any u ∈ Dom(Δ_{2}).

Γ_{2} ∪ {x: A} ∪ {y: C_{1}} ⊢ M′: C_{2} ; Δ_{2}

We can assume that y ∉ Dom(Γ_{1}) by Proposition 5.4.13, and get M′[N/x] = λ y. (M[N/x]). By the induction hypothesis, we have a derivation of

Γ_{1} ∪ Γ_{2} ∪ {y: C_{1}} ⊢ M′[N/x] : C_{2} ; Δ_{1} ⊔ Δ_{2}[Dom(Γ_{1})/{x}].  (5.2)

We get y ∉ (Δ_{1} ⊔ Δ_{2}[Dom(Γ_{1})/{x}])^{v}(u) for any u ∈ Dom(Δ_{1} ⊔ Δ_{2}[Dom(Γ_{1})/{x}]) since y ∉ Δ_{2}^{v}(u) for any u ∈ Dom(Δ_{2}) and y ∉ Dom(Γ_{1}). Therefore, we can derive

Γ_{1} ∪ Γ_{2} ⊢ λ y. (M′[N/x]) : C_{2} ; Δ_{1} ⊔ Δ_{2}[Dom(Γ_{1})/{x}]

by applying (⊃-I ) to (5.2).

Case 5: The last rule is one of the rest. Similar.

5.5 The subject reduction property of L_{c/t}

As mentioned in Section 5.4.2, the calculus does not have Church-Rosser property even if we consider only the well-typed terms. However, it has the subject reduction property, which compensates for this unpleasant feature. In this section, we show the subject reduction property of L_{c/t}.

Lemma 5.5.1 If Γ ⊢ M : C; Δ is derivable and M ↦_{t} throw v N, then Γ ⊢ throw v N : C; Δ is also derivable.

Proof. By induction on the depth of the derivation of Γ ⊢ M : C; Δ. Suppose that Γ ⊢ M : C; Δ is derivable and M ↦_{t} throw v N. By Proposition 5.4.16, it is enough to show that Γ ⊢ throw v N : C′; Δ is derivable for some C′. By cases according to the last rules used in the derivation.

Case 1: The last rule is (var). This is impossible because M ↦_{t} throw v N.

Case 2: The last rule is (catch). M = catch u M′ and the following judgement is derivable for some u, V and M′.

Γ ⊢ M′: C; Δ ⊔ {u: C^{V} }  (5.3)

Since M ↦_{t} throw v N, we get u ∉ F T V (throw v N) and

M′ = throw v N or M′ ↦_{t} throw v N.

Therefore, from (5.3) or the induction hypothesis on (5.3),

Γ ⊢ throw v N : C; Δ ⊔ {u: C^{V} }.

We get Γ ⊢ throw v N : C; Δ by Proposition 5.4.14 since u ∉ F T V (throw v N).

Case 3: The last rule is (throw). In this case, M = throw u M′ and the following judgement is derivable for some u, M′, E, Γ′ and Δ′ such that Γ′ ⊂ Γ and Δ = Δ′ ⊔ {u: E^{Dom(Γ′)}}.

Γ′ ⊢ M′: E; Δ′  (5.4)

We get M′ = throw v N or M′ ↦_{t} throw v N from M ↦_{t} throw v N. Therefore, from (5.4) or the induction hypothesis on (5.4),

Γ′ ⊢ throw v N : E; Δ′.

We get Γ ⊢ throw v N : E; Δ by Proposition 5.4.13 since Γ′ ⊂ Γ and Δ′ ⊏ Δ.

Case 4: The last rule is (⊃-I ). M = λ x. M′, C = C_{1} ⊃ C_{2} and the following judgement is derivable for some x, C_{1}, C_{2} and M′ such that x ∉ Δ^{v}(u) for any u ∈ Dom(Δ).

Γ ∪ {x: C_{1}} ⊢ M′: C_{2} ; Δ  (5.5)

Since M ↦_{t} throw v N, we get x ∉ F IV (throw v N) and

M′ = throw v N or M′ ↦_{t} throw v N.

Therefore, from (5.5) or the induction hypothesis on (5.5),

Γ ∪ {x: C_{1}} ⊢ throw v N : C_{2} ; Δ.

We get Γ ⊢ throw v N : C_{2} ; Δ by Proposition 5.4.14 since x ∉ F IV (throw v N).

Case 5: The last rule is one of the rest. Similar to Case 2 and Case 3.

Lemma 5.5.2 If Γ ⊢ M : C; Δ is derivable and M ↦_{n} N, then Γ ⊢ N : C; Δ is also derivable.

Proof. By induction on the depth of the derivation of Γ ⊢ M : C; Δ. Suppose that Γ ⊢ M : C; Δ is derivable and M ↦_{n} N. By cases according to the form of M.

Case 1: M = catch u N and u ∉ F T V (N). In this case, Γ ⊢ N : C; Δ ⊔ {u: C^{V} } is derivable for some V. We get Γ ⊢ N : C; Δ by Proposition 5.4.14 since u ∉ F T V (N).

Case 2: M = catch u (throw u N) and u ∉ F T V (N). The following judgement is derivable for some V, Γ′ and Δ′ such that Γ′ ⊂ Γ and Δ ⊔ {u: C^{V} } = Δ′ ⊔ {u: C^{Dom(Γ′)}}.

Γ′ ⊢ N : C; Δ′

Since Γ′ ⊂ Γ and Δ′ ⊏ Δ ⊔ {u: C^{V} }, Γ ⊢ N : C; Δ ⊔ {u: C^{V} } is derivable by Proposition 5.4.13. Therefore, Γ ⊢ N : C; Δ is also derivable by Proposition 5.4.14 since u ∉ F T V (N).

Case 3: M = (λ x. M_{1}) M_{2} and N = M_{1}[M_{2}/x] for some x, M_{1} and M_{2}. The following two judgements are derivable for some A, Γ_{1}, Γ_{2}, Δ_{1} and Δ_{2} such that Γ = Γ_{1} ∪ Γ_{2}, Δ = Δ_{1} ⊔ Δ_{2} and x ∉ Δ_{1}^{v}(u) for any u ∈ Dom(Δ_{1}).

Γ_{1} ∪ {x: A} ⊢ M_{1} : C; Δ_{1}  (5.6)
Γ_{2} ⊢ M_{2} : A; Δ_{2}  (5.7)

Therefore, by Lemma 5.4.17, we get Γ ⊢ M_{1}[M_{2}/x] : C; Δ_{1}[Dom(Γ_{2})/{x}] ⊔ Δ_{2} from (5.6) and (5.7), where Δ_{1}[Dom(Γ_{2})/{x}] ⊔ Δ_{2} = Δ_{1} ⊔ Δ_{2} = Δ since x ∉ Δ_{1}^{v}(u) for any u ∈ Dom(Δ_{1}).

Case 4: M = (κ u. M′) v and N = M′[v/u] for some u, v and M′. The following judgement is derivable for some E, Γ′, Δ′ and V such that Γ′ ⊂ Γ and Δ = Δ′ ⊔ {v: E^{Dom(Γ′)}}.

Γ′ ⊢ M′: C; Δ′ ⊔ {u: E^{V} }

Since Δ′ ∥ {v: E^{Dom(Γ′)}}, Γ′ ⊢ M′[v/u] : C; Δ′[v/u]∪{v: E^{V} } is derivable by Proposition 5.4.13. Since Γ′ ⊂ Γ, by Proposition 5.4.13 again,

Γ ⊢ M′[v/u] : C; Δ′[v/u] ∪ {v: E^{V} }.

Since V ⊂ Dom(Γ′) and Δ^{′v}(u) ⊂ Dom(Γ′),

Δ′[v/u] ⊔ {v: E^{V} } ⊏ Δ′[v/u] ⊔ {v: E^{Dom(Γ′)}} ⊏ Δ′ ⊔ {v: E^{Dom(Γ′)}} = Δ.

Therefore, Γ ⊢ M′[v/u] : C; Δ is derivable by Proposition 5.4.13.

Case 5: M = proj_{i} <M_{1}, M_{2}> and N = M_{i} for some i (i = 1, 2). Similar.

Case 6: M = case (inj_{i} M_{0}) x_{1}.M_{1} x_{2}.M_{2} and N = M_{i}[M_{0}/x_{i}] for some i (i = 1, 2). Similar.

Lemma 5.5.3 If Γ ⊢ M : C; Δ is derivable and M ↦ N, then Γ ⊢ N : C; Δ is also derivable.

Proof. Straightforward from Lemma 5.5.1 and Lemma 5.5.2.

Theorem 5.5.4 (Subject reduction) If Γ ⊢ M : C; Δ is derivable and M → N, then Γ ⊢ N : C; Δ is also derivable.

Proof. By induction on the depth of the derivation of Γ ⊢ M : C; Δ. Suppose that Γ ⊢ M : C; Δ is derivable and M → N. If M ↦ N, then trivial by Lemma 5.5.3. Therefore we can assume that M → N and M {/ \atop ↦} N. By cases according to the last rules used in the derivation. A typical one is the case that the last rule is (throw). In this case, M = throw u M′ and

Γ′ ⊢ M′: E; Δ′

is derivable for some u, M′, E, Γ′ and Δ′ such that Γ′ ⊂ Γ and Δ = Δ′ ⊔ {u: E^{Dom(Γ′)}}. Since M → N and M {/ \atop ↦} N, M′ → N′ and N = throw u N′ for some N′. Therefore, Γ′ ⊢ N′: E; Δ′ is derivable by the induction hypothesis. We get Γ ⊢ throw u N′: E; Δ by applying (throw). The proofs for other cases are just similar.

5.6 L_{c/t} as a logic

In this section, we show that L_{c/t} can be regarded as a conservative extension of the propositional fragment of the standard intuitionistic logic such as Gentzen’s NJ and LJ. We first translate each typing judgement of L_{c/t} into a formula, and then show its provability in the standard intuitionistic logic. Let ≤ be a total ordering over the union of Var and Tvar through this section.

Definition 5.6.1 Let Δ be a tag context, and u a tag variable. We define a tag context Δ\u as follows.

Dom(Δ\u) = Dom(Δ) − {u}
(Δ\u)(v) = Δ(v)  (v ∈ Dom(Δ) − {u})

Let Γ be an individual context, and x an individual variable. Γ\x is defined in the same way.

Definition 5.6.2 Let Δ be a tag context, and x an individual variable. We define two tag contexts Dep(x, Δ) and Indep(x, Δ) as follows.

Dep(x, {}) = Indep(x, {}) = {}
Dep(x, \{u: A^{V} \} ∪ Δ) = \{ \begin{matrix}\{u: A^{V} \} ∪ Dep(x, Δ\u) & if x ∈ V \\ Dep(x, Δ\u) & otherwise \end{matrix}

Indep(x, \{u: A^{V} \} ∪ Δ) = \{ \begin{matrix}\{u: A^{V} \} ∪ Indep(x, Δ\u) & if x ∉ V \\ Indep(x, Δ\u) & otherwise \end{matrix}

Definition 5.6.3 Let Δ be a non-empty tag context. We define a formula Disj(Δ) as follows. Let u be the tag variable such that u ∈ Dom(Δ) and u ≤ v for any v ∈ Dom(Δ). Then,

Disj(Δ) = \{ \begin{matrix}Δ^{t}(u) & if Dom(u) is a singleton \\ Δ^{t}(u) ∨ Disj(Δ\u) & otherwise. \end{matrix}

Definition 5.6.4 Let Γ be an individual context, Δ a tag context. Let C be a formula or a place holder denoted by ∗. We define a formulas T rans(Γ, C, Δ) as follows.

T rans(\{\}, C, Δ) = \{ \begin{matrix}C & if Dom(Δ) = \{\} \\ Disj(Δ) & if Dom(Δ) ≠ \{\} and C = ∗ \\ C ∨ Disj(Δ) & otherwise \end{matrix}

5.6 L_{c/t} as a logic  61

Let x be the individual variable such that x ∈ Dom(Γ) and x ≤ y for any y ∈ Dom(Γ). Then,

T rans(Γ, C, Δ) = \{ \begin{matrix}Γ(x) ⊃ T rans(Γ\x, C, Dep(x, Δ)) & if Dom(Indep(x, Δ)) = \{\} \\ \begin{matrix}(Γ(x) ⊃ T rans(Γ\x, C, Dep(x, Δ))) \\ ∨ T rans(Γ\x, ∗, Indep(x, Δ)) \end{matrix} & otherwise. \end{matrix}

Proposition 5.6.5 Γ ⊢ M : C; Δ is derivable in L_{c/t} if and only if T rans(Γ̃, C̃, Δ̃) is provable in the propositional fragment of NJ. Proof. By induction on the derivation of Γ ⊢ M : C; Δ.

A term model for the extended system

6.1 Term models

Definition 6.1.1 Let red be a subrelation of →. A red-sequence is a possibly infinite sequence M_{0}, M_{1}, M_{2}, … of terms such that M_{i} red M_{i+1} for any i. Definition 6.1.2 Let red be a subrelation of →. A term M is strongly normalizable w.r.t. red if there exists no infinite red-sequence starting with M. We simply say that M is strongly normalizable if so is w.r.t. →. Definition 6.1.3 Let n be a natural number. We define a relation →^{∗n} inductively as follows.

1. M →^{∗0} N iff M = N.

2. M →^{∗n+1} N iff M →^{∗n} N or M → M′ and M′ →^{∗n} N for some M′.

We also define ⟶^{sub∗n} in the same way. Proposition 6.1.4 Let M be a term, and let x and y be individual variables. Let u and v be tag variables, n a natural number. If M[y/x, v/u] →^{∗n} N, then M →^{∗n} N′ and N = N′[y/x, v/u] for some N′. Proof. Straightforward from Proposition 5.3.5. Definition 6.1.5 (Types) We define a collection Type of sets of terms as follows:

Type = { T | For any M ∈ T, M → N implies N ∈ T.} .

Elements of Type are called types. We use T, S, … to denote types. Definition 6.1.6 (Regular types) A type T is regular if and only if

M ∈ T implies M[v/u] ∈ T for any term M and for any tag variables u and v, Definition 6.1.7 Let V and V′ be finite sets of individual variables, and x an individual variable. We define V [V′/{x}] as

V [V′/\{x\}] = \{ \begin{matrix}(V − \{x\}) ∪ V′ & if x ∈ V \\ V & otherwise. \end{matrix}

Definition 6.1.8 (Frames) A set of term X is a frame if and only if 1. X is a regular type,

2. x ∈ X for any individual variable x,

3. if M, N ∈ X, then M[N/x] ∈ X, and

4. if Γ ⊢ M : C; Δ is derivable for some Γ and Δ, then M ∈ X.

Definition 6.1.9 Let n be a natural number, u a tag variable, T a type, and V a finite set of individual variables. A set of terms J_{n}(u, T, V) is defined as follows.

M ∈ J_{n}(u, T, V) if and only if 1. if M →^{∗n} throw u K, then K ∈ T,

2. if M →^{∗n} K for some normal form K such that u ∈ F T V (K) and F IV (K) ∩ V = {}, then K = throw u L for some closed term L,

3. if M →^{∗k} catch v L for some k (k ≤ n) and v ≠ u, then L ∈ J_{n−k}(u, T, V),

4. if M →^{∗k} throw v L for some k (k ≤ n), then L ∈ J_{n−k}(u, T, V),

5. if M →^{∗k} λ y. L for some k (k ≤ n), then L ∈ J_{n−k}(u, T, V − {y}),

6. if M →^{∗k} L_{1} L_{2} for some k (k ≤ n), then L_{1}, L_{2} ∈ J_{n−k}(u, T, V),

7. if M →^{∗k} <L_{1}, L_{2}> for some k (k ≤ n), then L_{1}, L_{2} ∈ J_{n−k}(u, T, V),

8. if M →^{∗k} proj_{i} L for some k (k ≤ n) and some i (i = 1, 2), then L ∈ J_{n−k}(u, T, V),

9. if M →^{∗k} inj_{i} L for some k (k ≤ n) and some i (i = 1, 2), then L ∈ J_{n−k}(u, T, V),

10. if M →^{∗k} case L_{0} y_{1}.L_{1} y_{2}.L_{2} for some k (k ≤ n), then – L_{0} ∈ J_{n−k}(u, T, V), and

– for any i (i = 1, 2), there exists some V′_{i} such that V′_{i}[F IV (L_{0})/{y_{i}}] ⊂ V and

L_{i} ∈ J_{n−k}(u, T, V′_{i}),

11. if M →^{∗k} κ v. L for some k (k ≤ n) and v ≠ u, then L ∈ J_{n−k}(u, T, V), and

12. if M →^{∗k} L v for some k (k ≤ n), then L ∈ J_{n−k}(u, T, V). Note that M ∈ J_{n}(u, T, V) is defined by induction on the lexicographic ordering of n and |M|.

Proposition 6.1.10 Let M be a term such that M ∈ J_{n}(u, T, V).

1. If m < n, then M ∈ J_{m}(u, T, V).

2. If M →^{∗k} N for some k (k ≤ n), then N ∈ J_{n−k}(u, T, V).

Proof. By induction on the lexicographic ordering of n and |M|.

Proposition 6.1.11 If T ⊂ T′ and V ⊂ V′, then J_{n}(u, T, V) ⊂ J_{n}(u, T′, V′) for any n and u. Proof. By induction on the lexicographic ordering of n and |M|. Proposition 6.1.12 If M ∈ J_{n}(u, T, V) and F IV (M) ⊂ V′ then M ∈ J_{n}(u, T, V′). Proof. By induction on the lexicographic ordering of n and |M|. Proposition 6.1.13 If u ∉ F T V (M), then M ∈ J_{n}(u, T, V) for any type T. Proof. By induction on the lexicographic ordering of n and |M|. Proposition 6.1.14 Let T be a regular type. Let M be a term, and v and w tag variables such that M ∈ J_{n}(u, T, V).

1. If w ≠ u, then M[w/v] ∈ J_{n}(u, T, V).

2. If M ∈ J_{n}(v, T, V), then M[w/v] ∈ J_{n}(u, T, V). Proof. By induction on the lexicographic ordering of n and |M|. Use Proposition 6.1.4. Definition 6.1.15 Let u be a tag variable, and T a type. We define J (u, T, V) as follows.

J (u, T, V) = {M | M ∈ J_{n}(u, T, V) for any n}.

Definition 6.1.16 Let u be a tag variable, and T a type. We define J^{−}(u, T, V) as follows. • if M = throw u K, then K ∈ T,

• if M is a normal form such that u ∈ F T V (M) and F IV (M)∩V = {}, then M = throw u L for some closed term L,

• if M = catch v L and v ≠ u, then L ∈ J (u, T, V),

• if M = throw v L, then L ∈ J (u, T, V),

• if M = λ y. L, then L ∈ J (u, T, V − {y}),

• if M = L_{1} L_{2}, then L_{1}, L_{2} ∈ J (u, T, V),

• if M = <L_{1}, L_{2}>, then L_{1}, L_{2} ∈ J (u, T, V),

• if M = proj_{i} L for some i (i = 1, 2), then L ∈ J (u, T, V),

• if M = inj_{i} L for some i (i = 1, 2), then L ∈ J (u, T, V),

• M = case L_{0} y_{1}.L_{1} y_{2}.L_{2}, then – L_{0} ∈ J (u, T, V), and

– for any i (i = 1, 2), there exists some V′_{i} such that V′_{i}[F IV (L_{0})/{y_{i}}] ⊂ V and

L_{i} ∈ J (u, T, V′_{i}),

• if M = κ v. L and v ≠ u, then L ∈ J (u, T, V), and

• if M = L v, then L ∈ J (u, T, V). Proposition 6.1.17 M ∈ J (u, T, V) if and only if

M →^{∗} N implies N ∈ J^{−}(u, T, V).

Proof. Obvious from the definitions. Proposition 6.1.18 If M ∈ J (u, T, V), then M →^{∗} N implies N ∈ J (u, T, V), that is, J (u, T, V) is a type. Proof. Straightforward from the previous proposition. Proposition 6.1.19 If u ∉ F T V (M), then M ∈ J (u, T, V) for any T and V. Obvious from Proposition 6.1.13 and Proposition 6.1.17. Proof. Proposition 6.1.20 If T ⊂ T′ and V ⊂ V′ then J (u, T, V) ⊂ J (u, T′, V′) for any tag variable u. Proof. Straightforward from Proposition 6.1.11 and Proposition 6.1.17. Proposition 6.1.21 Let u be a tag variable. If M ∈ J (u, T, V) and F IV (M) ⊂ V′ then M ∈ J (u, T, V′). Proof. Straightforward from Proposition 6.1.12 and Proposition 6.1.17. Proposition 6.1.22 Let T be a regular type. Let M be a term, and v and w tag variables such that M ∈ J (u, T, V).

1. If w ≠ u, then M[w/v] ∈ J (u, T, V).

2. If M ∈ J (v, T, V), then M[w/v] ∈ J (u, T, V). Proof. Straight forward from Proposition 6.1.14 and the definition of J (u, T, V). Proposition 6.1.23 If M ∈ J^{−}(u, T, V) and M →^{sub∗} M′, then M′ ∈ J^{−}(u, T, V). Proof. Straightforward from the definition of J^{−}(u, T, V) by Proposition 6.1.18. Definition 6.1.24 We define a set D^{−} of terms as follows. M ∈ D^{−} if and only if

1. for any proper subterm N of M, N ∈ D^{−}, and

2. if M is a normal form, then (a) if M = M_{1} M_{2} for some M_{1} and M_{2}, then F IV (M_{1}) ≠ {},

(b) if M = proj_{i} M′ for some i (i = 1, 2) and M′, then F IV (M′) ≠ {},

(c) if M = case M_{0} x.M_{1} y.M_{2} for some M_{0}, M_{1}, M_{2}, x and y, then F IV (M_{0}) ≠ {}, and (d) if M = M′ v for some M′ and v, then F IV (M′) ≠ {}.

Definition 6.1.25 Let C be a formula and X a frame. We define I^{−}(X , C) and I(X , C) inductively as follows.

• M ∈ I(X , C) iff

1. M ∈ X,

2. M is strongly normalizable, and

3. if M →^{∗} K, then K ∈ D^{−} ∩ I^{−}(X , C).

• If C is an atomic type expression, then M ∈ I^{−}(X , C) iff

1. if M is a normal form and F IV (M) = {}, then – M = throw u L for some u and L, or – M ∈ A(C).

• M ∈ I^{−}(X , C_{1} ⊃ C_{2}) iff

1. if M = λ y. L and K ∈ I(X , C_{1}), then L[K/y] ∈ I(X , C_{2}), and 2. if M is a normal form and F IV (M) = {}, then

– M = throw u L for some u and L, or – M = λ y. L for some y and L.

• M ∈ I^{−}(X , C_{1} ∧ C_{2}) iff

1. if M = <L_{1}, L_{2}>, then L_{1} ∈ I(X , C_{1}) and L_{2} ∈ I(X , C_{2}), and 2. if M is a normal form and F IV (M) = {}, then

– M = throw u L for some u and L, or – M = <L_{1}, L_{2}> for some L_{1} and L_{2}.

• M ∈ I^{−}(X , C_{1} ∨ C_{2}) iff

1. if M = inj_{i} L for some i (i = 1, 2), then L ∈ I(X , C_{i}), and

2. if M is a normal form and F IV (M) = {}, then – M = throw u L for some u and L, or – M = inj_{i} L for some i (i = 1, 2) and L.

• M ∈ I^{−}(X , C_{1} ◁ C_{2}) iff

1. if M = κ v. L, then L ∈ I(X , C_{1}) ∩ J (v, I(X , C_{2}), F IV (L)), and 2. if M is a normal form and F IV (M) = {}, then

– M = throw u L for some u and L, or – M = κ v. L for some v and L.

Proposition 6.1.26 Let X be a frame. I(X , C) is a regular type for any formula C. Proof. By induction on the structure of C. Use Proposition 5.3.5, Proposition 6.1.22 and the properties of the frame X.

Proposition 6.1.27 Let X be a frame. x ∈ I(X , C) for any type C and any individual variable x.

Proof. We get x ∈ X from the second property of frames. The other requirements for x ∈ I(X , C) are rather trivial since x is an individual variable.

Lemma 6.1.28 Let X be a frame. If throw u M ∈ I(X , A), then throw u M ∈ I(X , C) for any C.

Proof. Suppose that throw u M ∈ I(X , A). Obviously throw u M ∈ X and throw u M is strongly normalizable. Suppose that throw u M →^{∗} K. By the definition of →, K = throw v L for some v and L. Therefore, K ∈ I^{−}(X , C) for any formula C.

Lemma 6.1.29 Let X be a frame, and C a formula. If

1. M ∈ X,

2. M →^{sub∗} K implies K ∈ D^{−},

3. M →^{sub∗} K implies K ∈ I^{−}(X , C),

4. for any maximal proper subterm N of M, there exists some formula A such that N ∈ I(X , A), and

5. if M →^{sub∗} L ↦_{n} K for some L, then K ∈ I(X , C),

then M ∈ I(X , C).

Proof. First, we show that M is strongly normalizable. By the fourth premise, M is strongly normalizable w.r.t. →^{sub}. On the other hand, we get that L is strongly normalizable for any L such that M →^{sub∗} K ↦ L from the last premise. Therefore, so is M. Next, suppose that M →^{∗} K. It is enough to show that K ∈ D^{−} ∩ I^{−}(X , C) since M ∈ X by the first premise. There are three possible cases as follows:

1. M →^{sub∗} K,

2. M →^{sub∗} M′[throw v L/z] ↦_{t} throw v L →^{∗} K for some M′, z, v and L such that z ∈ F IV (M′) and M′ ≠ z.

3. M →^{sub∗} M′ ↦_{n} L →^{∗} K for some M′ and L.

In the first case, we get K ∈ D^{−} ∩ I^{−}(X , C) from the second and the third premises. In the second case, there exists some N such that N →^{∗} throw v L and N is a maximal proper subterm of M. Therefore, throw v L ∈ I(X , A) for some A by the fourth premise. We get throw v L ∈ I(X , C) by Lemma 6.1.28, and therefore, K ∈ D^{−} ∩ I^{−}(X , C) since throw v L →^{∗} K. As for the last case, it is obvious because L ∈ I(X , C) from the last premise. This completes the proof of M ∈ I(X , C).

Lemma 6.1.30 Let u be a tag variable, and T a type. If

1. M →^{sub∗} K implies K ∈ J^{−}(u, T, V),

2. M →^{sub∗} L ↦_{t} K implies K ∈ J (u, T, V), and

3. if M →^{sub∗} L ↦_{n} K for some L, then K ∈ J (u, T, V),

then M ∈ J (u, T, V).

Proof. Suppose that M →^{∗} K. There are three possible cases as follows:

1. M →^{sub∗} K,

2. M →^{sub∗} M′[throw v L/z] ↦_{t} throw v L →^{∗} K for some M′, z, v and L such that z ∈ F IV (M′) and M′ ≠ z,

3. M →^{sub∗} M′ ↦_{n} L →^{∗} K for some M′ and L.

It is enough to show that K ∈ J^{−}(u, T, V). In the first case, we get K ∈ J^{−}(u, T, V) from the first premise. In the second case, K ∈ J^{−}(u, T, V) because throw v L ∈ J (u, T, V) by the second premises. As for the third case, L ∈ J (u, T, V) from the last premise. Therefore, K ∈ J^{−}(u, T, V).

Definition 6.1.31 We define a type D as follows. M ∈ D iff

M →^{∗} K implies K ∈ D^{−} for any K.

Definition 6.1.32 A frame X is admissible if and only if

if M, N ∈ X ∩ J (u, T, V) and MN ∈ D, then MN ∈ J (u, T, V).

This property of admissible frames is crucial to the construction of the term model discussed here, but it is not trivial whether such a frame exists or not. We will give an example of admissible frame later.

Theorem 6.1.33 Let X be an admissible frame. Let Γ = {x_{1} : A_{1}, …, x_{m}: A_{m}} and Δ = {u_{1} : B_{1}, …, u_{n}: B_{n}}. Let Γ ⊢ M : C; Δ be a derivable judgement. Let N_{1}, …, N_{m} be terms such that N_{i} ∈ I(X , A_{i}) for any i (1 ≤ i ≤ m). Let u a tag variable, and V a finite set of individual variables. We define \overline{K} and \overline{U} as \overline{K} = K[N_{1}/x_{1}, …, N_{m}/x_{m}] and \overline{U} = U[F IV (N_{1})/{x_{1}}, …, F IV (N_{m})/{x_{m}}] for any K and U. Then,

• \overline{M} ∈ I(X , C), and (6.1)

• if N_{i} ∈ J (u, I(X , Δ^{t}(u)), V) for any i (1 ≤ i ≤ m), then

\overline{M} ∈ J (u, I(X , Δ^{t}(u)), \overline{Δ^{v}(u)} ∪ V),  (6.2)

where I(X , Δ^{t}(u)) = {} and Δ^{v}(u) = {} if u ∉ Dom(Δ).

Proof. Let Γ ⊢ M : C; Δ be a derivable judgement. By induction on the depth of the derivation. Suppose that

N_{i} ∈ I(X , A_{i}) for any i (1 ≤ i ≤ m).  (6.3)

First of all, we show \overline{M} ∈ X. Since Γ ⊢ M : C; Δ is derivable, M ∈ X by the last property of frames. Since N_{i} ∈ X by (6.3), we get \overline{M} ∈ X by the third property of frames. We show the rest properties of \overline{M} for (6.1) and (6.2) by cases according to the form of M.

Case 1: M is an individual variable. In this case, we can assume that M = x_{i} for some i. Therefore, obvious because \overline{M} = N_{i} and C = A_{i}.

Case 2: M = catch v M′ for some v and M′. That is, Γ ⊢ M′: C; Δ ⊔ {v: C^{V′}} is derivable for some V′. We can assume that v ∉ F T V (N_{i}) for any i. Let Δ′ be as Δ′ = Δ ⊔ {v: C^{V′}}. By the induction hypothesis,

\overline{M′} ∈ I(X , C).  (6.4)

On the other hand, since v ∉ F T V (N_{i}), we get

N_{i} ∈ J (v, I(X , Δ^{′t}(v)), {})  (6.5)

for any i by Proposition 6.1.19. Therefore, by the induction hypothesis, we get

\overline{M′} ∈ J (v, I(X , Δ^{′t}(v)), \overline{Δ^{′v}(v)}) = J (v, I(X , C), \overline{Δ^{′v}(v)}).  (6.6)

To show (6.1), we check the five premises of Lemma 6.1.29. We have \overline{M} ∈ X. For the second premise, suppose that \overline{M} →^{sub∗} K for some K. By the definition of →^{sub}, we get K = catch v K′ for some K′ such that \overline{M′} →^{∗} K′. Since \overline{M′} ∈ D by (6.4), we get K′ ∈ D^{−}. Therefore, K ∈ D^{−} from the form of K. For the third premise, suppose that \overline{M} →^{sub} K = catch v K′ for some K and K′ such that F IV (K) = F IV (K′) = {}. We show that K is not a normal form. Since v ∉ F T V (K′) implies K ↦_{n} K′, we assume that v ∈ F T V (K′). However, by (6.6), K′ = throw v L for some closed term L. This implies K = catch v throw v L ↦_{n} L, that is, K is not a normal form. Therefore, third premise is now obvious from the form of \overline{M} and the definition of I^{−}(X , C). On the other hand, the fourth premise holds for \overline{M} by (6.4). As for the last premise, suppose that \overline{M} →^{sub∗} L ↦_{n} K for some L. There are two possible cases as follows:

1. \overline{M} = catch v \overline{M′} →^{sub∗} catch v K ↦_{n} K,

2. \overline{M} = catch v \overline{M′} →^{sub∗} catch v (throw v K) ↦_{n} K,

where v ∉ F T V (K) in both cases. In the first case, since \overline{M′} →^{∗} K, we get K ∈ I(X , C) from (6.4). In the second case, since \overline{M′} →^{∗} throw v K, we get K ∈ I(X , C) from (6.6). We now get (6.1) by Lemma 6.1.29.

Next, we show (6.2). Suppose that N_{i} ∈ J (u, Δ^{t}(u), V) for any i. Since v ∉ \overline{M}, it is enough to show that \overline{M} ∈ J (u, I(X , Δ^{′t}(u)), \overline{Δ^{′v}(u)} ∪ V) by Proposition 6.1.19, and we can assume that v ≠ u. Since Δ^{t}(u) = Δ^{′t}(u), by the induction hypothesis,

\overline{M′} ∈ J (u, I(X , Δ^{′t}(u)), \overline{Δ^{′v}(u)} ∪ V).  (6.7)

We apply Lemma 6.1.30. For the first premise, suppose that \overline{M′} →^{sub∗} K = catch v K′ for some K and K′. We get K′ ∈ J^{−}(u, I(X , Δ^{′t}(u)), \overline{Δ^{′v}(u)} ∪ V) from (6.7). Suppose that u ∈ F T V (K) and F IV (K) ∩ (\overline{Δ^{′v}(u)} ∪ V) = \{\}. Since u ∈ F T V (K′), F IV (K′) = F IV (K) and \overline{M′} →^{∗} K′, we get K′ = throw u L for some closed term L from (6.7). That is, K is not a normal form. Therefore, the first premise is obvious from (6.7). For the second premise, suppose that \overline{M} →^{sub∗} L ↦_{t} K for some L. By the definition of →^{sub}, we get \overline{M′} →^{∗} K, and therefore, K ∈ J (u, I(X , Δ^{′t}(u)), \overline{Δ^{′v}(u)} ∪ V) from (6.7). To show that the last premise holds, suppose that \overline{M} →^{sub∗} L ↦_{n} K for some L. There are also the two possible cases above. Since \overline{M′} →^{∗} K or \overline{M′} →^{∗} throw v K, we get K ∈ J (u, I(X , Δ^{′t}(u)), \overline{Δ^{′v}(u)} ∪ V) from (6.7). We now get \overline{M} ∈ J (u, I(X , Δ^{′t}(u)), \overline{Δ^{′v}(u)} ∪ V) by Lemma 6.1.30.

Case 3: M = throw v M′ for some v and M′. That is, Γ′ ⊢ M′: E; Δ′ is derivable for some Γ′, E and Δ′ such that Γ′ ⊂ Γ and Δ = Δ′ ⊔ {v: E^{Dom(Γ′)}}. We can assume that Δ = Δ′ by Proposition 5.4.13. By the induction hypothesis,

\overline{M′} ∈ I(X , E).  (6.8)

To show (6.1), we check the premises of Lemma 6.1.29. We have \overline{M} ∈ X. For the second and the third premises, suppose that \overline{M} →^{sub∗} K. We show that K ∈ D^{−} for the second premise. By the definition of →^{sub}, K = throw v K′ for some K′ such that \overline{M′} →^{∗} K′. We get K′ ∈ D^{−} from (6.8). For the third premise, K ∈ I^{−}(X , C) is obvious from the form of K. We also get the fourth premise from (6.8). As for the last premise, it is impossible that \overline{M} →^{sub∗} L ↦_{n} K by the definition of →^{sub} and ↦_{n}. We now get (6.1) by Lemma 6.1.29.

Next, we show (6.2). Suppose that N_{i} ∈ J (u, I(X , Δ^{t}(u)), V) for any i. By the induction hypothesis,

\overline{M′} ∈ J (u, I(X , Δ^{t}(u)), \overline{Δ^{t}(u)} ∪ V).  (6.9)

We check the three premises of Lemma 6.1.30. For the first premise, suppose that \overline{M} →^{sub∗} K = throw v K′. If u = v, then we get K′ ∈ I(X , E) = I(X , Δ^{t}(v)) from (6.8) since \overline{M′} →^{∗} K′. On the other hand, we get K′ ∈ J (u, I(X , Δ^{t}(u)), \overline{Δ^{t}(u)} ∪ V). from (6.9). Now, suppose that u ∈ F T V (K), F IV (K) ∩ (\overline{Δ^{t}(u)} ∪ V) = \{\} and K is a normal form. If u ∈ F T V (K′), then we get K′ = throw u L for some L from (6.9). Therefore, u ∉ F T V (K′), that is, u = v. We get F IV (K′) = \{\} from F IV (K) ∩ (\overline{Δ^{t}(u)} ∪ V) = \{\} and

F IV (K) ⊂ F IV (\overline{M′}) ⊂ \overline{Dom(Γ′)} ⊂ \overline{Δ^{t}(v)}.

Therefore, if w ∈ F T V (K′) for some w, then K′ = throw w L for some L, and this implies that K is not a normal form. That is, K′ is a closed term. Thus, the first premise holds. For the second premise, suppose that \overline{M} →^{sub∗} L ↦_{t} K for some L. By the definition of →^{sub}, we get \overline{M′} →^{∗} K, and therefore, K ∈ J (u, I(X , Δ^{t}(u)), \overline{Δ^{v}(u)} ∪ V) from (6.9). Since it is impossible that \overline{M} →^{sub∗} L ↦_{n} K, we now get (6.2) by Lemma 6.1.30.

Case 4: M = λ y. M′ for some y and M′. That is, Γ ∪ {y: C_{1}} ⊢ M′: C_{2} ; Δ is derivable for some C_{1} and C_{2} such that C = C_{1} ⊃ C_{2} and y ∉ Δ^{v}(u) for any u ∈ Dom(Δ). We can assume that y ∉ V and y ∉ F IV (N_{i}) for any i. Since y ∈ I(X , C_{1}), by the induction hypothesis,

\overline{M′} ∈ I(X , C_{2}).  (6.10)

First, we show (6.1). We use Lemma 6.1.29. We have \overline{M} ∈ X. For the second premise, suppose that \overline{M} →^{sub∗} K for some K. By the definition of →^{sub}, we get K = λ y. K′ for some K′ such that \overline{M′} →^{∗} K′. We get K′ ∈ D^{−} from (6.10). Therefore, the second premise holds. As for the third premise, suppose that \overline{M} = λ y. \overline{M′} →^{sub∗} λ y. L. To show that λ y. L ∈ I^{−}(X , C_{1} ⊃ C_{2}), suppose that K ∈ I(X , C_{1}). By the induction hypothesis,

M′[N_{1}/x_{1}, …, N_{m}/x_{m}, K/y] ∈ I(X , C_{2}).

On the other hand, M′[N_{1}/x_{1}, …, N_{m}/x_{m}, K/y] = \overline{M′}[K/y] →^{∗} L[K/y]. Therefore, L[K/y] ∈

I(X , C_{2}). The fourth premise is also satisfied by (6.10). As for the last premise, it is impossible that \overline{M} →^{sub∗} L ↦_{n} K by the definition of →^{sub} and ↦_{n}. We now get (6.1).

Next, we show (6.2). Suppose that N_{i} ∈ J (u, I(X , Δ^{t}(u)), V) for any i. Since y ∈ J (u, I(X , Δ^{t}(u)), V), by the induction hypothesis,

\overline{M′} ∈ J (u, I(X , Δ^{t}(u)), \overline{Δ^{v}(u)} ∪ V).  (6.11)

Since y ∉ Δ^{v}(u), y ∉ V and y ∉ F IV (N_{i}) for any i,

y ∉ \overline{Δ^{v}(u)} ∪ V.  (6.12)

We apply Lemma 6.1.30. For the first premise, suppose that \overline{M} →^{sub∗} K = λ y. K′. We get

K′ ∈ J (u, I(X , Δ^{t}(u)), (\overline{Δ^{v}(u)} ∪ V) − \{y\})

from (6.11) and (6.12). Suppose that u ∈ F T V (K) and F IV (K) ∩ (\overline{Δ^{v}(u)} ∪ V) = \{\}. Since F IV (K′) ⊂ F IV (K) ∪ \{y\}, we get F IV (K′) ∩ (\overline{Δ^{v}(u)} ∪ V) = \{\} by (6.12). Therefore, K′ = throw u L for some closed term L. This implies that K is not a normal form. Thus, the first premise holds. For the second premise, if \overline{M} →^{sub∗} L ↦_{t} K for some L, then we get \overline{M′} →^{∗} K, and therefore, K ∈ J (u, I(X , Δ^{t}(u)), \overline{Δ^{v}(u)} ∪ V) from (6.11). Since the last premise is trivial, we get (6.2) by Lemma 6.1.30.

Case 5: M = M_{1} M_{2} for some M_{1} and M_{2}. That is, Γ_{1} ⊢ M_{1} : D ⊃ C; Δ_{2} and Γ_{2} ⊢ M_{2} : D; Δ_{2} are derivable for some Γ_{1}, Γ_{2}, D, Δ_{1} and Δ_{2} such that Γ = Γ_{1} ∪ Γ_{2} and Δ = Δ_{1} ⊔ Δ_{2}. By the induction hypothesis,

\overline{M_{1}} ∈ I(X , D ⊃ C),  (6.13)
\overline{M_{2}} ∈ I(X , D).  (6.14)

First, we show (6.1) by applying Lemma 6.1.29. We have \overline{M} ∈ X. For the second premise, suppose that \overline{M} →^{sub∗} K for some K. By the definition of →^{sub}, we get K = K_{1} K_{2} for some K_{1} and K_{2} such that \overline{M_{1}} →^{∗} K_{1} and \overline{M_{2}} →^{∗} K_{2}. We get K_{1}, K_{2} ∈ D^{−} from (6.13) and (6.14). Suppose that K is a normal form. We get F IV (K_{1}) ≠ {} since F IV (K_{1}) = {} implies that

• K_{1} = throw v L and K ↦_{t} throw v L for some v and L, or

• K_{1} = λ y. L and K ↦_{n} L[K_{2}/y] for some y and L,

by (6.13). Therefore, K ∈ D^{−}. For the third premise, we similarly get that K is not a normal form if \overline{M} →^{sub∗} K and F IV (K) = \{\}. The fourth premise is obvious from (6.13) and (6.14). As for the last premise, suppose that \overline{M} →^{sub∗} L ↦_{n} K, that is, for some y, L_{1} and L_{2},

\overline{M_{1}} \overline{M_{2}} →^{sub∗} (λ y. L_{1}) L_{2} ↦_{n} L_{1}[L_{2}/y] = K.

Therefore, K ∈ I(X , C) from (6.13) and (6.14). We now get

\overline{M_{1}} \overline{M_{2}} ∈ I(X , C)  (6.15)

by Lemma 6.1.29.

Now, we show (6.2). Suppose that N_{i} ∈ J (u, I(X , Δ^{t}(u)), V) for any i. By the induction hypothesis, \overline{M_{1}} ∈ J (C, I(X , Δ_{1}^{t}(u)), \overline{Δ_{1}^{v}(u)} ∪ V) and \overline{M_{2}} ∈ J (C, I(X , Δ_{2}^{t}(u)), \overline{Δ_{2}^{v}(u)} ∪ V). Therefore, we get

\overline{M_{1}}, \overline{M_{2}} ∈ J (u, I(X , Δ^{t}(u)), \overline{Δ^{v}(u)} ∪ V).

Since X is admissible, we get \overline{M} ∈ J (u, I(X , Δ^{t}(u)), \overline{Δ^{v}(u)} ∪ V) from (6.13), (6.14) and (6.15).

Case 6: M = κ v. M′ for some v and M′. That is, Γ ⊢ M′: C_{1} ; Δ ⊔ {v: C_{2}^{V′}} is derivable for some C_{1}, C_{2} and V′ such that C = C_{1} ◁ C_{2}. We can assume that v ∉ F T V (N_{i}) for any i. Let Δ′ be as Δ′ = Δ ⊔ {v: C_{2}^{V′}}. By the induction hypothesis,

\overline{M′} ∈ I(X , C_{1}).  (6.16)

To show (6.1), we check the premises of Lemma 6.1.29. We have \overline{M} ∈ X. For the second premise, suppose that \overline{M} →^{sub∗} K for some K. By the definition of →^{sub}, we get K = κ v. K′ for some K′ such that \overline{M′} →^{∗} K′. We get K′ ∈ D^{−} from (6.16). Therefore, the second premise holds. For the third premise, suppose that \overline{M} = κ v. \overline{M′} →^{sub∗} κ v. L. We show that κ v. L ∈ I^{−}(X , C_{1} ◁ C_{2}). Since \overline{M′} →^{∗} L, we get L ∈ I(X , C_{1}) from (6.16). On the other hand, we get N_{i} ∈ J (v, I(X , C_{2}), {}) since v ∉ F T V (N_{i}) for any i. Therefore, by the induction hypothesis,

\overline{M′} ∈ J (v, I(X , C_{2}), \overline{Δ^{′v}(v)}).

Since \overline{M′} →^{∗} L, we get L ∈ J (v, I(X , C_{2}), \overline{Δ^{′v}(v)}), and therefore, L ∈ J (v, I(X , C_{2}), F IV (L))

by Proposition 6.1.21. As for the last premise, it is impossible that \overline{M} →^{sub∗} L ↦_{n} K by the definition of →^{sub} and ↦_{n}. We now get (6.1) by Lemma 6.1.29.

Next, we show (6.2). Suppose that N_{i} ∈ J (u, I(X , Δ^{t}(u)), V) for any i. Since v ∉ \overline{M}, it is enough to show that \overline{M} ∈ J (u, I(X , Δ^{′t}(u)), \overline{Δ^{′v}(u)} ∪ V) by Proposition 6.1.19, and we can assume that v ≠ u. Since Δ^{t}(u) = Δ^{′t}(u), by the induction hypothesis,

\overline{M′} ∈ J (u, I(X , Δ^{′t}(u)), \overline{Δ^{′v}(u)} ∪ V).  (6.17)

We apply Lemma 6.1.30. For the first premise, suppose that \overline{M} →^{sub∗} K = κ v. K′ for some K and K′. We get K′ ∈ J^{−}(u, I(X , Δ^{′t}(u)), \overline{Δ^{′v}(u)} ∪ V) from (6.17). Suppose that u ∈ F T V (K)

and F IV (K) ∩ (\overline{Δ^{′v}(u)} ∪ V) = \{\}. Since u ∈ F T V (K′), F IV (K′) = F IV (K) and \overline{M′} →^{∗} K′, we

get K′ = throw u L for some closed term L from (6.17). Therefore, K is not a normal form. Thus, the first premise holds. For the second premise, if \overline{M} →^{sub∗} L ↦_{t} K for some L, then we get K ∈ J (u, I(X , Δ^{′t}(u)), \overline{Δ^{′v}(u)} ∪ V) from (6.17) since \overline{M′} →^{∗} K. Since the last premise is trivial, we get (6.2) by Lemma 6.1.30.

Case 7: M = M′ v for some M′ and v. That is, Γ′ ⊢ M′: C ◁ E; Δ′ is derivable for some Γ′, E and Δ′ such that Γ′ ⊂ Γ and Δ = Δ′ ⊔ {v: E^{Dom(Γ′)}}. We can assume that Δ = Δ′ by Proposition 5.4.13. By the induction hypothesis,

\overline{M′} ∈ I(X , C ◁ E).  (6.18)

To show (6.1), we check the premises of Lemma 6.1.29. We have \overline{M} ∈ X. For the second premise, suppose that \overline{M} →^{sub∗} K for some K. We show that K ∈ D^{−}. By the definition of →^{sub}, we get K = K′ v for some K′ such that \overline{M′} →^{∗} K′. We get K′ ∈ D^{−} from (6.18). If F IV (K) = \{\}, then we get K′ = throw v′ L or K′ = κ v′. L for some v′ and L from (6.18), that is, K is not a normal form. Thus, we get K ∈ D^{−}. For the third premise, we similarly get that K is not a normal form if \overline{M} →^{sub∗} K and F IV (K) = \{\}. The fourth premise is obvious from (6.18). As for the last premise, suppose that \overline{M} →^{sub∗} L ↦_{n} K, that is, for some v′ and L′,

\overline{M′} v →^{sub∗} (κ v′. L′) v ↦_{n} L′[v/v′] = K.

We get L′ ∈ I(X , C) from (6.18) by the definition of I(X , C ◁ E), and therefore, K ∈ I(X , C) since I(X , C) is a regular type. We now get \overline{M} ∈ I(X , C) by Lemma 6.1.29.

Next, we show (6.2). Suppose that N_{i} ∈ J (u, I(X , Δ^{t}(u)), V) for any i. By the induction hypothesis,

\overline{M′} ∈ J (u, I(X , Δ^{t}(u)), \overline{Δ^{v}(u)} ∪ V).  (6.19)

We apply Lemma 6.1.30. For the first premise, suppose that \overline{M} →^{sub∗} K = K′ v. We get K′ ∈ J (u, I(X , Δ^{t}(u)), \overline{Δ^{v}(u)} ∪ V) from (6.19). Suppose that u ∈ F T V (K) and F IV (K) ∩ (\overline{Δ^{v}(u)} ∪ V) = {}. We show that K is not a normal form. Since F IV (K′) = F IV (K), we get

F IV (K′) ∩ (\overline{Δ^{v}(u)} ∪ V) = \{\}.

If u ∈ F T V (K′), then K′ = throw u L for some closed term L from (6.19), and this implies that K is not a normal form. On the other hand, if u = v, then F IV (K′) = {} since F IV (K) ⊂ F IV (\overline{M′}) ⊂ \overline{Dom(Γ′)} ⊂ \overline{Δ^{v}(v)}. Therefore, if K′ is a normal from, then K′ = throw w L or K′ = κ w. L for some w and L by (6.18). This implies that K is not a normal form. Thus, the first premise holds. For the second premise, if \overline{M} →^{sub∗} L ↦_{t} K for some L, then we get \overline{M′} →^{∗} K, and therefore, K ∈ J (u, I(X , Δ^{t}(u)), \overline{Δ^{v}(u)} ∪ V) from (6.19). As for the last premise, suppose that \overline{M} →^{sub∗} L ↦_{n} K for some L and K, that is, \overline{M} →^{sub∗} (κ v′. L′) v ↦_{n} L′[v/v′] = K for some v′ and L′. We get

L′ ∈ J (u, I(X , Δ^{t}(u)), \overline{Δ^{v}(u)} ∪ V)  (6.20)

from (6.19). If v ≠ u, then L′[v/v′] ∈ J (u, I(X , Δ^{t}(u)), \overline{Δ^{v}(u)} ∪ V) by Proposition 6.1.22. Therefore, we assume that v = u. We have L′ ∈ J (v, I(X , E), F IV (L′),) by (6.18). Since Δ^{t}(u) = Δ^{t}(v) = E and F IV (L′) ⊂ F IV (\overline{M}) ⊂ \overline{Δ^{v}(v)} = \overline{Δ^{v}(u)}, we get

L′ ∈ J (v, I(X , Δ^{t}(u)), \overline{Δ^{v}(u)} ∪ V)

by Proposition 6.1.20. Therefore, L′[v/v′] ∈ J (u, I(X , Δ^{t}(u)), \overline{Δ^{v}(u)}∪V) from (6.20) by Proposition 6.1.22. We now get (6.2) by Lemma 6.1.30.

Case 8: M has one of the other forms. We similarly get (6.1) and (6.2) by Lemma 6.1.29 and Lemma 6.1.30, respectively.

6.2 An admissible frame

Definition 6.2.1 A tag dependency is a finite mapping which assigns a set of individual variables to each tag variable in its domain. We use δ, δ′, … to denote tag dependencies. Let u_{1}, …, u_{n} be tag variables, and let V_{1}, …, V_{n} be sets of individual variables such that if u_{i} = u_{j} then V_{i} = V_{j} for any i and j. We use {u_{1} : V_{1}, …, u_{n}: V_{n}} to denote a tag dependency whose domain is {u_{1}, …, u_{n}} and which assigns V_{i} to u_{i} for each i.

Definition 6.2.2 Let δ and δ′ be tag dependencies. We define a tag dependency δ⊔δ′ as follows.

Dom(δ ⊔ δ′) = Dom(δ) ∪ Dom(δ′)
(δ ⊔ δ′)(u) = \{ \begin{matrix}δ(u) ∪ δ′(u) & if u ∈ Dom(δ) ∩ Dom(δ′) \\ δ(u) & if u ∈ Dom(δ) and u ∉ Dom(δ′) \\ δ′(u) & if u ∉ Dom(δ) and u ∈ Dom(δ′) \end{matrix}

Definition 6.2.3 Let M be a term. Let U and δ be a set of individual variables and a tag dependency, respectively, where δ(u) ⊂ U for any u ∈ Dom(δ). Frame judgements have the following form.

U ⊢_{f} M ; δ

Definition 6.2.4 We define a formal system for frame judgements.

U ∪ {x} ⊢_{f} x; δ (var)  U ⊢_{f} c; δ (const)

{U ⊢_{f} M ; δ ⊔ \{u: V \} \atop U ⊢_{f} catch u M ; δ} (catch)  {U_{1} ⊢_{f} M ; δ \atop U_{1} ∪ U_{2} ⊢_{f} throw u M ; δ ⊔ \{u: U_{1}\}} (throw)

{U ∪ \{x\} ⊢_{f} M ; δ \atop U ⊢_{f} λ x. M ; δ} ^{(⊃-I ) (x ∉ δ(u) for any u ∈ Dom(δ))}

\begin{matrix}U_{1} ⊢_{f} M ; δ_{1} & U_{2} ⊢_{f} N ; δ_{2} \\ U_{1} ∪ U_{2} ⊢_{f} M N ; δ_{1} ⊔ δ_{2} \end{matrix} (⊃-E )

{U ⊢_{f} M ; δ ⊔ \{u: V \} \atop U ⊢_{f} κ u. M ; δ} (◁-I ) {U_{1} ⊢_{f} M ; δ \atop U_{1} ∪ U_{2} ⊢_{f} M u; δ ⊔ \{u: U_{1}\}} (◁-E )

\begin{matrix}U_{1} ⊢_{f} M ; δ_{1} & U_{2} ⊢_{f} N ; δ_{2} \\ U_{1} ∪ U_{2} ⊢_{f} <M, N>; δ_{1} ⊔ δ_{2} \end{matrix} (∧-I )

{U ⊢_{f} M ; δ \atop U ⊢_{f} proj1 M ; δ} (∧_{1}-E )  {U ⊢_{f} M ; δ \atop U ⊢_{f} proj2 M ; δ} (∧_{2}-E )

{U ⊢_{f} M ; δ \atop U ⊢_{f} inj1 M ; δ} (∨_{1}-I )  {U ⊢_{f} M ; δ \atop U ⊢_{f} inj2 M ; δ} (∨_{2}-I )

\begin{matrix}U_{1} ⊢_{f} L; δ_{1} & U_{2} ∪ \{x\} ⊢_{f} M ; δ_{2} & U_{3} ∪ \{y\} ⊢_{f} N ; δ_{3} \\ U_{1} ∪ U_{2} ∪ U_{3} ⊢_{f} case L x.M y.N ; δ_{1} ⊔ δ_{2}[U_{1}/\{x\}] ⊔ δ_{3}[U_{1}/\{y\}] \end{matrix} (∨-E )

We presents a some basic properties of this formal system.

Proposition 6.2.5 Let M be a term. Let Γ be an individual context, C a formula, and Δ a tag context. If Γ ⊢ M : C; Δ is derivable, then Dom(Γ) ⊢_{f} M ; Δ^{v} is derivable.

Proof. Straightforward induction on the derivation of Γ ⊢ M : C; Δ.

Proposition 6.2.6 If U ⊢_{f} M ; δ is derivable, then F IV (M) ⊂ U and F T V (M) ⊂ Dom(δ).

Proof. By induction on the derivation of U ⊢_{f} M ; δ.

Definition 6.2.7 Let δ and δ′ be tag dependencies. We define a relation δ ⊏ δ′ as follows. The relation δ ⊏ δ′ holds if and only if

• Dom(δ) ⊂ Dom(δ′), and

• δ(u) ⊂ δ′(u) for any u ∈ Dom(δ).

Proposition 6.2.8 Let U ⊢_{f} M ; δ be a d-derivable frame judgement.

1. If U ⊂ U′ and δ ⊏ δ′, then U′ ⊢_{f} M ; δ′ is also d-derivable.

2. U[{y}/{x}] ⊢_{f} M[y/x] ; δ[{y}/{x}] is also d-derivable.

3. If δ[v/u] is well defined, then U ⊢_{f} M[v/u] ; δ[v/u] is also d-derivable.

Proof. By simultaneous inductions on d.

Proposition 6.2.9 Let x and u be as x ∉ F IV (M) and u ∉ F T V (M).

1. If U ∪ {x} ⊢_{f} M ; δ is derivable, then U ⊢_{f} M ; δ[{}/{x}] is also derivable.

2. If U ⊢_{f} M ; δ ⊔ {u: V } is derivable, then U ⊢_{f} M ; δ is also derivable.

Proof. Straightforward induction on the derivations.

Proposition 6.2.10 If U_{1} ⊢_{f} N ; δ_{1} and U_{2} ∪ {x} ⊢_{f} M ; δ_{2} are derivable, then U_{1} ∪ U_{2} ⊢_{f} M[N/x] ; δ_{1} ⊔ δ_{2}[U_{1}/{x}] is also derivable.

Proof. By induction on the depth of the derivation of U_{2} ∪ {x} ⊢_{f} M ; δ_{2}. Suppose that U_{1} ⊢_{f} N ; δ_{1} and U_{2} ∪ {x} ⊢_{f} M ; δ_{2} are derivable. First, suppose also that x ∉ F IV (M), that is, M[N/x] = M. Since U_{2} ∪{x} ⊢_{f} M ; δ_{2} is derivable, so is U_{2} ⊢_{f} M ; δ_{2}[{}/{x}] by Proposition 6.2.9, and this implies that U_{1} ∪U_{2} ⊢_{f} M ; δ_{1} ⊔δ_{2}[U_{1}/{x}] is derivable by Proposition 6.2.8. Therefore, we now assume that

x ∈ F IV (M).  (6.21)

By cases according to the form of M.

Case 1: M = y for some individual variable y. In this case, y ∈ U_{2} ∪ {x}. If M = x, then we can derive U_{1} ∪ U_{2} ⊢_{f} M[N/x] ; δ_{1} ⊔ δ_{2}[Dom(U_{1})/{x}] by applying Proposition 6.2.8 to the derivation of U_{1} ⊢_{f} N ; δ_{1} since M[N/x] = N and C = A in this case. If M ≠ x, then we can derive it by (var) since M[N/x] = y and y ∈ U_{2} in this case.

Case 2: M = catch u M′ for some u and M′. In this case, the following judgement is derivable for some V.

U_{2} ∪ {x} ⊢_{f} M′; δ_{2} ⊔ {u: V }

We can assume that u ∉ Dom(δ_{1}) by Proposition 6.2.8. By the induction hypothesis, we have a derivation of

U_{1} ∪ U_{2} ⊢_{f} M′[N/x] ; δ_{1} ⊔ (δ_{2} ⊔ {u: V })[Dom(U_{1})/{x}].  (6.22)

Since u ∉ Dom(δ_{1}), we get M[N/x] = catch u (M′[N/x]). By applying (catch) to (6.22), we get U_{1} ∪ U_{2} ⊢_{f} M[N/x] ; δ_{1} ⊔ δ_{2}[Dom(U_{1})/{x}].

Case 3: M = throw u M′ for some u and M′. In this case, the following judgement is derivable for some U′_{2} and δ such that U′_{2} ⊂ U_{2} ∪ {x} and δ_{2} = δ ⊔ {u: U′_{2}}.

U′_{2} ⊢_{f} M′; δ

We get x ∈ F IV (M′) from (6.21), that is, x ∈ U′_{2}. Let U be as U = U′_{2} − {x}. Note that U′_{2} = U ∪ {x}. Therefore, by Proposition 6.2.8,

U ∪ {x} ⊢_{f} M′; δ.

By the induction hypothesis, we have a derivation of

U_{1} ∪ U ⊢_{f} M′[N/x] ; δ_{1} ⊔ δ[U_{1}/{x}].

Since M[N/x] = throw u (M′[N/x]), by applying (throw),

U_{1} ∪ U ⊢_{f} M[N/x] ; δ_{1} ⊔ δ[U_{1}/{x}] ⊔ {u: U_{1} ∪ U}.

Since U ⊂ U_{2}, by Proposition 6.2.8 again,

U_{1} ∪ U_{2} ⊢_{f} M[N/x] ; δ_{1} ⊔ δ[U_{1}/{x}] ⊔ {u: U_{1} ∪ U}.

Note that δ[U_{1}/{x}] ⊔ {u: U_{1} ∪ U} = δ_{2}[U_{1}/{x}] because δ_{2} = δ ⊔ {u: U ∪ {x}} and x ∉ U.

Case 4: M = λ y. M′ for some y and M′. In this case, y ∉ δ_{2}(u) for any u ∈ Dom(δ_{2}) and the following judgement is derivable.

U_{2} ∪ {x} ∪ {y} ⊢_{f} M′; δ_{2}

We can assume that y ∉ U_{1} by Proposition 6.2.8, and get M′[N/x] = λ y. (M[N/x]). By the induction hypothesis, we have a derivation of

U_{1} ∪ U_{2} ∪ {y} ⊢_{f} M′[N/x] ; δ_{1} ⊔ δ_{2}[U_{1}/{x}].  (6.23)

Since y ∉ δ_{2}(u) for any u ∈ Dom(δ_{2}) and y ∉ U_{1}, we get y ∉ (δ_{1} ⊔ δ_{2}[U_{1}/{x}])(u) for any u ∈ Dom(δ_{1} ⊔ δ_{2}[U_{1}/{x}]). Therefore, we can derive U_{1} ∪ U_{2} ⊢_{f} λ y. (M′[N/x]) ; δ_{1} ⊔ δ_{2}[U_{1}/{x}] by applying (⊃-I ) to (6.23).

Case 5: M has one of the other forms. Similarly, U_{1} ∪ U_{2} ⊢_{f} M[N/x] ; δ_{1} ⊔ δ_{2}[U_{1}/{x}] is derivable.

Lemma 6.2.11 If U ⊢_{f} M ; δ is derivable and M ↦_{t} throw v N, then U ⊢_{f} throw v N ; δ is also derivable.

Proof. By induction on the depth of the derivation of U ⊢_{f} M ; δ. Suppose that U ⊢_{f} M ; δ is derivable and M ↦_{t} throw v N. By cases according to the form of M.

Case 1: M = x for some individual variable x. This is impossible because M ↦_{t} throw v N.

Case 2: M = catch u M′ for some u and M′. In this case, the following judgement is derivable for some V.

U ⊢_{f} M′; δ ⊔ {u: V }  (6.24)

We get u ∉ F T V (throw v N) and

M′ = throw v N or M′ ↦_{t} throw v N

from M ↦_{t} throw v N. Therefore, from (6.24) or the induction hypothesis on (6.24),

U ⊢_{f} throw v N ; δ ⊔ {u: V }.

We get U ⊢_{f} throw v N ; δ by Proposition 6.2.9 since u ∉ F T V (throw v N).

Case 3: M = throw u M′ for some u and M′. In this case, the following judgement is derivable for some U′ and δ′ such that U′ ⊂ U and δ = δ′ ⊔ {u: U′}.

U′ ⊢_{f} M′; δ′  (6.25)

We get M′ = throw v N or M′ ↦_{t} throw v N from M ↦_{t} throw v N. Therefore, from (6.25) or the induction hypothesis on (6.25),

U′ ⊢_{f} throw v N ; δ′.

We get U ⊢_{f} throw v N ; δ by Proposition 6.2.8 since U′ ⊂ U and δ′ ⊏ δ.

Case 4: M = λ x. M′ for some x and M′. In this case, x ∉ δ(u) for any u ∈ Dom(δ) and the following judgement is derivable.

U ∪ {x} ⊢_{f} M′; δ  (6.26)

We get x ∉ F IV (throw v N) and

M′ = throw v N or M′ ↦_{t} throw v N

from M ↦_{t} throw v N. Therefore, from (6.26) or the induction hypothesis on (6.26),

U ∪ {x} ⊢_{f} throw v N ; δ.

We get U ⊢_{f} throw v N ; δ by Proposition 6.2.9 since x ∉ F IV (throw v N).

Case 5: M has one of the other forms. Similarly, U ⊢_{f} throw v N ; δ is derivable.

Lemma 6.2.12 If U ⊢_{f} M ; δ is derivable and M ↦_{n} N, then U ⊢_{f} N ; δ is also derivable.

Proof. By induction on the depth of the derivation of U ⊢_{f} M ; δ. Suppose that U ⊢_{f} M ; δ is derivable and M ↦_{n} N. By cases according to the form of M.

Case 1: M = catch u N and u ∉ F T V (N). In this case, U ⊢_{f} N ; δ ⊔ {u: V } is derivable for some V. We get U ⊢_{f} N ; δ by Proposition 6.2.9 since u ∉ F T V (N).

Case 2: M = catch u (throw u N) and u ∉ F T V (N). The following judgement is derivable for some V, U′ and δ′ such that U′ ⊂ U and δ ⊔ {u: V } = δ′ ⊔ {u: U′}.

U′ ⊢_{f} N ; δ′

Since U′ ⊂ U and δ′ ⊏ δ⊔{u: V }, U ⊢_{f} N ; δ⊔{u: V } is derivable by Proposition 6.2.8. Therefore, U ⊢_{f} N ; δ is also derivable by Proposition 6.2.9 since u ∉ F T V (N).

Case 3: M = (λ x. M_{1}) M_{2} and N = M_{1}[M_{2}/x] for some x, M_{1} and M_{2}. The following two judgements are derivable for some U_{1}, U_{2}, δ_{1} and δ_{2} such that U = U_{1} ∪ U_{2}, δ = δ_{1} ⊔ δ_{2} and x ∉ δ_{1}(u) for any u ∈ Dom(δ).

U_{1} ∪ {x} ⊢_{f} M_{1} ; δ_{1}  (6.27)
U_{2} ⊢_{f} M_{2} ; δ_{2}  (6.28)

We get U ⊢_{f} M_{1}[M_{2}/x] ; δ_{2} ⊔ δ_{1}[U_{2}/{x}] from (6.27) and (6.28) by Proposition 6.2.10, where δ_{2} ⊔ δ_{1}[U_{2}/{x}] = δ since x ∉ δ_{1}(u) for any u ∈ Dom(δ_{1}).

Case 4: M = (κ u. M′) v and N = M′[v/u] for some u, v and M′. The following judgement is derivable for some U′, δ′ and V such that U′ ⊂ U and δ = δ′ ⊔ {v: U′}.

U′ ⊢_{f} M′; δ′ ⊔ {u: V }

By Proposition 6.2.8, U′ ⊢_{f} M′[v/u] ; δ′[v/u] ⊔ {v: V } is derivable, and since U′ ⊂ U, by Proposition 6.2.8 again,

U ⊢_{f} M′[v/u] ; δ′[v/u] ⊔ {v: V }.

Since V ⊂ U′ and δ′(u) ⊂ U,

δ′[v/u] ⊔ {v: V } ⊏ δ′[v/u] ⊔ {v: U′} ⊏ δ′ ⊔ {v: U′} = δ.

Therefore, U ⊢_{f} M′[v/u] ; δ is derivable by Proposition 6.2.8.

Case 5: M has one of the other forms. Similar.

Lemma 6.2.13 If U ⊢_{f} M ; δ is derivable and M ↦ N, then U ⊢_{f} N ; δ is also derivable.

Proof. Straightforward from Lemma 6.2.11 and Lemma 6.2.12.

Proposition 6.2.14 If U ⊢_{f} M ; δ is derivable and M → N, then U ⊢_{f} N ; δ is also derivable.

Proof. By induction on the depth of the derivation of U ⊢_{f} M ; δ. Suppose that U ⊢_{f} M ; δ is derivable and M → N. If M ↦ N, then trivial by Lemma 6.2.13. Therefore we can assume that M → N and M {/ \atop ↦} N. By cases according to the form of M. A typical one is the case that M = throw u M′ for some u and M′. In this case,

U′ ⊢_{f} M′; δ′

is derivable for some U′ and δ′ such that U′ ⊂ U and δ = δ′ ⊔ {u: U′}. Since M → N and M {/ \atop ↦} N, M′ → N′ and N = throw u N′ for some N′. Therefore, U′ ⊢_{f} N′; δ′ is derivable by the induction hypothesis. We get U ⊢_{f} throw u N′; δ by applying (throw). The proofs for other cases are just similar.

Definition 6.2.15 We define a set of term X_{0} as follows:

X_{0} = { M | U ⊢_{f} M ; δ is derivable for some U and δ}.

Proposition 6.2.16 X_{0} is a frame. Proof. X_{0} is a type by Proposition 6.2.14, and is regular by Proposition 6.2.8. x ∈ X_{0} for any x, since {x} ⊢_{f} x; {} is derivable. On the other hand, M, N ∈ X_{0} implies M[N/x] ∈ X_{0} by Proposition 6.2.10. Finally, by Proposition 6.2.5, we get M ∈ X_{0} for any term M such that Γ ⊢ M : C; Δ is derivable for some Γ, C and Δ. Definition 6.2.17 Let n be a natural number, u a tag variable, and T a type. We define J_{n}^{−}(u, T, V) as follows.

• if M = throw u K, then K ∈ T,

• if M is a normal form such that u ∈ F T V (M) and F IV (M)∩V = {}, then M = throw u L for some closed term L,

• if M = catch v L and v ≠ u, then L ∈ J_{n}(u, T, V),

• if M = throw v L, then L ∈ J_{n}(u, T, V),

• if M = λ y. L, then L ∈ J_{n}(u, T, V − {y}),

• if M = L_{1} L_{2}, then L_{1}, L_{2} ∈ J_{n}(u, T, V),

• if M = <L_{1}, L_{2}>, then L_{1}, L_{2} ∈ J_{n}(u, T, V),

• if M = proj_{i} L for some i (i = 1, 2), then L ∈ J_{n}(u, T, V),

• if M = inj_{i} L for some i (i = 1, 2), then L ∈ J_{n}(u, T, V),

• if M = case L_{0} y_{1}.L_{1} y_{2}.L_{2}, then – L_{0} ∈ J_{n}(u, T, V), and

– for any i (i = 1, 2), there exists some V′_{i} such that V′_{i}[F IV (L_{0})/{y_{i}}] ⊂ V and

L_{i} ∈ J_{n}(u, T, V′_{i}),

• if M = κ v. L and v ≠ u, then L ∈ J_{n}(u, T, V), and

• if M = L v, then L ∈ J_{n}(u, T, V). Proposition 6.2.18 M ∈ J_{n}(u, T, V) if and only if

if M →^{∗k} K for some k (k ≤ n), then M ∈ J_{n−k}^{−}(u, T, V).

Proof. Obvious from the definitions. Lemma 6.2.19 Let n be a natural number, u a tag variable, and T a type. If

1. M ⟶^{sub∗k} K implies K ∈ J_{n−k}^{−}(u, T, V),

2. M ⟶^{sub∗k} L ↦_{t} K implies K ∈ J_{n−k−1}(u, T, V), and

3. if M ⟶^{sub∗k} L ↦_{n} K for some L, then K ∈ J_{n−k−1}(u, T, V),

then M ∈ J_{n}(u, T, V).

Proof. Suppose that M →^{∗k} K. There are three possible cases as follows:

1. M ⟶^{sub∗k} K,

2. M ⟶^{sub∗l} M′[throw v L/z] ↦_{t} throw v L →^{∗k−l−1} K for some M′, z, v and L such that z ∈ F IV (M′) and M′ ≠ z,

3. M ⟶^{sub∗l} M′ ↦_{n} L →^{∗k−l−1} K for some M′ and L.

It is enough to show that K ∈ J_{n−k}^{−}(u, T, V). In the first case, we get K ∈ J_{n−k}^{−}(u, T, V) from the first premise. In the second case, K ∈ J_{n−k}^{−}(u, T, V) because throw v L ∈ J_{n−l−1}(u, T, V) by the second premises. As for the third case, L ∈ J_{n−l−1}(u, T, V) from the last premise. Therefore, K ∈ J_{n−k}^{−}(u, T, V).

Lemma 6.2.20 Let M and N be terms. Let n be a natural number, u a tag variable, and T a type. If

1. U ⊢_{f} M ; δ is drivable,

2. M ∈ J_{n}(u, T, V − {x}),

3. N ∈ X_{0},

4. N ∈ J_{n}(u, T, V),

5. x ∉ δ(u), and

6. M[N/x] ∈ D,

then M[N/x] ∈ J_{n}(u, T, V).

Proof. By induction on the lexicographic ordering of n and |M|, and by cases according to the form of M. Suppose that U ⊢_{f} M ; δ and N ∈ X_{0} are drivable, M, N ∈ J_{n}(u, T, V), x ∉ δ(u) and M[N/x] ∈ D.

Case 1: M = y for some individual variable y. Trivial because M[N/x] = M or M[N/x] = N in this case.

Case 2: M = catch v M′ for some v and M′. We can assume that v ∉ F T V (N) ∪ {u}, that is, M[N/x] = catch v (M′[N/x]). Since U ⊢_{f} M ; δ is derivable, U ⊢_{f} M′; δ ⊔ {v: V′} is derivable for some V′. On the other hand, we get M′ ∈ J_{n}(u, T, V − {x}) from M ∈ J_{n}(u, T, V − {x}), and get x ∉ (δ⊔{v: V′})(u) from x ∉ δ(u) because u ≠ v. Therefore, by the induction hypothesis,

M′[N/x] ∈ J_{n}(u, T, V).  (6.29)

We use Lemma 6.2.19 to show that M[N/x] ∈ J_{n}(u, T, V). For the first premise, suppose that M[N/x] ⟶^{sub∗k} K = catch v K′ for some K and K′. We show that K ∈ J_{n−k}^{−}(u, T, V). We get K′ ∈ J_{n−k}(u, T, V) from (6.29). Suppose that u ∈ F T V (K) and F IV (K) ∩ V = {}. Since u ∈ F T V (K′), F IV (K′) = F IV (K) and M′[N/x] →^{∗} K′, we get K′ = throw u L for some closed term L from (6.29), and therefore, K is not a normal form. Thus, the first premise holds. For the second premise, suppose that M[N/x] ⟶^{sub∗k} L ↦_{t} K for some L. By the definition of →^{sub}, we get M′[N/x] →^{∗k+1} K. Therefore, K ∈ J_{n−k−1}(u, T, V) from (6.29). For the last premise, suppose that M[N/x] ⟶^{sub∗k} L ↦_{n} K for some k (k ≤ n) and L. There are two possible cases.

1. catch v (M′[N/x]) ⟶^{sub∗k} catch v K ↦_{n} K,

2. catch v (M′[N/x]) ⟶^{sub∗k} catch v (throw v K) ↦_{n} K,

where v ∉ F T V (K) in both cases. In the first case, since M′[N/x] ⟶^{sub∗k+1} K, we get K ∈ J_{n−k−1}(u, T, V) from (6.29). On the other hand, in the second case, since M′[N/x] ⟶^{sub∗k+1} throw v K, we also get K ∈ J_{n−k−1}(u, T, V) from (6.29). Thus, the last premise holds. We now get M[N/x] ∈ J_{n}(u, T, V) by Lemma 6.2.19.

Case 3: M = throw v M′ for some v and M′. In this case, M[N/x] = throw v (M′[N/x]). Since U ⊢_{f} M ; δ is derivable, U′ ⊢_{f} M′; δ′ is derivable for some U′ and δ′ such that U′ ⊂ U and δ = δ′ ⊔ {v: U′}. We can assume that δ = δ′ by Proposition 6.2.8. Note that F IV (M′) ⊂ U′. On the other hand, M′ ∈ J_{n}(u, T, V − {x}) from M ∈ J_{n}(u, T, V − {x}). Since x ∉ δ(u) = δ′(u), by the induction hypothesis,

M′[N/x] ∈ J_{n}(u, T, V).  (6.30)

We apply Lemma 6.2.19. For the first premise, suppose that M[N/x] ⟶^{sub∗k} K = throw v K′ for some K and K′. We show that K ∈ J_{n−k}^{−}(u, T, V). We get K′ ∈ J_{n−k}^{−}(u, T, V) from (6.30). If u = v, then we get M[N/x] = M since x ∉ δ(u) = δ(v) ⊃ U′ ⊃ F IV (M′), and therefore, K′ ∈ T from M ∈ J_{n}(u, T, V − {x}). Next, suppose that u ∈ F T V (K), F IV (K) ∩ V = {} and K is a normal form. If u ∈ F T V (K′), then we get K′ = throw u L for some L from (6.30). Since K is normal, we get u ∉ F T V (K′), that is, u = v and M[N/x] = M, again. This implies that K′ is a closed term since M ∈ J_{n}(u, T, V − {x}). For the second premise, suppose that M[N/x] ⟶^{sub∗k} L ↦_{t} K for some L. By the definition of →^{sub}, we get M′[N/x] →^{∗k+1} K, and therefore, K ∈ J_{n−k−1}(u, T, V) from (6.30). For the last premise, it is impossible that M[N/x] ⟶^{sub∗k} L ↦_{n} K by the definition of →^{sub} and ↦_{n}. Therefore, we get M[N/x] ∈ J_{n}(u, T, V) by Lemma 6.2.19.

Case 4: M = λ y. M′ for some y and M′. We can assume that y ∉ F IV (N), that is, M[N/x] = λ y. (M′[N/x]). Since U ⊢_{f} M ; δ is derivable, so is U ∪ {y} ⊢_{f} M′; δ. We get M′ ∈ J_{n}(u, T, V − {x} − {y}) from M ∈ J_{n}(u, T, V − {x}). On the other hand, N ∈ J_{n}(u, T, V − {y}) since y ∉ F IV (N). Therefore, by the induction hypothesis,

M′[N/x] ∈ J_{n}(u, T, V − {y}).  (6.31)

We use Lemma 6.2.19 to show λ y. (M′[N/x]) ∈ J_{n}(u, T, V). For the first premise, suppose that M[N/x] ⟶^{sub∗k} K. By the definition of →^{sub}, we get K = λ y. K′ for some K′ such that M′[N/x] →^{∗k} K′. We get K′ ∈ J_{n−k}(u, T, V −{y}) from (6.31). On the other hand, suppose that u ∈ F T V (K), F IV (K)∩V = {} and K is a normal form, that is, u ∈ F T V (K′), F IV (K′)∩(V − {y}) = {} and K′ is normal. Therefore, K′ = throw u L for some closed term L from (6.31), and this implies K ↦_{t} K′, that is, a contradiction. Thus, the first premise holds. For the second premise, suppose that M[N/x] ⟶^{sub∗k} L ↦_{t} K for some L, that is, M′[N/x] →^{∗k+1} K. Therefore, K ∈ J_{n−k−1}(u, T, V − {y}) from (6.31). We get K ∈ J_{n−k−1}(u, T, V) by Proposition 6.1.11. Since the last premise is trivial, we get M[N/x] ∈ J_{n}(u, T, V) by Lemma 6.2.19.

Case 5: M = M_{1} M_{2} for some M_{1} and M_{2}. In this case, M[N/x] = (M_{1}[N/x]) (M_{2}[N/x]). Since U ⊢_{f} M ; δ is derivable, U_{1} ⊢_{f} M_{1} ; δ_{1} and U_{2} ⊢_{f} M_{2} ; δ_{2} are derivable for some U_{1}, U_{2}, δ_{1} and δ_{2} such that U = U_{1} ∪ U_{2} and δ = δ_{1} ⊔ δ_{2}. We also get M_{1}, M_{2} ∈ J_{n}(u, T, V − {x}) from M ∈ J_{n}(u, T, V − {x}). Therefore, by the induction hypothesis,

M_{1}[N/x], M_{2}[N/x] ∈ J_{n}(u, T, V).  (6.32)

We use Lemma 6.2.19. For the first premise, suppose that M[N/x] ⟶^{sub∗k} K = K_{1} K_{2}, that is, M_{i}[N/x] →^{∗k} K_{i} for any i (i = 1, 2). We get K_{1}, K_{2} ∈ J_{n−k}(u, T, V) from (6.32). On the other hand, suppose that u ∈ F T V (K), F IV (K) ∩ V = {} and K is a normal form, that is, u ∈ F T V (K_{i}), F IV (K_{i}) ∩ V = {} and K_{i} is normal for some i. Therefore, K_{i} = throw u L for some closed term L from (6.32), and this implies K ↦_{t} K_{i}, that is, a contradiction. For the second premise, suppose that M[N/x] ⟶^{sub∗k} L ↦_{t} K for some L, that is, M_{i}[N/x] →^{∗k+1} K for some i (i = 1, 2). We get K ∈ J_{n−k−1}(u, T, V) from (6.32). For the last premise, suppose that M[N/x] ⟶^{sub∗k} L ↦_{n} K, that is, for some y, L_{1} and L_{2},

(M_{1}[N/x]) (M_{2}[N/x]) ⟶^{sub∗k} (λ y. L_{1}) L_{2} ↦_{n} L_{1}[L_{2}/y] = K.

By Proposition 6.1.10, we get λ y. L_{1} ∈ J_{n−k}(u, T, V) and L_{2} ∈ J_{n−k}(u, T, V) from (6.32). Therefore, L_{1} ∈ J_{n−k}(u, T, V − {y}) and L_{2} ∈ J_{n−k}(u, T, V). By Proposition 6.1.10 and Proposition 6.1.11,

L_{1}, L_{2} ∈ J_{n−k−1}(u, T, V).  (6.33)

On the other hand, U′ ⊢_{f} M_{1}[N/x] ; δ′ is derivable for some U′ and δ′ by Proposition 6.2.10 since M_{1}, N ∈ X_{0}, and therefore U′ ⊢_{f} λ y. L_{1} ; δ′ is also derivable by Proposition 6.2.14 since

M_{1}[N/x] →^{∗} λ y. L_{1}. That is,

U′ ∪ {y} ⊢_{f} L_{1} ; δ′  (6.34)

is derivable and

y ∉ δ′(u).  (6.35)

As for L_{2}, we get M_{2}[N/x] ∈ X_{0} from M_{2}, N ∈ X_{0} by Proposition 6.2.10. That is, L_{2} ∈ X_{0} by Proposition 6.2.14. Moreover, we get L_{1}[L_{2}/y] ∈ D from M[N/x] ∈ D since M[N/x] →^{∗} L_{1}[L_{2}/y]. Therefore, by the induction hypothesis, we get

K = L_{1}[L_{2}/y] ∈ J_{n−k−1}(u, T, V)

from (6.33), (6.34) and (6.35). Thus, the last premise also holds. We now get M[N/x] ∈ J_{n}(u, T, V) by Lemma 6.2.19.

Case 6: M = κ v. M′ for some v and M′. We can assume that v ∉ F T V (N) ∪ {u}, that is, M[N/x] = κ v. (M′[N/x]). Since U ⊢_{f} M ; δ is derivable, so is U ⊢_{f} M′; δ ⊔ {v: V′} for some V′. On the other hand, we get M′ ∈ J_{n}(u, T, V − {x}) from M ∈ J_{n}(u, T, V − {x}), and get x ∉ (δ ⊔ {v: V′})(u) from x ∉ δ(u) because u ≠ v. Therefore, by the induction hypothesis,

M′[N/x] ∈ J_{n}(u, T, V).  (6.36)

We use Lemma 6.2.19 For the first premise, suppose that M[N/x] ⟶^{sub∗k} K = κ v. K′. We show

that K ∈ J_{n−k}^{−}(u, T, V). We get K′ ∈ J_{n−k}^{−}(u, T, V) from (6.36) since M′[N/x] →^{∗k} K′. If

u ∈ F T V (K) and F IV (K) ∩ V = {}, then since u ∈ F T V (K′), we get K′ = throw u L for some L from (6.36), that is, K is not normal. Therefore, the first premise holds. For the second premise, suppose that M[N/x] ⟶^{sub∗k} L ↦_{t} K for some L. By the definition of →^{sub}, we get M′[N/x] →^{∗k+1} K, and therefore, K ∈ J_{n−k−1}(u, T, V) from (6.30). Since the last premise is trivial, we get (6.2) by Lemma 6.2.19.

Case 7: M = M′ v for some M′ and v. In this case, M[N/x] = (M′[N/x]) v. Since U ⊢_{f} M ; δ is derivable, U′ ⊢_{f} M′; δ′ is derivable for some U′ and δ′ such that U′ ⊂ U and δ = δ′ ⊔ {v: U′}. We can assume that δ = δ′ by Proposition 6.2.8. Note that F IV (M′) ⊂ U′. On the other hand, M′ ∈ J_{n}(u, T, V − {x}) from M ∈ J_{n}(u, T, V − {x}). Since x ∉ δ(u) = δ′(u), by the induction hypothesis,

M′[N/x] ∈ J_{n}(u, T, V).  (6.37)

We use Lemma 6.2.19 For the first premise, suppose that M[N/x] ⟶^{sub∗k} K = K′ v. We get K′ ∈ J_{n−k}^{−}(u, T, V) from (6.37) since M′[N/x] →^{∗k} K′. Suppose that u ∈ F T V (K) and F IV (K)∩V = {}. We show that K is not normal. If u ∈ F T V (K′), then K = throw u L for some closed term L by (6.37). On the other hand, u ∉ F T V (K′) implies u = v, and therefore, M[N/x] = M since x ∉ δ(u) = δ(v) ⊃ U′ ⊃ F IV (M′). Therefore, K is not normal since M ∈ J_{n}(u, T, V − {x}) and M →^{∗k} K = K′ v. For the second premise, suppose that M[N/x] ⟶^{sub∗k} L ↦_{t} K for some L. By the definition of →^{sub}, we get M′[N/x] →^{∗k+1} K, and therefore, K ∈ J_{n−k−1}(u, T, V) from (6.37). For the last premise, suppose that M[N/x] ⟶^{sub∗k} L ↦_{n} K, that is, for some L′ and w,

M′[N/x] v ⟶^{sub∗k} (κ w. L′) v ↦_{n} L′[v/w] = K.  (6.38)

We can assume that w ≠ u. Since M′[N/x] →^{∗k} κ w. L′, we get κ w. L′ ∈ J_{n−k}(u, T, V) from (6.37), that is,

L′ ∈ J_{n−k}(u, T, V).

Therefore, if v ≠ u, then we get K = L′[w/v] ∈ J_{n−k}(u, T, V) by Proposition 6.1.14, that is, K ∈ J_{n−k−1}(u, T, V) by Proposition 6.1.10. On the other hand, if v = u, then we get M[N/x] = M since x ∉ δ(u) = δ(v) ⊃ U′ ⊃ F IV (M′). Therefore, K ∈ J_{n−k−1}(u, T, V) since M ∈ J_{n}(u, T, V − {x}) and M →^{∗k+1} K. Thus, the last premise holds. We now get M[N/x] ∈ J_{n}(u, T, V) by Lemma 6.2.19.

Case 8: M has one of the other forms. The proof is similar.

Theorem 6.2.21 X_{0} is an admissible frame.

Proof. Since X_{0} is a frame by Proposition 6.2.16, we show that X_{0} is admissible. Suppose that

M, N ∈ X_{0} ∩ J_{n}(u, T, V), and  (6.39)
M N ∈ D.  (6.40)

By Proposition 6.1.17, it is enough to show that

M N ∈ J_{n}(u, T, V).

We use Lemma 6.2.19. For the first premise, suppose that M N ⟶^{sub∗k} K = K_{1} K_{2}, that is, M →^{∗k} K_{1} and N →^{∗k} K_{2}. We get K_{1}, K_{2} ∈ J_{n−k}(u, T, V) from (6.39). On the other hand, suppose that u ∈ F T V (K), F IV (K) ∩ V = {} and K is a normal form. Since u ∈ F T V (M) and F IV (K_{1}) ∩ V = {}, or u ∈ F T V (N) and F IV (K_{2}) ∩ V = {}, we get M = throw u L or N = throw u L for some closed term L from (6.39), and this implies K ↦_{t} throw u L, that is, a contradiction. For the second premise, suppose that M N ⟶^{sub∗k} L ↦_{t} K for some L, that is, M →^{∗k+1} K or N →^{∗k+1} K. We get K ∈ J_{n−k−1}(u, T, V) from (6.39). For the last premise, suppose that M N ⟶^{sub∗k} L ↦_{n} K, that is, for some y, L_{1} and L_{2},

M N ⟶^{sub∗k} (λ y. L_{1}) L_{2} ↦_{n} L_{1}[L_{2}/y] = K.

We get λ y. L_{1} ∈ J_{n−k}(u, T, V) and L_{2} ∈ J_{n−k}(u, T, V) from (6.39) by Proposition 6.1.10. Therefore, L_{1} ∈ J_{n−k}(u, T, V − {y}) and L_{2} ∈ J_{n−k}(u, T, V). By Proposition 6.1.10,

L_{1} ∈ J_{n−k−1}(u, T, V − {y}),  (6.41)
L_{2} ∈ J_{n−k−1}(u, T, V).  (6.42)

On the other hand, λ y. L_{1} ∈ X_{0} by Proposition 6.2.14 since M →^{∗} λ y. L_{1}. That is, for some U and δ,

U ∪ {y} ⊢_{f} L_{1} ; δ  (6.43)

is derivable and

y ∉ δ(u).  (6.44)

As for L_{2}, we get L_{2} ∈ X_{0} by Proposition 6.2.14 since N ∈ X_{0}. Moreover, we get L_{1}[L_{2}/y] ∈ D from M N ∈ D since M N →^{∗} L_{1}[L_{2}/y]. Therefore, by Lemma 6.2.20, we get

L_{1}[L_{2}/y] ∈ J_{n−k−1}(u, T, V)

from (6.41), (6.42), (6.43) and (6.44). Thus, the last premise also holds. Therefore, we get M N ∈ J_{n}(u, T, V) by Lemma 6.2.19.

6.3 Strong normalizability and normal forms

We get strong normalizability of well-typed terms from the discussion on the term model. The term model also provides a results on the form of well-typed normal forms.

Theorem 6.3.1 Let M be a term. If Γ ⊢ M : C; Δ is derivable for some Γ, C and Δ, then M is strongly normalizable.

Proof. Since x ∈ I(X_{0}, Γ(x)) for any x ∈ Dom(Γ), M ∈ I(X_{0}, C) by Theorem 6.1.33 on X_{0}. Therefore, M is strongly normalizable by the definition of I(X_{0}, C).

Theorem 6.3.2 Let M be a normal form such that F IV (M) = {}. If Γ ⊢ M : C; Δ is derivable for some Γ, C and Δ, then one of the following holds.

1. M = throw u L for some closed term L.

2. C is an atomic formula, and M is a constant.

6.4 Realizability interpretation of L_{c/t}  85

3. C = A ⊃ B for some A and B, and M = λ y. L for some y and L.

4. C = A ∧ B for some A and B, and M = <L_{1}, L_{2}> for some L_{1} and L_{2}.

5. C = A ∨ B for some A and B, and M = inj_{i} L for some i (i = 1, 2) and L.

6. C = A ◁ B for some A and B, and M = κ v. L for some v and L.

Proof. Let x_{1}, …, x_{m} be as Dom(Γ) = {x_{1}, …, x_{2}}, and suppose that Γ ⊢ M : C; Δ is derivable. Since F IV (M) = {}, {} ⊢ M : C; Δ[{}/{x_{1}}, …, {}/{x_{m}}] is also derivable by Proposition 5.4.14. Therefore, by Theorem 6.1.33 on X_{0},

M ∈ I(X_{0}, C) ∩ J (u, I(X_{0}, Δ^{t}(u)), {})

for any u. Since M is normal and F IV (M) = {}, if u ∈ F T V (M), then M = throw u L for some closed term L. On the other hand, if F T V (M) = {}, then one of 2 through 6 holds since M ∈ I^{−}(X_{0}, C) and F IV (M) = {}.

6.4 Realizability interpretation of L_{c/t}

Let X be an admissible frame, and let A be a mapping which assigns a subset of Const to each atomic type. The realizability for L_{c/t} is defined relatively to X and A.

Definition 6.4.1 (Realizability of types) Let M be a term, and A a type. We define a relation r between terms and types as follows.

M r A iff M ∈ I(X , A).

Definition 6.4.2 (Realizability of tag contexts) Let M be a term, and Δ a tag context. We define a relation r between terms and tag contexts as follows.

M r Δ iff for any u, M ∈ J (u, I(X , Δ^{t}(u)), Δ^{v}(u)),

where I(X , Δ^{t}(u)) = {} and Δ^{v}(u) = {} if u ∉ Dom(Δ).

Definition 6.4.3 (Interpretation) We define the interpretation of typing judgements as follows. The relation

{x_{1} : A_{1}, …, x_{m}: A_{m}} ⊢ ⊢ M : C; {u_{1} : B_{1}^{V_{1}}, …, u_{n}: B_{n}^{V_{n}}}

holds if and only if for any terms K_{1}, …, K_{m} such that K_{i} r A_{i} and x_{j} ∉ F IV (K_{i}) for any i and j (1 ≤ i, j ≤ m),

1. M[K_{1}/x_{1}, …, K_{m}/x_{m}] r C, and

2. if K_{i} r Δ for any i (1 ≤ i ≤ m), then

M[K_{1}/x_{1}, …, K_{m}/x_{m}] r Δ[F IV (K_{1})/{x_{1}}, …, F IV (K_{m})/{x_{m}}].

The following soundness theorem assures us that we can regard the derivations of L_{c/t} as programs which satisfy the specification defined by the realizability interpretation defined above.

Theorem 6.4.4 (Soundness of L_{c/t}) If Γ ⊢ M : C; Δ is derivable in L_{c/t}, then Γ ⊢ ⊢ M : C; Δ holds.

Proof. Straight forward from Theorem 6.1.33.

Concluding remarks

We have presented two typing systems Lc/t^{CBV} and L_{c/t} which capture the catch/throw mechanism in the notion of “proofs as programs”. Although they are just variants of the standard constructive logic, they admit extra conclusions besides the main one. By this feature, we can naturally construct proofs which handle the exceptional situations efficiently as in practical programming languages. We showed the direct correspondence between such proofs and programs which make use of the catch and throw mechanism by certain realizability interpretations. The soundness theorems of the systems relative to these interpretations assure that they can still be basises for the formal method of computer programming. Moreover, the non-determinism introduced with the catch and throw mechanism does not break this paradigm, because we can take the meanings of programs by a realizability interpretation independent of the evaluation strategy, that is, reductions do not preserve the meaning of programs as values, but do preserve the meaning as realizers.

From a computational point of view, the catch and throw mechanism provides only a restricted access to the current continuation, and does not provide the full access as the first class objects. Therefore, it could be regarded as a trivial subcase of more powerful facilities such as call/cc of Scheme. However, from the viewpoint of the notion of “proofs as programs”, it assures correct programs without any of the restrictions required for the case of such more powerful ones [11, 20, 21]. And more importantly, the catch and throw mechanism has a natural counterpart in the reasoning of programmers, that is, a characteristic way of exception handling. We doubt whether there also exists such a natural reasoning corresponding to the use of call/cc and its variants beyond the catch/throw.

From the viewpoint of program verification, our work can be regarded as a higher-order extension of the work concerning goto statements in Hoare’s logic, whose main idea is also the existence of extra post-conditions [1, 2]. However, it should be noted that our work captures the logic of programmers behind the facilities for non-local exit rather than their computational behavior. In this sense, the catch and throw mechanism is just a sample of possible realizers for our logic.

There remain some problems which have not been discussed in this thesis. We have considered only a propositional fragment, and have not investigated the relation between the catch and throw mechanism and mathematical inductions. Actually, the mechanism is often used in subroutines that call themselves recursively in practical programming. We could expect that the standard

\underline{87}

rules for mathematical inductions would work as well from just a logical point of view, but more intensive investigation of the practice should be done in order to capture the class of proofs, that is, the class of programs, used in practical programming.

Bibliography

[1] S. Alagić and M. A. Arbib, The Design of Well-Structured and Correct Programs, Springer-Verlag, 1978.

[2] M. A. Arbib and S. Alagić, Proof Rules for Gotos, Acta Informatica, Vol. 11, pp. 139-148, 1979.

[3] F. Barbanera ad S. Berardi, A Symmetric Lambda Calculus for “Classical” Program Extraction, Theoretical Aspects of Computer Software, M. Hagiya and J. C. Mitchell, eds., Lecture Notes in Computer Science 789, pp. 495-515, Springer-Verlag, 1994.

[4] H. P. Barendregt, The Lambda Calculus: Its Syntax and Semantics, North-Holland, 1984.

[5] R. L. Constable, et al., Implementing Mathematics with the Nuprl Proof Development System, Prentice-Hall, 1986.

[6] T. Coquand and G. Huet, The Calculus of Construction, Information and Computation, Vol. 76, pp. 95-120, 1988.

[7] M. Felleisen, D. Friedman, E. Kohlbecker, and B. Duba, A syntactic theory of sequential control, Theoretical Computer Science, Vol. 52(3), pp. 205-237, 1987.

[8] H. Friedman, Classically and intuitionistically provably recursive functions, Higher Set Theory, D. S. Scott and G. H. Muller, eds., Lecture Notes in Mathematics 699, pp. 21-28, Springer-Verlag, 1978.

[9] J.-Y. Girard, A new constructive logic: classical logic, Mathematical Structures in Computer Science, Vol. 1, pp. 255-296, 1991.

[10] J.-Y. Girard, Y. Lafont and P. Taylor, Proofs and Types, Cambridge University Press, 1989.

[11] T. G. Griffin, A formulae-as-types notion of control, Conf. Rec. ACM Symp. on Principles of Programming Languages, pp. 47-58, 1990.

[12] S. Hayashi, Singleton, Union and Intersection Types for Programs, Theoretical Aspects of Computer Software, T. Ito and A.R. Meyer, eds., Lecture Notes in Computer Science 526, pp. 701-730, Springer-Verlag, 1991.

[13] S. Hayashi and H. Nakano, PX: A Computational Logic, The MIT Press, 1988.

[14] W. A. Howard, The Formulae-as-types Notion of Constructions, To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pp. 479-490, Academic Press, 1980.

[15] B. W. Kernighan and D. M. Ritchie, The C programming language (2nd ed.), Prentice-Hall, 1989.

[16] S. C. Kleene, Introduction to Metamathematics, North-Holland, 1952.

[17] P. J. Landin, The mechanical evaluation of expressions, Computer Journal, Vol. 6(4), 1964.

[18] S. Maehara, Eine Darstellung intuitionistischen Logik in der Klassishen, Nagoya Math. Journal, Vol. 7, pp. 45-64, 1954.

[19] P. Martin-Löf, Constructive mathematics and computer programming, Logic, Methodology, and Philosophy of Science VI, L. J. Choen, et al., eds., North-Holland, pp. 153-179, 1982.

[20] C. R. Murthy, An evaluation semantics for classical proofs, Proc. 6th Annual IEEE Symp. on Logic in Computer Science, pp. 96-107, 1991.

[21] C. R. Murthy, Classical Proofs as Programs: How, What and Why, Technical Report TR 91-1215, Department of Computer Science, Cornell University, 1991.

[22] C. R. Murthy, A Computational Analysis of Girard’s Translation and LC, Proc. 7th Annual IEEE Symp. on Logic in Computer Science, pp. 72-81, 1992.

[23] H. Nakano, A Constructive Formalization of the Catch and Throw Mechanism, Proc. 7th Annual IEEE Symp. on Logic in Computer Science, pp. 82-89, 1992.

[24] H. Nakano, The Non-deterministic Catch and Throw Mechanism and Its Subject Reduction Property, Logic, Language and Computation, N. D. Jones, et al., eds., Lecture Notes in Computer Science 792, pp. 61-72, Springer-Verlag, 1994.

[25] H. Nakano, A constructive logic behind the catch and throw mechanism, Annals of Pure and Applied Logic, Vol. 69, pp. 269-301, 1994.

[26] N. N. Nepejvoda, A bridge between constructive logic and computer programming, Theoretical Computer Science, Vol. 90, pp. 253-270, 1991.

[27] M. Parigot, Free Deduction: An Analysis of “Computations” in Classical Logic, Proc. Russian Conf. on Logic Programming, A. Voronkov, ed., Lecture Notes in Computer Science 592, pp. 361-380, Springer-Verlag, 1991.

[28] M. Parigot, λμ-Calculus: An Algorithmic Interpretation of Classical Natural Deduction, Proc. Int’l Conf. on Logic Programming and Automated Reasoning, Lecture Notes in Computer Science 624, pp. 190-201, Springer-Verlag, 1992.

[29] M. Parigot, Classical Proof as Programs, Computational logic and theory, Lecture Notes in Computer Science 713, G. Gottlob, et al., eds., pp. 263-276, Springer-Verlag, 1993.

[30] G. D. Plotkin, Call-by-name, call-by-value and the λ-calculus, Theoretical Computer Science, Vol. 1, pp. 125-159, 1975.

[31] N. J. Rehof and M. H. Sørensen, The λ_{Δ}-calculus, Theoretical Aspects of Computer Software, M. Hagiya and J. C. Mitchell, eds., Lecture Notes in Computer Science 789, pp. 516-542, Springer-Verlag, 1994.

[32] G. L. Steele, Common Lisp: The Language, Digital Press, 1984.

[33] K. Schütte, Vollständige Systeme Modaler und Intuitionistischer Logik, Springer-Verlag, 1968.

[34] G. Takeuti, Proof theory (2nd ed.), North Holland, 1987.

[35] Y. Takayama, Extraction of Redundancy-free Programs from Constructive Natural Deduction Proofs, Journal of Symbolic Computation, Vol. 12, pp. 29-69, 1991.

[36] M. Tatsuta, Program Synthesis Using Realizability, Theoretical Computer Science, Vol. 90, pp. 309-353, 1991.