数理解析研究所講究録
918 巻 1995 年 292-298

292

Concurrent Reflective Computations
in Rewriting Logic
Hiroshi lshikawa

Kokichi Futatsugi{ -ishika, kokichi,$\mathrm{h}$$\mathrm{t}\mathrm{a}\mathrm{k}\mathrm{u}\mathrm{o}$}Takuo Watanabe$\copyright \mathrm{i}^{\mathrm{a}\mathrm{i}\mathrm{a}}\mathrm{S}\mathrm{t}.\mathrm{C}$. jp

School of Information Science,
Japan Advanced lnstitute of Science and Technology \dag er(JAIST)
July 26, 1995

Abstract
Rewriting logic can represent dynamic behaviors of concurrent
reactive systems declaratively.
Declarative descriptions in rewriting logic are expected to be amenable to analysis of interesting properties. The group-wide architecture based on the actor model is a specific concurrent reflective computation
model based on “group-wide reflection”. It has a potential of modeling cooperative behaviors of several
software modules (or agents). This paper provides some basic considerations on methods of modeling thegroup-wide architecture in rewriting logic.
$\mathrm{a}\mathrm{n}\mathrm{d}/\mathrm{o}\mathrm{r}$1Introduction

The concurrent reflective computation model is recognized to be a useful framework forconstructing reliable and easy-to-maintain concurrent system.
That framework can basically be constructed in two ways. One is called Individual. Each object in the system has its own metaobject which
Based Architecture
governs its computation. Reflective
is realized by sending message
to metaobjects. The computational activity in an object is sequential. This implies eachmetaobject model only the local sequential aspects of an object. Therefore, IndividualBased Reflection is not sufficiently powerful to deal with the global information of a groupof objects.
The other is called Group-Wide Architecture. It is a specific concurrent
reflective computation model based on Group-Wide Reflection. It has a potential ofmodeling cooperative behaviors of several software modules (or agents). Our group-widearchitecture is based on the Actor model. All reflective operations are performed solely via$(\mathrm{I}\mathrm{B}\mathrm{A})[11]$$\mathrm{c}\mathrm{o}\mathrm{m}\mathrm{p}\mathrm{u}\mathrm{t}\mathrm{a}\mathrm{t}\mathrm{i}_{0}\mathrm{n}[5,10,13]$$(\mathrm{G}\mathrm{W}\mathrm{A})[12]$$\uparrow 15$

Asahidai, Tatsunokuchi, Ishikawa 923-12, Japan.

293

message sends, which are interpreted at the metalevel concurrently with interpretationsof actors in the baselevel.
can represent dynamic behaviors of concurrent
Rewritingreactive systems declaratively. Declarative descriptions in rewriting logic are expected to beamenable to analysis of interesting properties.
In this paper, we propose some basic considerations on methods of modeling the groupwide reflection in rewriting logic, and implement. We use a functional programming,
language Gofer, which is a sublanguage of functional programming language
to describe our model and perform an example of inter-group migration of object.
$\mathrm{l}\mathrm{o}\mathrm{g}\mathrm{i}\mathrm{c}[4,6,7]$$\mathrm{a}\mathrm{n}\mathrm{d}/\mathrm{o}\mathrm{r}$$\mathrm{i}\mathrm{t}[2,3]$$\mathrm{H}\mathrm{a}\mathrm{s}\mathrm{k}\mathrm{e}\mathrm{l}\mathrm{l}[8]$1.1Reflection

A system is said to be causally connected to its
if the internal structures
and the domain they represent are linked in such a way that if one of then changes, thisleads to a corresponding effect upon the other.
A reflective system is a system which incorporates structures representing (aspects of)itself. We call the sum of these structures the self-representation of the system. This
self-representation makes it possible for the system to answer questions about itself andsupport actions on itself. Because the self-representation is causally-connected to the
aspects of the system it represents, we can say that:$\mathrm{d}_{0}\mathrm{m}\mathrm{a}\mathrm{i}\mathrm{n}\mathrm{s}(\mathrm{F}\mathrm{i}\mathrm{g}.1(\mathrm{a}))$(i) The system always has an accurate representation of itself.
(ii) The status and computation of the system are always in compliance with this representation. This means that a reflective system can actually bringtoitself by virtue of its own computation.

.ns$\mathrm{m}\mathrm{o}\mathrm{d}\mathrm{i}\mathrm{f}\mathrm{i}_{\mathrm{C}}\mathrm{a}\mathrm{t}\mathrm{i}_{0}$Figure 1: The notion of reflective system

294

When we implement a reflective system like Fig.1 (a), the idea of proceduralis useful to do so.
proposed by$\mathrm{r}\mathrm{e}\mathrm{f}\mathrm{l}\mathrm{e}\mathrm{C}\mathrm{t}\mathrm{i}_{0}\mathrm{n}(\mathrm{F}\mathrm{i}\mathrm{g}.1(\mathrm{b}))$$\mathrm{B}.\mathrm{S}\mathrm{m}\mathrm{i}\mathrm{t}\mathrm{h}[9]$Group-Wide Architecture

1.2

In this architecture, a group of metalevel objects constructs the metalevel. The behaviorof an object is not managed by metaobjects; rather, the collective behavior of a group of
objects is represented as the coordinated actions of a group of metalevel objects, whichconstruct meta-group. As mentioned above, the Group-Wide Architecture we make useof in this study is based on the Actor model. Each object and a group of objects are
regarded as Actors. Of course, metalevel objects and a group of metalevel objects arealso regarded as Actors.

The Actor model

1.3

is one of the concurrent computation models. In the Actor model,
The Actora system consists of a set of autonomous computation agent called Actors; each Actor
represents a physical or conceptual entity in the system’s problem domain.
The features of the Actor model are as follows.
$\mathrm{m}\mathrm{o}\mathrm{d}\mathrm{e}\mathrm{l}[1]$Message passing: Actors can send messages to their acquaintance asynchronously.
Dynamic topology: A communication topology can be changed by sending an Actor’s
address with a message.
Concurrency: Any two Actors may run simultaneously.

Let be a system composed by actors. A configuration represents a computational
state of at a certain frame of reference. This is represented by a pair which is composed
and the other is a finite set of tasks inby two sets. One is a finite set of actors in. Computation in is modeled as transitions between configurations in the set of all
configurations of .
Now we construct a causally connected metalevel representation for an actor system
be a metalevel representation for . It is constructed as another actor system. Let
is an actor system which represents thewhich implements the transition system of .
is also used as a meta-circularconcurrent computational aspects of . In our model,
is automaticallyinterpreter for . Therefore, the causal-connection between
guaranteed.
is also an actor system, then a special configuIn this way, it becomes clear thatmeta-configuration.
calledaisration of
$C$

$S$

$S$

$S$

$S$

$S$

$S$

$S$

$S$

$\uparrow S$$S$$\uparrow S$$S$$\uparrow S$$S$$S\mathrm{a}\mathrm{n}\mathrm{d}\uparrow S$$\uparrow S$$\uparrow S$

Rewriting logic

1.4First, we introduce the definition of rewriting logic [4, 6, 7].
Definition 1 A (labelled) rewriting theory 71 is a 4-tuple $\mathcal{R}=(\Sigma, E, L, R)$ whereis a set of -equations, is a set of labels,
is a ranked alphabet of function symbols,
and is a set of pairs $R\subset L\cross(T_{\Sigma,E}(X)^{2}$ whose first component is a label and whose
second component is a pair of -equivalence classes of times, with X $=\{x_{1}, \cdots, x_{n}, \cdots\}$ acountably infinite set of variables. Elements of are called rewrite rules. We understand$\Sigma$$E$$\Sigma$

$R$

$E$

$R$

$L$

295

a rule $(r, ([t], [t’]))$ as a labelled sequent and use for it the notation$r$:$[t]arrow[t’]$.

is the set of variable occurring in either or , we write$[t(X_{1},\cdots,Xn)]arrow[t’(X_{1},\cdots,x_{n})]$ , or in abbreviated notation::$[t’]$ and write
Given a rewrite theory , we say that 7? entails a sequent$R\vdash[t]arrow[t’]$ if and only if $[t]arrow[t’]$ can be obtained by finite application of thefollowing rules of deduction:
To indicate that$\{x_{1}, \cdots, x_{n}\}$

$t$

$r$

$r$

$[t(\overline{x^{n}})]arrow[t’(\overline{xn})]\cdot\blacksquare$$[t]$$\mathcal{R}$$t’$$arrow$l.Reflexivity. For each $[t]\in T_{\Sigma,E}(X)$ ,$\overline{[t]arrow[t]}$2.

$\mathrm{c}\mathrm{o}\mathrm{n}\mathrm{g}\Gamma \mathrm{u}\mathrm{e}\mathrm{n}\mathrm{c}\mathrm{e}$. For each$f\in\Sigma_{n},$$n\in \mathrm{N}$

,

,

.

$, \frac{[t1].arrow[t_{1}’]\cdots[tn]arrow.[t_{n}]}{[f(t_{1,n}t)]arrow[f(t_{1}/,\cdot\cdot,t_{n}\prime)]}$$.$3.

. For each rewrite rule :$\mathrm{R}\mathrm{e}\mathrm{p}\mathrm{l}\mathrm{a}\mathrm{c}\mathrm{e}\mathrm{m}\mathrm{e}\mathrm{n}\mathrm{t}$

in

$R$

,

$r$

$[t(x_{1}, \cdots, x_{n})]arrow[t’(X_{1}, \cdots, Xn)]$,$\frac{[w_{1}]arrow[w_{1}’]\cdots[wn]arrow[w_{n}’]}{[t(\overline{w}/\overline{x})]arrow[t(w/\overline{X})]}$

4. Transitivity.

$\frac{[t_{1}]arrow[h][h]arrow[t_{3}]}{[t_{1}]arrow[t_{3}]}$$\blacksquare$

Rewriting logic is understood as a method of correct reasoning about some class ofentities. For rewriting logic, the entities above are concurrent systems having states, andevolving by means of $trans\dot{i}tions$ . Therefore, we can describe concurrent object-oriented
models with rewriting logic. In this logic, concurrent object-oriented computation isformalized as concurrent ACI-rewriting. The Actor model is a special case of those models.

2

Group-Wide Architecture in Rewriting Logic

In [12], both baselevel and metalevel of the group-wide architecture are composed by aneach group of actors. In order to describe them in rewriting logic, we define them, namely
actors(objects), messages, and rewrite rules as terms. After that, we compose the Term
Rewriting System and some functions to construct a causally connected between baseleveland metalevel.
Because of using in rewriting logic to describe our system, terms and rewriting correspond to states and transition of the computational system, respectively. In our groupwide architecture, the state of the system consists of finite set of messages and finite setof objects. In addition, the transition of the system means a change of the states. In
rewriting logic, we can represent terms as the states and a pair of terms as a change ofthe states. Furthermore a simple example, modeling migration of objects, is executed on
our system.

296

2.1

System Design

In the first place, we define some terms and termschemas (using for definition of rewrite
rules) as follows:data Namedata Term$=$

StringName
Val NameInt
App Term Term$=\mathrm{V}\mathrm{a}\mathrm{r}$

$\}$

1
$|$

1

$–\mathrm{v}\mathrm{a}\mathrm{r}\mathrm{i}\mathrm{a}\mathrm{b}\mathrm{l}\mathrm{e}$–valuenumberfunction application
list
pair
–

$\mathrm{C}\mathrm{o}\mathrm{n}$–[Terml$\mathrm{L}\mathrm{i}\mathrm{s}$–1par Term Term
data$\mathrm{T}\mathrm{e}\mathrm{r}\mathrm{m}\mathrm{s}_{\mathrm{C}\mathrm{h}\mathrm{e}\mathrm{m}}\mathrm{a}=$

1
$|$

1
$|$

1

–

SVar Name
SVal Name
SCon Int
SApp
SLis [TermSchema]
SPar

–

–

–

–

$\mathrm{T}\mathrm{e}\mathrm{r}\mathrm{m}\mathrm{s}_{\mathrm{C}\mathrm{h}\mathrm{e}\mathrm{m}}\mathrm{a}\mathrm{T}\mathrm{e}\mathrm{r}\mathrm{m}\mathrm{s}_{\mathrm{C}\mathrm{h}\mathrm{e}\mathrm{m}}\mathrm{a}$––$\mathrm{T}\mathrm{e}\mathrm{r}\mathrm{m}\mathrm{s}_{\mathrm{C}\mathrm{h}\mathrm{e}\mathrm{m}}\mathrm{a}\mathrm{T}\mathrm{e}\mathrm{r}\mathrm{m}\mathrm{s}_{\mathrm{C}\mathrm{h}\mathrm{e}\mathrm{m}}\mathrm{a}$variablevalue
numberfunctionlist$\mathrm{a}\mathrm{p}\mathrm{p}\mathrm{l}\mathrm{i}_{\mathrm{C}\mathrm{a}}\mathrm{t}\mathrm{i}\mathrm{o}\mathrm{n}$pair

In the second place, we define actor(object), message, configuration, and rewrite rule
as follows:
actor(object)
Lis [. . .1 ,Lis [Val–$\uparrow’ 0\mathrm{i}\mathrm{d}^{1\uparrow},$–messageLis [(Par Val’${}^{\mathrm{t}}\mathrm{M}\mathrm{i}\mathrm{d}^{1}$’Val

configurationPar
bjectsrewrite rule

. . .]$||\mathrm{D}\mathrm{e}\mathrm{s}^{11}$

) ,

..

.]

–

$1\mathrm{i}\mathrm{s}\mathrm{t}-_{\mathrm{o}\mathrm{f}}$$1\mathrm{i}\mathrm{s}\mathrm{t}-_{\mathrm{o}\mathrm{f}}$-mesages–$(\mathrm{l}\mathrm{h}\mathrm{s},\mathrm{r}\mathrm{h}\mathrm{S})$where lhs
rhs

$–$

$–$

SPar
SPar

$1\mathrm{i}\mathrm{s}\mathrm{t}^{-}\mathrm{o}\mathrm{f}^{-}1\mathrm{h}\mathrm{S}$-objects-objects$1\mathrm{i}\mathrm{s}\mathrm{t}-_{\mathrm{O}}\mathrm{f}-_{\mathrm{r}}\mathrm{h}\mathrm{S}$-messages-messages$1\mathrm{i}\mathrm{s}\mathrm{t}-\mathrm{o}\mathrm{f}-_{1\mathrm{h}}\mathrm{S}$$1\mathrm{i}\mathrm{s}\mathrm{t}-_{\mathrm{o}\mathrm{f}\mathrm{h}\mathrm{S}}-_{\mathrm{r}}$Finally, we define some functions which can translate data and rewrite rules in baselevel
into data in metalevel and those inverse one.
–from base to meta$\mathrm{m}\mathrm{a}\mathrm{k}\mathrm{e}_{-^{\mathrm{m}\mathrm{e}}}\mathrm{t}\mathrm{a}_{-\mathrm{o}\mathrm{n}}\mathrm{C}\mathrm{f}$::[$(\mathrm{T}\mathrm{e}\mathrm{r}\mathrm{m}\mathrm{S}\mathrm{c}\mathrm{h}\mathrm{e}\mathrm{m}\mathrm{a},$from meta to basebaserule : : Term $->$ [baseconf : : Term $->$ Term

TermSchema)]$->$

Term $->$ Term–$(\mathrm{T}\mathrm{e}\mathrm{r}\mathrm{m}\mathrm{S}\mathrm{c}\mathrm{h}\mathrm{e}\mathrm{m}\mathrm{a},$TermSchema)]

Function make-meta- conf needs two arguments-list of rewrite rules and configurationof baselevel–and translates them into data of metalevel. Function baserule needs one
argument–metalevel representation of rewrite rules of baselevel–and translates it into
rewrite rules used in baselevel. In same way, function baseconf needs one argumentmetalevel representation of configuration of baselevel-and translates it into configuration
representing baselevel.

2.2

An Example

Migration of an object from node (a group of metaobjects) to node is described as an
example of group-wide reflection. A node is constructed some metalevel objects, such as297

External Mailer, Task Handler, Database, Evaluator, and Migrator. Migrator is a special
object that has a method of doing migration.
When Evaluator accepts the message with the requirement to migrate an object
to another node
in nodeand rules of migration, it starts to interpret the rules,
already-known
data and rewritten terms. The migration rules are as follows.
referring$A_{1}$$N_{1}$$\bullet$$N_{2}$

Obtain the Migrator of the.
destination$N_{2}$$\bullet$Ask for the address of thedatabase of destination .
$N_{2}$$\bullet$Get the immigrant’s new
address in the destination.
$N_{2}$$\bullet$3

Perform Migration.

Figure 2: Migration for object

Discussion

Constructing the example in a way mentioned above, we faced the following problems:$\bullet$When we describe a mechanism for inter-group migration of objects, we must consider the direct sum of baselevel and metalevel of those groups. In our case, there
are two groups
and. Then there will be a possibility of conflict of rewrite
rules, that is, a rewrite rule application to a configuration can not be decided.
$N_{1}$$\bullet$$N_{2}$

Whether do the direct sum of the metalevel bothsum of their baselevel or not.

$N_{1}$

and$N_{2}$

represent the direct

We will be able to clear the former in the following way. When we define the rewrite
rules of such groups, we do the rules without same identifiers beforehand.
The latter one is as follows. In [12], it is proved
correctly represents interms of transition relations, where andmean a group of actors and the group whichforms a metalevel representation of respectively. In our case, we will be able to prove
such a property in the same way.
$\mathrm{t}\mathrm{h}\mathrm{a}\mathrm{t}\uparrow S$

$S$

$S$

$\uparrow S$$S$

4Conclusion and Future WorkWe described group-wide reflection based on actor model in rewriting logic. By constructing direct sum of configurations and rewriting rules in two groups, we were able to describe
a mechanism for inter-group migration of objects. We can expect that we describe it morethan three groups in the same way.
The research reported in this paper is their first attempt of formalizing group-widereflective architecture in rewriting logic. This research would become important.
Our group-wide architecture is based on the Actor model. After this we will describe
some other examples for GWA. Based on this work, we expect that it will be possible

298

to construct a new general reflective architecture based on the rewriting logic in future.
Moreover we expect that it will be possible to design and implement metalevel architectureof concurrent reflective computations more sutable to Rewriting Logic. The architecture
would be more effective in analyzing the properties of the concurrent reflective computation from several as pects.

References[1] Gul Agha. Actors : A Model of Concurrent Computation in Distributed Systems. The MIT
Press, 1987.

[2] Hiroshi Ishikawa, Kokichi Futatsugi, and Takuo Watanabe. Concurrent Reflective Computations in Rewriting Logic (in Japanese). In 11th Conference Proceedings Japan Society
for Soflware Science and Technology, pp. 313-316. Japan Society for Software Science andTechnology(JSSST), 1994.
[3] Hiroshi Ishikawa. Concurrent Reflective Computations in Rewriting Logic (in Japanese).
Master Thesis, Japan Advanced Institute of Science and Technology, February 1995.

[4] Jos\’e Meseguer, Kokichi Futatsugi, and Timothy Winkler. Using Rewriting Logic to Specify,
Program, Integrate, and Reuse Open Concurrent Systems of Cooperating Agents. Technical
Report SRI-CSL-92-11, Computer Science Laboratory, SRI International, 1992.
[5] Pattie Maes. Computational reflection. Ph. D. Thesis 87-2, Artificial Intelligence Laboratory,
Vrije Universiteit Brussel, 1987.
[6] Jos\’e Meseguer. Conditional rewriting logic as a unified model of concurrency. Technical
Report SRI-CSL-92-08, Computer Science Laboratory, SRI International, 1992.

[7] Jos\’e Meseguer. A logical theory of concurrent objects and its realization in the maudelanguage. In Peter Wegner Gul Agha and Akinori Yonezawa, editors, Research Directions
in Concurrent Object Oriented Programming. The MIT Press, 1993.

[8] Paul Hudack, Philip Wadler, et al. Report on the programming language Haskell, a nonstrict purely functional language (Version 1.2). Technical report, Yale
University, 1992.

$\mathrm{U}\mathrm{n}\mathrm{i}_{\mathrm{V}\mathrm{e}\mathrm{r}\mathrm{s}}\mathrm{i}\mathrm{t}\mathrm{y}/\mathrm{G}\mathrm{l}\mathrm{a}\mathrm{s}\mathrm{g}\mathrm{o}\mathrm{w}$[9] Brian Cantwell Smith. Reflection and Semantics in a Procedural Language(ph D.Thesis).
Technical Report TR-272, Laboratory for Computer Science, MIT, 1982.
[10] Brian Cantwell Smith. Reflection and Semantics in Lisp. In Proceedings of the A CM
Symposium on Principles of Programming Languages (POPL), pp. 23-35, 1984.
[11] Takuo Watanabe, Akinori Yonezawa. Reflection in an Object-Oriented Concurrent Language. In ABCL:An Object-Oriented Concurrent System, pp. 45-70. The MIT Press, 1990.
[12] Takuo Watanabe, Akinori Yonezawa. An Actor-Based Metalevel Architecture for GroupWide Reflection. In Proceedings of REX $School/Worksh_{\mathit{0}}p$ on Foundations of ObjectOriented Languages $(REx/FOOL)$ , Lecture Notes in Computer Science 489, pp. 405-425,
New York, 1991. Springer-Verlag.
[13] Takuo Watanabe. A Tutorial Introduction to Computational Reflection (in Japanese).
Computer Software, 11 (3):5-14, May 1994.