数理解析研究所講究録996 巻 1997 年 158-161

158

GRAPH TYPES FOR MONADIC MOBILE PROCESSES–EXTENDED ABSTRACT–NOBUKO YOSHIDA

The monadic -calculus [13, 11, 5, 3, 6] is a powerful formalism in which we canconstruct complex structures of concurrent computing by combining simple monadic
name passing. The construction of significant computational structures in this calculus is done by passing and using private names between interacting parties to control
the sharing of interaction points. For example, the following process expresses comis output, $(a)P$munication of a sequence of names (below ax.P is input andare fresh).
denotes scope restriction, and$\pi$$\overline{a}v.P$$c,$ $z$$az.zx_{1\cdot 2^{ZX_{3}.P}}zX.|(c)\overline{a}C.\overline{C}v_{1}.\overline{C}v_{2}.\overline{C}v3\cdot Qarrow P\{v_{1}v_{2}v_{3}/x_{1}x_{23}x\}|Q$(0.1)

In this example, coming from [13], the private channel is used during interaction, soand is done deterministicallythat, after the initial step, the communication of
without interference from the third party. This example also shows that we canrepresent polyadic (multiple) name passing from monadic name passing. Anotherexample with a more complex communication structure follows.
$c$$v_{1},$ $v_{2}$$v_{3}$$az.zX_{1^{\overline{Z}}1\cdot 2\cdot 2}.vZX\overline{\mathcal{Z}}v.P|(c)\overline{a}C.\overline{c}w_{1}.cy1\cdot\overline{C}w2\cdot cy2\cdot Qarrow+P\{w_{1}w_{2}/x_{1}x_{2}\}|Q\{v_{1}v_{2}/y_{1}y_{2}\}$(0.2)

Note input and output are mixed together. As in the previous example, once twoparties start interaction, a sequence of communication is done following a prescribedto moreprotocol using a private channel. The same scheme can be easily
complex communication structures, including those with parallelism and complex information flow.
As a means to study rich computational structures representable in name passing
processes, a notion of types called sorting was introduced by Milner [12] and has beenstudied extensively since then [1, 19, 2, 16, 17, 10, 18, 4, 9]. Sorting shows how a, and we have aname carries another name. For example, if has a type, say,
, a type which carries nat. This idea andterm, then should have a typeits ramifications have been used to analyse significant semantic properties of calculi
with polyadic name passing. However, as was already noticed in [12], the sorting in
the monadic -calculus is not powerful enough to type-abstract known encodings ofpolyadic name passing like (0.1) above: Indeed, (0.1) becomes ill-sorted if
have different sorts. As far as we know, the situation remains the same with the$\mathrm{g}\mathrm{e}\mathrm{n}\mathrm{e}\mathrm{r}\mathrm{a}\mathrm{l}\mathrm{i}_{\mathrm{S}}\mathrm{e}\mathrm{d}$$v$$\overline{a}v.0$$a$$\mathrm{n}\mathrm{a}\mathrm{t}$$(\mathrm{n}\mathrm{a}\mathrm{t})$$\pi$$v_{1},$ $v_{2},$ $v_{3}$Department of Computer Science, University of Edinburgh, The King’s Buildings, Mayfield Road,-mail: ny@dcs.ed.ac.uk. tel: 44-131-650-4889. fax: 44-131-667-7209.
Edinburgh, EH9$3\mathrm{J}\mathrm{Z},$$\mathrm{U}\mathrm{K}.,$$\mathrm{e}$159
refinements of sorting proposed in [16, 9, 4]. This means, among other things, thesorting restricted to the monadic terms does not give as rich semantic analysis as in
the polyadic case, while behaviourally the above encoding does mimic polyadic namepassing. In general, this is because the sorting does not capture the dynamic structureof interaction, especially those using the transmission of private names as in (0.1) and(0.2), which is omnipresent even in the polyadic setting.
In [22], we develop a syntactic theory of types for monadic -calculus which extends
the sorting in a simple way and by which we can extract the abstract operational
structures of -terms including those of (0.1), (0.2) as well as more complex ones
. The key technical idea is to represent a class of dynamic communicationof mobile processes using simple combinatorial expressions, i.e. graphs. Ina graph type, nodes denote atomic actions and edges denote the activation ordering
between them, representing as a whole a deterministic protocol a process will beengaged in. As a simple example, suppose we have two terms
and. Then they may be given types: Here on the left side, the action
$\pi$

$\pi$

$(\mathrm{c}\mathrm{f}.[22])$$\mathrm{b}\dot{\mathrm{e}}\mathrm{h}\mathrm{a}\mathrm{v}\mathrm{i}\mathrm{o}\mathrm{u}\mathrm{r}$$gb.(CX.\overline{b}x|(f)\overline{d}f.c\prime X.\overline{f}x)$$px.(\overline{c}X|\overline{c’}x)$$*\mathrm{b})-\mathrm{C}\}\mathrm{x}arrow \mathrm{b}\}\mathrm{x}$$\backslash _{\mathrm{d}}\}_{(\mathrm{t}\gammaarrow \mathrm{C}\dagger^{\mathrm{x}}}’arrow \mathrm{f}|\mathrm{x}$(the input of fresh name ) should take place directly preceding
and(and indirectly all the rest), while there is no activation ordering between, forexample,
andin the same graph. Now if two protocols are compatible, wecan compose them via “cuts,” i.e. pairs of complementary atomic actions, to yield
more complex types. Think of the following composition of the above two terms:$b$$g\downarrow(b)$$c\downarrow \mathrm{x}$$d\uparrow(f)$$c\downarrow \mathrm{x}$$f\uparrow \mathrm{x}$$(cc’f)(\overline{g}b.(cX.\overline{b}x|\overline{d}f.C’x.\overline{f}X)|px.(\overline{c}X|\overline{c’}x))$(0.3)

The process of giving a type to this composed term is illustrated in the following.

$\mathrm{O}$The picture shows how the term (0.3) is given a type on the right hand side after theprocedure of “cut elimination.” Notice how the original activation ordering relations
are merged to generate a new relation, so that a proper graph structure arises even
if the original types are trees.1 In the above example, the existence of two arrows
going toshows that the action should take place after its two parent actions takeplace. It also shows how the graph-based representation allows a refined expression$b\uparrow \mathrm{x}$1We also note that such protocol composition enables the distribution and merging of informationin communication, and the increase of parallelism, so can have a practical significance. It also plays
a key role in theory of combinators for mobile processes [6, 7, 21].

160of the flow of control in comparison with the syntactic construct like prefix, while still
keeping a simple combinatorial structure. Compared with sorting and its refinements,
the graph type-. tries to capture dynamic interactive behaviour of name passing proabove) based on a simple graphicalcesses including the new name .assing (as.

expression.

$d\uparrow(f)$$\mathrm{p}$.

$\cdot$.

This departure from the type abstraction of static usage of names to that of dynamic
process behaviour makes it possible to type-abstract many non-trivial computational
structures representable in -calculus. Indeed it allows us to solve Milner’s open
issue mentioned above in a sharper form. We show that not only the encoding ofsorted polyadic -terms into the monadic terms is typable preserving the original
type structure, but also it results in equational full abstraction: letandbesuitably defined behavioural equalities over sorted polyadic -terms and monadic.
terms, respectively. Then we get:
$\pi$

$\pi$

$=_{\mathrm{P}}$$=_{\pi}$$\pi-$$\pi$$\cdot$$P=_{\mathrm{P}}Q\Leftrightarrow[P\mathrm{I}=_{\pi}[Q\mathrm{I}$where [ is the standard encoding from polyadic -terms to monadic -terms. In the”
untyped setting, we can only get(adequacy) direction in terms of usual weak behavioural equivalences. This is due to possible violation of “protocols” by environment
processes, and relates to the lack of precise type abstraction of the communication
structure of various encodings such as (0.1) and (0.2) in preceding type disciplines,
even though the effect of process types on behavioural equalities has been studied
since the work of Pierce and Sangiorgi $[16, 9]$ . In this context, our result (whichseems the first of this kind with respect to the encoding of polyadic name passing)shows how precisely our type discipline captures essential behavioural informationthese protocols carry. What may be surprising is that this can be done using a simple
idea of graph-based types and a small typing system. Moreover the results can beeasily extended to encodings of calculi with more complex communication structures,. We also notice that the polyadic name passing is a typical example of encoding of high-level communication structures into -calculus, cf. [11, 8, 20], so thatthe presented construction and its extensions will hopefully become a basis for using
typed equality over -terms to verify semantic equality of various target languages
and calculi in a uniform framework. The detailed definitions of graph types, the fullabstraction result shown in this abstract and their proofs can be found in [22].
$\pi$$\cdot \mathrm{J}$$\pi$$”\Leftarrow$$\mathrm{c}\mathrm{f}.[22]$

$\pi$

$\pi$

REFERENCES[1] Gay, S., A Sort Inference Algorithm for the Polyadic -Calculus. POPL’93, ACM Press, 1993.
[2] Honda, K., Types for Dyadic Interaction. CONCUR’93, LNCS 715, pp.509-523, Springer-Verlag,
$\pi$

1993.

[3] Honda, K., A Study of -calculus and its Combinatory Representation, Phd Thesis in the Department of Computer Science, October, 1994.
[4] Honda, K., Composing Processes, POPL’g6, pp.344-357, ACM Press, 1996.
[5] Honda, K. and Tokoro, M., An Object Calculus for Asynchronous Communication. ECOOP’91,
LNCS 512, pp.133-147, Springer-Verlag 1991.
[6] Honda, K. and Yoshida, N., Combinatory Representation of Mobile Processes, POPL’94,
pp.348-360, ACM Press, 1994.
$\nu$

161

[7] Honda, K. and Yoshida, N., Replication in Concurrent Combinators, TACS’94, LNCS 789,

pp.786-805, Springer, 1994.
[8] Jones, C.B., Process-Algebraic Foundations for an Object-Based Design Notation.
1, Computer Science Department, Manchester University, 1993.
[9] Kobayashi, N., Pierce, B., and Turner, D., Linear Types and -calculus, POPL’96, pp.358-371,
ACM Press, 1996.
[10] Liu, X. and Walker, D., A polymorphic type system for the polyadic -calculus, CONCUR’95,
LNCS, Springer-Verlag, 1995.
[11] Milner, R., Functions as Processes. Mathematical Structure in Computer Science, 2(2), pp.119146, 1992.
[12] Milner, R., Polyadic -Calculus: a tutorial. Logic and Algebra of Specification, Springer-Verlag,$\mathrm{U}\mathrm{M}\mathrm{C}\mathrm{S}-93- 10-$..

$\pi$.

$\mathrm{p}\mathrm{i}$$\pi$

1992.

[13] Milner, R., Parrow, J.G. and Walker, D.J., A Calculus of Mobile Processes, Information andComputation 100(1), pp.1-77, 1992.
[14] Odersky, M., Applying : Towards a basis for concurrent imperative programming, 2nd. SIPL,
pp.95-108, 1995.
[15] Odersky, M., Polized Name Passing. FSTTCS’15, LNCS, Springer-Verlag, 1995.
[16] Pierce, B.C. and Sangiorgi. D, Typing and subtyping for mobile processes. LICS’93, pp.187-215,$\pi$

1993.

[17] Takeuchi, K., Honda, K. and Kubo, M., An Interaction-based Language and its Typing System.
PARLE’94, LNCS 817, pp.398-413, Springer-Verlag, 1994.
[18] Turner, D., The -calculus: Types, polymorphism and implementation, Phd Thesis, Universityof Edinburgh, 1996.
[19] Vasconcelos, V. and Honda, K., Principal Typing Scheme for Polyadic -Calculus. ONCUR’93,$\pi$$\pi$.C

LNCS 715, pp.524-538, Springer-Verlag, 1993.
[20] Walker, D., Objects in the -calculus. Information and Computation, Vol. 116, pp.253-271,
1995.
[21] Yoshida, N., Graph Notation for Concurrent Combinators, TPPP’94, LNCS 907, pp.393-412,
Springer-Verlag, 1995.
[22] Yoshida, N., Graph Types for obile Process Calculi, To appear in Proc. 16th,LNCS, Springer-Verlag, India, December, 1996. The full version is CS technical report, Keio
University, 1996. Available from ftp.dCS. ed. ac.
. ps. Z.
$\pi$$\dot{\mathrm{M}}$$\mathrm{F}\mathrm{S}\mathrm{T}/\mathrm{T}\mathrm{c}\mathrm{s}’ 16$$\mathrm{u}\mathrm{k}/\exp_{0}\mathrm{r}\mathrm{t}/\mathrm{n}\mathrm{y}/\mathrm{p}\mathrm{u}\mathrm{b}/\mathrm{g}\mathrm{r}\mathrm{a}\mathrm{p}\mathrm{h}1$