数理解析研究所講究録996 巻 1997 年 125-142

125

On Typing Systems for the Polyadic -Calculus$\pi$Atsushi Togashi*
Department of Computer Science, Shizuoka University,
3-5-1, Johoku, Hamamatsu 432, Japan
Tel.: +81-53-478-1463
Fax.: +81-53-475-4595
togashi@cs. $\inf$ .shizuoka. .jp$\mathrm{a}\mathrm{c}$Abstract
In the literature, there have been intensive studies on typing (sorting) systems
for the polyadic -calculus, originated by Milner’s sorting discipline [10] based onname matching. The proposed systems, so far, are categorized into the two groups–systems by name matching and ones by structure matching (possibly with subobtain similar results. A natural question arises “Is there any relationship between the two paradigms ?”. With this motivation, the present paper
gives
per investigations on typing systems between the two approaches. For thispurpose, a sorting system by name matching, a quite similar to the system in [7],and a typing system by structure matching with subtyping, a slight extension of
the system in [12], are presented, along with several basic properties. Then, correspondence between the sorting system and the typing system is investigated via
transformations both form sortings to typings and from typings to sortings. It isshown that if a process is. a safe sorting in the sorting system,
then it is well-typed for the transformed typing in the typing system, but not viceversa. This result can be straightforwardly extended to Liu and Walker’s consistentsortings. Under a certain condition, we can show the reverse implication. Furtheremore, on the other direction from typings to sortings, it is shown that the derived
typing from the sorting which is the result of applying transformation to a typing
coincides with the original typing. However, the derived sorting from the typing
which is the result of applying transformation to a sorting is proved to be a proper
specialization of the original sorting.
$\pi$$\mathrm{t}\mathrm{y}\mathrm{p}\mathrm{i}\mathrm{n}\mathrm{g})-\mathrm{a}\mathrm{n}\mathrm{d}$$\mathrm{d}\mathrm{e}\dot{\mathrm{e}}$$\mathrm{w}\mathrm{e}\mathrm{l}1_{-}\mathrm{s}\mathrm{o}\mathrm{r}\mathrm{t}\mathrm{e}\mathrm{d}w.r.i$*The work has been done during visiting the COGS, University of Sussex, Farmer, Brighton BN1, England.

$9\mathrm{Q}\mathrm{H}$

126

1

Introduction

The -calculus [11] has achieved a remarkable simplification by focusing on naming andallowing the communicated data along channels (names) to be names themselves. The
calculus is sufficiently expressive to describe mobile systems and the ability of naturalembeddings of both lazy and call-by-value -calculi into the -calculus [9] suggests that it
may form an appropriate foundation for the design of new programming languages. It has
been shown that higher-order processes can be faithfully encoded in the -calculus [13].
The polyadic -calculus by Milner [10] is a straightforward generalization of the monadic-calculus [11], in which finite tuples of names, instead of single names, are the atomic
unit of communication. Furthermore, the fact that a tuple of names is exchanged at each
communication step suggests a natural discipline of sorting.
In the literature, there have been intensive studies on the topic of typing (sorting)basedsystems for the polyadic -calculus, originated by Milner’s sorting discipline [on name matching. Name matching (or, by-name matching) determines sort equality byrelying on the syntactical names assigned to communication channels (or names) in a given
process, instead of no structure. An algorithm to infer the most general sorting of a term
has been reported by Gay in [6]. Milner’s original idea is further extended and exploredby Liu and Walker in [7], where an input sorting and an output sorting are distinguished.
On the other hand, typing systems based on structure matching are introduced in [16,12]. In the structure matching (or, by-structure matching), type equality or subtyping isdetermined by some abstract type structure, no by how types are syntactically presented.
The systems in both categories–the ones by name matching and the ones by structure
matching –are used to verify run-time type error and obtain the similar results. A
natural question arises “Is there any relationship between the two paradigms ?”. The
correspondence between Milner’s sorting and the typing system [16] is discussed in [15].
With this motivation, the present paper gives deeper investigations on the typing systems between the two approaches. For this purpose, a sorting system by name matching,a quite similar to the system in [7], and a typing system by structure matching with
subtyping, a slight extension of the system in [12], are presented, along with several basic
properties. Then, correspondence between the sorting system and the typing system isinvestigated via two transformations form sortings to typings and from typings to sortings.
On the transformation from sortings to typings, it is shown that if a process is wellsorted $w.r.t$ . for a safe sorting in the sorting system, then it is well-typed for the transformed typing in the typing system, but not vice versa. An illustrative counter example
will be given. This result can be straightforwardly extended to Liu and Walker’s consistentsortings. Under a certain condition, we can show the reverse implication.
On the other direction from typings to sortings, it is shown that the derived typing
from the sorting which is the result of applying transformation to a typing coincides withthe original typing. However, the derived sorting from the typing which is the result ofapplying transformation to a sorting is proved to be a proper specialization of the original
sorting.
The outline of the paper is as follows: Section 2 presents the polyadic -calculus
to a certain extent needed for the study. Section 3 and 4 introduce a sorting system$\pi$$\lambda$

$\pi$

$\pi$

$\pi$

$\pi$

$\pi$

$10\ovalbox{\tt\small REJECT}$

$\pi$

127
and a typing system, respectively. Secti.o..n 5, the main part of this paper, relates thesorting system and the typing system via both-directional transformations. This paper isconcluded in Section 6 with some concluding remarks.

The Polyadic -Calculus

2

$\pi$

This
introduces the polyadic -calculus [10], aof the$N$[11],
monadic -calculus
to a certain extent needed for the study. Let
be a possibly
infinite set of names. The basic syntax of processe. . we consider in this paper is defined
the follo.wing grammar:$\mathrm{s}\mathrm{e}\mathrm{c}\mathrm{t}^{r_{\mathrm{i}\mathrm{o}\mathrm{n}}}$$\mathrm{s}\mathrm{t}\mathrm{r}\mathrm{a}\mathrm{i}\mathrm{g}\mathrm{h}\mathrm{t}\mathrm{f}_{0}\mathrm{r}\mathrm{W}\mathrm{a}\mathrm{r}\mathrm{d}\mathrm{e}\mathrm{X}\mathrm{t}\mathrm{e}\mathrm{n}\mathrm{s}:\mathrm{i}\mathrm{o}\mathrm{n}$

$\pi$

$\pi$

$s$

$\mathrm{b}.\mathrm{y}$$P::=0|a(x_{1}, \ldots, x_{n}).P|\overline{a}\langle b_{1,,..n}, b\rangle.P|P|Q|(\nu x)P|!P$

is the nil process; $a(x_{1}, \ldots, X_{n}).P$ andwhere
are input-prefixes andoutput-prefixes, respectively; $P|Q$ are parallel compositions; $(\nu x)P$ are restrictions; $!P$
are replications. We use the metavariables$x,$, etc for names; $P,$ , andforprocesses. A sequenceof names is often written if its lengthis nottant. For a process , the set $fn(P)$ of .free names and the set $bn(.P)$ of bound names aredefined in the usual way. We formally identify processes up to renaming bound names
in , so that it is assumed that $fn(P)\cap bn(P)=\emptyset$ . This implies the usual conventions
about substitutions to avoid capturing of free names dur..ing.SubStitution, -conversion,side-condition concerning freshness of names, etc.
A structural congruence relation
defined to be the smallest congruence relation
over processes. which satisfies the axiom schemes listed below.
$0$$\overline{a}\langle b_{1}, \ldots , b_{n}\rangle.P$$a,$ $b,$ $c,$$y,$$\tilde{x}$$x_{1},$$\ldots,$

$R$

$Q$

$z$

$|\tilde{x}|$$x_{n}$$\mathrm{i}\mathrm{m}_{\mathrm{e}}\mathrm{p}\mathrm{o}\mathrm{r}-$

$P$

$P$

$P$

$\alpha$$\equiv \mathrm{i}\mathrm{s}$1. Ifthen $P\equiv Q$ : Processes are identified if they differ only by a change ofbound names.
$P\equiv_{\alpha}Q$

2. $P|(Q|R)\equiv(P|Q)|R$ ;$P|Q\equiv Q|P$ ;$P|0\equiv P$.

3. $!P\equiv!P|P$ .
4. $(\nu x)P\equiv P$

if $x\not\in fn(P)^{1}$ ; $(\nu x)(\nu y)P\equiv(\nu y)(\nu x)P$ ;$(\nu x)P|Q\equiv(\nu x)(P|Q)$
if $x\not\in fn(Q)^{2}$ .

Now, we define a reduction relation
satisfying the following rules:
COMM$arrow \mathrm{o}\mathrm{v}\mathrm{e}\mathrm{r}$processes to be the smallest relation$\overline{a(\tilde{x}).P|\overline{a}\langle\tilde{b}\rangle.Qarrow P\{\tilde{b}/\tilde{x}\}|Q}|\tilde{x}|=|\tilde{b}|$

REST

,

$\frac{Parrow P’}{(\nu x)Parrow(\nu x)P}$STRUCTPAR,$\frac{Parrow P’}{P|Qarrow P|Q}$,$\frac{Q\equiv PParrow P’P^{J}\equiv Q\prime}{Qarrow Q}$; $(\nu x)(\nu x)P\equiv(\nu x)P$ .
1This induces the usual axiom schemes:
2Note that the side condition can be viewed as a consequence of our convention of regarding bound$(\nu x)0\equiv 0$

names.

128

3A Sorting System by Name Matching
The introduction of sorting discipline into the -calculus [10] intends to ensure that names
are used consistently. In this section we present a sorting system based on Milner’s originalby Liu andsorting discipline, the resulting system is quite similar to the typing
Walker [7].
be a finite set of (subject) sorts.
Letdenotes the set of all finite sequences
is called an object sort, denoted by, orof elements in . An element in
if the number of the sequence is not important. We use and to range over
simplely. A subject sorting on is a finite set of subject sort assignments a: , where $a\in N$, such that :andimplies $s=t$ . An object sorting on is a finite:
set of object sort assignments of the form either
: or
,
and
: , where$\star\in\{+$implies $u=v$ , forsuch that,::. A sorting on is a pairof a subject sorting and an object sorting .
is safe in if :implies:is safe in all in then is called safe. A sortingis safe if its object$u=v$ . Ifsorting is safe.
$\pi$

sy. .stem$\cdot$$\Sigma^{*}$$\Sigma$$(s_{1}, \ldots, s_{n})$$\Sigma^{*}$$\Sigma$$u$$(\tilde{s})$$\Sigma^{*}$$\Sigma$$\Gamma$$s\in\Sigma$

$a$

$s,$

$s$

$t\in\Gamma$$a$$\Omega$$s^{+}$$s^{\star}$$v\in\Omega$$s^{\star}$

$u,$

$v$

-

$\Omega$$\Gamma$$\Omega$$s$$s^{-}$$u$$s\in\Sigma$

$u$

$s$

$s^{+}$$\Omega$$\Sigma$$u\in\Sigma^{*}$$\Sigma$$\}$$\Omega$$\Sigma$$u,$$s^{-}$$\Gamma;\Omega$$v\in\Omega$$\Gamma;\Omega$$\Omega$

Definition 3.1 A sorting judgment (by name matching) on
is an expression of theform:: , where
is a sorting, is a process, and is the special symbolforwell-behavednessofa process.
standing$\Sigma$$\Gamma;\Omega\vdash P$

$()$

$P$

$\Gamma;\Omega$$()$$\square$An object sorting is usually called a sorting [10, 6, 7]. As usual at most one sort is
assigned to a name in and at most one object sort is assigned to each polarized subject
sort, the subject sort with the polarity, in . So thatanddenote the assigned
subject sort to and the object sort to , respectively. Let $dom(\Gamma)$ and $dom(\Omega)$ denotethe domains of and , respectively. $s\in dom(\Omega)$ is an abuse notation to mean that$s^{+}\in dom(\Omega)$ or $s^{-}\in dom(\Omega)$ .
and
are often represented as sequences.
:denotes the subject sorting, provided that $a\not\in dom(\Gamma)$ . We apply the same
notational convention to .
$\Gamma$$\Omega$$\Gamma(a)$$\Omega(s^{\star})$$s^{\star}$$a$$\Omega$$\Gamma$$\Omega$$\Gamma$$\Gamma\cup\{a :$\Gamma,$

$a$

$s$

s\}$

$\Omega$

Definition 3.2
inference rules:

is a sorting system (by name matching) consisting of the following$\mathrm{S}$$\mathrm{S}- \mathrm{N}1\iota$$\mathrm{S}$$\Gamma;\Omega\vdash 0:()$$\tau_{a:},S,\tilde{X}$$\mathrm{S}$-IN:$t\sim\cdot,\Omega,$$s^{+}$-COMP: $(t)\vdash P:()\sim$$\mathrm{S}$$\Gamma,$$a$:$s;\Omega,$ $s^{+}$$\mathrm{S}$:$(t)\vdash a(\tilde{X}).P\sim$

-REPL

:

$()$

$\Gamma,’\Omega\vdash!\Gamma.\Omega\vdash P.()P.()$$\mathrm{S}$$\frac{\Gamma,\Omega\vdash P\cdot()\Gamma\cdot\Omega\vdash Q\cdot()}{\Gamma\cdot\Omega\vdash P|Q.()},.\cdot$

-OUT

-REST

,

$. \frac{\Gamma,.a.s,..\overline{b}.\cdot\cdot t,\Omega\sim\cdot,.\cdot\sim s^{-.(}t)\vdash P.\cdot()}{\Gamma,a.s,\tilde{b}t\sim,\Omega,s^{-}\cdot(t^{\sim})\vdash a\langle\tilde{b}\rangle P\cdot()}.$.

$\frac{\Gamma,x\cdot s,\Omega\vdash P.\cdot()}{\Gamma\cdot\Omega\vdash(\nu X}$,.
$\square$

The interesting cases are the rules for input and output. In order to be sure that the
input prefix
is well-behaved in a given sorting, we must check that first the object$a(\tilde{x}).P$129
sort for the subject sort of with the positive polarity matches the sort of the sequence ofnames read from ; secondly the continuation is well-behaved in the augmented sortingby the sort assignments : . The case for the output prefix is analogous. The notation: indicates that the sorting judgment: is provable in the systemS.
It is easy to take the correspondence between our sorting system and the typing system
by Liu and Walker [7].
represents a sorting signature consisting of the set of sorts
and the input, output sortings
such that at most one input and one
output object sorts are assigned to a subject sort though multiple object sorts assignments
are allowed in the typing system [7];represents a partial function : $Narrow\Sigma$ of sortassignments to names. Taking account of these correspondences, the inference rules are
essentially same as the ones in [7]. In fact, we have the following proposition by induction
on proofs.
$a$

$P$

$a$

$t\sim$$\tilde{x}$$()$$\Gamma;\Omega\vdash_{\mathrm{S}}P$$\Gamma;\Omega\vdash P$$()$$\Omega$$\Sigma$$ob^{+},$ $ob-:\Sigma-\Delta\wp(\Sigma^{*})$$\Gamma$

Proposition 3.1 Let
proved to possess the type$\phi$

be a sorting anda process.
in the type system [7].
$P$$\Gamma;\Omega$$\Gamma;\Omega\vdash_{\mathrm{S}}P$

:

iff

$()$

$P$

can be$\langle\Omega, \Gamma\rangle$$\square$Definition 3.3 (Due to [7] though slight modifications are made. )1. Letandbe object sortings on . A homomorphism fromtois a function$\star\in\{+,-\}^{3}$such that if :
then
:
, for
.

$\Omega_{1}$$\Sigma$$\Omega_{2}$$\theta:\Sigmaarrow\Sigma$

2. Let$\Gamma_{1}$$\Gamma_{1}$$\Gamma_{1}$

;
;
;

;

$\Gamma_{1}$$\Omega_{1}$and$\Omega_{1}$;$\Omega_{2}$.

$\Omega_{2}$$(\theta(t))\sim\in\Omega_{2}$$\theta(s)^{\star}$be sortings and a homomorphism fromto
. We write
if :
implies:
for all and . We writeiff ;;for some andis called a specialization of$\Gamma_{2};\Omega_{2}$$\Omega_{1}\subseteq_{\theta}\Gamma_{2};\Omega_{2}$$\Omega_{1}\subseteq\Gamma_{2}$$\Omega_{1}$$(t)\sim\in\Omega_{1}$$s^{\star}$$\theta$$s\in\Gamma_{1}$$x$$\Omega_{1}\subseteq_{\theta}\Gamma_{2}$$\Gamma_{1}$$\Omega_{1}$$\theta(s)\in\Gamma_{2}$$x$$\theta$$\Omega_{2}$$\Omega_{2}$

$x$

$s$

$\Gamma_{2};\Omega_{2}$3. An object sorting is self-consistent if for every, whenever:then $n=m$ and there exists a homomorphism
such that, for $1\leq i\leq n$ .
4. A sorting
is consistent if there exists a self consistent sorting$s\in\Sigma$$\Omega$$s^{-}$$(t_{1}, \ldots , t_{m})\in\Omega$:from$(s_{1}, \ldots , s_{n})$$s^{+}$$\theta$$\Omega$to,$\Omega$$\theta(s_{i})=\theta(t_{i})$$\Gamma;\Omega$$\Gamma;\Omega\subseteq\Gamma 0;\Omega 0$$\Gamma_{0};\Omega_{0}$such that.

$\square$Proposition 3.2
1. If

;

and

:

.
2. Any safe sortingis a consistent sorting. Conversely, if
sorting then there exists a safe sorting
such that$\Gamma_{1}$$\Omega_{1}\subseteq\Gamma_{2};\Omega_{2}$$\Gamma_{1}$;$\Omega_{1}\vdash_{\mathrm{S}}P$

$()$

then

$\Gamma_{2}$;$\Omega_{2}\vdash_{\mathrm{S}}P$:$\Gamma;\Omega$$\Gamma_{0};\Omega_{0}$Proof:$()$$\Gamma;\Omega$$\Gamma;\Omega\subseteq\Gamma_{0};\Omega_{0}$is a consistent.

Proof of 1. By Proposition 3.1 and Lemma 8 in [7].

Proof of 2.

It is straightforward from definition that any safe sorting is a consistentsorting. Now, suppose
is a consistent sorting on . Then there is a self-consistentsorting ;such that;for some homomorphism fromto. If
there is a sort insuch that::for some and with(note that), then there exists a homomorphism
fromtosuch that$\Gamma;\Omega$$\Gamma_{1}$$\Omega_{1}$$\Sigma$$\Gamma;\Omega\subseteq_{\theta}\Gamma_{1}$$s$$\Sigma$$s^{+}$$(t^{\sim}),$$\Omega$$\theta$$\Omega_{1}$$s^{-}$$t\sim$$(\tilde{u})\in\Omega_{1}$$|t^{\sim}|=|\tilde{u}|$3We use a total function rather than a partial function. See [7].

$\theta_{1}$$\Omega_{1}$$\tilde{u}$$\Omega_{1}$$\Omega_{1}$$t\sim\neq\tilde{u}$130. If we let; .
, then we have ;and. We repeat this process $n-1$ times for some until there is noThus,. By construction, ;for any and within such that
: $(t),$ :.
is a safe sorting and$\theta_{1}(t)\sim=\theta_{1}(\tilde{u})$$\Omega_{2}=\theta_{1}(\Omega_{1})$$\Gamma_{2}=\theta_{1}(\tau_{1})$$\Gamma_{1}$$n$$\Gamma;\Omega\subseteq_{\theta_{1}\theta}\tau_{2};\Omega 2$$s^{-}\sim$$s^{+}$$\Sigma$$\Omega_{1}\subseteq_{\theta_{1}}\Gamma_{2}$$t^{\sim}$$(\tilde{u})\in\Omega_{n}$$s$$t\sim\neq\tilde{u}$$\tilde{u}$$\Omega_{2}$$\Gamma_{n}$$\Omega_{n,\square }$$\Gamma;\Omega\subseteq\Gamma_{n};\Omega_{n}$Any safe object sorting induces a consistent partition of , see [7] for the definition ofa consistent partition of a sorting signature. Conversely, the safe object sorting is derived
from a consistent partition. Therefore, Proposition 3.2.2 corresponds to Theorem 14 in [7].
The next corollary is a direct consequence of this proposition.
$\Omega$$\Omega$

Corollary 3.1 Let.
sorting on
consistent sorting$\Sigma_{f}i.e$$P$

be a process.

:$\Gamma;\Omega\vdash_{\mathrm{S}}P$$\Gamma’;\Omega^{J}$

$()$

.

has a safe sorting on
iff
for a safe sorting$P$$\Sigma$$\Gamma;\Omega$2.
and$\Gamma;\Omega\subseteq\Gamma_{0};\Omega_{0}$’$\Gamma;\Omega\subseteq\Gamma’;\Omega$$\Gamma_{0};\Omega_{0}$$()$$\Gamma_{0};\Omega_{0}$for somein the sense that$\Gamma_{0};\Omega_{0}$$\Gamma;\Omega$andhas a consistent:
for a$\Gamma’;\Omega’\vdash_{\mathrm{S}}P$$\Gamma;\Omega\subseteq\Gamma’;\Omega’$$\Gamma;\Omega$

1.

$P$

$\square$has a safe specialization, $i.e$ .
Corollary 3.2 If a sorting, thenhas a most general safe sorting
safe sorting$\Gamma’;\Omega’$iff

is safe;for some safe sorting$\Gamma’;\Omega^{J}$

implies$\Gamma_{0};\Omega_{0}\subseteq\Gamma’;\Omega’$,is unique up to isomorphism4

is consistent. The construction of a safe sorting from
Proof: By the assumption,a consistent sorting in the proof of Proposition 3.2 gives a required most general safe
sorting. The uniqueness is obvious from the construction.
$\Gamma;\Omega$$\square$Proposition 3.3 If
Proposition 3.4 If.

$\Gamma;\Omega\vdash_{\mathrm{S}}P$

:

$()$

and $P\equiv Q$ then$\Gamma;\Omega\vdash_{\mathrm{S}}P$

:

$()$

for a safe sorting$\Gamma;\Omega\vdash_{\mathrm{S}}Q$$\Gamma;\Omega$

:

$()$

.

and $Parrow Q$ then$\square$$\Gamma;\Omega\vdash_{\mathrm{S}}$

Q.‘

$()$

Proof: By induction on the proof of the reduction $Parrow Q$ .

$\square$In the inference rule COMM of the reduction relation, it is required that the arities of
the input-prefix and the output prefix must be equal. If a process contains unguarded, thenandwith
prefixes
is said to contain a communication
mismatch [7] or a run-time type error [12.’ 16].
is free from communication mismatch$Parrow*P’$$P’$
if wheneverthendoes not contain a communication mismatch. Thus, by
Corollary 3.1 and Corollary 12 in [7] we can conclude that if a process has a safe sorting
then is free from communication mismatch.
$P$$a(\tilde{x}).Q$$P$$|\tilde{x}|\neq|\tilde{b}|$$\overline{a}\langle\tilde{b}\rangle.R$

$P$

$P$

$\theta$:

4Let$\Omega_{1}$$\Omega_{1}arrow\Omega_{2}$andbe sortings on . An isomorphism form
is a bijective homomorphism
to:such that its inverseis also a homomorphism.
$\Sigma$$\Omega_{2}$$\theta^{-1}$$\Omega_{1}$$\Omega_{2}arrow\Omega_{1}$$\Omega_{2}$

131

4

Typing Systems by Subtyping

In this section we introduce a typing system based on subtyping by Pierce and Sangiorgi[12], which is a slightof the one by Pierce and Sangiorgi [12] with theconstant types (top)are added as the universal type and the inconsistenttype, respectively. Some basic preliminaries are stated as well for later discussions.
Let $I\leq J$ be the least preorder on the tags
containingand. A
type, ranged over by or , is defined by the grammar:$\mathrm{v}\mathrm{a}\mathrm{r}\mathrm{i}a\mathrm{n}\mathrm{t}/\mathrm{e}\mathrm{x}\mathrm{t}\mathrm{e}\mathrm{n}S\mathrm{i}\mathrm{o}\mathrm{n}$$\mathrm{T}$$\mathrm{a}\mathrm{n}\mathrm{d}\perp(bott_{\mathit{0}}m)$$T$$\mathrm{b}\leq \mathrm{w}$$\mathrm{b}\leq \mathrm{r}$$\{\mathrm{r}, \mathrm{w}, \mathrm{b}\}$

$S$

$T$

$::=$

$\alpha|\mathrm{T}|\perp|(T_{1}, \ldots, T_{n})^{I}|\mu\alpha.S$

$I$

$::=$

$\mathrm{r}|\mathrm{w}|\mathrm{b}$,is a type-variables;andare constant types top and bottom, respectively;
is a tagged tuple;
is a recursive type. Let $T$ and $T$ denote the set ofall (open) types and the set of all closed types, respectively, where -convergent types
are identified. The identification over types will be justified by the equality over types
defined below. A type is called finite if it contains no recursive types as subterms. The
symbols and range over finite types. A type is contractive in a type variable ifevery free occurrence of in is within some tagged tuple. An-tree isa finitely branching tree whose nodes are labeled with the labels–tags in, typevariables, or constants(cf. [12]). We can identify an-tree with a partial function
from the tree domain–the set of all finite sequences of non-zero natural numbers–to the set of labels $[3, 4]$ .
denotes the tree whose root is labeled withand whose subtrees are, where is a tag. With each type we associate the-tree Tree $(T)$ ; it is the unique tree satisfying the following equations:where$\perp$$\mathrm{T}$$\alpha$$(\tau_{1}, \ldots, \tau_{n})^{I}$$\mu\alpha.S$$\alpha$

$t$

$T$

$s$

$\alpha$$T$$\alpha$$(\tau_{1}, \ldots, \tau_{n})^{I}$$\mathrm{I}/\mathrm{O}$$\{\mathrm{r},\mathrm{w}, \mathrm{b}\}$$\mathrm{T},$$\perp$$\mathrm{I}/\mathrm{O}$$\mathcal{T}$$\mathrm{N}_{+}^{*}$$I$$[\mathcal{T}_{1}, \ldots,\mathcal{T}_{n}]^{I}$$\mathcal{T}_{1},$$I$$\ldots,\mathcal{T}_{n}$$T$$\mathrm{I}/\mathrm{O}$

Tree
Tree
Tree

$(\alpha)$$=$$(\mathrm{T})$$=$$(\perp)$$=$

Tree $((\tau_{1,\ldots,n}T)I)$

$=$

$[$

$\tau_{\Gamma ee}(\mu\alpha.\tau)$

$=$

$\{$

$\alpha$

;

;
;
Tree
Tree
1

$\mathrm{T}$$\perp$$(\tau 1),$$\ldots,$$\tau ree(T)n]^{I}$$(\tau\{\mu\alpha.T/\alpha\})$;if is contractive in ,otherwise.
$T$$\alpha$The equality of types is defined by $S=_{t}T$ iff Tree $(S)=Tree(\tau)$ . This equality justifies
the identification of -convergent types in the sense that
implies $S=_{t}T$ . Furthermore, we have
. It is easy to see the equality
is a congruence$T,$relation on types. For every typeis a regular tree, a tree with a finite numberof different subtrees. Every tree is completely specified by the language of its occurrencesof the labels, which is a regular language [3]. It follows that for given types and thedecision problem of the identity of types, $S=_{t}T$ , is reducible to the equivalence problem
of deterministic finite-state automata, thus is decidable.
To simplify the case analysis in the following proofs we introduce canonical forms fortypes. A type in canonical form is defined by the grammar:$S\equiv_{\alpha}T$$\alpha$$\mu\alpha.T=_{t}T\{\mu\alpha.T/\alpha\}$$=_{t}$$T_{\Gamma}ee(T)$

$S$

$T$

$T$

$::=$

$\alpha|\mathrm{T}|\perp|(\tau_{1}\ldots., \tau_{n})^{I}|\mu\alpha.(T_{1}\ldots., \tau_{n})^{I}$,$T$$\cdot$132. Hence,must occur free in the body.
where in the casethe body of a in canonical form must immediately start with a tugged tuple. The
following two results are inspired by the ones on type equivalence for a recursive types of
the typed -calculus [1] and can be proved in a similar way.
$\mu\alpha$$(T_{1}\ldots.

, T_{n})^{I},$$(\tau_{1}\ldots., \tau_{n})^{I}$

$a$

$\mu$

$\lambda$

Lemma 4.1 The following equalities hold on types with respect to type equality.

1.

$\mu\alpha.a=\perp$2.

$\mu\alpha.T=\tau\{\mu\alpha.T/\alpha\}$3. If

is contractive in a then $T\{S/\alpha\}=S$implies $S=S’$ .
and$T$$T\{S’/\alpha\}=S’$4.

$\mu\alpha.T=\mu\alpha T\{\tau/\alpha\}$5.

$\mu\alpha.\mu\beta.T=\mu\gamma.T\{\gamma/\alpha,\gamma/\beta\}$

Proposition 4.1 For any type$\square$.
$T$$\square$there is a type

$S$

,.

in canonical form such that $T=_{t}S$ .
$=$:.

By this proposition, in the remainder of this paper, unless specified otherwise, a type will
always mean a type in canonical form.
Let be a sequence of pairs of types $S\leq T$ . A subtyping judgment is an expression, pronounced as is a subtype of under the assumption .
of the form$\Lambda$$S$$\Lambda\vdash S\leq T$

Definition 4.1 A is a subtyping system
ASMP$\overline{\Lambda\vdash S\leq \mathrm{T}}$for each ,$i$$I\leq \mathrm{r}$

RB-R

REC-L

for each ,$i$$\mathrm{c}\mathrm{o}\mathrm{n}\mathrm{S}\mathrm{i}\mathrm{s}.\mathrm{t}\mathrm{i}\mathrm{n}g_{0}\mathrm{f}$.

BTM$\Lambda\vdash S_{i}\leq T_{i}$$\Lambda$

the following rules :REF$\overline{\Lambda,S\leq\tau\vdash S\leq T}$

TOP

BB

$T$

$\overline{\Lambda\vdash T\leq T}$$\overline{\Lambda\vdash\perp\leq T}$$\Lambda\vdash T_{i}\leq S_{i}$$\Lambda\vdash(s_{1}, \ldots, sn)^{\mathrm{b}}\leq(\tau_{1}, \ldots,\tau_{n})^{\mathrm{b}}$$\Lambda\vdash S_{i}\leq T_{i}$$\Lambda\vdash(S_{1}, \ldots, S_{n})^{I}\leq(T_{1}, \ldots, Tn)^{\mathrm{f}}$$\frac{\Lambda,\mu\alpha.S\leq\tau\vdash S\{\mu\alpha.s/\alpha\}\leq T}{\Lambda\vdash\mu\alpha.s\leq T}$$I\leq \mathrm{w}$

WB-W

REC-R

for each ,$i$$\Lambda\vdash T_{i}\leq S_{i}$$\Lambda\vdash(S_{1}, \ldots, S_{n})^{I}\leq(T_{1}, \ldots,T_{n})\mathrm{w}$$\frac{\Lambda,S\leq\mu\alpha.T\vdash S\leq T\{\mu\alpha.\tau/\alpha\}}{\Lambda\vdash S\leq\mu\alpha.T}$$\square$

5In the subtyping system regarding closed types only as in [12],. the rule REF is derivable by wellfounded induction on subtyping judgments. See [14]. However, it is no more derivable when open types
are concerned.

133

$T$

In the same way as the sorting system,
is provable in A. We write$\Lambda\vdash_{\mathrm{A}}S\leq T$$S\leq_{sub}\tau_{\mathrm{W}}\mathrm{h}\mathrm{e}\mathrm{n}\vdash_{\mathrm{A}}S\leq T$$T\leq_{sub}S$.

indicates the judgement
and $S=_{sub}T$ when $S\leq_{sub}T$ and$\Lambda\vdash S\leq$:

Proposition 4.2 The subtype relationand the bottom element 1.

$\leq_{sub}$$j$.

is a partial order on $T$ with the top element$\mathrm{T}$$\square$

As a direct consequence of this proposition, $S=_{sub}T$ implies $S=_{t}T$ . The otherinclusion can be proved as follows. On the one hand, along the same line as $[1],$restricted on types in canonical form can be proved to coincide with the least congruent
relation with respect to the type constructors satisfying the properties Lemma 4.1.2 andLemma 4.1.3. On the other hand,
can be proved to be the congruence relation
satisfying the ame properties in Lemma 4.1. Thus, $S=_{t}T$ implies $.S.=_{sub}T$ . So we use
the symbol
to denote the provable identification instead of.
$=_{t}$$=_{sub}$$s$,$=_{sub}$$=_{t}$

Proposition 4.3
is a lattice with the meet A and the join satisfying, for instance, thefollowing equalities (We will drop the dual equalities and quite obvious equalities regarding, and type variables ):
$T$

${ }$

$\mathrm{T}_{f}\perp$$\alpha$1.

$(S_{1}, \ldots , S_{n})^{I}$

A $(T_{1}, . . ‘, Tm)^{j}=\perp(n\neq m)$ .

2.

$(S_{1}, \ldots, S_{n})^{I}$

A $(S_{1}, .. ., S_{n})^{J}=(S_{1}, \ldots, S_{n})^{I\wedge I}$ .

3.

$(S_{1}, \ldots, S_{n})^{\mathrm{r}}$A4.

$(S_{1}, \ldots, S_{n})\mathrm{w}$5.

$(S_{1}, \ldots, s_{n})\mathrm{b}_{\wedge}(s_{1}, \ldots, Sn)^{\mathrm{b}}=\{$$(T_{1}, \ldots, T_{n})^{\mathrm{r}}=(S_{1} \mathrm{A} T_{1}, \ldots, S_{n} \mathrm{A} T_{n})^{\mathrm{r}}$.

A $(T_{1}, \ldots, T_{n})\mathrm{w}=(S_{1}T_{1}, \ldots, S_{n}T_{n})^{\mathrm{w}}$ .

if, for $1\leq i\leq n$otherwise.

$(S_{1}, \ldots, S_{n})^{\mathrm{b}}$$\perp$

The meet on the set$\{\mathrm{r}, \mathrm{w}, \mathrm{b}\}$$S_{i}=T_{i}$is defined by $I\wedge J=I$ if $I=J$ and$I\wedge J=\mathrm{b}$otherwise.

$\square$Definition 4.2 A typing judgment (by subsorting) is an expression of the form,
where
is a set of type assignments a : $T,$
is a proc..e , and is the special symbol
standing for well-behavedness of the process.
$\Delta\vdash P:0$

$P$$\Delta$$\mathrm{S}\mathrm{S}$$0$$\square$Definition 4.3$\mathrm{T}$is a typing system (by subtyping) consisting of the following rules:

T-NIL$\mathrm{T}$$\overline{\Delta\vdash 0\cdot.\circ}\backslash$

-COMP

.

$\mathrm{T}- \mathrm{I}_{\mathrm{N}}$$\frac{\vdash\Delta(a)\leq(\tilde{\tau})^{\mathrm{r}}\Delta,\tilde{x}.\prime\tilde{\tau}\vdash P:0}{\Delta\vdash a(\tilde{x}).P.\circ}$$\mathrm{T}$-REPL$\mathrm{T}$$\mathrm{T}$$\Delta.\vdash!P\cdot.\circ\Delta\vdash P\circ$$\frac{\Delta\vdash P\cdot\circ\Delta\vdash Q.\cdot \mathrm{Q}}{\Delta\vdash P|Q\cdot 0}$

.

-OUT

-REST

$\frac{\vdash\Delta(a)\leq(\Delta(\tilde{b}))\mathrm{W}\Delta\vdash P.\mathrm{O}}{\Delta\vdash\overline{a}\langle\tilde{b}\rangle.P\cdot \mathrm{O}}.\cdot$$\frac{\Delta,x.T\vdash P.\cdot \mathrm{O}}{\Delta\vdash(\nu x)P.\circ}$.
$\square$134
Pierce and Sangiorgi [12] have formulated their typing system in the Church style(\’a a Church), where typing information for the input parameters and restricted names
are given explicitly. As there is often a simple relationship between the two styles in thetyped -calculi [2] there is a simple relationship between the type system in this paper
and the one by Pierce and Sangiorgi [12]. This will be explained below: Let } be thefunction mapping process terms with type ornamentations into the ordinary processes inthis paper by erasing the all type information.
$\lambda$$|$

Proposition 4.4
1. Let be a process with type annotations. If $\Delta\vdash Q:0$ is provable in the Pierce and: .
Sangiorgi’s Church style typing system [12], then$Q$$\Delta\vdash_{\mathrm{T}}|Q|$$0$with type annotations: then there is a process
be a process. If
2. Letand $|Q|.=P$ .
is provable in the Pierce and Sangiorgi’s
such that$P$$\Delta\vdash_{\mathrm{T}}P$

$Q$

$0$

$syst\tilde{e}m$$\Delta\vdash Q:0$

Proof: 1. By induction on the proof of the judgment
2. Type annotations can be found from the proof. For instance, supposeon the proof$\Delta\vdash Q:0$$\Delta\vdash_{\mathrm{T}}P:0$.

.

$\mathrm{T}\mathrm{h}\mathrm{e}_{\mathrm{P}^{\mathrm{r}\mathrm{o}\mathrm{o}\mathrm{f}}}$.

is by induction$\Delta\vdash_{\mathrm{T}}P:0$.
$\frac{\vdash\Delta(a)\leq(\tau_{1},\ldots,T_{n})\mathrm{r}\Delta.’

x_{11}:\tau,..\cdot.,x.T\vdash P\cdot \mathrm{o}nn}{\Delta\vdash a(X_{1}..,Xn).P\cdot \mathrm{O}},\cdot$is the last inference. The annotated process is given as $a(x_{1} : T_{1}, \ldots, x_{n} : T_{n}).P’$ , where$P’$ is the annotated process corresponding toobtained by the induction hypothesis.
Suppose$P$$\Delta,$

$x$

:

:

$T\vdash P$$\Delta\vdash(\nu x)P$

:

$0$

$0$

is the last inference. The annotated process is given as $(\nu x : T)P’$ , where $P’$ is theannotated version of .
$P$$\square$5

Relating Sortings and Typings

5.1

From Sortings to Typings: we will associate a typing judgment
With each sorting judgment: such that hopefully we expect: . For this purpose,: iff [, mapping (free) sorts to closed
given an object sorting and an environment :and istypes, for each sort in the corresponding type [of with respect todefined as follow :$\Gamma;\Omega\vdash P$

$P$

$()$

$[\Gamma \mathrm{I}\Omega\vdash$$()$$\Gamma;\Omega\vdash_{\mathrm{S}}P$$0$$\rho$$s$$\Gamma \mathrm{J}_{\Omega}\vdash_{\mathrm{T}}P$$0$$\Sigmaarrow T$$\Omega$$\Sigma$$s\mathrm{I}_{\Omega}^{\rho}$$s$$\Omega$$\rho$$s$[$def=$$\mathrm{S}_{\Omega}^{\rho}(S, \emptyset)$$s\mathrm{J}^{\rho}\Omega$$s$$def=$$\{$$\mathrm{S}_{\Omega}^{\rho}(_{S}, x)$;$\mu s$.($\mathrm{T}_{\Omega}^{\rho}(S^{+},$$x\cup\{s\})$$(\mathrm{S}_{\Omega}^{\rho}(t,x\sim))\mathrm{r}$$def=$$\mathrm{T}_{\Omega}^{\rho}(S^{\star}, x)$$\{$$(\mathrm{S}_{\Omega}^{\rho}(t\sim,X))\mathrm{w}$$\rho(s)$A$\mathrm{T}_{\Omega}^{\rho}(S^{-,x}\cup\{s\})$

if
if
–and
otherwise.

$\star=+\mathrm{a}\mathrm{n}\mathrm{d}s^{+}:$$(t^{\sim})\in\Omega$$\star=$$(t^{\sim})\in\Omega$$s^{-}:$

if $s\in X$) otherwise;

135
denote the sequence
In the definition we use the notational convention
, for
.. .,
.
Let
be a sorting then the corresponding typing [is defined by$\mathrm{S}_{\Omega}^{\rho}(^{\sim}t, X).\mathrm{t}_{0}$$\mathrm{S}_{\Omega}^{\rho}(t_{1}, X)$$t\sim=t_{1},$ $\ldots,t_{n}$$\mathrm{S}_{\Omega}^{\rho}(t_{n}, X)$$\Gamma;\Omega$$\Gamma \mathrm{J}_{\Omega}^{\rho}$[$\Gamma \mathrm{I}_{\Omega}^{\rho}def=\{a$: [:$s\mathrm{I}^{\rho}\Omega|a$.

$s\in^{\tau\}}$for each
Usually, the environment, is used to as sign types to sorts.
However, almost results stated in this section hold for any environment . So thatand [are the abbreviations of [and [for any environment , respectively,
possesses object assignments towhen is not very important. Note that [parameters.
having mismatch in number with the$s\in\Sigma$$\rho_{\mathrm{T}}(s)^{d}=\mathrm{e}J_{\mathrm{T}}$$\rho_{\mathrm{T}},$$[s\mathrm{I}\Omega$$\rho$$\Gamma \mathrm{I}\Omega$$s\mathrm{I}_{\Omega}^{\rho}$$\Gamma \mathrm{J}_{\Omega}^{\rho}$$\rho$$s\mathrm{I}_{\Omega}=_{t}\perp \mathrm{i}\mathrm{f}\Omega$$\rho$$s$$\mathrm{I}/\mathrm{O}$be a safe object sorting andLemma 5.1 Let
then$\Omega$$(s^{-} :$\rho$

be an environment.

If$s^{+}$:$(t^{\sim})\in\Omega$(t)\sim\in\Omega)$$\vdash[s\mathrm{I}_{\Omega}^{\rho}=sub([t\mathrm{I}_{\Omega}^{\rho})^{I}\sim$for some I such that

$I\leq \mathrm{r}(I\leq \mathrm{w})$. Thus,,$[s\mathrm{I}_{\Omega}^{\rho}=_{t}([^{\sim}t\mathrm{I}^{\rho}\Omega)^{I}$.

. By the definition of, the safety:
Proof: Suppose, for some ,can be expressed as [property of implies that [. Since unfolding of the recursive definition preserves the identity,
where
see Corollary 2.4.6 in [12],$s^{+}$$(t)\sim\in\Omega(s^{-} :$\Omega$(t^{\sim})\in\Omega)$$\mathrm{S}_{\Omega}^{\rho}(s, X)$$s\ovalbox{\tt\small REJECT}_{\Omega}^{\rho}=\mu s.(\mathrm{S}^{\beta}\Omega(t\sim, \{s\}))^{I}$$s\mathrm{J}_{\Omega}^{\rho}$$I$$I\leq \mathrm{r}(I\leq \mathrm{w})$$\vdash[s\mathrm{I}^{\beta}\Omega=_{Sub}(\mathrm{s}_{\Omega}\rho(t, \{s\}\sim)\{[S\mathrm{I}\rho\Omega/s\})^{I}$

Let be the -th element in the sequence . If $t_{i}=s$ then
[
. If
then
.

.

$t^{\sim}$$t_{i}$$t_{i}\mathrm{I}_{\Omega}^{\rho}$$i$$t_{i}\neq s$

Theorem 5.1 If$\mathrm{S}_{\Omega}^{\rho}(t_{i}, \{s\})\{[s\mathrm{I}\rho/\Omega s\}=[s\mathrm{I}_{\Omega}^{\rho}=\square$$\mathrm{S}_{\Omega}^{\rho}(t_{i}, \{s\})\{[s\mathrm{J}^{\rho}\Omega/s\}=[t_{i}\mathrm{J}_{\Omega}^{\rho}$$\Gamma;\Omega\vdash_{\mathrm{S}}P$:

for a safe sorting$()$

Proof: By induction on the proof ofthe last inference is by -IN or -OUT.
Case S-IN: Suppose::$\Gamma;\Omega\vdash P$$\mathrm{S}$:$\Gamma;\Omega$

$()$

then

$[\Gamma \mathrm{J}_{\Omega}\vdash_{\mathrm{T}}P:0$.

in S. Interesting case is the one when$\mathrm{S}$$\Gamma,$$a$$\Gamma,$$a$$s,\tilde{x}$:$(^{\sim}t)\vdash P$

:

$()$

$(t)\vdash\sim a(\tilde{X}).P$

:

$()$

$t;\Omega,s^{+}:\sim$$s;\Omega,$ $s^{+}:$

is the last inference by applying S-IN. Let $\Omega’=\Omega\cup\{s^{+} : (t)\}\sim$ . By the induction
hypothesis, [. It remains to show that: [[to deduce the typing judgment [. This can be obtained:
Lemma 5.1. The case by -OUT is similar.
$\Gamma \mathrm{I}_{\Omega}’,$$a:[s\mathrm{I}_{\Omega}’,\tilde{x}$$t\mathrm{I}_{\Omega’}\sim\vdash_{\mathrm{T}}P:0$$\tau’\mathrm{J}_{\Omega}’,$$a$$\vdash[s]_{\Omega}’\leq([.t\mathrm{I}_{\Omega’})^{\mathrm{r}}\sim$$s\mathrm{I}\Omega’\vdash_{\mathrm{T}}a(\tilde{X}).P:0$$\mathrm{b}\mathrm{y}\square$$\mathrm{S}$The theorem insists that if a process is well-sorted with respect to a safe sorting in thesystem employing by-name matching, then it is well-typed as well in the system employing
by-structure matching with subtyping.

,

136
Example 5.1 As an example, let us consider the process
and the sorting $\Gamma_{1}=\{a:s, b:t\};\Omega 1=\{s^{+} : (s, t), S^{-} : (s, t), t^{-} : (s)\}$ on
can be proved to be wel.l-behaved in under the assumption ; .

$P_{1}=\overline{a}\langle a,b\rangle.0|a(x,y).\overline{y}\langle X\rangle.0$$\mathrm{S}$$\sum_{\sim}1=\{s,t\}$.

$P_{1}$$\Omega_{1}$$\Gamma_{1}$.
$.’.. \frac{\frac{\Gamma_{1}.’\Omega_{1}.\vdash 0.()}{\Gamma_{1}\cdot\Omega_{1}\vdash\overline{a}\langle a,b\rangle.0\Gamma_{1}()}\frac{\frac{\Gamma_{1},.x.\cdot s,.y.t\cdot\Omega 1\vdash 0..()}{\Gamma_{1},x\cdot s,yt\cdot\Omega 1\vdash\overline{y}\langle x\rangle.0\cdot()}}{\Gamma_{1}\vdash P_{1}\Omega_{1}\vdash a(x()y).\overline{y}\langle X\rangle.0\cdot()}}{\Omega_{1}}.\cdot.,\cdot,.\cdot.,\cdot,’.$From definition, [
. Let

$T$

$s\mathrm{I}_{\Omega_{1}}=\mu s.(s, \mu t.(s)^{\mathrm{w}})\mathrm{b}=_{t}\mu s.(s, (s)^{\mathrm{W}})^{\mathrm{b}}=S,$$\Delta_{1}=[\Gamma_{1}\mathrm{J}_{\Omega_{1}}=\{a :S, b:T\}$

.

[I
$t$

$\Omega_{1}=\mu t.(\mu s.(s, t)^{\mathrm{b}})^{\mathrm{W}}=$$.. \frac{\vdash T\leq(s)^{\mathrm{W}}\Delta_{1},X.S,y..T\vdash 0.\mathrm{O}}{\Delta_{1},x.S,y.\tau\vdash\overline{y}\langle x\rangle 0.0}...\cdot$.
$. \frac{\frac{\vdash S}{}\leq(S,T)\mathrm{W}\Delta 1.\vdash 0\cdot 0\Delta_{1}\vdash\overline{a}\langle a,b\rangle.0.0\frac{\vdash S\leq(S,T)^{\mathrm{r}}}{\Delta_{1}\vdash P_{1}\cdot\circ\Delta 1\vdash a(X,y).\overline{y}\langle X\rangle.0\cdot \mathrm{O}}}{}..,.\cdot$$\square$

Theorem 5.1 can be extended to a consistent sorting in a straightforward way.
be a consistent sorting. Let
be the unique most general
Corollary 5.1 Let
byexistenceisguaranteed
Corollarysorting,
its
Then
3.2.
safe
for a process $P,$.
: implies$\Gamma;\Omega$$\Gamma_{0};\Omega_{0}$$\Gamma;\Omega\vdash_{\mathrm{S}}$

$P$

$()$

$[\Gamma_{0}\mathrm{J}_{\Omega}0\vdash_{\mathrm{T}}P:0$

Proof: By Proposition 3.2.1 and Theorem 5.1.

$\square$tr.ue in general. T.he

The converse of Theorem 5.1 is not
example illustrates the fact:$\mathrm{f}\mathrm{o}\mathrm{l}\mathrm{l}\mathrm{o}\mathrm{w}.\mathrm{i}\mathrm{n}.\mathrm{g}$simple counter

Example 5.2 Let us consider the process
under the afe sorting:$;\Omega_{2}=\{s^{-}$$\Sigma_{2}=\{s,t,r\}$$(t),$
: }
:
: (),
: (),
: () on. By the transformation,
[
, [I
, [
, and [. Then, trivially wehave [: . But,
because $t\neq r$ .
$P_{2}=\overline{a}\langle b\rangle.0$

$s,$

$b$

$r^{+}$$t^{+}$$r$$t$$s\mathrm{I}_{\Omega_{2}}=(\mathrm{r})^{\mathrm{w}}$$\Gamma_{2}\mathrm{I}\Omega_{2}\vdash_{\mathrm{T}}P_{2}$$r^{-}$$\Gamma_{2}\mathrm{J}_{\Omega_{2}}=\{a :$r\mathrm{J}_{\Omega_{2}}=\mathrm{b}$$\Omega_{2}=\mathrm{r}$$\Gamma_{2}=\{a$

$s$

$\}$

(\mathrm{r})^{\mathrm{w}}, b :\mathrm{b}\}$$\square$$\Gamma_{2};\Omega_{2}\mu_{\mathrm{s}}P_{2}$$0$

If the transformation defined by a safe object sorting from sorts into types satisfies
a certain condition, then the converse of Theorem 5.1 holds. To show this fact, we need
the following lemma.
$\Omega$Lemma 5.2 Let
1. Let$s\in\Sigma$$\Gamma;\Omega$. For any

2. For any sortand there exists$s\in\Sigma$$\mathit{2}\mathrm{a}$$2\mathrm{b}$be a safe sorting on$T\in sub([s\mathrm{I}\rho \mathrm{T})\Omega$’$\Sigma$.

there exists a sort

, if [, where$1\leqi\leqn$, for each, such that$s\mathrm{I}_{\Omega}^{\rho \mathrm{T}}=(T_{1}, \ldots, T_{n})^{I}$$I\leq \mathrm{r}(I\leq \mathrm{w})$.

$T_{i}=_{t}[t_{i}\mathrm{J}_{\Omega)}^{\rho_{\mathrm{T}}}1\leq i$.

$s^{+}$$T=_{t}[t\mathrm{I}_{\Omega}^{\rho_{\mathrm{T}}}\cdot$, then $s\in dom(\Omega)$$s\in\Sigma_{f}$

if [

.

$\leq n_{f}\cdot$$(t_{1}, \ldots, t_{n})\in\Omega(s^{-} :3. For any sortsuch that$t_{i}\in\Sigma$.

:$t\in\Sigma$(t_{1}, \ldots, t_{n})\in\Omega)$$s\mathrm{J}_{\Omega}^{\rho_{\mathrm{T}}}=\mathrm{T}$$-$.

, then $s\not\in dom(\Omega)$ .

$\square$

137

Theorem 5.2 Let
for any sorts

be a safe sorting on such that
implies. Then, [$t\in\Sigma^{6}$$s,$$\Sigma$$\Gamma;\Omega$

Proof: By induction on the proof [rules. For detailed proof, refer to [14].

5.2$\tau \mathrm{I}_{\Omega}^{\rho \mathrm{T}}\vdash_{\mathrm{T}}P$:$0$

implies $s=t$ ,, for any process .

$[s]^{\rho \mathrm{T}}\Omega\leq_{sub}[t]_{\Omega}^{\rho_{\mathrm{T}}}$$\Gamma;\Omega\vdash_{\mathrm{S}}P:()$$\Gamma \mathrm{J}_{\Omega}^{\rho_{\mathrm{T}}}\vdash_{\mathrm{T}}P:0$$P$and by case analysis of the applied$\square$From Typings to Sortings;in terms of a typing . To this end, we need someWe will define a sorting
preliminaries. Given an open type , let Sub $(T)$ be the set obtained from the set of all
the subterms of by replacing each bound type variable appearing in a subterm by its
definition, .rmally Sub $(T)$ is defined inductively as follows:$\Delta^{@}$$\Delta$$\Delta^{*}$$\backslash$

$T$

$T$

$\mathrm{f}\mathrm{o}$Sub $(a)$

Sub

Sub

$(\mathrm{T})$Sub$(\perp)$$d\mathrm{e}j=$$\{\alpha\}$$((\tau_{1}, \ldots,Tn)^{I})$

Sub $(\mu a.T)$$def=$$def=$$def=$;$\{\mathrm{T}\}$;$\{\perp\}$;$def=$$\{(T_{1}, \ldots,Tn)^{I}\}\cup Sub(T1)\cup\cdots\cup Sub(T_{n})$$\{\mu\alpha.\tau\}\cup\{S\{\mu\alpha.T/\alpha\}|S\in Sub(T)\}$;.

From definition it is easy to see that Sub $(T)$ is finite for any type . In fact, Sub $(T)$ canhave no more elements than the number of distinct subterms of .
..
consistingWith an open type in canonical form $T\in T$ we associate tuple
by
are
.
The
sorts
definedof sorts and the object sortingof the set
$T$

$T$

$\cdot$$a$$\langle\Sigma(\tau), T^{\#}\rangle$$\tau\#$$\Sigma(T)$$\Sigma(T)^{def}=\{[S]|S\in Sub(T)\}$

for a type , where $[T]d\mathrm{e}f=\{S|T=_{t}S\}$ is the congruence class of with respect to theis defined by structural induction on .
on $T$ . The object sorting
identity relation
$T$

$T$

$T$

$\tau\#$$=_{t}$$\emptyset$$\Omega_{\perp}$$T^{\#}=def\{$

if $T=a$ , or
if $T=\perp$
if
if$\mathrm{T}$$T=(\tau_{1}, \ldots, \tau_{n})^{I}$$\Omega_{t}\cup T_{1}^{\#}\cup\cdots\cup T_{n}^{\#}$$\Omega_{T}\cup(T_{1}^{\#}\cup\cdots\cup T_{n}^{\#})\{[T]/[a]\}$$T=\mu\alpha.(T_{1}, \ldots, \tau_{n})^{I}$

,

where
$def=$$\dot{1}2_{\perp}$$\{[\perp]^{+} :$def=$$\Omega_{t}$$\{$(), [\perp]^{-} :([\perp])^{\mathrm{w}}\}$$\{[T]^{+} :([T_{1}], \ldots, [T_{n}])\}$$\{[T]^{-} :([T_{1}], \ldots, [T_{n}])\}$$\{[T]^{+} :([T_{1}], \ldots, [T_{n}]), [T]^{-} :([T_{1}], \ldots, [T_{n}])\}$

if
if
if

$I=\mathrm{r}$$I^{\cdot}.=\mathrm{w}$$I=\mathrm{b}$.

ue ject sorting up to renaming of sorts such thatcondition means that represents theno distinct sorts represent the same type where the type equality by forgetting the tags is used as the,is well-typed with respect to: means
identity of types. Under this condition, [where only by-structure matching without subtyping is used.

$\overline{6\mathrm{T}\mathrm{h}\mathrm{i}\mathrm{s}}$$\mathrm{u}\mathrm{n}\mathrm{i}\acute{\mathrm{q}}$$0\dot{\mathrm{b}}$$\Omega$$\Gamma \mathrm{J}_{\Omega}\rho_{\mathrm{T}}\vdash_{\mathrm{T}}P$

$0$

$P$

$[\Gamma \mathrm{J}_{\Omega}\rho_{\mathrm{T}}$138$def=$$\{$$\Omega_{r}$$\{[T]^{+} :([T_{1}\{T/\alpha\}], \ldots, [T_{n}\{T/\alpha\}])\}$$\{[T]^{-} :([\tau_{1}\{T/\alpha\}], \ldots, [T_{n}\{T/a\}])\}${$([T_{1} \{T/\alpha\}], \ldots, [T_{n}\{\tau\int\alpha\}])$:$[T]^{+}$

,

if
if
if

$I=\mathrm{r}$$I-arrow \mathrm{w}$

$I$

$=$

$\mathrm{b}$

.

.

.

$[T]^{-}:$ $([T1\{T/\alpha\}], \ldots, [T_{n}\{T/\alpha\}])\}$

Let$\Delta$

be a typing. The corresponding set of subject sorts is defined by{$\Sigma(\Delta)=d\mathrm{e}j\cup$

The associated sortingon$\Delta^{@};\Delta^{\#}$$def=$$\Delta^{@}$$\Sigma(\Delta)$$\{x :$def=$$\Delta^{\#}$:$\Sigma(T)|x$$\cup${$T\in\Delta$

with[T]|x :

$T^{\#}|x$$\Delta$, for some

$x$

}.

is defined as follows:

T\in\Delta\}$;: $T\in\Delta$ , for some

$x$

}.

For notational simplicity, the square brackets are often omitted and the sortusing the prefix notation. So that, e.g. the obis sometimes written as:
is the abbreviation of:ject sort assignment$([T_{1}], \ldots, [T_{n}])$ .

$(\tau_{1}, \ldots, \tau_{n})^{I}$$I(T_{1}, \ldots, T_{n})$$[(T_{1}, \ldots, T)^{\mathrm{b}}n]^{+}$$(T_{1}, \ldots, T_{n})$$\mathrm{b}(T_{1}, \ldots , T_{n})^{+}$. The set of sort is given bysorting is obtained bycorresponding. The$\Delta_{3}^{@}=\{b:s\};\Delta_{3}^{\#}=\{s^{+} : (t, t), s^{-} : (t, t),t^{+} : (), t^{-} : ()\}$ . It is worth while to note that.
and[Example 5.3 Consider the typing. Let$\Delta_{3}=\{b :$s=\mathrm{b}(\mathrm{b}, \mathrm{b}),$$\Sigma(\Delta_{3})=\{\mathrm{b}(\mathrm{b}, \mathrm{b}), \mathrm{b}\}$$s$(\mathrm{b}, \mathrm{b})^{\mathrm{b}}\}$$t=\mathrm{b}$$\square$$[\Delta_{3\mathrm{I}_{\Delta}3}^{@}\#=\Delta_{3}$$s\mathrm{J}_{\Delta_{3}^{\#}}=(\mathrm{b}, \mathrm{b})^{\mathrm{b}};[t1_{\Delta_{3}^{\#}}=\mathrm{b}$Example 5.4 As a more involved example, let us consider the typing$\Delta_{4}=\{a :\mu\alpha.(a, (\alpha)\mathrm{W})^{\mathrm{b}}, b :\mu\beta.(\mu a.(\alpha, \beta)^{\mathrm{b}})\mathrm{w}\}$.

. Then we obtain theLet$T,$. Among them, andsorts by construction: $S,$
we have $sdef=S=\mathrm{b}(S, \mathrm{W}(s))=U=\mathrm{b}(U, T);td\mathrm{e}f=\mathrm{w}(U)=\mathrm{w}(S)$ . Thus, the set ofis given by $\Delta_{4}^{@}=\{a : s, b : t\}$ ;sort is given by $\Sigma(\Delta_{4})=\{s,t\}$ . The sorting from
$S=\mu\alpha.(\alpha, (\alpha)^{\mathrm{W}})^{\mathrm{b}};T=\mu\beta.(\mu\alpha.(\alpha,\beta)^{\mathrm{b}})\mathrm{w};U=\mu\alpha.(\mathit{0}, T)^{\mathrm{b}}$$\mathrm{b}(S, \mathrm{W}(s)),$$\mathrm{w}(S),$$\mathrm{w}(U),$$U$$\mathrm{b}(U, T)$$\Delta_{4}$.
in Exam;is the resulting typing obtained from the sorting
Recall that;Thus,
coincides with the original sorting.
ple 5.1 and the derived sorting.
, where;;[[$\Delta_{4}^{\#}=\{S^{+} :(s, t), s^{-} :(S, t),t-:(S)\}$$\Gamma_{1}$$\Delta_{4}$$\Omega_{1}$$\Gamma_{1}$$\Delta_{4}^{@};\Delta_{4}^{\#}$$\Omega_{1}=$$\square$$\Gamma_{1}\mathrm{I}_{\Omega_{1}}^{\#}$$\Gamma_{1}\mathrm{J}_{\Omega_{1}}^{@}$$[\Gamma_{1}\mathrm{I}_{\Omega_{1}}=\Delta_{4}$$\Delta_{4}=[\Delta_{4\mathrm{I}_{\Delta_{4}^{\#}}}^{@}$: . But, unfortunately;: implies
We hope that for instancethere is a simple counter example. Let us consider the context.
is well-typed under the context .
and the process$\Delta\vdash_{\mathrm{T}}P$$0$$\Delta^{@}$$()$$\Delta^{\#}\vdash_{\mathrm{S}}P$$\Delta=\{a :$P=\overline{a}\langle b\rangle.0$$P$(\mathrm{T})^{\mathrm{W}}, b:(\mathrm{T})^{\mathrm{r}}\}$$\Delta$$. \frac{(\mathrm{T})^{\mathrm{w}}\leq((\mathrm{T})^{\mathrm{r}})^{\mathrm{W}}.a\cdot(\mathrm{T})\mathrm{W}b.(\mathrm{T})^{\mathrm{r}}\vdash 0\cdot\circ}{\overline{a}.(\mathrm{T})^{\mathrm{w}},b\cdot(\mathrm{T})^{\mathrm{r}}\vdash a\langle b\rangle.0\cdot 0}.,\cdot.\cdot$

Thus,$\Delta\vdash_{\mathrm{T}}P$$\Delta^{\#}=${$\mathrm{w}(\mathrm{T})^{-}:$: . By definition,(T),}. Because$\Sigma(\Delta)=\{\mathrm{w}(\mathrm{T}), \mathrm{r}(\mathrm{T}), \mathrm{T}\};\Delta^{@}=\{a :$0$$\mathrm{r}(\mathrm{T})^{+}:$$(\mathrm{T})$$\mathrm{T}\neq \mathrm{r}(\mathrm{T}),$$\Delta@;\Delta\#$

Vs

$P$

:

\mathrm{w}(\mathrm{T}), b :

$()$

.

;

\mathrm{r}(\mathrm{T})\}$

139
Proposition 5.1 Let
any $S\in sub(T)$ .

$T$

be a type and$\rho$

an environment, then$[[S]\mathrm{I}^{\rho}\tau\#=_{t}\ovalbox{\tt\small REJECT}[S]\mathrm{I}_{s\#}\rho,$$for\coprod$

Lemma 5.3 Let be any function mapping type variables to closed types
and be any type. Define the environment : $\Sigma(T)arrow T$ by$\sigma$$\alpha$$\sigma(\alpha)\in T$$T$$\rho$$\sigma(\alpha)$$\rho([S])^{d}=^{f}e\{$$S$

for $[S]\in\Sigma(T)$ . Then, we haveif

$S=[\alpha]$otherwise,$[[T]\mathrm{I}_{T^{*}}^{\rho}=_{t}\sigma(T)$for some$\alpha$.

Proof: We will show Treeby induction on
and by case analysis on . The interesting case arrises when $T=\mu a.(T_{1}, \ldots, \tau_{n})^{I}.$ By
definition,$([[\tau]\mathrm{I}^{\rho}\tau\#)(\pi)=Tree(\sigma(\tau))(\pi)$$\pi\in \mathrm{N}_{+}^{*}$$T$$\Sigma(T)$$=$$\{[T]\}\cup\{[S\{T/\alpha\}]|S\in sub((T_{1}, \ldots, T)^{I}n)\}$$T^{\#}$$=$$\Omega_{r}\cup(T_{1}\#\cup\cdots\cup\tau_{n}\#)\{[\tau]/[a]\}$

where

;

.

.

$\Omega_{r}=def\{$$\{[T]^{+} :([T_{1}\{T/\alpha\}], \ldots, [T_{n}\{T/\alpha\}])\}$$\{[T]^{-} :([T_{1}\{T/\alpha\}], \ldots, [T_{n}\{T/\alpha\}])\}${$[T]^{+}$

if
if
if

: $([T_{1}\{T/\alpha\}], \ldots, [\tau_{n}\{T/a\}])$ ,$I=\mathrm{r}$$I=\mathrm{w}$$I=\mathrm{b}$.

$[T]^{-}:$ $([T_{1}\{T/\alpha\}], \ldots, [T_{n}\{T/\alpha\}])\}$

Thus, by Lemma 5.1 and Proposition 5.1

Tree
Tree

$(\sigma(T))$$=$$[\tau_{r}ee(\sigma(\tau 1\{T/\alpha\})), \ldots, Tree(\sigma(\tau n\{T/\alpha\}))]^{I}$$([[T]\mathrm{I}_{\tau\#}\beta)$

$=$

[Tree

$=$

[Tree

$([[\tau_{1}\{\tau/\alpha\}]\mathrm{I}^{\rho}T\#),$;$Tree([[T_{n}\{\tau/\alpha\}]\mathrm{I}^{\rho}T\#)]^{I}$$\ldots,$$([[T_{1}\{\tau/\alpha\}]\mathrm{I}^{\rho}T1\{\tau/\alpha\}\#),$$\tau_{r}ee([[T\{n\tau/\alpha\}]\mathrm{I}\rho T_{n}\{T/\alpha\}\#)]I$$\ldots,$

Obviously

Tree
Let

$k\pi$$([[T]\mathrm{I}_{T\#}^{\rho})(6)=Tree(\sigma(\tau))(\epsilon)$.

be a current path. If $k\leq n$ thenTree$([[\tau]\mathrm{I}_{T\#}^{\rho})(k\pi)=Tree(\sigma(\tau))(k\pi)$,by the induction hypothesis$T_{\Gamma e}e([[T_{i}]\mathrm{I}_{T^{\#}i}^{\rho})(\pi)=Tree(\sigma(Ti))(\pi)$for each$i,$$1\leq i\leq n$,. If $k>n$ then both the trees are undefined on

Theorem 5.3
1.

$\Gamma;\Omega\subseteq[\Gamma \mathrm{I}^{\copyright}\Omega;[\Gamma \mathrm{J}_{\Omega}^{\#}$, for any safe sorting2.

$\Gamma;\Omega\neq[\Gamma \mathrm{I}_{\Omega}^{@};[\Gamma \mathrm{J}_{\Omega}^{*}$, for some safe sorting

3.

$\Delta=[\Delta^{@}\mathrm{I}_{\Delta\#}$, for any typing$\Delta$.

$\Gamma;\Omega$on$\Gamma;\Omega$$\Sigma$on.
$\Sigma$.

$k\pi$.

.

140
Proof: 1. Let :then : [Suppose :homomorphism from to [By Lemma 5.1, [we have [:($\theta$

$x$

, for
.
be the function defined byby definition. It remains to show that is a
, where.
Suppose, where) Thus by construction,(or, as required.
I )$\theta(s)^{def}=[[S\mathrm{J}_{\Omega}]$$\Sigmaarrow\Sigma([\Gamma \mathrm{J}_{\Omega})$$s\in\Gamma$$x$$\Omega$$\theta$$[s\mathrm{I}_{\Omega}]\in[\Gamma \mathrm{J}_{\Omega}^{@}$$\Gamma \mathrm{I}_{\Omega}^{\#}\cdot$$s^{*}:$$(t_{1}, \ldots , t_{n})\in\Omega$$s\mathrm{I}\Omega=_{t}([t_{1}\mathrm{I}\Omega, \ldots, [t_{n}\mathrm{I}\Omega)^{I}$$\star=+(\mathrm{o}\mathrm{r}\star= -)$$I\leq \mathrm{w}$$I\leq \mathrm{r}$$.\cdot$$[[t_{1}\mathrm{I}\Omega],$$[S\mathrm{I}\Omega]^{\star}$$s\in\Sigma$$\ldots,$$[[t_{n}$$\Omega]$$\in[\Gamma \mathrm{I}_{\Omega}^{\#}$

2. Consider the safe sorting $\Gamma_{0}=\{a : t, b:s\};\Omega_{0}=\{t^{+}$ : (),inequality is obvious from the followings: [[: () .
$\Gamma_{0}\mathrm{I}_{\Omega}0=\{a :$s^{+}$: () on$\}$$\{s, t\}$. The\mathrm{r}, b:\mathrm{r}\};[\tau_{\mathrm{o}\mathrm{I}_{\Omega_{0}}^{@}}=\{a:[\mathrm{r}], b:[\mathrm{r}]\}$

;

$\}$

$\Gamma_{0}\mathrm{J}^{\#}\Omega 0=\{[\mathrm{r}]^{+}$

3. The proof is by Lemma 5.3 since any$\tilde{\mathrm{t}}\mathrm{y}\mathrm{p}\mathrm{e}$in$\Delta$

is closed.

$\square$Corollary 5.2

1.
2.

6

$If.\Gamma;\Omega\vdash_{\mathrm{S}}P$

:

$()$

for a safe sorting$\Gamma;\Omega$then [$\Gamma \mathrm{I}_{\Omega}^{@}$;[$\Gamma \mathrm{I}_{\Omega}^{\#}\vdash_{S}P$

:

$()$

.
$\square$$[\Gamma \mathrm{J}_{\Omega}=[\mathbb{I}\tau \mathrm{I}^{@}\Omega \mathrm{I}1\Gamma]_{\Omega}\#\cdot$

Concluding Remarks

In this paper, the sorting system by name matching and the typing system by structure
matching with subtyping were related via the transformations. The introduced sorting(typing) system is quite closed to the typing system by Liu and Walker [7] (by Pierce andSangiorgi [12] . So the results obtained in this paper are applicable to the investigationof the correspondence between them. If we forget the polarities (the tags and subtyping),
then the resulting sorting (typing) system turns out to coincide with a variant of Milner’ssorting system [10] (the typing system by Vasconcelos and Honda [16]). Thus, our resultsinterpret the relationship between both the systems as well.
The correspondence between Milner’s sorting and the typing system [16] is informally
discussed with the illustrative example in [16] and more formally discussed in [16]. The
idea is that a set of basic sorts and sorting defines a regular system of equations; sucha system has a unique solution whose components are represented as regular trees; thenderive a typing from the solution. Conversely, trees in a finite set of regular trees arecomponents of the unique solution of a single system of equation [3]; from such a system
the set of sorts and sorting are obtained. But, the preliminary theorem Theorem 5.1.3
in [15] is erroneous. Because distinct sorts may correspond to the same type. Refer to
Example 5.2.
The transformation from sortings to typings has a similar flavor to the one from
regular system equations in canonical form to recursive types discussed in $[1, 14]$ . To makeclear the correspondence between the two transformations, we derive a regular system of
equations from an object sorting. Let
be a safe object sorting on . For, thefinite typewith subject sorts taken as type variables is defined by$)$$\Omega$$\Sigma$$\langle s\rangle_{\Omega}$$(t^{\sim})^{\mathrm{b}}$$(t^{\sim})^{\mathrm{r}}$$\langle s\rangle_{\Omega}=d\mathrm{e}f\{$$(t^{\sim})^{\mathrm{w}}$$\mathrm{T}$if::for some:
iffor some , and:if
for some , andif $s\not\in dom(\Omega)$ .
$s^{+}$$(t^{\sim}),$$s^{+}$$(t^{\sim})\in\Omega$$(t^{\sim})$$s^{-}\not\in dom(\Omega)$$s^{-}$$(t^{\sim})\in\Omega$$(t)\sim$$s^{+}\not\in dom(\Omega)$$s^{-}$$(t^{\sim})\in\Omega$$(t)\sim$$s\in\Sigma$

141
The systemof equations is obtained from

$E(\Omega)$$\Omega$by$E(\Omega)^{de}=^{J}\{s=\langle s\rangle\Omega|s\in\Sigma\}$.

be a safe object sorting on . For any sort in ,Proposition 6.1 ([14]) Let, where [is the type represented by the type variable $sw.r.t$ .
[this means. (Note thatthe system of equations.
represents the same tree as the typethat $sw.r.t$ .
$\Omega$$\Sigma$$\Sigma$$s$$\langle_{S}, E(\Omega)\rangle \mathrm{I}$$s\mathrm{J}_{\Omega}=_{t}[\langle_{S}, E(\Omega)\rangle \mathrm{I}$$E(\Omega)$$Tree\langle S, E(\Omega)\rangle=Tree[\langle S, E(\Omega)\rangle \mathrm{I}$$E(\Omega)$$\square$$[\langle s, E(\Omega)\rangle \mathrm{J})$of equations in canonical form we define theConversely, given a regular systemwith type variables appearing in and two constants
corresponding object sorting
as subjects sorts.
$E$

$E$

$\Omega(E)$.

$\perp \mathrm{t}\mathrm{a}\mathrm{k}\mathrm{e}\mathrm{n}$$\mathrm{T},$$\Omega(E)$$dej=$$\{\alpha^{+} :(\tilde{\beta})|a--(\tilde{\beta})^{\mathrm{b}}\in E\}\cup\{\alpha^{-} :$\cup\{\alpha^{+} :(\tilde{\beta})|\alpha=(\tilde{\beta})^{\mathrm{b}}\in E\}$(\tilde{\beta})|\alpha=(\tilde{\beta})^{\mathrm{r}}\in E\}\cup\{\alpha^{-} :where(\tilde{\beta})|\alpha=(\tilde{\beta})^{\mathrm{w}}\in E\}\cup\Omega_{\perp}(E),$.

ifotherwise.

$E\mathrm{c}\mathrm{o}\mathrm{n}\mathrm{t}\mathrm{a}\mathrm{i}\mathrm{n}\mathrm{S}\perp$$\Omega_{\perp}(E)=d\mathrm{e}j\{$$\emptyset\{1^{+} :(), \perp^{-}:(\perp)^{\mathrm{w}}\}$

Proposition 6.2 ([14]) Let be a regular system of equations in canonical form
, thenbe a type variable,$E$$\mathrm{T},$$or\perp$$andp\coprod$$[p\mathrm{I}_{\Omega(E)}=_{t}[\langle p, E\rangle \mathrm{I}\cdot$

From typings without subtyping to Milner’s sortings, as stated in [16], well-typing
induces well-sorting. But, as illustrated in Section 5.2, in general well-typing doesn’tthat the following
always implies well-sorting along the given translation. But,. weconjecture must hold.

.nvince$\mathrm{c}\mathrm{o}$Conjecture 6.1 If$\Delta\vdash_{\mathrm{T}}P$$dom(\Delta 0)\supset dom(\Delta)$

Note that$\Delta_{0}\vdash_{\mathrm{T}}P:0$

and
. See

:

$0$

such thatthen there exists a typing$x\in
dom(\Delta)$
–and
all
.

$\Delta_{0}(x)\leq\Delta(x)f,\mathit{0}.r$$[1\mathit{2}, 14]$$\Delta_{0}$$\Delta_{0}\preceq\Delta$$\Delta_{0}^{@},.\Delta_{0}\#\vdash_{\mathrm{S}}P$

:

–

.

$()\square$

Finally, the relations between incremental systems and non-incremental systems are
discussed in both sorting and typing in [14].

References[1] Amadio, R.M., Cardelli, L., Subtyping recursive types, TOPLAS, 15, No. 4, pp.575631, 1993.

[2] Barendregt, H.P., Lambda calculi with types, in: Handbook of Logic in Computer
Science, Volume 2, Background: Computational Structures, Edts. S. Abramsky, D.M.
Gabbay, and T.S.E. Maibaum, Oxford Science Publications, 1992.
[3] Courcelle, B., Fundamental properties of infinite trees, TCS, 25, pp.95-169, 1983.

142[4] G., Cousineau, M., Nivar., On rational expressions representing infinite
8th MFCS, LNCS, 74, pp.567-580, 1979.

$\mathrm{r}\mathrm{a}\mathrm{t}\mathrm{i}_{\mathrm{o}\mathrm{n}}\mathrm{a}\mathrm{I}$trees:[5] Hindley, R., The completen.ess theorem for typing -terms, TCS, 22, pp.1-7, pp.127133, 1983.
$\lambda$[.6] Gay, S.J., A sort inference algorithm for the polyadic -calculus, in 20th POPL, 1993.
$\pi$[7] Liu, X., Walker, D., A polymorphic type system for the polyadic -calculus, CONCUR’95, LNCS, 962, pp.103-116, 1995.
$\pi$[8] Milner, R., Communication and Concurrency, Prentice Hall, 1989.
[9] Milner, R., Functions as processes, th ICALP ’90, LNCS, 443, 1990.
[10] Milner, R., The p.olyadic -calculus: A tutorial,
LFCS, Dept. of Comput. Sci., Edinburgh Univ., 1991.

$\dot{\mathrm{T}}\mathrm{e}\mathrm{c}\mathrm{h}\mathrm{n}\mathrm{i}\mathrm{c}\mathrm{a}\mathrm{l}$$\pi$Report ECS-LFCS-91-180,[11] Milner, R., Parrow, J., Walker, D., A calculus of mobile processes, Part I and II,
Info. Comp., 100, No.1, pp.1-40, pp.41-47, 1992.
$\not\in \mathrm{y}$[12] B., Pierce, D. Sangiorgi, Typing and subtyping for mobile processes, Dep. of Computer Science, University of Edinburgh, 1994.

[13] Sangiorgi, D., Expressing mobility in process algebras: first-order and higher-orderparadigms, Ph.D. Thesis, Edinburgh University, 1992.
[14] Togashi, A., On typing systems for the polyadic
Report, COGS, University of Sussex, 1996.

$\pi- \mathrm{c}\mathrm{a}\mathrm{l}\mathrm{c}\mathrm{u}\mathrm{I}\mathrm{u}\mathrm{s}$, to appear in Technical[15] Vasconcelos, V.T., Honda, K., Principal typing-schemes in a polyadic -calculus, CS
92-4, Keio University, 1992.
$\pi$[16] Vasconcelos, V.T., Honda, K., Principal typing schemes in a polyadic
CONCUR’93, LNCS, 715, pp.524-538, 1993.

$\pi$-calculus,