\documentclass[12pt]{article} \usepackage{amsmath} \usepackage{amssymb} %\title{Strong Process Types for Coordinating Objects} \title{Process Types for Active Objects} \author{\small Franz Puntigam \\[-5pt] \small Technische Universit\"{a}t Wien, Institut f\"{u}r Computersprachen \\[-5pt] \small Argentinierstra{\ss}e 8, A-1040 Vienna, Austria \\[-5pt] \small E-mail: franz@complang.tuwien.ac.at } \date{} \setlength{\oddsidemargin}{0in} \setlength{\evensidemargin}{0in} \setlength{\headsep}{0pt} \setlength{\topmargin}{0in} \setlength{\textheight}{9.3in} \setlength{\textwidth}{6.3in} \setcounter{topnumber}{2} \setcounter{bottomnumber}{0} \setcounter{totalnumber}{2} \renewcommand{\topfraction}{.9} \renewcommand{\textfraction}{.1} \renewcommand{\floatpagefraction}{0.9} \newtheorem{definition}{Definition} \newtheorem{theorem}{Theorem} \newtheorem{proposition}[theorem]{Proposition} \newtheorem{corollary}[theorem]{Corollary} \newcommand{\rfig}[1]{Fig.~\ref{#1}} \newcommand{\rthm}[1]{Theorem~\ref{#1}} \newcommand{\rprp}[1]{Proposition~\ref{#1}} \newcommand{\rsec}[1]{Sect.~\ref{#1}} \newcommand{\rdef}[1]{Def.~\ref{#1}} \newcommand{\qed}{\hspace*{\fill}~\ensuremath{\square}} \newcommand{\lsb}{\boldsymbol{[}} \newcommand{\rsb}{\boldsymbol{]}} \newcommand{\llb}{\langle} \newcommand{\rlb}{\rangle} \newcommand{\lcb}{\boldsymbol{\{}} \newcommand{\rcb}{\boldsymbol{\}}} \newcommand{\nil}{\ensuremath{\lcb\rcb}} \newcommand{\isd}{\ensuremath{{:}{:}{=}}} \newcommand{\call}[1]{\ensuremath{@{#1}}} \newcommand{\new}[3]{\ensuremath{{#1}\,{:}{=}\,{#2}@{#3}}} \newcommand{\snd}[2]{\ensuremath{{#1}{\triangleleft}{#2}}} \newcommand{\msg}[2]{\ensuremath{{#1}\llb{#2}\rlb}} \newcommand{\rcv}[2]{\ensuremath{{#1}\llb{#2}\rlb}} \newcommand{\cond}[3]{\ensuremath{{#1}\,{?}\,{#2}\,|\,{#3}}} \newcommand{\class}[2]{\ensuremath{\lcb{#1}\rcb{:}\lcb{#2}\rcb}} \newcommand{\rec}[1]{\ensuremath{{!}\ul{#1}}} \newcommand{\typ}[2]{\ensuremath{\lcb{#1}\rcb\lsb{#2}\rsb}} \newcommand{\sign}[2]{\ensuremath{{#1}\llb{#2}\rlb}} \newcommand{\beh}[3]{\ensuremath{{#1}\lsb{#2}\rsb\lsb{#3}\rsb}} \newcommand{\creat}[2]{\ensuremath{@{#1}\lsb{#2}\rsb}} \newcommand{\mset}[1]{\ensuremath{\lsb{#1}\rsb}} \newcommand{\lst}[1]{\ensuremath{\llb{#1}\rlb}} \newcommand{\coll}[1]{\ensuremath{\lcb{#1}\rcb}} \newcommand{\gr}[1]{\ensuremath{\tilde{#1}}} \newcommand{\ul}[1]{\ensuremath{\underline{#1}}} \newcommand{\ulg}[1]{\ensuremath{\underline{\tilde{#1}}}} \newcommand{\subst}[2]{\ensuremath{[{#1}/{#2}]}} \newcommand{\trans}[1]{\ensuremath{\stackrel{#1}{\longrightarrow}}} \newcommand{\free}[1]{\ensuremath{\textit{free}({#1})}} \newcommand{\relevant}[1]{\ensuremath{\textit{eff}\,\coll{#1}}} \newcommand{\act}[1]{\ensuremath{\textit{enbl}{#1}}} \newcommand{\init}[1]{\ensuremath{\textit{init}\,\coll{#1}}} \newcommand{\seq}[1]{\ensuremath{\textit{seq}\,({#1})}} \newcommand{\cseq}[1]{\ensuremath{\textit{cseq}\,({#1})}} \newcommand{\TE}[1]{\ensuremath{\Gamma_{\!\!{#1}}}} \newcommand{\mtyp}{\textrm{type}} \newcommand{\num}{\textrm{int}} \begin{document} \maketitle \begin{abstract} \noindent An object's type is usually regarded as a contract between the object and each of its clients. However, in concurrent (and sometimes also in sequential) systems it is more useful to regard a type as a contract between an object and the unity of all clients: When the object acts as a shared resource, the clients must be coordinated before sending messages to the object. Process types of active objects specify constraints on the ordering of messages. Static type checking ensures that clients are coordinated so that the objects receive messages only in acceptable orderings. As presented in this article, the process type system is based on a simple computation model, where active objects communicate via asynchronous message passing. \paragraph{Keywords:} Type systems, concurrent programming languages, active objects. \end{abstract} \section{Introduction} Each expression written in a statically typed programming language has a unique type known at compile time. Strong typing ensures that violations of type constraints (type errors) cannot occur during program execution~\cite{CaWe85}. Static and strong typing can increase the readability and reliability of programs and support optimizations. In the object-oriented programming paradigm, types specify contracts between objects (used as servers) and their clients~\cite{Meye94}. These relatively stable contracts play an important role in the maintenance and reuse of software. They decouple details of the objects' implementations from the objects' uses and, thereby, help to keep incremental program modifications local. Subtyping supports polymorphism and allows the programmer to provide types at multiple levels of abstraction. An object's type is usually represented by the object's signature, often associated with a name used as informal description of the object's behavior. In some languages like Eiffel~\cite{Meye92}, programmers can formally express their expectations on the input and result parameters and give partial specifications of the behavior using assertions (preconditions, postconditions and invariants). Clients can safely use the object's methods and will get the promised results whenever the preconditions are satisfied. This type concept is quite useful for a large class of applications. For other applications, however, assertions are not sufficient~\cite{LiWi94}. Especially, expectations on \emph{sequences} of messages sent to objects cannot be expressed appropriately. This problem, which shows up quite frequently in concurrent applications, shall be tackled in the present article. This is the structure of the article: A simple example in \rsec{problem} demonstrates the problem. A general solution is briefly presented in \rsec{design-space}. %The prerequisites for this solution affect conventional approaches to %subtyping and genericity, as pointed out in \rsec{intro-sub}. The proposed type system and the underlying computation model are surveyed in \rsec{proposal}. A formal presentation of computation model and type system follows in \rsec{model}. Static type checking is dealt with in \rsec{type-check}. %The results of this work and indented uses of the type system are discussed %in \rsec{discussion}. A comparison with related work is given in \rsec{related}. \subsection{The Problem} \label{problem} Sometimes, methods shall be called only in certain circumstances depending on the object's state and history. For example, let ``iconify'' be a method that replaces a window on a screen with an icon. Preconditions seem to be appropriate for specifying that ``iconify'' shall be called only when the window is displayed. However, preconditions have limitations: They are not ``history sensitive''~\cite{MaYo93} and cannot always be checked statically, loosing the advantages of strongly typed languages. In concurrent and distributed systems it is quite difficult for a client to know an object's state even at run time if other clients running concurrently may cause unpredictable state changes. Unexpected effects may occur in this case even if all preconditions are satisfied. For example, two concurrent clients send ``iconify'' at about the same time to a displayed window. The window is replaced with an icon when the first message is handled. A further client sees the new state and sends ``uniconify'', a message causing the window to be displayed. Then, after handling this message, the window is immediately replaced with an icon again when the second ``iconify'' message is handled. This behavior is probably unexpected because one of the ``iconify'' messages is dealt with in a context different from the one in which the message was sent. In general, delaying the handling of received messages until the object is in an expected state (as proposed by several groups \cite{Caro93,KoYo94,Meye93}) is not always a satisfactory solution of the problem that some messages cannot be handled in each state. There are several ways to prevent that messages are dealt with in wrong contexts. For example, the programmer implements a protocol ensuring that always only one client can send ``iconify'' and ``uniconify'' in alternation, and these messages are handled in the same sequence they were sent. However, there is no support from current type systems, where a type is a contract between each individual client and an object, but not between the set of all clients and the object. It is not possible to express in the type that clients must be coordinated before sending messages like ``iconify'' and ``uniconify''. There is the implicit assumption that each object must be able to handle all supported messages from all clients in arbitrary interleaving. As the window example shows, this assumption can be too restrictive in practice. \subsection{A Solution and its Prerequisites} \label{design-space} This problem can be solved by using types that express not only the sets of messages the objects will accept, but also constraints on the acceptable sequences of these messages. The acceptability of messages can depend on previously accepted messages. To be sure that the message will be accepted, a client who wants to send a message to an object must know that, when the message arrives, the object will already have accepted all messages the acceptability of this message depends on. The information needed by the client has several aspects. The client must know \begin{enumerate} \item on which previous messages the acceptability depends; \item which of these messages have already been sent to the object; \item in which order sent messages will be received by the object. \end{enumerate} Since static type checking shall be supported (where a compiler ensures that all messages sent to an object are acceptable) this information must be provided statically: \begin{enumerate} \item Information about expected message sequences (expressing dependencies between messages) can easily be encoded in the static type of the object receiving the messages. There are many different formalisms to specify message sequences. For example, regular expressions, push-down automata and process calculi are appropriate. However, when using the most expressive formalisms, it is, in general, not decidable whether two types specify the same set of message sequences \cite{HoUl69}, and static type checking may become very difficult. Hence, less expressive formalisms and/or stricter notions of type equivalence must be used. \item If an object has only a single client, it is easy for the client to know the sequence of all messages already sent to the object. This information is statically available for many programming language concepts. However, most objects have several clients. Even in this case each client has enough information if the messages sent by a client depend only on previous messages sent by the same client. If a message to be sent by one client depends on messages sent by other clients, the clients have to be coordinated: The other clients have to inform the first one about sending the messages. Since there are many different ways to coordinate clients, it is nearly impossible to check appropriate coordination just by examining the communication patterns. Another approach is more promising: The current state of sending messages is encoded in types associated with references to objects. When sending messages to objects via these references, the types are updated. Clients coordinate themselves by exchanging object references with up-to-date type information. The type checker has to ensure only that each client has the needed references with appropriate types. \item It is easy to require that all messages arrive at the addressee in the same order as they were sent and are handled in the same order as they arrive. This solution is attractive because the context for handling a message is already known when the message is sent. However, complete serialization is inefficient in parallel and distributed applications. Fortunately, it is sufficient to require that all messages are handled in the same \emph{logical} order as they were sent; a message must be handled before another message only if sending the second message depends on previously sending the first message. There are efficient techniques to enforce that the logical ordering is kept. \end{enumerate} These considerations suggest that it should be possible to design a concurrent object-oriented programming language with a type system, where a type is regarded as a contract between an object and the unity of all clients. Messages in this language must be handled in the same logical order as they were sent. Types associated with object references must be updated when sending messages; they cannot be immutable. If types shall be more expressive than regular expressions, the notion of type equivalence must be stricter than that of the equivalence of message sequence sets. A crucial aspect of type systems for object-oriented languages is the support of subtyping. According to the principle of substitutability, an instance of a subtype can be used wherever an instance of a supertype is expected~\cite{LiWi94,WeZd88}. In the proposed type system, a subtype can extend a supertype by specifying additional messages and less constraints on acceptable message sequences so that each message accepted by an object of a supertype is also accepted by an object of a subtype. However, if types are more expressive than regular expressions, the notion of subtyping has to be stricter than that of the containment of message sequence sets. Furthermore, the possibility of updating types has to be considered: The subtype relationship between two types has to remain intact when these types are updated according to sending (or accepting) the same message. Possible updating of types requires consideration also when dealing with genericity, especially constrained genericity: A type parameter can occur in several parts of a program. The value of (i.\,e., type in) the type parameter is not connected to a single object reference and, therefore, is not updated when a message is sent to the object. Sometimes it is necessary to refer to the value of the type parameter after type updating, although this value my be unknown at compile time. Similar considerations are necessary when using dynamic type information by, for example, performing checked type conversions. \subsection{The Proposal} \label{proposal} Systems composed of active objects that communicate through asynchronous message passing are considered. This form of communication is semantically simple and performs efficiently on current communication networks. More complex communication protocols can easily be based on asynchronous message passing. Each object has its own (single) thread of execution, a unique identifier used as mail address, a behavior and an unlimited queue of received messages, as in the actor model~\cite{Agha86,AMST92}. According to its behavior, an object can accept messages in its message queue, send messages to objects, create new objects and change its own behavior. The behavior can depend on the equality of object identifiers and subtype relationships between type expressions. Other than in the actor model and as required by the type system, all messages are received and accepted in the same logical order they were sent; message queues operate in a first-in-first-out manner. This model provides a natural basis for concurrent and distributed object-oriented systems. Process calculi like those explored by Hoare~\cite{Hoar78}, Milner~\cite{MiPW92,Miln89,Miln91} and others~\cite{BaWe90,Henn88,HoTo91} provide a theoretically well-founded and expressive basis for specifying the behavior of active objects. But they have to be adapted so that all messages sent to some address are handled sequentially by a single object, and some atomic actions carry type information. The used calculus shall be simple enough to show static type checking, and expressive enough to support all important language concepts. Types in the proposed type system are called \emph{process types} because they partially specify processes, i.\,e., the behavior of objects. A process type consists of several parts: a state, a set of message descriptors and a set of creator descriptors. A message descriptor specifies the signature of a message, the acceptability of corresponding messages depending on the state, and updates of the state when sending or accepting such messages. A creator descriptor specifies the signature of a message creating a new instance of the type, and the initial state of the new instance. Several operations are applicable to process types: \begin{description} \item[Type updating:] The state of a type is updated when sending or accepting messages. \item[Type splitting:] A type is split into two types (being supertypes of the first type) such that all arbitrary interleavings of message sequences specified by one of the latter types with those specified by the other of the latter types are specified by the first type also. \item[Type combination:] The reverse operation to type splitting; two types are combined to a single one (being a subtype of both of the two types). \end{description} % There are three different uses of process types: \begin{description} \item[Object type:] Each object is associated with a type partially specifying the object's behavior. The object must accept all message sequences specified by the type. The type is updated when the object accepts a message. Type splitting and type updating of the object's type are useful only in a special case (see \rsec{type-check}). \item[Type mark:] Each reference to an object is associated with a type mark which specifies all sequences of messages that can be sent to the object via this reference. The type mark is updated when a message is sent via the reference. Whenever a new reference to an object (alias) is introduced by copying an existing reference, the type mark of the existing reference has to be split into two supertypes: One of the supertypes becomes the new type mark of the existing reference; the other becomes the type mark of the new reference. This application of type splitting ensures that the object accepts messages sent according to the type marks of the two references in arbitrary interleaving; no coordination is necessary. Two references to the same object can be combined into a single one with a single type mark. The combination of two type marks may specify more message sequences than arbitrary interleavings of message sequences specified by the two type marks. Thus, the combination can be used in a more flexible way. \item[Free type:] A type supplied as value of a type parameter is free because it is associated with neither an object nor an object reference. None of the operations on process types is applicable to free types. \end{description} A type mark can be regarded as a ``claim'' to sending messages. It can be used up (by sending messages) or given to another object (in part or as a whole) as side-effect of sending messages: An object reference supplied as message argument introduces a new object reference known by the object accepting of the message; the type mark of the first reference must be split into two supertypes so that each of the two references gets a supertype as new type mark. It is up to the programmer to specify how the type mark is split, i.\,e., how much of the claim is given to the object accepting the message. By specifying which object references are passed as arguments and how the corresponding type marks are split, the programmer specifies how the clients are coordinated. A type checker (compiler) implicitly updates each object's type and each type mark for each message accepting action and message sending action found while walking through the code and ensures statically that \begin{itemize} \item each object can deal with all message sequences specified by the object's type; \item the type mark of the first reference to each new object corresponds to the new object's type; \item type marks are split appropriately when new aliases are introduced; \item each message sequence sent to an object via a reference is specified by the type mark of this reference. \end{itemize} In a type-conforming program, all objects can deal properly with all received messages. There are no ``message-not-understood-errors'', unintended behaviors or deadlocks caused by wrong messages or wrong message orders. (The type system cannot prevent all kinds of deadlocks. But it can prevent that an object blocks with a nonempty message queue, waiting for messages not in the queue.) Most strongly typed object-oriented programming languages used in practice (C++, Java, Eiffel, etc.)\ apply name-based type equivalence and subtyping. Type names reflect the intended behavior and usage of the types' instances. Structural types and structural subtyping are applied less frequently in practice, although they could be used in a more flexible way. Because of this observation the author thinks that it is more important for process types to be expressive in specifying acceptable message sequences than it is to provide very general notions of type equivalence. Therefore, stricter notions of type equivalence and subtyping than equivalence or containment of message sequence sets are used. \section{The Computation Model} \label{model} \rsec{notation} contains an introduction to some notation and the syntax of the proposed calculus, and an informal description of its semantics. Examples in \rsec{examples} demonstrate the use of types in the calculus. Several type equivalence relations and the subtyping relation are introduced in \rsec{typing}. Message sequences specified by types and some properties of the type system are discussed in \rsec{sequences}. Deterministic types and their properties are the topic of \rsec{deterministic}. The operational (dynamic) semantics of the calculus are formally defined in \rsec{semantics}. \subsection{Notation and Syntax} \label{notation} An infinite set $\mathbb{V}$ of names (denoted by $u,v,w,\dots$) and a set $\mathbb{C}$ of constant symbols ($x,y,z,\dots$) with $\mathbb{V}\cap\mathbb{C}=\emptyset$ are considered given. Constant symbols are used as message selectors and in types to specify states. Names are used as parameters and object identifiers. Parameters are underlined if they occur at positions where free types, nonnegative integers or object identifiers shall be substituted for them. An underlined occurrence of a name \emph{binds} all following occurrences of this name. A name is free in an expression $e$ if it is not bound in $e$; \free{e} denotes the set of all names occurring free in $e$, and \free{e_1,\dots,e_n} is an abbreviation of $\free{e_1}\cup\dots\cup\free{e_n}$. $\subst{e_1,\dots,e_n}{u_1,\dots,u_n}f$ denotes the simultaneous substitution of $e_i$ for all free occurrences of $u_i$ in $f$ for $i=1,\dots,n$, where the names $u_1,\dots,u_n$ are pairwise different. Following conventions to simplify the notation are used: For each symbol $e$, \gr{e} is an abbreviation of $e_1,\dots,e_n$ for an arbitrary $n$ with $n\ge0$. ($i,j,m,n,\dots$ always denote nonnegative integers.) For example, \gr{u} denotes a list of names $u_1,\dots,u_n$, and \gr{\tau} a list of types $\tau_1,\dots,\tau_n$ because $\tau$, possibly quoted or indexed, denotes a type; $\gr{\tau},\gr{u}$ is an abbreviation of $\tau_1,\dots,\tau_m,u_1,\dots,u_n$. (The symbols used in this article are listed in \rfig{symbols} at the end of the article.) Likewise, $\{\gr{e}\}$ denotes the smallest set containing $e_1,\dots,e_n$, and $\lvert\gr{e}\rvert$ the length of the sequence. For each binary operator~$\cdot$, $\gr{e}{\cdot}f$ stands for $e_1{\cdot}f,\dots,e_n{\cdot}f$, and $\gr{e}{\cdot}\gr{g}$ for $e_1{\cdot}g_1,\dots,e_n{\cdot}g_n$ ($\lvert\gr{e}\rvert=\lvert\gr{g}\rvert$). $\subst{\gr{e}}{\gr{u}}\gr{g}$ denotes the simultaneous substitution of $\gr{e}$ for all free occurrences of $\gr{u}$ in each expression in \gr{g} ($\lvert\gr{e}\rvert=\lvert\gr{u}\rvert$ and all names \gr{u} pairwise different). It is implicitly assumed that all names in an underlined parameter list \ulg{u} are pairwise different. The syntax of the expressions in the proposed calculus is given in \rfig{syntax}. The semantics of these expressions is described informally. A formal presentation is given in \rsec{semantics}. \emph{Processes} (denoted by $P,Q,R,\dots$) specify object behavior. An object behaving as a process of the form $\coll{\gr{A}}$ waits until there is a message in its message queue; then, depending on the first message in the queue, a \emph{guarded process} $A\in\{\gr{A}\}$ is selected. (Normal braces denote sets, while bold braces and bold square brackets are part of the syntax.) A guarded process of the form $\rcv{x}{\ulg{u}}.P$ is selectable if the first message in the queue is of the form $\msg{x}{\gr{\varphi},\gr{v}}$ with $\lvert\gr{u}\rvert=\lvert\gr{\varphi},\gr{v}\rvert$, where $x$ is the message selector and \lst{\gr{\varphi},\gr{v}} the list of arguments to be substituted for the parameters \gr{u}; $\subst{\gr{\varphi},\gr{v}}{\gr{u}}P$ is the behavior of the object after selecting this guarded process and removing the message from the queue. There are several kinds of arguments: \gr{\varphi} is a list of nonnegative integers and free types used as values of type parameters; these arguments may (partially) specify type marks and object types. And \gr{v} is a list of object identifiers. Nonnegative integer expressions and types together are denoted by $\varphi,\dots$, nonnegative integer expressions alone by $p,q,\dots$ Latter expressions are either nonnegative integers, parameters standing for integers, or functions that always evaluate to nonnegative integers. It is assumed that at least addition (with the usual semantics) is available, but there may be further functions also. $\mathbb{I}$ denotes the set of all nonnegative integer expressions. \begin{figure} \rule{\textwidth}{1pt} \[ \begin{array}{@{}r@{~\;}r@{~\;}l@{\qquad}l@{}} P & \isd & \coll{\gr{A}} \;\;\mid\;\; \snd{u}{\mu}.P \;\;\mid\;\; \cond{u{=}v}{P}{Q} \;\;\mid\;\; \cond{\sigma{\le}\tau}{\ul{u}.P}{Q} \;\;\mid\;\; \cond{p{\ge}q}{\ul{u}.P}{Q} \;\;\mid{} \\ & & \new{\ul{u}}{\class{\gr{A}}{\gr{\alpha}}}{\mu}.P \;\;\mid\;\; \new{\ul{u}}{v}{\mu}.P \;\;\mid\;\; \call{\mu} \\ A & \isd & \rcv{x}{\ulg{u}}.P \\ \mu & \isd & \msg{x}{\gr{\varphi},\gr{u}} \\ \varphi& \isd & p \;\;\mid\;\; \tau \\ p & \isd & n \;\;\mid\;\; u \;\;\mid\;\; p+q \\ \tau & \isd & \typ{\gr{\alpha}}{\gr{r}} \;\;\mid\;\; \rec{u}\typ{\gr{\alpha}}{\gr{r}} \;\;\mid\;\; \sigma\|\tau \;\;\mid\;\; u \\ \alpha & \isd & \beh{a}{\gr{r}}{\gr{s}} \;\;\mid\;\; \creat{a}{\gr{r}} \\ a & \isd & \sign{x}{\ulg{u}{:}\gr{\eta},\gr{\tau}} \\ \eta & \isd & \mtyp \;\;\mid\;\; \num \\ r & \isd & x^\infty \;\;\mid\;\; x^p \;\;\mid\;\; x^{[p]} \end{array} \] \rule{\textwidth}{1pt} \caption{Syntax} \label{syntax} \end{figure} Messages are denoted by $\mu,\nu,\xi,\dots$ An object behaving as a process of the form $\snd{u}{\mu}.P$ sends a message $\mu$ to an object with identifier $u$ and then behaves as $P$. A process \cond{u{=}v}{P}{Q} specifies the behavior $P$ if $u$ and $v$ are equal object identifiers, and $Q$ otherwise. A process \cond{\sigma{\le}\tau}{\ul{u}.P}{Q} (or \cond{p{\ge}q}{\ul{u}.P}{Q}) specifies the behavior $\subst{\rho}{u}P$ (or $\subst{q'}{u}P$) if $\sigma$ is a subtype of $\tau$, and $\rho$ the difference between $\sigma$ and $\tau$ (or $p$ and $q+q'$ evaluate to the same integer), and $Q$ otherwise. An object behaving as a process $\new{\ul{u}}{\class{\gr{A}}{\gr{\alpha}}}{\mu}.P$ creates a new object with identifier $u$ and then behaves as $P$. For simplicity of the model it is assumed that, except of the self reference $u$, object identifiers and object parameters do not occur free in \coll{\gr{A}}. The new object behaves as \coll{\gr{A}}, where the first message in the message queue is $\mu$. \coll{\gr{\alpha}} and $\mu$ together specify the type mark of $u$ and the type of the new object. An object behaving as $\new{\ul{u}}{v}{\mu}.P$ also creates a new object with identifier $u$ and then behaves as $P$. The behavior of the new object is equal to the behavior of the object with identifier $v$ at the time when it was created; $u$ becomes a clone of $v$. The first message in the message queue of the new object is $\mu$. The new behavior of an object behaving as \call{\mu} becomes that of the object at the time when it was created with $\mu$ inserted as the first message in the message queue; the other messages remain in the queue. \emph{Types} are denoted by $\pi,\rho,\sigma,\tau,\dots$ A type of the form \typ{\gr{\alpha}}{\gr{r}} consists of a set of (message and creator) descriptors \gr{\alpha}---the static part---and a state \mset{\gr{r}}---the dynamic part. Each \emph{token} (denoted by $r,s,t,\dots$) in a state is of the form $x^p$, $x^\infty$ or $x^{[q]}$, where $x$ is the token symbol and $p$ or $\infty$ the multiplication factor, and $q$ specifies the part size (see below). \mset{\gr{r}} can be regarded as a multi-set of $p$ token symbols $x$ for each $x^p\in\{\gr{r}\}$ and an infinite number of $x$ for each $x^\infty\in\{\gr{r}\}$. Tokens of the form $x^{[q]}$ specify that the sequence of acceptable messages may depend on the exact number of token symbols $x$ in a state---not just the minimum number---and the state contains about the $1/2^q$ part of all token symbols $x$ to be considered; the state has been split $q$ times, each time into two parts. The state contains all token symbols $x$ to be considered if $x^{[0]}$ is in the state. Each \emph{message descriptor} is of the form \beh{a}{\gr{s}}{\gr{t}}, where $a$ is the signature of a message, \mset{\gr{s}} the \emph{in-set} and \mset{\gr{t}} the \emph{out-set}. A message of signature $a$ is acceptable if each token in the in-set occurs in the type's state \mset{\gr{r}} and, for each token $x^{[0]}$ in the in-set, no further token with token symbol $x$ occurs in \mset{\gr{r}}; the type is updated according to this message by removing all tokens in the in-set from the state, and adding all tokens in the out-set to the state. Tokens of the form $x^{[p]}$ with $p\neq0$ must not occur in in-sets and out-sets; they can occur only in states. A token of the form $x^{[0]}$ can occur in the out-set only if it occurs also in the in-set. A \emph{creator descriptor} in \coll{\gr{\alpha}} is of the form \creat{a}{\gr{s}}, where $a$ is the message signature of the creator and \mset{\gr{s}} the initial state; a new object receiving a message of signature $a$ as creator message has the initial type \typ{\gr{\alpha}}{\gr{s}}. Tokens of the form $x^{[p]}$ can occur in initial states only with $p=0$. Descriptors are denoted by $\alpha,\beta,\gamma,\dots$ A \emph{message signature} (denoted by $a,b,c,\dots$) is of the form \sign{x}{\ulg{u}{:}\gr{\eta},\gr{\tau}}, where $x$ is the message selector, the \gr{u} are type and integer parameters, the \gr{\eta} meta-types ($\lvert\gr{u}\rvert=\lvert\gr{\eta}\rvert$) and the \gr{\tau} types of object parameters; the \gr{u} can occur in the \gr{\tau}. Meta-types (denoted by $\eta,\dots$) are ``\mtyp'', the type of all type expressions, and ``\num'', the type of all nonnegative integers. A type of the form $\rec{u}\typ{\gr{\alpha}}{\gr{r}}$ is a recursive version of a type. The type parameter $u$ can (recursively) occur in the message signatures in \gr{\alpha}. A name $u$ used as type parameter can occur in each position where a type can occur. A type of the form $\sigma\|\tau$ denotes the combination of two types, $\sigma$ and $\tau$; $\sigma\|\tau$ can be split into $\sigma$ and $\tau$. \subsection{Examples of Types and Processes} \label{examples} The use of the type system is demonstrated with some examples. The type of a simple displayed window as used in \rsec{problem} can be expressed by \textit{Win}\mset{\text{displ}^1}, where the static part of the type is: % \[ \textit{Win}\,\stackrel{\text{\tiny def}}{=} \coll{\beh{\sign{\text{iconify}}{}}{\text{displ}^1}{\text{icon}^1},\, \beh{\sign{\text{uniconify}}{}}{\text{icon}^1}{\text{displ}^1}} \] % The messages ``iconify'' and ``uniconify'' are acceptable only if the state contains displ$^1$ and icon$^1$, respectively. An object of type \textit{Win}\mset{\text{displ}^1} first accepts ``iconify'', then ``un\-iconify'', then ``iconify'' again, and so on. Thereby, the type is updated to \textit{Win}\mset{\text{icon}^1}, then \textit{Win}\mset{\text{displ}^1} again, and so on. Windows usually understand further messages like ``move'' to change the location of the displayed window or icon, and ``redisplay'' to redisplay the possibly scrambled contents of the displayed window. A window with these extensions can have the type % \[ \textit{Win}\,\mset{\text{displ}^1}\,\|\, \typ{\beh{\sign{\text{move}}{\textit{Location}}}{}{},\, \beh{\sign{\text{redisplay}}{}}{\text{displ}^1}{\text{displ}^1}}{} \] % where \textit{Location} is the type of an object specifying the location on a screen. The message ``move'' is accepted in arbitrary interleaving with the other messages. But ``redisplay'' is accepted only if the window is displayed. A client with a reference of type mark \textit{Win}\mset{\text{displ}^1} can send ``iconify'' and ``uniconify'' (in alternation) to the window. A client with a reference of a type mark equal to the type at the right of ``$\|$'' can send only ``move'' because the state known by the client does not contain displ$^1$; ``redisplay'' can be sent only if the type mark is the combination of the two types. The next example shows the static part of the type of a simple heterogeneous buffer: % \begin{align*} \textit{Buf}\, &\stackrel{\text{\tiny def}}{=} \coll{\beh{\sign{\text{put}}{\ul{u}{:}\mtyp,u}}{\text{empty}^1 }{\text{full}^1},\, \beh{\sign{\text{get}}{\textit{Back}\,\mset{\text{one}^1}} }{\text{full}^1}{\text{empty}^1}} \\ \textit{Back}\, &\stackrel{\text{\tiny def}}{=} \coll{\beh{\sign{\text{back}}{\ul{u}{:}\mtyp,u}}{\text{one}^1}{}} \end{align*} % A message ``put'' is accepted if a buffer slot is empty, and ``get'' if a slot is full; the empty slot becomes full, and the full slot empty. ``Put'' has two parameters, a type parameter $u$ and an object parameter; an object reference with a type mark equal to the free type provided as first argument is expected as second argument. ``Get'' expects as argument a reference to an object accepting a single message ``back''; it is assumed that the contents of a buffer slot as well as its type are provided as arguments of ``back''. \textit{Buf}\mset{\text{empty}^1} is the type of an empty buffer with a single slot, \textit{Buf}\mset{\text{empty}^{50}} that of an empty buffer with fifty slots, and \textit{Buf}\mset{\text{empty}^\infty} that of an empty buffer with an unlimited number of slots. The behavior partially specified by the last type is specified also by \textit{BufI}\mset{} with: % \[ \textit{BufI}\, \stackrel{\text{\tiny def}}{=} \coll{\beh{\sign{\text{put}}{\ul{u}{:}\mtyp,u}}{}{\text{full}^1},\, \beh{\sign{\text{get}}{\textit{Back}\,\mset{\text{one}^1}}}{ \text{full}^1}{}} \] % An object of this type always accepts ``put'', but ``get'' only if there is a full slot. Objects of the types \textit{BufI}\mset{\text{full}^\infty} and \textit{Buf}\mset{\text{empty}^\infty,\text{full}^\infty} accept ``put'' and ``get'' in arbitrary ordering. Extensions of the buffer types, \textit{BufID}\mset{\text{ok}^{[0]},\text{ok}^\infty} and \textit{BufD}\mset{\text{empty}^{50},\text{ok}^{[0]},\text{ok}^\infty}, allow clients to explicitly delete buffers by sending a message ``del'' so that the buffers stop to accept any further messages: % \begin{align*} \textit{BufID}\, &\stackrel{\text{\tiny def}}{=} \coll{\beh{\sign{\text{put}}{\ul{u}{:}\mtyp,u}}{\text{ok}^1 }{\text{full}^1},\, \beh{\sign{\text{get}}{\textit{Back}\,\mset{\text{one}^1}} }{\text{ok}^1,\text{full}^1}{},\, \beh{\sign{\text{del}}{}}{\text{ok}^{[0]},\text{ok}^\infty}{}} \\ \textit{BufD}\, &\stackrel{\text{\tiny def}}{=} \boldsymbol{\{} \begin{array}[t]{@{}l@{}} \beh{\sign{\text{put}}{\ul{u}{:}\mtyp,u}}{\text{ok}^1,\text{empty}^1 }{\text{full}^1}, \\ \beh{\sign{\text{get}}{\textit{Back}\,\mset{\text{one}^1}} }{\text{ok}^1,\text{full}^1}{\text{empty}^1},\, \beh{\sign{\text{del}}{}}{\text{ok}^{[0]},\text{ok}^\infty}{} \boldsymbol{\}} \end{array} \end{align*} % The token $\text{ok}^\infty$ is present in a type's state as long as the buffer of this type is alive; the token is removed when ``del'' is accepted. Because of the token $\text{ok}^{[0]}$ in the in-set, ``del'' can be sent only if there is no other reference to the buffer with a token $\text{ok}^p$ in the type mark's state. Sometimes a more homogeneous buffer is needed, where all elements in the buffer are subtypes of a given type. \textit{BufIB}\mset{} is the type of such an empty buffer; all object references in this buffer must have a subtype of \textit{Buf}\mset{\text{empty}^1} as type mark: % \[ \textit{BufIB}\, \stackrel{\text{\tiny def}}{=} \coll{\beh{\sign{\text{put}}{\ul{u}{:}\mtyp,\textit{Buf}\, \mset{\text{empty}^1}\|u}}{}{\text{full}^1},\, \beh{\sign{\text{get}}{\textit{Back}\,\mset{\text{one}^1}}}{ \text{full}^1}{}} \] % The type parameter $u$ specifies the difference between the type mark of the object reference and \textit{Buf}\mset{\text{empty}^1}. Using recursion it can be required that object references in the buffer have a subtype of the buffer type itself as type mark: % \[ \rec{u}\typ{\beh{\sign{\text{put}}{\ul{v}{:}\mtyp,u\|v}}{}{\text{full}^1},\, \beh{\sign{\text{get}}{\textit{Back}\,\mset{\text{one}^1}}}{ \text{full}^1}{}}{} \] % Before type updating, this type must be transformed into an equivalent type not containing recursion at the outermost level. Usually, type marks need not contain creator descriptors. However, each object's type---being a subtype of the type mark of each reference to the object---must contain at least one creator descriptor. Otherwise it would have been impossible to create the object. Types of many objects contain even several creator descriptors. These descriptors specify the signatures of ``procedures'' that can be called (recursively) to specify the object's behavior. For example, \textit{BufIDC} is the static part of a type who's instances are created by the messages ``init'' or ``buf'' and accept ``put'' and ``get'' in arbitrary order until accepting ``del'': % \[ \textit{BufIDC}\, \stackrel{\text{\tiny def}}{=} \boldsymbol{\{} \begin{array}[t]{@{}l@{}} \beh{\sign{\text{put}}{\ul{u}{:}\mtyp,u}}{\text{ok}^1}{\text{full}^1},\, \beh{\sign{\text{get}}{\textit{Back}\,\mset{\text{one}^1}} }{\text{ok}^1,\text{full}^1}{},\, \beh{\sign{\text{del}}{}}{\text{ok}^{[0]},\text{ok}^\infty}{}, \\ \creat{\sign{\text{init}}{}}{\text{ok}^{[0]},\text{ok}^\infty}, \\ \creat{\sign{\text{buf}}{\ul{u}{:}\num,\ul{v}{:}\mtyp, \textit{BufID}\,\mset{\text{full}^u,\text{ok}^{[0]}, \text{ok}^\infty},v} }{\text{full}^{u+1},\text{ok}^{[0]},\text{ok}^\infty} \boldsymbol{\}} \end{array} \] % \textit{BufIDC} can be used in a process $\new{\ul{u}}{\coll{A_1,A_2}{:}\textit{BufIDC}}{\msg{\text{init}}{}}.P$, where % \begin{align*} A_1 &\stackrel{\text{\tiny def}}{=} \rcv{\text{init}}{}.\coll{ \rcv{\text{put}}{\ul{v},\ul{w}}. \new{\ul{u}'}{u}{\msg{\text{init}}{}}. \call{\msg{\text{buf}}{0,v,u',w}},\; \rcv{\text{del}}{}. \coll{}} \\ A_2 &\stackrel{\text{\tiny def}}{=} \rcv{\text{buf}}{\ul{u}'',\ul{v},\ul{u}',\ul{w}}.\boldsymbol{\{} \begin{array}[t]{@{}l@{}} \rcv{\text{put}}{\ul{v}',\ul{w}'}. \snd{u'}{\msg{\text{put}}{v',w'}}. \call{\msg{\text{buf}}{u''+1,v,u',w}}, \\ \rcv{\text{get}}{\ul{v}'}. u''{\ge}1\,?\, \begin{array}[t]{@{}l@{}} \ul{w}'. \snd{u'}{\msg{\text{get}}{v'}}. \call{\msg{\text{buf}}{w',v,u',w}}\,| \\ \snd{v'}{\msg{\text{back}}{v,w}}. \snd{u'}{\msg{\text{del}}{}}. \call{\msg{\text{init}}{}}, \end{array} \\ \rcv{\text{del}}{}. \snd{u'}{\msg{\text{del}}{}}. \coll{} \boldsymbol{\}} \end{array} \end{align*} % The buffer of identifier $u$ stores data in a simple linear list. Initially, the buffer behaves as $A_1$; there are no data in the buffer. The behavior changes to $A_2$ after accepting ``put''. The first parameter of ``buf'' specifies the number of data items in the rest of the list (i.\,e.\ the number of data items in the buffer minus one), the third parameter specifies the rest of the list. When ``get'' is accepted, the message is forwarded to the next element in the list if there are data items in the rest of the list; otherwise the data in the first element are sent to the argument of ``get''. ``Del'' is sent to list elements when they are no longer needed. \begin{figure} \rule{\textwidth}{1pt} \begin{align*} \textit{Fork} &\stackrel{\text{\tiny def}}{=} \coll{\beh{\sign{\text{take}}{}}{\text{down}^1}{\text{up}^1},\, \beh{\sign{\text{put\_down}}{}}{\text{up}^1}{\text{down}^1},\, \creat{\sign{\text{rec}}{}}{\text{down}^1}} \\ \textit{Phil} &\stackrel{\text{\tiny def}}{=} \lcb \begin{array}[t]{@{}l@{}l@{}} \beh{\sign{\text{ask}}{\textit{Phil}\,\mset{\text{hungry}^1}}}{}{},\, \beh{\sign{\text{yes}}{\textit{Phil}\,\mset{\text{nice}^1},\textit{Fork}\,\mset{\text{down}^1}}}{\text{hungry}^1}{},\\ \beh{\sign{\text{no}}{}}{\text{hungry}^1}{},\, \beh{\sign{\text{back}}{\textit{Fork}\,\mset{\text{down}^1}}}{\text{nice}^1}{} & \rcb \end{array} \\ \textit{Break} &\stackrel{\text{\tiny def}}{=} \coll{\beh{\sign{\text{break}}{}}{\text{br}^1}{\text{br}^1}} \\ \textit{PhilC} &\stackrel{\text{\tiny def}}{=} \lcb \begin{array}[t]{@{}l@{}l@{}} \beh{\sign{\text{ask}}{\textit{Phil}\,\mset{\text{hungry}^1}}}{}{},\, \beh{\sign{\text{yes}}{\textit{Phil}\,\mset{\text{nice}^1},\textit{Fork}\,\mset{\text{down}^1}}}{\text{hungry}^1}{},\\ \beh{\sign{\text{no}}{}}{\text{hungry}^1}{},\, \beh{\sign{\text{back}}{\textit{Fork}\,\mset{\text{down}^1}}}{\text{nice}^1}{},\, \beh{\sign{\text{init}}{\textit{Phil}\,\mset{}}}{\text{new}^1}{},\\ \beh{\sign{\text{break}}{}}{\text{br}^1}{\text{br}^1},\, \creat{\sign{\text{new}}{}}{\text{new}^1},\, \creat{\sign{\text{think}}{\textit{Phil}\,\mset{},\textit{Fork}\,\mset{\text{down}^1}}}{\text{br}^1},\\ \creat{\sign{\text{hungry}}{\textit{Phil}\,\mset{},\textit{Fork}\,\mset{\text{down}^1}}}{\text{br}^1,\text{hungry}^1},\, \creat{\sign{\text{nice}}{\textit{Phil}\,\mset{}}}{\text{br}^1,\text{nice}^1},\\ \creat{\sign{\text{eat}}{\textit{Phil}\,\mset{\text{nice}^1},\textit{Fork}\,\mset{\text{up}^1},\textit{Fork}\,\mset{\text{up}^1}}}{\text{br}^1} & \rcb \end{array} \\ P_{\text{phil}} &\stackrel{\text{\tiny def}}{=} \begin{array}[t]{@{}l@{}} \new{\ul{u}}{\coll{A_1,\dots,A_5}{:}\textit{PhilC}}{\msg{\text{new}}{}}. \\ \new{\ul{u}_2}{u}{\msg{\text{new}}{}}.\new{\ul{u}_3}{u}{\msg{\text{new}}{}}.\new{\ul{u}_4}{u}{\msg{\text{new}}{}}.\new{\ul{u}_5}{u}{\msg{\text{new}}{}}. \\ \snd{u}{\msg{\text{init}}{u_2}}.\snd{u_2}{\msg{\text{init}}{u_3}}.\snd{u_3}{\msg{\text{init}}{u_4}}.\snd{u_4}{\msg{\text{init}}{u_5}}.\snd{u_5}{\msg{\text{init}}{u}}.\coll{} \end{array} \\ A_1 &\stackrel{\text{\tiny def}}{=} \rcv{\text{new}}{}.\lcb \begin{array}[t]{@{}l@{}} \rcv{\text{ask}}{\ul{v}'}.\snd{v'}{\msg{\text{no}}{}}.\call{\msg{\text{new}}{}}, \\ \rcv{\text{init}}{\ul{v}}. \begin{array}[t]{@{}l@{}l@{}} \new{\ul{u}'}{\coll{\rcv{\text{rec}}{\ul{u}}.\snd{u}{\msg{\text{break}}{}}.\call{\msg{\text{rec}}{u}}}{:}\coll{\creat{\msg{\text{rec}}{\textit{Break}\,\mset{\text{br}^1}}}{}}}{\msg{\text{rec}}{u}}. \\ \new{\ul{w}}{\coll{\rcv{\text{rec}}{}.\coll{\rcv{\text{take}}{}.\coll{\rcv{\text{put\_down}}{}.\call{\msg{\text{rec}}{}}}}}{:}{\textit{Fork}}}{\msg{\text{rec}}{}}. \\ \call{\msg{\text{think}}{v,w}} & \rcb \end{array} \end{array} \\ A_2 &\stackrel{\text{\tiny def}}{=} \rcv{\text{think}}{\ul{v},\ul{w}}.\coll{\rcv{\text{ask}}{\ul{v'}}.\snd{v'}{\msg{\text{yes}}{u,w}}.\call{\msg{\text{nice}}{v}},\, \rcv{\text{break}}{}.\snd{v}{\msg{\text{ask}}{u}}.\call{\msg{\text{hungry}}{v,w}}} \\ A_3 &\stackrel{\text{\tiny def}}{=} \rcv{\text{nice}}{\ul{v}}.\coll{\rcv{\text{ask}}{\ul{v'}}.\snd{v'}{\msg{\text{no}}{}}.\call{\msg{\text{nice}}{v}},\,\rcv{\text{break}}{}.\call{\msg{\text{nice}}{v}},\, \rcv{\text{back}}{w}.\call{\msg{\text{think}}{v,w}}} \\ A_4 &\stackrel{\text{\tiny def}}{=} \rcv{\text{hungry}}{\ul{v},\ul{w}}.\lcb \begin{array}[t]{@{}l@{}l@{}} \rcv{\text{ask}}{\ul{v'}}.\snd{v'}{\msg{\text{no}}{}}.\call{\msg{\text{hungry}}{v,w}},\,\rcv{\text{break}}{}.\call{\msg{\text{hungry}}{v,w}}, \\ \rcv{\text{yes}}{\ul{v},\ul{w}'}.\snd{w}{\msg{\text{take}}{}}.\snd{w'}{\msg{\text{take}}{}}.\call{\msg{\text{eat}}{v,w,w'}},\,\rcv{\text{no}}{}.\call{\msg{\text{think}}{v,w}} & \rcb \end{array} \\ A_5 &\stackrel{\text{\tiny def}}{=} \rcv{\text{eat}}{\ul{v},\ul{w},\ul{w}'}.\lcb \begin{array}[t]{@{}l@{}l@{}} \rcv{\text{ask}}{\ul{v'}}.\snd{v'}{\msg{\text{no}}{}}.\call{\msg{\text{eat}}{v,w,w'}}, \\ \rcv{\text{break}}{}.\snd{w}{\msg{\text{put\_down}}{}}.\snd{w'}{\msg{\text{put\_down}}{}}.\snd{v}{\msg{\text{back}}{w'}}.\call{\msg{\text{think}}{v,w}} & \rcb \end{array} \end{align*} \rule{\textwidth}{1pt} \caption{Example: Dining Philosophers} \label{phil} \end{figure} The example in \rfig{phil} shows a solution of the dining philosophers problem. $P_{\text{phil}}$ is a process that creates five philosophers. Each philosopher sitting on a table always is in one of five states: new (not yet initialized, i.\,e., not yet having a fork and not knowing his right neighbor), thinking, being hungry (asking his right neighbor for a fork), being nice (giving his fork to his left neighbor) and eating with two forks (his own and a borrowed one). The acceptable messages depend on the state. A fork can be in two states: down on the table or up in a philosopher's hand. When asked for a fork, a thinking philosopher can give his fork to a neighbor by sending ``yes'' to the philosopher who asked. (Name $u$ identifies the philosopher itself, $v$ his right neighbor, $v'$ his left neighbor who asks for the fork, $w$ the own fork and $w'$ a borrowed fork.) When a philosopher becomes hungry (after receiving ``break''), he sends ``ask'' to his right neighbor. All further requests for a fork are answered with ``no''. A nice philosopher waits for the message ``back'' from his left neighbor returning the fork, and then continues with thinking. A hungry philosopher waits for an answer from his right neighbor. If the answer is ``no'', he continues with thinking. Otherwise he takes his and his neighbor's fork and begins to eat. When he is no longer hungry (after receiving ``break''), he puts the forks on the table, returns one of them to his neighbor and begins to think again. On initialization, each philosopher gets associated with an object $u'$ that repeatedly sends ``break'' to him. The example shows that parameter types (i.\,e., type marks of parameters) can be supertypes of the corresponding arguments' type marks. As shown later, \textit{Phil}\mset{} and \textit{Break}\mset{\text{br}^1} are supertypes of \textit{PhilC}\mset{\text{br}^1}. The concept of dynamically and implicitly extending a self reference's type mark is explained in \rsec{rules}: In the above example, the type mark of the self reference $u$ is extended by adding br$^1$, hungry$^1$ and nice$^1$ to its state before creating the object $u'$, sending ``ask'' to the right neighbor and sending ``yes'' to the left neighbor, respectively. A final example demonstrates the expressiveness of types. An object of the type % \[ \lcb \begin{array}[t]{@{}l@{}} \beh{a_1}{x_1^1}{x_1^1,y^1},\, \beh{a_2}{x_1^1,x_2^{[0]},y^1}{x_2^1,y^1,z^1},\, \beh{a_2}{x_2^1}{x_2^1,z^1}, \\ \beh{a_3}{x_2^1,x_3^{[0]},y^1}{x_3^1},\, \beh{a_3}{x_3^1,y^1}{x_3^1},\, \beh{a_4}{x_3^1,y^{[0]},z^1}{x_3^1,y^{[0]}} \rcb \mset{x_1^1,x_2^{[0]},x_3^{[0]},y^{[0]}} \end{array} \] % first accepts $n>0$ messages of the signature $a_1$, then $m>0$ messages of the signature $a_2$, then $n$ messages of the signature $a_3$, and finally $m$ messages of the signature $a_4$. Using regular grammars and LR(k) grammars it is not possible to specify words of the form $a_1^na_2^ma_3^na_4^m$. \subsection{Equivalence and Subtyping} \label{typing} From the informal description of the syntax it shall be clear that expressions of the form \coll{\gr{e}} denote the smallest sets containing \gr{e}, and expressions of the form \mset{\gr{r}} denote essentially multi-sets of token symbols. Expressions can be regarded as equivalent if they denote the same sets or multi-sets. Furthermore, names of parameters have no semantic relevance; they can be renamed as long as name conflicts are avoided. As in the $\lambda$-calculus, such renaming is called $\alpha$-conversion. \begin{definition} \label{def:eqv} \upshape The equivalence relation $e\equiv f$ on all expressions corresponding to the syntax given in \rfig{syntax} is the least congruence closed under the rules: \begin{alignat*}{3} \coll{\gr{e},f,\gr{g}} &\equiv \coll{\gr{e},\gr{g},f} &\qquad \coll{\gr{e},f} &\equiv \coll{\gr{e},f,f} &\qquad e &\equiv f \ \text{ ($e$ $\alpha$-convertible to $f$)} \\ \mset{\gr{r},t,\gr{s}} &\equiv \mset{\gr{r},\gr{s},t} &\qquad \mset{\gr{r},x^{p+q}} &\equiv \mset{\gr{r},x^p,x^q} &\qquad \mset{\gr{r}} &\equiv \mset{\gr{r},x^0} \\ \mset{\gr{r},x^\infty} &\equiv \mset{\gr{r},x^\infty,x^\infty} &\qquad \mset{\gr{r},x^\infty} &\equiv \mset{\gr{r},x^\infty,x^p} &\qquad \mset{\gr{r},x^{[p]}} &\equiv \mset{\gr{r},x^{[p+1]},x^{[p+1]}} \\ p &\equiv q \quad \makebox[0em][l]{($p$ and $q$ can be evaluated to the same expression)} \end{alignat*} \end{definition} Much richer equivalence relations can be defined on type expressions. The set \relevant{\gr{\alpha}} aids these definitions; it contains all effective tokens in the static part \coll{\gr{\alpha}} of a type: % \begin{align*} \relevant{} &= \emptyset \\ \relevant{\gr{\alpha},\beh{a}{}{\gr{s}}} &= \relevant{\gr{\alpha}} \\ \relevant{\gr{\alpha},\beh{a}{\gr{r},x^p}{\gr{s}}} &= \{x^{[q]},x^{q'},x^\infty\mid q,q'\in\mathbb{I}\}\cup \relevant{\gr{\alpha},\beh{a}{\gr{r}}{\gr{s}}} \\ \relevant{\gr{\alpha},\beh{a}{\gr{r},x^\infty}{\gr{s}}} &= \{x^{[q]},x^\infty\mid q\in\mathbb{I}\}\cup \relevant{\gr{\alpha},\beh{a}{\gr{r}}{\gr{s}}} \quad (x^{[0]}\notin\{\gr{r}\}) \\ \relevant{\gr{\alpha},\beh{a}{\gr{r},x^{[0]}}{\gr{s}}} &= \{x^{[p]},x^q,x^\infty\mid p,q\in\mathbb{I}\}\cup \relevant{\gr{\alpha},\beh{a}{\gr{r}}{\gr{s}}} \quad (x^\infty\notin\{\gr{r}\}) \\ \relevant{\gr{\alpha},\beh{a}{\gr{r},x^{[0]},x^\infty}{\gr{s}}} &= \{x^{[p]},x^\infty\mid p\in\mathbb{I}\}\cup \relevant{\gr{\alpha},\beh{a}{\gr{r}}{\gr{s}}} \\ \relevant{\gr{\alpha},\creat{a}{\gr{s}}} &= \relevant{\gr{\alpha}} \end{align*} % A token is effective in \coll{\gr{\alpha}} if the presence of this token in a state \mset{\gr{r}} may contribute to the acceptability of a message by an object of type \typ{\gr{\alpha}}{\gr{r}}. A token of the form $x^\infty$ or $x^{[p]}$ is effective if any token with token symbol $x$ occurs in the in-set of a message descriptor; a token $x^p$ is effective only if a token $x^q$ or $x^{[0]}$ (not in combination with $x^\infty$) occurs in an in-set. The function \textit{eff} computes a conservative approximation: Some tokens do not contribute to the acceptability of a message, although they occur in \relevant{\gr{\alpha}}. Tokens not occurring in \relevant{\gr{\alpha}} are always non-effective; they have no semantic meaning. \begin{definition} \label{equiv-rel} \upshape The \emph{strong type equivalence} relation $\sigma\equiv_{\text{t}}\tau$ on types is the least congruence closed under the rules in \rfig{equiv}. \end{definition} \begin{figure} \rule{\textwidth}{1pt} \begin{align} \sigma &\equiv_{\text{t}} \tau \quad (\sigma\equiv\tau) \tag{eq$_{\cong}$} \\ \rec{u}\typ{\gr{\alpha}}{\gr{r}} &\equiv_{\text{t}} \subst{\rec{u}\typ{\gr{\alpha}}{\gr{r}}}{u}\typ{\gr{\alpha}}{\gr{r}} \tag{rec$_{\cong}$} \\ (\rho\|\sigma)\|\tau &\equiv_{\text{t}} \rho\|(\sigma\|\tau) \tag{assoc$_{\cong}$} \\ \sigma\|\tau &\equiv_{\text{t}} \tau\|\sigma \tag{comm$_{\cong}$} \\ \tau &\equiv_{\text{t}} \tau\|\typ{}{} \tag{zero$_{\cong}$} \\ \typ{\gr{\alpha},\gr{\gamma}}{\gr{r},\gr{s}} &\equiv_{\text{t}} \typ{\gr{\alpha}}{\gr{r}}\|\typ{\gr{\gamma}}{\gr{s}} \quad (1) \tag{comb$_{\cong}$} \\ \typ{\gr{\alpha}}{\gr{r}} &\equiv_{\text{t}} \typ{\gr{\alpha}}{\gr{r},s} \quad (s\notin\relevant{\gr{\alpha}}) \tag{state$_{\cong}$} \end{align} (1)\quad $ \begin{array}[t]{@{}l@{\ }l} \gr{r}\in\relevant{\gr{\alpha}}; & \forall_{x,p}\,x^{[p]}\in\{\gr{r}\}\,\Rightarrow\, (x^{[0]}\notin\relevant{\gr{\gamma}}\,\vee\, \exists_{q}\,x^{[q]}\in\{\gr{s}\}); \\ \gr{s}\in\relevant{\gr{\gamma}}; & \forall_{x,p}\,x^{[p]}\in\{\gr{s}\}\,\Rightarrow\, (x^{[0]}\notin\relevant{\gr{\alpha}}\,\vee\, \exists_{q}\,x^{[q]}\in\{\gr{r}\}) \end{array} $ \\[2ex] \rule{\textwidth}{1pt} \caption{Strong Type Equivalence} \label{equiv} \end{figure} Rule (rec$_{\cong}$) in \rfig{equiv} deals with folding and unfolding recursive types. An important special case of this rule is $\rec{u}\typ{\gr{\alpha}}{\gr{r}}\equiv_{\text{t}}\typ{\gr{\alpha}}{\gr{r}}$ if $u\notin\free{\typ{\gr{\alpha}}{\gr{r}}}$. Similar rules for recursive types are frequently used in the literature~\cite{AmCa91}. Type combination is an associative, commutative operation with the empty type \typ{}{} as neutral element. As specified by (comb$_{\cong}$), two types of the forms \typ{\gr{\alpha}}{\gr{r}} and \typ{\gr{\gamma}}{\gr{s}} are combined to \typ{\gr{\alpha},\gr{\gamma}}{\gr{r},\gr{s}} by building the unions of the sets of descriptors and the multi-sets of tokens. The rule (state$_{\cong}$) specifies that non-effective tokens can be added to and removed from states. The side-condition of (comb$_{\cong}$) ensures that this rule together with (state$_{\cong}$) cannot be used for introducing arbitrary effective tokens into the state of a type. Furthermore, the side-condition ensures that, if a token of the form $x^{[p]}$ occurs in \mset{\gr{r},\gr{s}}, tokens of this form (possibly with different part sizes $p$) occur in both, \mset{\gr{r}} and \mset{\gr{s}}, or these tokens are not effective in one of the types. When a type containing $x^{[p]}$ in the state is split such that $x^{[p]}$ is effective in both, \coll{\gr{\alpha}} and \coll{\gr{\gamma}}, the information about part sizes has to be updated so that both, \mset{\gr{r}} and \mset{\gr{s}}, contain $x^{[p+1]}$. A token $x^{[0]}$ in an in-set specifies that a corresponding message is acceptable only if $x^{[0]}$ and a certain number of token symbols $x$ is in the state. The message is not acceptable if the state contains only $x^{[p]}$ with $p\neq0$. Type combination reintroduces $x^{[p]}$ into the state if \mset{\gr{r}} as well as \mset{\gr{s}} contains $x^{[p+1]}$. In the window example in \rsec{examples}, a single application of (comb$_{\cong}$) derives: % \[ \begin{array}{@{}l@{}} \textit{Win}\,\mset{\text{displ}^1}\,\|\, \typ{\beh{\sign{\text{move}}{\textit{Location}}}{}{},\, \beh{\sign{\text{redisplay}}{}}{\text{displ}^1}{\text{displ}^1}}{}\\ \qquad{}\equiv_{\text{t}}\,\lcb \begin{array}[t]{@{}l@{}l@{}} \beh{\sign{\text{iconify}}{}}{\text{displ}^1}{\text{icon}^1},\, \beh{\sign{\text{uniconify}}{}}{\text{icon}^1}{\text{displ}^1}, \\ \beh{\sign{\text{move}}{\textit{Location}}}{}{},\, \beh{\sign{\text{redisplay}}{}}{\text{displ}^1}{\text{displ}^1} & \rcb\mset{\text{displ}^1} \end{array} \end{array} \] A special case of (comb$_{\cong}$) used together with (eq$_{\cong}$) is $\typ{\gr{\alpha}}{\gr{r},\gr{s}}\equiv_{\text{t}}\typ{\gr{\alpha}}{\gr{r}} \|\typ{\gr{\alpha}}{\gr{s}}$, where \gr{r} and \gr{s} satisfy the side-condition of (comb$_{\cong}$). Each state of a type can be split into two states satisfying the side-condition; for each state splitting, the type is easily split into two types such that the split types have the same static part as the combined type. This kind of type splitting will be used frequently when checking type safety. Strong type equivalence is useful in specifying the semantics of types. However, a less strict notion of type equivalence is needed as basis of subtyping. \begin{definition} \label{def:weak} \upshape The \emph{weak type equivalence} relation $\Pi\vdash\sigma\cong\tau$ on types is the least congruence closed under the rules in \rfig{equiv} (with all expressions of the form $\sigma\equiv_{\text{t}}\tau$ replaced by $\Pi\vdash\sigma\cong\tau$) and the rule \begin{align} \Pi\vdash\rec{u}\typ{\gr{\alpha},\gr{\gamma}}{\gr{r}} \cong \rec{u}\typ{\gr{\alpha}}{\gr{r}} \quad (\forall_{\gamma\in\{\gr{\gamma}\}} \exists_{\alpha\in\{\gr{\alpha}\}}\, \Pi,\relevant{\gr{\alpha}}\vdash\alpha\succeq\gamma) \tag{red$_{\cong}$} \end{align} where (with $\Pi\vdash\tau\le\sigma$ being the subtyping relation and $\Pi$ an environment of subtyping assumptions on names as defined below) \begin{align*} \Pi,T &\vdash \beh{\sign{x}{\ulg{v}{:}\gr{\eta},\gr{\sigma}}}{\gr{r}}{\gr{s},\gr{t}} \succeq \beh{\sign{x}{\ulg{v}{:}\gr{\eta},\gr{\tau}}}{\gr{r},\gr{r}' }{\gr{s},\gr{s}'} \\[-.5ex] & \hspace*{15em} (\Pi\vdash\gr{\tau}\le\gr{\sigma};\;\gr{s}'{\notin}T;\; \forall_{y,p}\,y^{[0]}{\in}T\Rightarrow y^p{,}y^\infty{\notin} \{\gr{r}',\gr{t}\}) \\ \Pi,T &\vdash \creat{\sign{x}{\ulg{v}{:}\gr{\eta},\gr{\sigma}}}{\gr{r},\gr{s}} \succeq \creat{\sign{x}{\ulg{v}{:}\gr{\eta},\gr{\tau}}}{\gr{r},\gr{t}} \quad (\Pi\vdash\gr{\tau}\le\gr{\sigma};\;\gr{t}{\notin}T;\; \forall_{y,p}\,y^{[0]}{\in}T\Rightarrow y^p{,}y^\infty{\notin} \{\gr{s}\}) \end{align*} If the environment is empty ($\Pi=\emptyset$), $\sigma\cong\tau$ is written instead of $\Pi\vdash\sigma\cong\tau$. \end{definition} The additional rule allows us to remove redundant descriptors. A descriptor is redundant if there is another descriptor that can be used wherever the redundant descriptor can be used. Redundant descriptors must be considered because they can be introduced by combining types: Even if two types, \typ{\gr{\alpha}}{\gr{r}} and \typ{\gr{\beta}}{\gr{s}}, are free of redundant descriptors, their combination, \typ{\gr{\alpha},\gr{\beta}}{\gr{r},\gr{s}}, can contain redundant descriptors. For each descriptor $\gamma$ removed by (red$_{\cong}$) there is another descriptor $\alpha$ with the same message selector, the same integer and type parameters and the same number of object parameters. The object parameter types in $\gamma$ are subtypes of the corresponding parameter types in $\alpha$. If the descriptors are message descriptors and $x^{[0]}$ is not relevant, the in-set of $\gamma$ can contain more tokens of the form $x^p$ than that of $\alpha$. Therefore, whenever a message specified by $\gamma$ is acceptable, this message is specified and acceptable by $\alpha$, too. The out-set or initial state of $\gamma$ must not contain more effective tokens than that of $\alpha$ does (to ensure that the state after updating the type according to $\gamma$ does not contain more effective tokens than that after updating the type according to $\alpha$). However, the out-set or initial state of $\gamma$ may contain additional tokens not effective in the type after removing $\gamma$. The rule (red$_{\cong}$) can remove several descriptors simultaneously because it is possible that a token becomes non-effective by removing several descriptors, but not by removing just a single descriptor. $\textit{BufI}\,\mset{}\cong\textit{BufI}\,\mset{}\|\textit{Buf}\, \mset{\text{empty}^p}$ is an example of weak type equivalence. Clearly, these types are not strongly type-equivalent because % \[ \boldsymbol{\{} \begin{array}[t]{@{}l@{}} \beh{\sign{\text{put}}{\ul{u}{:}\mtyp,u}}{}{\text{full}^1},\, \beh{\sign{\text{get}}{\textit{Back}\,\mset{\text{one}^1}} }{\text{full}^1}{}, \\ \beh{\sign{\text{put}}{\ul{u}{:}\mtyp,u}}{\text{empty}^1 }{\text{full}^1},\, \beh{\sign{\text{get}}{\textit{Back}\,\mset{\text{one}^1}} }{\text{full}^1}{\text{empty}^1} \boldsymbol{\}} \mset{\text{empty}^p} \end{array} \] % cannot be simplified using the rules in \rfig{equiv}. But, (red$_{\cong}$) is applicable to remove the redundant message descriptors in the second line. After removing the descriptors, empty$^p$ is no longer effective and can be removed using (state$_{\cong}$). Using weak type equivalence, it is easy to define subtyping: \begin{definition} \label{def:subtyping} \upshape The \emph{subtyping} relation $\Pi\vdash\sigma\le\tau$ on types is the least reflexive and transitive relation closed under the rules in \rfig{subtyping}; the relation depends on an environment $\Pi$ of subtyping assumptions on names (type parameters). $\sigma\le\tau$ is written instead of $\emptyset\vdash\sigma\le\tau$, where $\emptyset$ is the empty environment. \end{definition} \begin{figure} \rule{\textwidth}{1pt} \begin{gather} \Pi\cup\{u\le v\}\vdash u\le v \tag{assmp$_{\le}$} \\ \dfrac{\exists_{\rho}\,\Pi\vdash\sigma\cong\tau\|\rho}{ \Pi\vdash\sigma\le\tau} \tag{sub$_{\le}$} \\ \dfrac{\Pi\vdash\pi\le\rho\quad\Pi\vdash\sigma\le\tau}{ \Pi\vdash\pi\|\sigma\le\rho\|\tau} \tag{comb$_{\le}$} \\ \dfrac{\Pi\cup\{u\le v\}\vdash\typ{\gr{\alpha}}{\gr{r}}\le \typ{\gr{\gamma}}{\gr{s}}}{ \Pi\vdash\rec{u}\typ{\gr{\alpha}}{\gr{r}}\le \rec{v}\typ{\gr{\gamma}}{\gr{s}}} \ (u,v\notin\free{\Pi};\ u\notin\free{\tau};\ v\notin\free{\sigma}) \tag{rec$_{\le}$} \end{gather} \rule{\textwidth}{1pt} \caption{Subtyping} \label{subtyping} \end{figure} Rule (sub$_{\le}$) states that $\sigma$ is a subtype of $\tau$ if there is a type $\rho$ such that $\sigma$ is weakly type-equivalent to the combination of $\tau$ and $\rho$; $\rho$ specifies the difference between $\sigma$ and $\tau$. As a special case where $\rho$ is the empty type \typ{}{}, (sub$_{\le}$) states that $\Pi\vdash\sigma\cong\tau$ implies $\Pi\vdash\sigma\le\tau$. Also, if $\rho$ is selected to be equal to $\sigma$, $\Pi\vdash\sigma\le\typ{}{}$ follows from (sub$_{\le}$). Rules like (rec$_{\le}$) were shown to be useful for the subtyping of recursive types~\cite{AmCa91}. For example, $\textit{BufI}\,\mset{}\le\textit{Buf}\,\mset{\text{empty}^p}$ follows from $\textit{BufI}\,\mset{}\cong\textit{BufI}\,\mset{}\|\textit{Buf}\, \mset{\text{empty}^p}$. In a similar way, further subtyping relationships can be shown: \begin{alignat*}{2} \textit{Buf}\,\mset{\text{full}^{p+p'},\text{empty}^{q+q'}} &\le \textit{Buf}\,\mset{\text{full}^p,\text{empty}^q} &\qquad& (\textit{Buf}\,\mset{\text{full}^{p'},\text{empty}^{q'}}) \\ \textit{BufI}\,\mset{\text{full}^{p+p'}} &\le \textit{Buf}\,\mset{\text{full}^p,\text{empty}^q} &\qquad& (\textit{BufI}\,\mset{\text{full}^{p'}}) \\ \textit{BufI}\,\mset{\text{full}^{p+q}} &\le \textit{BufI}\,\mset{\text{full}^p} &\qquad& (\textit{BufI}\,\mset{\text{full}^{q}}) \\ \textit{BufID}\,\mset{\text{full}^{p+q},\text{ok}^{[0]},\text{ok}^\infty} &\le \textit{BufI}\,\mset{\text{full}^p} &\qquad& (\textit{BufID}\,\mset{\text{full}^{q}}) \\ \textit{BufID}\,\mset{\text{full}^{p+p'},\text{ok}^{[0]},\text{ok}^\infty} &\le \textit{BufD}\,\mset{\text{full}^p,\text{empty}^q,\text{ok}^{[0]}, \text{ok}^\infty} &\qquad& (\textit{BufID}\,\mset{\text{full}^{p'}}) \\ \textit{BufIDC}\,\mset{\text{full}^{p+q},\text{ok}^{[0]},\text{ok}^\infty} &\le \textit{BufID}\,\mset{\text{full}^p,\text{ok}^{[0]},\text{ok}^\infty} &\qquad& (\textit{BufIDC}\,\mset{\text{full}^{q}}) \\ \textit{PhilC}\,\mset{\text{nice}^1} &\le \textit{Phil}\,\mset{} &\qquad& (\textit{PhilC}\,\mset{\text{nice}^1}) \\ \textit{PhilC}\,\mset{\text{nice}^1,\text{br}^1} &\le \textit{Break}\,\mset{\text{br}^1} &\qquad& (\textit{PhilC}\,\mset{\text{nice}^1}) \end{alignat*} % (The types in parentheses show for each subtyping relationship the difference between subtype and supertype.) As in these examples, for types of the form \typ{\gr{\alpha}}{\gr{r}}, the static part of the type specifying the difference between subtype and supertype can always be selected to be equal to the static part of the subtype. This general observation helps in finding a type $\rho$ needed by (sub$_{\le}$). \subsection{Message Signature Sequences} \label{sequences} The set of acceptable message sequences determines, to a large extent, the semantics of a type. Using the notions introduced next, general properties of types and equivalence relations on types (concerning message signature sequences that correspond to acceptable message sequences) are developed. \begin{definition} \label{def:enabled} \upshape A message signature $a$ is \emph{enabled} with a \emph{follow-state} \mset{\gr{s}} in a type \typ{\gr{\alpha}}{\gr{r}} if $a\mset{\gr{s}}\in\act{\typ{\gr{\alpha}}{\gr{r}}}$, where \textit{enbl} is defined by: % \begin{align*} \act{\typ{}{\gr{r}}} &= \emptyset \\ \act{\typ{\beh{a}{\gr{s}}{\gr{t}},\gr{\gamma}}{\gr{r}}} &= \{a\mset{\gr{t},\gr{t}'}\}\cup \act{\typ{\gr{\gamma}}{\gr{r}}} \quad ( \begin{array}[t]{@{}l@{}} \mset{\gr{r}}{\equiv}\mset{\gr{s},\gr{t}'};\ \forall_{x,p}\,x^{[0]}{\in}\{\gr{s}\}\Rightarrow x^p{,}x^\infty{\notin}\{\gr{t}'\}; \\ \forall_x(x^\infty{\in}\{\gr{r}\}\wedge x^{[0]}{\notin}\{\gr{s}\}) \Rightarrow x^\infty{\in}\{\gr{t}'\}) \end{array} \\ \act{\typ{\beh{a}{\gr{s}}{\gr{t}},\gr{\gamma}}{\gr{r}}} &= \act{\typ{\gr{\gamma}}{\gr{r}}} \quad (\nexists_{\gr{t}'}\,\mset{\gr{r}}\equiv\mset{\gr{s},\gr{t}'}) \\ \act{\typ{\creat{a}{\gr{t}},\gr{\gamma}}{\gr{r}}} &= \act{\typ{\gr{\gamma}}{\gr{r}}} \end{align*} \end{definition} If a message signature $a$ is enabled with a follow-state \mset{\gr{s}} in a type \typ{\gr{\alpha}}{\gr{r}}, an object of this type will accept a (single) message of signature $a$. When the message is accepted, the type is updated to \typ{\gr{\alpha}}{\gr{s}}. The signatures of the messages acceptable next are enabled in \typ{\gr{\alpha}}{\gr{s}}. Type marks are updated in the same way when sending messages. \begin{definition} \label{seq} \upshape The set \seq{\tau} of all message signature sequences specified by a type $\tau$ of the form \typ{\gr{\alpha}}{\gr{r}} is constructed inductively on the lengths of the sequences: \[ \begin{array}{r@{{}={}}l} S_0 & \{\lst{}\mset{\gr{r}}\} \\ S_{i+1} & \{\lst{\gr{a},\sign{x}{\ulg{u}{:}\gr{\eta},\gr{\sigma}}} \mset{\gr{s}}\mid \begin{array}[t]{@{}l@{}} \lst{\gr{a}}\mset{\gr{t}}\in S_i;\; \sign{x}{\ulg{v}{:}\gr{\eta},\gr{\tau}}\mset{\gr{s}}\in \act{\typ{\gr{\alpha}}{\gr{t}}}; \\ \gr{\sigma}\equiv_{\text{t}}\subst{\gr{u}}{\gr{v}}\gr{\tau};\; \gr{u}\in(\mathbb{V}\setminus\free{\gr{\tau}})\cup\{\gr{v}\} \quad\} \quad (i\ge0) \end{array} \\ \seq{\tau} & \{\lst{\gr{a}}\mid \lst{\gr{a}}\mset{\gr{s}}\in\bigcup_{i\ge0}S_i\} \end{array} \] The set \cseq{\tau} of all message signature sequences conforming to $\tau$ is given by: \[ \cseq{\tau} = \{ \begin{array}[t]{@{}l@{}} \lst{\sign{x_1}{\ulg{u}_1{:}\gr{\eta}_1,\gr{\sigma}_1},\dots, \sign{x_n}{\ulg{u}_n{:}\gr{\eta}_n,\gr{\sigma}_n}} \mid{} \\ \lst{\sign{x_1}{\ulg{u}_1{:}\gr{\eta}_1,\gr{\tau}_1},\dots, \sign{x_n}{\ulg{u}_n{:}\gr{\eta}_n,\gr{\tau}_n}}\in\seq{\tau};\; \gr{\sigma}_1\le\gr{\tau}_1,\dots,\gr{\sigma}_n\le\gr{\tau}_n \} \end{array} \] \end{definition} For each sequence of message signatures $\lst{\gr{a}}\in\seq{\tau}$, \seq{\tau} also contains all message signature sequences that are equal to \lst{\gr{a}} except for renaming bound names ($\alpha$-conversion) and applying strict type equivalence to object parameter types. For each $\lst{\gr{a}}\in\cseq{\tau}$, \cseq{\tau} also contains all message signature sequences with subtypes substituted for the object parameter types in \lst{\gr{a}}. \textit{Cseq} is motivated by the fact that an object accepting a message with arguments of types \gr{\tau} also accepts messages with the same message selector and arguments of types \gr{\sigma} with $\gr{\sigma}\le\gr{\tau}$. Obviously, $\seq{\tau}\subseteq\cseq{\tau}$. It is easy to see from the construction of \textit{cseq} that, for all types \typ{\gr{\alpha}}{\gr{r}} and \typ{\gr{\gamma}}{\gr{s}}, $\seq{\typ{\gr{\alpha}}{\gr{r}}}=\seq{\typ{\gr{\gamma}}{\gr{s}}}$ implies $\cseq{\typ{\gr{\alpha}}{\gr{r}}}=\cseq{\typ{\gr{\gamma}}{\gr{s}}}$, but not vice versa. The reason of this difference is that \textit{cseq} hides redundant message descriptors, while \textit{seq} does, in general, not. This difference suggests that \textit{seq} is related to strong type equivalence and \textit{cseq} to weak type equivalence: \begin{proposition} \label{prp:equiv} Let $\sigma$ and $\tau$ be types of the forms \typ{\gr{\alpha}}{\gr{r}} and \typ{\gr{\gamma}}{\gr{s}}, respectively. Then, \begin{itemize} \item $\sigma\equiv_{\text{\upshape t}}\tau$ implies $\seq{\sigma}=\seq{\tau}$; \item $\sigma\cong\tau$ implies $\cseq{\sigma}=\cseq{\tau}$. \end{itemize} \end{proposition} The proof of $\seq{\sigma}=\seq{\tau}$ if $\sigma\equiv_{\text{\upshape t}}\tau$ is sketched. The rule (state$_{\cong}$) in \rfig{equiv} adds non-effective tokens to or deletes them from states. Since these tokens have no effect on the enablement of message signatures (according to the definition of \textit{enbl}), they have no effect on $\seq{\sigma}$ and $\seq{\tau}$. The other rules in \rfig{equiv} are obvious. (Rules dealing with recursion and type combination need not be considered.) To prove that $\sigma\cong\tau$ implies $\cseq{\sigma}=\cseq{\tau}$, let $\sigma\cong\tau$. If $\sigma\equiv_{\text{t}}\tau$, then $\cseq{\sigma}=\cseq{\tau}$ follows from $\seq{\sigma}=\seq{\tau}$. Otherwise let (red$_{\cong}$) be applied to $\sigma$ and $\tau$ such that $\mset{\gr{r}}\equiv\mset{\gr{s},\gr{t}}$ for some $\gr{t}$ with $\gr{t}\notin\relevant{\gr{\gamma}}$, and $\coll{\gr{\alpha}}\equiv\coll{\gr{\gamma},\gr{\beta}}$ for some $\gr{\beta}$; the descriptors $\gr{\beta}$ have been deleted by applying (red$_{\cong}$). Hence, $\seq{\tau}\subseteq\seq{\sigma}$ and $\cseq{\tau}\subseteq\cseq{\sigma}$. The side-condition of (red$_{\cong}$) implies that a descriptor is deleted only if there remains a more general descriptor. The signature of the remaining descriptor is enabled whenever that of the deleted descriptor was enabled. For each $\lst{\gr{a}}$ in $\seq{\sigma}$ there is a $\lst{\gr{c}}$ in $\seq{\tau}$, where $\lst{\gr{c}}$ is equal to $\lst{\gr{a}}$ except that parameter types in $\lst{\gr{a}}$ can be subtypes of the corresponding parameter types in $\lst{\gr{c}}$. This implies $\cseq{\sigma}\subseteq\cseq{\tau}$. Therefore, $\cseq{\sigma}=\cseq{\tau}$. \qed Unfortunately, the reverses of \rprp{prp:equiv} do not hold. For example, $\textit{BufID}\,\mset{}\equiv_{\text{t}}\typ{}{}$ does not hold, although these types specify the same set of message signature sequences. $\seq{\sigma}=\seq{\tau}$ does not imply $\sigma\equiv_{\text{t}}\tau$, and $\cseq{\sigma}=\cseq{\tau}$ does not imply $\sigma\cong\tau$. There are several reasons for that: \begin{itemize} \item \textit{Seq} and \textit{cseq} do not reflect creator descriptors in types. Two types with unrelated sets of creator descriptors may still specify the same set of message signature sequences, although these types are not (weakly or strongly) type-equivalent. \item Strong and weak type equivalence depend on the equality of token symbols. Two types are not equivalent if one of them is constructed from the other by renaming token symbols. By requiring token symbol equality, types are combined in the same way as they were previously split. \item Types in the proposed calculus are much more expressive than regular expressions. As argued in \rsec{design-space} and in analogy to the theory of automata and formal languages, it is quite unlikely that there can be an algorithm to decide whether two arbitrary types specify the same set of message signature sequences. To be concrete, \textit{eff} as defined in \rsec{typing} is just a conservative approximation. The accuracy of the correspondence between $\sigma\equiv_{\text{t}}\tau$ and $\seq{\sigma}=\seq{\tau}$ could be improved by increasing the accuracy (and complexity) of this approximation and adding further type equivalence rules. But there always remains a gap. \end{itemize} Because of \rprp{prp:equiv}, \rdef{seq} can be extended: For all types $\tau$ such that there is a type of the form \typ{\gr{\alpha}}{\gr{r}} with $\tau\equiv_{\text{t}}\typ{\gr{\alpha}}{\gr{r}}$, let $\seq{\tau}=\seq{\typ{\gr{\alpha}}{\gr{r}}}$ and $\cseq{\tau}=\cseq{\typ{\gr{\alpha}}{\gr{r}}}$. As mentioned in \rsec{proposal}, an object of type $\sigma\|\tau$ (the combination of $\sigma$ and $\tau$) has to accept all messages sent according to $\sigma$ and $\tau$ in arbitrary interleaving. The set of all arbitrary interleavings of a message signature sequence \lst{\gr{a}} with a message signature sequence \lst{\gr{c}} is given by $\lst{\gr{a}}\otimes\lst{\gr{c}}$: % \begin{align*} \lst{a,\gr{a}}\otimes\lst{c,\gr{c}} &= \{\lst{a,\gr{b}}\mid\lst{\gr{b}}\in\lst{\gr{a}}\otimes\lst{c,\gr{c}}\}\cup \{\lst{c,\gr{b}}\mid\lst{\gr{b}}\in\lst{a,\gr{a}}\otimes\lst{\gr{c}}\} \\ \lst{\gr{a}}\otimes\lst{} &= \lst{\gr{a}} \\ \lst{}\otimes\lst{\gr{a}} &= \lst{\gr{a}} \end{align*} \begin{proposition} \label{prp:otimes} Let $\sigma$ and $\tau$ be types such that \textit{seq} is defined on $\sigma$, $\tau$ and $\sigma\|\tau$. Then, $\lst{\gr{a}}\otimes\lst{\gr{c}}\subseteq\seq{\sigma\|\tau}$ for each $\lst{\gr{a}}\in\seq{\sigma}$ and $\lst{\gr{c}}\in\seq{\tau}$. \end{proposition} The proof is sketched. Without restricting generality, let $\sigma=\typ{\gr{\alpha}}{\gr{r}}$ and $\tau=\typ{\gr{\gamma}}{\gr{s}}$ such that $\sigma\|\tau\equiv_{\text{t}}\typ{\gr{\alpha},\gr{\gamma}}{\gr{r},\gr{s}}$. It is easy to see from the definition of \textit{seq} that \typ{\gr{\alpha},\gr{\gamma}}{\gr{r},\gr{s}} contains (among other sequences) all arbitrary interleavings of message signature sequences constructed from \typ{\gr{\alpha}}{\gr{r}} with those constructed from \typ{\gr{\beta}}{\gr{s}}. $\lst{\gr{a}}\otimes\lst{\gr{c}}$ is exactly the sequence of all arbitrary interleavings of $\lst{\gr{a}}$ with $\lst{\gr{c}}$. \qed The principle of substitutability requires that an instance of a subtype can be used wherever an instance of a supertype was expected. Especially, an object of a subtype must accept all message sequences accepted by an object of a supertype. The subtyping relation $\sigma\le\tau$ conforms to this principle: \begin{proposition} \label{prp:sub} Let $\sigma$ and $\tau$ be types, where $\sigma$ is of the form \typ{\gr{\alpha}}{\gr{r}}. Then $\sigma\le\tau$ implies $\cseq{\tau}\subseteq\cseq{\sigma}$. \end{proposition} To sketch the proof, let $\sigma\le\tau$. There is a type $\rho$ with $\sigma\cong\tau\|\rho$ according to (sub$_{\le}$). Therefore, there is a type \typ{\gr{\gamma}}{\gr{s}} with $\tau\|\rho\equiv_{\text{t}}\typ{\gr{\gamma}}{\gr{s}}$ so that \textit{seq} and \textit{cseq} are defined on $\tau$ and $\tau\|\rho$. Because of \rprp{prp:equiv}, $\cseq{\sigma}=\cseq{\tau\|\rho}$. Because of \rprp{prp:otimes}, $\lst{\gr{a}}\otimes\lst{}\subseteq\seq{\tau\|\rho}$ for all $\lst{\gr{a}}\in\seq{\tau}$. Thus, $\seq{\tau}\subseteq\seq{\tau\|\rho}$ and $\cseq{\tau}\subseteq\cseq{\sigma}$. \qed \subsection{Deterministic Types} \label{deterministic} Types without redundant descriptors play an important role: The type of each object must be free of redundant descriptors to ensure that, when a message is accepted, this type is updated in the same way as the corresponding type mark was updated when the message was sent. \begin{definition} \upshape A static part \coll{\gr{\alpha}} of a type, each $\alpha_i$ of the form \beh{\sign{x_i}{\ulg{u}_i{:}\gr{\eta}_i,\gr{\tau}_i}}{\gr{s}_i}{\gr{t}_i} or \creat{\sign{x_i}{\ulg{u}_i{:}\gr{\eta}_i,\gr{\tau}_i}}{\gr{t}_i}, is \emph{deterministic} if for all $i,j=1,\dots,\lvert\gr{\alpha}\rvert$ with $x_i=x_j$ and $\lvert\gr{\eta}_i,\gr{\tau}_i\rvert=\lvert\gr{\eta}_j,\gr{\tau}_j\rvert$ at least one of these conditions holds: \begin{itemize} \item $i=j$; \item either $\alpha_i$ or $\alpha_j$ is a message descriptor, the other a creator descriptor; \item $\alpha_i,\alpha_j$ message descriptors, $\exists_{x}\forall_{p,\gr{t}'}(\mset{\gr{s}_i}{\equiv}\mset{x^{[0]},x^p,\gr{t}'}\wedge x^\infty{\notin}\{\gr{t}'\})\Rightarrow\exists_{\gr{s}'}\mset{\gr{s}_j}{\equiv}\mset{x^{p+1},\gr{s}'}$; \item $\alpha_i,\alpha_j$ message descriptors, $\exists_{x}\forall_{p,\gr{t}'}(\mset{\gr{s}_j}{\equiv}\mset{x^{[0]},x^p,\gr{t}'}\wedge x^\infty{\notin}\{\gr{t}'\})\Rightarrow\exists_{\gr{s}'}\mset{\gr{s}_i}{\equiv}\mset{x^{p+1},\gr{s}'}$. \end{itemize} A type is deterministic if it is of the form \typ{\gr{\alpha}}{\gr{t}} and \coll{\gr{\alpha}} is deterministic. \end{definition} Deterministic types are free of redundant descriptors; no application of (red$_{\cong}$) to a deterministic type can remove a descriptor that cannot be removed by applying strong type equivalence. For example, all types of the form \typ{\gr{\alpha}}{\gr{r}} shown in \rsec{examples} are deterministic. It is easy to see that $\Pi\vdash\sigma\cong\tau$ and $\sigma$ and $\tau$ deterministic implies $\sigma\equiv_{\text{t}}\tau$. The main reason for using deterministic types is expressed by this proposition: \begin{proposition} \label{prp:det-seq} Let \typ{\gr{\alpha}}{\gr{r}} be a deterministic type, $\tau$ a type with $\typ{\gr{\alpha}}{\gr{r}}\le\tau$, and let $\lst{\sign{x_1}{\ulg{u}_1{:}\gr{\eta}_1,\gr{\sigma}_1},\dots,\sign{x_n}{ \ulg{u}_n{:}\gr{\eta}_n,\gr{\sigma}_n}}\in\seq{\tau}$. Then, there is exactly one sequence of states $\mset{\gr{s}_0},\dots,\mset{\gr{s}_n}$ with $\mset{\gr{s}_0}=\mset{\gr{r}}$ such that $\sign{x_i}{\ulg{v}_i{:}\gr{\eta}_i,\gr{\rho}_i}\mset{\gr{s}_i}\in \act{\typ{\gr{\alpha}}{\gr{s}_{i-1}}}$ with $\lvert\gr{\rho}_i\rvert=\lvert\gr{\sigma}_i\rvert$ for each $i=1,\dots,n$; furthermore, $\gr{\sigma}_i\le\subst{\gr{u}_i}{\gr{v}_i}\gr{\rho}_i$. \end{proposition} Because of $\typ{\gr{\alpha}}{\gr{r}}\le\tau$, there is at least one such sequence of states as a consequence of \rprp{prp:sub}. The uniqueness of the sequence follows immediately from the fact that \coll{\gr{\alpha}} is free of redundant message descriptors so that each message signature and follow-state is completely determined by the corresponding message selector and number of parameters. \qed An important precondition of the type system is that subtyping is compatible with type updating. The next proposition is stronger than \rprp{prp:sub}: \begin{proposition} \label{prp:enbl-le} Let $\sigma$ and $\tau$ be types of the forms \typ{\gr{\alpha}}{\gr{r}} and \typ{\gr{\gamma}}{\gr{s}}, respectively, with $\sigma$ deterministic and $\sigma\le\tau$; and let $\sign{x}{\ulg{u}{:}\gr{\eta},\gr{\tau}}\mset{\gr{s}'}\in \act{\typ{\gr{\gamma}}{\gr{s}}}$. Then, $\typ{\gr{\alpha}}{\gr{r}'}\le\typ{\gr{\gamma}}{\gr{s}'}$ for $\sign{x}{\ulg{v}{:}\gr{\eta},\gr{\sigma}}\mset{\gr{r}'}\in \act{\typ{\gr{\alpha}}{\gr{r}}}$. \end{proposition} According to \rprp{prp:det-seq}, \typ{\gr{\alpha}}{\gr{r}}, $x$ and $\lvert\gr{\eta},\gr{\tau}\rvert$ completely determine \typ{\gr{\alpha}}{\gr{r}'}. Since \coll{\gr{\gamma}} need not be deterministic, there can be several message descriptors $\gamma\in\{\gr{\gamma}\}$ with the same message selector and the same number of parameters. There must be a type $\rho$ of the form \typ{\gr{\alpha}}{\gr{t}} with $\sigma\cong\tau\|\rho$. Because of $\typ{\gr{\alpha}}{\gr{r}}\cong\typ{\gr{\alpha},\gr{\gamma}}{\gr{s},\gr{t}}$, the descriptors \gr{\gamma} are redundant: For each message descriptor $\gamma\in\{\gr{\gamma}\}$ there is exactly one $\alpha\in\{\gr{\alpha}\}$ with $\relevant{\gr{\alpha}}\vdash\alpha\succeq\gamma$. The side-conditions in \rdef{def:weak} ensure that the out-set of $\gamma$ does not contain more tokens effective in \coll{\gr{\alpha}} than the out-set of $\alpha$, and the in-set of $\alpha$ does not contain more tokens than the in-set of $\gamma$. Therefore, there are tokens $\gr{t}'$ with $\typ{\gr{\alpha}}{\gr{r}'}\cong\typ{\gr{\alpha},\gr{\gamma}}{\gr{s}',\gr{t}'}$ and $\typ{\gr{\alpha}}{\gr{r}'}\le\typ{\gr{\gamma}}{\gr{s}'}$. \qed Let $\sigma$ be the deterministic type of an object, and let $\tau$ (not necessarily deterministic) with $\sigma\le\tau$ be the type mark of a reference to the object. Because of \rprp{prp:det-seq}, each sequence of messages sent according to $\tau$ is accepted by the object, although $\sigma$ is updated by the object on accepting a message step by step, without knowing the rest of the message sequence. And because of \rprp{prp:enbl-le}, $\sigma'\le\tau'$ for all types $\sigma'$ and $\tau'$ constructed by updating $\sigma$ and $\tau$, respectively, according to the same message sequence. A further precondition of the type system is that subtyping is compatible with type splitting and type combination: \begin{proposition} \label{prp:le-comb} Let $\sigma$ be a deterministic type with $\sigma\equiv_{\text{t}}\tau_1\|\dots\|\tau_n$ ($n\ge2$), and $\tau_i\le\rho_i$ for $1\le i\le n$. Then, for each index set $\{i_1,\dots,i_m\}\subseteq\{1,\dots,n\}$ ($m\ge2$), there is a type $\pi$ of the form \typ{\gr{\gamma}}{\gr{s}} with $\rho_{i_1}\|\dots\|\rho_{i_m}\equiv_{\text{t}}\pi$ and $\sigma\le\pi$. \end{proposition} Let $\sigma$ be of the form \typ{\gr{\alpha}}{\gr{r}}. $\sigma$ is split into $\tau_1,\dots,\tau_n$ using (comb$_{\cong}$). The side-condition of this rule ensures that if a token $x^{[p]}$ occurs in \mset{\gr{r}}, a token $x^{[p_i]}$ occurs in the state of each $\tau_i$ (where this token is effective). The $\tau_i$ can easily be selected so that they are deterministic. There are $\rho'_i$ so that $\tau_i\cong\rho_i\|\rho'_i$. Therefore, there are types of the form \typ{\gr{\beta}_i}{\gr{t}_i} with $\rho_i\equiv_{\text{t}}\typ{\gr{\beta}_i}{\gr{t}_i}$ and $\gr{t}_i\in\relevant{\gr{\beta}_i}$. %If $x^{[p_i]}$ does not occur in the state of $\tau_i$, it cannot occur in %the state of $\rho_i$. The side-conditions of (comb$_{\cong}$) are satisfied so that all \typ{\gr{\beta}_j}{\gr{t}_j} (with $j\in\{i_1,\dots,i_m\}$) can be combined to $\pi$. $\sigma\le\pi$ follows from transitivity of the subtyping relation. \qed The definition of the subtyping relation has to consider the compatibility of creator descriptors. If the type mark of a reference to an object contains a creator descriptor, the user of the reference can create a new object by cloning the referred object. Since the type mark is a supertype of the referred object's type, the creator descriptors in the type mark and the object's type can be different. The next proposition states that the creator descriptor in the type mark provides useful information. \begin{proposition} \label{prp:creator} Let $\sigma$ and $\tau$ be types of the forms \typ{\gr{\alpha}}{\gr{r}} and \typ{\gr{\gamma}}{\gr{s}}, respectively, with $\sigma$ deterministic and $\sigma\le\tau$; and let $\creat{\sign{x}{\ulg{u}{:}\gr{\eta},\gr{\rho}}}{\gr{s}'}\in\{\gr{\gamma}\}$. Then, there is exactly one creator descriptor $\alpha\in\{\gr{\alpha}\}$ with $\alpha=\creat{\sign{x}{\ulg{v}{:}\gr{\eta},\gr{\pi}}}{\gr{r}'}$ and $\lvert\gr{\pi}\rvert=\lvert\gr{\rho}\rvert$; furthermore, $\gr{\rho}\le\subst{\gr{u}}{\gr{v}}\gr{\pi}$ and $\typ{\gr{\alpha}}{\gr{r}'}\le\typ{\gr{\gamma}}{\gr{s}'}$. \end{proposition} Since $\sigma$ is deterministic, it is easy to see that $\sigma$ contains exactly one creator descriptor with the same message selector and number of arguments as a creator descriptor in $\tau$. There is a type $\rho$ of the form \typ{\gr{\alpha}}{\gr{t}} with $\sigma\cong\tau\|\rho$, i.e., $\typ{\gr{\alpha}}{\gr{r}}\cong\typ{\gr{\alpha},\gr{\gamma}}{\gr{s},\gr{t}}$. For each creator descriptor $\gamma\in\{\gr{\gamma}\}$ there is exactly one $\alpha\in\{\gr{\alpha}\}$ with $\relevant{\gr{\alpha}}\vdash\alpha\succeq\gamma$. The side-conditions in \rdef{def:weak} ensure $\gr{\rho}\le\subst{\gr{u}}{\gr{v}}\gr{\pi}$. Furthermore, they ensure that the initial state of $\gamma$ does not contain more tokens effective in \coll{\gr{\alpha}} than the initial state of $\alpha$. Therefore, there are tokens $\gr{t}'$ with $\typ{\gr{\alpha}}{\gr{r}'}\cong\typ{\gr{\alpha},\gr{\gamma}}{\gr{s}',\gr{t}'}$ and $\typ{\gr{\alpha}}{\gr{r}'}\le\typ{\gr{\gamma}}{\gr{s}'}$. \qed \subsection{Reduction Semantics} \label{semantics} Now, the semantics of the proposed calculus is defined formally. A \emph{system configuration} $E$ is an environment that contains expressions of the forms $u\mapsto(\gr{A};P;\gr{\mu})$. This expression specifies the initial behavior as well as the current state and behavior of an object with identifier $u$: The object currently behaves as $P$, where $P$ already contains state information (i.e., arguments substituted for parameters). The ordered list \gr{\mu} reflects the object's queue of received, but not yet accepted messages; the next message to be accepted is the leftmost message in the list. \gr{A} specifies the object's initial behavior. For each $u\in\mathbb{V}$, $E$ contains at most one expression of the form $u\mapsto(\gr{A};P;\gr{\mu})$. $E[u_1\mapsto(\gr{A}_1;P_1;\gr{\mu}_1),\dots, u_n\mapsto(\gr{A}_n;P_n;\gr{\mu}_n)]$ denotes a system configuration with the expressions in the square brackets added to $E$, where $u_1,\dots,u_n$ are pairwise different names not occurring to the left of $\mapsto$ in $E$. \begin{definition} \label{def:exec} \upshape The \emph{single-$u$-execution-step} relation $\trans{u}$ on system configurations ($u\in\mathbb{V}$) is the least relation closed under the rules in \rfig{exec-rules}. The \emph{single-execution-step} relation $\trans{}$ is the least closure of all $\trans{u}$. The \emph{execution} relation $\trans{*}$ is the least reflexive and transitive closure of $\trans{}$. \end{definition} \begin{figure} \rule{\textwidth}{1pt} \begin{align} \makebox[0em]{\ $\dfrac{E\equiv E' \quad E'\trans{u}F' \quad F'\equiv F}{E\trans{u}F}$} \tag{eq$_{\text{E}}$} \\ E[u\mapsto(\gr{A};\coll{\rcv{x}{\ulg{u}}.P,\gr{B}}; \msg{x}{\gr{\varphi},\gr{v}},\gr{\mu})] &\trans{u} E[u\mapsto(\gr{A};\subst{\gr{\varphi},\gr{v}}{\gr{u}}P;\gr{\mu})] \tag{sel$_{\text{E}}$} \\ E[u\mapsto(\gr{A};\snd{v}{\xi}.P;\gr{\mu}),\,v\mapsto(\gr{B};Q;\gr{\nu})] &\trans{u} E[u\mapsto(\gr{A};P;\gr{\mu}),\,v\mapsto(\gr{B};Q;\gr{\nu},\xi)] \tag{send1$_{\text{E}}$} \\ E[u\mapsto(\gr{A};\snd{u}{\xi}.P;\gr{\mu})] &\trans{u} E[u\mapsto(\gr{A};P;\gr{\mu},\xi)] \tag{send2$_{\text{E}}$} \\ E[u\mapsto(\gr{A};\cond{v{=}v}{P}{Q};\gr{\mu})] &\trans{u} E[u\mapsto(\gr{A};P;\gr{\mu})] \tag{cmp1$_{\text{E}}$} \\ E[u\mapsto(\gr{A};\cond{v{=}w}{P}{Q};\gr{\mu})] &\trans{u} E[u\mapsto(\gr{A};Q;\gr{\mu})] \quad (v\neq w) \tag{cmp2$_{\text{E}}$} \\ E[u\mapsto(\gr{A};\cond{\sigma{\le}\tau}{\ul{v}.P}{Q};\gr{\mu})] &\trans{u} E[u\mapsto(\gr{A};\subst{\rho}{v}P;\gr{\mu})] \quad (\sigma\cong\tau\|\rho) \tag{sub1$_{\text{E}}$} \\ E[u\mapsto(\gr{A};\cond{\sigma{\le}\tau}{\ul{v}.P}{Q};\gr{\mu})] &\trans{u} E[u\mapsto(\gr{A};Q;\gr{\mu})] \quad (\nexists_{\rho}\,\sigma\cong\tau\|\rho) \tag{sub2$_{\text{E}}$} \\ E[u\mapsto(\gr{A};\cond{p{\ge}q}{\ul{v}.P}{Q};\gr{\mu})] &\trans{u} E[u\mapsto(\gr{A};\subst{q'}{v}P;\gr{\mu})] \quad (p\equiv q+q') \tag{more1$_{\text{E}}$} \\ E[u\mapsto(\gr{A};\cond{p{\ge}q}{\ul{v}.P}{Q};\gr{\mu})] &\trans{u} E[u\mapsto(\gr{A};Q;\gr{\mu})] \quad (\nexists_{q'}\,p\equiv q+q') \tag{more2$_{\text{E}}$} \\ E[u\mapsto(\gr{A};\new{\ul{v}}{\class{\gr{B}}{\gr{\alpha}}}{\xi}.P; \gr{\mu})] &\trans{u} E[u\mapsto(\gr{A};P;\gr{\mu}),\,v\mapsto(\gr{B};\coll{\gr{B}};\xi)] \tag{intro$_{\text{E}}$} \\ E[u\mapsto(\gr{A};\new{\ul{v}}{w}{\xi}.P;\gr{\mu})] &\trans{u} \begin{array}[t]{@{}l@{}} E[u\mapsto(\gr{A};P;\gr{\mu}),\,v\mapsto(\subst{v}{w}\gr{B}; \subst{v}{w}\coll{\gr{B}};\xi)] \\ \makebox[0pt][l]{$((u=w\,\wedge\,\gr{A}=\gr{B})\,\vee\, w\mapsto(\gr{B};Q;\gr{\nu})\in E)$} \end{array} \tag{new$_{\text{E}}$} \\ E[u\mapsto(\gr{A};\call{\xi};\gr{\mu})] &\trans{u} E[u\mapsto(\gr{A};\subst{u}{v}\coll{\gr{A}};\xi;\gr{\mu})] \tag{bec$_{\text{E}}$} \end{align} \rule{\textwidth}{1pt} \caption{Execution Rules (Operational Semantics)} \label{exec-rules} \end{figure} Rule (eq$_{\text{E}}$) in \rfig{exec-rules} states that the equivalence relation $\equiv$ can be applied before and after each execution step. Especially, this rule must be applied to rename parameters as required, and to reorder guarded processes in selection processes of the form \coll{\gr{A}}. Rule (sel$_{\text{E}}$) selects a guarded process whose message selector and number of parameters equals the message selector and number of arguments of the first message in the queue of received messages. The rules (send1$_{\text{E}}$) and (send2$_{\text{E}}$) append a message to be sent to the receiver's queue of received messages. The latter rule deals with objects sending messages to themselves. The rules (cmp1$_{\text{E}}$), (cmp2$_{\text{E}}$), (sub1$_{\text{E}}$), (sub2$_{\text{E}}$), (more1$_{\text{E}}$) and (more2$_{\text{E}}$) select conditional processes for execution. The conditions have to be evaluated immediately before selecting the process to be executed. New objects are created by (intro$_{\text{E}}$) and (new$_{\text{E}}$). Using (eq$_{\text{E}}$), the identifier $v$ of the new process must be selected so that $v$ does not yet occur to the left of $\mapsto$ in $E$. While (intro$_{\text{E}}$) requires that the behavior of the new object is specified explicitly in the process, (new$_{\text{E}}$) takes the initial behavior from another object to be cloned. The initial message sent to the new object is always specified explicitly. Rule (bec$_{\text{E}}$) lets the behavior of an object become equal to the initial behavior of the object. This is the only rule that can insert a message at the begin of the queue of received messages. A system configuration can be regarded as a snapshot of an object system. The execution relation relates earlier snapshots with later snapshots of the same system. The execution is nondeterministic: There are system configurations $E$, $F$ and $F'$ with $E\trans{*}F$ and $E\trans{*}F'$, but no $G$ with $F\trans{*}G$ and $F'\trans{*}G$. Rule (sel$_{\text{E}}$) together with (eq$_{\text{E}}$) in \rfig{exec-rules} introduces nondeterminism: A process of the form \coll{\gr{A}} may contain several guarded processes that accept the next message in the message queue. But also (intro$_{\text{E}}$) and (new$_{\text{E}}$) together with (eq$_{\text{E}}$) introduce nondeterminism by selecting arbitrary names in $\mathbb{V}$ as identifers of new objects. The major source of nondeterminism in a system is that the rules can be applied in a large number of possible sequences. If several clients send messages to the same object, the sequence of rule applications determines the sequence of messages in the object's queue. \emph{Initial configurations}, the system configurations from which all other system configurations are generated by repeatedly applying the rules in \rfig{exec-rules}, are of the form $\{u_1\mapsto(;P_1;),\dots,u_n\mapsto(;P_n;)\}$, where $P_1,\dots,P_n$ are the \emph{initial processes} (or program modules) of the system. To ensure that each identifier in the initial processes identifies an object, $\free{P_1,\dots,P_n}\subseteq\{u_1,\dots,u_n\}$ is required. Initial configurations provide the basis for static type checking. \section{Type Checking} \label{type-check} %Before we can deal with type checking, we have to state clearly what the %notion of type consistency means. Intuitively, a system configuration $E$ is type consistent if, for each object with an identifier $u$ in $E$, there is an execution step $E\trans{u}F$, except if the object is waiting for a message to be received; an object with identifier $u$ waits for a message if an expression of the form $u\mapsto(\gr{A};\coll{\gr{B}};)$ is in $E$, i.\,e., the queue of received messages is empty. Other reasons for an object to be non-executable are regarded as type errors. A type error has occurred if \begin{itemize} \item $E$ contains an expression $u\mapsto(\gr{A};\coll{\gr{B}};\nu,\gr{\mu})$ and (sel$_{\text{E}}$) is not applicable because no guarded process in \coll{\gr{B}} can deal with $\nu$, or \item $E$ contains an expression $u\mapsto(\gr{A};\snd{e}{\xi}.P;\gr{\mu})$ or $u\mapsto(\gr{A};\new{\ul{w}}{e}{\xi}.P;\gr{\mu})$, but $E$ contains no expression $e\mapsto(\gr{B};Q;\gr{\nu})$, i.\,e., the referenced object with identifier $e\in\mathbb{V}$ does not exist, or $e$ is not an object identifier. \end{itemize} Furthermore, type consistency of a system configuration $E$ shall imply that each system configuration $F$ with $E\trans{*}F$ also is type-consistent. Therefore, the following definition of type consistency of initial configurations is used: \begin{definition} \label{def:consistency} \upshape An initial configuration $E$ is \emph{type-consistent} if for each system configuration $F$ with $E\trans{*}F$, where $F$ contains an expression of the form $u\mapsto(\gr{A};\coll{\gr{B}};\nu,\gr{\mu})$ or $u\mapsto(\gr{A};P;\gr{\mu})$ with $P$ not of the form \coll{\gr{B}}, there exists a system configuration $G$ with $F\trans{u}G$. \end{definition} A set of type checking rules is proposed in \rsec{rules}. Initial configurations conforming to these rules are type-consistent, as shown in \rsec{proof}. Decidability of strong and weak type equivalence, subtyping and type checking is dealt with in \rsec{algorithm}. \subsection{Type Checking Rules} \label{rules} \rfig{checking} lists the type checking rules. An expression of the form $\TE{u}\vdash\lst{P{:}\tau}$ means that the process $P$ specifies a behavior compatible with the behavior partially specified by the type $\tau$ (an object behaving as $P$ is of type $\tau$), depending on the typing environment \TE{u}. This environment contains typings, i.\,e., expressions of the forms $v{:}\sigma$ ($v$ is an object parameter of type mark $\sigma$), $v{:}\mtyp$ ($v$ is a type parameter) and $v{:}\num$ ($v$ is a nonnegative-integer parameter). The object parameter $u$ in \TE{u} is regarded as a self reference of an object behaving as $P$. If it does not matter which object parameter is regarded as self reference, the typing environment is simply denoted by $\Gamma$. A typing environment of the form $\TE{u}[\gr{v}{:}\gr{e}]$ (or $\Gamma$[\gr{v}{:}\gr{e}]) is constructed from \TE{u} (or $\Gamma$) by adding the typings $\gr{v}{:}\gr{e}$. The names \gr{v} must not occur in \TE{u} (or $\Gamma$) to the left of ``:''; the names to the left of ``:''\ of all typings in a typing environment are always pairwise different. \begin{figure} \rule{\textwidth}{1pt} \begin{gather} \dfrac{\sigma\le\pi \quad \rho\le\tau \quad \Gamma[u{:}\pi]\vdash\lst{\gr{e},P{:}\rho}}{ \Gamma[u{:}\sigma]\vdash\lst{\gr{e},P{:}\tau}} \ (\rho\text{ deterministic}) \tag{gen$_{\Gamma}$} \\ \dfrac{\TE{u}[u{:}\typ{\gr{\alpha}}{\gr{s}',\gr{t}}]\vdash \lst{\gr{e},P{:}\typ{\gr{\alpha}}{\gr{r},\gr{s}'}}}{ \TE{u}[u{:}\typ{\gr{\alpha}}{\gr{s},\gr{t}}]\vdash \lst{\gr{e},P{:}\typ{\gr{\alpha}}{\gr{r},\gr{s}}}} \ (\forall_x\,x^\infty\in\{\gr{s}\}\,\Rightarrow\,x^\infty\in\{\gr{r}\}) \tag{self$_{\Gamma}$} \\ \dfrac{\forall_{i=1..n}\,\Gamma[\gr{u}_i{:}\gr{\eta}_i, \gr{v}_i{:}\gr{\tau}_i]\vdash \lst{P_i{:}\typ{\gr{\alpha}}{\gr{s}_i}}}{ \Gamma\vdash\lst{\coll{\rcv{x_1}{\ulg{u}_1,\ulg{v}_1}.P_1,\dots, \rcv{x_n}{\ulg{u}_n,\ulg{v}_n}.P_n}\,{:}\,\typ{\gr{\alpha}}{\gr{r}}}} \ (1) \tag{sel$_{\Gamma}$} \\ \dfrac{\Gamma[u{:}\typ{\gr{\alpha}}{\gr{s}}\|\sigma]\vdash \lst{\gr{\varphi}{:}\gr{\eta},\gr{u}{:}(\subst{\gr{\varphi}}{\gr{v}} \gr{\tau}),P{:}\tau}}{ \Gamma[u{:}\typ{\gr{\alpha}}{\gr{r}}\|\sigma]\vdash \lst{\snd{u}{\msg{x}{\gr{\varphi},\gr{u}}}.P\,{:}\,\tau}} \ (\sign{x}{\ulg{v}{:}\gr{\eta},\gr{\tau}}\mset{\gr{s}}\in \act{\typ{\gr{\alpha}}{\gr{r}}}) \tag{send$_{\Gamma}$} \\ \dfrac{\TE{u}[v{:}\rho\|\sigma]\vdash \lst{\subst{v}{w}P{:}\tau} \quad \TE{u}[v{:}\rho,w{:}\sigma]\vdash\lst{Q{:}\tau}}{ \TE{u}[v{:}\rho,w{:}\sigma]\vdash \lst{\cond{v{=}w}{P}{Q}\,{:}\,\tau}} \ (u\neq w) \tag{cmp$_{\Gamma}$} \\ \dfrac{\Gamma[v{:}\mtyp]\vdash\lst{\subst{\sigma\|v}{u}P{:}\tau} \quad \Gamma[u{:}\mtyp]\vdash\lst{\sigma{:}\mtyp,Q{:}\tau}}{ \Gamma[u{:}\mtyp]\vdash\lst{\cond{u{\le}\sigma}{\ul{v}.P}{Q}\,{:}\,\tau}} \ (u\notin\free{\sigma}) \tag{sub$_{\Gamma}$} \\ \dfrac{\Gamma[v{:}\num]\vdash\lst{\subst{p+v}{u}P{:}\tau} \quad \Gamma[u{:}\num]\vdash\lst{p{:}\num,Q{:}\tau}}{ \Gamma[u{:}\num]\vdash\lst{\cond{u{\ge}p}{\ul{v}.P}{Q}\,{:}\,\tau}} \ (u\notin\free{p}) \tag{more1$_{\Gamma}$} \\ \dfrac{\Gamma[v{:}\num]\vdash\lst{\subst{v+1}{u}P{:}\tau} \quad \Gamma\vdash\lst{\subst{0}{u}Q{:}\tau}}{ \Gamma[u{:}\num]\vdash\lst{\cond{u{\ge}1}{\ul{v}.P}{Q}\,{:}\,\tau}} \tag{more2$_{\Gamma}$} \\ \smash[b]{\dfrac{\Gamma[u{:}\typ{\gr{\alpha}}{\gr{r}_j},\gr{u}{:}\gr{\eta}] \vdash\lst{\typ{\gr{\alpha}}{}{:}\mtyp,\gr{\varphi}{:}\gr{\eta}_j, \gr{w}{:}(\subst{\gr{\varphi}}{\gr{u}_j}\gr{\tau}_j),P{:}\tau} \quad \forall_{i=1..n}\,\TE{u}^i\vdash\lst{P_i{:}\typ{\gr{\alpha}}{\gr{r}_i}}}{ \Gamma[\gr{u}{:}\gr{\eta}]\vdash\lst{\new{\ul{u}}{\class{\rcv{x_1}{ \ulg{u}_1,\ulg{v}_1}.P_1,\dots,\rcv{x_n}{\ulg{u}_n,\ulg{v}_n}.P_n}{ \gr{\alpha}}}{\msg{x_j}{\gr{\varphi},\gr{w}}}.P\,{:}\,\tau}}} \ (2) \tag{intro$_{\Gamma}$} \\ \dfrac{\Gamma[u{:}\typ{\gr{\alpha}}{\gr{r}},v{:}\typ{\gr{\alpha}}{} \|\sigma]\vdash\lst{\gr{\varphi}{:}\gr{\eta},\gr{u}{:} (\subst{\gr{\varphi}}{\gr{v}}\gr{\tau}),P{:}\tau}}{ \Gamma[v{:}\typ{\gr{\alpha}}{}\|\sigma]\vdash \lst{\new{\ul{u}}{v}{\msg{x}{\gr{\varphi},\gr{u}}}.P\,{:}\,\tau}} \ (\coll{\gr{\alpha}}\equiv\coll{\creat{\sign{x}{\ulg{v}{:}\gr{\eta}, \gr{\tau}}}{\gr{r}},\gr{\gamma}}) \tag{new$_{\Gamma}$} \\ \dfrac{\TE{u}[u{:}\typ{\gr{\alpha}}{}\|\sigma]\vdash\lst{\gr{\varphi}{:} \gr{\eta},\gr{u}{:}(\subst{\gr{\varphi}}{\gr{v}}\gr{\tau}), \coll{}{:}\typ{}{}}}{ \TE{u}[u{:}\typ{\gr{\alpha}}{}\|\sigma]\vdash \lst{\call{\msg{x}{\gr{\varphi},\gr{u}}}\,{:}\, \typ{\gr{\alpha}}{\gr{r}}}} \ (\coll{\gr{\alpha}}\equiv\coll{\creat{\sign{x}{\ulg{v}{:}\gr{\eta}, \gr{\tau}}}{\gr{r}},\gr{\gamma}}) \tag{bec$_{\Gamma}$} \\ \dfrac{\Gamma[u{:}\sigma]\vdash\lst{\gr{e}}}{ \Gamma[u{:}\sigma\|\tau]\vdash\lst{u{:}\tau,\gr{e}}} \tag{obj$_{\Gamma}$} \\ \dfrac{\forall_{i=1..n}\,\Gamma[u{:}\mtyp,\gr{u}_i{:}\gr{\eta}_i]\vdash \lst{\gr{\tau}_i{:}\mtyp,\gr{v}_i{:}\num,\coll{}{:}\typ{}{}} \quad \Gamma\vdash\lst{\gr{w}{:}\num,\gr{e}}}{ \Gamma\vdash\lst{\sigma{:}\mtyp,\gr{e}}} \ (3) \tag{type$_{\Gamma}$} \\ \dfrac{\Gamma\vdash\lst{\sigma{:}\mtyp,\tau{:}\mtyp,\gr{e}}}{ \Gamma\vdash\lst{\sigma\|\tau{:}\mtyp,\gr{e}}} \tag{comb$_{\Gamma}$} \\ \dfrac{\Gamma[u{:}\mtyp]\vdash\lst{\gr{e}}}{ \Gamma[u{:}\mtyp]\vdash\lst{u{:}\mtyp,\gr{e}}} \tag{par$_{\Gamma}$} \\ \dfrac{\Gamma[\gr{u}{:}\num]\vdash\lst{\gr{e}}}{ \Gamma[\gr{u}{:}\num]\vdash\lst{p{:}\num,\gr{e}}} \ (\free{p}=\{\gr{u}\}) \tag{int$_{\Gamma}$} \end{gather} \vspace*{-3ex} \[ \begin{array}{@{}rl@{}} (1) & \act{\typ{\gr{\alpha}}{\gr{r}}}= \{\sign{x_1}{\ulg{u}_1{:}\gr{\eta}_1,\gr{\tau}_1}\mset{\gr{s}_1}, \dots,\sign{x_n}{\ulg{u}_n{:}\gr{\eta}_n,\gr{\tau}_n} \mset{\gr{s}_n}\} \\[.8ex] %\coll{\gr{\alpha}}\text{ deterministic} \\[.8ex] (2) & 1\le j\le n;\ \coll{\gr{\alpha}}\text{ deterministic};\ \free{\gr{\alpha}}\subseteq\{\gr{u}\};\ \TE{u}^i=\{u{:}\typ{\gr{\alpha}}{},\gr{u}{:}\gr{\eta},\gr{u}_i{:} \gr{\eta}_i,\gr{v}_i{:}\gr{\tau}_i\}_u; \\ & \coll{\gr{\alpha}}\equiv\coll{\creat{\sign{x_1}{\ulg{u}_1{:} \gr{\eta}_1,\gr{\tau}_1}}{\gr{r}_1},\dots, \creat{\sign{x_n}{\ulg{u}_n{:}\gr{\eta}_n,\gr{\tau}_n}}{\gr{r}_n}, \beh{a_1}{\gr{s}_1}{\gr{t}_1},\dots,\beh{a_m}{\gr{s}_m}{\gr{t}_m}} \\[.8ex] (3) & \sigma\cong\rec{u}\typ{\alpha_1,\dots,\alpha_n}{\gr{r}};\ \alpha_i=\creat{\sign{x_i}{\ulg{u}_i{:}\gr{\eta}_i,\gr{\tau}_i}}{ \gr{s}_i}\ (\text{assuming }\lvert\gr{r}_i\rvert=0)\text{ or} \\ & \alpha_i=\beh{\sign{x_i}{\ulg{u}_i{:}\gr{\eta}_i,\gr{\tau}_i}}{ \gr{r}_i}{\gr{s}_i};\ \{\gr{v}_i\}=\free{\gr{s}_i};\ \{\gr{w}\}=\free{\gr{r},\gr{r}_1,\dots,\gr{r}_n}%;\ i=1,\dots,n \end{array} \] \rule{\textwidth}{1pt} \caption{Type Checking Rules} \label{checking} \end{figure} An expression of the form $\TE{u}\vdash\lst{e_1,\dots,e_n,P{:}\tau}$ specifies that the additional checks (possibly causing modifications of \TE{u}) expressed by $e_1,\dots,e_n$ must be performed before checking $P{:}\tau$. Each $e_i$ is of the form $v{:}\sigma$ ($v$ is used as an argument and $\sigma$ is the corresponding parameter type), $\sigma{:}\mtyp$ ($\sigma$ is a free type to be substituted for a type parameter) or $p{:}\num$ ($p$ is a nonnegative integer to be substituted for an integer parameter). Rule (obj$_{\Gamma}$) deals with additional type checks of the form $u{:}\tau$. An object or object parameter $u$ is used as argument, introducing a new alias of $u$; the corresponding parameter type is $\tau$. The rule requires a typing $u{:}\sigma\|\tau$ to be in the typing environment; $u$'s type mark is split into $\sigma$ and $\tau$; the new type mark of $u$ in the typing environment becomes $\sigma$. Rule (gen$_{\Gamma}$) allows a type checker to use (weak) type equivalence to bring $u$'s type mark into the form needed by (obj$_{\Gamma}$). In fact, the type mark can safely be replaced with a supertype, but there is usually no need to do so. Rule (type$_{\Gamma}$) checks if an expression of the form $\rec{u}\typ{\alpha_1,\dots,\alpha_n}{\gr{r}}$ or \typ{\alpha_1,\dots,\alpha_n}{\gr{r}} actually is a type. Especially, it has to check if each parameter occurring free in the type occurs also in the typing environment with the appropriate meta-type. For each descriptor $\alpha_i$, the rule must check whether all expressions used as parameter types are types, and all expressions used as nonnegative integers are nonnegative integers. Before performing some of these checks, the type parameters and integer parameters are added to the typing environment. ($\Gamma\vdash\lst{\coll{}{:}\typ{}{}}$ holds for each $\Gamma$. $\coll{}{:}\typ{}{}$ is used only because the type checking rules assume that there is an expression of the form $P{:}\tau$.) According to (comb$_{\Gamma}$), an expression of the form $\sigma\|\tau$ is a type if $\sigma$ and $\tau$ are types. Rule (par$_{\Gamma}$) states that a name $u$ is a type only if the typing environment contains $u{:}\mtyp$. This check can be performed for nonnegative integer expressions by a single rule (int$_{\Gamma}$) because these expressions can contain only one kind of parameters. The remaining rules except (gen$_{\Gamma}$) and (self$_{\Gamma}$) deal with checking the (partial) correspondence between processes and types. Rule (sel$_{\Gamma}$) ensures that a process \coll{\gr{A}} has at least one guarded process for each enabled message descriptor in the corresponding type \typ{\gr{\alpha}}{\gr{r}}, and each guarded process in $\{\gr{A}\}$ corresponds to the type updated according to the accepted message. For example, \[ \Gamma\vdash\lst{\coll{\rcv{\text{put}}{\ul{v},\ul{w}}. \new{\ul{u}'}{u}{\msg{\text{init}}{}}.\call{\msg{\text{buf}}{0,v,u',w}},\; \rcv{\text{del}}{}.\coll{}}: \textit{BufIDC}\,\mset{\textrm{ok}^{[0]},\textrm{ok}^\infty}} \] (with \textit{BufIDC} as shown in \rsec{examples}) passes the type checker if \[ \Gamma[v{:}\mtyp,w{:}v]\vdash\lst{\new{\ul{u}'}{u}{\msg{\text{init}}{}}. \call{\msg{\text{buf}}{0,v,u',w}}:\textit{BufIDC}\, \mset{\textrm{ok}^{[0]},\textrm{ok}^\infty,\textrm{full}^1}} \] and $\Gamma\vdash\lst{\coll{}{:}\textit{BufIDC}\,\mset{}}$ because (after renaming the type parameter of ``put'') \[ \textit{enbl\,BufIDC}\,\mset{\textrm{ok}^{[0]},\textrm{ok}^\infty}= \{\sign{\textrm{put}}{\ul{v}{:}\mtyp,v}\mset{\textrm{ok}^{[0]}, \textrm{ok}^\infty,\textrm{full}^1},\;\sign{\textrm{del}}{}\mset{}\}. \] $\Gamma\vdash\lst{\coll{}{:}\textit{BufIDC}\,\mset{}}$ passes the checker simply because of $\textit{enbl\,BufIDC}\,\mset{}=\emptyset$. Rule (send$_{\Gamma}$) ensures that a message sent to an object with identifier $u$ corresponds to an enabled message descriptor in $u$'s type mark; $u$'s type mark is updated accordingly, the free types and nonnegative integers used as arguments are checked to be of the appropriate meta-types, and the object identifiers (or parameters) used as arguments are checked to have appropriate type marks. For example, $\Gamma[v'{:}\textit{Back}\,\mset{\textrm{one}^1}]\vdash \lst{\snd{v'}{\msg{\textrm{back}}{v,w}}.P:\tau}$ (with \textit{Back} as defined in \rsec{examples}) passes the type checker if $\Gamma[v'{:}\textit{Back}\,\mset{}]\vdash\lst{v{:}\mtyp,w{:}v,P{:}\tau}$. Rule (par$_{\Gamma}$) checks if $v{:}\mtyp$ has already been introduced into $\Gamma$; then, (obj$_{\Gamma}$) ensures that an expression $w{:}v\|\sigma$ (with $\sigma$ equal to \typ{}{} in this case) is in $\Gamma$ and replaces $w{:}v\|\sigma$ with $w{:}\sigma$ before checking $P{:}\tau$. Object identity comparisons are dealt with by (cmp$_{\Gamma}$): The typing environment must associate type marks with the compared names. The process $P$ is executed if the objects are identical; in this case one name is replaced with the other, and the names' type marks are combined. The replaced name must be different from the distinguished self reference so that this self reference remains in the typing environment. Type comparisons are dealt with by (sub$_{\Gamma}$): The type to the left of $\le$ in the comparison must be a type parameter. This type parameter $u$ is replaced with the combination of the type $\sigma$ to the right of $\le$ with the new type parameter (that will be replaced with the difference between $u$ and $\sigma$) in the process executed when the subtype relationship is satisfied. It is also checked whether $\sigma$ actually is a type without a free occurrence of $u$. Rule (more1$_{\Gamma}$) deals with nonnegative integer comparisons in much the same way as (sub$_{\Gamma}$) does for type comparisons. Rule (more2$_{\Gamma}$) is a specialization of (more1$_{\Gamma}$): In the process executed when the comparison is not satisfied, the integer parameter is known to be 0; this information may be needed when the acceptability of a message depends on the exact number of token symbols in a state, or the integer parameter occurs in a part size. Rule (intro$_{\Gamma}$) deals with object creation, where the behavior of the new object is explicitly specified. There must be at least one guarded process for each creator descriptor in \coll{\gr{\alpha}}, the deterministic static part of the new object's type. Each of these (guarded) processes is checked with a new typing environment that contains an initial type mark for the distinguished self reference $u$, type parameters and nonnegative-integer parameters selected form the current typing environment---at least those occurring free in \coll{\gr{\alpha}}---and the parameters of the guarded processes. The initial message sent to the new object must be specified in \coll{\gr{\alpha}}. The type \typ{\gr{\alpha}}{} is checked to be a type; hence, all \typ{\gr{\alpha}}{\gr{r}_i} also are types. The arguments of the initial message are checked in the same way as by (send$_{\Gamma}$), where the typing environment of the process $P$ is extended by the object parameter referring to the new object and its type mark. Rule (new$_{\Gamma}$) resembles (intro$_{\Gamma}$). However, a new object is created by cloning an existing one. It is checked whether the cloned object's (or the corresponding parameter's) type mark supports the initial message. Also, (bec$_{\Gamma}$) resembles (new$_{\Gamma}$) because changing the behavior is similar to cloning itself, except that no new object identity is introduced and no process remains to be checked. The type partially specifying the new behavior must (after accepting the initial message) be a subtype of the current type \typ{\gr{\alpha}}{\gr{r}}. These types can be made equal by applying (gen$_{\Gamma}$) before (bec$_{\Gamma}$). Rule (gen$_{\Gamma}$) allows type marks to be replaced with corresponding supertypes and types partially specifying object behavior with corresponding subtypes. In an expression $P{:}\tau$, creator descriptors occurring in $\tau$ are not used, except in (bec$_{\Gamma}$). But this rule requires the creator descriptors to be the same as in the type mark of the distinguished self reference. Rule (self$_{\Gamma}$) allows the type mark of the distinguished self reference and the type partially specifying object behavior to be changed in the same way. Arbitrary tokens can be removed from and added to the states of these types simultaneously. A token removed from the state of the self reference' type mark can safely be removed from the other type because a message depending on this token can no longer be sent by an object to itself through the self reference; the object need not be able to deal with that message. On the other side, if tokens are added to the type partially specifying object behavior, an object of this type can deal with all additional messages depending on the added tokens; it is safe to add these tokens also to the state of the self reference' type mark so that these messages actually can be sent. A typical use of (self$_{\Gamma}$) is demonstrated by an example (part of the dining philosophers example in \rfig{phil}): \[ \TE{u}[u{:}\textit{PhilC}\,\mset{},\,v{:}\textit{Phil}\,\mset{},\, w{:}\textit{Fork}\,\mset{\text{down}}]\vdash \lst{\snd{v}{\msg{\textrm{ask}}{u}}.\call{\msg{\text{hungry}}{v,w}} {:}\textit{PhilC}\,\mset{\text{br}^1}}. \] First, (send$_{\Gamma}$) is applied. It remains to show \[ \TE{u}[u{:}\textit{PhilC}\,\mset{},\,v{:}\textit{Phil}\,\mset{},\, w{:}\textit{Fork}\,\mset{\text{down}}]\vdash \lst{u{:}\textit{Phil}\,\mset{\text{hungry}^1},\, \call{\msg{\text{hungry}}{v,w}}{:}\textit{PhilC}\,\mset{\text{br}^1}}. \] Since \textit{Phil}\mset{\text{hungry}^1} is not a supertype of \textit{PhilC}\mset{}, but a supertype of \textit{PhilC}\mset{\text{hungry}^1}, (self$_{\Gamma}$) is applied in order to add hungry$^1$ to the state of the self reference's type mark. It remains to show \[ \begin{array}{@{}l@{}} \TE{u}[u{:}\textit{PhilC}\,\mset{\text{hungry}^1},\,v{:}\textit{Phil}\, \mset{},\,w{:}\textit{Fork}\,\mset{\text{down}}]\vdash{} \\ \hspace*{6em} \lst{u{:}\textit{Phil}\,\mset{\text{hungry}^1},\, \call{\msg{\text{hungry}}{v,w}}{:} \textit{PhilC}\,\mset{\text{br}^1,\text{hungry}^1}} \end{array} \] by applying (obj$_{\Gamma}$) and (bec$_{\Gamma}$). It remains to show \[ \TE{u}[u{:}\textit{PhilC}\,\mset{},\,v{:}\textit{Phil}\,\mset{},\, w{:}\textit{Fork}\,\mset{\text{down}}]\vdash \lst{v{:}\textit{Phil}\,\mset{},\,w{:}\textit{Fork}\,\mset{\text{down}},\, \coll{}{:}\typ{}{}}. \] by applying twice (obj$_{\Gamma}$) and then (sel$_{\Gamma}$). \subsection{Type Consistency of Initial Configurations} \label{proof} The type checking rules in \rfig{checking} applied to initial configurations can actually ensure type consistency: \begin{theorem} \label{thm1} Let $E$ be an initial configuration of the form $\{u_1\mapsto({;}P_1{;}),\dots,u_n\mapsto({;}P_n{;})\}$, and $\tau_1,\dots,\tau_n$ and $\sigma_{1,1},\dots,\sigma_{n,n}$ types, where $\tau_i\le\sigma_{i,1}\|\dots\|\sigma_{i,n}$ and each $\tau_i$ is deterministic and of the form \typ{\beh{a_1}{\gr{s}_1}{\gr{t}_1},\dots, \beh{a_m}{\gr{s}_m}{\gr{t}_m}}{\gr{r}}, such that $\{u_1{:}\sigma_{1,i},\dots,u_n{:}\sigma_{n,i}\}_{u_i}\vdash \lst{P_i{:}\tau_i}$ for $i=1,\dots,n$. Then, $E$ is type consistent. \end{theorem} The proof by case analysis is sketched. For each system configuration $F$ and each expression of the form $u\mapsto(\gr{A};\coll{\gr{B}};\nu,\gr{\mu})$ or $u\mapsto(\gr{A};P;\gr{\mu})$ ($P$ not of the form \coll{\gr{B}}) in $F$ it has to be shown that (case a) there exists a system configuration $G$ with $F\trans{u}G$ or (case b) $E\trans{*}F$ cannot hold under the conditions of \rthm{thm1}. (Case 1) Let $v\mapsto(\gr{A};\coll{\gr{B}};\msg{x}{\gr{\varphi},\gr{v}},\gr{\mu})$ be in $F$. If $\{\gr{B}\}$ contains an expression $\rcv{x}{\ulg{w}}.P$ with $\lvert\gr{w}\rvert=\lvert\gr{\varphi},\gr{v}\rvert$, (case a) there is a $G$ with $F\trans{u}G$. Otherwise (case b) let $E\trans{*}F$ and $\TE{v}\vdash\lst{\coll{\gr{B}}{:}\typ{\gr{\alpha}}{\gr{r}}}$ for some typing environment $\TE{v}$ and type $\typ{\gr{\alpha}}{\gr{r}}$. The rule (sel$_{\Gamma}$) requires that $\coll{\gr{B}}$ contains at least one guarded process satisfying the condition of case a) for each expression in $\act{\typ{\gr{\alpha}}{\gr{r}}}$. (Initial messages are handled in a similar way by rule (intro$_{\Gamma}$) for all creator descriptors.) In case b) it must be assumed that there is no expression $\sign{x}{\ulg{u}'{:}\gr{\eta},\gr{\rho}}\mset{\gr{s}}$ with $\lvert\gr{\eta},\gr{\rho}\rvert=\lvert\gr{\varphi},\gr{v}\rvert$ in $\act{\typ{\gr{\alpha}}{\gr{r}}}$ (and there is no creator descriptor $\creat{\sign{x}{\ulg{u}'{:}\gr{\eta},\gr{\rho}}}{\gr{s}}$ in $\{\gr{\alpha}\}$). The type \typ{\gr{\alpha}}{\gr{r}} is deterministic, no matter if it is equal to some $\tau_i$, has been introduced according to (intro$_{\Gamma}$) or modified according to (self$_{\Gamma}$). Some object $u$ must have sent $\msg{x}{\gr{\varphi},\gr{v}}$ to $v$. Rule (send$_{\Gamma}$) requires $v'{:}\tau\in\TE{u}'$, where $v'$ is equal to $v$ or has been replaced with $v$ during execution, $\TE{u}'$ is the typing environment of the sender $u$, and $\tau$ is a subtype of some type $\typ{\beta}{\gr{r}'}$ with $\sign{x}{\ulg{u}'{:}\gr{\eta},\gr{\pi}} \mset{\gr{t}}\in\act{\typ{\beta}{\gr{r}'}}$ ($\gr{\pi}\le\gr{\rho}$). (Sending initial messages by (intro$_{\Gamma}$) and (new$_{\Gamma}$) and changing the behavior by (bec$_{\Gamma}$) have the same requirements, and the types $\tau_i$ do not contain creator descriptors.) The typing $v'{:}\tau$ can be introduced into $\TE{u}'$ (if it is not there from the beginning) as a parameter of a message or the identifier of a new object. Let us ignore type updating for the moment. An analysis of the rules in \rfig{checking} shows in each case $\typ{\gr{\alpha}}{\gr{r}}\le\sigma$, where $\sigma$ is constructed from $\tau$ by substituting type parameters and integer parameters. When ignoring type updating, $E\trans{*}F$ is a contradiction in case b) because it is not possible that a supertype of $\tau$ contains a message descriptor $\beh{\sign{x}{\ulg{u}'{:}\gr{\eta},\gr{\pi}}}{\gr{t}'}{\gr{t}}$ with \sign{x}{\ulg{u}'{:}\gr{\eta},\gr{\pi}} enabled, while a type (strongly) type-equivalent to $\typ{\gr{\alpha}}{\gr{r}}$ contains no message descriptor $\beh{\sign{x}{\ulg{u}'{:}\gr{\eta},\gr{\rho}}}{\gr{s}'}{\gr{s}}$ with \sign{x}{\ulg{u}'{:}\gr{\eta},\gr{\rho}} enabled. Now let us consider type updating. Types are checked when all message queues are empty. Rule (obj$_{\Gamma}$) together with the other rules ensures that all type marks are split whenever a new alias of an element of $\mathbb{V}$ is introduced (i.\,e., for each occurrence of an object identifier or parameter as argument). The object with identifier $v$ behaves according to a deterministic type $\typ{\gr{\alpha}}{\gr{r}}$ with $\typ{\gr{\alpha}}{\gr{r}}\le\sigma_1\|\dots\|\sigma_n$, where $\sigma_1,\dots,\sigma_n$ are the type marks of all identifiers to be replaced with $v$ (after substituting type parameters). Since $\typ{\gr{\alpha}}{\gr{r}}$ is deterministic, rule (obj$_{\Gamma}$) updates the type marks $\sigma_1,\dots,\sigma_n$ of all aliases in the same way as rule (sel$_{\Gamma}$) does for $\typ{\gr{\alpha}}{\gr{r}}$ (\rprp{prp:det-seq}). $\typ{\gr{\alpha}}{\gr{r}'}\le\sigma'_1\|\dots\|\sigma'_n$ holds for $\typ{\gr{\alpha}}{\gr{r}'}$ and $\sigma'_1,\dots,\sigma'_n$ constructed by updating $\typ{\gr{\alpha}}{\gr{r}}$ and $\sigma_1,\dots,\sigma_n$, respectively. Hence, $E\trans{*}F$ is a contradiction in case b) even if type updating is considered. (Case 2) Let $v\mapsto(\gr{A};\snd{u}{\xi}.P;\gr{\mu})$ be in $F$. If $u\mapsto(\gr{B};R;\gr{\nu})\in F$ for some $(\gr{B};R;\gr{\nu})$, (case a) there is a $G$ with $F\trans{v}G$. Otherwise (case b) let $E\trans{*}F$ and $\TE{v}\vdash\lst{\snd{u}{\xi}.P{:}\tau}$ for some $\TE{v}$ and $\tau$. Rule (send$_{\Gamma}$) requires $u{:}\sigma\in\TE{v}$. If $u{:}\sigma$ is not in $\TE{v}$ from the beginning (i.\,e.\ $u\in\{u_1,\dots,u_n\}$), it is introduced for identifiers of newly created objects and for parameters to be substituted by object identifiers. The rules in \rfig{checking} ensure that the typing environments contain expressions of the form $w{:}\rho$ for all arguments $w$ substituting such parameters. Thus, there is an object for each $u{:}\sigma\in\TE{v}$, and $E\trans{*}F$ is a contradiction in case b). (Case 3) If an expression $v\mapsto(\gr{A};\cond{u{=}w}{P}{R};\gr{\mu})$ or $v\mapsto(\gr{A};\cond{\sigma{\le}\tau}{\ul{w}.P}{R};\gr{\mu})$ or $v\mapsto(\gr{A};\cond{p{\ge}q}{\ul{w}.P}{R};\gr{\mu})$ or $v\mapsto(\gr{A};\new{\ul{u}}{\class{\gr{B}}{\gr{\alpha}}}{\gr{\xi}}.P; \gr{\mu})$ or $v\mapsto(\gr{A};\call{\gr{\xi}};\gr{\mu})$ is in $F$, there always is a $G$ with $F\trans{v}G$. (Case 4) Let $v\mapsto(\gr{A};\new{\ul{w}}{u}{\gr{\xi}}.P;\gr{\mu})$ be in $F$. If $v=u$ or $u\mapsto(\gr{B};R;\gr{\nu})\in F$ for some $(\gr{B};R;\gr{\nu})$, there is a $G$ with $F\trans{v}G$. The proof of the other case corresponds to that of case 2b). \qed \rthm{thm1} shows not only that the type checking rules can be applied to ensure that an initial configuration is type-consistent, but also that the type system supports separate compilation: The rules are applied separately to each $P_i$ representing a program module in the initial configuration. Let an initial configuration of the form $\{u_1\mapsto({;}P_1{;}),\dots,u_i\mapsto({;}P_i{;}),\dots,u_n\mapsto({;} P_n{;})\}$ and the types $\tau_1,\dots,\tau_n$ and $\sigma_{1,1},\dots,\sigma_{n,n}$ satisfy the conditions of \rthm{thm1}, and let $P'_i$ be a process and $\tau'_i$ a type with $\{u_1{:}\sigma_{1,i},\dots,u_n{:}\sigma_{n,i}\}_{u_i}\vdash\lst{P'_i{:} \tau'_i}$ and $\tau'_i\le\tau_i$. Then, the initial configuration $\{u_1\mapsto({;}P_1{;}),\dots,u_i\mapsto({;} P'_i{;}),\dots,u_n\mapsto({;}P_n{;})\}$ also satisfies the conditions of \rthm{thm1}, and this configuration is type-consistent. \subsection{Decidability} \label{algorithm} %If a type checker based on the rules in \rfig{checking} proves that a given %initial configuration and given types satisfy the conditions of \rthm{thm1}, %then this configuration is type-consistent. %But, so far we do not know if and under which conditions a type checker %terminates, i.\,e., type checking is decidable. Before dealing with the decidability of type checking, it must be shown that $\sigma\equiv_{\text{t}}\tau$, $\sigma\cong\tau$ and $\sigma\le\tau$ are decidable for arbitrary finite types $\sigma$ and $\tau$. \begin{figure} \rule{\textwidth}{1pt} \begin{align} \coll{\gr{\alpha},\beta,\beta} &\to \coll{\gr{\alpha},\beta} \tag{dupl$_{\to}$} \\ p+n+n' &\to p+m \quad (m=n+n') \tag{add$_{\to}$} \\ \mset{\gr{r},x^p,x^q} &\to \mset{\gr{r},x^{p+q}} \tag{sum$_{\to}$} \\ \mset{\gr{r},x^0} &\to \mset{\gr{r}} \tag{null$_{\to}$} \\ \mset{\gr{r},x^\infty,x^\infty} &\to \mset{\gr{r},x^\infty} \tag{infinity1$_{\to}$} \\ \mset{\gr{r},x^\infty,x^p} &\to \mset{\gr{r},x^\infty} \tag{infinity2$_{\to}$} \\ \mset{\gr{r},x^{[p+n]},x^{[p+n]}} &\to \mset{\gr{r},x^{[p+m]}} \quad (m=n-1) \tag{split$_{\to}$} \\ \subst{\rec{u}\typ{\gr{\alpha}}{\gr{r}}}{u}\typ{\gr{\alpha}}{\gr{r}} &\to \rec{u}\typ{\gr{\alpha}}{\gr{r}} \quad (u\in\free{\typ{\gr{\alpha}}{\gr{r}}}) \tag{rec1$_{\to}$} \\ \rec{u}\typ{\gr{\alpha}}{\gr{r}} &\to \typ{\gr{\alpha}}{\gr{r}} \quad (u\notin\free{\typ{\gr{\alpha}}{\gr{r}}}) \tag{rec2$_{\to}$} \\ \tau\|\typ{}{} &\to \tau \tag{zero$_{\to}$} \\ \typ{\gr{\alpha}}{\gr{r}}\|\typ{\gr{\gamma}}{\gr{s}} &\to \typ{\gr{\alpha},\gr{\gamma}}{\gr{r},\gr{s}} \quad (1) \tag{comb1$_{\to}$} \\ \typ{\gr{\alpha}}{\gr{r}}\|\rec{u}\typ{\gr{\gamma}}{\gr{s}} &\to \typ{\gr{\alpha}, \subst{\rec{u}\typ{\gr{\gamma}}{\gr{s}}}{u}\gr{\gamma}}{\gr{r},\gr{s}} \quad (1) \tag{comb2$_{\to}$} \\ \rec{u}\typ{\gr{\alpha}}{\gr{r}}\|\rec{v}\typ{\gr{\gamma}}{\gr{s}} &\to \typ{(\subst{\rec{u}\typ{\gr{\alpha}}{\gr{r}}}{u}\gr{\alpha}), \subst{\rec{v}\typ{\gr{\gamma}}{\gr{s}}}{v}\gr{\gamma}}{\gr{r},\gr{s}} \quad (1) \tag{comb3$_{\to}$} \\ \typ{\gr{\alpha}}{\gr{r},s} &\to \typ{\gr{\alpha}}{\gr{r}} \quad (s\notin\relevant{\gr{\alpha}}) \tag{state1$_{\to}$} \\ \rec{u}\typ{\gr{\alpha}}{\gr{r},s} &\to \rec{u}\typ{\gr{\alpha}}{\gr{r}} \quad (s\notin\relevant{\gr{\alpha}}) \tag{state2$_{\to}$} %\\ \end{align} (1)\quad $ \begin{array}[t]{@{}l@{\ }l} \gr{r}\in\relevant{\gr{\alpha}}; & \forall_{x,p}\,x^{[p]}\in\{\gr{r}\}\,\Rightarrow\, (x^{[0]}\notin\relevant{\gr{\gamma}}\,\vee\, \exists_{q}\,x^{[q]}\in\{\gr{s}\}); \\ \gr{s}\in\relevant{\gr{\gamma}}; & \forall_{x,p}\,x^{[p]}\in\{\gr{s}\}\,\Rightarrow\, (x^{[0]}\notin\relevant{\gr{\alpha}}\,\vee\, \exists_{q}\,x^{[q]}\in\{\gr{r}\}) \end{array} $ \\[2ex] \rule{\textwidth}{1pt} \caption{Rewrite Rules for Type Normalization} \label{rewrite} \end{figure} The first step in deciding strong type equivalence is to bring the types in \emph{strong normal form.} The strong normalization procedure repeatedly applies the rewrite rules in \rfig{rewrite} and the equivalences \begin{itemize} \item $\alpha$-conversion, \item associativity and commutativity of $\|$ and $+$, and \item reordering of descriptors in static type parts \coll{\gr{\alpha}} and tokens in multi-sets \mset{\gr{r}}, \end{itemize} until no further application of the rewrite rules is possible. The resulting type $\tau'$ is in strong normal form. Obviously, $\tau\equiv_{\text{t}}\tau'$ holds because the rewrite rules in \rfig{rewrite} are just directed versions of rules in \rdef{def:eqv} and \rfig{equiv}, some of them combined with (rec$_{\cong}$). If the rewrite rules and equivalences of the strong normalization procedure are applied in different orderings, the results are equal up to the above list of equivalences. Two types are strongly type-equivalent if and only if the corresponding types in strong normal form are equal up to these equivalences. Of course, strong equivalence of types in strong normal form is decidable. It is possible to find a rating of all type expressions such that the rating of a type which matches the left hand side of a rewrite rule is strictly larger than the rating of the corresponding type at the right hand side. (Only (comb2$_{\to}$) and (comb3$_{\to}$) need a little thought.) Thus, and because the function \textit{eff} and all side-conditions of the rules are easily decidable, the strong normalization procedure always terminates and $\sigma\equiv_{\text{t}}\tau$ is decidable for arbitrary finite types $\sigma$ and $\tau$. To decide weak type equivalence, the types are brought into \emph{weak normal form.} The weak normalization procedure repeatedly applies the above equivalences, the rewrite rules in \rfig{rewrite} and the additional rewrite rule % \begin{align} \rec{u}\typ{\gr{\alpha},\gr{\gamma}}{\gr{r}} \to \rec{u}\typ{\gr{\alpha}}{\gr{r}} \quad (\forall_{\gamma\in\{\gr{\gamma}\}} \exists_{\alpha\in\{\gr{\alpha}\}}\, \Pi,\relevant{\gr{\alpha}}\vdash\alpha\succeq\gamma) \tag{red$_{\to}$} \end{align} % (with $\Pi,T\vdash\alpha\succeq\gamma$ as defined in \rdef{def:weak}) until no further application of the rewrite rules is possible. The additional rule is a directed version of the rule in \rdef{def:weak}. It depends on an environment $\Pi$ of subtyping assumptions on names. Two types are weakly type-equivalent (based on an environment of subtyping assumptions $\Pi$) if and only if the corresponding types in weak normal form are equal up to the above equivalences. To decide $\Pi,T\vdash\alpha\succeq\gamma$, it is necessary to decide subtyping on parameter types, depending on $\Pi$. Weak type equivalence is decidable if and only if subtyping of parameter types is decidable. Decidability of subtyping in conventional type systems (based on finite trees) has been addressed by Amadio and Cardelli in \cite{AmCa91}. The proof of decidability of subtyping in the proposed type system goes along the lines of their proof. The major difference from Amadio and Cardelli's notion of subtyping is rule (sub$_{\le}$): $\Pi\vdash\sigma\le\tau$ holds if there is a type $\rho$ with $\Pi\vdash\sigma\cong\tau\|\rho$. The difficult part is to find an appropriate $\rho$. As mentioned in \rsec{typing}, if $\sigma$ is of the form \typ{\gr{\alpha}}{\gr{r}} (or \rec{u}\typ{\gr{\alpha}}{\gr{r}}), there is an appropriate type $\rho$ of the form \typ{\gr{\alpha}}{\gr{s}} (or \rec{u}\typ{\gr{\alpha}}{\gr{s}}) such that there is a $\mset{\gr{t}}$ with $\mset{\gr{r}}\equiv\mset{\gr{s},\gr{t}}$. In general, if $\sigma$ is of the form $\sigma_1\|\dots\|\sigma_n\|u_1\|\dots\|u_m$ and each $\sigma_i$ ($1\le i\le n$) of the form \typ{\gr{\alpha}_i}{\gr{r}_i} or \rec{v_i}\typ{\gr{\alpha}_i}{\gr{r}_i}, there is an appropriate type $\rho$ of the form $\rho_1\|\dots\|\rho_n\|u_{i_1}\|\dots\|u_{i_j}$, where $\rho_i$ is of the form \typ{\gr{\alpha}_i}{\gr{s}_i} or \rec{u_i}\typ{\gr{\alpha}_i}{\gr{s}_i} such that there are $\mset{\gr{t}_i}$ with $\mset{\gr{r}_i}\equiv\mset{\gr{s}_i,\gr{t}_i}$, and $i_1,\dots,i_j$ are pairwise different indexes in the range $1,\dots,m$. The names $u_{i_1}\|\dots\|u_{i_j}$ are exactly those names occurring at the top level in $\sigma$, but not in $\tau$. The tokens $\gr{s}_i$ (which represent tokens available in $\sigma$, but not in $\tau$) can be computed as a side-effect of deciding weak type equivalence. Therefore, an appropriate type $\rho$ can always be found in a finite number of steps. Subtyping based on $\Pi$ is decidable if weak type equivalence based on $\Pi$ is decidable; and weak type equivalence is decidable if subtyping of parameter types is decidable. Thus, subtyping and weak type equivalence are decidable for finite types, because in finite types there is a limited number of parameter levels. The type checking rules in \rfig{checking} specify a type checking algorithm: When the expression below the horizontal line of a rule matches the expression to be checked and the side-conditions are satisfied, the rule can be applied and the corresponding expressions above the horizontal line are checked. Type checking succeeds if no expression remains to be checked after (repeatedly) applying rules. Type checking fails if for all possible repeated rule applications there always remain expressions that cannot be removed by applying any rule. Provided that subtyping is decidable, it is not very difficult to see that $\TE{u}\vdash\lst{\gr{e},P{:}\tau}$ is decidable if \TE{u} and \lst{\gr{e},P{:}\tau} are finite: Except for (gen$_{\Gamma}$) and (self$_{\Gamma}$), each application of a type checking rule in \rfig{checking} to $\TE{u}\vdash\lst{\gr{e},P{:}\tau}$ creates a finite number of $\TE{u'}'\vdash\lst{\gr{e}',P'{:}\tau'}$ that remain to be checked. Each \lst{\gr{e}',P'{:}\tau'} is in some way smaller than \lst{\gr{e},P{:}\tau}: When applying (sel$_{\Gamma}$), (send$_{\Gamma}$), (cmp$_{\Gamma}$), (sub$_{\Gamma}$), (more1$_{\Gamma}$), (more2$_{\Gamma}$), (intro$_{\Gamma}$), (new$_{\Gamma}$) or (bec$_{\Gamma}$), the process $P$ becomes smaller, but expressions \gr{e} can be added. When applying (obj$_{\Gamma}$), (par$_{\Gamma}$) or (int$_{\Gamma}$), expressions are removed from \gr{e}, while $P$ remains unchanged. When applying (type$_{\Gamma}$) or (comb$_{\Gamma}$), an expression in \gr{e} is replaced with a list of parts of this expression. Since \lst{\gr{e},P{:}\tau} is finite, each sequence of applications of these rules is finite. It remains to consider (gen$_{\Gamma}$) and (self$_{\Gamma}$). A single application of one of these rules can have the same effect as the repeated application of the rule (without applying other rules in between). Each sequence of rule applications is finite if (gen$_{\Gamma}$) and (self$_{\Gamma}$) are applied at most once between applications of other rules. The side-conditions of the rules are easily decidable. Thus, type checking is decidable if typing environments, processes and types are finite. %However, when using some of the rules it is necessary to make correct %predictions to get successful derivations. %For example, using (gen$_{\Gamma}$) it is necessary to predict the type that %partially specifies the same behavior specified by the checked process at the %needed degree of abstraction. %When the rule is applied, this information is, in general, not available. \section{Related Work} \label{related} Much work on types for concurrent languages has been done. The majority of this work is based on Milner's $\pi$-calculus \cite{MiPW92,Miln91} and similar calculi. Especially, the problem of inferring most general types was considered by Gay~\cite{Gay93} and Vasconcelos and Honda~\cite{VaHo93}. Nierstrasz~\cite{Nier93}, Pierce and Sangiorgi~\cite{PiSa93}, Vasconcelos~\cite{Vasc94} and Kobayashi and Yonezawa~\cite{KoYo94} deal with subtyping in such calculi. But their type models differ in an important aspect from the one presented in this work: They are not able to represent constraints on the ordering of messages and, therefore, cannot ensure that all sent messages can be processed. The proposal of Kobayashi and Yonezawa~\cite{KoYo94} supports subtyping in a similar way as sequential object-oriented languages based on a typed $\lambda$-calculus: A type of an active object specifies the set of messages that will be accepted by all instances; a subtype specifies an extended set of messages. Messages in the message queue can be processed in an ordering different from the ordering the messages were sent, as required by synchronization constraints. Their type system, like many similar approaches \cite{Caro93,Meye93}, does not ensure that each received message will eventually be processed. The widely known work of Liskov and Wing on behavioral subtyping \cite{LiWi94} shows the importance of ``constraints'' in subtyping: Preconditions, postconditions and invariants on methods are not sufficient to specify an object's behavior at the presence of subtyping and aliases or concurrent execution. A large amount of work based on ``path expressions'' \cite{CaHa74,BoPS81} and, more recently, process algebra \cite{BaWe90,Miln89} shows that reasoning about the order of messages in concurrent systems is quite difficult. Not much work was done on type models able to deal with constraints on the ordering of messages because of the difficulty of this problem. Nierstrasz~\cite{Nier93} argues that it is essential for a type model to regard an object as a process in a process calculus. He proposes ``regular types'' and ``request substitutability'' as foundations of subtyping. However, his very general results are not concrete enough to develop a static type system from them. Another similar definition of subtyping was given by Bowman et al.~\cite{BBDS97}. In general, subtyping according to this definition is not decidable. The proposal of Nielson and Nielson~\cite{NiNi93,NiNi94} also can deal with constraints on the ordering of messages. Types in their proposal are based on a process algebra, and a type checker updates type information while walking through a process expression. %However, their proposal does not control aliases; types are regarded as %contracts between an object and a single user, not as a contract between %an object and the whole set of its users. Their type model cannot ensure that all sent messages are understood. But, subtyping is supported so that instances of subtypes preserve the properties expressed in supertypes; if a program corresponding to a supertype sends only understood messages, also a program corresponding to a subtype does so. Because types in their model specify the communication between processes completely, subtyping is rather restricted; a subtype cannot specify additional message orderings and messages. The original process type model~\cite{PuntFORTE95,PuntFMOODS96} (where types are expressions in a process calculus) considers constraints on the ordering of messages, supports subtyping and ensures that all sent messages are understood. But there are some problems with that model: The support of coordinating clients is restricted because it is not possible to combine (the equivalent of) type marks, and recursive types are supported only in some special cases. The work presented in \cite{PuntECOOP97} improves that model. To provide better support of coordination it was necessary to apply a different type representation. To support recursive types, the notion of type equivalence had to be relaxed. A further improved process type model is presented in this article. One improvement concerns dynamic aspects of the type model: Clients can use dynamic type information available only at run time, and objects can dynamically modify their own types. The expressiveness was increased by allowing the acceptability of messages to depend on exact numbers of available token symbols. Furthermore, this article describes the process type model in more detail. %and uses a simpler set of type checking rules than was used in previous work. The proposal of Najm and Nimour \cite{NaNi97} has a similar purpose as process types. However, their approach does not support type splitting and type combination. At each time there can be only one client interacting with a server through an interface if the set of acceptable messages changes. Hence, clients can coordinate themselves only in a very limited way. The restriction to one client per interface is a consequence of problems caused by aliasing. The need for protecting objects against aliasing was detected earlier, and mechanisms for alias protection like ``islands'' were proposed \cite{Hogg91}. Unlike the islands approach, process types do not restrict aliasing to small islands. \section{Conclusions} The results of this work show that it is indeed feasible to regard a type as a contract between an (active) object and the unity of all clients. Types specify constraints on the expected orderings of messages. A type checker can ensure statically that concurrent clients are coordinated so that all sequences of messages sent to an object conform to the object's type, and the object accepts all type-conforming messages. Subtyping, genericity and separate compilation are supported. \bibliography{types} \bibliographystyle{plain} \begin{figure} \rule{\textwidth}{1pt} \[ \begin{array}{@{}l@{\quad}l@{}} a,b,c,\dots & \text{message signature (\rfig{syntax})} \\ e,f,g,h,\dots & \text{arbitrary expression} \\ i,j,m,n,\dots & \text{nonnegative integer} \\ p,q,\dots & \text{element of $\mathbb{I}$ (nonnegative integer expression, \rfig{syntax})} \\ r,s,t,\dots & \text{token (\rfig{syntax})} \\ u,v,w,\dots & \text{element of $\mathbb{V}$ (parameter or object identifier, \rsec{notation})} \\ x,y,z,\dots & \text{element of $\mathbb{C}$ (constant symbol, \rsec{notation})} \\ A,B,C,\dots & \text{guarded process expression (\rfig{syntax})} \\ E,F,G,\dots & \text{system configuration (\rsec{semantics})} \\ P,Q,R,\dots & \text{non-guarded process expression (\rfig{syntax})} \\ \alpha,\beta,\gamma,\dots & \text{(message or creator) descriptor (\rfig{syntax})} \\ \eta,\dots & \text{meta-type ``\mtyp'' or ``\num'' (\rfig{syntax})} \\ \mu,\nu,\xi,\dots & \text{message (\rfig{syntax})} \\ \pi,\rho,\sigma,\tau,\dots & \text{type expression (\rfig{syntax})} \\ \varphi,\dots & \text{type or nonnegative integer expression (\rfig{syntax})} \\ \TE{u},\Gamma & \text{typing environment; self reference $u$ (\rsec{rules})} \\ \Pi & \text{environment for subtyping (\rdef{def:subtyping})} \\ \mathbb{C} & \text{set of constant symbols ($\mathbb{C}\cap\mathbb{V}=\emptyset$, \rsec{notation})} \\ \mathbb{I} & \text{set of nonnegative integer expressions (\rsec{notation})} \\ \mathbb{V} & \text{infinite set of parameters and object identifiers (\rsec{notation})} \\ \gr{e} & \text{abbreviation of $e_1,\dots,e_n$ for arbitrary $n$ ($n\ge0$, \rsec{notation})} \\ \num & \text{the (meta-)type of all nonnegative integer expressions} \\ \mtyp & \text{the (meta-)type of all type expressions} \\ \cseq{\tau} & \text{the set of all message signature sequences conforming to $\tau$ (\rdef{seq})} \\ \relevant{\gr{\alpha}} & \text{the set of tokens effective in \coll{\gr{\alpha}} (\rsec{typing})} \\ \act{\typ{\gr{\alpha}}{\gr{r}}} & \text{the set of enabled message signatures with follow-states (\rdef{def:enabled})} \\ \free{\gr{e}} & \text{the set of all names occurring free in \gr{e} (\rsec{notation})} \\ \seq{\tau} & \text{the set of all message signature sequences specified by $\tau$ (\rdef{seq})} \\ \emptyset & \text{the empty set} \\ \{\gr{e}\} & \text{the smallest set containing the expressions \gr{e} (\rsec{notation})} \\ \lvert\gr{e}\rvert & \text{$n$, where $\gr{e}$ is an abbreviation of $e_1,\dots,e_n$ (\rsec{notation})} \\ \subst{\gr{e}}{\gr{u}}f & \text{simultaneous substitution of $\gr{e}$ for all free names $\gr{u}$ in $f$ (\rsec{notation})} \\ e\equiv f & \text{general equivalence relation on expressions (\rdef{def:eqv})} \\ \sigma\equiv_{\text{t}}\tau & \text{strong type equivalence relation (\rdef{equiv-rel})} \\ \sigma\cong\tau & \text{weak type equivalence relation (\rdef{def:weak})} \\ \sigma\le\tau & \text{subtyping relation, $\sigma$ is a subtype of $\tau$ (\rdef{def:subtyping})} \\ \lst{\gr{a}}\otimes\lst{\gr{c}} & \text{the set of all arbitrary interleavings of $\lst{\gr{a}}$ with \lst{\gr{c}} (\rsec{sequences})} \\ E\trans{u}F & \text{single-$u$-execution-step relation on system configurations (\rdef{def:exec})} \\ E\trans{*}F & \text{execution relation on system configurations (\rdef{def:exec})} % \Rightarrow & \text{logical implication} \end{array} \] \rule{\textwidth}{1pt} \caption{Symbols and Notation} \label{symbols} \end{figure} \end{document} % LocalWords: genericity iconify uniconify supertype Hoare Milner supertypes % LocalWords: interleavings displ Buf def BufI BufID ok BufD del mark's BufIB % LocalWords: BufIDC buf rec br PhilC phil reference's LR equiv eq assoc comm % LocalWords: assmp enablement prp otimes det le sel typings gen cmp bec obj % LocalWords: thm dupl eqv Amadio Cardelli Cardelli's Milner's Vasconcelos al % LocalWords: Nierstrasz Sangiorgi Yonezawa Liskov Najm Nimour Subtyping init % LocalWords: polymorphism subtyping Cseq cseq seq enbl eff int