Introduction
A reversible system is capable of executing both in the forward (normal) direction
and in the backward one. In a sequential setting, executing backwards is quite
straightforward since there exists only one execution order. In a concurrent
system, things are more complex as there exist no clear notion of last action: indeed,
several independent processes may execute concurrently. Causally-consistent
reversibility [
7
] relates causality and reversibility of a concurrent system in the
following way: an action can be reverted provided all its consequences have been
reverted.
In Milner's CCS, there exists just one notion of causality: the so-called
structural which is imposed by the pre xing `.' operator and by synchronizations.
An evidence of this is that the two reversible variants of CCS, RCCS [
4
] and
CCSK [
9
] are shown to be equivalent [
8
]. When moving to more expressive
calculi with name creation and passing like -calculus things are more complex,
since there exist di erent notions of causality as witnessed by the plethora of
causal semantics for -calculus [
2, 5, 1
] (just to cite a few of them). In -calculus,
structural causality is determined by the nesting of the pre xes; for example, in
process ba:ce the output on channel c structurally depends on the output on b.
Extruding (or opening) a name generates an object dependency; for example, in
process a (ba j a(z)) the input action on a depends on the output on b. Sending
a bound name to the context will make all the successive actions using that
name dependent on the extruder. There exist di erent interpretations on how
the rst extrusion of a name causes the processes using it. In this short note we
will consider the causal semantics introduced by Boreale and Sangiorgi [
1
], by
Degano and Priami [
5
] and by Cristescu, Krivine and Varacca [
2
]; and we will
discuss on how these notions generate di erent interpretations of backward moves
especially when considering silent actions. Our goal is to devise a reversible
calculus parametric with respect the underlying causal semantics, in order to better
compare them.
2
Causal semantics by example
Processes in -calculus are derived from the following syntax:
P; Q ::= 0 j :P j P j Q j a(P )
::= bc j b(a) j
A process can be inactive 0, a pre xed process :P , the parallel composition
P j Q and the restriction of a name a(P ) meaning that the channel name a is
only known in process P . A pre x denotes the output, input and the silent
action, respectively. The semantics of -calculus is expressed via an LTS and the
generated actions/labels are ::= bc j b(a) j bh ai j , where bh ai represents
sending of a bound name a. Let us consider the process P = a (ba j ca j a(z)),
where the actions are executed in following order: P b!a c!a a( !) P 0 and stands
for either y or z depending on whether the considered semantics is a late ( = z)
or an early ( = y) one. We now show how the di erent causal semantics behave.
Boreale et al. Causal information is added to the syntax and semantics of
calculus in order to track down subject dependencies. Causal processes are of
the form K :: P , where the cause-set K contains all the causes of the process P .
Every visible action is associated with a unique cause k. The actions are not
observable and do not exhibit causes. The set of the previous causes is noted by
K and in our example it is ;. Object dependencies can be observed in the labels
of the transitions, by looking at the process trace/run. In our example:
P b;h;ka1!i k1 :: 0 j ca j a(z) ;c;ka!2 k1 :: 0 j k2 :: 0 j a(z) a;;(ky!3) k1 :: 0 j k2 :: 0 j k3 :: 0
According to [
1
], the extrusion (the rst action) causes every following action
in which a is a free name. This implies that both of the actions ca and a(y) are
caused by bh ai. Hence bh ai cannot be undone unless ca and a(y) are undone.
To be able to capture this behaviour we need to be sure that action bh ai is the
last one to be undone, the other two can be undone in any order.
Degano et al. The authors keep track of the structural dependence by specifying
which component of the process is performing a move. To uniquely identify the
actions, they use labels of the form # and #hk0 #0 0; k1 #1 1i where # 2 fk0; k1
g represents the position of the (sub-)process making the action, and 0 = b(x)
i 1 is either ba or bh ai, or vice versa. The tag k0 (k1) is used to record that the
left (right) component in the process is moving. The object (link) dependency
can be observed by looking at the process run. In our example:
P k0k0bh a!i 0 j ca j a(z) k0k1c!a 0 j 0 j a(z) k1a(z!) 0 j 0 j 0
The extrusion bh ai causes every following action that has the name a in the
subject position. In this way, the input a(z) is caused by the rst action. The
output ca is neither object dependent on the extrusion, nor concurrent with it.
To order these kind of actions, the authors introduced the notion of temporal
precedence (structural and object). In this way, action bh ai has object
precedence over action ca even if they are not causally dependent. From the reversible
point of view this notion of causality is similar to [
1
].
Cristescu et al. A compositional semantics for the reversible -calculus is
introduced in [
2
]. The information about the past actions are kept into a memory
added to every process. A term of the form m . P represents the reversible
process, where memory m is a stack of events and P is process. A memory1 event
hi; k; i contains the identi er i, the contextual cause k and executed action ,
respectively. If the action does not have a cause, it is noted with . The indexed
restriction a behaves as the classical restriction when = ;, otherwise it is
used to keep track of the past scope of the variable. The process that we get
from P after the execution of the rst two actions is:
ai;h(hi; ; bai . 0 j hh; ; cai . 0 j a(z))
The outputs ba and ca are associated with the identi ers i and h, respectively.
Since these two actions were sending the bound name a to the context, their
identi ers are recorded into the process ai;h. According to the semantics, these
two actions are meant to be executed concurrently and both of them can be seen
as the extrusion of the name a. Hence, the input action a(z) can choose its cause
between i and h, according to the context. For example, by choosing h, we will
get the process:
ai;h(hi; ; bai . 0 j hh; ; cai . 0 j hl; h; a[ =z]i . 0)
Since in the memory hl; h; a[ =z]i, h is saved as a cause of the action l, that
force us to undo the action a(z) before the extrusion ca. The other extrusion
(ba) can be reversed at any time.
2.1
Causalities and silent actions
The semantics introduced in [
1, 5
] lose information about object dependence
when it comes to consider silent actions. Let us consider the process P =
a (ba j ca j a(z)) with a context b(x):xy j c(w) and see what happens.
Boreale et al. By adding a context to the example, all the executed actions will
become silent. Since after a synchronization the causes of the two synchronizing
processes are merged, and no new causes are created, in order to keep track of
them we need to give to processes initial and unique causes. We have:
a (k1 :: ba j k2 :: ca j k3 :: a(z)) j k4 :: b(x):xy j k5 :: c(w) !
a (fk1; k4g :: 0 j k2 :: ca j k3 :: a(z) j fk1; k4g :: ay) j k5 :: c(w) !
a (fk1; k4g :: 0 j fk2; k5g :: 0 j k3 :: a(z) j fk1; k4g :: ay j fk2; k5g :: 0) !
a (fk1; k4g :: 0 j fk2; k5g :: 0 j fk3; k1; k4g :: 0 j fk1; k4; k3g :: 0 j fk2; k5g :: 0))
1 For the sake of simplicity we are simplifying the information contained into the
memory m. We refer to [
2
] for more details on memories.
We can notice that the (silent) actions are no longer object-dependent (as the
example of the previous section). The third action is structurally dependent
on the rst one and we can detect it in the set of the causes fk1; k4; k3g. If
instead of imposing unique causes ki to the initial processes, we were to use ;
(as prescribed by the silent actions) we were unable to observe this fact. In [
6
],
authors proved that the causal information used to support reversibility in is
consistent with this notion of causality, if a reduction semantics is considered.
Degano et al. The object dependence after the communication is not needed
because through the rule Close the object is localised to the rest of the
communicating processes via a. Hence these three silent actions are not object
dependent. The computation with a context will look like:
From the structural point of view the third action is depending on the rst one
and we can notice it in the labels. Output k1k0 ay has a pre x in the rst label.
Cristescu et al. After the two synchronizations on the channel b and c, we will
get the process:
a;( ah( ai;h(hi; ; bai . 0 j hh; ; cai . 0 j a(z)) j hi; ; b[a=x]i . xy) j hh; ; c[a=w]i . 0)
According to the authors, processes a(z) and hi; ; b[a=x]i.xy can communicate2
only if the instantiator of the action xy is equal to the cause of the action a(z).
Since action i instantiates the name x with the name a, the cause of the input
action on the channel a is k = i. Considering the silent actions, the causal order
does not change, as one property of their causal semantics is that object causality
correspond to the subject one.
2.2
Silently regaining information
From these examples we can notice the change in the dependences between the
visible actions and the silent ones. When considering just actions in [
1, 5
],
there is no object dependency among actions; they are considered as concurrent
events. Moreover, information on extruders is lost. To be able to use these causal
semantics for a reversible calculus we need to keep track of which process did
the extrusion and to record where the binder was before. Moreover, also silent
actions have to bring the same causal information as their visible counterpart.
But when considering these modi ed semantics we will have that in the
structurally equivalent processes, the same actions have di erent causal order. If we
consider our example we will have that Q = a (ba j ca j a(z)) j b(x):xy j c(w),
Q0 = a( (ba j ca j a(z)) j b(x):xy j c(w)) with Q Q0 , we will have that if
Q b !c executes the synchronization on b and then on c these two silent actions
!
will be object dependent, while in Q0 !b !c the two actions are concurrent. This
2 Memory m is used as a variables store, hence variable x is evaluated into a.
is not the case of [
2
] since this semantics enjoys some correctness criteria [
3
] (one
of which is that causality is preserved via structural congruence) that the other
two semantics do not.
3
Conclusions and future work
We reviewed three notions of causality for -calculus, two non reversible [
1, 5
]
and one reversible [
2
], and we showed the di erences among them. From the
reversible perspective we pointed out the di culties while using semantics [
1,
5
] and proposed a reinterpretation of them in particular when it comes to
consider silent actions. More in details, information about the extruder have to be
maintained, in order to bring back the binder while reverting a bound action. It
seems that di erent data structures can be used to maintain such information;
indeed, [
2
] uses a set while in [
1, 5
] since the rst extruder causes the other an
indexed set should be the ideal data structure. Di erent data structures will induce
a di erent notion of causality. Currently we are working on developing a general
framework for reversible -calculi parametric with respect to the data structure
used to save extruders information. Then, depending on the underlying data
structure used to instantiate the framework, we could obtain di erent causal
semantics. In this way, once we are able to capture the two known reversible
variants of -calculus [
6, 2
], it will be simpler to compare them.