数理解析研究所講究録902 巻 1995 年 103-116

103

Concurrent Programming in Linear Logic
Naoki Kobayashi
koba@is.s.u-tokyo.ac.jp

Toshihiro Shimizu
shimizu@is.s.u-tokyo.ac.jp

Akinori Yonezawa
yonezawa@is.s.u-tokyo.ac.jp
Department of lnformation Science
University of Tokyo
7-3-1 Hongo, Bunkyo-ku, Tokyo, 113 Japan

Abstract
HACL is a novel asynchronous concurrent programming language developed
based on linear logic. It provides fruitful mechanisms for concurrent program-style type system.
ming including higher-order concurrency and an elegant
Although HACL provides only a small set of primitive constructs, various constructs for communication and synchronization between processes are definable interms of primitive asynchronous message passing and higher-order processes. In
this paper, we demonstrate the power of HACL by showing several programming
examples. For readers who are not familiar with linear logic and concurrent linear
logic programming, we also give a brief introduction to the logical backgroundof HACL.
$\mathrm{M}\mathrm{L}$1

Introduction

We developed a novel typed, higher-order, concurrent programming language called. ACL is a variant of linear logic
HA CL based on a higher-order extension ofprogramming, whose operational semantics is described in terms of bottom-up search
for a cut-free proof in linear logic. ACL naturally models concurrent computation
based on asynchronous message passing, while traditional concurrent logic program, we
ming languages model stream-based communication. In thecomputation,
have shown most of computational models for asynchronous concurrent
including actor models, Linda, concurrent constraint programming, and asynchronous
counterpart of CCS and -calculus, can be naturally embedded in ACL. The powerof ACL can be further strengthened by replacing the underlying logic with higher(in short, HACL),
order linear logic. The resulting framework, Higher-Orderallows higher-order concurrent programming, where processes can be parameterized$\mathrm{A}\mathrm{C}\mathrm{L}[3][2]$$\mathrm{P}^{\mathrm{r}\mathrm{e}\mathrm{V}\mathrm{i}\mathrm{o}\mathrm{u}\mathrm{S}}.\mathrm{P}^{\mathrm{a}}\mathrm{p}\mathrm{e}\mathrm{r}\mathrm{S}[3][2]$$\pi$$\mathrm{A}\mathrm{C}\mathrm{L}[5]$104

by other processes, communication interfaces, and functions. HACL is also equipped-style type system, hence the type inference system infers thewith an elegant
most general types for untyped programs, and ensures that any well-typed program
never causes type mismatch error at run-time.
The purpose of this paper is to demonstrate the power of HACL by showing
several program.ming examples. Higher-order processes allow us to define a large
process by composing smaller subprocesses, by which improving the modularity andcode reuse of concurrent programs, and are also useful for making topologies between
multiple processes. Therefore, various constructs for concurrent programming, which
are introduced as primitives in an $ad$ hoc manner in many concurrent programming
languages, can be defined using higher-order processes. HACL also allows objectoriented style programming, as is shown in [4]. We believe that HACL can be used
not only as a specific concurrent programming language, but also as a common vehicle
urrent programming languages, to develop
to design novel, clean and powerfulprogramming languages, and to discuss
concurrent
fortechniques
analysisprogramefficient implementation techniques.
Prototype interpreter of HACL and examples given in this paper are available via.
. is. -tokyo. . jp:
anonymous ftp from$\mathrm{M}\mathrm{L}$$\mathrm{c}\mathrm{o}\mathrm{n}\dot{\mathrm{c}}$$\mathrm{c}\dot{\mathrm{a}}\mathrm{m}\mathrm{i}\mathrm{l}\mathrm{l}\mathrm{e}$$\mathrm{s}.\mathrm{u}$2$\mathrm{a}\mathrm{c}$$\mathrm{p}\mathrm{u}\mathrm{b}/\mathrm{h}\mathrm{a}\mathrm{c}\mathrm{l}$Overview of Higher-Order ACL

This section informally overviews the syntax and operational semantics of higherorder ACL. For the concrete definitions, please refer to $[5][4]$ . For readers who are
not familiar with linear logic and concurrent linear logic programming, we attach abrief introduction to both linear logic and its connection with concurrent computationin Appendix.
, computation in Higher-order ACL (in short, HACL)
As in the first-orderis described in terms of bottom-up proof search in Girard’s (higher-order) linear. Each formula of (a fragment of) higher-order linear logic is viewed as aprocess, while each sequent, a multiset of formulas, is regarded as a certain state of
the entire processes. A message is represented by an atomic formula, whose predicate is called a message predicate. The whole syntax of HACL process expressions issummarized in Figure 2. The first column shows textual notations for process expressions. The second column shows corresponding formulas of linear logic. In the figure,over process expresover process expressions, andis ranged over variables,
cess is naturally derived
sions of the form $x(x_{1}, \ldots, xn)=\rangle P$ . A behavior of eachfrom inference rules of linear logic. For example, from the inference shown in theas a process which
Figure 1, we can regard a formula. Message
receives a message
and then behaves like
$x.P
operator.
creates anotation)predicates are created by the $(V, in linear logic
either remessage predicate and binds to it in . A choice, or receives a message
and becomes
and becomesceives a message$\mathrm{A}\mathrm{C}\mathrm{L}[3][2]$$\mathrm{l}\mathrm{o}\mathrm{g}\mathrm{i}\mathrm{c}[1]$

$R$

$P$

$x$

$\mathrm{p}\mathrm{r}o$$\exists x_{1}\cdots\exists x_{n}.(X(x_{1}, \ldots, Xn)^{\perp}\otimes P)$$P[v_{1}/x_{1}, \ldots, v_{n}/x_{n}]^{1}$$x(v_{1}, \ldots, v_{n})$$x$$\mathrm{m}(\mathrm{v})$$P$$\mathrm{P}[\mathrm{v}/\mathrm{x}]$$(\mathrm{m}(\mathrm{x})=\rangle \mathrm{p})\ (\mathrm{n}(\mathrm{X})=\rangle \mathrm{Q})$$\mathrm{n}(\mathrm{v})$1For other correspondence between process transitions and inference rules, please refer to $[3][2]$ .

105$\frac{\vdash x(v_{1},..\cdot.\cdot..\cdot’.v_{n}),x(v_{1},...\cdot.’

v_{n})^{\perp}.\vdash P[v_{1}/x_{1},..\cdot.\cdot.’.v_{n}/xn],\mathrm{r}}{\frac{\vdash x(v_{1},,v_{n})^{\perp}\otimes P[v1/x_{1},..,v_{n}/x_{n}],x(v_{1},.,v_{n}),\Gamma}{\vdash\exists x_{1}\exists x_{n}.(x(x_{1},.,x_{n})^{\perp}\otimes P),x(v1,.,v_{n}),\mathrm{r}}\exists}\otimes$

Figure 1: Inference corresponding to Message Reception$\mathrm{Q}[\mathrm{v}/\mathrm{x}]$. A proc statement defines aa recursive function inproc forwarderforwarder$\mathrm{v}\mathrm{a}l$$\mathrm{M}\mathrm{L}$$\mathrm{r}\mathrm{e}\acute{\mathrm{c}}\mathrm{u}\mathrm{r}\mathrm{S}\mathrm{i}\mathrm{v}\mathrm{e}$. For example,$\mathrm{m}\mathrm{n}=\mathrm{m}\mathrm{x}=>\mathrm{n}\mathrm{x}$process just as a fun statement defines;$=proc:(’ a->\mathit{0})->(’ \mathrm{a}->\mathit{0})_{->}\mathit{0}$defines forwarder as a process which takes two message predicates and as arguments, and receives a value of via a message and sends it via a message . Theline printed in slantedis the system’s output. It indicates that forwarder has
the following type:,$\mathrm{m}$$\mathrm{x}$$\mathrm{n}$$\mathrm{m}$$\mathrm{n}$$\psi \mathrm{y}\mathrm{l}\mathrm{e}$$\forall\alpha.((\alphaarrow \mathit{0})arrow(\alphaarrow \mathit{0})arrow \mathit{0})$where is the type for processes or messages. Therefore, the type of forwarder
implies that it takes two message predicates,
should take an argument of thesame type.2
A process point is defined in HACL as follows:$\mathit{0}$$\mathrm{w}\mathrm{h}\mathrm{i}\mathrm{C}_{\backslash }\mathrm{h}$proc point( , y) (getx,$\mathrm{x}$getx(reply)(reply (x)&gety(reply)

gety, set)$=$$=\rangle$$|$

po int$(\mathrm{x},\mathrm{y})(\mathrm{g}.\mathrm{e}\mathrm{t}\mathrm{x}$, gety, set))$=\rangle$(reply (y) 1 point) $=>$& set (newx,newy,$(\mathrm{x},\mathrm{y})$(getx, gety, set))$\mathrm{a}\mathrm{c}\mathrm{k}$(ack ()$\mathrm{v}\mathrm{a}l$poin

1 point (newx, newy) (getx, gety, set));$t=_{P^{roc}}:’\mathrm{a}*’ b_{->}((’ a_{->O})_{-}>\mathit{0})*((’ \mathrm{a}_{->O})->\mathit{0})*(’ \mathrm{a}*’ b_{->)->}o.\mathit{0}$The process point has two internal state variables and , and is parameterized bymessage predicates getx, gety, and set. If it receives a getx message, it sends thevalue of to the reply destination reply. If it receives a set message, it sends an
acknowledgement message ack $()$ , and changes values of and to newx and newy.
The following expression creates a new point process, and sends to it a getx message.
$\mathrm{x}$$\mathrm{y}$$\mathrm{x}$$\mathrm{x}$$\mathrm{y}$$getx. $gety. $set.
(point (1.0, 2.0) (getx, gety, set)2More refined type system, where$\mathrm{I}/\mathrm{O}$$|$$reply. (getx (reply)

$|$

reply

information of messages is inferred, is given in [5].

$(\mathrm{x})=>$

.

106

$*_{1}\ldots$$*_{2}\ldots$

sends a message
receives a message (, and then behaves likee), and then behaves like $P[e_{1}/x_{1}, \ldots,e_{n}/x_{n}]$$P$$x(e_{1}, \ldots , e_{n})$$x$$e_{1,\ldots,}$

Figure 2: Syntax of HACL process expressions

3

Programming in HACL

of HACL, by showing several examples of conThis section demonstrates the
HACL,processes can be parameterized by othercurrent programming in HACL. In
processes and interfaces (message predicates), just as functions can be parameterizedby other functions in functional programming. This dramatically improves the modularity and code reuse of concurrent programs. We also show that HACL extended
rrent object-oriented style programming.
with records naturally allows$\mathrm{p}\mathrm{o}\mathrm{w}^{\backslash }\mathrm{e}\mathrm{r}$$\mathrm{c}\mathrm{o}\mathrm{n}\mathrm{c}\mathrm{u}\backslash$Object-Oriented Style Programming

3.1

In the definition of point process in the previous section, readers might have noticed
that it is very cumbersome to separately create getx, gety, and set message predicates, and to remember in which order they should be applied to the point process.
In order to overcome this problem, it is very natural to introduce records, and put
the three message predicates together in a record:proc point ( , y) self$\mathrm{x}$$=$(point(x.y) self )#getx self (reply)(
point(x,y) self )& #gety self (reply)(point (newx, newy) self );&#set self (newx, newy)$=\rangle$$\mathrm{r}\mathrm{e}\mathrm{p}\mathrm{l}\mathrm{y}(\mathrm{x})|$$=\rangle$$\mathrm{r}\mathrm{e}\mathrm{p}\mathrm{l}\mathrm{y}(\mathrm{y})|$$=>$$\mathrm{v}al_{P}o.int=proc:’a*’ b->’ C::\mathrm{t}getx:(’ \mathrm{a}->\acute{o})->\mathit{0},$$g\mathrm{e}ty:(’ b->\mathit{0})->\mathit{0},$$set:’ \mathrm{a}*’ b-$$>\mathit{0}\}->O$-name) is an operator for field extraction. The resulting process definition just. self, which is a record consisting
looks like the definition of concurrentof at least three fields getx, gety, and set, can be considered as an identifier ofa concurrent object point. self can be used for sending a message to itself, as in$\#\langle \mathrm{f}\mathrm{i}\mathrm{e}\mathrm{l}\mathrm{d}$$\mathrm{o}\mathrm{b}\mathrm{j}\mathrm{e}\mathrm{c}\mathrm{t}\mathrm{S}[10]$107

ordinary object-oriented languages. The type inference is based on Ohori’s algorithm
for polymorphic record. The inferred type indicates that point takes apair of values of type and as its first argument, and a record of type {getx :, gety:, set:} as its second argument self.
The following is an expression for creating a new point object and sends to it amessage getx.
$\mathrm{c}\mathrm{a}\mathrm{l}\mathrm{C}\mathrm{u}\mathrm{l}\mathrm{u}\mathrm{S}[6]$$\alpha$$(\alphaarrow \mathit{0})arrow \mathit{0}$$\beta$$(\betaarrow \mathit{0})arrow \mathit{0}$$\alpha\cross\betaarrow \mathit{0},$$id. (point (1.0, 2.0) id$|$$\ldots$$reply. (#getx id reply

reply

$|$

$(\mathrm{x})=>$. . .)

If a programmer wants to ensure that messages except for getx, gety, and set arenever sent to the point object, he can explicitly attach the following type constraints
on self:
proc point ( , y) (self: {getx: ’ , gety: ’ , set: ’ )(#getx self (reply)
point(x,y) self )(& #gety self (reply)
point(x,y) self )(newx,(newx,
newy)&#set self(pointnewy) self );point$\mathrm{c}\}$$\mathrm{b}$$\mathrm{X}$$\mathrm{a}$$=\rangle$$\mathrm{r}\mathrm{e}\mathrm{p}\mathrm{l}\mathrm{y}(\mathrm{x})|$$=\rangle$$\mathrm{r}\mathrm{e}\mathrm{p}\mathrm{l}\mathrm{y}(\mathrm{y})$

$=$

$|$

$=>$

$=proc:’ \mathrm{a}*’ b->\{g\mathrm{e}t\mathrm{x}:(’ a->\mathit{0})->\mathit{0}, gety:(’ b->\mathit{0})->0, Set:’$\mathrm{v}\mathrm{a}l$\mathrm{a}*’ b_{-}>\mathit{0}\}-$$>O$

Then, sending a message other than getx, gety and set is statically detected as aninvalid field extraction from the record self.
Based on these observations, we can easily construct a typed concurrent objectoriented programming language with inheritance and method overriding on top of
HACL. By the type system of HACL, all message not understood errors can bestatically detected at type-checking phase.[4]3.2

Synchronization and Sequencing between Processes

It is often important to write synchronization or serialization of execution of processes. Constructs for such purposes can be defined using higher-order processes. For
example, consider the following process seq:proc seq$\mathrm{v}\mathrm{a}l$$(\mathrm{p}1, \mathrm{p}2)=$$token. (pl (token)$|$

token $()=>$ p2 ());

$seq=p\mathrm{r}oc:((\mathrm{u}\mathrm{n}it->\mathit{0})->\mathit{0})*(\mathrm{u}nit->\mathit{0})->\mathit{0}$seq (soutput$(^{\mathrm{t}}’ \mathrm{h}\mathrm{e}110’\dagger)$, fn$()=>\mathrm{o}\mathrm{u}\mathrm{t}\mathrm{p}\mathrm{u}\mathrm{t}(^{11}\mathrm{w}\mathrm{o}\mathrm{r}\mathrm{l}\mathrm{d}\backslash \mathrm{n}\dagger|)$);

hello world

seq
executes a process pl (token) at first, and p2 is invoked only when
the process pl sends a message token . soutput is a built-in process which takes
a string and a message predicate
as an argume. . It displays he string , and$m()$then sends the message.
It is also easy to write processes for realizing broadcast, barrier synchronization,etc. For example, the following process make-group takes a message predicate anda list of processes procs as arguments. Sending a message
from the externals
causes a value of is broadcasted to a process in procs.
$()$$(\mathrm{p}1, \mathrm{p}2)$

$()$

$m$

$s$

$\mathrm{n}\mathrm{t}$$\mathrm{t}$

$s$

$.$

$\mathrm{m}$$\mathrm{m}(\mathrm{x})$

$x$

108

local

proc roadcast
case ns of

ns$\dot{\mathrm{b}}$$\mathrm{x}$$=$nil $=>$$|\mathrm{n}$::($\mathrm{n}\mathrm{s}’=\rangle$$\mathrm{n}(\mathrm{x})|$broadcast$\mathrm{x}\mathrm{n}8’$)inproc broadcaster$\mathrm{m}(\mathrm{x})=>$

ns$\mathrm{m}$$=$(broadcast (1.

$\mathrm{n}\mathrm{s})|$broadcaster$\mathrm{m}\mathrm{n}\mathrm{s}$

)

end
local

proc parapp procs ms
case procs ofnil $=>$: :procs’

$=$

$-$

$=>$

$|\mathrm{p}\mathrm{r}$(case ms of$\mathrm{m}$::$\mathrm{m}\mathrm{s}’=>(\mathrm{p}\mathrm{r}(\mathrm{m})|$parapp procs’$\mathrm{m}\mathrm{s}’)$)inproc make-group$\mathrm{m}$

procs

$=$

let

val

$=$
$\mathrm{g}\mathrm{s}\mathrm{i}\mathrm{z}.\mathrm{e}$in.

length(procs)$\mathrm{m}\mathrm{a}\mathrm{k}\mathrm{e}_{-,-}\mathrm{m}\mathrm{p}\mathrm{r}\mathrm{e}\mathrm{d}_{-\mathrm{S}}1\mathrm{i}\mathrm{t}$(gsize. fn$\mathrm{x}=>$(broadcaster$\mathrm{m}\mathrm{x}|$parapp procs$\mathrm{x})$

)

end
end

Higher-Order Processes for Making Topologies between
Processes

3.3

Higher-order processes in HACL are especially useful for making topologies between
processes. For example, consider the following higher-order process linear:proc linear procs left rightcase procs ofnil $=>$: : nil$|\mathrm{p}\mathrm{r}$$|\mathrm{p}\mathrm{r}$$=>\mathrm{p}\mathrm{r}$: :procs2$=\rangle$$=$(left, right)$link. ( (left, link)$\mathrm{p}\mathrm{r}$$\mathrm{v}alli\mathrm{n}ear=p\mathrm{r}oc:((’ a->\mathit{0})*(’ a->\mathit{0})->\mathit{0})$

list-

$|$

linear procs2 link right);$>(’ a->\mathit{0})->’(a->\mathit{0})->\mathit{0}$We use the notation of ML for the case statement and list expressions. The higherorder process linear takes a list of processes procs as the first argument, and connects them in a linear topology. A ring structure can be constructed by just assigning
the same message predicate to the left and right of linear process.
$\mathrm{p}\dot{\mathrm{r}}$oc ring procs$\mathrm{v}al$$=$$m. (linear procs$ring=p\mathrm{r}oc:((’ \mathrm{a}->\mathit{0})^{*}(’ a->\mathit{0})->\mathit{0})$$\mathrm{m}\mathrm{m}$);$list->\mathit{0}$The dining philosopher problem candescribed by defining a behavior of eachphilosopher, then connecting them by ring:$\dot{\mathrm{b}}\mathrm{e}$

109

2

$[\ovalbox{\tt\small REJECT}\not\equiv 3\cdot 1]$(1)$\mathrm{v}\in \mathrm{V}_{\mathrm{t}}$.

$T$ $\hslash 6$$*9f\approx \mathrm{f}\mathrm{f}\mathrm{l}\mathrm{g}\tau\epsilon \mathrm{P}_{\mathrm{M}}\mathrm{t}\mathrm{y})\emptyset \mathrm{f}\mathrm{f}\mathrm{l}\epsilon*\mathrm{g}\ovalbox{\tt\small REJECT} \mathrm{b}f\underline{\wedge}@\mathrm{f}\mathrm{f}\mathrm{i}$op (PN)$(\mathrm{x})$, label ($\mathrm{g}6l\mathrm{f}$$\delta$*PM*PM (x)$(,\mathrm{x})\Leftrightarrow \mathrm{P}\mathrm{M}\langle \mathrm{y}${(I$\ovalbox{\tt\small REJECT}$(PM (y) )$2\rangle \mathrm{v}\in \mathrm{V}_{\mathrm{b}\mathrm{o}\mathrm{t}}$

ff,#

.2

.

$\theta_{\mathrm{P}}\not\in 3$]$\omega^{-}\mathrm{F}\vee \mathfrak{M}0\ovalbox{\tt\small REJECT}\gtrless$ii)$\mathrm{z}[(1,1\rangle , (\mathrm{m}, 2\mathrm{m})]=\mathrm{x}[\mathrm{t}1,1),$.

$\mathcal{E}T6$

mM5-ト$arrow\veearrow \mathrm{T}^{\backslash }\vee,$:$\underline{(^{\sim}1}r1\mathrm{v}:=\mathrm{v}_{0}\epsilon h^{\backslash }<$$\mathrm{b}\mathrm{b}*$$\cap\underline{2}$8. 1 3:.

$\ovalbox{\tt\small REJECT}\not\equiv 3$$\Rightarrow*\grave{[}\mathrm{R}\mathrm{o}^{\sim}\mathrm{g}\beta f\mathrm{g}$

$|?$

,

.

-k

$6L^{\mathrm{r}}\mathfrak{l}_{arrow}\wedge$\S . 2,,$\mathrm{u}_{1},\ldots$

,

)

フ x

$\mathrm{v}_{2},\ldots$,. ... ,

. a $T6$$\tau\cdot r_{J}\mathrm{t}\gamma nl\mathrm{f}$,$\mathrm{P}_{\mathrm{M}}(\mathrm{x})\mathrm{e}$PM$\not\in$$,$A$\mathrm{Y}6$.

$\mathrm{t}\mathrm{y}$))$\downarrow \mathcal{O}$6&6$\mathrm{a}\Re_{\grave{1}}\underline{langle}$,$l\mathrm{f}$’$\mathrm{v}:=\mathrm{v}$$( arrow \mathrm{Y}\mathrm{x}\Phi^{\Rightarrow}\mathrm{s}+\geqq*if8\mathrm{o}^{rightarrow 5_{\backslash }}\mathrm{B}\mathbb{R}i.\mathrm{r} \mathrm{v}_{1\{}\mathrm{b}\mathrm{b}\langle l\mathrm{f} \mathrm{u}_{\mathrm{J}}\mathit{0})\prod \mathrm{r}\hslash$$p\backslash \yen^{p_{1}}\backslash \backslash t\mathrm{t}\gamma_{\simeq}p\backslash ^{*}$$arrow\veearrow T\vee\cdot \mathrm{t}\mathrm{f}$,$a\equiv \text{ト}\Rightarrow \mathrm{f}\mathrm{f}\mathrm{i}\ovalbox{\tt\small REJECT} \mathrm{p}_{\kappa()}\mathrm{Z}$’$arrowarrow n\mathrm{t}\mathrm{f}$$\mathrm{T}\mathrm{l}\mathrm{M}$)&ffl;\Rea$\tau$$arrow\vee\succeq f\mathrm{g}$$–\mathrm{T}_{1}r_{\mathrm{a}^{\backslash }}\epsilon\ovalbox{\tt\small REJECT} \mathrm{t}V\omega \mathfrak{R}\overline{i\mathrm{E}}\iota_{\sim \mathrm{B}}^{\wedge}T$,...

ffi7 ,$\mathrm{u}_{4},\mathrm{v}_{4}$,,)$.\mathit{9}_{\backslash \backslash }\mathrm{V}8\not\in\emptyset \text{フ^{}p}-\backslash \cdot$$\backslash \triangleright 1\mathrm{a}\mathrm{L}^{r}\mathrm{e}1\{\iota^{*})\mathrm{g}\subset,c\mathrm{B}|\mathrm{J}\mathrm{b}\gamma_{\mathrm{d}\backslash }\backslash$\S$\mathcal{E}\mathrm{y}\mathrm{t}_{\vee}^{\sim}X\backslash \mathrm{f}\mathrm{Y}$$\mathrm{v}_{3},\mathrm{u}_{9}.,\ldots$$\ldots,\mathrm{u}’ 2,$ $\backslash ^{r}\mathrm{s},\ldots,\mathrm{V}’ 3,$$\mathcal{E}\not\equiv<\sigma_{-}\star t\iota\delta 4_{\circ\emptyset 8\tau\S}(\mathrm{E}^{\backslash }2$$6$$\mathrm{t}\delta \mathrm{s}_{\mathrm{P}_{\mathrm{b}\mathrm{t}}\mathrm{t}\mathrm{y}\rangle}(\mathrm{v}))$.
.

$\square$$\backslash /\mathrm{A}\overline{\pi}\overline{\tau}-$,$(\mathrm{v}))$$2\mathrm{m})]$$k\mathfrak{B}\#$$\mathrm{v}_{0}$$\circ$$\mathrm{u}\mathrm{z}$)$\acute{\mathrm{x}}\mathrm{g}\mathrm{R}\equiv+a\Rightarrow \mathrm{E}\Re$us,$\mathrm{v}\mathrm{s},$,$\ldots$PN$1\mathrm{x}$), PN (y),$p\backslash \not\in r\iota\epsilon\hslash$$\mathrm{u}\epsilon,\mathrm{v}_{6},\ldots,\mathrm{v}-,\mathrm{u}_{7},\ldots,\mathrm{u}_{8},\mathrm{v}_{8}$...

,$\mathrm{v}’ 1,\mathrm{u}_{3},$$\not\simeq’k^{\lambda}*\grave{)}\underline{\Phi}$$\mathrm{t}2\mathrm{m},$$\emptyset\hslash 6\mathrm{L}(\mathrm{m}\mathrm{I}\mathrm{f}\mathrm{f}\mathrm{i}\Phi\Phi\overline{j\mathrm{E}}\mathrm{X}\mathrm{I}\mathrm{E}\mathrm{g}$$\mathrm{z}\in \mathrm{T}\mathrm{t}\mathrm{M}$’$1^{)}\mathrm{c}arrow \mathcal{E}l_{arrow}^{arrow}\tau$\={o}$\not\in$$\mathrm{r}\mathrm{m}3\cdot 1]\mathrm{R}\mathfrak{B}_{\mathrm{c}}^{*}\mathrm{g}^{\tau}\not\in\downarrow \mathrm{r}\xi rarrow\emptyset\vee$

$,$

,

.

$\ovalbox{\tt\small REJECT}\Re \mathrm{v}\emptyset \mathrm{f}\mathrm{F}\emptyset’\yen_{\backslash }p_{t}\int\emptyset\backslash ^{*}$$(\mathrm{z}\not\in \mathrm{T}_{1}f_{-\dot{|}}^{\sim\pm}grightarrow)$$\mathrm{t}\mathrm{x}$$\mathrm{b}\gamma_{\simeq}2r\lambda\overline{\pi}\overline{\mathcal{T}}-\text{フ^{}\mathrm{o}}$.

$\mathrm{k}^{\backslash }1\backslash \tau_{\mathrm{c}}|\gamma 2\epsilon\ovalbox{\tt\small REJECT} \mathfrak{y}\grave{x}\underline{\mathrm{B}}\tau$$l^{\backslash }A4_{\mathrm{i}}b_{-\lambda}^{arrow}\mathfrak{y}$$\nwarrow r_{1}$ae$\delta\star(\mathrm{v})_{-}-\{\mathrm{V}’\}\gamma x\epsilon^{\mathrm{m}}\epsilon \mathrm{p}|\mathrm{g}_{\backslash }.\iota^{r}$$’\in \mathrm{V}\{\mathrm{p}_{\mathrm{N}}(\mathrm{X})\ominus \mathrm{p}_{\mathrm{M}(}\mathrm{y}))\delta^{\mathrm{i}^{\backslash }}T\neq\not\in\tau$$p\backslash *(-\not\in \mathrm{i}_{\backslash r’\cdot\backslash }\mathrm{a}g\mathrm{g}T\delta)\mathrm{M}\emptyset \mathrm{z}$$\mathrm{E}\int \mathrm{j}6\theta^{1}$

... ,

label

$(\mathrm{v}))=$

fPM,$(\mathrm{m}, 2\mathrm{m})]$$\mathrm{z}[(\mathrm{m}+1,1\rangle , (2\mathrm{m}, 2\mathrm{m})]=\mathrm{y}[\mathrm{l}\mathrm{m}+1,1)$$\epsilon\Rightarrow\overline{\mathrm{X}}6$.

)$\delta$,$\mathrm{Q}_{1}(\mathrm{z})=\mathrm{n}_{2}(\mathrm{Z})--_{2\mathrm{m}}$iii)$\prime_{d^{\backslash }}$$\mathrm{e}\mathrm{P}u\langle \mathrm{y}$$\mathrm{z}\xi \mathrm{x}\emptyset\lrcorner_{\mathrm{i}}\#\epsilon\epsilon \mathrm{y}\omega^{-}\mathrm{r}*9\#\backslash \not\in$

i)

...

$\delta$label 1$\langle \mathrm{v}\rangle)=$$\Re\rangle$$T^{r_{Jb\mathrm{t}}}$\S, label ($r_{J}\mathrm{e}\iota \mathrm{f}$)f#$\llcorner f\underline{arrow}2tfi\backslash \overline{\pi}\overline{\mathcal{T}}-$

フo

(a)

... ,

,

$\mathrm{U}5,\ldots,\mathrm{u}’ 4,\mathrm{v}_{2}$$r_{J}6(y.

$\tau^{\gamma}$.

’ $\mathrm{s},\mathrm{u}_{1},\ldots,\mathrm{u}’ 6,\mathrm{v}_{6},\ldots,\mathrm{V}’ 7,\mathrm{u}_{7},\ldots,\mathrm{u}’ 8,\mathrm{v}_{6}\ldots$\}_{\sim}^{\wedge}(\mathrm{b})e\sim*\#\mathrm{P}\backslash )$$\mathrm{Z}t\approx \mathrm{x}_{\backslash }\iota \mathrm{b}T*;^{\backslash }\lambda\emptyset$A.

$-\vee\emptyset \mathcal{E}\mathrm{g}$$\mathrm{X}\emptyset \mathrm{k}-*9\epsilon \mathrm{y}\emptyset\uparrow$)$*\overline{\supset}^{\gamma.p}\mathrm{d}^{\backslash }\mathrm{X}\mathrm{E}\overline{\exists}+\mathrm{r}\Rightarrow \mathrm{f}\mathrm{f}_{L}\Re \mathrm{P}_{\mathrm{M}}\mathrm{t}\mathrm{Z}$$’$$\theta \mathrm{l}$ffl ffi$\mathrm{S}n$$\mathrm{v}_{1},\mathrm{u}_{1},\ldots,\mathrm{u}’\epsilon,\mathrm{v}\iota,\ldots,\mathrm{v}_{5},\mathrm{u}_{5},\ldots,\mathrm{u}’ 4,\mathrm{v}_{2},\ldots,\mathrm{v}_{3},\mathrm{u}_{3},\ldots,\mathrm{u}’ 2,\mathrm{v}_{8}\ldots$$( \mathrm{E}2(\mathrm{c})4\sim\approx\oint \mathrm{e}\backslash )\square$$[\mathrm{f}\mathrm{f}\mathrm{l} \ovalbox{\tt\small REJECT} 3.

$\mathrm{b}T$

2 \sigma 2\ovalbox{\tt\small REJECT}^{\beta}\beta\sigma)\ovalbox{\tt\small REJECT} \mathrm{g}]$$8\mathrm{E}6\delta\backslash \mathrm{t}\sim|arrow,$$|\mathrm{V}(\mathrm{m})|=(2\mathrm{m}$I$\mathrm{m}T^{\backslash }b6$,{$\mathrm{C}(\mathrm{m})=$$\mathrm{C}\mathrm{r}\mathrm{o}\mathrm{s}\mathrm{s}_{-}\mathrm{P}\mathrm{a}\mathrm{i}\mathrm{r}$(PN$1\mathrm{x}\rangle$)$|\exists \mathrm{x}\in \mathrm{V}\mathrm{l}\mathrm{m})$[PM8$\llcorner \mathrm{e}[\mathrm{m}]/2_{\mathrm{J}}$$\mathrm{L}_{-}^{-}\mathrm{o}\Sigma$$p\backslash ;\mathfrak{X}\mathfrak{y}\mathrm{E}\cdot\supset$ク“$\text{フ}-$5-ト$\Rightarrow \mathrm{E}$

ffl]

}

,

$|\mathrm{C}(\mathrm{m})|\leqq$2$\mathrm{g}_{\mathrm{m}\underline{\rangle}1}\iota_{-\Re}^{\sim}$$(\mathrm{X})\iota \mathrm{f}\mathrm{M}\mathrm{o}_{\mathrm{X}_{-}\mathrm{b}}\emptyset$$\mathrm{L}(\mathrm{m})\mathrm{f}\mathrm{f}\mathrm{i}\mathfrak{B}\Phi_{\hat{\mathrm{E}}^{\mathfrak{B}}}\mathrm{J}\mathrm{g}\mathrm{x}$$k^{\backslash }\mathrm{t}\mathrm{J}l\mathrm{f}$. $-x,$

フ.

$arrow\veearrow\vee l_{\sim}^{\wedge}$$\mathrm{G}\mathrm{o}_{\mathrm{R}}^{\mathrm{m}_{\beta}}$A,. $\leqq$$\mathrm{e}[\mathrm{m}]=\mathrm{s}(2\mathrm{m}+2)\mathrm{L}\{2\mathrm{m}\rangle$」,$k_{\dot{\mathfrak{Q}}}^{\Delta}$$\mathrm{a}\ovalbox{\tt\small REJECT}_{\square ^{\hslash\backslash ^{\backslash }}}^{\mathrm{A}}\backslash$,$\{\mathrm{e}[\mathrm{m}]\mathrm{L}=0\Sigma\}\leqq 222\cdot \mathrm{e}[\mathrm{m}]$$\mathrm{t}^{\mathrm{L}\mathrm{t}2\mathrm{m})}$$\epsilon n\epsilon n\mathrm{v}\mathrm{t}\mathrm{G}$$\delta \mathrm{s}_{\mathrm{G}(_{\mathrm{V}})}=\{\mathrm{v}’\in \mathrm{v}\langle \mathrm{G}\}|1\mathrm{v},\backslash \gamma’)\in \mathrm{E}\mathrm{t}\mathrm{G})\}\epsilon\not\in\ovalbox{\tt\small REJECT} T\epsilon$

.

,
),

$\mathrm{S}$tf$\mathrm{M}\emptyset\#\Phi$$\mathrm{E}(\mathrm{G})\emptyset\epsilon \mathrm{g},$ffiJ$\ovalbox{\tt\small REJECT} \mathrm{f}\mathrm{f}\mathrm{l}\emptyset*\ovalbox{\tt\small REJECT}\Re$,$\mathrm{t}$$\Leftrightarrow \mathrm{V}\in \mathrm{V}(\mathrm{G})\iota_{-}^{\sim}\Re \mathrm{b}T$

,

110

(
$\mathrm{v}al$point$\mathrm{a}\mathrm{c}\mathrm{k}()$

point

$|$

$(\mathrm{x}+\mathrm{d}\mathrm{x}+0.0,$

self );$\mathrm{y}\star \mathrm{d}\mathrm{y}+0.0)$$get_{X}:(real->\mathit{0})->\mathit{0},$$=p\mathrm{r}oc:real^{*}real->’ \mathrm{a}::\{get\mathrm{X}:(\mathrm{r}ea\iota_{-}>\mathit{0})_{->}\mathit{0},$$mo\mathrm{V}e.re\mathrm{a}\mathit{1}*era\mathit{1}*(\mathrm{u}\mathrm{n}it$$>\mathit{0})->\mathit{0}\}->O$

We can define a rectangle process by composing two point processes as follows.
local

proc rectangle’$(\mathrm{p}1, \mathrm{p}2)$#getcx self (reply)($m. (#getx pl(reply& #getcy self (reply)($m. (#gety pl(reply& #move self

self

$–$

$=>$
$\mathrm{m}|\mathrm{m}(\mathrm{x}\mathrm{l})-->$$((\mathrm{x}1+\mathrm{X}2)/2.0)$(#getx p2
rectangle’$\mathrm{m}|\mathrm{m}(\mathrm{x}2)=>$$|$$(\mathrm{p}1,$$\mathrm{p}2)$self ) $)))$$=>$

m(yl) $=>$ (#gety p2
rectangle’$\mathrm{m}|\mathrm{m}(\mathrm{y}2)=>$$\mathrm{m}|$$((\mathrm{y}\mathrm{l}+\mathrm{y}2)/2.0)$$|$$(\mathrm{p}1,$$\mathrm{p}2)$self ) $)))$$(\mathrm{d}\mathrm{x}, \mathrm{d}\mathrm{y}, \mathrm{a}\mathrm{c}\mathrm{k})=>$($ack2. (#move pl ($|$$\mathrm{d}\mathrm{x},\mathrm{d}\mathrm{y}$ack2 $()=>$ (, ack2)$\#\mathrm{m}\mathrm{o}\mathrm{v}\mathrm{e}$p2$(\mathrm{d}\mathrm{x},\mathrm{d}\mathrm{y},\mathrm{a}\mathrm{C}\mathrm{k})$$|$rectangle2$(\mathrm{p}1,$$\mathrm{p}2)$inproc rectangle (pointl, point2) self
$idl. $id2. (point 1 idl

$|$

$=$

point2 id2

rectangle’$|$$(\mathrm{i}\mathrm{d}\mathrm{l},$$\mathrm{i}\mathrm{d}2)$

self )

end;

A particular instance of rectangle process is created by instantiating pl and p2 topoint processes as follows:

proc new-rectangle$(\mathrm{x}1, \mathrm{y}1, \mathrm{x}2, \mathrm{y}2)$

rectangle (point$\mathrm{v}\mathrm{a}l\mathrm{n}$ew-rectangle$>\mathit{0})->O,$$(\mathrm{x}1,$$\mathrm{y}1)$

self, point$=$$(\mathrm{x}2,$$\mathrm{y}2)$) self;$=proc:re\mathrm{a}l*real*real*\mathrm{r}eal->’ \mathrm{a}::\{get_{C}X:(real->\mathit{0})->\mathit{0},$ $getcy:(\mathrm{r}e\mathrm{a}l-$$\mathrm{m}o\mathrm{v}e.real*_{r}*e\mathrm{a}l$( nit$\mathrm{u}$$>\mathit{0}$)$->0\}->\mathit{0}$Important point about the above rectangle process is that it is independent of aparticular implementation of point processes. Let point2 be another implementationof the point process. Then, we can make a rectangle process by applying point2
instead of point:proc new-rectangle2$(\mathrm{x}1, \mathrm{y}1, \mathrm{x}2, \mathrm{y}2)$

rectangle (point2

3.5$(\mathrm{x}1,$$\mathrm{y}1)$

self, point2$=$$(\mathrm{x}2,$$\mathrm{y}2)$) self;Atomic Execution of Methods

Some of successive executions of methods should be made atomic. For example, consider the point process in the previous section. When implementing a move method
using getx, gety, and set methods, one might want to invoke getx, gety, and set
methods atomically, so that values of and are not changed by other objects between executions of the getx method and the set method. The following lpoint
process allows such an atomic execution of methods.
$\mathrm{x}$$\mathrm{y}$self )

111

local

proc philosopher(lfork, rfork)( get left and right forks )lfork$\mathrm{n}$

$*$

$=$

$*$

$()=>\mathrm{r}\mathrm{f}\mathrm{o}\mathrm{r}\mathrm{k}()=>$(

start eating )),seq (soutput (makestring: I am( finish eating )fnoutput(make string: ini( release forks, and )fn
rfork $()$
( repeat the same behavior )(lfork, rfork) $))))$ ,philosopher
$*$

$*$

$(\mathrm{n})^{-\uparrow\dagger}$$*$$\mathrm{e}\mathrm{a}\mathrm{t}\mathrm{i}\mathrm{n}\mathrm{g}\backslash \mathrm{n}||$$*$J$()=>_{\mathrm{S}}\mathrm{e}\mathrm{q}(\mathrm{s}$$(\mathrm{n}$$*$$)\sim \mathrm{t}\mathrm{t}$$\mathrm{f}$$\mathrm{s}\mathrm{h}\mathrm{e}\mathrm{d}\backslash \mathrm{n}^{\mathfrak{l}\mathfrak{l}}$

),

$*$

$()=>(\mathrm{l}\mathrm{f}\mathrm{o}\mathrm{r}\mathrm{k}()$

$|$

$*$

$*$

$|$

$\mathrm{n}$

in
proc

$\mathrm{p}\mathrm{h}\mathrm{i}\mathrm{l}\mathrm{o}\mathrm{s}\mathrm{o}\mathrm{P}\mathrm{h}\mathrm{e}\mathrm{r}-\mathrm{a}\mathrm{n}\mathrm{d}_{-\mathrm{o}\mathrm{r}}\mathrm{f}\mathrm{k}\mathrm{n}$(lfork, rfork)

lfork $()$
end;
fun nlist

ifproc philosophers $()$$\mathrm{n}\mathrm{f}=$$\mathrm{n}=0$then nil else$=$ring (nlist 5$|$$\mathrm{f}(\mathrm{n})$$=$philospher: : (nlist$\mathrm{n}$(lfork. rfork)$(\mathrm{n}-1)$

f );
);

$\mathrm{p}\mathrm{h}\mathrm{i}\mathrm{l}\mathrm{o}\mathrm{S}\mathrm{o}\mathrm{p}\mathrm{h}\mathrm{e}\mathrm{r}-\mathrm{a}\mathrm{n}\mathrm{d}_{-}\mathrm{f}\mathrm{o}\mathrm{r}\mathrm{k}$philosophers $()$ ;5: am eating
5: finished
3: am eating
1: am ting
3: finished
$I$

$I$

$I$

$e\mathrm{a}$In the same manner, we can also define higher-order processes for making any topologies between processes, such as mesh topology and torus topology. Note that thiskind of programming was cumbersome with traditional concurrent object-oriented
languages such as.
$\mathrm{A}\mathrm{B}\mathrm{C}\mathrm{L}[9]$3.4

Hierarc-hical Construction of Processes

By using higher-order processes, we can construct a large process by composing
smaller subprocesses. Although it might look possible with only first-order processes(as is shown in [3]), higher-order processes are very important in the sense that it
makes a process independent of a particular implementation of its subcomponent
processes, by which enhancing the modularity.
For example, consider the following point process:proc point ( , y) self
#getx self (reply)& #gety self (reply)& #move self$\mathrm{X}$$=$$=\rangle$$=\rangle$(($\mathrm{r}\mathrm{e}\mathrm{p}\mathrm{l}\mathrm{y}(\mathrm{x})|\mathrm{p}\mathrm{o}\mathrm{i}\mathrm{n}\mathrm{t}(\mathrm{x}$$\mathrm{r}\mathrm{e}\mathrm{p}\mathrm{l}\mathrm{y}(\mathrm{y})|\mathrm{p}_{\mathrm{o}\mathrm{i}}\mathrm{n}\mathrm{t}(\mathrm{x}$$(\mathrm{d}\mathrm{x}, \mathrm{d}\mathrm{y}, \mathrm{a}\mathrm{c}\mathrm{k})=\rangle$.

y) self ), y) self )112proc lpoint (x.y,oldself ) self
$lock self (reply)$key. (reply(key)& #unlock self(case oldself of self ’ : : oldself ’...
&#getx self (reply)& #getx self (reply)) $=>\ldots$ ;&#set self (newx, newy,
$=$

$=>$

$()$

$|$

lpoint$(\mathrm{x},\mathrm{y}$lpoint$(\mathrm{x},\mathrm{y}$, self: : oldself ) key)$=>$$=\rangle$$=\rangle$$=\rangle$, oldself ’) self ’)...

$\mathrm{a}\mathrm{c}\mathrm{k}$proc new-lpoint( , y) self$\mathrm{X}$$=$lpointself;$(\mathrm{X}, \mathrm{y}, [])$

Then, a lpoint can be moved as follows: (l)send lock message to the lpoint process, and get key, (2)getx and gety messages to key, and get values of and ,a unlock message. This kind of programa set message to key, and (4)(3)
ming is possible because communication interfaces (message predicates, or identity)of each process can be directly manipulated in HACL.
$\mathrm{s}\mathrm{e}\mathrm{n}\mathrm{d}$$\mathrm{x}$$\mathrm{y}$$\mathrm{s}\mathrm{e}\mathrm{n}\mathrm{d}$$\mathrm{s}\mathrm{e}\mathrm{n}\mathrm{d}$3.6

Invocation of Processes from Functions, and toHACL allows functions to be defined using a fun statement just as intoinvokeexpression
catch
be called from a process. Conversely, HACL also has theprocesses from a function. The catch expression takes the following form:$\mathrm{M}\mathrm{L}$catch $m$ in

$p$

end,

which means “create a new message predicate , and execute a process . If a
is eventually sent, the whole expression is evaluated to ”
message$m$ in) $/x$ ] can be considered an abbreviated form of the following expression.
$m$

$p$

$m(\mathrm{v})$$\mathrm{v}.$$\mathrm{e}[(\mathrm{c}\mathrm{a}\mathrm{t}_{\mathrm{C}\mathrm{h}}$$p\mathrm{e}\mathrm{n}\mathrm{d}$$m. (p1$\mathrm{m}(\mathrm{x})=>\mathrm{e}$The following function)$\mathrm{p}\mathrm{f}$ib computes the fibonacci number in parallel.

fun fib (n)ifthen 1 else if;
ibelse fibfun pfib(n)then fib(n)ifelse catch result$=$$\mathrm{n}=1$$\mathrm{n}=0$$(\mathrm{n}-1)+_{\mathrm{f}}$then 1$(\mathrm{n}-2)$$=$$\mathrm{n}<5$in$ml. $m2. (ml (pf ib$(\mathrm{n}-2)$)$|$m2 (pfibresult$|\mathrm{m}1(\mathrm{x})=\rangle \mathrm{m}2(\mathrm{y})=>$$(\mathrm{n}-1)$)$(\mathrm{x}+\mathrm{y}))$

.

end;

If is less than 5, pfib (n) computes the fibonnaci number sequentially. Otherwise
in parallel, and add results. In this manner,and pfib
computes pfib
processes can be easily invoked from functions, and vice versa.
$\mathrm{n}$$(\mathrm{n}-2)$$(\mathrm{n}-1)$

113

Related Work

4

Pierce andare developing a concurrent language called PICT, based on
Milner’s -calculus. We believe that concurrent linear logic programming potentiallyoffers a more fruitful programming model than -calculus; It can formalize many kindsofincluding Linda’s generative communication, and also allow anatural integration with traditional logic programming.
$\mathrm{T}\mathrm{u}\mathrm{r}\mathrm{n}\mathrm{e}\mathrm{r}[7]$

$\pi$

$\pi$

$\mathrm{c}\mathrm{o}\mathrm{m}\mathrm{m}\mathrm{u}\mathrm{n}\mathrm{i}\mathrm{c}\mathrm{a}\mathrm{t}_{!}\mathrm{o}\mathrm{n}[2]$5Conclusion

We proposed HACL, a higher-order extension of the concurrent linear logic programming language ACL. Outstanding features of HACL include higher-order processes,
which dramatically enhances the modularity of concurrent programs, and the elegant-style type system. We demonstrated the power of HACL by showing several examples. We have already implemented a prototype system of HACL. We are currently
developing an efficient compiler system for HACL. Our current work also includes thedesign of a high-level concurrent object-oriented language on top of HACL, and thedevelopment of static analysis techniques for concurrent programs based on HACL.
It would be also interesting to integrate HACL with traditional logic programming.
$\mathrm{M}\mathrm{L}$-References[1] Girard, J.-Y., “Linear Logic,” Theoretical Computer Science, vol. 50, pp. 1-102,

1987.
[2] Kobayashi, N., and A. Yonezawa, “Asynchronous Communication Model Basedon Linear Logic.” to appear in Journal of Formal Aspects of Computing,Springer-Verlag.
[3] Kobayashi, N., and A. Yonezawa, “ACL–A Concurrent Linear Logic Programming Paradigm,” in Logic Programming: Proceedings of the 1993 International
Symposium, pp. 279-294, MIT Press, 1993.
[4] Kobayashi, N., and A. Yonezawa, “Type-Theoretic Foundations for Concurrent
Object-Oriented Programming,” in Proceedings of $ACM$ SIGPLAN Conference
on Object-Oriented Progmmmingand Applications (OOP, to appear, 1994.
$\mathrm{s}_{y_{Ste}m\mathit{8}},$$Language\mathrm{s}_{f}$$SLA’ \mathit{9}\mathit{4})$[5] Kobayashi, N., and A. Yonezawa, “Typed Higher-Order Concurrent Linear Logic. Programming,” Tech. Rep. 94-12, Department of Information Science, Universityof Tokyo, 1994. to be presented at Theory and Practice of Parallel Programming, Sendai, Japan.
$(\mathrm{T}\mathrm{P}\mathrm{P}\mathrm{p}’ 94)$[6] Ohori, A., “A Compilation Method for ML-Style Polymorphic Record Calculi,”
in Proceedings of $ACM$ SIGA $CT/SIGPLAN$ Symposium on Principles of Programming Language, pp. 154-165, 1992.

114[7] Pierce, B. C., “Programming in the Pi-Calculus: An Experiment in Programming Language Design.” Lecture notes for a course at the LFCS, University of
Edinburgh., 1993.

[8] Troelstra, A. S., “Tutorial on Linear Logic,” 1992. Tutorial notes in JICSLP’92.

[9] Yonezawa, A., ABCL: An Object-Oriented Concurrent System. MIT Press, 1990.
[10] Yonezawa, A., and M. Tokoro,
MIT Press, 1987.

A$O\acute{b}ject$-Oriented Concurrent Programming. The

The Essence of Concurrent Linear Logic Pro-

gramming
Brief

A.l

Guid.e to Linear Logic

This section gives an intuitive idea for understanding Girard’s linear, using
the well-known examples.[8] Let us consider the following three formulas $A,$ $B$ and:$\mathrm{l}\mathrm{o}\mathrm{g}\mathrm{i}\mathrm{c}[1]$

$C$

$A$

$B$
$C$

: You have one dollar.
: You can buy a chocolate.
: You can buy a candy.

We assume here that each of a chocolate and a candy costs $1. Then, it is trivial that
implies $B$ , and implies . But what’s the meaning of “implies”? Let’s consider
it as an implication in classical logic, that is, interpret “A implies $B$ ” as “ $A\supset B$ ”
and “A implies ” as “ $A\supset C.$ ” Then, we can deduce( $B$ A ) from $A\supset B$ and$A\supset C$. Therefore, we are led to the strange conclusion that “if you have one dollar,
then you can buy a chocolate and a candy.”
What was wrong with the above reasoning? It was the interpretation of “ implies.”
If you have one dollar, then you can buy a chocolate, but at the same time, you lose
one dollar, that is, you can deduce $B$ from , but you do not have any more. In
order to express the above “implies,” we need to introduce a new implication $‘-0$ ’of linear logic, which is called linear implication.
means that if we have ,$B$$con\mathit{8}umingA$
we can obtain by. Therefore, each formula of linear logic should beconsidered as a kind of consumable resource.
Going back to the above example, we also need to reconsider the interpretation of“and.” If you have one dollar, it is both true that you can buy a chocolate and thatyou can buy a candy. But they cannot be true at the same time. In order to express
it, we need to use ‘&’, one of linear logic conjunctions. $A-0$ B&C means that “wecan obtain any one of $B$ and from , but not both at the same time”. In contrast,
the other linear logic conjunction $‘ A\otimes B$ ’ means that we have both $A\otimes B$ at thesame time. Therefore,means that “If you have one dollar and one
dollar (that is, two dollars), you can buy both a chocolate and a candy at the sametime (and you lose two dollars!).”
$A$

$A$

$C$

$C$

$A\supset$

$A$

$A$

$A-\mathrm{o}B$

$C$

$A$

$A\otimes A-\mathrm{o}B\otimes C$

$C$

$A$

115

Linear logic$\mathrm{d}\mathrm{i}\mathrm{s}\mathrm{j}\mathrm{u}\mathrm{n}\mathrm{c}\mathrm{t}\mathrm{i}_{\mathrm{o}\mathrm{n}}\oplus \mathrm{a}\mathrm{n}\mathrm{d}\mathit{8}$is respectively de Morgan dual of&and\otimes :$(A\ B)^{\perp}\equiv A^{\perp}\oplus B\perp$$(A\otimes B)^{\perp}\equiv A^{\perp_{\mathit{8}}}B^{\perp}$

a linear negation. $A\oplus B$ means that “at least one of and holds.”
where
A. 1
can be also defined as(Compare with A&B.)
connectives
forsymbolsofchoiceGirard’s
above
respectively unit of\otimes and&. The
seems to be motivated by the following distributive laws:$A$$(\bullet)^{\perp}\mathrm{i}_{\mathrm{S}}$$A^{\perp}-\mathrm{o}B\equiv B^{\perp}-0$$A^{)}\mathit{8}B$$B$$\mathrm{a}\mathrm{n}\mathrm{d}\perp \mathrm{i}\mathrm{s}$$A\otimes(B\oplus c)\equiv(A\otimes B)\oplus(A\otimes C)$

A&(B\epsilon C)\equiv (A&B)\epsilon (A&C)
Girard also introduced exponential ‘!’ for expressing unbounded resource. If wehave ‘ ! $A’$ , we can use any number of times. ‘?’ is de Morgan dual of ‘!’.
$A$

Connection between Linear Logic and Concurrent Computation

A.2

What is the connection between linear logic and concurrent computation?3
Consider the situation where multiple processes perform computation while communication with each other via asynchronous message passing. Each message disappears after read by a process, that is, a message is a consumable resource. Therefore,
it is natural to interpret a message as a formula of linear logic. From now on, we represent a message by an atomic formula of linear logic. How about process? Consider
a process , which waits for a message and behaves like after reception. con.
sumes $m$ and produces , hence is interpreted by a linear logic implication
Therefore, a process is also represented by a formula of linear logic. Consumption ofis represented by the following deduction:a message $m$ by a process
$A$

$B$

$m$

$m-\mathrm{o}B$

$A$

$B$

$A$

$m-\triangleleft B$$m\otimes(m-\mathrm{o}B)\otimes c-\mathrm{o}B\otimes C$

where can be considered as other processes and messages, or an environment. Notethat we cannot interpret it by connectives of classical logic. With classical logic, we
can deduce
$C$

$m$

A $(m\supset B)\supset B$

but we can also deduce$m$

A $(m\supset B)\supset m$ A $(m\supset B)$ A $B$

which implies that the original message and process $m\supset B$ may still remain after
message reception!
means that we have both a process
Let us try to interpret other connectives.
at the same time, i.e., we have two concurrent processes andand a process$m$$A\otimes B$

$A$

$B$

$A$

givesa connection based on proof search paradigm. Regarding the alternative
approach, proof reduction paradigm, please refer to other literatures.

$\overline{3\mathrm{T}\mathrm{h}\mathrm{i}\mathrm{s}\mathrm{m}\mathrm{a}\mathrm{t}\mathrm{e}\mathrm{r}\mathrm{i}\mathrm{a}\mathrm{J}}$116. Therefore,

a concurrent composition. If is a message, we can alsointerpret
as a process which throws a message and behaves like $B$ .
, but
and
means that we have any one of, we can obtain a process ,not both at the same time. So, if there is a message, we can, we can obtain . But even if we have bothandand if there is):(compare withandonly obtain either of
$B$

$A$

$\otimes \mathrm{r}\mathrm{e}\mathrm{p}\mathrm{r}\mathrm{e}\mathrm{S}\mathrm{e}\mathrm{n}\mathrm{t}_{\mathrm{S}}$$A$$A\otimes B$$(m_{1}-\mathrm{o}A_{1})\ (m_{2}-\mathrm{o}A_{2})$$m_{1}-\mathrm{o}A_{1}$$m_{2}-\mathrm{o}A_{2}$$A_{1}$$m_{1}$$A_{2}$$m_{2}$$m_{1}$$m_{2}$$(m_{1}-\mathrm{o}A_{1})\otimes(m_{2}-\mathrm{o}A_{2})$$A_{2}$$A_{1}$$m_{1}\otimes((m_{1}-\mathrm{o}A_{1})\ (m_{2}-\mathrm{o}A_{2}))\otimes C-arrow A_{1}\otimes C$$m_{2}\otimes((m_{1}-\mathrm{o}A_{1})\ (m_{2}-\mathrm{o}A_{2}))\otimes C-\mathrm{o}A_{2}\otimes C$

Therefore, $(m_{1}-\mathrm{o}A1)\ (m2-\mathrm{o}A_{2})$ can be interpreted as a process which waits for any, and becomesordepending on the received message.
one ofand
Let us consider predicate logic. An atomic formula $m(a)$ can be interpreted as amessage carrying a value . A predicate $m$ can now be considered a communication
channel, or a port name. Then, what does $\forall x.(m(x)-\mathrm{o}A(x))$ mean? It implies thatfor any , if $m(x)$ holds, we can deduce $A(x)$ . Computationally, it can be interpreted
as “for any , if there is a message $m$ carrying , we obtain a process $A(x).$ ” Therefore,$\forall x.(m(x)-\mathrm{o}A(x))$ represents a process which receives a value of
via a message $m$ ,and becomes $A(x)$ :$A_{1}$$m_{2}$$m_{1}$$A_{2}$

$a$

$x$

$x$

$x$

$x$

$m(a)\otimes\forall x.(m(x)-\mathrm{o}A(x))\otimes C-\infty A(a)\otimes C$

hides from externals. Therefore, can
How about existential quantification?
be used as a private name, which is used for identifying a message receiver.
There are several minor variants for expressing communication. For example, if
we allow a formula of the form: $\forall x.(m(a,x)-\mathrm{o}A(x))$ , it receives only a message $m$
whose first argument matches to , hence we can realize Linda-like generative communication. $\forall x.(m(x, X)-\mathrm{o}A(x))$ receives only a message $m$ whose first and second
arguments match. A formula $\forall x.\forall y.(m(x)\otimes n(y)-\mathrm{o}A(x, y))$ receives a value via$m$ , andvia , and behaves like $A(x, y)$ . Since the formula is equivalent to$\exists x.A$

$x$

$x$

$a$

$x$

$y$

$n$

$\forall x.(m(X)-0\forall y.(n(y)-\mathrm{o}A(x,y)))\equiv\forall y.(n(y)-0\forall x.(m(X)-\mathrm{o}A(x, y)))$,it can receives a message $m(a)$ and $n(b)$ in any order. Whether to delay the message
reception until both $m(a)$ and $n(b)$ are ready or not is up to the choice of language
designer.
Figure 3 summarizes the connection between linear logic formula and process.
Some of concurrent linear logic programming languages, including ACL and HigherOrder ACL, are formalized using dual connectives. We show this dual representationin the second column (In the second column, positive and negative atoms are also
exchanged).

A.3

Higher-Order ACL

with -abstraction.
is based on Girard’s second-order linear
Higher-Order
Note that with higher-order linear logic, a predicate can take predicates as arguments,
hence we can express processes which take processes as arguments. Quantifications$\mathrm{A}\mathrm{C}\mathrm{L}[5]$$\mathrm{l}\mathrm{o}\mathrm{g}\mathrm{i}\mathrm{c}[1]$$\lambda$

117

Linear Logic Formula Dual Representation Process Interpretation

Figure 3: Connection between formula and process
can be also over predicates, hence processes can communicate processes and communication channels via a message.
type system. Note that types
Higher-Order ACL is equipped with an
in Higher-Order ACL have nothing to do with Curry-Howard isomorphism, because
we regard formulas as processes, not as types. Higher-Order ACL took the similar
in introducing types. We have a special type ’ for propositions.
approach tois aComputationally, it corresponds to the type of processes and messages.
type of predicate on integers. Computatinally, it is a type of processes or messages
is a type of processes or
which take an integer as an argument.
messages which take a process or a message that takes an integer as an argument.
$(intarrow \mathit{0})arrow int$ is a type of functions which take a process that takes an integer as
an argument, and returns an integer. Processes can be defined and used polymorphiel in e2 end statement, which is analogous fun
cally, by using let proc
. Process definitions could be expressed by a formula $!(p(X)-\mathrm{o}e1)$ , (orstatement in$!(p(x)0-e1)$ by the dual encoding), which corresponds to clause in traditional logic
in $e2$ end
programming. However, we prefered to interpret it as let-style polymorphic typewhere fix is a fixpoint operator, for the introduction ofsystem. It makes sense, because unlike traditional logic programming, we can restrict
so that each predicate has only one definition clause.
$\mathrm{M}\mathrm{L}- \mathrm{S}\mathrm{t}\mathrm{y}\mathrm{i}_{\mathrm{e}}$$‘ \mathit{0}$$\lambda \mathrm{p}\mathrm{r}\mathrm{o}\log$$intarrow \mathit{0}$$(intarrow \mathit{0})arrow \mathit{0}$$\mathrm{p}(\mathrm{x})=$$\mathrm{M}\mathrm{L}$$p=\mathrm{f}\mathrm{i}\mathrm{x}(\lambda p.\lambda X.e1)$$\mathrm{M}\mathrm{L}$