# A partially deadlock-free typed process calculus.

We propose a novel static type system for a process calculus, which ensures both partial deadlock-freedom and partial confluence. The key novel ideas are (1) introduction of the order of channel use as type information, and (2) classification of communication channels into reliable and unreliable channels based on their usage and a guarantee of the usage by the type system. We can ensure that communication on reliable channels never causes deadlock and also that certain reliable channels never introduce nondeterminism. After presenting the type system and formal proofs of its correctness, we show encodings of the A-calculus and typical concurrent objects in the deadlock-free fragment of the calculus and demonstrate how type information can be used for reasoning about program behavior.Categories and Subject Descriptors: D.3.1 [Programming Languages]: Formal Definitions and Theory; D.3.3 [Programming Languages]: Language Constructs and Features

General Terms: Languages

Additional Key Words and Phrases: Concurrency, deadlock-freedom, type theory

1. INTRODUCTION

1.1 Backgrounds and Problems

Various concurrent programming languages [Kobayashi 1996a; Peyton Jones 1996; Pierce and Turner 1997; Reppy 1991; Shapiro 1989; Yonezawa and Tokoro 1987] have recently been proposed and are attracting a great deal of attention because of their usefulness in describing symbolic/numeric computations for parallel or distributed environments and inherently concurrent applications such as GUIs. Many of them share some common primitives for concurrent computation-creations of first-class communication channels (which we here call channels for short), communication over those channels, and concurrent execution of processes-which have recently been studied extensively through process calculi [Honda and Yoshida 1995; Kobayashi et al. 1996; Milner et al. 1992; Pierce and Sangiorgi 1993; Sangiorgi 1992]. They have been found to be expressive enough to provide higher-level mechanisms such as concurrent objects [Kobayashi and Yonezawa 1995; Pierce and Turner 1995; Walker 1995].

However, such concurrency primitives are too low-level, and they suffer from serious problems: deadlock and nondeterminism. They often make it difficult to debug programs and to think about program behavior. For example, if we extend a functional programming language with concurrency primitives [Reppy 1991], a term of a function type may not behave like a function: it may return nondeterministic results, or may be blocked forever without returning the result. Deadlock and nondeterminism also make static decision of control flows difficult, disabling efficient implementation of concurrency primitives.

1.2 Our Approach

The goal of this article is to overcome the above problems by identifying deadlock-free and/or deterministic parts of concurrent programs with a static type system. The important observation behind this solution is that not all parts of concurrent programs suffer from deadlock and nondeterminism: most parts of actual programs should be deadlock-free and/or deterministic. The key ideas in our approach (especially for ensuring partial deadlock-freedom) are (1) to introduce the order of channel use as type information, and (2) to classify channels according to their usage and to enforce the usage by a type system.

To illustrate these ideas, we consider the following asynchronous process calculus (which is a subset of the calculus we consider in this article):

P ::= [P.sub.1]|[P.sub.2] (executes [P.sub.1] and [P.sub.2] concurrently)

x![y] (sends y along the channel x)

x?[z].P (receives values v along x and behaves like [v/z]P)

x?*[z].P (repeatedly receives values v along x

and spawns the process [v/z]P)

(vx) P (creates a channel x and executes P)

0 (becomes silent) Here y abbreviates a sequence [y.sub.1],..., [y.sub.n]. As in the [Pi]-calculus [Milner 1993], channels are first-class values in the sense that they can be dynamically created and passed as data along other channels. Note that x?* [z]. P behaves like a (recursive) process definition x![z] - P since the process x?*[z].P|x![v] is reduced to x?*[z].P|[v/z]P.

Let us write ?? [T] for the type of channels used for sending/receiving a sequence of values of types T. In earlier type systems for process calculi or concurrent languages [Gay 1993; Reppy 1991; Vasconcelos and Honda 1993], x?[]. y![] is typed as

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

The first key idea of the present work is to attach a time tag to each instance of a channel type constructor and keep ordering between them. So in our type system, the above type judgment is replaced by

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

where the relation {([t.sub.x], [t.sub.y])} expresses the fact that a channel x may be used before y (a more correct intuition is: "communication on y may be delayed until that on x is completed"). On the other hand, a process y?[]. X![] is typed as

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

where {([t.sub.y], [t.sub.x])} expresses the fact that a channel y may be used before x (or "communication on x may be delayed until that on y is completed"). Thus, if we make the parallel composition x?[].y![]|y?[].x![], we detect a cyclic ordering {([t.sub.y], [t.sub.x]), ([t.sub.y], [t.sub.x])} which indicates that the process may fall into deadlock because of bad use of the channels x and y. Let us consider the case where channels are passed as first-class values, [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] with the relation {([s.sub.y], [s.sub.z])} means that x is a channel to send/receive two channels y, z such that (1) a receiver from x cannot use y, z in an order unspecified by {([s.sub.y], [s.sub.z])} (i.e., it is not allowed to delay communication on y until that on z is completed), and (2) channels sent along x must be those that can be used in an order specified by {([s.sub.y], [s.sub.z])}. So the processes x?[y, z].(y?[].z![]), x?[y, z].(y?[].0|z![]) and x![u, v] are well-typed under [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] with {([s.sub.y], [s.sub.z])}, but neither x?[y,z].(z?[].y![]) nor x![u, v] |v?[].u![] is. (x![u,v]|v?[].u![] is not allowed because a receiver of x?[u, v] cannot use u before v as v?[].u![] uses v before u.) In general, a type judgment is written in the form [x.sub.1]: [T.sub.1],..., [x.sub.n]: [T.sub.n], ?? P, where [T.sub.1],..., [T.sub.n] are types annotated with time tags and ?? is a binary relation on time tags. To avoid deadlock, we require that the transitive closure of ?? should be a strict partial order.

The second key idea of the present work is to classify channels. Note that introduction of ordering information is itself not able to ensure freedom from deadlock completely. For example, although the process (vx) (x?[].y?[].0)|[y![] does not have any cyclic dependency on channel use, it is blocked forever. In order to reject such a process, we need to require, in addition to the lack of cyclic dependency, that every process communicating over a certain channel can eventually find its communication partner. We consider three kinds of such channels (which we call reliable channels) and ensure the correct usage of each channel by using a static type system. For other kinds of channels (unreliable channels), we give up ensuring deadlock-freedom.

By combining the above ideas, we can ensure that use of reliable channels does not cause deadlock. That is, (1) if only reliable channels are used in a process, deadlock never occurs, and (2) deadlock may occur if a process also uses unreliable channels, but only if there is bad use of the unreliable channels (when a process deadlocks, there is some subprocess trying to communicate over an unreliable channel). As will be demonstrated later, the lambda-calculus and typical concurrent objects can be encoded by using only reliable channels. From this observation and brief profiling of several concurrent programs for window systems and numerical computation, we expect that large parts of many concurrent programs can be written with reliable channels and that our type system helps programmers to pinpoint the source of deadlock in such programs.

1.3 Main Results

The main results of this work are (1) the formulation of typing rules to guarantee the channel usage and order of channel use mentioned above, and (2) formal proofs of the above claim that reliable channels never cause deadlock in a well-typed process.

In order to show the expressive power of reliable channels and demonstrate how type information can be used for reasoning on the program behavior, we show that every well-typed term of call-by-value, call-by-name, and call-by-need simply typed [Lambda]-calculi is encoded into a well-typed process of our process calculus without using unreliable channels, and we use the theorem on partial deadlock-freedom for inferring that the evaluation of those processes never gets stuck. Moreover, in the cases of the call-by-value and call-by-need lambda-calculi, type information is sufficient for us to infer that the result of the evaluation is unique (up to some typed process congruence [Kobayashi et al. 1996]). These kinds of reasoning have previously been possible only by looking at the code in detail. We also show (informally) that typical concurrent objects are also implemented by using reliable channels.

In addition, it would be worth mentioning that there exists a polynomial time type check algorithm which, given [Gamma] = [x.sub.1]: [T.sub.1],..., [x.sub.n]: [T.sub.n] and P, decides whether or not there exists ?? such that [Gamma], ?? P (this implies that a programmer need not annotate a program with ordering information).

1.4 Other Applications

In addition to the static detection of deadlock, there are several interesting potential applications outside the scope of this article. Because the ordering ?? in a judgment [x.sub.1]: [T.sub.1],..., [x.sub.n]: [T.sub.n], ?? P expresses the order in which P uses channels for communicating with external processes, our type system gives a better specification of processes than do previous type systems, which typically only specify which type of values are transmitted via each channel. Therefore, our type system would be useful for improving module systems of concurrent programming languages although a lot of work is still left to be done for this purpose (for example, we need to make it much easier for programmers to write and read types). It would also be useful for efficient implementation of concurrency primitives: for example, we expect it can be used for eliminating run-time check of the channel status. The latter issue is discussed in Section 9 in more detail.

1.5 Advantages of Our Approach

1.5.1 Why Not Just Introduce High-Level Primitives? An alternative, more obvious approach to avoiding the problems of deadlock and nondeterminism would be to provide higher-level constructs as primitives, so that programmers can be assured that a program is deadlock-free and/or deterministic as long as those constructs are used. However, we think that it is hard to provide a set of high-level constructs that is satisfactory for any application programs in any parallel/distributed environments; even if it is possible, the set of primitives would become quite large: as a result, other analyses and implementation would become very complicated, and addition or modification of high-level constructs would be difficult. Consider concurrent objects, for example: we need various kinds of concurrent objects--from simple ones to complex ones supporting transactions, intraobject concurrency, etc. In parallel/distributed environments, many primitives (for parallel evaluation, transmission of data, etc.) seem necessary even for functional programs, unless one expects that it is possible to realize automatic, optimal parallelization and data distribution.

In contrast, although we are not opposed to adding some basic constructs for functions and concurrent objects as primitives, our approach in this article is to let programmers define high-level constructs as derived forms, and still to provide a way for reasoning about the behavior of those constructs in terms of a static type system. Such an approach has been exploited in other recent work that tries to design and implement a concurrent programming language based on solid theoretical foundations of process calculi [Igarashi and Kobayashi 1997; Kobayashi 1996a; Kobayashi and Yonezawa 1995; Oyama et al. 1997; Pierce and Sangiorgi 1997; Pierce and Turner 1997; Turner 1996]. Advantages of the approach should be clear: other analyses and implementation are simplified, and programmers can safely define and use application-specific high-level constructs. From encodings of various evaluation strategies for the [Lambda]-calculus and concurrent objects given later, we think that our type system works well at least for a class of concurrent programs in which concurrency primitives are used mainly for controlling parallelism and data distribution, and also for simple reactive programs. More studies will be necessary before we can conclude that our approach is reasonable also for complex reactive programs.

1.5.2 Why Type Systems? Our type system presented here may look rather complex. So one might wonder if the same thing can be clone more easily by using other methods, such as abstract interpretation. However, using a type system seems preferable in many points. First, designing a suitable abstract domain is not easier than designing our type system: for the purpose of analyzing deadlock, one cannot simply map multiple communication channels to the same abstract channel, as discussed in Section 8. So, an abstract process would be more or less what we represent by a type environment and what abstract interpretation does would be similar to what we do in type checking. Second, type systems seem more suitable for compositional reasoning: the reason is that types can express the assumption about the behavior of the environment as well as the behavior of a process itself, so that two processes can be composed as long as they satisfy each other's assumption about the environment. Third, with type systems, correctness and complexity of the analysis can be discussed in a systematic and standard manner: in our type system, for example, correctness can be ensured by the subject reduction property and properties that immediately follow from typing rules. Furthermore, a type system provides more than a means for automatic analysis; it can also allow a programmer to specify the intended behavior of a program.

1.6 Structure of the Article

The rest of this article is structured as follows. Section 2 explains basic notations. Section 3 gives our type system and Section 4 shows that a well-typed process satisfies a partial deadlock-freedom property. Section 5 informally presents a polynomial-time type check algorithm for our type system. In order to show the expressive power of our type system and demonstrate how type information can be used for reasoning about program behavior, Section 6 shows encodings of functions and concurrent objects into the deadlock-free fragment of our process calculus. Section 7 discusses other remaining issues and Section 8 discusses related work. Section 9 concludes this article.

2. NOTATIONAL PRELIMINARIES

This section introduces the syntax of types, expressions, and type judgments. If types are ignored, our process calculus can be considered a subset of the polyadic [Pi]-calculus [Milner 1993]. We dropped synchronous outputs, summations (choices), and matchings from the [Pi]-calculus, and we restricted replications to be only performed to input prefixes. In the course of introducing the notations, we also sharpen the intuitions given in Section 1.

2.1 Types

For simplicity in this article, we consider channel types and base types as primary type constructors, [p.sup.m][[[T.sub.1],..., [T.sub.n]].sup.t] (abbreviated to [p.sup.m][[T].sup.t]) represents the type of channels which carry a sequence of values of types [T.sub.1],..., [T.sub.n]. Extra annotations p, called a polarity, p, called a multiplicity or mode, and t, called a time tag, are explained as follows.

2.1.1 Multiplicities. A multiplicity m ranges over {1, *, M, w:}. It represents how channels can be used:

--If m = 1, types are called linear channel types and channels linear channels [Kobayashi et al. 1996]. A linear channel can be used just once for communication. More precisely, it can be used once for an output (send) operation and once for an input (receive) operation.

--If m = *, types are called replicated input channel types and channels replicated input channels or simply replicated channels. A replicated input channel x can be used just once in a replicated input prefix (x?* [y]. ), and an arbitrary number of times in output expressions (x![y]), but cannot be used in any input (vx)(x?*[y]. P|Q), which creates a replicated input channel x and executes two processes x?* [y]. P and Q. Here x cannot be used for any input operations in P or Q. So it can be considered a process that executes Q under the process definition x![y] = P.

--If m = M, types are called mutex channel types and channels mutex channels. A single message must be put into a mutex channel after its creation. Afterward, the channel can be used an arbitrary number of times for input, as long as a process that has extracted a value from it eventually puts a value into it. A mutex channel can, therefore, be considered a binary semaphore.

--If m = w, types are called unreliable channel types and channels unreliable channels. We have no particular restriction on the use of unreliable channels, except that they cannot be used in replicated input prefixes.

A channel is also called reliable if it is a linear, replicated input, or mutex channel. The reason why we call them "reliable" is that, with our type system, input/output operations on linear channels, output operations on replicated input channels, and input operations on mutex channels can eventually proceed, unless the whole program falls into an infinite loop or a deadlock caused by bad use of unreliable channels.

2.1.2 Polarities. A polarity p, which ranges over subsets of the set {I, O} of input/output capabilities, controls whether a channel is used for input or output. We write ?? for {I, O}, ? for {I}, ! for {O}, and I for the empty set [diameter]. For example, a type binding [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] means that x can be used both for input and output an arbitrary number of times, and x: [?.sup.1] [[int].sup.t] means that x can be used just once for input. The polarity of a mutex channel type [p.sup.M] [[T].sup.t] has a slightly special meaning: If p = ?, a channel can be used for receiving a value of type T, and after that, the process has the obligation to send some value back to the channel.

The above usage of channels would be better understood if we consider that types represent both capabilities and obligations. For example, if a process holds a linear channel of type [?.sup.1] [y], then it has the capability to receive a value once from the channel, and at the same time, the obligation to do so. If a process holds a mutex channel of type [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII], then it has the capability to send/receive a value along the channel (the send operation is allowed only once), but it only has an obligation to send a value: it need not receive a value from the channel. Similarly, if a process holds a replicated input channel of type [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII], it has the capability to send/receive a value along the channel, but the obligation is just to (be ready to) receive a value (via replicated input prefix). In the case of an unreliable channel, a process has capabilities but no obligation.

2.1.3 Time Tags. A time tag s(, t, u,...) intuitively describes when channels should be used. As indicated in Section 1, we will later associate time tags with a binary relation ??. [T.sub.1] ?? [t.sup.2] means "a process may be blocked on the channel tagged with [T.sub.1] before it fulfills an obligation to communicate over the channel tagged with [t.sup.2]." So if a process has a channel x of type [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] and y of type [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] such that [T.sub.1] ?? [t.sup.2], the process can behave like x?[m]. y?[n].0 but cannot behave like y?[n].x?[m].0. As another example, suppose [t.sub.x] is the time tag of a mutex channel x and [t.sub.y] is the time tag of another channel y, then

--If y is a linear channel, [t.sub.x] ?? [t.sub.y] implies that a process may try to acquire a lock x (i.e., wait for a value on x) before communicating over y. For example, the process x?[]. (y][] |x![]) is allowed only if there is an ordering [t.sub.x] ?? [t.sub.y].

--[t.sub.y] ?? [t.sub.x] implies that a process may try to communicate over y before releasing a lock x (i.e., sending a value along x). For example, if y is also a mutex channel, a process can behave like x?[]. y?[]. (x![] |y![]) only if [t.sub.y] ?? [t.sub.x] holds, since the process tries to communicate over the channel y before fulfilling the obligation to send a value to the channel x. Note that, in this case, the ordering [t.sub.x] ?? [t.sub.y] is unnecessary because receiving a value from the mutex channel y is not an obligation.

Since we cannot keep an arbitrary ordering on an infinite set of time tags, many actual channels may be mapped to the same tag in our type system. For example, consider the type [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] and [s.sub.z] correspond to any channels sent along a channel of that type.

The set of time tags, written T*, includes a special tag *. T denotes T*\{*}. We always annotate replicated input channel types and unreliable channel types with the special tag *, in order to ignore when channels of those types are used.

We could keep orderings on the use of replicated input channels in the same manner as we do on the use of linear and mutex channels. We, however, do not take that approach in this article because it would damage the expressive power of the deadlock-free fragment of the calculus.(1) Instead, we take a more trivial approach to deadlock-freedom: we ensure (by typing rules and the definition of [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] given later) that the obligation on a replicated input channel must be fulfilled immediately after its creation; in other words, a replicated input channel must be used for input (in a replicated input prefix) immediately after its creation.

In order to simplify later arguments, we assume that the set T can be divided into two disjoint sets [T.sub.O] and [T.sub.I]: we will use an element of[T.sub.O]for the outermost time tag of a type and use an element of [T.sub.I] for the other time tags.

2.1.4 Types. Now we are ready to formally define types. We use the word bare type for a type whose outermost time tag is dropped.

Definition 2.1.4.1. The sets of bare types and types are given by the following syntax, with the additional well-formedness conditions described below:

[Rho] (bare types) ::= b (base types) | [p.sup.m][T]

T, U (types) ::= [[Rho].sup.t]

Here [p.sup.m][T] abbreviates [p.sup.m][[T.sub.1],...,[T.sub.n]]. The additional conditions are given as follows:

(1) t in [Rho].sup.t] is * if and only if [Rho] is a base type b, an unreliable channel-type [p.sup.w] [T], or a replicated input channel type p* [T].

(2) If a type contains a bare type of the form: [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII], then for each i [element of] {1,..., n}, one of the following conditions holds:

--[[Rho].sup.i] is a base type, an unreliable channel type, or a replicated input channel type;

--[[Rho].sup.i] = [q.sup.M] [T] and O [not an element of] q; or

--[[Rho].sup.i] = [q.sup.1] [f], and q is neither ! nor ?. (i.e., output-only/input-only linear channels and output ends of mutex channels cannot be transmitted along mutex channels).

We assume that the set of base types contains "bool."

The second additional condition means that a channel containing some obligation cannot be put into a mutex channel. The reason for this is that there is no guarantee by our type system that the value in a mutex channel will eventually be extracted: since a mutex channel is used as a reference cell extended with a mutual exclusion mechanism, we want to ensure that a receiver is not blocked forever, but we do allow a sender to be blocked forever. For example, let x be a mutex channel to send/receive the output end of a linear channel, and let y be a linear channel; if we removed the restriction, x![y]|y?[]. 0 would be well typed, but are in deadlock (if there is no receiver on x in parallel to this process).

Notation 2.1.4.2. When the time tag is not important (especially when it is *), we sometimes just write [Rho] for [Rho].sup.t].We also often write/[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] for [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII].

Terminology and operations on types are introduced below. Because we must be very sensitive to how often each channel is used, it is convenient to classify types into unlimited types and nonunlimited types, according to whether or not a value of the type can appear in an unlimited number of places. Whether or not a type is unlimited depends on its polarity and multiplicity: for example, the output end of a replicated input channel can be used an arbitrary number of times, but the input end cannot.

Definition 2.1.4.3. A type T is unlimited if (1) T is a base type or an unreliable channel type, (2) T = p*[T]* and I [not an element of] p, (3) T = [p.sup.M][[T].sup.t] and O [is not an element of] p, or (4) T = |[sup.1] [[T].sup.t]

Consider a process P|Q. If P uses x as a channel of type [!.sup.1] [int] (i.e., P uses x just once for output) and Q uses x as a channel of type [?.sup.1][int], then x is totally used once for output and once for input in P|Q, thus x should have a type [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] [int] in P|Q. The operator + defined below captures this: the type of a variable in a process is calculated by combining the types of the variable in its subprocesses with +. In the example above, [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] can be defined as [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII].

Definition 2.1.4.4. The combination of two bare types [Rho].sub.1] and [Rho].sub.2], written [Rho].sub.1] + [Rho].sub.2] , is defined by

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] is an unlimited type.

For the other cases, [Rho].sub.1] + [Rho].sub.2] is undefined. The combination of two types, written [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII], is defined as ([MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] only if [Rho].sub.1] + [Rho].sub.2] is well defined and [T.sub.1] = [t.sup.2].

Definition 2.1.4.5. Let T be a type. The type Rem(T) is defined by

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

2.2 Process Expressions

Here we add some annotations and conditional expressions to the syntax used in Section 1. The process 0 in Section 1 will be defined as a derived form below.

Definition 2.2.1. The set of process expressions is given by the following syntax:

P ::= [ P.sub.1] |[ P.sub.2] (concurrent composition)

x![y] (output expressions)

x?[z].P (input expressions)

x?*[z].P (replicated input expressions)

(vx : T) P (channel creation) if x then [ P.sub.1] else [P.sub.2](conditional expression)

where y abbreviates a sequence [y.sub.1], [y.sub.n] (n may be 0). In an expression (vx : [[Rho].sup.s]) P, s must be an element of [T.sub.O] [union] {*}, and all the time tags in [Rho] must b elements of [T.sub.I] [union] {*}.

As usual, we assume that z are bound by prefixes x?[z] and x?*[z] and that x is bound by (vx: T). We identify expressions up to the renaming of bound variables (i.e., [Alpha]-conversion): for example, we do not distinguish between (vx: T)x![] and (vy: T)y![]. We give prefixes (x?[y],x?*[y],(vx: T)) a higher precedence than concurrent composition (|), so that x?[]. (vy: T)x![]|y![] means (x?[].((vy: T) x![]))|y![]. We often write (vx:T) P for ([vx.sub.1]: [T.sub.1]) ...([vx.sub.n]: [T.sub.n]) P (n may be 0), and 0 for [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] where t is a fresh time tag.

We write New(P) for the set of time tags t of y-prefixes (vx : [[Rho].sup.t]) in P. It is formally defined by

New([P.sub.1]|[P.sub.2] ) = New([ P.sub.1]) [union] New ([ P.sub.2])

New(x![y]) = [diameter]

New(x?[y].P) = New(P)

New(xt*[y].P) = New(P)

New((vx : ps) p) = ({s}\{*}) [union] New(P)

New(if b then Pi else [ P.sub.2]) = New([ P.sub.1] ) U New([ P.sub.2]).

Examples

In order to help understand the syntax, we give examples below of process expressions and show how they are reduced. A formal definition of the operational semantics, which is based on the standard reduction relation [Milner 1993], is deferred until Section 4.

Example 2.2.2. The process x![[y.sub.1], [y.sub.2]][x?[\[z.sub.1], [z.sub.2]].[z.sub.1]![[z.sub.2]]|[y]? [w].w![] can be reduced to [y.sub.2]![[y.sub.2]] [yz?[w].w![] by communication on x. Then it is reduced to [y.sub.2]![] by communication on [y.sub.1].

Example 2.2.3. The process x![[y.sub.1],[y.sub.2]] [x?*[[z.sub.1],[z.sub.2]].[z.sub.1]![[z.sub.2]] can be reduced to the process [y.sub.1]![[y.sub.2]]]x?*[[z.sub.1], [z.sub.2]].[z.sub.1]![[z.sub.2]].

Example 2.2.4. The process

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

can be viewed as a definition of the factorial function. (For simplicity, we assume that we have x, = on integers as primitives in this example,) It receives an integer n and a linear channel r along the replicated input channel fact, and sends the factorial of n to r. For example, P | fact![2, y] is reduced as follows:

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

Example 2.2.5. The following process, which represents a counter object, shows typical use of a mutex channel.

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

The mutex channel st is used for keeping the internal state of the object, so the process st![1] expresses that the current counter value is 1. The processes inc?*[r].... and read?* [r].... can be viewed as definitions of methods for incrementing and reading the current value respectively: if a message inc![r] arrives, the process inc?* [r].... receives it, extracts the current value from the mutex channel st, sends a null tuple to the reply channel r, and puts the incremented value into st. The assumption of st being a mutex channel avoids easy mistakes such as forgetting to write back a new state and duplicating a state.

2.3 Type Judgment Form

We introduce type environments, several operations on them, and the form of type judgments.

2.3.1 Type Environments. A type environment is a mapping from a finite set of variables to types. If true (false, resp.) is in the domain of a type environment ??, then ?? (true) (??(false), resp.) must be bool. We also assume that if ??(x) = [Rho].sup.s], then s is an element of To U (*} and all the time tags in p are elements of [T.sub.I] [union] (*}.

Notation 2.3.1.1. We often use metavariables ??, [Delta] for type environments. The domain of ?? is denoted by dom(??). We write x1: [T.sub.1],..., xn: [T.sub.n] (or x : T in an abbreviated form) for the type environment ?? such that dom(??) = {x1,...,xn), ??([x.sub.i]) = [T.sub.I] for each i [element of] {1,...,n}. When dom(??) [intersection] {x} = [diameter], we write ??, x : T for the type environment [Delta] such that dom([Delta]) = dom(??) [union] {x}, [Delta] (x) = ?? and [Delta](y) = ?? (y) for y ?? dom(??). We also write [diameter] for the type environment whose domain is empty.

We say ?? is unlimited if ??(x) is unlimited for each x [element of] dom(F). The operation + is extended to type environments as follows:

Definition 2.3.1.2. Let [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] and [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] be type environments. We define [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] + [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] by

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

Trivially, + is associative and commutative. We sometimes write [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] for [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII].

Example 2.3.1.3. [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

Example 2.3.1.4. [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

2.3.2 Tag Ordering. A tag ordering [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] T x T is a binary relation on time tags such that its transitive closure, written [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII], is a strict partial order (i.e., a relation R that satisfies transitivity and irreflexivity: [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]. Note that we do not require ?? itself to be a strict partial order.(2) We often regard a tag ordering ?? (?? T x T) as the binary relation T* on the set T* defined by: [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII].

Let ?? be a tag ordering. We extend ?? to a relation between time tags and type environments. Intuitively, t ?? [Gamma] means that a process may be blocked on the channel tagged with t before fulfilling the obligations specified by [Gamma]. Therefore, t ?? x: T always holds if T represents no obligation. In particular, t ?? x: T always holds if T is an unlimited type since it cannot represent any obligation (because a Value of the unlimited type may not be used at all).

Definition 2.3.2.1. Let t be a time tag, [Gamma] be a type environment, and ?? be a tag ordering. We define t ?? [Gamma] by

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII].

Careful readers may think that we should have required t ?? s for [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] to hold. We do not require it, however, because deadlock-freedom is not affected by a process being blocked on a channel specified by t before performing both send and receive operations on a linear channel. This can be understood by considering that [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] currently represents no obligation and that the obligation to receive (send, resp.) a value along a channel of type [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] arises only when the capability to send (receive, resp.) a value is used. Note also that, if a type T contains the obligation to receive a value from a replicated input channel, t ?? x: T never holds regardless of the relation ??. This means that a process must never try to communicate over other channels before using the input end of a replicated input channel. We introduce several notations on tag orderings.

Definition 2.3.2.2. Let ?? [subset or equal to] T x T and [S.sub.1], [S.sub.2] [subset or equal to] T*. We define [S.sub.1] ?? [S.sub.2] by

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII].

When ?? is subscripted with i,j, k,..., we write ??, etc.

Definition 2.3.2.3. Let R ([subset or equal to] T x T) be a relation on time tags and S([subset or equal to] T,) be a set of time tags. We define R [arrow down]S, R [arrow up]S, R??S, by

R [arrow down] S = R [intersection] (T\S x T\S)(= R\((S x T) [union](T x S)))

R [arrow up] = R [intersection]((S x T) [union] (T x S))

R ?? S = R [arrow down] S] U{(s,t) | s, t [is not equal to] s and [sRu.sub.1]R... [Ru.sub.n][R.sub.t] for some [u.sub.1],..., [u.sub.n] [element of] S\{*}(n [is greater than or equal to] 0)}.

Definition 2.3.2.4. Let ?? [subset or equal to] T x T be a relation on time tags, and let [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] be a renaming on time tags. We define the relation [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] by

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII].

Definition 2.3.2.5. Let ?? be a tag ordering. We define [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] as the least relation ?? such that ?? [subset or equal to] ?? and [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII].

2.3.3 Type Judgment Form. A type judgment is of the form [Gamma], ?? P, where F is a type environment and ?? is a tag ordering. We require that each element of To has at most one occurrence in a type judgment. Therefore, [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] is a type judgment only if [t.sub.1],..., [t.sub.n] and the elements of New(P) are distinct from each other. (Note that this is analogous to the usual assumption that all the bound variables in P and the variables in [Gamma] are distinct from each other.)

Intuitively, [Gamma], ?? P means that (1) the process P uses only the capabilities specified by [Gamma], (2) P fulfills all the obligations specified by [Gamma], and (3) P obeys the ordering specified by -4 in fulfilling the obligations. An ordering ?? specifies an upper-bound of the ordering of channel use in P, rather than the exact ordering. For example, if [[Rho].sub.x], [[Rho].sub.y] are linear channel types and [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] P holds, then communication on y may (not must) be blocked by communication on x (by x?[n]. y![n], for instance) in P: P may use x and y concurrently as x?[n]. 0 y|![n] does. Note also that there may be an ordering between different type bindings. For example, [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] implies that P cannot wait for a value on a channel received via x before it sends an integer along y.

3. TYPING RULES

We give typing rules below and mainly explain the conditions on tag orderings. The conditions on type environments are basically the same as those for the linear channel type system and are explained there in detail [Kobayashi et al. 1996].

(T-PAR) is one of the key rules. The rule should be read "if [P.sub.1], [P.sub.2] are respectively well typed under [[Gamma].sub.1], [[Gamma].sub.2] and a tag ordering ??, and if [[Gamma].sub.1] + [[Gamma].sub.2] is well defined, then [P.sub.1] | [P.sub.2] is well typed under [[Gamma].sub.1] + [[Gamma].sub.2] and ??." Note that the ordering ?? must be shared between [P.sub.1] and [P.sub.2]: it ensures that there is no conflict on the order of channel use between [P.sub.1] and [P.sub.2]. For example, consider [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]. [P.sub.1] and [P.sub.2] are respectively well typed under type environments [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] and [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] and [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] is well defined. However, [P.sub.1] | [P.sub.2] is not well typed under [[Gamma].sub.1] + [[Gamma].sub.2] because [P.sub.1] and [P.sub.2] cannot be typed under the same ordering ??: while [P.sub.1] requires [t.sub.x] ?? [t.sub.y], [P.sub.2]. requires the reverse ordering [t.sub.y] ?? [t.sub.x].

(T-PAR) [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

If y is sent on x by the expression x![y], the components of y can be used only after they are extracted from x. So, the type environment must allow the fulfillment of the obligations specified by [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] to be delayed until the communication on x is completed. It is ensured by the condition [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] in the rule (T-OUT). The condition (|t/u| ?? [subset or equal to] ?? means that if there is an ordering on u, in ??, then there must also be the corresponding ordering on t, so that a receiver can safely use y in an order specified by the ordering on u.

(T-OUT) [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

In the rule for input expressions below, the condition [u/s] ?? [subset or equal to] ensures that the components of z must not be used in P in an order unspecified by the ordering on u. Since the body of an input expression can be executed only after communication on x is completed, we need the condition t ?? [Gamma] to allow the fulfillment of the obligations specified by [Gamma] to be delayed. The ordering on s can be deleted, because all the dependencies on the use of the bound variables z are already taken into account by the ordering on u. An additional condition {s} ?? {u} is necessary for a subtle technical reason.

(T-IN) [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

The rule (T-MIN) for input prefixes on mutex channels is identical to (T-IN), except for the condition O [an element of] p, which ensures that a value is put into x in the body of the input expression:

(T-MIN) [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

The rule (T-RIN) for replicated input expressions is also similar to (T-IN). The type environment F below must be unlimited because the body of a replicated input expression may be executed more than once. (The condition u ?? [Gamma] is not required here because it is implied by the condition that [Gamma] is unlimited.)

(T-RIN) [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

We have two rules for v-expressions. The condition {s} ?? [T.sub.I] in the rule (T-NEW-1) means intuitively that there is only local dependency on the use of the created channel. If this is the case, the ordering on s can be removed from the type judgment. Otherwise, (T-NEW-2) must be applied and the ordering on s must be preserved.

(T-NEW-1) [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

(T-NEW-2) [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

In a conditional expression, both a type environment and a tag ordering are shared between the then-part and the else-part.

(T-IF) [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

Examples

We give several examples of valid/invalid type judgments below. We write P [right arrow] Q when P is reduced to Q in one step, and P ?? Q when P is reduced to Q in zero or more steps. They are the same as the standard reduction relation for the [Pi]-calculus [Milner 1993], and formal definitions are given in Section 4. The time tags for int and bool (which are always ,) are omitted in the rest of this article.

Example 3.1. Let ?? = {([t.sub.1], [t.sub.2])). Then,

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

but

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

Example 3.2. Let us consider a process P = x?[y, z]. y?[n], z![n]|x![v, w], and let ?? = (([t.sub.x], [t.sub.v]),([t.sub.v], [t.sub.w]),([t.sub.x], [t.sub.w]),([u.sub.y],[u.sub.z])}. Then, we have

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

for ?? = {([s.sub.y], [s.sub.z])} [union] ??. By (T-IN), we obtain

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII].

On the other hand, x![v, w] is typed as

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII].

Thus, we obtain

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII].

The condition [t.sub.x] ?? [t.sub.v] ?? [t.sub.w] implies that x is first used for communication, v is used next, and then w is used. Note that ?? can be inferred from the given type environment and process: the subexpression x?[y, z]. y?[n], z![n] requires [u.sub.y] ?? [u.sub.z], and the subexpression x![v, w] requires [t.sub.x] ?? [t.sub.v], [t.sub.w] and [[t.sub.v]/[u.sub.y], [t.sub.w]/[u.sub.z]] ?? [subset or equal to] ??, by which we obtain [t.sub.x] ?? [t.sub.v] ?? [t.sub.w]. Such reconstruction of a tag ordering is discussed later in Section 5.

Example 3.3. Let [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]. Then, [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII].

Example 3.4. Let [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]. Then, [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII].

Example 3.5. Let us consider the following process, which corresponds to a recursive function definition.

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII].

By applying (T-NEW-l) to

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII],

we obtain

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII].

By (T-IF) and (T-RIN), we further obtain [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII].

The following two examples indicate that the side condition {s} ?? [T.sub.I] in (T-NEW-I) cannot be dropped.

Example 3.6. Let P be the following process:

z![]|w?*[x,y].(>?[].x?[].(x![]|z![])|y?[].z?[].(y![]|z![]))

Then,

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII].

If we could ignore the side condition of (T-NEW-I), we would have

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII],

from which we could obtain

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII].

However, it may deadlock as follows:

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

Example 3.7. Let

P = m?[y].y?[].x![]|n![x]

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

?? = {([u.sub.y], [t.sub.x]), ([t.sub.m], [t.sub.x]), ([t.sub.n], [t.sub.x)}.

Then, [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]. We can apply (T-NEW-2) to obtain [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII], but we cannot apply (T-NEW-i) to obtain [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]. Note that if we ignored the side condition of (T-NEW-1), we would have

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII].

But [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] falls into deadlock:

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII].

Technical Properties

We state several key lemmas that will be used for proving type soundness: Lemmas 3.8-3.12 are used for strengthening and weakening the typing assumption (the left-hand side) of a type judgment. Lemma 3.13 corresponds to the substitution lemma in the usual type systems. Readers who are not interested in proofs can safely skip the rest of this section.

LEMMA 3.8. If [Gamma], x: T, ?? P and x is not free in P, then T is unlimited and [Gamma], ?? P.

PROOF. By the typing rules, x:T must be introduced in (T-OUT). Therefore, T must be unlimited and we can obtain [Gamma], ?? P from a derivation of [Gamma], x: T, ?? P by dropping all the bindings on x. []

LEMMA 3.9. Let [Gamma] be a type environment and T be an unlimited type such that [Gamma] + x :T, ?? P is well formed. Then [Gamma], ?? P implies [Gamma] + x: T, ?? P.

PROOF. This is proved by straightforward induction on typing derivations. (A derivation of [Gamma] + x :T, ?? P can be obtained from that of [Gamma], ?? P by replacing each type environment [Gamma]' in the derivation with [Gamma]' + x:T.) []

LEMMA 3.10. Suppose [Gamma], ?? P and s [an element of] [T.sub.O] does not appear in [Gamma], P. Then, [Gamma], [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII].

PROOF. If s has been removed somewhere in the derivation of [Gamma], ?? P, then ?? cannot contain s, i.e., [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]. So [Gamma], [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] follows immediately. Otherwise, a derivation of [Gamma], [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] is obtained from that of [Gamma] ?? P just by replacing each ordering [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] in the derivation of [Gamma], ?? P with [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]. []

LEMMA 3.11. Suppose [Gamma], ?? P. Then [Gamma], ?? [union] ?? P holds if ??' satisfies the following conditions:

--[(?? [union] ??').sup.+] is a strict partial order and

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII],

where S is the set of time tags excluded from the tag ordering by (T-NEW-1) in the derivation of [Gamma], ?? P.

PROOF. The derivation of [Gamma], ?? [union]?? P is obtained from that of [Gamma], ?? P just by replacing each ordering ?? in the derivation of [Gamma], ?? P with ?? [union] ??'. []

LEMMA 3.12. Suppose [Gamma], ?? P, and t is a fresh time tag taken from [T.sub.O]; then [Gamma], ?? [union] [t/s] ?? P.

PROOF. It is trivial that [(?? [union][t/s] ??).sup.+] is a strict partial order. The derivation of [Gamma], [union] [t/s] ?? P can be obtained from that of [Gamma], ?? P just by replacing each ordering ?? in the derivation of [Gamma], ?? P with ?? [union] [t/s] ??. []

LEMMA 3.13. The rule

(T-REN) [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

is admissible, i.e., if

--[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

--[([[t.sub.y]/[t.sub.x] ??).sup.+] is a strict partial order, and

--the judgment [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] is well formed,

then [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] is derivable.

PROOF. See Appendix A.1. []

4. TYPE SOUNDNESS AND PARTIAL DEADLOCK-FREEDOM

In this section, we present an operational semantics and show that typing is respected by the operational semantics: in particular, we check that reliable channels (i.e., linear, replicated input, or mutex) never cause deadlock in a well-typed process.

4.1 Reduction Semantics

As usual, the operational semantics is defined via two relations: a structural congruence and a reduction relation [Milner 1993].

The following structural congruence simplifies the definition of the reduction relation.

Definition 4.1.1. Structural congruence [equivalent] is the least congruence closed under the following rules.

P |Q [equivalent] Q|P (S-COMMUT) (P|Q)|R [equivalent] P|(Q|R) (S-ASSOC) (vx: T) P|Q [equivalent] (vx: T) (P|Q) x not free in Q (S-EXTR)

Note that structurally congruent processes have the same typing property:

LEMMA 4.1.2. If P = Q, then [Gamma], ?? [assertion] P if and only if [Gamma], ?? [assertion] Q.

PROOF. See Appendix A.2. []

To simplify the arguments below, we introduce the notion of normal forms.

Definition 4.1.3. A process (vx:T) ([P.sub.1]|... |[P.sub.n]) is in normal form if [P.sub.1] ,...,[P.sub.n] are guarded processes, where a process is guarded if it is an input, output, replicated input, or a conditional expression.

LEMMA 4.1.4. for any process P, there is some Q in normal form such that P [equivalent] Q.

PROOF. By the associativity and commutativity of |, and the fact that any (vx:T) not guarded by input or replicated prefixes can be moved to the outside using (S-EXTR). []

The reduction relation is basically the same as the standard one [Milner 1993; Sangiorgi 1992], but it is annotated with some extra information [Kobayashi et al. 1996] that is used later for stating properties of the semantics. The reduction relation is of the form [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]. ([MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII], is a five-place relation as a whole. It says nothing about typing of P and P' and therefore, it should not be confused with ([MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII].) Intuitively, the type environment f represents the capabilities that can be used before the reduction, while [Gamma]' represents those that can be used after the reduction. The multiplicity m records on which kind of channel the reduction is performed, rename(P) in the rule (R-RCOM) represents a process expression obtained from P by renaming all the time tags in New(P) with fresh time tags. Note that for well-typed processes, the reduction relation defined below coincides with the standard reduction relation for untyped process calculi.

(R-COM) [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

(R-RCOM) [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

(R-PAR) [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

(R-NEW) [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

(R-IFT) [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

(R-IFF) [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

(R-CONG) [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

Notation 4.1.5. When the label m is not important, we just write [Gamma] [assertion] P [right arrow] Q ?? [Delta] For [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]. We write [Gamma] [assertion] P [right arrow] Q if [Gamma] [assertion] P [right arrow] Q ?? [Delta] for some [Delta] and write [GAMMA] [assertion] P ?? (or P ?? when [GAMMA] is known From the context) if there is no Q such that [GAMMA] [assertion] P [right arrow] Q.

Definition 4.1.6. [GAMMA] [assertion] P ?? Q ?? [Delta] is the least relation closed under the following rules.

[GAMMA][assertion]P ?? P ?? [GAMMA]

[GAMMA][assertion] P [right arrow] Q ?? [Delta] [Delta] [assertion]Q ?? R ?? [Theta] / [GAMMA][assertion] P ?? R ?? [Theta]

We just write P ?? Q if [Gamma] [assertion] P ?? Q ?? [Delta] for some [GAMMA] and [Delta]. for well-typed processes, P ?? Q coincides with the reflexive and transitive closure of the standard reduction relation [Milner 1993].

4.2 Partial Confluence

As claimed in Kobayashi et al. [1996], communication on a linear or replicated input channel enjoys the confluence property. It implies that communication on those channels essentially preserves the equivalence class of a process. We do not give any proof here since it is the same as that in Kobayashi et al. [1996].

THEOREM 4.3.1 (PARTIAL CONFLUENCE). Suppose that [GAMMA], ?? [assertion] P for some ?? and [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] for m = 1 or *. If [GAMMA] [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII], then P' [equivalent] Q or there is some Q', [Delta]' such that [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] and [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII].

4.3 Partial Deadlock-freedom

Deadlock-freedom is ensured by two theorems: (1) subject reduction theorem (Theorem 4.3.1), which states that typing is preserved by reductions, and (2) Theorem 4.3.2, which states that reliable channels do not cause deadlock immediately in a well-typed process.

The subject reduction theorem is stated below. The major difference from the ordinary subject reduction is that the reduced process expression is well typed not under the original type environment but under the new type environment obtained by removing the used capabilities from the original one. The tag ordering is changed by the reduction, but not in a significant way: the new tag ordering is obtained just by some renaming of the original ordering.

THEOREM 4.3.1. If [GAMMA], ?? [assertion] P and [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII], then [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] For s, s' such that

(1) {s'} = New(P')\New(P) and

(2) {s} [subset or equal to] New(p).

Note that [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] is always a tag ordering because s' are fresh time tags.

PROOF. Induction on the derivation of [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]. See Appendix A.3. []

The theorem below ensures that reliable channels (linear, replicated input, and mutex channels) cannot immediately cause deadlock. We use the shorthand {|Q) for either nothing or a parallel composition with the process Q. We say that x is half used in [GAMMA] if [GAMMA](x) is of the form [?.sup.m] [[T].sup.t] or [!.sup.m][[T].sup.t]. The theorem essentially says that if a well-typed process P can no longer be reduced, then either (1) some subprocess is trying to communicate over some unreliable or half used channel (in the first case below); or (2) all computation has been completed and only processes corresponding to process definitions (replicated input expressions) or stores (i.e., outputs on mutex channels) are left (in the second case below).

THEOREM 4.3.2. Suppose [GAMMA], ?? [assertion] P and {x | [GAMMA](x) = bool} [subset or equal to] {true, false}. If [GAMMA] [assertion] P ??, then one of the following conditions holds:

(1) Either P [equivalent] (vw:U)(x?[z]. Q{|R}) or P [equivalent] (vw:U)(x![z]{|R}); and x has an unreliable channel type (in [GAMMA] or w:U) or is half used in [GAMMA].

(2) P [equivalent] (vw:U) ([P.sub.1] | ... |[P.sub.n]) and each [P.sub.i] is either of the form x![y] for a mutex channel x or of the form x?* [y]. Q.

PROOF. Let (vw:U)([P.sub.1]|... |[P.sub.n]) be a normal form of P. By Lemma 4.1.2, [GAMMA], ?? [assertion] (vw:U)([P.sub.1]|... |[P.sub.n]). By (T-NEW-1), (T-NEW-2), and (T-PAR), there exist [[GAMMA].sub.1],... ,[[GAMMA].sub.n] and [??.sub.1] such that

[[GAMMA].sub.i], [??.sub.1] [assertion] [P.sub.i] (1 [is less than or equal to] I [is less than or equal to] n)

[[GAMMA].sub.1] + ... + [[GAMMA].sub.n] = [GAMMA], w:U.

None of [P.sub.i](i [is an element of] {1,..., n}) is a conditional expression, because otherwise it must be that [P.sub.i] = if true then [Q.sub.1] else [Q.sub.2] or [P.sub.i] = if false then [Q.sub.1] else [Q.sub.2],which contradicts with the assumption P ??. Suppose that the first condition of the above theorem does not hold, i.e., no process is trying to communicate over an unreliable or half-used channel. Then, without loss of generality, we can assume that

--[P.sub.i] = x![y] and ([GAMMA], w:U)(x) = ??*[T]* for some x for each i(1 [is less than or equal to] i [is less than or equal to] j),

--[P.sub.i] = x?[y]. Q and ([GAMMA], w:U)(x) = [??.sup.M] [[T].sup.t] for some x for each i(j + 1 [is less than or equal to] i [is less than or equal to] k),

--([GAMMA], w:U)(x) = [??.sup.1] [[T].sup.t] and either [P.sub.i] = x![y] or [P.sub.i] = x?[y]. Q for some x for each i(k+ 1 [is less than or equal to] i [is less than or equal to] l), and

--either [P.sub.i] = x![y] for some mutex channel x, or [P.sub.i] = x?*[y]. Q for some x, for each i(l + 1 [is less than or equal to] i [is less than or equal to] n)

where 0 [is less than or equal to] j [is less than or equal to] k [is less than or equal to] l [is less than or equal to] n. We show l = 0, which implies the second condition of the theorem.

First, suppose j [greater than] 0. Then, [P.sub.1] = x![y] and ([GAMMA], w:U)(x) = ??*[T]* for some x. By the typing rules, [[GAMMA].sub.i](x) = p*[T]* and I [is an element of] p for some i [is an element of] {2,...,n}. Again by the typing rules, [P.sub.i] must be of the form x?*[v]. Q, which contradicts with the assumption P ??. Therefore, j must be 0.

Let us define the set S by

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

Note that * [is not element of] S. We shall show S = ?? (i.e., l = 0) by contradiction, which completes the proof. Suppose that S [is not equal to] 0. Then because [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] is a strict partial order, there is [t.sub.i] [is an element of] S such that there is no t' [is an element of] S such that t' [??.sub.1] [t.sub.i]. The case analysis below shows that such [t.sub.i] does not exist. The key point is that some process [P.sub.i], must hold the other end of [x.sub.i], and since [t.sub.i] is a minimal element of S, the first prefix of [P.sub.i], must be on [x.sub.i], which implies [P.sub.i] and [P.sub.i], can be further reduced.

--Suppose that [t.sub.i] comes from the first set of S, i.e.,

[P.sub.i] = [x.sub.i]?[y].Q ?? [[Gamma].sub.i](x)=[p.sup.M][[T].sup.ti] ?? (1 [is less than or equal to] i [is less than or equal to] k).

By (T-IN), p must be ?. Since [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII], there is some i'([is not equal to] i) such that [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] and O [is an element of] q. Since [t.sub.i] is a minimal element of S, it must be that l + 1 [is less than or equal to] i' [is less than or equal to] n. So, [P.sub.i], must be either u?*[z].R or u![v]. The first case contradicts with the condition of (T-RIN) ([[GAMMA].sub.i], ([x.sub.i]) must be unlimited). In the second case, since the output end of a mutex channel cannot be put into a mutex channel (by the condition on type expressions), u must be [x.sub.i], which contradicts with the condition P ??.

--Suppose that [t.sub.i] comes from the second set of S, i.e.,

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

By (T-OUT), p must be !. Since ([GAMMA], w:U)([x.sub.i])= [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII], there is some i'([is not equal to] i) such that [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]. Because [t.sub.i] is a minimal element of S, it must be that k + 1 [is less than or equal to] i' [is less than or equal to] n. If k + 1 [is less than or equal to] i' [is less than or equal to] l, then [P.sub.i], must be of the form [x.sub.i]?[u]. [Q.sub.i'], which contradicts with the fact that P ??. If l + 1 [is less than or equal to] i' [is less than or equal to] n, then [P.sub.i'], is either an output on a mutex channel or a replicated input. The first case contradicts with the condition that the input end of a linear channel cannot be put into a mutex channel, and the second case contradicts with the condition of (T-RIN) ([[GAMMA].sub.i],([x.sub.i]) must be unlimited).

--Case where [t.sub.i] comes from the third set of S: Similar to the second case. []

The subject reduction property (Theorem 4.3.1) together with the lack of immediate deadlock (Theorem 4.3.2) ensures the following partial deadlock-freedom property.

THEOREM 4.3.3 (PARTIAL DEADLOCK-FREEDOM). Suppose that [GAMMA], ?? [assertion] P and {x | [GAMMA](x) = bool} [subset or equal to] {true, false}. If [GAMMA] [assertion] P ?? P' ?? [Gamma] and [Gamma] [assertion] P' ??, then one of the following conditions holds:

(1) either P' [equivalent] (vw:U)(x?[z].Q{|R}), or P' [equivalent] (vw:U)(x![z]{|R}); and x has an unreliable channel type (in [GAMMA] or w:U) or is half used in [GAMMA].

(2) P' [equivalent] (vw:U)([P.sub.1] |... |[P.sub.n]) and each [P.sub.i] is either of the form x![y] for a mutex channel x or of the form x?* [y]. Q.

PROOF. Corollary of Theorem 4.3.1 and Theorem 4.3.2. []

The following corollary is a special case of Theorem 4.3.3.

COROLLARY 4.3.4. Suppose that [GAMMA], ?? [assertion] P, {x | [GAMMA](x) = bool} [subset or equal to] {true, false}, and that all the channel types in [GAMMA], P are reliable channel types and that no channel in [GAMMA] is half used. If [GAMMA] [assertion] P ?? Q ?? [Delta], then, either

(1) Q [equivalent] (vw:U)([P.sub.1]| ... |[P.sub.n]) and each [P.sub.i] is either of the form x![y] for a mutex channel x or of the form x?* [y]. R or

(2) [Delta] [assertion] Q [right arrow] Q' ?? [Delta]' for some [Delta]', Q'.

PROOF. A special case of Theorem 4.3.3. []

By the above corollary, a program never falls into deadlock if only reliable channels are used. for the cases where unreliable channels are used, Theorem 4.3.2 says just that, in a deadlocking process, some sub-process is always trying to communicate over an unreliable or half-used channel. However, its proof also implies that if there is a process blocked on a reliable channel, then some process is trying to communicate over an unreliable or half-used channel while blocking communication on a reliable channel. Moreover, the proof indicates that we can identify such a bad process by looking at the tag ordering.

5. TYPE CHECK

In this section, we show that there is an algorithm, which, given a type environment [GAMMA] and an expression P, decides whether or not there exists a tag ordering ?? such that [GAMMA], ?? [assertion] P. It should be clear from the informal discussion below that the algorithm runs in time polynomial in the size of input: ([GAMMA], P).

The algorithm consists of the following steps:

(1) first, ignore conditions on ?? and construct a derivation tree of [GAMMA], ?? [assertion] P.

(2) Extract conditions on ?? and decide whether or not there exists a tag ordering ??.

The first step is done by reading the typing rules in a bottom-up manner. The nontrivial case is the one where we encounter (T-PAR)' we must split the current type environment for two subprocesses. The key technique to avoid combinatorial explosion is to split the type environment lazily. In order to type check [GAMMA], ?? [assertion] [P.sub.1] | [P.sub.2] (with conditions on ?? ignored), we first check [P.sub.1] (with information that its type environment should be a part of [GAMMA]). If the check succeeds, we can remove the used type environment [[GAMMA].sub.1] from [GAMMA], and check [P.sub.2] under the resulting environment [[GAMMA].sub.2]. The typing rules are reformulated in Appendix B in order to express this algorithm. The same idea is also used for proving a linear logic sequent "[GAMMA] [assertion] A [cross product] B" in linear logic programming languages [Hodas and Miller 1994] and for reconstructing types in linear functional programming languages [Mackie 1994].

Note that the first step can be done in a polynomial time (with respect to the size of [GAMMA], P): only one rule can be applied at each step of the construction of a derivation tree,(3) the size of the derivation tree is linear in the size of P, and the required computation (for deciding which rule should be applied and removing the used type environment at the node of (T-PAR)) at each node of the derivation tree is linear in the size of [GAMMA], P.

The second step is described as follows. first, introduce the set {[[Beta].sub.s,t] | s, t [is an element of] T} of variables ranging over {0, 1}. Then, ?? is completely determined by the values of the variables: we can define [[Beta].sub.s,t] = 1 if s ?? t, and [[Beta].sub.s,t] = 0 otherwise. All the conditions on ?? are expressed by constraints of the form

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

Constraints of the first form come from conditions of the form t [??.sup.#] [GAMMA], the second constraints from [Theta] ?? [subset or equal to] ??, and the third from [S.sub.1] ?? ?? [S.sub.2]. Then, the above constraints can be solved by the following simple iterations:

(1) first, let [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] if there is constraint [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII], and let [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] for other ([t.sub.1], [t.sub.2]). Let k [left arrow] 0.

(2) If there is a constraint [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII], and if [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII], then [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] 1. Otherwise [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] If [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] for some [t.sub.1], [t.sub.2], then let k [left arrow] k + 1 and repeat this step.

(3) for each constraint [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII], check whether [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

For the resulting relation ??, whether or not [??.sup.+] is a strict partial order can be checked by a well-known cycle detection algorithm for directed graphs.

The second step can be done in time polynomial in the size of an input ([GAMMA], P). Let n be the size of an input. Then the number of time tags appearing in the derivation is O(n). Because the number of variables is O([n.sup.2]), the number of steps of iterations is at most O([n.sup.2]). Because the number of constraints is at most O([n.sup.4]), the time required for each step is O([n.sup.4]). Therefore, the total time used for solving constraints is O([n.sup.6]). (This is a very rough estimate, and we could obtain a much better upper bound. For example, if we assume that the arity of a channel, i.e., the number of arguments passed through a channel, is bound by some constant, O([n.sup.4]) is an upper bound.)

There is one important thing that has not been mentioned above: how to choose (T-NEW-i) or (T-NEW-2) when extracting the constraints on time tags in the beginning of the second phase. Actually, the extraction and solving of the constraints must be overlapped. However, it does not affect the above estimation of the computational cost: in order to extract the constraints from a derivation for (vx: [[Rho].sup.s]) P, we can first gather the constraints from the sub-derivation for P, solve the constraints on s locally, and then choose (T-NEW-1) or (T-NEW-2) according to whether or not the side condition {s} ?? [T.sub.1] is met by the local solution.

6. FUNCTIONS AND CONCURRENT OBJECTS ON TOP OF THE CALCULUS

We show that functions and typical concurrent objects are implemented by using reliable channels, and demonstrate applications of the theorems on partial deadlock-freedom. We need only type information for inferring that a function or method will return a result unless it falls into an infinite loop. Note that such reasoning, unlike in typed functional languages, has not been possible in previous typed concurrent programming languages (including typed process calculi and typed concurrent object-oriented languages).

We first discuss encoding of the call-by-value, simply typed [Lambda]-calculus in detail. Then, we show that the call-by-name and call-by-need simply typed [Lambda]-calculi can also be encoded into the deadlock-free fragment. Encodings of concurrent objects are also informally presented and discussed.

6.1 Encoding Call-by-Value [Lambda]-Calculus

We show encoding of call-by-value, simply typed [Lambda]-calculus into our process calculus.(4) As will be clear from the encoding, we could obtain the same result in the presence of recursion.

6.1.1 Syntax and Typing of [[Lambda].sup.[right arrow]. We first introduce the syntax of the simply typed [Lambda]-calculus.

Definition 6.1.1.1. The sets of types and terms are given by the following syntax:

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

Definition 6.1.1.2. A term e has a type [Tau] under a type environment [Tau] if [Tau] ?? e : [Tau] can be derived by the following set of rules:

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

LEMMA 6.1.1.3. If [Tau] ?? e: [Tau] and [Tau] e: [Tau]', then [Tau] = [Tau]'.

PROOF. Trivial induction on the structure of e.

Notation 6.1.1.4. By Definition 6.1.1.2 and Lemma 6.1.1.3, if e is well typed under the type environment [Tau], there is a unique [Tau] such that [Tau] e: [Tau]. We write [Tau](e) = [Tau] if T ?? e : [Tau].

6.1.2 Encoding. We encode [[Lambda].sup.[right arrow]-terms into our calculus, following Milner [1990] and Pierce and Sangiorgi [1993]. We first give encoding of types and type environments. To understand the encoding of function types below, note that a function will be implemented as a process waiting on a replicated input channel for requests for evaluation, and that the invocation of the function will be implemented as a process that sends a request (consisting of an argument and a channel for receiving the result) on the replicated input channel (recall Example 2.2.4).

Definition 6.1.2.1. Types of [[Lambda].sup.[right arrow] are encoded by the following function [[.]]:

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

Here, we assume that the same tag u is used in all encodings of function types. The encoding function is pointwise extended to type environments:

[[0]] = 0

[[[Tau], x : [Tau]]] = [[[Tau]]], x : [[[Tau]]]

LEMMA 6.1.2.2. Let [Tau] be a type of [[Lambda].sup.[right arrow]. Then, [[[Tau]]] is an unlimited type.

PROOF. Trivial by the definition of [[[Tau]]].

Now we give an encoding of [[Lambda].sup.[right arrow]-terms. Given a [[Lambda].sup.[right arrow]-term e and its type environment [Tau], the encoding function [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] returns a process that evaluates e and returns the result to the channel a. We use a linear channel as the result channel a. A variable just returns its name to the return address.

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

The [Lambda]-abstraction [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] first spawns a process which, given an argument x and a return address q, sends the result back to q and then it returns the address of the spawned process.

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

Here [[Tau].sub.2] = ([Tau], x: [[Tau].sub.1](e).

A function application [e.sub.1][e.sub.2] first spawns processes to evaluate the function [e.sub.1] and the argument [e.sub.2], and then applies the function to the argument.(5)

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

Here [s.sub.1], [s.sub.2] are fresh time tags and [[Tau].sub.1] = [Tau]([e.sub.2]), [[Tau].sub.2] = [Tau]([e.sub.1] [e.sub.2]).

6.1.3 Reasoning about Encoded Terms. We show that a process [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] will eventually return a value to x or fall into an infinite loop.(6) All we need to check is that [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] is well typed: once it is checked, the required property is obtained as an immediate corollary of the theorems on partial deadlock-freedom.

THEOREM 6.1.3.1 (ENCODING PRESERVES TYPING). If [Tau] ?? e : [Tau], then we have [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] for a fresh time tag t.

PROOF. Proved by induction on the structure of e. []

--Case e = x: In this case, [Tau] = [Tau]', x : [Tau] and P = a![x]. Since [[[Tau]']] is unlimited, we have [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] by (T-OUT), i.e., [[[Tau]]],a : [!.sup.1] [[[[Tau]]]].sup.t], 0 ?? P.

--Case [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]. In this case, [Tau], x : [[Tau].sub.1] ?? e' : [[Tau].sub.2]. Let [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]. By induction hypothesis, we have

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

for a fresh time tag [s.sub.1]. By (T-RIN),

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

Because [[[Tau]]] is unlimited, we also have

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

By (T-PAR), (T-NEW-2), and the fact that [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII],

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

--Case e = [e.sub.1] [e.sub.2]: In this case, [Tau] ?? [e.sub.1] : [[Tau].sub.1] [right arrow] [[Tau].sub.2], [Tau] ?? [e.sub.2] : [[Tau].sub.1]. Let [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] and [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]. By induction hypothesis, we have

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

for fresh time tags [s.sub.1] and [s.sub.2]. By Lemma 3.11,

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

for ?? = {([s.sub.1], [s.sub.2]), ([s.sub.2],t), ([s.sub.1],t)}. On the other hand, by (T-IN) and (T-OUT),

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

By (T-PAR) and (T-NEW-1), [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII].

We obtain the theorem below as a corollary of Theorems 4.3.3 and 6.1.3.1. The theorem essentially says that the evaluation of an encoded term never gets stuck. Note that we also know by Theorem 4.2.1 that the returned result is unique up to some appropriate typed process congruence. (We do not give a formal definition of the process congruence, but a weak typed barbed congruence that is similar to the one developed for the linear channel type system [Kobayashi et al. 1996] will suffice.)

THEOREM 6.1.3.2. Let e be a closed [[Lambda].sup.[right arrow]-term (i.e., 0 ?? e : [Tau]). If [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] for some [Delta]. Then either

(1) P' [equivalent] (vw:U)(a![v]{|Q}) or (2) there is some Q such that [Delta] ?? P' [right arrow] Q.

PROOF. Let T = [!.sup.1] [[[[[Tau]]]].sup.t]. By Theorem 6.1.3.1, [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]. By the definition of the reduction relation, [Delta] = a: T. Suppose that [Delta] ?? P' ??. By the subject reduction theorem (Theorem 4.3.1), we have a: T, 0 ?? P'. Since every channel in P' is a linear or replicated input channel, we have either

(1) P' [equivalent] (vw:U)(a![v]{|Q}) or (2) P' [equivalent] (vw:U)([P.sub.1]|...| [P.sub.n]) and each [P.sub.i] is of the form x?*[y].Q

by Theorem 4.3.3. The second case cannot happen because the type environment [Delta] is not unlimited. []

6.2 Encoding Call-by-Name [Lambda]-Calculus

This subsection presents an encoding of the call-by-name, simply typed [Lambda]-calculus. We can again infer that a process which simulates a well-typed [[Lambda].sup.[right arrow]-term never deadlocks by using type information. We use the same syntax for [Lambda]-terms and types as in Section 6.1.

We follow Ostheimer and Davie [1993] and Turner [1996] for the encoding of call-by-name reduction. In call-by-name reduction, an argument is passed to a function before it is evaluated. So, a function type is represented by the type of channel along which a caller process passes a pair of channels, one of which is used by a callee process to trigger the evaluation of the argument, and the other of which is used to return the result. Thus, encoding of types and type environments is given as follows.

Definition 6.2.1. Types of [[Lambda].sup.[right arrow] are encoded by the following function [[.]]:

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

(The same time tag is used for u in all encodings of function types.)

A type binding x : [Tau] is encoded into x : !*[[!.sup.1] [[[[[Tau]]]].sup.u]]*. This is because the name of a variable in a [Lambda]-term is used as the name of a channel on which a request for a value should be sent.

Definition 6.2.2. Encoding of type environments is given by

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

We give an encoding of terms below. As in the previous section, the encoding function [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] returns a process that evaluates e (in the call-by-name style) and returns the result to the channel a.

A variable is implemented as a process that requests the value of the variable to be sent to a. The name of a variable is used as the name of the channel on which the request should be sent.

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

The encoding of a [Lambda]-abstraction [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] is almost the same as the one in the call-by-value [Lambda]-calculus, except for a type annotation.

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

Here [[Tau].sub.2] = ([Tau], x : [[Tau].sub.1](e).

The function application [e.sub.1] [e.sub.2] first spawns a process to evaluate the function el, then it passes to the function two channels: one for triggering evaluation of the argument and the other for receiving the result. We use an auxiliary process [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]. It waits on a channel x for a request for the value of e, and upon a request, it evaluates e and returns the value.

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

Here [[Tau].sub.1] = [Tau]([e.sub.2]), [[Tau].sub.2] = [Tau]([e.sub.1] [e.sub.2]), and s is a fresh time tag.

We can again prove the same theorems as those on the encoding of call-by-value reduction: typing is preserved by the encoding, and as its corollary, we can reason that the evaluation of an encoded term never gets stuck. Proofs are omitted here because they are almost the same as those for the call-by-value [Lambda]-calculus.

THEOREM 6.2.3. If [Tau] ?? e : [Tau] then [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] for a fresh time tag t.

THEOREM 6.2.4. Let e be a closed [[Lambda].sup.[right arrow]-term (i.e., 0 ?? e : [Tau]). If [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] for some [Delta], then either

(1) P' [equivalent] (vw:U) (a![v]{|Q}) or (2) there is some Q such that [Delta] ?? P' [right arrow] Q.

6.3 Encoding Call-by-Need [Lambda]-Calculus

We can obtain encoding of the call-by-need [Lambda]-calculus by minor modification to the encoding of the call-by-name [Lambda]-calculus. We need to redefine [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]. In the case of the call-by-need [Lambda]-calculus, it waits on a channel x for a request for the value of e, and upon the first request, evaluates e and supplies the value. After that, it just supplies the value computed before for each request. We also modify the encoding function so that it also returns an appropriate tag ordering under which the encoded process should be typed.

The encoding [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] is given by (t in [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] below represents the time tag of k)

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

where [s.sub.1], [s.sub.2], t are fresh time tags and where [Tau] = [[[Tau](e)]. The above encoding uses a mutex channel flag to remember whether or not e has been evaluated, and another mutex channel r to memorize the value of e. For simplicity, we regard dummy as a constant of type [[[Tau]]] here. Strictly speaking, for each function type [Tau] = [[Tau].sub.1] = [right arrow] [[Tau].sub.2], there should be a free replicated input channel [dummy.sub.[Tau], and a process [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] should run in parallel to the processes obtained by the above encoding (and also type bindings [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] should appear in type environments).

Other encodings are given below. They are the same as the encoding of the call-by-name [Lambda]-calculus except for orderings.

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

We can again prove that typing is preserved by the encoding, and as its corollary, we can reason, by using type information, that the evaluation of the encoded term never gets stuck. Unfortunately, because mutex channels are used, type information is not sufficient for reasoning about the uniqueness of the result.

THEOREM 6.3.1. Suppose [Tau] ?? e : [Tau], and let [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]. Then ??+ is a strict partial order, and [[[Tau]]], true: bool, false: bool, a : [!.sup.1] [[[[[Tau]]]].sup.t], ?? P.

THEOREM 6.3.2. Let e be a closed [[Lambda].sup.[right arrow]-term (i.e., 0 ?? e: [Tau]), and [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]. If a : [!.sup.1] [[[[[Tau]]]].sup.t] ?? P ?? P' ?? [Delta] for some [Delta]. Then, either

(1) P' [equivalent] (vw:U)(a![v]{|Q}) or (2) there is some Q such that [Delta] ?? P' [right arrow] Q.

6.4 Concurrent Objects

A concurrent object is a very useful data structure in concurrent programs. The main differences between a concurrent object and a functional object are that a concurrent object has an internal state and that a concurrent object must have a mechanism to ensure the atomic execution of a method (because more than one process may request method execution simultaneously).

We show two encodings of concurrent objects into the deadlock-free fragment of our typed calculus. The first one is simple and efficient, but restricted (for example, a concurrent object cannot invoke its own method during execution of a state-updating method). The second one is slightly more complicated, but more expressive.

6.4.1 Simple Encoding. Basically, a concurrent object is modeled by multiple processes, each of which handles each method. In order to avoid simultaneous executions of methods of the same objects (that mw lead to inconsistency), a state is implemented by using a mutex channel. The encoding presented here is based on the one by Pierce and Turner [1995].

The process below corresponds to a definition of concurrent objects. We use records for readability: {[l.sub.1] = [x.sub.1],..., [l.sub.n] = [x.sub.n]} creates a record whose field [l.sub.i] has value [x.sub.i] for each i([an element of] {1,..., n}), and x.1 extracts the value of field l from record x.

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

The above process waits for a request for the creation of a concurrent object with an initial state init and methods [meth.sub.1],..., [meth.sub.n]. When it receives a request, it stores the initial state in the internal (mutex) channel st, spawns processes to handle the methods, and returns a record each field of which contains a channel on which a request for method execution should be sent. The record of channels corresponds to the reference to a concurrent object. Each method handler ([m.sub.i]?* [v, c]. ...) repeatedly receives a message, reads the current state, and executes the corresponding method. When it finishes the method execution, it replies with the result and writes a new state into st. Thus, the above concurrent objects are implemented by using linear channels (used for receiving the reference of a created object and for receiving the result of method execution), mutex channels (used for storing states), and replicated input channels (used for receiving requests for method executions).

In the above example, the mutex channel st plays an important role in guaranteeing safe execution of methods: because st is a mutex channel, other method handlers must wait at st?[state]. ... until a new state is written, so that the consistency of the object's state is guaranteed. Moreover, since a method handler having the lock on st will eventually free the lock, the other method handlers do not remain blocked forever (if the method does not fall into infinite loop and the fairness is preserved).

Example 6.4.1.1. The following process is a definition of counter objects. (For simplicity, we assume primitive operations on integers.)

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

P is typed as

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

The following process Q creates a new counter object and invokes the methods inc and read:

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

We get 4 in the channel result when this process is executed in parallel to the counter definition process. By our type system, P | Q is typed as

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

By the theorems in Section 4, the above type judgment implies that if P | Q is reduced to a process which can no longer be reduced, then the process must be congruent to (vw:W) (result![m]|R), i.e., we get a value in the channel result.

The following example shows limitations of the simple encoding of concurrent objects: invocation of its own method causes deadlock with the simple encoding (a similar deadlock can happen also when two concurrent objects call mutual methods before releasing their locks on the states). Our type system can correctly detect such cases.

Example 6.4.1.2. Let us consider a case where a method of a concurrent object calls itself. With the above simple encoding, a definition is expressed as follows:

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

An object created by the above definition has a single method m. In the body of the method (st?[n]....), the method acquires a state, creates a new channel c', and calls itself. It results in deadlock as the following reductions show:

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

In our type system, the above process new?*[init, r]..., is judged to be ill typed: We obtain t ?? s from the subexpression c'?[res']. (c![res]| st![n']), the ordering s ?? u from m?*[c]. ..., and the condition [t/u] ?? [subset or equal to] ?? from m![c']. Thus, {(t,s), (s,t)} [subset or equal to] ??, which implies that ?? is not a strict partial order.

6.4.2 Alternative Encoding. We show a slightly more complicated encoding of concurrent objects in order to allow a concurrent object to invoke a method of itself. The idea of the encoding is (1) to distinguish between a channel used for ensuring exclusive execution of methods and a channel for storing the state and (2) to spawn two processes for handling each method: one for handling method invocations from the inside of the object and the other for handling method invocations from the outside. The new process corresponding to a definition of a concurrent object looks like

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

where let sel f = v in P is a shorthand for (vx) (x]![v]|x?[sel f]. P). Note that we still use only reliable channels.

7. DISCUSSIONS

We discuss some of the remaining issues on our type system, and also mention several extensions and variants.

7.1 Compositional Type Checking and Type Reconstruction

Compositional type checking and type reconstruction are important in practice. Unfortunately, the current formulation of the type system is not completely suitable for the compositional type checking. Consider a parallel composition [P.sub.1] | [P.sub.2]. Given typings [[Gamma].sub.1], ?? [P.sub.1] and [[Gamma].sub.2], ?? [P.sub.2], we cannot simply obtain [[Gamma].sub.1] + [[Gamma].sub.2], ?? [union] ?? [P.sub.1] | [P.sub.2]; it must be checked that ?? [union] ?? satisfy the conditions required in the derivations of [[Gamma].sub.1], ?? [union] [[Gamma].sub.2] ?? [P.sub.1] and [[Gamma].sub.2], ?? [union] ?? [P.sub.2] (and we may need to add some orderings to ?? [union] ??). In order to make the rules look more compositional, it would be sufficient to use constraints C on the tag ordering in a type judgment and write [Gamma], C ?? P, instead of using the tag ordering itself.

Type reconstruction is not so easy as type checking. However, it is not much more difficult than that for the linear channel type system [Kobayashi et al. 1996] because we can infer the required tag ordering automatically from a type environment and a type-annotated process expression. Since we have already developed a type reconstruction algorithm [Igarashi and Kobayashi 1997] for a variant of the linear channel type system, it would be possible to develop a (probably partial) type reconstruction algorithm along similar lines.

7.2 Variants and Extensions

7.2.1 Cyclic Ordering. The current type system requires that the transitive closure of a tag ordering should be a strict partial order; otherwise the process is ill typed and rejected. It may be too restrictive in practice because our type system sometimes rejects a process which actually does not deadlock. Instead of rejecting a cyclic ordering completely, we could provide it for the programmer as debugging information. Then, the programmer can examine the part warned by the type checker to know whether it really causes deadlock. For example, let [t.sub.x], [t.sub.y], and [t.sub.z] be time tags of channels x, y, and z. Given a tag ordering {([t.sub.x], [t.sub.y]), ([t.sub.y], [t.sub.x]), ([t.sub.y], [t.sub.z])}, a programmer knows that he or she needs to check the use of the channels x and y, but need not worry about the use of z.

7.2.2 Lower Bound of the Order of Channel Use. The tag ordering in our type system gives an upper bound of the dependency allowed in the use of channels. For example, let [t.sub.x], [t.sub.y] be the time tags of x, y. {([t.sub.x], [t.sub.y])} means that a process may be blocked on x before performing communication on y, but it does not mean that a process must do so.

If we are interested in using the tag ordering as a specification of processes, a lower bound of the dependency would also be useful: for example, if the relation {([t.sub.x], [t.sub.y])} is given as a lower bound, x must be used before y. A new type judgment would be of the form [Gamma], (??, ??) ?? P where ?? is a lower-bound of the ordering on channel use while -42 is an upper-bound of the ordering.

A lower bound would also be necessary if we want to guarantee deadlock-freedom for more general usage of channels which are currently classified as unreliable. For example, consider the process P = x?[]. y?[].x![]: it would be typed as

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

Note that we use here a multiset of type bindings as the type environment: two bindings ([MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]) on x express that x is used twice for input in P. The lower and upper bounds of the ordering indicate that x is used for input at first, y is used next, and then x is used again for input. Let us consider another process Q that is typed as

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII].

It implies that Q uses y for output after it uses x either once or twice. If we run P and Q in parallel, we cannot tell whether the binding [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] represents the first or second use of x. Thus, P | Q would be typed as

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

and the ordering {([t.sub.2], s), (s, [t.sub.2])} indicates that P | Q may deadlock: in fact, if Q is x![]|x![].y![], then P | Q can deadlock (here, we use an output guard x![].P for simplicity). However, if we strengthen the requirement for Q by refining the lower-bound

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII],

then P | Q can be typed as

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

Thus, deadlock-freedom is guaranteed. This example indicates that a lower bound of the ordering is strongly related to an upper bound and it sometimes plays an important role when we reason about deadlock.

7.2.3 Subtyping on Time Tags. Subtyping on time tags can be used to refine the deadlock-free fragment of the calculus. Consider the following type judgment for an output expression:

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

In our type system, [[Rho].sub.1] and [[Rho].sub.2] must be exactly the same. This requirement sometimes propagates unnecessary orderings, which leads to the rejection of processes that actually do not deadlock. We can avoid it by allowing [[Rho].sub.1] and [[Rho].sub.2] to be different in their time tags. For example, if [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII], then it is sufficient that the condition [[u.sub.1]/[u.sub.2]] ?? holds. These conditions can be generalized to a kind of subtyping relation. The resulting rule for output expressions would (roughly) look like

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

where a relation [Theta] ?? T [is less than or equal to] S can be structurally defined on types T, S.

7.2.4 Polymorphism on Time Tags. The side condition of the rule (T-NEW1) indicates that we cannot always forget the orderings on some of the channels bound by v-prefixes. For example, in the encoding of concurrent objects shown in Section 6, the orderings on the time tags of mutex channels must be kept globally. It sometimes leads to the rejection of processes which actually do not deadlock.

For example, consider the following object definition:

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

The above process creates an object with a method m. The method m invokes the method m of another object o. If o happens to be an object created by the above process, then our type system detects the cyclic dependency: s ?? u, u ?? s. This is because the orderings on the mutex channel used in o and those on st are merged by our type system.

We can avoid the above problem by allowing s to be passed via channels (and by introducing subtyping):

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

7.2.5 Infinite Set of Time Tags. In the current type system, only a finite number of time tags can appear in a type environment and a process. Therefore, the same tag may be assigned to distinct channels, which may cause nonexisting deadlock to be detected. One solution would be to use a finite representation of an ordering on an infinite set of time tags: a "regular" infinite graph (an analogue of a regular tree) whose leafs are labelled with time tags. It would be useful, for instance, for introducing recursive types: a recursive type [[micro]X.!.sup.1][[X].sup.t] can be viewed as a regular tree [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] with the relation {(t.0, t.1.0), (t.1.0, t.1.1.0),...}.

By combining an infinite time tag set and polymorphism on time tags, we might be able to eliminate the ad hoc rule (T-NEW-I). For example, the process of Example 3.5 would be written as

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

where an infinite set of time tags {t.0, t.1.0, t.1.1.0,...} with the relation {(t.1.0, t.0), (t.1.1.0, t.1.0),...} should be passed through X.

7.3 Process Equivalence

Since the tag ordering restricts processes that can be composed, it might be interesting to develop a new theory of process equivalence that takes the ordering into account. However, we think that, with the current type system, the resulting process equivalence would not be much coarser than the weak typed barbed congruence studied in the linear channel type system [Kobayashi et al. 1996]. One might expect that x?[]. P is behaviorally equivalent to x?[]. 0 | P if x is a reliable channel; however, it is not the case. There are two main reasons for this: one reason is that unreliable channels may be used to block a sender on x, as in ([MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]); and the other reason is that, even if the use of unreliable channels is forbidden, a process may be infinitely reduced without ever sending a value to x--for example, consider y![x] | y?*[z].y![z].

8. RELATED WORK

Although a number of type systems for process calculi have so far been proposed, as far as the author knows, our type system is the first one that can deal with deadlock in a satisfactory manner in name passing process calculi like the [Pi]-calculus (except for an earlier version of our type system [Kobayashi 1996b], which cannot ensure that typical concurrent objects are deadlock-free). It is because each type binding was handled separately in previous type systems (as in type systems for functional programming languages), while we need to keep track of dependency between type bindings to ensure deadlock-freedom. The type system by Berger et al. [1997] ensures deadlock-freedom, but the calculus is synchronous (in the sense that all processes must proceed in lock-step) and its communication topology is completely static.

Our type system is built on top of the previous type systems for process calculi: the input-only/output-only channel type system [Pierce and Sangiorgi 1993] and the linear channel type system [Kobayashi et al. 1996]. Especially, we used ideas of the latter to ensure the correct usage of communication channels, though ordering information was not introduced there.

Recently, Yoshida [1996] independently studied a type system for the monadic [Pi]-calculus where types can be represented by graph structures. They improved an equivalence theory of processes using the graph types, and proved the full abstraction theorem on the encoding of the polyadic [Pi]-calculus [Milner 1993] into the monadic [Pi]-calculus [Milner et al. 1992]. Although the purpose of their type system is different from ours, their type system and ours seem to have some similarities: an edge of their graphs corresponds roughly to an ordering between two time tags in our type system. Therefore, it might be interesting to develop a unifying, more general theory of their and our type system.

Sangiorgi [1997] introduced the notion of receptiveness: roughly speaking, a channel is receptive if its input end is immediately used after it is created. Their receptive channel is, therefore, very similar to our replicated input channel. They showed how receptiveness can improve an equivalence theory of processes.

Nestmann [1997] used our type system for showing partial correctness--the fact that the encoding does not introduce deadlock--of his encoding of a version of the [Pi]-calculus with the choice operator (+) into the one without choice.

Several techniques have been proposed for static analysis of communication in CML: Nielson and Nielson [1994] proposed a technique to extract terms of process algebra from CML programs and Colby [1995] proposed another technique based on abstract interpretation. Those techniques help programmers understand the behaviors of CML programs to some extent. However, (a possibly infinite number of) multiple communication channels are mapped to the same abstract channel during static analysis (which is called a region in Nielson and Nielson's analysis). Therefore, we cannot use those techniques to reason about deadlock, etc. To see why we cannot reason about deadlock, consider the process x?[ ]. 0 | y![ ]. If there is no process communicating over x or y in parallel to this process, it falls into deadlock. However, if we alias x and y to the same channel z (this can in fact happen in Nielson's analysis when x and y are sent somewhere through the same channel), the resulting process z?[]. 0 | z![] can be reduced to 0. On the other hand, consider the process x?[]. z?[]. Y![] | x![] | y? []. 0 | z![]. It is always reduced to 0. However, if we map x and y to the same channel w, then the resulting process

w?[]. z?[]. w![] | w![] | w?[].0 | z![]

may be reduced to the blocked process:

w?[]. z?[].w![] | 0 | z![].

As indicated by those examples, once distinct channels are mapped to the same channel, whether or not the original program deadlocks is irrelevant to whether or not its approximation does.

9. CONCLUSION

We have proposed a static type system for a process calculus that ensures partial deadlock freedom and shown that functions and typical concurrent objects can be implemented in the deadlock-free fragment of the calculus.

In addition to the issues discussed in Section 7, future work includes applications of our type system to static debuggers, compile-time optimizations, and run-time systems of concurrent programming languages. More studies of actual concurrent programs would also be necessary to judge whether or not the present type system is sufficient and to find an appropriate extension of the type system.

An idea of applying our type system to compile-time optimizations is as follows. Consider, for example, a process ([MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]), and suppose that P uses the output end of x and Q uses the input end of x. Suppose also we know by type information that P does not deadlock. Then, if we schedule P before Q, there is no need to check whether a value is in the channel x before Q receives the value from x. We are now trying to formalize this idea using the compilation framework developed by Oyama et al. [1997].

APPENDIX

A. PROOFS OF MAJOR LEMMAS AND THEOREMS

A.1 Proof of Lemma 3.13

PROOF. The proof follows from the fact that (T-REN) applied just below (TOUT) can be merged into (T-OUT), while (T-REN) applied just below other rules can be permuted upward. Because the other cases are similar and simpler, we show only the cases where (T-REN) is applied below (T-OUT), (T-IN), or (T-NEW-1).

--Case where (T-REN) is applied below (T-OUT): The derivation must be of the form

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

(where [[t.sub.y]/[t.sub.x], y/x](v:T) is defined as [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]. By the side conditions of (T-OUT), we have [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] (which follows from [u.sub.z] [an element of] [T.sub.I] and [t.sub.x], [t.sub.y] [an element of] [T.sub.O]),

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

Therefore, the derivation can be replaced by

(T-OUT) [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

--Case where (T-REN) is applied below (T-IN): The derivation must be of the form

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

We show that it can be replaced by

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

where the last step uses the rule (T-IN). Let ?? = [[t.sub.y]/[t.sub.x]] ??. Then, it suffices to check

(1) [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] is a strict partial order, (2) [[u.sub.z]/[s.sub.z]] ?? [subset or equal to] ??, (3) {[u.sub.z]} ?? {[s.sub.z]}, and (4) [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

By the conditions on the original derivation, we have

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

from which the third and fourth conditions immediately follow. We also have the second condition by

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

Suppose [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] is not a strict partial order. Then, by

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] is not a strict partial order either: a contradiction. Thus we have shown the first condition.

--Case where (T-REN) is applied below (T-NEW-1): The derivation must be of the form

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

We show that it can be replaced by

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

Notice that [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]. So, it is sufficient to show that [([t.sub.y]/[t.sub.x]] ??).sup.+] is a strict partial order. Suppose it is not the case. Then either (1) s ?? s holds, or (2) [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] is not a strict partial order. In either case, it contradicts with the fact that both ?? and [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] are tag orderings. Therefore, [([[t.sub.y]/[t.sub.x]] ??).sup.+] must be a strict partial order. []

A.2 Proof of Lemma 4.1.2

PROOF. This is proved by induction on the proof of P [equivalent] Q. The base cases (the leaves of the proof) consist of the four rules for structural congruence, plus reflexivity. The induction steps (inner nodes of the proof) arise from the definition of structural congruence as a congruence relation; they include rules allowing structural congruence to be applied to each subterm of each process constructor, plus symmetry and transitivity. Most cases are trivial: for example, the cases for the rules (S-COMMUT) and (S-ASSOC) follow from commutativity and associativity of "+." We present only the cases for the rule (S-EXTR) (in both directions).

Let P = (vx: [[Rho].sup.s]) [P.sub.1] | [P.sub.2], Q = (vx: [[Rho].sup.s]) ([P.sub.1] | [P.sub.2]), where x is not free in [P.sub.2], and suppose that [Gamma], ?? (vx: [[Rho].sup.s]) [P.sub.1] | [P.sub.2]. Then there are some [[Gamma].sub.1], [[Gamma].sub.2] such that [[Gamma].sub.1], ?? (vx: [[Rho].sup.s]) [P.sub.1] and [[Gamma].sub.2], ?? [P.sub.2], with [[Gamma].sub.1] + [[Gamma].sub.2] = [Gamma]. [[Gamma].sub.1], ?? (vx:[[Rho].sub.s]) [P.sub.1] must be derived by either (T-NEW-1) or (T-NEW-2).

--If it is derived by (T-NEW-1), then [[Gamma].sub.1],x:[[Rho].sup.s], ?? [P.sub.1] for some ?? such that [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]. By the side condition of (T-NEW-1), {s} ?? [T.sub.I], which implies (?? \ ??) [subset or equal to] [T.sub.O] x [T.sub.O]. So by Lemma 3.11, we have [[Gamma].sub.1], ?? [union] ?? [P.sub.1] and [[Gamma].sub.1], ?? [union] ?? [P.sub.2]. By T-PAR and (T-NEW-1), we have [Gamma], [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII].

--If [[Gamma].sub.1], ?? (vx: [[Rho].sup.s]) [P.sub.1] is derived by (T-NEW-2), it must be that [[Gamma].sub.1], x: [[Rho].sup.s], ?? [P.sub.1]. By (T-PAR) and (T-NEW-2), we have [Gamma], ?? (vx: [[Rho].sup.s]) ([P.sub.1] | [P.sub.2]).

On the other hand, suppose that [Gamma], ?? (vx: [[Rho].sub.s]) ([P.sub.1] | [P.sub.2].). It must be derived by either (T-NEW-1) or (T-NEW-2)

--If it is derived by (T-NEW-1), then [Gamma], x:[[Rho].sup.s], ([P.sub.1] | [P.sub.2]) for some ??, such that [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]. By (T-PAR), there are [[Gamma].sub.1], [[Gamma].sub.2], [[Rho].sub.1], such that [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]. By Lemmas 3.8 and 3.9, [[Gamma].sub.1], x: [[Rho].sup.s], [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]. By [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]. We therefore obtain [[Gamma].sub.2]\x, ?? [P.sub.2] by Lemmas 3.10 and 3.11. On the other hand, by [[Gamma].sub.1], x:[[Rho].sup.s], ?? [P.sub.1] and Lemma 3.11, we also obtain [[Gamma].sub.1], x: [[Rho].sup.s], ?? [union] ?? [P.sub.1]. By (T-NEW-I) and (T-PAR), we have [Gamma], ??-(vx: [[Rho].sup.s]) [P.sub.1] | [P.sub.2].

--If it is derived by (T-NEW-2), then [Gamma], x: [[Rho].sup.s], ?? [P.sub.1] | [P.sub.2]. By (T-PAR), there are some [[Gamma].sub.1], [[Gamma].sub.2] such that [[Gamma].sub.1], ?? [P.sub.1] and [[Gamma].sub.2], ?? [P.sub.2], with [[Gamma].sub.1] + [[Gamma].sub.2] = [Gamma],x :[[Rho].sup.s]. From the fact that x is not free in [P.sub.2] and Lemmas 3.8 and 3.9, we can assume [[Gamma].sub.1](x)= [[Rho].sup.s] and x [is not an element of](dom([[Gamma].sub.2]). By (T-NEW-2)and (T-PAR), we obtain [[Gamma].sub.1]\x + [[Gamma].sub.2], ?? (vx:[[Rho].sup.s]) [P.sub.1] | [P.sub.2], that is, [Gamma], ?? (vx:[[Rho].sup.s]) [P.sub.1] | [P.sub.2]. []

A.3 Proof of Subject Reduction Theorem (Theorem 4.3.1)

After proving several lemmas in A.3.1, we show the theorem by induction on the derivation of [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII].

A.3.1 Lemmas. The following two lemmas are used in the induction step for the rule (R-PAR).

LEMMA A.3.1.1. If [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] and [Gamma] + [Delta] is well defined, then [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII].

PROOF. The proof follows by induction on the derivation of [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]. The base cases (cases for the rules (R-COM) and (R-RCOM)) follow from the fact that if [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] is well defined, then [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]. Induction steps are straightforward. []

LEMMA A.3.1.2. If [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] and [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII], then [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] and [Gamma]' = [[Gamma]'.sub.1] + [[Gamma].sub.2] for some [[Gamma]'.subs.1].

PROOF. This is proved by induction on the derivation of [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]. Because the other cases are trivial, we show only the case for (R-PAR). In this case, [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII], and [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] and (T-PAR), we have

[[Gamma].sub.3] + [[Gamma].sub.4] = [[Gamma].sub.1]

[[Gamma].sub.3], ?? [P.sub.1]

[[Gamma].sub.4], ?? [P.sub.2]

for some [[Gamma].sub.3] and [[Gamma].sub.4]. Since [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] and [[Gamma]'.sub.3] + ([[Gamma].sub.4] + [[Gamma].sub.2]) = [Gamma]' for some [[Gamma]'.sub.3] by induction hypothesis. By Lemma A.3.1.1, [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]. Let [[Gamma]'.sub.1] = [[Gamma]'.sub.3] + [[Gamma].sub.4]. Then, [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]. []

The following lemma, together with Lemma 3.9, plays a key role in the base cases for (R-COM) and (R-RCOM).

LEMMA A.3.1.3. Let ?? be a strict partial order, and s,t, u time tags. If [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII], and {u} ?? {s}, then [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII].

PROOF. [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] follows from [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII].

On the other hand, by {u} ?? {s}, we have [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]. Therefore,

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII].

A.3.2 Proof of Theorem 4.3.1

PROOF. This is proved by induction on the derivation of [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII], with case analysis on the last rule used. When [Gamma] = [Gamma]', x: T, we write [Gamma] - x for [Gamma]', x: Rem(T).

--Case (R-COM): In this case, P = x![y] | x?[z]. Q, and P' = [y/z]Q. By (T-PAR) and (T-OUT), we have

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

for some [[Gamma].sub.1], [[Gamma].sub.2]. Without loss of generality (by Lemmas 3.8 and 3.9), we can assume that [[Gamma].sub.1] = 0 and [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]. We show [Gamma]', ?? P' by case analysis on m.

--Case m = 1 or w: In this case, by (T-IN),

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

for some [[Gamma].sub.3], ??. Note that

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII].

The above equation also implies that [Sigma]{y : [[Rho].sup.t]} + [[Gamma].sub.3] is well defined. By Lemma A.3.1.3, we have [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]. Therefore by repeated applications of Lemma 3.13 to [[Gamma].sub.3], [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII], we have

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII].

By weakening (Lemma 3.9),

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII],

i.e[Gamma]', ?? P'.

--Case m = M: In this case, by (T-MIN),

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

for some [[Gamma].sub.3]. Note that

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

The above equation also implies that [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] is well defined. By Lemma A.3.1.3, we have [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]. Therefore, by repeated applications of Lemma 3.13 to [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII], we have

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII].

By weakening (Lemma 3.9),

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII],

i.e., [Gamma]', ?? P'.

--Case (R-RCOM): In this case, P = x![y]|x?*[z]. Q, and P' = [y/z]Q'|x?*[z]. Q, with Q' = rename(Q). By replacing time tags in the derivation of [Tau], ?? P, we also have the derivation of

[Tau], [s'/s] ?? x![y]| [x?*[z].Q'

where {s} = New(Q) and s' are the corresponding time tags in Q' ({s'} = New(Q')). Let [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]. Then by Lemma 3.12,

[Tau], ?? x![y]| x?*[z].Q'.

By (T-PAR), (T-OUT), and (T-RIN),

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

for some unlimited type environment [[Tau].sub.2]. By Lemma A.3.1.3, ?? = [t/[t.sub.z]] [??.sub.2]. So by repeated applications of Lemma 3.13 [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII], we obtain [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]. On the other hand, by replacing s' with s in the derivation of [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII], we also have

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

By (T-PAR),

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

By Lemma 3.9 and [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII], we have [Tau]', ?? P'.

--Case (R-PAR): In this case, P = [P.sub.1] | [P.sub.2], P' = [P'.sub.1] | [P.sub.2], and [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]. Moreover,

[[Tau].sub.1], ?? [P.sub.1]

[[Tau].sub.2], ?? [P.sub.2]

[[Tau].sub.1], + [[Tau].sub.2] = [Tau]

for some [[Tau].sub.1], [[Tau].sub.2]. By Lemma A.3.1.2, [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] for some [[Tau]'.sub.1], and [Tau]' = [[Tau]'.sub.1] + [[Tau].sub.2]. By induction hypothesis, [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] and some {s} [subset or equal to] New([P.sub.1]). By repeated applications of Lemma 3.12, [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]. By (T-PAR), [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII], i.e., [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]. Note that New(P')\New(P) = New([P'.sub.1])\New([P.sub.1]) = {s'} and {s} [subset or equal to] New([P.sub.1]) [subset or equal to] New(P).

--Case (R-NEW): In this case, P = (vx: [[Rho].sup.t])Q, P' = (vx : [[Rho]'.sup.t])Q', and [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] can be derived by either (T-NEW-1) or (T-NEW-2).

--Case for (T-NEW-1): [Tau], x [[Rho],sup.t], [??.sub.1] ?? Q for some [??.sub.1] such that [??.sub.1] [??.sub.{t}] = ??.

By Lemma 3.11, [Tau], x : [[Rho].sup.t], [??.sub.1] [union] ?? Q. By induction hypothesis, [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] for {s'} = New(Q')\New(Q)(= New(P')\New(P)) and {s} [subset or equal to] New(Q)([subset or equal to] New(P)). By (T-NEW-1), we have [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]. Note that [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII].

--Case for (T-NEW-2): [Tau], x : [[Rho].sup.t], ?? Q. By induction hypothesis, [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] for (s') = New(Q')\New(Q)(= New(P')\New(P)) and {s} [subset or equal to] New(Q)([subset or equal to] New(P)). By (T-NEW-2), [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII].

--Cases (R-IFT) and (R-IFF) are trivial.

--Case (R-CONG) follows immediately from Lemma 4.1.2.

B. RULES FOR TYPE CHECK

This appendix presents modified typing rules in order to clarify the first phase of the type check algorithm explained informally in Section 5. In order to make the flow of type information in the algorithm more explicit, we consider a type judgment of the form [[Tau].sub.1], ?? P :: [[Tau].sub.2]. A type environment [[Tau].sub.1] represents capabilities that may be consumed by the process P, while [[Tau].sub.2] represent capabilities that are actually consumed by P. Each of the new typing rules will express how [[Tau].sub.2] can be computed from inputs [[Tau].sub.1] and P. For example, the rule for parallel composition is given as follows:

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

Here [[Tau].sub.1] - [[Tau].sub.2], defined below, represents a type environment obtained from [[Tau].sub.1] by removing capabilities in [[Tau].sub.2].

We need several definitions before presenting the rules.

Definition B. 1. The binary operation - on types is defined by

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

In other cases, [[Tau].sub.1] - [[Tau].sub.2] is undefined. - is extended to the operation on type environments: [[Tau].sub.1] - [[Tau].sub.2] is defined as follows, only if dom([[Tau].sub.1]) [contains or equal to] dom([[Tau].sub.2]) and [[Tau].sub.1] (x) - [[Tau].sub.2](x) is defined for each x [element of] dom([[Tau].sub.2]).

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

Definition B.2. The binary operation ?? on types is defined by

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

In other cases, [T.sub.1] ?? [T.sub.2] is undefined. U is extended to the operation on type environments: [[Tau].sub.1] ?? [[Tau].sub.2] is defined as follows, only if [[Tau].sub.1] (x) ?? [[Tau].sub.2](x) is defined for each

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

Notation B.3. We write [Tau]\S for the type environment [Delta] such that dom([Delta]) = dom([Delta])\S and [Delta](x) = [Delta](x) for each x [element of] dom([Delta]). [Tau]|S represents the type environment [Delta] such that dom([Delta]) = S [intersection] dom([Tau]) and [Delta](x) = [Tau](x) for each x [element of] dom([Delta]).

The new typing rules are given below. In each type judgment [[Tau].sub.1], ?? P :: [[Tau].sub.2] in the rules, we implicitly assume that [[Tau].sub.1]-[[Tau].sub.2] is well defined. Although the assumption is redundant for Theorem B.4, it is necessary in the actual type-checking algorithm: for example, in (TC-IN), the assumption is used to determine m, [Rho], t, etc.

(TC-PAR) [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

(TC-OUT) [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

(TC-IN) [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

(TC-MIN) [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

(TC-RIN) [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

(TC-NEW-1) [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

(TC-NEW-2) [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

(TC-IF) [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

We explain how to read a few of the above rules in the first phase of type check. The rule (TC-PAR) means that in order to check [P.sub.1] | [P.sub.2] under a type environment [[Tau].sub.1], we should first check [P.sub.1] under [[Tau].sub.1], and obtain [[Tau].sub.2]; then we can check [P.sub.2] under [[Tau].sub.1] - [[Tau].sub.2]. The rule (TC-IN) means that in order to check x?[z].P under [Tau], we should first check P under [Tau], z : [[Rho].sup.s] and obtain [Delta] (here [Rho] is known by looking at the binding of x in [Tau]); then we should check that [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] is unlimited (which means the obligations on z are fulfilled in P) and output [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII].

It is a routine to check that the new rules are essentially equivalent to the original rules.

THEOREM B.4. If [Tau], ?? P, then [Tau], ?? P :: [Delta] for some [Delta] such that [Tau] - [Delta] is unlimited. On the other hand, if [Tau], ?? P :: [Delta] for some [Delta] such that [Tau] - [Delta] is unlimited, then [Tau], ?? P.

ACKNOWLEDGMENTS

The author would like to thank Benjamin C. Pierce and David N. Turner for joyful discussions and a number of useful suggestions. Among others, Benjamin C. Pierce suggested that we consider polymorphism on time tags, and David N. Turner suggested encoding of call-by-need [Lambda]-calculus. Their questions also helped us improve understanding of our type system. The author would also like to thank Nobuko Yoshida, Davide Sangiorgi, Simon Gay, and Uwe Nestmann for discussions on the relationships between their work and ours. Special thanks are also due to anonymous referees, for their very useful comments.

(1) This is for a rather subtle technical reason coming from the side condition of rule (T-NEW-1) in Section 3. It might be possible to keep ordering on replicated input channels by relaxing the condition.

(2) This follows intuitively because we want to distinguish between direct dependency (e.g., the dependency between x and y in x?[]. yl[]) and indirect dependency (e.g., the one between x and y in x?[]. z![] [z?[].y![]) of channel usage. This distinction is especially important in the rule (T-NEW-1) in Section 3.

(3) (T-NEW-1) and (T-NEW-2) are regarded as the same rule in this step, since they differ only in a condition on time tags.

(4) We expect that it is possible to encode [Lambda]-calculi with more advanced type systems by appropriate extensions of our process calculus with subtyping [Pierce and Sangiorgi 1993], polymorphism [Pierce and Sangiorgi 1997], etc. It is because the communication behavior of a process obtained by encoding a function does not depend so much on the presence of subtyping or polymorphism. For example, a polymorphic identity function would be encoded into a process like f?*[[Alpha], x : [Alpha], r : [!.sup.1] [[Alpha]]]. r![x], which essentially has the same communication behavior as its monomorphic counterpart: f?* [x, r]. r![x].

(5) The encoding presented here evaluates a function and its argument in parallel. Alternative encoding, which evaluates a function and its argument sequentially, is of course possible, and satisfies the same properties as those proved below.

(6) Actually, as we encode the simply typed [Lambda]-calculus, the process never falls into an infinite loop. But our type information is not sufficient for such reasoning.

REFERENCES

BERGER, M., GAY, S., and NAGARAJAN, e. 1997. A typed calculus of deadlock-free processes. Draft paper, Imperial College, London.

COLBY, C. 1995. Analyzing the communication topology of concurrent programs. In Proceedings of the ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation. ACM Press, New York, 202-213.

GAY, S. J. 1993. A sort inference algorithm for the polyadic [Pi]-calculus. In Proceedings of ACM SIGPLAN/SIGACT Symposium on Principles of Programming Languages. ACM Press, New York, 429-438.

HODAS, J. S. and MILLER, D. 1994. Logic programming in a fragment of intuitionistic linear logic. Inf. Comput. 110, 2, 327-365.

HONDA, K. and YOSHIDA, N. 1995. On reduction-based process semantics. Theor. Comput. Sci. 151, 2, 437-486.

IGARASHI, A. and KOBAYASHI, N. 1997. Type-based analysis of usage of communication channels for concurrent programming languages. In Proceedings of International Static Analysis Symposium (SAS '97). Lecture Notes in Computer Science, vol. 1302. Springer-Verlag, Berlin, 187-201.

KOBAYASHI, N. 1996a. Concurrent linear logic programming. Ph.D. thesis, Dept. of Information Science, Univ. of Tokyo, Japan.

KOBAYASHI, N. 1996b. A partially deadlock-free typed process calculus (I)--a simple system. Tech. Rep. 96-02, Dept. of Information Science, Univ. of Tokyo, Japan.

KOBAYASHI, N. and YONEZAWA, A. 1995. Towards foundations for concurrent object-oriented programming--types and language design. Theory Pract. Object Syst. 1, 4, 243-268.

KOBAYASHI, N., PIERCE, B. C., and TURNER, D. N. 1996. Linearity and the pi-calculus. In Proceedings of ACM SIGPLAN/SIGACT Symposium on Principles of Programming Languages. ACM Press, New York, 358-371.

MACKIE, I. 1994. Lilac: A functional programming language based on linear logic. J. Funct. Program. 4, 4 (Oct.), 1-39.

MILNER, a. 1990. Function as processes. In Automata, Language and Programming. Lecture Notes in Computer Science, vol. 443. Springer-Verlag, Berlin, 167-180.

MILNER, R. 1993. The polyadic [Pi]-calculus: A tutorial. In Logic and Algebra of Specification, F. L. Bauer, W. Brauer, and H. Schwichtenberg, Eds. Springer-Verlag, Berlin.

MILNER, R., PARROW, J., and WALKER, D. 1992. A calculus of mobile processes, I, II. Inf. Comput. 100, 1-77.

NESTMANN, U. 1997. What is a 'good' encoding of guarded choice? In Proceedings of EXPRESS '97. Electronic Notes in Theoretical Computer Science, vol. 7. Elsevier Science Publishers, Amsterdam.

NIELSON, H. a. and NIELSON, F. 1994. Higher-order concurrent programs with finite communication topology. In Proceedings of ACM SIGPLAN/SIGACT Symposium on Principles of Programming Languages. ACM Press, New York, 84-97.

OSTHEIMER, G. and DAVIE, A. J. T. 1993. [Pi]-calculus characterizations of some practical [Lambda]-calculus reduction strategies. Tech. rep., St. Andrews Univ., Scotland.

OYAMA, Y., TAURA, K., and YONEZAWA, A. 1997. An efficient compilation framework for languages based on a concurrent process calculus. In Proceedings of Euro-Par '97 Parallel Processing, Object-Oriented Programming. Lecture Notes in Computer Science, vol. 1300. Springer-Verlag, Berlin, 546-553.

PEYTON JONES, S. 1996. Concurrent Haskell. In Proceedings of ACM SIGPLAN/SIGACT Symposium on Principles of Programming Languages. ACM Press, New York, 295-308.

PIERCE, B. and SANGIORGI, D. 1993. Typing and subtyping for mobile processes. In Proceedings of IEEE Symposium on Logic in Computer Science. IEEE, New York, 376-385.

PIERCE, B. C. and SANGIORGI, D. 1997. Behavioral equivalence in the polymorphic pi-calculus. In Proceedings of ACM SIGPLAN/SIGACT Symposium on Principles of Programming Languages. ACM Press, New York, 242-255.

PIERCE, B. C. and TURNER, D. N. 1995. Concurrent objects in a process calculus. In Theory and Practice of Parallel Programming (TPPP). Lecture Notes in Computer Science, vol. 907. Springer-Verlag, Berlin, 187-215.

PIERCE, B. C. and TURNER, D. N. 1997. Pict: A programming language based on the pi-calculus. Tech. rep., Computer Science Dept., Indiana Univ. To appear in Milner Festschrift, MIT Press, 1997.

REPPY, J. H. 1991. CML: A higher-order concurrent language. In Proceedings of the ACM SIGPLAN '91 Conference on Programming Language Design and Implementation. ACM Press, New York, 293-305.

SANGIORGI, D. 1992. Expressing mobility in process algebras: First-order and higher-order paradigms. Ph.D. thesis, Univ. of Edinburgh, Edinburgh, Scotland.

SANGIORGI, D. 1997. The name discipline of uniform receptiveness (extended abstract). In Proceedings of ICALP '97. Lecture Notes in Computer Science, vol. 1256. Springer-Verlag, Berlin, 303-313.

SHAPIRO, E. 1989. The family of concurrent logic programming languages. ACM Comput. Surv. 21, 3 (Sept.), 413-510.

TURNERS, D. T. 1996. The polymorphic pi-calculus: Theory and implementation. Ph.D. thesis, Univ. of Edinburgh, Edinburgh, Scotland.

VASCONCELOS, V. T. and HONDA, K. 1993. Principal typing schemes in a polyadic [Pi]-calculus. In Proceedings of CONCUR'93. Lecture Notes in Computer Science, vol. 715. Springer-Verlag, Berlin, 524-538.

WALKER, D. 1995. Objects in the [Pi]-calculus. Inf. Comput. 116, 253-271.

YONEZAWA, A. and TOKORO, M. 1987. Object-Oriented Concurrent Programming. The MIT Press, Cambridge, Mass.

YOSHIDA, N. 1996. Graph types for monadic mobile processes. In Proceedings of FST/TCS'16. Lecture Notes in Computer Science, vol. 1180. Springer-Verlag, Berlin, 371-387. Full version as LFCS report, ECS-LFCS-96-350, Univ. of Edinburgh.

An extended and revised version of the paper presented at 12th IEEE Symposium on Logic in Computer Science (LICS'97).

Author's address: Department of Information Science, University of Tokyo, 7-3-1 Hongo, Bunkyoku, Tokyo 113-0033, Japan; email:koba@is.s.u-tokyo, ac.jp. Permission to make digital/hard copy of all or part of this material without fee for personal or classroom use provided that the copies are not made or distributed for profit or commercial advantage, the ACM copyright/server notice, the title of the publication, and its date appear, and notice is given that copying is by permission of the ACM, Inc. To copy otherwise, to republish, to post on servers, or to redistribute to lists requires prior specific permission and/or a fee. [C] 1998 ACM 0164-0925/98/0300-0436 $5.00

Printer friendly Cite/link Email Feedback | |

Author: | Kobayashi, Naoki |
---|---|

Publication: | ACM Transactions on Programming Languages & Systems |

Date: | Mar 1, 1998 |

Words: | 21721 |

Previous Article: | A new framework for elimination-based data flow analysis using DJ graphs. |

Next Article: | The design, implementation, and evaluation of Jade. |

Topics: |