arXiv:cs/0504050v2 [cs.LO] 15 Jan 2006

Under consideration for publication in Theory and Practice of Logic Programming

1

Mapping Fusion and Synchronized Hyperedge
Replacement into Logic Programming∗
IVAN LANESE and UGO MONTANARI
Dipartimento di Informatica, Università di Pisa
Largo Bruno Pontecorvo,3 56127 Pisa, Italia
(e-mail: {lanese,ugo}@di.unipi.it)
submitted 27 December 2003; revised 14 April 2005; accepted 5 January 2006

Abstract
In this paper we compare three different formalisms that can be used in the area of models
for distributed, concurrent and mobile systems. In particular we analyze the relationships
between a process calculus, the Fusion Calculus, graph transformations in the Synchronized Hyperedge Replacement with Hoare synchronization (HSHR) approach and logic
programming. We present a translation from Fusion Calculus into HSHR (whereas Fusion
Calculus uses Milner synchronization) and prove a correspondence between the reduction
semantics of Fusion Calculus and HSHR transitions. We also present a mapping from
HSHR into a transactional version of logic programming and prove that there is a full
correspondence between the two formalisms. The resulting mapping from Fusion Calculus
to logic programming is interesting since it shows the tight analogies between the two
formalisms, in particular for handling name generation and mobility. The intermediate
step in terms of HSHR is convenient since graph transformations allow for multiple, remote synchronizations, as required by Fusion Calculus semantics. To appear in Theory
and Practice of Logic Programming (TPLP).
KEYWORDS: Fusion Calculus, graph transformation, Synchronized Hyperedge Replacement, logic programming, mobility

1 Introduction
In this paper we compare different formalisms that can be used to specify and
model systems which are distributed, concurrent and mobile, as those that are usually found in the global computing area.
Global computing is becoming very important because of the great development
of networks which are deployed on huge areas, first of all Internet, but also other
kinds of networks such as networks for wireless communications. In order to build
and program these networks one needs to deal with issues such as reconfigurability,
synchronization and transactions at a suitable level of abstraction. Thus powerful
∗ Work supported in part by the European IST-FET Global Computing project IST-2001-33100
PROFUNDIS and the European IST-FET Global Computing 2 project IST-2005-16004 Sensoria.

2

Ivan Lanese and Ugo Montanari

formal models and tools are needed. Until now no model has been able to emerge
as the standard one for this kind of systems, but there are a lot of approaches with
different merits and drawbacks.
An important approach is based on process calculi, like Milner’s CCS and Hoare’s
CSP. These two calculi deal with communication and synchronization in a simple
way, but they lack the concept of mobility. An important successor of CCS, the πcalculus (Milner et al. 1992), allows to study a wide range of mobility problems in
a simple mathematical framework. We are mainly interested in the Fusion Calculus
(Parrow and Victor 1998; Victor 1998; Gardner and Wischik 2000; Gardner and
Wischik 2004), which is an evolution of π-calculus. The interesting aspect of this
calculus is that it has been obtained by simplifying and making more symmetric
the π-calculus.
One of the known limitations of process-calculi when applied to distributed systems is that they lack an intuitive representation because they are equipped with an
interleaving semantics and they use the same constructions for representing both
the agents and their configurations. An approach that solves this kind of problems is
based on graph transformations (Ehrig et al. 1999). In this case the structure of the
system is explicitly represented by a graph which offers both a clean mathematical
semantics and a suggestive representation. In particular we represent computational
entities such as processes or hosts with hyperedges (namely edges attached to any
number of nodes) and channels between them with shared nodes. As far as the
dynamic aspect is concerned, we use Synchronized Hyperedge Replacement with
Hoare synchronization (HSHR) (Degano and Montanari 1987). This approach uses
productions to specify the behaviour of single hyperedges, which are synchronized
by exposing actions on nodes. Actions exposed by different hyperedges on the same
node must be compatible. In the case of Hoare synchronization all the edges must
expose the same action (in the CSP style). This approach has the advantage, w.r.t.
other graphical frameworks such as Double Pushout (Ehrig et al. 1973) or Bigraphs
(Jensen and Milner 2003), of allowing a distributed implementation since productions have a local effect and synchronization can be performed using a distributed
algorithm.
We use the extension of HSHR with mobility (Hirsch et al. 2000; Hirsch and Montanari 2001; König and Montanari 2001; Ferrari et al. 2001; Lanese 2002), that
allows edges to expose node references together with actions, and nodes whose references are matched during synchronization are unified.
For us HSHR is a good step in the direction of logic programming (Lloyd 1993).
We consider logic programming as a formalism for modelling concurrent and distributed systems. This is a non-standard view of logic programming (see Bruni et al.
2001 for a presentation of our approach) which considers goals as processes whose
evolution is defined by Horn clauses and whose interactions use variables as channels
and are managed by the unification engine. In this framework we are not interested

Mapping Fusion and SHR into Logic Programming

3

only in refutations, but in any partial computation that rewrites a goal into another.
In this paper we analyze the relationships between these three formalisms and we
find tight analogies among them, like the same parallel composition operator and
the use of unification for name mobility. However we also emphasize the differences
between these models:
• the Fusion Calculus is interleaving and relies on Milner synchronization (in
the CCS style);
• HSHR is inherently concurrent since many actions can be performed at the
same time on different nodes and uses Hoare synchronization;
• logic programming is concurrent, has a wide spectrum of possible controls
which are based on the Hoare synchronization model, and also is equipped
with a more complex data management.
We will show a mapping from Fusion Calculus to HSHR and prove a correspondence
theorem. Note that HSHR is a good intermediate step between Fusion Calculus and
logic programming since in HSHR hyperedges can perform multiple actions at each
step, and this allows to build chains of synchronizations. This additional power is
needed to model Milner synchronization, which requires synchronous, atomic routing capabilities. To simplify our treatment we consider only reduction semantics.
The interleaving behaviour is imposed with an external condition on the allowed
HSHR transitions.
Finally we present the connections between HSHR and logic programming. Since
the logic programming paradigm allows for many computational strategies and is
equipped with powerful data structures, we need to constrain it in order to have
a close correspondence with HSHR. We define to this end Synchronized Logic Programming (SLP), which is a transactional version of logic programming. The idea
is that function symbols are pending constraints that must be satisfied before a
transaction can commit, as for zero tokens in zero-safe nets (Bruni and Montanari
2000). In the mapping from HSHR to SLP edges are translated into predicates,
nodes into variables and parallel composition into AND composition.
This translation was already presented in the MSc. thesis of the first author
(Lanese 2002) and in Lanese and Montanari (2002). Fusion Calculus was mapped
into SHR with Milner synchronization (a simpler task) in Lanese and Montanari
(2004a) where Fusion LTS was considered instead of Fusion reduction semantics.
The paper Lanese and Montanari (2002) also contains a mapping of Ambient calculus into HSHR. This result can be combined with the one here, thus obtaining
a mapping of Ambient calculus into SLP. An extensive treatment of all the topics
in this paper can also be found in the forthcoming Ph.D. thesis of the first author
(Lanese 2006).
Since logic programming is not only a theoretical framework, but also a well developed programming style, the connections between Fusion, HSHR and logic pro-

4

Ivan Lanese and Ugo Montanari

gramming can be used for implementation purposes. SLP has been implemented
in Lanese (2002) through meta-interpretation. Thus we can use translations from
Fusion and HSHR to implement them. In particular, since implementations of logic
programming are not distributed, this can be useful mainly for simulation purposes.
In Section 2 we present the required background, in particular we introduce the
Fusion Calculus (2.1), the algebraic representation of graphs and the HSHR (2.2),
and logic programming (2.3). Section 3 is dedicated to the mapping from Fusion
Calculus to HSHR. Section 4 analyzes the relationships between HSHR and logic
programming, in particular we introduce SLP (4.1), we prove the correspondence
between it and HSHR (4.2) and we give some hints on how to implement Fusion
Calculus and HSHR using Prolog (4.3). In Section 5 we present some conclusions
and traces for future work. Finally, proofs and technical lemmas are in Appendix A.
2 Background
Mathematical notation. We use T σ to denote the application of substitution σ to T
(where T can be a term or a set/vector of terms). We write substitutions as sets of pairs
of the form t/x, denoting that variable x is replaced by term t. We also denote with σ1 σ2
the composition of substitutions σ1 and σ2 . We denote with σ −1 (x) the set of elements
mapped to x by σ. We use | − | to denote the operation that computes the number of
elements in a set/vector. Given a function f we denote with dom(f ) its domain, with Im(f )
its image and with f |S the restriction of f to the new domain S. We use on functions and
substitutions set theoretic operations (such as ∪) referring to their representation as sets
of pairs. Similarly, we apply them to vectors, referring to the set of the elements in the
vector. In particular, \ is set difference. Given a set S we denote with S ∗ the set of strings
on S. Also, given a vector ~v and an integer i, ~v [i] is the i-th element of ~v . Finally, a vector
is given by listing its elements inside angle brackets h−i.

2.1 The Fusion Calculus
The Fusion Calculus (Parrow and Victor 1998; Victor 1998) is a calculus for modelling distributed and mobile systems which is based on the concepts of fusion and
scope. It is an evolution of the π-calculus (Milner et al. 1992) and the interesting
point is that it is obtained by simplifying the calculus. In fact the two action prefixes for input and output communication are symmetric, whereas in the π-calculus
they are not, and there is just one binding operator called scope, whereas the πcalculus has two (restriction and input). As shown in Parrow and Victor (1998),
the π-calculus is syntactically a subcalculus of the Fusion Calculus (the key point
is that the input of π-calculus is obtained using input and scope). In order to have
these properties fusion actions have to be introduced. An asynchronous version of
Fusion Calculus is described in Gardner and Wischik (2000), Gardner and Wischik
(2004), where name fusions are handled explicitly as messages. Here we follow the
approach by Parrow and Victor.

Mapping Fusion and SHR into Logic Programming

5

We now present in details the syntax and the reduction semantics of Fusion Calculus. In our work we deal with a subcalculus of the Fusion Calculus, which has no
match and no mismatch operators, and has only guarded summation and recursion.
All these restrictions are quite standard, apart from the one concerning the match
operator, which is needed to have an expansion lemma. To extend our approach to
deal with match we would need to extend SHR by allowing production applications
to be tagged with a unique identifier. We leave this extension for future work. In
our discussion we distinguish between sequential processes (which have a guarded
summation as topmost operator) and general processes.
We assume to have an infinite set N of names ranged over by u, v, . . . , z and an
infinite set of agent variables (disjoint w.r.t. the set of names) with meta-variable
X. Names represent communication channels. We use φ to denote an equivalence
relation on N , called fusion, which is represented in the syntax by a finite set of
equalities. Function n(φ) returns all names which are fused, i.e. those contained in
an equivalence class of φ which is not a singleton.
Definition 1
The prefixes are defined by:
α : : = u~x

(Input)

u~x

(Output)

φ

(Fusion)

Definition 2
The agents are defined by:
S::=
P ::=

P

i

αi .Pi

(Guarded sum)

0

(Inaction)

S

(Sequential Agent)

P1 |P2

(Composition)

(x)P

(Scope)

rec X.P
X

(Recursion)
(Agent variable)

The scope restriction operator is a binder for names, thus x is bound in (x)P .
Similarly rec is a binder for agent variables. We will only consider agents which are
closed w.r.t. both names and agent variables and where in rec X.P each occurrence
of X in P is within a sequential agent (guarded recursion). We use recursion to define infinite processes instead of other operators (e.g. replication) since it simplifies
the mapping and since their expressive power is essentially the same. We use infix
+ for binary sum (which thus is associative and commutative).
Given an agent P , functions fn, bn and n compute the sets fn(P ), bn(P ) and

6

Ivan Lanese and Ugo Montanari

n(P ) of its free, bound and all names respectively.
Processes are agents considered up to structural axioms defined as follows.
Definition 3 (Structural congruence)
The structural congruence ≡ between agents is the least congruence satisfying the
α-conversion law (both for names and for agent variables), the abelian monoid laws
for composition (associativity, commutativity and 0 as identity), the scope laws
(x)0 ≡ 0, (x)(y)P ≡ (y)(x)P , the scope extrusion law P |(z)Q ≡ (z)(P |Q) where
z∈
/ fn(P ) and the recursion law rec X.P ≡ P {rec X.P/X}.
Note that fn is also well-defined on processes.
In order to deal with fusions we need the following definition.
Definition 4 (Substitutive effect )
A substitutive effect of a fusion φ is any idempotent substitution σ : N → N having
φ as its kernel. In other words xσ = yσ iff xφy and σ sends all members of each
equivalence class of φ to one representative in the class1 .
The reduction semantics for Fusion Calculus is the least relation satisfying the
following rules.
Definition 5 (Reduction semantics for Fusion Calculus)
(~z)(R|(· · · + u~x.P )|(u~y .Q + . . . )) → (~z)(R|P |Q)σ
where |~x| = |~y | and σ is a substitutive effect of {~x = ~y } such that dom(σ) ⊆ ~z.
(~z)(R|(· · · + φ.P )) → (~z)(R|P )σ
where σ is a substitutive effect of φ such that dom(σ) ⊆ ~z.
P ≡ P ′ , P ′ → Q′ , Q′ ≡ Q
P →Q
2.2 Synchronized Hyperedge Replacement
Synchronized Hyperedge Replacement (SHR) (Degano and Montanari 1987) is an
approach to (hyper)graph transformations that defines global transitions using local
productions. Productions define how a single (hyper)edge can be rewritten and the
conditions that this rewriting imposes on adjacent nodes. Thus the global transition
is obtained by applying in parallel different productions whose conditions are compatible. What exactly compatible means depends on which synchronization model
we use. In this work we will use the Hoare synchronization model (HSHR), which
requires that all the edges connected to a node expose the same action on it. For a
general definition of synchronization models see Lanese and Montanari (2004b).
We use the extension of HSHR with mobility (Hirsch et al. 2000; Hirsch and Montanari 2001; König and Montanari 2001; Ferrari et al. 2001; Lanese 2002), that
1

Essentially σ is a most general unifier of φ, when it is considered as a set of equations.

Mapping Fusion and SHR into Logic Programming

7

allows edges to expose node references together with actions, and nodes whose references are matched during synchronization are unified.
We will give a formal description of HSHR as labelled transition system, but first
of all we need an algebraic representation for graphs.
An edge is an atomic item with a label and with as many ordered tentacles as
the rank rank(L) of its label L. A set of nodes, together with a set of such edges,
forms a graph if each edge is connected, by its tentacles, to its attachment nodes.
We will consider graphs up to isomorphisms that preserve2 nodes, labels of edges,
and connections between edges and nodes.
Now, we present a definition of graphs as syntactic judgements, where nodes correspond to names and edges to basic terms of the form L(x1 , . . . , xn ), where the xi
are arbitrary names and rank(L) = n. Also, nil represents the empty graph and |
is the parallel composition of graphs (merging nodes with the same name).
Definition 6 (Graphs as syntactic judgements)
Let N be a fixed infinite set of names and LE a ranked alphabet of labels. A
syntactic judgement (or simply a judgement) is of the form Γ ⊢ G where:
1. Γ ⊆ N is the (finite) set of nodes in the graph.
2. G is a term generated by the grammar
G : : = L(~x) | G1 |G2 | nil
where ~x is a vector of names and L is an edge label with rank(L) = |~x|.
We denote with n the function that given a graph G returns the set n(G) of all the
names in G. We use the notation Γ, x to denote the set obtained by adding x to Γ,
assuming x ∈
/ Γ. Similarly, we write Γ1 , Γ2 to state that the resulting set of names
is the disjoint union of Γ1 and Γ2 .
Definition 7 (Structural congruence and well-formed judgements)
The structural congruence ≡ on terms G obeys the following axioms:
(AG1) (G1 |G2 )|G3 ≡ G1 |(G2 |G3 )
(AG2) G1 |G2 ≡ G2 |G1
(AG3) G|nil ≡ G
The well-formed judgements Γ ⊢ G over LE and N are those where n(G) ⊆ Γ.
Axioms (AG1),(AG2) and (AG3) define respectively the associativity, commutativity and identity over nil for operation |.
Well-formed judgements up to structural axioms are isomorphic to graphs up to
isomorphisms. For a formal statement of the correspondence see Hirsch (2003).
We will now present the steps of a SHR computation.
2

In our approach nodes usually represent free names, and they are preserved by isomorphisms.

8

Ivan Lanese and Ugo Montanari

Definition 8 (SHR transition)
Let Act be a set of actions. For each action a ∈ Act, let ar(a) be its arity.
A SHR transition is of the form:
Λ,π

Γ ⊢ G −−→ Φ ⊢ G′
where Γ ⊢ G and Φ ⊢ G′ are well-formed judgements for graphs, Λ : Γ → (Act×N ∗ )
is a total function and π : Γ → Γ is an idempotent substitution. Function Λ assigns
to each node x the action a and the vector ~y of node references exposed on x by the
transition. If Λ(x) = (a, ~y ) then we define actΛ (x) = a and nΛ (x) = ~y . We require
that ar(actΛ (x)) = | nΛ (x)|, namely the arity of the action must equal the length of
the vector.
We define:
• n(Λ) = {z|∃x.z ∈ nΛ (x)}
set of exposed names;
• ΓΛ = n(Λ) \ Γ
set of fresh names that are exposed;
• n(π) = {x|∃x′ 6= x.xπ = x′ π}
set of fused names.
Substitution π allows to merge nodes. Since π is idempotent, it maps every node into
a standard representative of its equivalence class. We require that ∀x ∈ n(Λ).xπ =
x, i.e. only references to representatives can be exposed. Furthermore we require
Φ ⊇ Γπ ∪ ΓΛ , namely nodes are never erased. Nodes in ΓInt = Φ \ (Γπ ∪ ΓΛ ) are
fresh internal nodes, silently created in the transition. We require that no isolate,
internal nodes are created, namely ΓInt ⊆ n(G′ ).
Note that the set of names Φ of the resulting graph is fully determined by Γ, Λ,
π and G′ thus we will have no need to write its definition explicitly in the inference
rules. Notice also that we can write a SHR transition as:
Λ,π

Γ ⊢ G −−→ Γπ, ΓΛ , ΓInt ⊢ G′ .
We usually assume to have an action ǫ ∈ Act of arity 0 to denote “no synchronization”. We may not write explicitly π if it is the identity, and some actions if
they are (ǫ, hi). Furthermore we use Λǫ to denote the function that assigns (ǫ, hi)
to each node in Γ (note that the dependence on Γ is implicit).
We derive SHR transitions from basic productions using a set of inference rules.
Productions define the behaviour of single edges.
Definition 9 (Production)
A production is a SHR transition of the form:
Λ,π

x1 , . . . , xn ⊢ L(x1 , . . . , xn ) −−→ Φ ⊢ G
where all xi , i = 1 . . . n are distinct.
Productions are considered as schemas and so they are α-convertible w.r.t. names
in {x1 , . . . , xn } ∪ Φ.

Mapping Fusion and SHR into Logic Programming

9

We will now present the set of inference rules for Hoare synchronization. The
intuitive idea of Hoare synchronization is that all the edges connected to a node
must expose the same action on that node.
Definition 10 (Rules for Hoare synchronization)
Λ,π

(par)

Γ ⊢ G1 −−→ Φ ⊢ G2

(Γ ∪ Φ) ∩ (Γ′ ∪ Φ′ ) = ∅

Λ∪Λ′ ,π∪π ′

Γ, Γ′ ⊢ G1 |G′1 −−−−−−−→ Φ, Φ′ ⊢ G2 |G′2
Λ,π

(merge)

Λ′ ,π ′

Γ′ ⊢ G′1 −−−→ Φ′ ⊢ G′2

Γ ⊢ G1 −−→ Φ ⊢ G2

∀x, y ∈ Γ.xσ = yσ ∧ x 6= y ⇒ actΛ (x) = actΛ (y)
Λ′ ,π ′

Γσ ⊢ G1 σ −−−→ Φ′ ⊢ G2 σρ
where σ : Γ → Γ is an idempotent substitution and:
(i). ρ = mgu({(nΛ (x))σ = (nΛ (y))σ|xσ = yσ} ∪ {xσ = yσ|xπ = yπ}) where ρ
maps names to representatives in Γσ whenever possible
(ii). ∀z ∈ Γ.Λ′ (zσ) = (Λ(z))σρ
(iii). π ′ = ρ|Γσ

Λǫ ,id

(idle) Γ ⊢ G −−−→ Γ ⊢ G
Λ,π

(new)

Γ ⊢ G1 −−→ Φ ⊢ G2

x∈
/ Γ ~y ∩ (Γ ∪ Φ ∪ {x}) = ∅
Λ∪{(x,a,~
y)},π

Γ, x ⊢ G1 −−−−−−−−−→ Φ′ ⊢ G2
A transition is obtained by composing productions, which are first applied on
disconnected edges, and then by connecting the edges by merging nodes. In particular rule (par) deals with the composition of transitions which have disjoint sets
of nodes and rule (merge) allows to merge nodes (note that σ is a projection into
representatives of equivalence classes). The side condition requires that we have the
same action on merged nodes. Definition (i) introduces the most general unifier ρ
of the union of two sets of equations: the first set identifies (the representatives of)
the tuples associated to nodes merged by σ, while the second set of equations is
just the kernel of π. Thus ρ is the merge resulting from both π and σ. Note that
(ii) Λ is updated with these merges and that (iii) π ′ is ρ restricted to the nodes
of the graph which is the source of the transition. Rule (idle) guarantees that each
edge can always make an explicit idle step. Rule (new) allows adding to the source
graph an isolated node where arbitrary actions (with fresh names) are exposed.
Λ,π

Λ,π

We write P (Γ ⊢ G −−→ Φ ⊢ G′ ) if Γ ⊢ G −−→ Φ ⊢ G′ can be obtained from
the productions in P using Hoare inference rules.
We will now present an example of HSHR computation.

10

Ivan Lanese and Ugo Montanari
Fig. 1. Star graph
x

S
v

y

w
S

S

S
z

Fig. 2. Productions
ε,<>
y

y

r,<w>
y

y

C

C

C

S

w

z

x

x
ε,<>

C

x
r,<w>

x

Example 1 (Hirsch et al. 2000 )
We show now how to use HSHR to derive a 4 elements ring starting from a one
element ring, and how we can then specify a reconfiguration that transforms the
ring into the star graph in Figure 1.
We use the following productions:
(x,ǫ,hi),(y,ǫ,hi)

x, y ⊢ C(x, y) −−−−−−−−−→ x, y, z ⊢ C(x, z)|C(z, y)
(x,r,hwi),(y,r,hwi)

x, y ⊢ C(x, y) −−−−−−−−−−−−→ x, y, w ⊢ S(y, w)
that are graphically represented in Figure 2. Notice that Λ is represented by decorating every node x in the left hand with actΛ (x) and nΛ (x). The first rule allows
to create rings, in fact we can create all rings with computations like:
x ⊢ C(x, x) → x, y ⊢ C(x, y)|C(y, x) →
→ x, y, z ⊢ C(x, y)|C(y, z)|C(z, x) →
→ x, y, z, v ⊢ C(x, y)|C(y, z)|C(z, v)|C(v, x)
In order to perform the reconfiguration into a star we need rules with nontrivial
actions, like the second one. This allows to do:
(x,r,hwi),(y,r,hwi),(z,r,hwi),(v,r,hwi)

x, y, z, v ⊢ C(x, y)|C(y, z)|C(z, v)|C(v, x) −−−−−−−−−−−−−−−−−−−−−−−−→
→ x, y, z, v, w ⊢ S(x, w)|S(y, w)|S(z, w)|S(v, w)
Note that if an edge C is rewritten into an edge S, then all the edges in the ring
must use the same production, since they must synchronize via action r. They must
agree also on nΛ (x) for every x, thus all the newly created nodes are merged. The
whole transition is represented in Figure 3.

11

Mapping Fusion and SHR into Logic Programming
Fig. 3. Ring creation and reconfiguration to star
x

x

x

x
C

C

S

C
v

x

C

C

C

C

y
C

C

S

C
S

y
z

y

w
S

y

v

z
z

It is easy to show that if we can derive a transition T , then we can also derive
every transition obtainable from T by applying an injective renaming.
Lemma 1
Let P be a set of productions and σ an injective substitution.
Λ,π
P (Γ ⊢ G −−→ Φ ⊢ G′ ) iff:
Λ′ ,π ′

P (Γσ ⊢ Gσ −−−→ Φσ ⊢ G′ σ)
where Λ′ (xσ) = (Λ(x))σ and xσπ ′ = xπσ.
Proof
By rule induction.
2.3 Logic programming
In this paper we are not interested in logic computations as refutations of goals for
problem solving or artificial intelligence, but we consider logic programming (Lloyd
1993) as a goal rewriting mechanism. We can consider logic subgoals as concurrent
communicating processes that evolve according to the rules defined by the clauses
and that use unification as the fundamental interaction primitive. A presentation
of this kind of use of logic programming can be found in Bruni et al. (2001).
In order to stress the similarities between logic programming and process calculi
we present a semantics of logic programming based on a labelled transition system.
Definition 11
We have for clauses (C) and goals (G) the following grammar:
C ::=A ← G
G : : = G, G | A | 
where A is a logic atom, “,” is the AND conjunction and  is the empty goal.
We can assume “,” to be associative and commutative and with unit .
The informal semantics of A ← B1 , . . . , Bn is “for every assignment of the variables, if B1 , . . . , Bn are all true, then A is true”.
A logic program is a set of clauses. Derivations in logic programming are called
SLD-derivations (from “Linear resolution for Definite clauses with Selection function”). We will also consider partial SLD-derivations.

12

Ivan Lanese and Ugo Montanari

Definition 12 (Partial SLD-derivation)
Let P be a logic program.
We define a step of a SLD-resolution computation using the following rules:
H ← B1 , . . . , B k ∈ P

θ = mgu({A = Hρ})

atomic goal
P A−
→ (B1 , . . . , Bk )ρθ
where ρ is an injective renaming of variables such that all the variables in the clause
variant (H ← B1 , . . . , Bk )ρ are fresh.
θ

P
P

θ

G−
→F
θ

G, G′ −
→ F, G′ θ

conjunctive goal

We will omit P if P is clear from the context.
A partial SLD-derivation of P ∪ {G} is a sequence (possibly empty) of steps of
SLD-resolution allowed by program P with initial goal G.

3 Mapping Fusion Calculus into Synchronized Hyperedge Replacement
In this section we present a mapping from Fusion Calculus to HSHR.
This mapping is quite complex since there are many differences between the two
formalisms. First of all we need to bridge the gap between a process calculus and a
graph transformation formalism, and this is done by associating edges to sequential processes and by connecting them according to the structure of the system.
Moreover we need to map Milner synchronization, which is used in Fusion Calculus, into Hoare synchronization. In order to do this we define some connection
structures that we call amoeboids which implement Milner synchronization using
Hoare connectors. Since Hoare synchronization involves all the edges attached to a
node while Milner one involves just pairs of connectors, we use amoeboids to force
each node to be shared by exactly two edges (one if the node is an interface to the
outside) since in that case the behaviour of Hoare and Milner synchronization is
similar. An amoeboid is essentially a router (with no path-selection abilities) that
connects an action with the corresponding coaction. This is possible since in HSHR
an edge can do many synchronizations on different nodes at the same time. Finally,
some restrictions have to be imposed on HSHR in order to have an interleaving
behaviour as required by Fusion Calculus.
We define the translation on processes in the form (~x)P where P is the parallel
composition of sequential processes. Notice that every process can be reduced to
the above form by applying the structural axioms: recursive definitions which are
not inside a sequential agent have to be unfolded once and scope operators which
are not inside a sequential agent must be taken to the outside. We define the translation also in the case (~x)P is not closed w.r.t. names (but it must be closed w.r.t.
process variables) since this case is needed for defining productions.
In the form (~x)P we assume that the ordering of names in (~x) is fixed, dictated

Mapping Fusion and SHR into Logic Programming

13

by some structural condition on their occurrences in P .
For our purposes, it is also convenient to express process P in (~x)P as P = P ′ σ,
where P ′ is a linear agent, i.e. every name in it appears once. We assume that
the free names of P ′ are fresh, namely fn(P ′ ) ∩ fn(P ) = ∅, and again structurally
ordered. The corresponding vector is called fnarray(P ′ ).
The decomposition P = P ′ σ highlights the role of amoeboids. In fact, in the
translation, substitution σ is made concrete by a graph consisting of amoeboids,
which implement a router for every name in fn(P ). More precisely, we assume the
existence of edge labels mi and n of ranks i = 2, 3, . . . and 1 respectively. Edges
labelled by mi implement routers among i nodes, while n edges “close” restricted
names ~x in (~x)P ′ σ.
Finally, linear sequential processes S in P ′ must also be given a standard form.
In fact, they will be modelled in the HSHR translation by edges labelled by LS ,
namely by a label encapsulating S itself. However in the derivatives of a recursive
process the same sequential process can appear with different names an unbound
number of times. To make the number of labels (and also of productions, as we will
see in short) finite, for every given process, we choose standard names x1 , . . . , xn
and order them structurally:
S = Ŝ(x1 , . . . , xn )ρS with S1 = S2 ρ implying Ŝ1 = Ŝ2 and ρS1 = ρρS2 .
We can now define the translation from Fusion Calculus to HSHR. The translation is parametrized by the nodes in the vectors ~v and w
~ we choose to represent
the names in ~x and fnarray(P ′ ). We denote with x∈S Gx the parallel composition
of graphs Gx for each x ∈ S.
Definition 13 (Translation from Fusion Calculus to HSHR)

J(~x)P ′ σK~v ,w~ = Γ ⊢ JP ′ K{w/
~ fnarray(P ′ )}|JσK{~v /~x}{w/
~ fnarray(P ′ )}| x∈~v n(x)
where:
|~v | = |~x|,
|w|
~ = | fnarray(P ′ )|,
~v ∩ w
~ =∅
and with:
Γ = fn((~x)P ′ σ), ~v , w.
~
J0K = nil
JSK = LŜ (x1 , . . . , xn )ρS with n = | fn(Ŝ)|
JP1 |P2 K = JP1 K|JP2 K

JσK = x∈Im(σ) mk+1 (x, σ −1 (x)) where k = |σ −1 (x)|.
In the above translation, graph JP ′ K consists of a set of disconnected edges, one
for each sequential process of (~x)P ′ σ. The translation produces a graph with three
kinds of nodes. The nodes of the first kind are those in w.
~ Each of them is adjacent
to exactly two edges, one representing a sequential process of P ′ , and the other an
amoeboid. Also the nodes in ~v are adjacent to two edges, an amoeboid and an n

14

Ivan Lanese and Ugo Montanari
Fig. 4. Amoeboids for σ
r

y

m2

w

m3

z

x

edge. Finally the nodes in fn((~x)P ′ σ) are adjacent only to an amoeboid.
As mentioned above, translation JσK builds an amoeboid for every free name x
of P ′ σ: it has k + 1 tentacles, where k are the occurrences of x in P ′ σ, namely the
free names of P ′ mapped to it. Notice that the choice of the order within σ −1 (x) is
immaterial, since we will see that amoeboids are commutative w.r.t. their tentacles.
However, to make the translation deterministic, σ −1 (x) could be ordered according
to some fixed precedence of the names.
Example 2 (Translation of a substitution)
Let σ = {y/x, y/z, r/w}. The translation of σ is in Figure 4.
Example 3 (Translation of a process)
Let us consider the (closed) process (uz)uz.0| rec X.(x)ux.(ux.0|X). We can write
it in the form (~x)P as:
(uzy)uz.0|uy.(uy.0| rec X.(x)ux.(ux.0|X))
Furthermore we can decompose P into P ′ σ where:
P ′ = u1 z1 .0|u2 y1 .(u3 y2 .0| rec X.(x)u4 x.(u5 x.0|X))
σ = {u/u1, z/z1 , u/u2, y/y1 , u/u3 , y/y2 , u/u4 , u/u5}.
We can now perform the translation.
We choose ~v = (u, z, y) and w
~ = (u1 , z1 , u2 , y1 , u3 , y2 , u4 , u5 ):
J(~x)P ′ σK~v ,w~ = u, z, y, u1, z1 , u2 , y1 , u3 , y2 , u4 , u5 ⊢
Lx1 x2 .0 (u1 , z1 )|Lx1 x2 .(x3 x4 .0| rec X.(x)x5 x.(x6 x.0|X)) (u2 , y1 , u3 , y2 , u4 , u5 )|
m6 (u, u1 , u2 , u3 , u4 , u5 )|m2 (z, z1 )|m3 (y, y1 , y2 )|n(u)|n(z)|n(y)
Now we define the productions used in the HSHR system.
We have two kinds of productions: auxiliary productions that are applied to amoeboid edges and process productions that are applied to process edges.
Before showing process productions we need to present the translation from Fusion
Calculus prefixes into HSHR transition labels.
Definition 14
The translation from Fusion Calculus prefixes into HSHR transition labels is the
following:
JαK = (Λ, π) where
if α = u~x then Λ(u) = (inn , ~x), Λ(x) = (ǫ, hi) if x 6= u with n = |~x|, π = id
if α = u~x then Λ(u) = (outn , ~x), Λ(x) = (ǫ, hi) if x 6= u and n = |~x|, π = id

15

Mapping Fusion and SHR into Logic Programming
if α = φ then Λ = Λǫ and π is any substitutive effect of φ.
We will write Ju~xK and Ju~xK as (u, inn , ~x) and (u, outn , ~x) respectively.

Definition 15 (Process productions)
We have a process production for each prefix at the top level of a linear standard
P
sequential process (which has {x1 , . . . , xn } as free names). Let i αi .Pi be such a
process. Its productions can be derived with the following inference rule:
JPj ξK~v ,w~ = Γ ⊢ G

Jαj K = (Λ, π)
Jαj K

x1 , . . . , xn ⊢ LP i αi .Pi (x1 , . . . , xn ) −−−→ Γ, Γ′ ⊢ G|JξK|JπK|



x∈Γ′′

n(x)

if ~v ∪ w,
~ {x1 , . . . , xn } and fn(Pj )ξ are pairwise disjoint with ξ injective renaming
from fn(Pj ) to fresh names, Γ′ = x1 , . . . , xn and Γ′′ = Γ′ \ (n(Λ) ∪ n(π) ∪ fn(Pj )).
We add some explanations on the derivable productions. Essentially, if αj .Pj is
a possible choice, the edge labelled by the process can have a transition labelled
by Jαj K to something related to JPj K~v ,w~ . We use Pj ξ instead of Pj (and then we
add the translation of ξ) to preserve the parity of the number of amoeboid edges
on each path (see Definition 17). The parameter ~v of the translation contains fresh
nodes for restricted names that are taken to the top level during the normalization
of Pj while w
~ contains the free names in the normalization of Pj (note that some of
them may be duplicated w.r.t. Pj , if this one contains recursion). If αj is a fusion
φ, according to the semantics of the calculus, a substitutive effect π of it should
be applied to Pj , and this is obtained by adding the amoeboids JπK in parallel.
Furthermore, Γ ⊢ G must be enriched in other two ways: since nodes can never
be erased, nodes which are present in the sequential process, i.e. the nodes in Γ′ ,
must be added to Γ. Also “close” n edges must be associated to forgotten nodes
(to forbid further transitions on them and to have them connected to exactly two
edges in the result of the transition), provided they are not exposed, i.e. to nodes
in Γ′′ .
Note that when translating the RHS (~x)P σ of productions we may have names
in P σ which occur just once. Since they are renamed by σ and ξ, they will produce
in the translation some chains of m2 connectors of even length, which, as we will see
shortly, are behaviourally equivalent to simple nodes. For simplicity, in the examples
we will use the equivalent productions where these connectors have been removed
and the nodes connected by them have been merged.
Example 4 (Translation of a production)
Let us consider firstly the simple agent x1 x2 .0.
The only production for this agent (where ~v = w
~ = hi) is:
(x1 ,out1 ,hx2 i)

x1 , x2 ⊢ Lx1 x2 .0 (x1 , x2 ) −−−−−−−−−→ x1 , x2 ⊢ n(x1 )
where we closed node x1 but not node x2 since the second one is exposed on x1 .
Let us consider a more complex example:
x1 x2 .(x3 x4 .0| rec X.(x)x5 x.(x6 x.0|X)).
The process x3 x4 .0| rec X.(x)x5 x.(x6 x.0|X)ξ where xi ξ = x′i can be transformed

16

Ivan Lanese and Ugo Montanari

into:
(y)y1 y2 .0|y3 y4 .(y5 y6 .0| rec X.((x)y7 x.(y8 x.0|X)))σ
where σ = {x′3 /y1 , x′4 /y2 , x′5 /y3 , y/y4 , x′6 /y5 , y/y6 , x′5 /y7 , x′6 /y8 }.
Its translation (with ~v = hyi and w
~ = hy1 , y2 , y3 , y4 , y5 , y6 , y7 , y8 i) is:
x′3 , x′4 , x′5 , x′6 , y1 , y2 , y3 , y4 , y5 , y6 , y7 , y8 , y ⊢
Lx1 x2 .0 (y1 , y2 )|Lx1 x2 .(x3 x4 .0| rec X.((x)x5 x.(x6 x.0|X))) (y3 , y4 , y5 , y6 , y7 , y8 )|
m2 (x′3 , y1 )|m2 (x′4 , y2 )|m3 (x′5 , y3 , y7 )|m3 (x′6 , y5 , y8 )|m3 (y, y4 , y6 )|n(y)
Thus the production is:
x1 , x2 , x3 , x4 , x5 , x6 ⊢ Lx1 x2 .(x3 x4 .0| rec X.(x)x5 x.(x6 x.0|X)) (x1 , x2 , x3 , x4 , x5 , x6 )
(x1 ,in1 ,hx2 i)

−−−−−−−−→
x1 , x2 , x3 , x4 , x5 , x6 , y3 , y4 , y5 , y6 , y7 , y8 , y, x′5 , x′6 ⊢
Lx1 x2 .0 (x3 , x4 )|Lx1 x2 .(x3 x4 .0| rec X.((x)x5 x.(x6 x.0|X))) (y3 , y4 , y5 , y6 , y7 , y8 )|
m3 (x′5 , y3 , y7 )|m3 (x′6 , y5 , y8 )|m3 (y, y4 , y6 )|n(y)|m2 (x5 , x′5 )|m2 (x6 , x′6 )|n(x1 )
where for simplicity we collapsed y1 with x3 and y2 with x4 .
We will now show the productions for amoeboids.
Definition 16 (Auxiliary productions)
We have auxiliary productions of the form:
(x1 ,inn ,~
y1 ),(x2 ,outn ,~
y2 )

Γ ⊢ mk (Γ) −−−−−−−−−−−−−−−→ Γ, ~y1 , ~y2 ⊢ mk (Γ)|



i=1...|~
y1 |

m2 (~y1 [i], ~y2 [i])

We need such a production for each k and n and each pair of nodes x1 and x2 in Γ
where Γ is a chosen tuple of distinct names with k components and ~y1 and ~y2 are
two vectors of fresh names such that |~y1 | = |~y2 | = n.
Note that we also have the analogous production where x1 and x2 are swapped. In
particular, the set of productions for a mk edge is invariant w.r.t. permutations of
the tentacles, modelling the fact that its tentacles are essentially unordered.
We have no productions for edges labelled with n, which thus forbid any synchronization.
The notion of amoeboid introduced previously is not sufficient for our purposes.
In fact, existing amoeboids can be connected using m2 edges and nodes that are no
more used can be closed using n edges. Thus we present a more general definition
of amoeboid for a set of nodes and we show that, in the situations of interest, these
amoeboids behave exactly as the simpler mi edges.
Definition 17 (Structured amoeboid )
Given a vector of nodes ~s, a structured amoeboid M (~s) for the set of nodes S
containing all the nodes in ~s is any connected graph composed by m and n edges
that satisfies the following properties:
• its set of nodes is of the form S ∪ I, with S ∩ I = ∅;
• nodes in S are connected to exactly one edge of the amoeboid;

Mapping Fusion and SHR into Logic Programming

17

• nodes in I are connected to exactly two edges of the amoeboid;
• the number of edges composing each path connecting two distinct nodes of S
is odd.
Nodes in S are called external, nodes in I are called internal. We consider equivalent all the amoeboids with the same set S of external nodes. The last condition
is required since each connector inverts the polarity of the synchronization, and we
want amoeboids to invert it.
Note that m|S| (~s) is an amoeboid for S.
Lemma 2
If M (~s) is a structured amoeboid for S, the transitions for M (~s) which are non idle
and expose non ǫ actions on at most two nodes x1 , x2 ∈ S are of the form:


Λ,id
S, I ⊢ M (~s) −−−→ S, I, I ′ , ~y1 , ~y2 ⊢ M (~s)| i=1...|~y1 | M (~y1 [i], ~y2 [i])| M̃ (∅)
where Λ(x1 ) = (inn , ~y1 ) and Λ(x2 ) = (outn , ~y2 ) (non trivial actions may be exposed
also on some internal nodes) and ~y1 and ~y2 are two vectors of fresh names such
that |~y1 | = |~y2 | = n. Here M̃ (∅) contains rings of m2 connectors connected only to
fresh nodes which thus are disconnected from the rest of the graph. We call them
pseudoamoeboids. Furthermore we have at least one transition of this kind for each
choice of x1 , x2 , ~y1 and ~y2 .

Proof
See Appendix A.
Thanks to the above result we will refer to structured amoeboids simply as amoeboids.
We can now present the results on the correctness and completeness of our translation.
Theorem 1 (Correctness)
For each closed fusion process P and each pair of vectors ~v and w
~ satisfying the
′
constraints of Definition 13, if P → P then there exist Λ, Γ and G such that
Λ,id
~′)
JP K~v ,w~ −−−→ Γ ⊢ G. Furthermore Γ ⊢ G is equal to JP ′ Kv~′ ,w~′ (for some v~′ and w
up to isolated nodes, up to injective renamings, up to equivalence of amoeboids
(Γ ⊢ G can have a structured amoeboid where JP ′ Kv~′ ,w~′ has a simple one) and up
to pseudoamoeboids.

Proof
The proof is by rule induction on the reduction semantics.
See Appendix A.

18

Ivan Lanese and Ugo Montanari

Theorem 2 (Completeness)
Λ,π

For each closed fusion process P and each pair of vectors ~v and w
~ if JP K~v ,w~ −−→ Γ ⊢
G with a HSHR transition that uses exactly two productions for communication
or one production for a fusion action (plus any number of auxiliary productions)
~ ′ ) up to isolate
then P → P ′ and Γ ⊢ G is equal to JP ′ Kv~′ ,w~′ (for some v~′ and w
nodes, up to injective renamings, up to equivalence of amoeboids (Γ ⊢ G can have a
structured amoeboid where JP ′ Kv~′ ,w~′ has a simple one) and up to pseudoamoeboids.

Proof
See Appendix A.
These two theorems prove that the allowed transitions in the HSHR setting correspond to reductions in the Fusion Calculus setting. Note that in HSHR we must
consider only transitions where we have either two productions for communication
or one production for a fusion action. This is necessary to model the interleaving
behaviour of Fusion Calculus within the HSHR formalism, which is concurrent. On
the contrary, one can consider the fusion equivalent of all the HSHR transitions:
these correspond to concurrent executions of many fusion reductions. One can give
a semantics for Fusion Calculus with that behaviour. Anyway in that case the notion of equivalence of amoeboids is no more valid, since different amoeboids allow
different degrees of concurrency. We thus need to constrain them. The simplest case
is to have only simple amoeboids, that is to have no concurrency inside a single
channel, but there is no way to force normalization of amoeboids to happen before
undesired transitions can occur. The opposite case (all the processes can interact
in pairs, also on the same channel) can be realized, but it requires more complex
auxiliary productions.
Note that the differences between the final graph of a transition and the translation of the final process of a Fusion Calculus reduction are not important, since
the two graphs have essentially the same behaviours (see Lemma 1 for the effect
of an injective renaming and Lemma 2 for the characterization of the behaviour of
a complex amoeboid; isolated nodes and pseudoamoeboids are not relevant since
different connected components evolve independently). Thus the previous results
can be extended from transitions to whole computations.
Note that in the HSHR model the behavioural part of the system is represented
by productions while the topological part is represented by graphs. Thus we have
a convenient separation between the two different aspects.
Example 5 (Translation of a transition)
We will now show an example of the translation. Let us consider the process:
(uxyzw)(Q(x, y, z)|uxy.R(u, x)|uzw.S(z, w))

19

Mapping Fusion and SHR into Logic Programming
Fig. 5. (uxyzw)(Q(x, y, z)|uxy.R(u, x)|uzw.S(z, w))

n

x

x1

m4

1

z1

LQ(x ,x ,x ) 3
1 2

m4

3

z

n

2

x3

x2
2

y1

5

Lx1x2x3.R(x4,x5)
1

y2

3

z2

m3

4

z3

y
u1

n

u2

m4

2

u3
1

Lx1x2x3.S(x 4,x 5)
3

u

n

4

5

w1

w2

m3

w

n

Note that it is already in the form (~x)P . It can do the following transition:
(uxyzw)(Q(x, y, z)|uxy.R(u, x)|uzw.S(z, w)) →
(uxy)(Q(x, y, z)|R(u, x)|S(z, w)){x/z, y/w}
We can write P in the form:
(Q(x1 , y1 , z1 )|u1 x2 y2 .R(u2 , x3 )|u3 z2 w1 .S(z3 , w2 ))σ
where:
σ = {x/x1 , y/y1 , z/z1, u/u1 , x/x2 , y/y2 , u/u2, x/x3 , u/u3 , z/z2, w/w1 , z/z3 , w/w2 }.
A translation of the starting process is:
u, x, y, w, z, x1 , y1 , z1 , u1 , x2 , y2 , u2 , x3 , u3 , z2 , w1 , z3 , w2 ⊢
LQ(x1 ,x2 ,x3 ) (x1 , y1 , z1 )|Lx1 x2 x3 .R(x4 ,x5 ) (u1 , x2 , y2 , u2 , x3 )|
Lx1 x2 x3 .S(x4 ,x5 ) (u3 , z2 , w1 , z3 , w2 )|m4 (u, u1 , u2 , u3 )|m4 (x, x1 , x2 , x3 )|
m3 (y, y1 , y2 )|m4 (z, z1 , z2 , z3 )|m3 (w, w1 , w2 )|n(u)|n(x)|n(y)|n(w)|n(z)
A graphical representation is in Figure 5.
We have the following process productions:
(y1 ,out2 ,hy2 ,y3 i)

y1 , y2 , y3 , y4 , y5 ⊢ Lx1 x2 x3 .R(x4 ,x5 ) (y1 , y2 , y3 , y4 , y5 ) −−−−−−−−−−−→
y1 , y2 , y3 , y4 , y5 ⊢ LR(x1 ,x2 ) (y4 , y5 )|n(y1 )
(y1 ,in2 ,hy2 ,y3 i)

y1 , y2 , y3 , y4 , y5 ⊢ Lx1 x2 x3 .S(x4 ,x5 ) (y1 , y2 , y3 , y4 , y5 ) −−−−−−−−−−→
y1 , y2 , y3 , y4 , y5 ⊢ LS(x1 ,x2 ) (y4 , y5 )|n(y1 )
In order to apply (suitable variants of) these two productions concurrently we have

20

Ivan Lanese and Ugo Montanari
Fig. 6. Graph with actions

n

x

x1

m4

1

z1

LQ(x ,x ,x ) 3
1 2

m4

3

z

n

2

x3

x2
2

y1

5

Lx1x2x3.R(x4,x5)
1

y2

3

z3

y

out2 x2 y2 u 1
out2 l 1 l2

n

u2

m4

2

u3
1

in2 l 3 l4
u
in2 z2 w1

n

z2

m3

4

Lx1x2x3.S(x 4,x 5)
3

4

5

w1

w2

m3

w

n

to synchronize their actions. This can be done since in the actual transition actions
are exposed on nodes u1 and u3 respectively, which are connected to the same m4
edge. Thus the synchronization can be performed (see Figure 6) and we obtain as
final graph:
u, x, y, w, z, x1 , y1 , z1 , u1 , x2 , y2 , u2 , x3 , u3 , z2 , w1 , z3 , w2 ⊢
LQ(x1 ,x2 ,x3 ) (x1 , y1 , z1 )|LR(x1 ,x2 ) (u2 , x3 )|n(u1 )|LS(x1 ,x2 ) (z3 , w2 )|n(u3 )|
m4 (u, u1 , u2 , u3 )|m4 (x, x1 , x2 , x3 )|m3 (y, y1 , y2 )|m4 (z, z1 , z2 , z3 )|m3 (w, w1 , w2 )|
m2 (x2 , z2 )|m2 (y2 , w1 )|n(u)|n(x)|n(y)|n(w)|n(z)
which is represented in Figure 7.
The amoeboids connect the following tuples of nodes:
(u, u1 , u2 , u3 ), (x, x1 , x2 , x3 , z2 , z, z1, z3 ), (w, w1 , w2 , y2 , y, y1 ). Thus, if we connect
these sets of nodes with simple amoeboids instead of with complex ones, we have up
to injective renamings a translation of (uxy)Q(x, y, x)|R(u, x)|S(x, y) as required.
Example 6 (Translation of a transition with recursion)
We will show here an example that uses recursion. Let us consider the closed process
(uz)uz| rec X.(x)ux.(ux.0|X). The translation of this process, as shown in Example
3 is:
u, z, y, u1, z1 , u2 , y1 , u3 , y2 , u4 , u5 ⊢
Lx1 x2 .0 (u1 , z1 )|Lx1 x2 .(x3 x4 .0| rec X.(x)x5 x.(x6 x.0|X)) (u2 , y1 , u3 , y2 , u4 , u5 )|
m6 (u, u1 , u2 , u3 , u4 , u5 )|m2 (z, z1 )|m3 (y, y1 , y2 )|n(u)|n(z)|n(y)
We need the productions for two sequential edges (for the first step): x1 x2 .0 and
x1 x2 .(x3 x4 .0| rec X.(x)x5 x.(ux6 .0|X)).

21

Mapping Fusion and SHR into Logic Programming
Fig. 7. Resulting graph

m2
x2

n

x

z2

x1

m4

1

z1

LQ(x ,x ,x ) 3
1

2

3

z

m4

n

2

x3

z3

y1

2

1

LR(x ,x )

m3

1 2

1

u1

n

LS(x

1 ,x 2)

2

y2

u2

n

y

m4

u3

w2

m2

n

w1

m3

w

n

u

n

The productions are the ones of Example 4 (we write them here in a suitable αconverted form):
(u1 ,out1 ,hz1 i)

u1 , z1 ⊢ Lx1 x2 .0 (u1 , z1 ) −−−−−−−−−→ u1 , z1 ⊢ n(u1 )
u2 , y1 , u3 , y2 , u4 , u5 ⊢ Lx1 x2 .(x3 x4 .0| rec X.(x)x5 x.(x6 x.0|X)) (u2 , y1 , u3 , y2 , u4 , u5 )
u2 ,in1 ,hy1 i

−−−−−−−→
u2 , y1 , u3 , y2 , u4 , u5 , w1 , w2 , w3 , w4 , w5 , w6 , y ′ , u′4 , u′5 ⊢
Lx1 x2 .0 (u3 , y2 )|Lx1 x2 .(x3 x4 .0| rec X.((x)x5 x.(x6 x.0|X))) (w1 , w2 , w3 , w4 , w5 , w6 )|
m3 (u′4 , w1 , w5 )|m3 (u′5 , w3 , w6 )|m3 (y ′ , w2 , w4 )|n(y ′ )|m2 (u4 , u′4 )|m2 (u5 , u′5 )|n(u2 )
By using these two productions and a production for m6 (the other edges stay idle)
we have the following transition:
u, z, y, u1, z1 , u2 , y1 , u3 , y2 , u4 , u5 ⊢
Lx1 x2 .0 (u1 , z1 )|Lx1 x2 .(x3 x4 .0| rec X.(x)x5 x.(x6 x.0|X)) (u2 , y1 , u3 , y2 , u4 , u5 )|
m6 (u, u1 , u2 , u3 , u4 , u5 )|m2 (z, z1 )|m3 (y, y1 , y2 )|n(u)|n(z)|n(y)
(u1 ,out1 ,hz1 i)(u2 ,in1 ,hy1 i)

−−−−−−−−−−−−−−−−−→
u, y, z, x, u1, z1 , u2 , y1 , u3 , y2 , u4 , u5 , w1 , w2 , w3 , w4 , w5 , w6 , y ′ , u′4 , u′5 ⊢
n(u1 )|Lx1 x2 .0 (u3 , y2 )|Lx1 x2 .(x3 x4 .0| rec X.((x)x5 x.(x6 x.0|X))) (w1 , w2 , w3 , w4 , w5 , w6 )|
m3 (u′4 , w1 , w5 )|m3 (u′5 , w3 , w6 )|m3 (y ′ , w2 , w4 )|n(y ′ )|m2 (u4 , u′4 )|m2 (u5 , u′5 )|n(u2 )|
m6 (u, u1 , u2 , u3 , u4 , u5 )|m2 (z1 , y1 )|m2 (z, z1 )|m3 (y, y1 , y2 )|n(u)|n(z)|n(y)
The resulting graph is, up to injective renaming and equivalence of amoeboids, a

22

Ivan Lanese and Ugo Montanari

translation of:
(uyy ′ )(uy.0|uy ′ .(uy ′ .0| rec X.(x)ux.(ux.0|X)))
as required.
We end this section with a simple schema on the correspondence between the
two models.
Fusion

HSHR

Closed process
Graph
Sequential process Edge
Production
Prefix execution

Fusion

HSHR

Reduction Transition
Name
Amoeboid
0
N il

As shown in the table, we represent (closed) processes by graphs where edges
are sequential processes and amoeboids model names. The inactive process 0 is the
empty graph nil. From a dynamic point of view, Fusion reductions are modelled by
HSHR transitions obtained composing productions that represent prefix executions.
4 Mapping Hoare SHR into logic programming
We will now present a mapping from HSHR into a subset of logic programming
called Synchronized Logic Programming (SLP). The idea is to compose this mapping with the previous one obtaining a mapping from Fusion Calculus into logic
programming.
4.1 Synchronized Logic Programming
In this subsection we present Synchronized Logic Programming.
SLP has been introduced because logic programming allows for many execution
strategies and for complex interactions. Essentially SLP is obtained from standard
logic programming by adding a mechanism of transactions. The approach is similar
to the zero-safe nets approach (Bruni and Montanari 2000) for Petri nets. In particular we consider that function symbols are resources that can be used only inside a
transaction. A transaction can thus end only when the goal contains just predicates
and variables. During a transaction, which is called big-step in this setting, each
atom can be rewritten at most once. If a transaction can not be terminated, then
the computation is not allowed. A computation is thus a sequence of big-steps.
This synchronized flavour of logic programming corresponds to HSHR since:
• used goals correspond to graphs (goal-graphs);
• clauses in programs correspond to HSHR productions (synchronized clauses);
• resulting computations model HSHR computations (synchronized computations).
Definition 18 (Goal-graph)
We call goal-graph a goal which has no function symbols (constants are considered
as functions of arity 0).

Mapping Fusion and SHR into Logic Programming

23

Definition 19 (Synchronized program)
A synchronized program is a finite set of synchronized rules, i.e. definite program
clauses such that:
• the body of each rule is a goal-graph;
• the head of each rule is A(t1 , . . . , tn ) where ti is either a variable or a single
function (of arity at least 1) symbol applied to variables. If it is a variable
then it also appears in the body of the clause.
Example 7
q(f (x), y) ← p(x, y)
q(f (x), y) ← p(x, f (y))
q(g(f (x)), y) ← p(x, y)
q(f (x), y, f (z)) ← p(x)
q(f (x), f (z)) ← p(x)

synchronized rule;
not synchronized since p(x, f (y)) is not a goal-graph;
not synchronized since it contains nested functions;
not synchronized since y is an argument of the head
predicate but it does not appear in the body;
synchronized, even if z does not appear in the body.

In the mapping, the transaction mechanism is used to model the synchronization
of HSHR, where edges can be rewritten only if the synchronization constraints
are satisfied. In particular, a clause A(t1 , . . . , tn ) ← B1 , . . . , Bn will represent a
production where the head predicate A is the label of the edge in the left hand side,
and the body B1 , . . . , Bn is the graph in the right hand side. Term ti in the head
represents the action occurring in xi , if A(x1 , . . . , xn ) is the edge matched by the
production. Intuitively, the first condition of Definition 19 says that the result of a
local rewriting must be a goal-graph. The second condition forbids synchronizations
with structured actions, which are not allowed in HSHR (this would correspond to
allow an action in a production to synchronize with a sequence of actions from
a computation of an adjacent subgraph). Furthermore it imposes that we cannot
disconnect from a node without synchronizing on it 3 .
Now we will define the subset of computations we are interested in.
Definition 20 (Synchronized Logic Programming)
Given a synchronized program P we write:
θ

G1 ⇒ G2
θ′

iff G1 −→* G2 and all steps performed in the computation expand different atoms
of G1 , θ′ |n(G1 ) = θ and both G1 and G2 are goal-graphs.
θ

We call G1 ⇒ G2 a big-step and all the → steps in a big-step small-steps.
A SLP computation is:
G1 ⇒∗ G2 i.e. a sequence of 0 or more big-steps.
3

This condition has only the technical meaning of making impossible some rewritings in which
an incorrect transition may not be forbidden because its only effect is on the discarded variable.
Luckily, we can impose this condition without altering the power of the formalism, because we
can always perform a special f oo action on the node we disconnect from and make sure that all
the other edges can freely do the same action. For example we can rewrite q(f (x), y, f (z)) ← p(x)
as q(f (x), f oo(y), f (z)) ← p(x), which is an allowed synchronized rule. An explicit translation
of action ǫ can be used too.

24

Ivan Lanese and Ugo Montanari
4.2 The mapping

We want to use SLP to model HSHR systems. As a first step we need to translate graphs, i.e. syntactic judgements, to goals. In this translation, edge labels are
mapped into SLP predicates. Goals corresponding to graphs will have no function symbols. However function symbols will be used to represent actions. In the
translation we will lose the context Γ.
Definition 21 (Translation for syntactic judgements)
We define the translation operator J−K as:
JΓ ⊢ L(x1 , . . . , xn )K = L(x1 , . . . , xn )
JΓ ⊢ G1 |G2 K = JΓ ⊢ G1 K, JΓ ⊢ G2 K
JΓ ⊢ nilK = 
Sometimes we will omit the Γ part of the syntactic judgement. We can do this
because it does not influence the translation. For simplicity, we suppose that the
set of nodes in the SHR model coincides with the set of variables in SLP (otherwise
we need a bijective translation function). We do the same for edge labels and names
of predicates, and for actions and function symbols.
Definition 22
Let Γ ⊢ G and Γ′ ⊢ G′ be graphs. We define the equivalence relation ∼
= in the
following way: Γ ⊢ G ∼
= Γ′ ⊢ G′ iff G ≡ G′ .
Observe that if two judgements are equivalent then they can be written as:
Γ, Γunused ⊢ G
Γ, Γ′unused ⊢ G
where Γ = n(G).
Theorem 3 (Correspondence of judgements and goal-graphs)
The operator J−K defines an isomorphism between judgements (defined up to ∼
=)
and goal-graphs.
Proof
The proof is straightforward observing that the operator J−K defines a bijection
between representatives of syntactic judgements and representatives of goal-graphs
and the congruence on the two structures is essentially the same.
We now define the translation from HSHR productions to definite clauses.
Definition 23 (Translation from productions to clauses)
We define the translation operator J−K as:
Λ,π

JL(x1 , . . . , xn ) −−→ GK = L(a1 (x1 π, ~y1 ), . . . , an (xn π, ~yn )) ← JGK
if Λ(xi ) = (ai , ~yi ) for each i ∈ {1, . . . , n} and if ai 6= ǫ. If ai = ǫ we write simply
xi π instead of ǫ(xi π).

25

Mapping Fusion and SHR into Logic Programming

The idea of the translation is that the condition given by an action (x, a, ~y ) is
represented by using the term a(xπ, ~y ) as argument in the position that corresponds
to x. Notice that in this term a is a function symbol and π is a substitution. During
unification, x will be bound to that term and, when other instances of x are met, the
corresponding term must contain the same function symbol (as required by Hoare
synchronization) in order to be unifiable. Furthermore the corresponding tuples of
transmitted nodes are unified. Since x will disappear we need another variable to
represent the node that corresponds to x. We use the first argument of a to this
purpose. If two nodes are merged by π then their successors are the same as required.
Observe that we do not need to translate all the possible variants of the rules
since variants with fresh variables are automatically built when the clauses are applied. Notice also that the clauses we obtain are synchronized clauses.
The observable substitution contains information on Λ and π. Thus given a transition we can associate to it a substitution θ. We have different choices for θ according
to where we map variables. In fact in HSHR nodes are mapped to their representatives according to π, while, in SLP, θ cannot do the same, since the variables of
the clause variant must be all fresh. The possible choices of fresh names for the
variables change by an injective renaming the result of the big-step.
Definition 24 (Substitution associated to a transition)
Λ,π

Let Γ ⊢ G −−→ Φ ⊢ G′ be a transition. We say that the substitution θρ associated
to this transition is:
θρ = {(a(xπρ, ~y ρ)/x|Λ(x) = (a, ~y), a 6= ǫ} ∪ {xπρ/x}|Λ(x) = (ǫ, hi)}
for some injective renaming ρ.
We will now prove the correctness and the completeness of our translation.
Theorem 4 (Correctness)
Let P be a set of productions of a HSHR system as defined in definitions 9 and 10.
Let P be the logic program obtained by translating the productions in P according
to Definition 23. If:
Λ,π
P (Γ ⊢ G −−→ Φ ⊢ G′ )
then we can have in P a big-step of Synchronized Logic Programming:
θρ

JΓ ⊢ GK ⇒ T
for every ρ such that xρ is a fresh variable unless possibly when x ∈ Γ∧Λ(x) = (ǫ, hi).
Λ,π

In that case we may have xρ = x. Furthermore θρ is associated to Γ ⊢ G −−→ Φ ⊢ G′
and T = JΦ ⊢ G′ Kρ. Finally, used productions translate into the clauses used in the
big-step and are applied to the edges that translate into the predicates rewritten
by them.
Proof
The proof is by rule induction.
See Appendix A.

26

Ivan Lanese and Ugo Montanari

Theorem 5 (Completeness)
Let P be a set of productions of a HSHR system. Let P be the logic program
obtained by translating the productions in P according to Definition 23. If we have
in P a big-step of logic programming:
θ
JΓ ⊢ GK ⇒ T
Λ,π

then there exist ρ, θ′ , Λ, π, Φ and G′ such that θ = θρ′ is associated to Γ ⊢ G −−→
Φ ⊢ G′ . Furthermore T = JΦ ⊢ G′ Kρ and P

Λ,π

(Γ ⊢ G −−→ Φ ⊢ G′ ).

Proof
See Appendix A.
Example 8
We continue here Example 5 by showing how that fusion computation can be translated into a Synchronized Logic Programming computation.
(uxyzw)(Q(x, y, z)|uxy.R(u, x)|uzw.S(z, w)) →
(uxy)(Q(x, y, z)|R(u, x)|S(z, w)){x/z, y/w}
Remember that a translation of the starting process is:
u, x, y, w, z, x1 , y1 , z1 , u1 , x2 , y2 , u2 , x3 , u3 , z2 , w1 , z3 , w2 ⊢
LQ(x1 ,x2 ,x3 ) (x1 , y1 , z1 )|Lx1 x2 x3 .R(x4 ,x5 ) (u1 , x2 , y2 , u2 , x3 )|
Lx1 x2 x3 .S(x4 ,x5 ) (u3 , z2 , w1 , z3 , w2 )|m4 (u, u1 , u2 , u3 )|m4 (x, x1 , x2 , x3 )|
m3 (y, y1 , y2 )|m4 (z, z1 , z2 , z3 )|m3 (w, w1 , w2 )|n(u)|n(x)|n(y)|n(w)|n(z)
We have the following productions:
(y1 ,out2 ,hy2 ,y3 i)

y1 , y2 , y3 , y4 , y5 ⊢ Lx1 x2 x3 .R(x4 ,x5 ) (y1 , y2 , y3 , y4 , y5 ) −−−−−−−−−−−→
y1 , y2 , y3 , y4 , y5 ⊢ LR(x1 ,x2 ) (y4 , y5 )|n(y1 )
(y1 ,in2 ,hy2 ,y3 i)

y1 , y2 , y3 , y4 , y5 ⊢ Lx1 x2 x3 .S(x4 ,x5 ) (y1 , y2 , y3 , y4 , y5 ) −−−−−−−−−−→
y1 , y2 , y3 , y4 , y5 ⊢ LS(x1 ,x2 ) (y4 , y5 )|n(y1 )
that corresponds to the clauses (we directly write suitably renamed variants):
Lx1 x2 x3 .R(x4 ,x5 ) (out2 (u′1 , x′2 , y2′ ), x′2 , y2′ , u′2 , x′3 ) ← LR(x1 ,x2 ) (u′2 , x′3 )|n(u′1 )
′′′
′′′
′′′
′′′ ′′′
′′′
′′′
′′′
′′′
Lx1 x2 x3 .S(x4 ,x5 ) (in2 (u′′′
3 , z2 , w1 ), z2 , w1 , z3 , w2 ) ← LS(x1 ,x2 ) (z3 , w2 )|n(u3 )
plus the clause obtained from the auxiliary production:
m4 (u′′ , out2 (u′′1 , x′′2 , y2′′ ), u′′2 , in2 (u′′3 , z2′′ , w1′′ )) ←
m4 (u′′ , u′′1 , u′′2 , u′′3 ), m2 (x′′2 , z2′′ ), m2 (y2′′ , w1′′ )
We obtain the big-step represented in Figure 8. The observable substitution of the
big-step is {out2 (u′1 , x2 , y2 )/u1 , in2 (u′′3 , z2 , w1 )/u3 }. This is associated to the wanted
HSHR transition with ρ = {u′1 /u1 , u′′3 /u3 } and by applying ρ to the final graph of

Mapping Fusion and SHR into Logic Programming

27

Fig. 8. Big-step for a Fusion transition
LQ(x1 ,x2 ,x3 ) (x1 , y1 , z1 ), Lx1 x2 x3 .R(x4 ,x5 ) (u1 , x2 , y2 , u2 , x3 ),
Lx1 x2 x3 .S(x4 ,x5 ) (u3 , z2 , w1 , z3 , w2 ),
m4 (u, u1 , u2 , u3 ), m4 (x, x1 , x2 , x3 ), m3 (y, y1 , y2 ), m4 (z, z1 , z2 , z3 ), m3 (w, w1 , w2 ),
n(u), n(x), n(y), n(w), n(z)
′
out2 (u′1 ,x2 ,y2 )/u1 ,x2 /x′2 ,y2 /y2
,u2 /u′2 ,x3 /x′3

−−−−−−−−−−−−−−−−−−−−−−−−−−−−−→
LQ(x1 ,x2 ,x3 ) (x1 , y1 , z1 ), LR(x1 ,x2 ) (u2 , x3 ), n(u′1 ), Lx1 x2 x3 .S(x4 ,x5 ) (u3 , z2 , w1 , z3 , w2 ),
m4 (u, out2 (u′1 , x2 , y2 ), u2 , u3 ), m4 (x, x1 , x2 , x3 ), m3 (y, y1 , y2 ),
m4 (z, z1 , z2 , z3 ), m3 (w, w1 , w2 ), n(u), n(x), n(y), n(w), n(z)
u/u′′ ,u′ /u′′ ,x2 /x′′ ,y2 /y ′′ ,u2 /u′′ ,in2 (u′′ ,z ′′ ,w′′ )/u3

1
2
2
3 2
−−−−−−
−−1−−−−−
−−−−2−−−−−
−−−−−
−−−−1−−−→

LQ(x1 ,x2 ,x3 ) (x1 , y1 , z1 ), LR(x1 ,x2 ) (u2 , x3 ), n(u′1 ),
Lx1 x2 x3 .S(x4 ,x5 ) (in2 (u′′3 , z2′′ , w1′′ ), z2 , w1 , z3 , w2 ),
′
m4 (u, u1 , u2 , u′′3 ), m2 (x2 , z2′′ ), m2 (y2 , w1′′ ), m4 (x, x1 , x2 , x3 ), m3 (y, y1 , y2 ),
m4 (z, z1 , z2 , z3 ), m3 (w, w1 , w2 ), n(u), n(x), n(y), n(w), n(z)
u′′ /u′′′ ,z2 /z ′′ ,w1 /w′′ ,z2 /z ′′′ ,w1 /w′′′ ,z3 /z ′′′ ,w2 /w′′′

3
2
1
3
−−
−−3−−−−−2−−−−−1−−−−−
−−−−−
−−−−−
−−−−−2→

LQ(x1 ,x2 ,x3 ) (x1 , y1 , z1 ), LR(x1 ,x2 ) (u2 , x3 ), n(u′1 ), LS(x1 ,x2 ) (z3 , w2 ), n(u′′3 ),
m4 (u, u′1 , u2 , u′′3 ), m2 (x2 , z2 ), m2 (y2 , w1 ), m4 (x, x1 , x2 , x3 ), m3 (y, y1 , y2 ),
m4 (z, z1 , z2 , z3 ), m3 (w, w1 , w2 ), n(u), n(x), n(y), n(w), n(z)

the HSHR transition we obtain:
LQ(x1 ,x2 ,x3 ) (x1 , y1 , z1 )|LR(x1 ,x2 ) (u2 , x3 )|n(u′1 )|LS(x1 ,x2 ) (z3 , w2 )|n(u′′3 )|
m4 (u, u′1 , u2 , u′′3 )|m4 (x, x1 , x2 , x3 )|m3 (y, y1 , y2 )|m4 (z, z1 , z2 , z3 )|m3 (w, w1 , w2 )|
m2 (x2 , z2 )|m2 (y2 , w1 )|n(u)|n(x)|n(y)|n(w)|n(z)
that, translated, becomes the final goal of the big-step as required.
We end this section with a simple schema on the correspondence between the
two models.
HSHR

SLP

HSHR

SLP

Graph
Edge
Parallel comp.
Production

Goal
Atomic goal
And comp.
Clause

Transition
Node
N il
Action

Big-step
Variable

Function s.

Essentially the correspondence is given by the homomorphism between graphs
and goals, with edges mapped to atomic goals, nodes to variables, parallel composition to And composition and nil to . Dynamically, HSHR transitions are

28

Ivan Lanese and Ugo Montanari

modelled by big-steps, that are transactional applications of clauses which model
productions. Finally, HSHR actions are modelled by function symbols.
4.3 Using Prolog to implement Fusion Calculus
The theorems seen in the previous sections can be used for implementation purposes. As far as Synchronized Logic Programming is concerned, in Lanese (2002) a
simple meta-interpreter is presented.
The idea is to use Prolog ability of dynamically changing the clause database
to insert into it a set of clauses and a goal and to compute the possible synchronized computations of given length. This can be directly used to simulate HSHR
transitions. In order to simulate Fusion Calculus processes we have to implement
amoeboids using a bounded number of different connectors (note that m2 , m3 and
n are enough) and to implement in the meta-interpreter the condition under which
productions can be applied in a single big-step. This can be easily done. Furthermore this decreases the possible choices of applicable productions and thus improves
the efficiency w.r.t. the general case.
5 Conclusion
In this paper we have analyzed the relationships between three different formalisms,
namely Fusion Calculus, HSHR and logic programming.
The correspondence between HSHR and the chosen transactional version of logic
programming, SLP, is complete and quite natural. Thus we can consider HSHR as
a “subcalculus” of (synchronized) logic programming.
The mapping between Fusion Calculus and HSHR is instead more involved because it has to deal with many important differences:
• process calculi features vs graph transformation features;
• interleaving models vs concurrent models;
• Milner synchronization vs Hoare synchronization.
Hoare synchronization was necessary since our aim was to eventually map Fusion
Calculus to logic programming. If the aim is just to compare Fusion Calculus and
SHR it is possible to use SHR with Milner synchronization, achieving a much simpler and complete mapping, which considers the LTS of Fusion Calculus instead of
reductions (see Lanese and Montanari 2004a).
We think that the present work can suggest several interesting lines of development, dictated by the comparison of the three formalisms studied in the paper.
First, our implementation of routers in terms of amoeboids is rather general and abstract, and shows that Fusion Calculus names are a rather high level concept. They
abstract out the behaviour of an underlying network of connections which must
be open and reconfigurable. Had we chosen π-calculus instead (see a translation of
π-calculus to Milner SHR in (Hirsch and Montanari 2001)), we would have noticed
important differences. For instance, fusions are also considered in the semantics

Mapping Fusion and SHR into Logic Programming

29

of open π-calculus by Davide Sangiorgi (Sangiorgi 1993), but in that work not all
the names can be fused: newly extruded names cannot be merged with previously
generated names. This is essential for specifying nonces and session keys for secure
protocols. Instead, Fusion Calculus does not provide equivalent constructs. Looking at our translation, we can conclude that logic programming does not offer this
feature, either. Thus logic programming is a suitable counterpart of Fusion Calculus, but it should be properly extended for matching open π-calculus and security
applications.
In a similar line of thought, we observe that we have a scope restriction operator in
the Fusion Calculus, but no restriction is found in our version of HSHR. We think
this omission simplifies our development, since no restriction exists in ordinary
logic programming, either. However versions of SHR with restriction have been
considered (Hirsch and Montanari 2001; Ferrari et al. 2001; Lanese 2002). Also
(synchronized) logic programming can be smoothly extended with a restriction
operator (Lanese 2002). More importantly, Fusion Calculus is equipped with an
observational abstract semantics based on (hyper) bisimulation. We did not consider
a similar concept for SHR or logic programming, since we considered it outside the
scope of the paper. Furthermore our operational correspondence between HSHR
and SLP is very strong and it should respect any reasonable abstract semantics.
The mapping from Fusion Calculus into HSHR deals only with closed terms, thus
no observations can be considered. However a bisimulation semantics of SHR has
been considered in (König and Montanari 2001), and an observational semantics of
logic programming is discussed in (Bruni et al. 2001).
Another comment concerns concurrency. To prove the equivalence of Fusion Calculus and of its translation into HSHR we had to restrict the possible computations
of the latter. On the contrary, if all computations were allowed, the same translation would yield a concurrent semantics of Fusion Calculus, that we think is worth
studying. For instance in the presence of concurrent computations not all equivalent amoeboids would have the same behaviour, since some of them would allow for
more parallelism than others.
Finally we would like to emphasize some practical implication of our work. In fact,
logic programming is not only a model of computation, but also a well developed
programming paradigm. Following the lines of our translation, implementations
of languages based on Fusion Calculus and HSHR could be designed, allowing to
exploit existing ideas, algorithms and tools developed for logic programming.

References
Bruni, R. and Montanari, U. 2000. Zero-safe nets: Comparing the collective and individual token approaches. Information and Computation 156, 1-2, 46–89.
Bruni, R., Montanari, U., and Rossi, F. 2001. An interactive semantics of logic
programming. Theory and Practice of Logic Programming 1, 6, 647–690.
Degano, P. and Montanari, U. 1987. A model for distributed systems based on graph
rewriting. Journal of the ACM (JACM) 34, 2, 411–449.
Ehrig, H., Kreowski, H.-J., Montanari, U., and Rozenberg, G., Eds. 1999. Hand-

30

Ivan Lanese and Ugo Montanari

book of Graph Grammars and Computing by Graph Transformation, Vol.3: Concurrency, Parallelism, and Distribution. World Scientific.
Ehrig, H., Pfender, M., and Schneider, H. J. 1973. Graph grammars: an algebraic
approach. In Proc. of IEEE Conference on Automata and Switching Theory. IEEE
Computer Society, 167–180.
Ferrari, G. L., Montanari, U., and Tuosto, E. 2001. A LTS semantics of ambients via
graph synchronization with mobility. In Proc. of ICTCS’01. LNCS, vol. 2202. Springer,
1–16.
Gardner, P. and Wischik, L. 2000. Explicit fusions. In Mathematical Foundations of
Computer Science. 373–382.
Gardner, P. and Wischik, L. 2004. Strong bisimulation for the explicit fusion calculus.
In Proc. of FoSSaCS’04. LNCS, vol. 2987. Springer, 484–498.
Hirsch, D. 2003. Graph transformation models for software architecture styles. Ph.D.
thesis, Departamento de Computación, Facultad de Ciencias Exactas y Naturales, Universidad de Buenos Aires, Argentina.
Hirsch, D., Inverardi, P., and Montanari, U. 2000. Reconfiguration of software
architecture styles with name mobility. In Proc. of COORDINATION 2000. LNCS, vol.
1906. Springer, 148–163.
Hirsch, D. and Montanari, U. 2001. Synchronized hyperedge replacement with name
mobility. In Proc. of CONCUR’01. LNCS, vol. 2154. Springer, 121–136.
Jensen, O. H. and Milner, R. 2003. Bigraphs and transitions. SIGPLAN Not. 38, 1,
38–49.
König, B. and Montanari, U. 2001. Observational equivalence for synchronized graph
rewriting. In Proc. of TACS’01. LNCS, vol. 2215. Springer, 145–164.
Lanese, I. 2002. Process synchronization in distributed systems via Horn clauses. M.S.
thesis, Computer Science Department, University of Pisa, Pisa, Italy. Downloadable
from http://www.di.unipi.it/~lanese/tesi.ps.
Lanese, I. 2006. Synchronization strategies for global computing models. Ph.D. thesis,
Computer Science Department, University of Pisa, Pisa, Italy. Forthcoming.
Lanese, I. and Montanari, U. 2002. Software architectures, global computing and graph
transformation via logic programming. In Proc SBES’2002 - 16th Brazilian Symposium
on Software Engineering. Anais, 11–35.
Lanese, I. and Montanari, U. 2004a. A graphical fusion calculus. In Proc. of the
Workshop of the COMETA Project on Computational Metamodels. Electronic Notes in
Theoretical Computer Science, vol. 104. Elsevier Science, 199–215.
Lanese, I. and Montanari, U. 2004b. Synchronization algebras with mobility for graph
transformations. In Proc. of FGUC’04 – Foundations of Global Ubiquitous Computing.
Electronic Notes in Theoretical Computer Science, vol. 138. Elsevier Science, 43–60.
Lloyd, J. W. 1993. Foundations of Logic Programming, Second Extended Edition.
Springer.
Milner, R., Parrow, J., and Walker, D. 1992. A calculus of mobile processes. Information and Computation 100, 1–77.
Palamidessi, C. 1990. Algebraic properties of idempotent substitutions. In Proc. of
ICALP’90. LNCS, vol. 443. Springer, 386–399.
Parrow, J. and Victor, B. 1998. The fusion calculus: Expressiveness and symmetry in
mobile processes. In Proc. of LICS ’98. IEEE, Computer Society Press.
Sangiorgi, D. 1993. A theory of bisimulation for the pi-calculus. In Proc. of CONCUR’93.
LNCS, vol. 715. Springer, 127–142.
Victor, B. 1998. The fusion calculus: Expressiveness and symmetry in mobile processes.
Ph.D. thesis, Dept. of Computer Systems, Uppsala University, Sweden.

Mapping Fusion and SHR into Logic Programming

31

Appendix A Proofs
We have here the proofs that are missing in the main part and some lemmas used
in these proofs. Lemmas are just before the proofs that use them.
Proof of Lemma 2
Notice that all the auxiliary productions perform two non trivial actions, and because of Hoare synchronization and because each node is shared by at most two
edges, synchronizing edges form chains. There are two alternatives: each chain either starts and begins on an external node, or it is a cycle that contains only internal
nodes. Exactly one chain must be of the first type. In fact if we have no chain of
that kind we have only trivial actions on nodes in S. Also, if we have more than
one, we have more than two non trivial actions on nodes in S. Thanks to the last
condition of Definition 17 this chain contains an odd number of connectors, which
must be m connectors. One can easily check by induction on the (odd) length of the
chain that the transition creates an amoeboid M (~y1 [i], ~y2 [i]) for each component of
vectors ~y1 and ~
y2 of fresh names and that these vectors are exposed on the external
nodes together with an inn and an outn action, where n = |~y1 | = |~y2 |.
Let us now consider the other kind of chains: these chains produce rings of m2
edges connected only to fresh nodes, which thus correspond to isolate subgraphs.
Furthermore, they affect only the labels of internal nodes as required.
Lemma 3
Given a set of amoeboids
 for σ and a substitutive effect θ of a fusion φ = {xi =
yi |i = 1 . . . n} then JσK| i=1...n M (xi , yi ) is a set of amoeboids for σθ.
Proof
Since we are working up to injective
renamings we only have to prove that two

names are connected by JσK| i=1...n M (xi , yi ) iff they are merged by σθ and that
all the paths connecting external nodes in the final graph have odd length. By
definition two names are connected by JσK iff they are merged by σ. Assume that
two names x and y are merged by σθ. Then their images along σ are merged by θ.
This means that we have in φ a chain of equalities from xσ to yσ. Thus we have
amoeboids connecting the amoeboids of xσ and of yσ, thus x and y are connected.
Assume now that x and y are connected. Then there exists an amoeboid connecting
the amoeboids for xσ and for yσ. Thus θ merges xσ and yσ as required. Finally
note that all the paths between external nodes are created by connecting existing
paths via new amoeboids. In particular, each new path is composed by n old paths
and n − 1 new amoeboids. Thus its length is the sum of 2n − 1 odd lengths and
thus it is odd.
Proof of Theorem 1
The proof is by rule induction on the reduction semantics.
Let us consider the reduction rule:
(~z)(R|(· · · + u~x.P )|(u~y .Q + . . . )) → (~z)(R|P |Q)σ

32

Ivan Lanese and Ugo Montanari

where |~x| = |~y | and σ is a substitutive effect of {~x = ~y } such that dom(σ) ⊆ ~z.
In order for that process to be in the standard form we just need to make R
sequential by unfolding recursion and taking bound names to the outside if required.
For simplicity, we show just the case where R is already sequential, the other being
essentially equal.
Let P1 be (· · · + u~x.P ) and Q1 be (u~y .Q + . . . ).
The translation of the LHS has the form:

Γ ⊢ LR̂′ (~r)|LP̂ ′ (~
p1 )|LQ̂′ (~q1 )|JθK| x∈~v n(x)
1

1

where R′ = R̂′ ρR′ , P1′ = P̂1′ ρP1′ , Q′1 = Q̂′1 ρQ′1 and R′ θ = R, P1′ θ = P1 , Q′1 θ = Q1 .
We also use (u′1~x′ .P ′ )θ = u~x.P and (u′2 ~y ′ .Q′ )θ = u~y.Q.
We have for LP̂ ′ and LQ̂′ the two following productions:
1

1

(u′1 ,in|~
x′ )
x′ | ,~

p~1 ⊢ LP̂ ′ (~
p1 ) −−−−−−−−→ p~1 , ~x′ , ~vP ⊢ JP K~vp ,w~ P |
1

(u′2 ,out|~
y′ )
y′ | ,~



q1 ⊢ LQ̂′ (~
~
q1 ) −−−−−−−−−→ ~q1 , ~y ′ , ~vQ ⊢ JQK~vQ ,w~ Q |
1

x∈Γ′′
P



x∈Γ′′
Q

n(x)
n(x)

The choice of the parameters ~vP and ~vQ is not important since they are fresh
names and we work up to injective renamings. The choice of w
~ P and w
~ Q is important
instead, since they have to correspond to the nodes in the LHS that are still used
by the process. The choice performed in Definition 15 ensures that.
Note that JθK contains an amoeboid for a set U with u′1 , u′2 ∈ U . Thus from
Lemma 2 the two above productions can synchronize via the amoeboid. Using rule
(idle) for the other edges, we obtain as a result:

Γ, ΓInt ⊢ LR̂′ (~r)|JP K~vP ,w~ P |



x∈Γ′′
P



n(x)|JQK~vQ ,w~ Q | x∈Γ′′ n(x)|JθK| x∈~v n(x)|
Q


M (~x′ [i], ~y ′ [i])| M̃ (∅)
i=1...|~
x′ |

Note that the fusion π of the transition is the identity since each synchronization
involves two edges, and at least one of them is an amoeboid which exposes fresh
names. Furthermore amoeboids expose each fresh name twice. Thus no names in Γ
are merged.
Also, in the final graph each node is shared by two edges. In fact, the only connections whose cardinality is not preserved by productions are the ones between
nodes whose references are exposed, namely ~x′ and ~y′ , and the corresponding process edges, but these nodes are connected to the new M amoeboids created by the
auxiliary productions.


In particular, x∈Γ′′ n(x)| x∈Γ′′ n(x)|JθK is an amoeboid for θ|fn(R′ |P ′ |Q′ ) . FurQ
P

thermore thanks to Lemma 3 by adding in parallel i=1...|~x′ | M (~x′ [i], ~y ′ [i]) we obtain
an amoeboid for θ|fn(R′ |P ′ |Q′ ) σ.
Thus we can rewrite the final graph up to pseudoamoeboids as:
Γ, ΓInt ⊢ LR̂′ (~r)|JP K~vP ,w~ P |JQK~vQ ,w~ Q |Jθ|fn(R′ |P ′ |Q′ ) σK|



x∈~
v

n(x)

Mapping Fusion and SHR into Logic Programming

33

The RHS of the fusion rule is (~z)(R|P |Q)σ, which has to be normalized into
(~z~vP ~vQ )(R|P̃ |Q̃)θ1 σ with (~vP )P̃ ≡ P and (~vQ )Q̃ ≡ Q. Furthermore we can choose
the names (since we are reasoning up to injective renamings) in such a way that θ1 =
θ|fn(R′ |P ′ |Q′ ) (plus an injective renaming on names in ~vp and ~vQ which corresponds
to an equivalence on the resulting amoeboids).
Thus the translation of the RHS is equivalent to:
Γ, ΓInt′ ⊢ LR̂′ (~r)|JP K~vP ,w~ P |JQK~vQ ,w~ Q |Jθ1 σK|



x∈~
v

n(x)

The correctness of the rule follows.
Let us consider now rule:
(~z)(R|(· · · + φ.P )) → (~z)(R|P )σ
where σ is a substitutive effect of φ such that dom(σ) ⊆ ~z.
We use essentially the same technique as before. Let us suppose R already sequential. Let P1 be · · · + φ.P . The translation of the LHS has the form:
Γ ⊢ LR̂′ (~r)|LP̂ ′ (~
p1 )|JθK|
1



x∈~
v

n(x)

where R′ = R̂′ ρR′ , P1′ = P̂1′ ρP1′ and R′ θ = R, P1′ θ = P1 . We also use (φ′ .P ′ )θ = φ.P .
We have for LP̂ ′ the following production:
1

Λ

ǫ
~p1 , ~vP ⊢ JP K~vP ,w~ P |JσK|
p~1 ⊢ LP̂ ′ (~
p1 ) −→
1



x∈Γ′′

n(x)

For ~vP and w
~ P the considerations for the preceding rule are still valid.
Using rule (idle) for the other edges, we obtain as a result:
Γ, ΓInt ⊢ LR̂′ (~r)|JP K~vP ,w~ P |JσK|



x∈Γ′′
P

n(x)|JθK|



x∈~
v

n(x)

Note that the fusion part of the transition label is an identity since we have only
trivial synchronizations.
Also, in the final graph each node is shared by two edges since the production
preserves the cardinality of connected edges for each node.

In particular, x∈Γ′′ n(x)|JθK is an amoeboid for θ|fn(R′ |P ′ ) . Furthermore, note
P

that JσK has the form i=1...n m2 (xi , yi ) and thus thanks to Lemma 3 by adding it
in parallel we obtain an amoeboid for θ|fn(R′ |P ′ ) σ.
Thus we can rewrite the final graph as:
Γ, ΓInt ⊢ LR̂′ (~r)|JP K~vP ,w~ P |Jθ|fn(R′ |P ′ ) σK|



x∈~
v

n(x)

The RHS of the fusion rule is (~z)(R|P )σ, which has to be normalized into
(~z~vP )(R|P̃ )θ1 σ with (~vP )P̃ ≡ P . Furthermore we can choose the names (since
we are reasoning up to injective renamings) in such a way that θ1 = θ|fn(R′ |P ′ )
(plus an injective renaming on names in ~vP which corresponds to an equivalence
on the resulting amoeboids).
Thus the translation of the RHS is equivalent to:

34

Ivan Lanese and Ugo Montanari

Γ, ΓInt′ ⊢ LR̂′ (~r)|JP K~vP ,w~ P |Jθ1 σK|



x∈~
v

n(x)

The correctness of the rule follows.
Consider now the rule:
P ≡ P ′ , P ′ → Q′ , Q′ ≡ Q
P →Q
Equivalent agents are converted into the same representative (up to α-conversion)
before being translated, thus the translation of P and P ′ are equal up to injective
renamings. Similarly for the translation of Q and Q′ , thus the thesis follows.
Lemma 4
Let θ1 and θ2 be idempotent substitutions. Let eqn(θ1 ) = {x = y|x/y ∈ θ1 }. Then
mgu(eqn(θ1 ) ∪ eqn(θ2 )) = θ1 mgu(eqn(θ2 )θ1 ).
Proof
See Palamidessi (1990).
Lemma 5
Given a graph Γ ⊢ G and one or zero productions for each edge in G let:
Λ1 ,π1
Γ ⊢ G −−−−→ Φ1 ⊢ G′1
Λ2 ,π2

Γ ⊢ G −−−−→ Φ2 ⊢ G′2
be two transitions obtained by applying the chosen production for each edge (and
using the (idle) rule if no production is chosen). Then there exists an injective
renaming σ such that:
•
•
•
•

Λ1 (x) = σ(Λ2 (x)) if x is not an isolated node;
π1 = σπ2 ;
Φ1 = σ(Φ2 );
G′1 = σ(G′2 ).

Proof
The proof is a simple rule induction if one proves that derivations can be done in a
standard way, namely by applying to the axioms first rules (par), then rule (merge)
and finally rules (new). This can be proved by showing that one can exchange
the order of rules and that one can substitute two applications of (merge) with
substitutions σ and σ ′ with just one application with substitution σ ′ σ. We have
many cases to consider, but they are not so interesting. As examples we will show
the detailed proof for commutation of rule (merge) and (par) and for composition
of two different rules (merge).
Let us consider the first case. Suppose we have a part of a derivation of the form:
Λ,π

Γ ⊢ G1 −−→ Φ ⊢ G2
Λ1 ,π1

Γσ ⊢ G1 σ −−−−→ Φ1 ⊢ G2 σρ

Λ′ ,π ′

Γ′ ⊢ G′1 −−−→ Φ′ ⊢ G′2

Λ1 ∪Λ′ ,π1 ∪π ′

Γσ, Γ′ ⊢ G1 σ|G′1 −−−−−−−−→ Φ1 , Φ′ ⊢ G2 σρ|G′2

(A1)

Mapping Fusion and SHR into Logic Programming

35

where for readability we have not written explicitly the side conditions (see Definition 10). Then we must also have a derivation for the same transition obtained
applying rule (par) first and then rule (merge):
Λ,π

Γ ⊢ G1 −−→ Φ ⊢ G2

Λ′ ,π ′

Γ′ ⊢ G′1 −−−→ Φ′ ⊢ G′2

Λ∪Λ′ ,π∪π ′

Γ, Γ′ ⊢ G1 |G′1 −−−−−−−→ Φ, Φ′ ⊢ G2 |G′2
Λ′′ ,π ′′

(Γ, Γ′ )σ ⊢ (G1 |G′1 )σ −−−−→ Φ′′ ⊢ (G2 |G′2 )σρ′

(A2)

We have to prove that this derivation is allowed and that the resulting transition is
the one derived also by derivation A1. The first step is allowed iff (Γ∪Φ)∩(Γ′ ∪Φ′ ) =
∅. Since the first derivation is allowed by hypothesis, then (Γσ ∪ Φ1 ) ∩ (Γ′ ∪ Φ′ ) = ∅.
Thus the only problem is when a name which is after renamed (by σ or ρ) creates
a conflict. In that case thanks to Lemma 1 we can suppose to start with a different
name. The final result of the derivation is not changed by that since the name
disappears. Thus the first step is legal.
For the second step we need ∀x, y ∈ Γ, Γ′ .xσ = yσ ∧ x 6= y ⇒ actΛ∪Λ′ (x) =
actΛ∪Λ′ (y). Note that since (Γ ∪ Φ) ∩ (Γ′ ∪ Φ′ ) = ∅ and σ : Γ → Γ, we have that σ is
the identity on Γ′ , thus the only x, y such that xσ = yσ ∧ x 6= y are in Γ, thus the
condition is satisfied since it was satisfied in derivation A1. Furthermore we have
(Γ, Γ′ )σ = Γσ, Γ′ and (G1 |G′1 )σ = G1 σ|G′1 .
We must now consider ρ′ . We have:
ρ′ = mgu({(nΛ∪Λ′ (x))σ = (nΛ∪Λ′ (y))σ|xσ = yσ} ∪{xσ = yσ|x(π ∪π ′ ) = y(π ∪π ′ )})
For what already said we have ρ′ = mgu({(nΛ (x))σ = (nΛ (y))σ|xσ = yσ}∪{xσ =
yσ|xπ = yπ} ∪ {xσ = yσ|xπ ′ = yπ ′ }) = ρπ ′ where ρ is the one used in derivation
A1.
In particular, Λ′′ (x) = Λ1 (x) if x ∈ Γσ and Λ′′ (x) = Λ′ (x)π ′ = Λ′ (x) since π ′ is
the identity on representatives (see Definition 8). Thus Λ′′ = Λ1 ∪ Λ′ . Furthermore
π ′′ = ρ′ |Γσ,Γ′ = π1 ∪ π ′ .
Also, Φ′′ = Φ1 , Φ′ since it is determined by the first part of transition. Finally
(G2 |G′2 )σρ′ = G2 σρ′ |G′2 σρ′ = G2 σρ|G′2 π ′ = G2 σρ|G′2 . This proves that case.
We will now consider the composition of two (merge) rules, with substitutions σ
and σ ′ respectively. Suppose we have a derivation of the form:
Λ,π

Γ ⊢ G1 −−→ Φ ⊢ G2
Λ′ ,π ′

Γσ ⊢ G1 σ −−−→ Φ′ ⊢ G2 σρ
Λ′′ ,π ′′

Γσσ ′ ⊢ G1 σσ ′ −−−−→ Φ′′ ⊢ G2 σρσ ′ ρ′

(A3)

We want to be able to derive the same transition using just one inference step,
with substitution σσ ′ . We have:
Λ,π

Γ ⊢ G1 −−→ Φ ⊢ G2
Λ1 ,π1

Γσσ ′ ⊢ G1 σσ ′ −−−−→ Φ1 ⊢ G2 σσ ′ ρ1

(A4)

36

Ivan Lanese and Ugo Montanari

First of all we have to prove that the step is allowed. The required condition is
that ∀x, y ∈ Γ.xσσ ′ = yσσ ′ ∧ x 6= y ⇒ actΛ (x) = actΛ (y). We have two cases.
If xσ = yσ then the thesis follows from the analogous condition of the first step
of derivation A3. Otherwise we can rewrite the condition as ∀x, y ∈ Γ.xσσ ′ =
yσσ ′ ∧ xσ 6= yσ ⇒ actΛ (x) = actΛ (y). Note that actΛ′ (xσ) = actΛ (x) thus we can
rewrite the condition as ∀x′ , y ′ ∈ Γσ.x′ σ ′ = y ′ σ ′ ∧ x′ 6= y ′ ⇒ actΛ′ (x′ ) = actΛ′ (y ′ )
what is the condition for the second step of derivation A3.
The main step now is to prove that σσ ′ ρ1 = σρσ ′ ρ′ . We have:
ρ = mgu({(nΛ (x))σ = (nΛ (y))σ|xσ = yσ} ∪ {xσ = yσ|xπ = yπ})
ρ′ = mgu({(nΛ′ (x))σ ′ = (nΛ′ (y))σ ′ |xσ ′ = yσ ′ } ∪ {xσ ′ = yσ ′ |xπ ′ = yπ ′ })
ρ1 = mgu({(nΛ (x))σσ ′ = (nΛ (y))σσ ′ |xσσ ′ = yσσ ′ } ∪ {xσσ ′ = yσσ ′ |xπ = yπ})
In particular we have:
1

σσ ′ ρ1 =
= σσ ′ mgu({(nΛ (x))σσ ′ = (nΛ (y))σσ ′ |xσσ ′ = yσσ ′ ∧ x 6= y}∪
2

∪ {xσσ ′ = yσσ ′ |xπ = yπ}) =
= σ mgu({(nΛ (x))σ = (nΛ (y))σ|xσσ ′ = yσσ ′ ∧ x 6= y}∪
3

∪ {xσ = yσ|xπ = yπ} ∪ eqn(σ ′ )) =
= σ mgu({(nΛ (x))σ = (nΛ (y))σ|xσ = yσ ∧ x 6= y}∪
4

∪{(nΛ (x))σ = (nΛ (y))σ|xσσ ′ = yσσ ′ ∧xσ 6= yσ}∪{xσ = yσ|xπ = yπ}∪eqn(σ ′ )) =
5

= σ mgu(eqn(ρ) ∪ {(nΛ (x))σ = (nΛ (y))σ|xσσ ′ = yσσ ′ ∧ xσ 6= yσ} ∪ eqn(σ ′ )) =
6

= σρ mgu({(nΛ (x))σρ = (nΛ (y))σρ|xσσ ′ = yσσ ′ ∧ xσ 6= yσ} ∪ eqn(σ ′ )ρ) =
7

= σρ mgu({nΛ′ (xσ) = nΛ′ (yσ)|xσσ ′ = yσσ ′ ∧ xσ 6= yσ} ∪ eqn(σ ′ ) ∪ eqn(ρ)) =
8

= σρσ ′ mgu({(nΛ′ (xσ))σ ′ = (nΛ′ (yσ))σ ′ |xσσ ′ = yσσ ′ ∧ xσ 6= yσ} ∪ eqn(ρ)σ ′ ) =
= σρσ ′ mgu({(nΛ′ (x′ ))σ ′ = (nΛ′ (y ′ ))σ ′ |x′ σ ′ = y ′ σ ′ ∧ x′ 6= y ′ }∪
9

∪ eqn(π ′ )σ ′ ∪ eqn(ρ \ π ′ )σ ′ ) =
= σρσ ′ mgu({(nΛ′ (x′ ))σ ′ = (nΛ′ (y ′ ))σ ′ |x′ σ ′ = y ′ σ ′ ∧ x′ 6= y ′ }∪
10

∪ {xσ ′ = yσ ′ |xπ ′ = yπ ′ } ∪ eqn(ρ \ π ′ )σ ′ ) =
11

= σρσ ′ ρ′ mgu(eqn(ρ \ π ′ )σ ′ ρ′ ) =

= σρσ ′ ρ′
We add some explanations for that (long) sequence of equations. Step 1 is just
the definition of ρ1 . Step 2 is allowed by Lemma 4. Step 3 is a simple mathematical
transformation. Step 4 applies the definition of ρ. Step 5 is Lemma 4 again. Step
6 creates a new ρ on the outside using idempotence, then it brings it inside using
Lemma 4 and uses idempotence again to delete it where it is not necessary. It
uses the definition of Λ′ too. Step 7 is Lemma 4 again. Steps 8 and 9 are trivial
mathematics. Step 10 is another application of Lemma 4. Finally, step 11 is justified
since the names in the domain of ρ \ π ′ are neither in the domain of σ ′ (since

Mapping Fusion and SHR into Logic Programming

37

otherwise they would be in π ′ ) nor in the domain of ρ′ (since ρ′ is computed
after having applied ρ, which is idempotent). Thus an allowed mgu is a subset of
(ρ \ π ′ )σ ′ ρ′ which can be deleted by idempotence.
Proof of Theorem 2
Let us first consider the case of two productions for communication actions.
In order to apply them we need two sequential process edges to be rewritten.
Each production needs to be synchronized with at least another one since each
node is shared by exactly two edges. Since process edges are connected only through
amoeboids we can have a synchronization only if the two actions done by process
edges are equal to two actions allowed by amoeboids. Thanks to Lemma 2, they
must be two complementary actions, i.e. an inn and an outn . Furthermore they have
to be done on the same amoeboid, that is on two names merged by the substitution
σ corresponding to the amoeboids.
Thus P can be decomposed in the form (~x)P ′ σ where P ′ = P1′ |P2′ |Q′ with P1′
and P2′ sequential processes which are translated into the rewritten edges.
We must have P1′ = · · · + u1 ~x′ .P1′′ and P2′ = u2 ~y ′ .P2′′ + . . . (or swapped) with
′
|~x | = |~y ′ |. Furthermore σ merges u1 and u2 thus we have a transition P → P ′ that
corresponds to the synchronized execution of the two prefixes.
The productions to be applied are thus forced except for the ones inside the
amoeboids, but the only difference among the choices (as shown by Lemma 2)
amounts to pseudoamoeboids and exchanges between equivalent amoeboids in the
result. From Lemma 5 we know that the result of a transition is determined up to
injective renamings (and actions on isolated nodes) by the starting graph and the
productions chosen. Thus the transition that corresponds to P → P ′ for Theorem
Λ,id
1 is equal up to injective renamings to a transition that differs from JP K~v ,w~ −−−→
Γ′ ⊢ G only for pseudoamoeboids and substitutions of equivalent amoeboids. The
thesis follows.
The other case is analogous.
Lemma 6
Let A1 , . . . , An be a goal.
We want to build a big-step where the clause unified with Ai is Hi ← Bi , if
any (some Ai may not be replaced, in that case as notation we use Bi = Ai ). As
a notational convention we use xi,1 , . . . , xi,ni to denote the arguments of Ai and
′
ai,j (x′i,j , ~yi,j
) to denote the jth argument of Hi if it is a complex term and x′i,j if it
is a variable (note that we have different names for the same variable, one for each
′
occurrence). All these are undefined if Ai is not replaced, ai,j and ~yi,j
are undefined
also if the jth argument of Hi is a variable.
Let θr be the mgu of the following set of equations:
′
′
= ~yp,q
|xi,j = xp,q } ∪ {xi,j = x′i,j |the jth argument of Hi is x′i,j }
{x′i,j = x′p,q , ~yi,j

We will denote xθr with [x].
θ

We will have a big-step of the form A1 , . . . , An ⇒ G1 , . . . , Gn iff
∀i, p ∈ {1, . . . , n}.∀j ∈ {1, . . . , ni }.∀q ∈ {1, . . . , np }.xi,j = xp,q ⇒ ai,j = ap,q .

38

Ivan Lanese and Ugo Montanari

Furthermore we have:
′
′
′ ])/x |a
yi,j
[l]∨(vk =
θ = {ai,j ([x′i,j ], [y~i,j
i,j i,j is defined}∪{[vk ]/vk |(vk = xi,j ∨vk = ~
xi,j ∧ ai,j is undefined )) ∧ [vk ] 6= vk }
G1 , . . . , Gn = (B1 , . . . , Bn )θr
′
′ ][l] = [y~
where [y~i,j
i,j [l]].
The big-step is determined (up to injective renamings) by the choice of the clauses
and of the atoms they are applied to.
Proof
We will prove a more general result by induction on the number of “considered”
atoms, that is we consider an increasing chain of derivations, and considered atoms
are the ones that, if expanded in the complete derivation, have already been expanded. For simplicity, atoms are considered in numeric order, i.e. at step m atoms
A1 , . . . , Am−1 have already been considered, and atom Am becomes considered.
θ
We will prove that a computation of the form A1 , . . . , An −
→* G1 , . . . , Gn where
we substitute only atoms in the starting goal and where the atoms generated by
considered atoms do not contain function symbols exists iff:
∀i, p ∈ {1, . . . , m}.∀j ∈ {1, . . . , ni }.∀q ∈ {1, . . . , np }.xi,j = xp,q ⇒ ai,j = ap,q and
that furthermore:
~′ ]′ )/xi,j |ai,j is defined ∧ i ≤ m} ∪ {[vk ]′ /vk |(vk = x′ ∨ vk =
• θ = {ai,j ([x′i,j ]′ , [yi,j
i,j
′
~yi,j [l] ∨ (vk = xi,j ∧ ai,j is undefined )) ∧ [vk ]′ 6= vk };
• G1 , . . . , Gn = (B1 , . . . , Bm )θr′ , (Am+1 , . . . , An )θ;
where θr′ is the mgu of the subset of eqn(θ) containing only equalities between
variables occurring in considered atoms and where [x]′ = xθr′ .
Note that if all the atoms are considered we obtain the thesis.
Base case, m = 1) We have the following transition:
θ

1
(B1 , A2 , . . . , An )θ1
A1 , . . . , An −→
where θ1 is an mgu of {A1 = H1 }. This transition exists iff θ1 exists.
We have:
′
θ1 = mgu({x1,j = a1,j (x′1,j , ~y1,j
)|a1,j is defined} ∪ {x1,j = x′1,j |a1,j is undefined}).
Note that if x1,j = x1,q ; a1,j = a1,q then the mgu does not exist (if ai,j and a1,q
are both defined, otherwise they have to be both undefined since if just one of them
is defined then a function symbol will remain in the considered part against the
hypothesis).
If the condition is satisfied we have:

′
θ1 = mgu({x1,j = a1,j (x′1,j , ~y1,j
)|a1,j is defined}∪
′
′
∪ {a1,q (x′1,q , ~y1,q
) = a1,j (x′1,j , ~y1,j
)|x1,j = x1,q } ∪ {x1,j = x′1,j |a1,j is undefined}) =
′
)|a1,j is defined}∪
= mgu({x1,j = a1,j (x′1,j , ~y1,j
′
′
∪ {x′1,q = x′1,j , ~y1,q
=~
y1,j
|x1,j = x1,q } ∪ {x1,j = x′1,j |a1,j is undefined})

Note that the last part is exactly eqn(θr′ ), thus θr′ is its mgu.
Thus we have:
′
θ1 = mgu({x1,j = a1,j (x′1,j , ~y1,j
)|a1,j is defined} ∪ {[vk ]′ = vk |[vk ]′ 6= vk }).

Mapping Fusion and SHR into Logic Programming

39

To have the real mgu we just need to apply θr′ to the equations in the first part
(note that x1,j is unified with some other variable only if a1,j is undefined thus the
domain variables of the first part are not changed).
This proves the first part since this mgu exists and the second one since it has the
wanted form.
The third part follows from the observation that θ1 |n(B1 ) = θr′ |n(B1 ) .
θg

Inductive case, m ⇒ m + 1) Assume that A1 , . . . , An −→* G1 , . . . , Gn is a logic
computation where we substitute only atoms in the starting goal, where atoms
A1 , . . . , Am+1 are considered and where the atoms generated by them do not contain
function symbols.
Let us take the subcomputation where only the first m atoms have been considered.
By inductive hypothesis we have that this part of the computation exists iff:
∀i, p ∈ {1, . . . , m}.∀j ∈ {1, . . . , ni }.∀q ∈ {1, . . . , np }.xi,j = xp,q ⇒ ai,j = ap,q
and that:
′
′ ])/x |a
• θ = {ai,j ([x′i,j ], [y~i,j
i,j i,j is defined ∧ i ≤ m} ∪ {[vk ]/vk |(vk = xi,j ∨ vk =
′
~yi,j [l] ∨ (vk = xi,j ∧ ai,j is undefined )) ∧ [vk ] 6= vk };

• G1 , . . . , Gn = (B1 , . . . , Bm )θr , (Am+1 , . . . , An )θ.
We will now consider the atom Am+1 . If it is not substituted then the thesis follows
trivially (note that Am+1 does not contain variables substituted with a complex
term by θ, since this can happen only if we have xi,j = xm+1,q with i < m + 1,
xi,j defined and xm+1,q undefined, and this is forbidden; thus we have Am+1 θ =
Am+1 θr ). Let us consider the case in which it is substituted.
We will have a small step of the form:
θ′

(G1 , . . . , Gm , Am+1 , . . . , An )θ −→ ( G1 , . . . , Gm+1 , Am+2 , . . . , An )θθ′
where θ′ = mgu({Am+1 θ = Hm+1 }) (note that we can assume that θ is also applied
to Gm+1 since we can assume dom(θ) ∩ n(Gm+1 ) = ∅).
We have:
θ′ = mgu({Am+1 θ = Hm+1 }) =
′
= mgu({xm+1,j θ = am+1,j (x′m+1,j , ~ym+1,j
)|am+1,j is defined}∪

∪ {xm+1,j θ = x′m+1,j |am+1,j is undefined})
For each binding we must consider two cases: either the variable xm+1,j appears in
already considered atoms (we call it an old variable) or it does not (we call it a new
variable). In the second case θ is the identity on that variable. In the first case if
am+1,j is defined then the mgu exists iff we have am+1,j = ap,q where ap,q is the
function symbol in the binding for xm+1,j in θ. Note that if ap,q is undefined then
also am+1,j must be undefined otherwise the function symbol remains in the final
goal.

40

Ivan Lanese and Ugo Montanari

Thus we will have:
θ′ = mgu({Am+1 θ = Hm+1 }) =
′
′
′ ]) = a
= mgu({ap,q ([x′p,q ], [y~p,q
ym+1,j
)|am+1,j is defined ∧
m+1,j (xm+1,j , ~

∧ xp,q = xm+1,j ∧ xm+1,j is old} ∪ {[xm+1,j ] = x′m+1,j |am+1,j is undefined}∪
′
∪ {xm+1,j = am+1,j (x′m+1,j , ~ym+1,j
)|am+1,j is defined ∧ xk+1,j is new} =
′
′ ]=~
= mgu({[x′p,q ] = x′m+1,j , [y~p,q
ym+1,j
|am+1,j is defined ∧

∧ xp,q = xm+1,j ∧ xm+1,j is old} ∪ {[xm+1,j ] = x′m+1,j |am+1,j is undefined}∪
′
)|am+1,j is defined ∧ xm+1,j is new}
∪ {xm+1,j = am+1,j (x′m+1,j , ~ym+1,j

where we use [−] to denote the representative of the equivalence class according to
θ. We can reorder this substitution into:
′
mgu({xm+1,j = am+1,j (x′m+1,j , ~ym+1,j
)|am+1,j is defined ∧ xm+1,j is new}∪
′
′ ]=~
ym+1,j
|ak+1,j is defined ∧
∪ {[x′p,q ] = x′m+1,j , [y~p,q

∧ xp,q = xm+1,j ∧ xm+1,j is old} ∪ {[xm+1,j ] = x′m+1,j |am+1,j is undefined}
Note that the second part is a renaming that does not involve variables in the
domain of the first part. Thus we can define new equivalence classes [−]′ according
to this substitution θr′ and put the substitution in the resolved form:
′
mgu({xm+1,j = am+1,j ([x′m+1,j ]′ , [~ym+1,j
]′ )|am+1,j is defined ∧ xm+1,j is new}∪

∪ {[vk ]′ = vk |[vk ]′ 6= vk })
Thus the mgu exists and the first part of the thesis is proved.
Let us consider the substitution θg = θθ′ . Note that the renaming part of θ′ substitutes variables according to the equivalence between variables in the Hm+1 and
representatives of the corresponding variables in Am+1 thus the composed substitution θr′′ maps each variable to the representative of the equivalence class that is
defined by the union of the two sets of equations as required. Furthermore bindings
with complex terms (the first part of the substitution) have disjoint domains and
thus the union of them is made. Bindings coming from θ′ have already the wanted
representatives in the image, while to bindings in θ the renaming is applied, mapping variables into the representatives of their equivalence classes. Thus θg has the
wanted form w.r.t. the equivalence classes determined by all the equivalences on
variables.
We have:
(G1 , . . . , Gm+1 , Am+2 , . . . , An )θg = (G1 , . . . , Gm+1 )θr′′ , (Am+2 , . . . , An )θg
as required since (dom(θg ) \ dom(θr′′ )) ∩ n(G1 , . . . , Gm+1 ) = ∅.
Note that this result does not depend on the order of application of clauses
and that after having chosen which clauses to apply and to which atoms it is
deterministic up to an injective renaming (which depends on the choice of names
for new variables and on the choice of representatives for the equivalence classes).

Mapping Fusion and SHR into Logic Programming

41

Proof of Theorem 4
The proof is by rule induction.
Axioms)
Assume we have a production:
Λ,π
x1 , . . . , xn ⊢ s(x1 , . . . , xn ) −−→ Φ ⊢ G
where:
Λ(xi ) = (ai , ~yi ) ∀i ∈ {1 . . . n}
and π : {x1 , . . . , xn } → {x1 , . . . , xn } is an idempotent substitution.
Then we have in P a clause:
s(a1 (xi π, ~y1 ), . . . , an (xn π, ~yn )) ← JΦ ⊢ GK
where we have xi π instead of ai (xi π, ~yi ) if ai = ǫ.
We can have an applicable variant of this clause for each injective renaming ρ
that maps each variable to a fresh one. Let us consider the goal:
Js(x1 , . . . , xn )K = s(x1 , . . . , xn )
It unifies with the clause variant:
s(a1 (xi π, ~y1 ), . . . , an (xn π, ~yn ))ρ ← JΦ ⊢ GKρ
with mgu θρ :
θρ = {ai (xi πρ, ~yi ρ)/xi |ai 6= ǫ} ∪ {xi πρ/xi |ai = ǫ}.
Note that θρ = θρ |n(s(x1 ,...,xn )) . We can see that θρ is associated to x1 , . . . , xn ⊢
Λ,π

s(x1 , . . . , xn ) −−→ Φ ⊢ G as required. Observe also that the result of the computation is:
T = JΦ ⊢ GKρθρ = JΦ ⊢ GKρ
because n(Gρ) ∩ dom(θρ ) = ∅. This proves the thesis. To deal with the missing
possibilities for ρ w.r.t. the theorem statement note that bindings in the last part
of θρ can also be resolved also as xi /xi πρ. In that case we have no binding for xi in
θρ . This is equivalent to defining xi ρ = xi , and this covers the missing cases for ρ.
Note finally that we used as clause the translation of the production and that we
applied it to the translation of the rewritten edge.
Rule (par))
Λ,π

Γ ⊢ G1 −−→ Φ ⊢ G2

Λ′ ,π ′

Γ′ ⊢ G′1 −−−→ Φ′ ⊢ G′2

(Γ ∪ Φ) ∩ (Γ′ ∪ Φ′ ) = ∅

Λ∪Λ′ ,π∪π ′

Γ, Γ′ ⊢ G1 |G′1 −−−−−−−→ Φ, Φ′ ⊢ G2 |G′2
By inductive hypothesis we have:
θρ

• JΓ ⊢ G1 K ⇒ T
Λ,π

where θρ is associated to Γ ⊢ G1 −−→ Φ ⊢ G2 and T = JΦ ⊢ G2 Kρ;
θρ′ ′

• JΓ′ ⊢ G′1 K ⇒ T ′

Λ′ ,π ′

where θρ′ ′ is associated to Γ′ ⊢ G′1 −−−→ Φ′ ⊢ G′2 and T ′ = JΦ′ ⊢ G′2 Kρ′ .
In both cases by inductive hypothesis we used as clauses the translations of the
productions used in the proof of the HSHR transition applied to the translations
of the edges on which the productions were applied.
Thanks to Lemma 1 we can assume that the sets of variables used in the two

42

Ivan Lanese and Ugo Montanari

computations are disjoint. Thanks to Lemma 6 we know that these big-steps exist
iff xi,j = xp,q ⇒ ai,j = ap,q . Since the used variable sets are disjoint the same
condition guarantees the existence of a big-step of the form:
θρ θρ′ ′

JΓ, Γ′ ⊢ G1 |G′1 K −−−→* T, T ′
where we used as clauses the unions of the clauses used in the two smaller computations, applied to the same predicates.
We have that θρ θρ′ ′ is associated to:
Λ∪Λ′ ,π∪π ′

Γ, Γ′ ⊢ G1 |G′1 −−−−−−−→ Φ, Φ′ ⊢ G2 |G′2 .
We also have θρ θρ′ ′ = (θθ′ )ρρ′ and thus:
T, T ′ = JΦ ⊢ G2 Kρ, JΦ′ ⊢ G′2 Kρ′ = JΦ, Φ′ ⊢ G2 |G′2 Kρρ′ as required.
Rule (merge))
Λ,π

Γ ⊢ G1 −−→ Φ ⊢ G2

∀x, y ∈ Γ.xσ = yσ ∧ x 6= y ⇒ actΛ (x) = actΛ (y)
Λ′ ,π ′

Γσ ⊢ G1 σ −−−→ Φ′ ⊢ G2 σρg
where σ : Γ → Γ is an idempotent substitution and:
(i). ρg = mgu({(nΛ (x))σ = (nΛ (y))σ|xσ = yσ} ∪ {xσ = yσ|xπ = yπ}) where ρg
maps names to representatives in Γσ whenever possible
(ii). ∀z ∈ Γ.Λ′ (zσ) = (Λ(z))σρg
(iii). π ′ = ρg |Γσ
where we used ρg instead of ρ to avoid confusion with the injective renaming ρ. For
inductive hypothesis we have:
θρ

JΓ ⊢ G1 K ⇒ T
Λ,π

where θρ is associated to Γ ⊢ G1 −−→ Φ ⊢ G2 and T = JΦ ⊢ G2 Kρ and we used as
clauses the translations of the productions used in the proof of the HSHR transition
applied to the translations of the edges on which the productions were applied.
Thanks to Lemma 6 we have that this computation exists iff:
xi,j = xp,q ⇒ ai,j = ap,q
and that:
′
′
• θr = mgu({x′i,j = x′p,q , ~yi,j
= ~yp,q
|xi,j = xp,q }∪
′
{xi,j = xi,j |the jth argument of Hi is x′i,j })
′
′
′ ])/x |a
yi,j
[l] ∨ (vk =
• θ = {ai,j ([x′i,j ], [y~i,j
i,j i,j is defined} ∪ {[vk ]/vk |(vk = xi,j ∨ vk = ~
xi,j ∧ ai,j is undefined )) ∧ [vk ] 6= vk }

• T = (B1 , . . . , Bn )θr
where JΓ ⊢ G1 K = A1 , . . . , An and we used the naming conventions defined in
Lemma 6. In particular ρ maps each variable to its primed version.
We have:
JΓ ⊢ G1 Kσ = JΓσ ⊢ G1 σK
We want to find a big-step that uses the same clauses of the previous one applied
to the same atoms, but starting from this new goal. We will use an overline to

Mapping Fusion and SHR into Logic Programming

43

denote the components of the new big-step. Thanks to Lemma 6 such a big-step
exists iff:
xi,j σ = xp,q σ ⇒ ai,j = ap,q
but if xi,j = xp,q this has already been proved, otherwise this is guaranteed by the
applicability conditions of the rule.
We have to prove that θ ρ is associated to:
Λ′ ,π ′

Γσ ⊢ G1 σ −−−→ Φ′ ⊢ G2 σρg .
From Lemma 6 we have:
~′ ]′ )/xi,j σ|ai,j is defined} ∪ {[vk ]′ /vk |(vk = x′ ∨ vk = ~y ′ [l] ∨
θρ = {ai,j ([x′i,j ]′ , [yi,j
i,j
i,j
(vk = xi,j ∧ ai,j is undefined )) ∧ [vk ]′ 6= vk }
where [−]′ maps each variable to the representative of the equivalence class given
by:
′
′
{x′i,j = x′p,q , ~yi,j
= ~yp,q
|xi,j σ = xp,q σ}∪

∪ {xi,j σ = x′i,j |the jth argument of Hi is x′i,j }
Note that xi,j σ is never unified with a primed variable unless ai,j is undefined.
Since Λ′ (xi,j σ) = (Λ(xi,j ))σρg we need to prove that θr = θr ρ−1 σρg ρ, that is
that [x′ ]′ = [y ′ ]′ iff xσρg = yσρg .
From the hypothesis and from Lemma 4 we have that σρg = mgu({nΛ (x) =
nΛ (y)|xσ = yσ} ∪ {x = y|xπ = yπ} ∪ eqn(σ)). The first and the third part are equal
(adding primes) to the equations for [−]′ . As far as the second part is concerned,
ρ maps variables merged by π to the same primed variable, thus these equations
become trivial.
Λ′ ,π ′
This proves that θρ is associated to Γσ ⊢ G1 σ −−−→ Φ′ ⊢ G2 σρg as required.
By hypothesis and using Lemma 6 we have:
JΦ ⊢ G2 Kρ = (B1 , . . . , Bn )θr
The result of the new computation is:
(B1 , . . . , Bn )θr
Thanks to the properties of ρ we have:
(B1 , . . . , Bn )θr = (B1 , . . . , Bn )θr ρ−1 σρg ρ = JΦ ⊢ G2 Kρρ−1 σρg ρ = JΦ′ ⊢ G2 σρg Kρ.
Rule (idle))
Λǫ ,id

Γ ⊢ G −−−→ Γ ⊢ G
The proof is analogous to the proof for axioms, using as clause corresponding to
the production the translation of the (idle) rule.
Rule (new))
Λ,π

Γ ⊢ G1 −−→ Φ ⊢ G2

x∈
/ Γ ~y ∩ (Γ ∪ Φ ∪ {x}) = ∅
Λ∪{(x,a,~
y)},π

Γ, x ⊢ G1 −−−−−−−−−→ Φ′ ⊢ G2
For inductive hypothesis we have in P the following big-step of Synchronized Logic
Programming:
θρ

JΓ ⊢ G1 K −→* T
where θρ is associated to:
Λ,π

Γ ⊢ G1 −−→ Φ ⊢ G2

44

Ivan Lanese and Ugo Montanari

and T = JΦ ⊢ G2 Kρ but because x ∈
/ n(G1 ) we have that θρ is also associated to:
Λ∪{(x,a,~
y)},π

Γ, x ⊢ G1 −−−−−−−−−→ Φ′ ⊢ G2
The thesis follows.
Proof of Theorem 5
The translation JΓ ⊢ GK can be written in the form A1 , . . . , An where the Ai s are
translations of single edges. We want to associate a HSHR production to each Ai .
θ
For edges associated to atoms that are rewritten in JΓ ⊢ GK ⇒ T we use an instance
of the axiom that corresponds to the clause used to rewrite it, otherwise the rule
obtained from rule (idle) applied to that edge and to nodes that are all distinct.
Let T1 , . . . , Tn be the heads of these rules. We choose the names in the following
way: for each first occurrence of a variable in A1 , . . . , An we use the same name for
the node in the corresponding position, we use new names for all other occurrences.
Note that there exists a substitution σ such that (T1 , . . . , Tn )σ = A1 , . . . , An and
that σ is idempotent. Note also that for each i all names in Ti are distinct.
For each i we can choose an instance Ri of the associated rule with head Ti such
that for each i, j, i 6= j we have n(Ri ) ∩ n(Rj ) = ∅. As notation we use:
Λi ,πi

Ri = Γi ⊢ Gi −−−→ Φi ⊢ G′i
Since all the rules have a disjoint set of names we can apply n − 1 times rule (par)
in order to have:
S
S


S
S
i Λi , i πi
−
−
−
−
−
−−→ i Φi ⊢ i G′i
Γ
⊢
G
i i
i i
Now we want to apply rule (merge) with substitution σ. We can do it since σ is
S
idempotent. We have to verify that xσ = yσ ∧ x 6= y ⇒ ( i Λi )(x) = (a, ~v ) ∧
S
~ This happens thanks to Lemma 6. Thus we obtain a rule of
( i Λi )(x) = (a, w).
the form:
Λ,π
n(A1 , . . . , An ) ⊢ A1 , . . . , An −−→ Φ ⊢ G′
Thanks to Theorem 4 we can have in P the following big-step of Synchronized Logic
Programming:
θρ′

Jn(A1 , . . . , An ) ⊢ A1 , . . . , An K ⇒ T ′
for every ρ that satisfies the freshness conditions. Furthermore θρ′ is associated to
Λ,π

n(A1 , . . . , An ) ⊢ A1 , . . . , An −−→ Φ ⊢ G′ and T ′ = JΦ ⊢ G′ Kρ. Finally we used as
clauses the translations of the productions used in the proof of the HSHR rewriting.
Note that Jn(A1 , . . . , An ) ⊢ A1 , . . . , An K = JΓ ⊢ GK. Since the result of a big-step is
determined up to injective renaming by the starting goal and the used clauses (see
Lemma 6) then we must have θ = θρ′ ρ′ and T = T ′ ρ′ for some injective renaming
ρ′ . Note that ρρ′ satisfies the freshness conditions (since variables generated in logic
′′
programming are always fresh) and we also have θ = θρρ
′.
Λ,π

Thus we have that θ is associated to Γ ⊢ G −−→ Φ ⊢ G′ and that T = T ′ ρ = JΦ ⊢
G′ Kρρ′ . This proves the thesis.

