Composed Reduction Systems

David Sands^{∗} diku, University of Copenhagen^{†}

Abstract

This paper studies composed reduction systems: a system of programs built up from the reduction relations of some reduction system, by means of parallel and sequential composition operators. The trace-based compositional semantics of composed reduction systems is considered, and a new graph-representation is introduced as an alternative basis for the study of compositional semantics, refinement, true concurrency (in the case of composed rewriting systems) and program logics.

1 Introduction

Reduction systems are simply sets equipped with some collection of binary “rewrite” relations. A reduction systems can be thought of as an abstract view of computation, embodying the fundamental computational concepts of iteration, termination, and nontermination. Computation is the process of repeatedly rewriting, beginning with some object of the set, and termination corresponds to obtaining an object which cannot be rewritten further; nontermination is the ability to rewrite indefinitely.

Since reduction systems have little structure, there are relatively few properties one can state about theses systems, although unique-termination (“Church-Rosser”) properties of reduction systems have been studied by eg. Rosen [Ros73], Hindley [Hin69] Staples [Sta74].

In this paper we consider systems (“programs”) whose basic components are the reduction relations of some reduction system. These systems, which we call composed reduction systems, are built by composing reduction relations with two natural composition operators: parallel and sequential composition. Composed reduction systems are not necessarily reduction systems, but they possess a notion of a “reduction step”, and a corresponding notion of termination.

• Parallel composition allows arbitrary interleaving of reduction steps. In the simplest case, the parallel composition of two reduction relations corresponds to the union of these relations. Parallel composition terminates when, simultaneously, both sub-systems have terminated.

∗This work was partially funded by ESPRIT BRA 9102, “Coordination”

†Universitetsparken 1, 2100 København Ø, DENMARK. e-mail: dave@diku.dk

• Sequential composition, on the other hand, takes us outside the realm of reduction systems (over the given set). The sequential composition of two reduction relations is the system which behaves like the first reduction relation, until termination of the first system, after which it behaves like the second system. The sequentially composed system is said to terminate when the second sub-system has terminated.

Note, then, that the sequential composition of two reduction relations (the simplest case) is not the relational composition of these relations. Composed reduction systems over a given reduction system are built from arbitrary sequential and parallel compositions of reduction relations.

In this paper we study the semantics of composed reduction systems, expressed in terms of its constituent reduction relations. We focus on a comparison relation for programs which partially orders programs on the basis of their “input-output” behaviours, and is also a precongruence with respect to program construction.

In the first part of the paper (Section 2) we consider a standard compositional semantics based on ”reactive traces” (sequences of object-pairs) derived from the SOS-like rules which give the operational semantics for composed reduction systems. We outline some of the program laws that can be obtained, and consider the relationship to an alternative form of parallel composition.

In the second part of the paper (Section 3), we define a static graph representation for programs, and argue that it forms a better basis (than the transition traces) for the study of:

• compositional semantics, since it is higher-level than the transition traces;

• refinement laws, since the graphs can also be defined compositionally;

• concurrency, since “concurrently active” reduction relations are explicit in the representation, and

• program logics, since logics for the underlying reduction systems can be used to reasoning about paths through the graph.

Related Work and Applications This work grew out of the study of composition of specific kind of reduction system, namely programs in the Gamma model [BM93], which can be thought of as conditional associative-commutative string rewriting. The composition operators for Gamma were introduced in [HMS92], and the compositional semantics and laws were studied in [San93a][San93b]. The development of section 2 is a direct (and straightforward) adaptation of [San93a][San93b] to this more general setting. The graph representation in section 3 is new, and is particularly relevant from the point of view of composed Gamma programs. ^{1}

The techniques given here may also be interesting when applied to other concrete reduction systems. In particular we have in mind rewriting systems in which the objects rewritten have some structure (eg. trees, graphs, strings), and the reduction relation is specified by rules for rewriting a substructure, in terms of purely local conditions. For such systems (eg. the usual notion of term rewriting [Klo92] [DJ89]) there is a natural (implicit) notion of concurrency, viz. disjoint parts of a substructure can be rewritten asynchronously, and hence concurrently. This view of rewriting as a natural vehicle for concurrency and parallel programming is central to Meseguer’s approach [Mes92][MW91]; the composition operators studied here also make sense in that setting.

1For example, through this representation have discovered additional laws for Gamma programs.

Another form of reduction system, where one could reasonably employ the composition operators studied here, is the guarded iteration statement from [Dij76], also known as action systems [Bac89a][Bac89b]. Action systems are nondeterministic do-od programs consisting of a collection of guarded atomic actions, which are executed nondeterministicly so long as some guard remains true. In their uninitialised form, guarded iteration statements can be thought of as reduction systems over program states. The method of parallel execution is to allow actions involving disjoint program variables to be executed in parallel, which is consistent with the rewriting viewpoint above. In [Bac89b] Back studies compositional notions of refinement for action systems with respect to a metalinguistic parallel composition operator. ^{2} The parallel composition studied here is strictly more general since it permits parallel composition of sequentially composed systems.

2 Operational and Compositional Semantics

In this section we give the operational semantics of composed reduction systems built from basic reduction relations, parallel and sequential composition.

In what follows, we assume some reduction system ⟨U, {→_{r}}_{r∈R}⟩, where U is a set, with typical elements M, N, M_{1} . . .. We will sometimes refer to the elements of U as states. The reduction relations, {→_{r}}_{r∈R} are just binary relations on states.We will think of the elements of the indexing set R, ranged over by r, r_{2} …, as the basic units of our composed reduction systems. Somewhat improperly, for more concrete examples we will think of R as the set of representations of the corresponding reduction relation.

With respect to some r, we say that

• M reduces to N if M→_{r}N (ie. (M, N) ∈ →_{r});

• M converges immediately, written M↓^{r}, if ¬∃N. M→_{r}N.

For the moment we consider composed reduction systems, ranged over by P, Q, P_{1}, Q_{1} etc, given by the following grammar:

P ::= r | P ; Q | P ∥ − Q

Henceforth we will use the terms “composed reduction system” and “program” synonymously.

2UNITY [CM88] has a similar composition operator, called union, but UNITY is not a reduction system in the same sense because the notion of termination for UNITY is that of stability—reaching a fixed-point—rather than inactivity.

2.1 SOS semantics

Because of the presence of sequential composition, programs cannot be viewed as reduction systems over U, since the program is not a static entity. To define the semantics for these programs we define a single step transition relation between configurations. The configurations are program-state pairs, written ⟨P, M⟩. The final result of a computation is given by an immediate-convergence predicate, ↓, on configurations. Single step reduction and immediate-convergence is given by SOS-style rules in figure 1. It is easily verified that immediate con-

\begin{matrix}\frac{M→_{r}N}{⟨r, M⟩ → ⟨r, N⟩} & \frac{M↓^{r}}{⟨r, M⟩↓} \\ \frac{⟨P, M⟩ → ⟨P′, M′⟩}{⟨P ; Q, M⟩ → ⟨P ; Q, M′⟩} & \frac{⟨P, M⟩↓}{⟨P ; Q, M⟩ → ⟨Q, M⟩} \\ \frac{⟨P, M⟩ → ⟨P′, M′⟩}{⟨P ∥ − Q, M⟩ → ⟨P′ ∥ − Q, M′⟩} & \frac{⟨Q, M⟩ → ⟨Q′, M′⟩}{⟨P ∥ − Q, M⟩ → ⟨P ∥ − Q′, M′⟩} & \frac{⟨P, M⟩↓ ⟨Q, M⟩↓}{⟨P ∥ − Q, M⟩↓} \end{matrix}

Figure 1: Structural Operational Semantics of composed reduction systems

vergence of a configuration corresponds to the absence of any transitions for that configuration. In other words, ⟨P, M⟩ → ⟨Q, N⟩ for some ⟨Q, N⟩ if and only if ¬(⟨P, M⟩↓).

Let →^{∗} denote the transitive, reflexive closure of →. By a small abuse of the notation, we will write ⟨P, M⟩ →^{∗} N to mean that there exists some ⟨Q, N⟩ such that ⟨P, M⟩ →^{∗} ⟨Q, N⟩ and ⟨Q, N⟩↓.

2.2 Behavioural orderings

In this paper we will focus on the relational (input-output) behaviours of a program. A number of “refinement” orderings on programs arise from the various natural ways to compare programs on the basis of their input-output (or relational) behaviour. One possible “behaviour” which we should consider significant is the possibility of nontermination for a given input. Non-termination, or “divergence” is a predicate on program configurations:

Definition 1 P may diverge on M, ⟨P, M⟩↑, if there exist {⟨P_{i}, M_{i}⟩}_{i∈ω} such that ⟨P_{0}, M_{0}⟩ = ⟨P, M⟩ and ⟨P_{i}, M_{i}⟩ → ⟨P_{i+1}, M_{i+1}⟩.

It is convenient to abstract the possible relational behaviours of a program as a set of possible input-output pairs. This includes the possibility of nontermination, which we represent as a possible “output” using symbol ‘⊥’ (∉ U):

Definition 2 The behaviours of a program P are given by

\begin{aligned}B(P) & = & \{(M, N) | ⟨P, M⟩ →^{∗} N\} \\ & ∪ & \{(M, ⊥) | ⟨P, M⟩↑\} \end{aligned}

Note that for every P, M, either (M, N) ∈ B(P) for some N, or (M, ⊥) ∈ B(P) (or both). There are a variety of orderings on programs obtained by comparing their behaviours: the partial correctness ordering ignores divergent behaviours; the lower and upper orderings are formed by considering the associated discrete power-domain orderings on U_{⊥}. In this study we only consider the strong correctness ordering, which attaches the same significance to nonterminating computations as to the terminating ones. The strong correctness ordering is defined to be the largest (pre)congruence which satisfies

P ⊑_{o} Q ⇒ B(P) ⊆ B(Q)

This is given directly by the following:

Definition 3 Let C range over program contexts. We define strong precongruence (⊑_{o}) and strong congruence(≡_{o}) respectively by:

\begin{aligned}P ⊑_{o} Q & ⟺ & ∀C. B(C[P]) ⊆ B(C[Q]) \\ P ≡_{o} Q & ⟺ & P ⊑_{o} Q & Q ⊑_{o} P \end{aligned}

2.3 Laws

In this section we present a number of the basic laws of strong precongruence, and show the relationship to an alternative definition of parallel composition. Let Δ denote the empty reduction relation, satisfying ∀M. M↓^{Δ}. For example, in conditional rewriting systems, this could be represented by a reduction rule with the condition false.

Proposition 4

\begin{matrix}1. & P ; (Q ; R) ≡_{o} (P ; Q) ; R & 5. & Δ ∥ − P ≡_{o} P ∥ − Δ ≡_{o} P \\ 2. & P ∥ − (Q ∥ − R) ≡_{o} (P ∥ − Q) ∥ − R & 6. & P ⊑_{o} P ; Δ \\ 3. & P ∥ − Q ≡_{o} Q ∥ − P & 7. & P ≡_{o} Δ ; P \\ 4. & Q ; (P_{1} ∥ − P_{2}) ⊑_{o} (Q ; P_{1}) ∥ − P_{2} & 8. & P ⊑_{o} P ∥ − P \end{matrix}

These are just a few of the laws of strong precongruence. In fact, almost all of the partial correctness laws of composed Gamma programs [San93b] hold for these more general composed reduction systems. Note in particular that law 6 cannot be strengthened to an equality, ie.

P ; Δ ≢_{o} P

The intuition for this is that Δ acts as a de-synchroniser for parallel composition: P must synchronise with its context in order to terminate, but with P ; Δ, P is allowed to terminate autonomously, leaving Δ to synchronise with its context—which it is trivially always able to do. As an example consider the following two term rewrite rules, where a and b are constants: a → b and b → a. It is easily seen that ⟨(a → b) ∥ − (b → a), a⟩ can never terminate, but

⟨(P_{1} ; Δ) ∥ − P_{2}, a⟩ →^{∗} a

and so (P_{1} ; Δ) ∥ − P_{2} ⋢_{o} P_{1} ∥ − P_{2}.

An Alternative Parallel Composition

There is a natural alternative form of parallel program composition, which does not require that the two programs terminate synchronously. Extend the syntax of the language with P ::= P_{1} ∥ P_{2}, and add the operational rules:

\frac{⟨Q, M⟩↓}{⟨P ∥ Q, M⟩ → ⟨P, M⟩} \frac{⟨P, M⟩↓}{⟨P ∥ Q, M⟩ → ⟨Q, M⟩}

The expected associativity and commutativity properties also hold for ∥. Some relationships with ; and ∥ − can be summarised in the diagram in figure 2, where the arrows (→) depict the ordering ⊑_{o}. To give some intuition to the fact in

\begin{matrix}(P ; Δ) ∥ − (Q ; Δ) ≡_{o} (P ; Δ) ∥ (Q ; Δ) \\ ↑ \\ P ∥ Q \\ ↗ ↖ \\ \begin{matrix}(P ; Δ) & ∥ − & Q \\ ↗ & & ↖ \end{matrix} & \begin{matrix}P & ∥ − & (Q ; Δ) \\ ↗ & & ↖ \end{matrix} \\ P ; Q  P ∥ − Q  Q ; P \end{matrix}

Figure 2: Relationships between Compositions

this diagram, consider the increasing chain of “behaviours”:

P ; Q ⊑_{o} (P ; Δ) ∥ − Q ⊑_{o} P ∥ Q ⊑_{o} (P ; Δ) ∥ − (Q ; Δ)

For P ∥ Q to terminate, either P (or some derivative thereof) terminates followed by Q, or vice-versa, and either P or Q is left to synchronise its termination with the context. The system (P ; Δ) ∥ − Q has fewer behaviours because although reductions from P are potentially concurrent with reductions from Q, P must always terminate first. (P ; Δ) ∥ − (Q ; Δ), on the other hand, exhibits more behaviours since P and Q are “concurrent”, can terminate autonomously, and neither of them is required to synchronise its termination with the context.

2.4 Trace Semantics

We can characterise ⊑_{o} (in order to prove the laws of the previous section) by finding a compositional semantics which is consistent (ie. sound) with respect to the behaviours. Clearly the behaviours of a program will not suffice as its denotation. As is well-known from the study state-based concurrency, it insufficient to use sequences of states as a means of distinguishing programs. The solution we adopt follows a simple approach to modelling shared-state (interleaving) concurrency via sequences of state-pairs^{3} (eg. sequences of “moves”[Abr79]; “abstract paths” of [Par79]). Following the terminology of [Bro93], we will use the term transition traces, or simply traces to refer to this kind of sequence. In these models, a pair of states in the trace of a program represents an atomic computation step of the program; adjacent pairs in any given sequence model a possible interference by some other process executing in parallel with the program.

3The set of all such sequences for a program can be thought of as an “unraveling” of the program’s resumption semantics [Plo76][HP79]. This “unraveling” leads to a mathematically simpler domain (no powerdomains) which is more amenable to further refinements than resumptions.

The transition traces have a straightforward operational specification:

Definition 5 The transition traces of a program, T[[P]], are the finite and infinite sequences of state-pairs, given by:

T[[P]] = \begin{cases}(M_{0}, N_{0})(M_{1}, N_{1}) … (M_{k}, N_{k})| \\ ⟨P, M_{0}⟩ → ⟨P_{1}, N_{0}⟩ & \\ ⟨P_{1}, M_{1}⟩ → ⟨P_{2}, N_{1}⟩ & … & ⟨P_{k}, M_{k}⟩↓, & M_{k} = N_{k}\} \end{cases}

∪

\begin{cases}(M_{0}, N_{0})(M_{1}, N_{1}) … (M_{i}, N_{i}) … | \\ ⟨P, M_{0}⟩ → ⟨P_{1}, N_{0}⟩ & ⟨P_{i}, M_{i}⟩ → ⟨P_{i+1}, N_{i}⟩, i ≥ 1\} \end{cases}

The intuition behind the use of transition traces is that each transition trace

(M_{0}, N_{0})(M_{1}, N_{1}) … ∈ T[[P]]

represents computation steps of program P in some context; starting with state M_{0}, each of the pairs (M_{i}, N_{i}) represents computation steps performed by (derivatives of) P and the adjacent states N_{i−1}, M_{i} represent possible interfering computation steps performed by the “context”. If the trace is finite then the last step corresponds to the termination “step” for a derivative of P.

Stuttering

Clearly the behaviours of a program are obtainable from its transition traces, by considering the “chained” traces of the form: (M_{0}, M_{1})(M_{1}, M_{2}) . . .. Transition traces are adequate for giving a compositional semantics to composed reduction systems, by interpreting sequential composition as (set-wise) trace concatenation, and parallel composition as interleaving (with the proviso that interleaved finite traces must agree on their last elements).

However, the transition traces distinguish between programs which compute at different “speeds”. For example, considering the empty action system DO OD, then the transition traces of DO OD are different from those of (DO OD) ; (DO OD) ^{4} The key to obtaining a better level of abstraction is to equate processes which only vary by “uninteresting” steps. This is the “stuttering equivalence” well-known from Lamport’s work on temporal logics for concurrent systems [Lam89]. Closure under stuttering equivalence has been used by de Boer et al [dBKPR91], and by Brookes [Bro93] to provide fully abstract semantics for languages with shared-state and parallel composition.

Following Brookes [Bro93] we define a closure operation for sets of transition traces:

4In order to obtain full abstraction for a while-language with parallel composition, Hennessy and Plotkin added a co-routine command, which is able to distinguish these programs.

Definition 6 Let ϵ denote the empty sequence. Let α range over finite sequences of state pairs, and β range over finite or infinite sequences. A set T of finite and infinite traces is closed under left-stuttering^{5} and absorption if it satisfies the following two conditions

left-stuttering \frac{αβ ∈ T, β ≠ ϵ}{α(M, M)β ∈ T}  absorption \frac{α(M, N)(N, M′)β ∈ T}{α(M, M′)β ∈ T}

Let ‡T denote the left-stuttering and absorption closure (henceforth just closure) of a set T.

In [dBKPR91] a slightly different closure operation is used, in which only stuttered steps can be absorbed. With respect to the above closure conditions, the difference is that in the clause for absorption we should also require that either M = N or N = M′. This leads to a coarser abstraction for specific reduction systems; for example, the composed string-rewriting systems: (1, 1 → 2, 2) ∥ − (1 → 2) and (1 → 2) have different traces under the stuttering-closure operation of [dBKPR91], but are the same under ‡.

Clearly the behaviours are also derivable from ‡T[[P]], and what is more, ‡T[[P]] can be specified compositionally (using monotonic operators) which gives the following:

Proposition 7 ‡T[[P]] ⊆ ‡T[[Q]] ⟹ P ⊑_{o} Q

In the appendix we give the compositional definition of transition traces.

For a specific collection of reduction relations over some given universe, the transition traces may not be fully abstract. In other words, we cannot reverse the implication in the above proposition. For a specific example where full abstraction fails, see [San93a]. Even if we allow all reduction relations over a given universe it is unclear as to whether the transition traces are fully abstract.

3 Graph Representation

In this section we outline a static graph-representation for composed reduction systems, and argue that it forms a better basis for the study of compositional semantics, refinement, true concurrency and program logics.

The graph representation we will develop is something like a finite, acyclic control-flow graph, where each node corresponds to a simple form of loop. A node carries a set of reduction relations which are (con)currently active; an edge represents an internal termination step, where the child node may inherit some reductions from the parent but adds some new active reductions. From the viewpoint of the observational semantics, we will identify the graph with its set of complete paths.

The idea is best illustrated with an example. Consider a program consisting of four reduction relations:

(r_{1} ; r_{2}) ∥ − (r_{3} ; r_{4})

5Notice that we say left-stuttering to reflect that the context is not permitted to change the state after the termination of the program. In this way each transition trace of a program only charts interactions with its context up to the point of the programs termination.

Initially r_{1} and r_{3} are active and thereby able to contribute to the reduction steps. At some time, r_{1} or r_{3} may be able to terminate. Suppose r_{1} terminates first; then r_{2} and r_{3} become active. Symmetrically, if r_{3} terminates first then r_{1} and r_{4} become active. Continuing in this way we construct the graph for this program:

{r_{1}, r_{3}}
{r_{3}} ↙  ↘^{{r_{1}}}
{r_{1}, r_{4}}  {r_{2}, r_{3}}
{r_{1}} ↘  ↙_{{r_{3}}}
{r_{2}, r_{4}}

The operational semantics of such graphs should be transparent: control begins at the root-node of the graph, and each node is labeled with a set of concurrently active reduction-relations; each arc is labeled with a set of reduction relations which must converge with respect to the current state for the control to be allowed move along that edge.

3.1 From SOS rules to Graph Representation

The graph representation will be constructed from two “abstract interpretations” of the one-step evaluation relation. Consider any possible one-step reduction on configurations:

⟨P, M⟩ → ⟨P′, M′⟩

From inspection of the rules it is clear that either:

1. P ≠ P′ and M = M′, or

2. P = P′ and M→_{r}M′ for some reduction r in P.

In the terminology of [HMS92], we call a transition of the first kind as a passive step, and one of the second kind as an active step. The passive step corresponds to some internal termination step in which the left-operand of a sequential composition is discarded. The convergence of a configuration can similarly be considered to be a passive step. An active step corresponds to a reduction step on the state-component of a configuration.

We construct the graph representation of a given program by separately abstracting:

1. the passive steps, which will give us the arcs in the graph, and

2. the active steps which will tell us what reductions are contained in the nodes.

Abstract Passive Steps We abstract the passive steps performable by a program via a (labeled) transition system with judgements of the form P ⇝^{R} Q, where R is a set of reductions. As an auxiliary, we define a notion of convergence for programs which is an abstraction of the convergence predicate for configurations. The abstract convergence predicate is trivial: a program can converge only if it does not contain any sequential compositions. Let [P] denote the set of reduction relations that comprise the program P. Figure 3 defines the rules, closely following the form of the rules of figure 1.

\overline{r↓} ; \frac{P ⇝^{R} P′}{P ; Q ⇝^{R} P′ ; Q} \frac{P ↓}{P ; Q ⇝^{[P]} Q} ; \frac{P ⇝^{R} P′}{P ∥ − Q ⇝^{R} P′ ∥ − Q} \frac{Q ⇝^{R} Q′}{P ∥ − Q ⇝^{R} P ∥ − Q′} \frac{P ↓ Q↓}{P ∥ − Q↓}

Figure 3: Abstract Passive Steps

Active Region We abstract the active steps of a program simply by saying which reductions in the program are immediately applicable. The immediatelyapplicable reductions are just those which are not “guarded” by a sequential composition on their left. The active region of a program P, written ⌈P ⌉, is defined inductively by:

\begin{aligned}⌈r⌉ & = & \{r\} \\ ⌈P ; Q⌉ & = & ⌈P ⌉ \\ ⌈P ∥ − Q⌉ & = & ⌈P ⌉ ∪ ⌈Q⌉ \end{aligned}

The following proposition states the precise relationship between the above abstractions and the transition relation of the structural operational semantics:

Proposition 8 For all composed reduction systems P over some universe U, and for all M, N ∈ U,

⟨P, M⟩ → ⟨Q, N⟩ if and only if either

1. M = N and P ⇝^{R} Q for some R such that for all r ∈ R, M↓^{r}, or

2. P = Q, and there exits some r ∈ ⌈P ⌉ such that M→_{r}N.

The graph form will be constructed by combining the passive steps with the active regions. We note the following facts about the passive steps.

• Passive steps are normalising: ie. there are no infinite chains of the form P ⇝^{R_{1}} P_{1} ⇝^{R_{2}} P_{2} ⇝^{R_{3}} ⋯, since the size of the programs are strictly decreasing with each passive step.

• For any P, the number of R and Q such that P ⇝^{R} Q is finite.

In fact, ⇝ satisfies a “strong diamond property”, namely that if P ⇝^{R_{1}} P_{1} and P ⇝^{R_{2}} P_{2} with P_{1} ≠ P_{2}, then there is a Q such that P_{1} ⇝^{R_{2}} Q and P_{2} ⇝^{R_{1}} Q.

The graph form of a program P is rooted directed finite acyclic graph formed by (i) forming the passive-graph according to the ⇝ relation, and then (ii) mapping the function ⌈ ⌉ over the nodes of the passive-graph to extract their active reductions. So, for example, taking the program (r_{1} ; r_{2}) ∥ − (r_{3} ; r_{4}) we (i) construct the passive graph:

(r_{1} ; r_{2}) ∥ − (r_{3} ; r_{4})
{r_{3}} ↙  ↘^{{r_{1}}}
(r_{1} ; r_{2}) ∥ − r_{4}  r_{2} ∥ − (r_{3} ; r_{4})
{r_{1}} ↘  ↙_{{r_{3}}}
r_{2} ∥ − r_{4}

and (ii) abstract the active region from each node to obtain:

{r_{1}, r_{3}}
{r_{3}} ↙  ↘^{{r_{1}}}
{r_{1}, r_{4}}  {r_{2}, r_{3}}
{r_{1}} ↘  ↙_{{r_{3}}}
{r_{2}, r_{4}}

3.2 Reasoning from Graphs

It should be clear from Proposition 8 that the transition traces of a program can be constructed from its graph. In fact, from the point of view of giving the operational semantics a program P, we can use the tree corresponding to the graph.

We will show how the graph representation can be used to reason about strong equivalence and strong approximation between programs. For the purpose of the behaviours (or transition traces) of programs, only need the set of complete paths through the graph.

Let paths(P) denote the complete (and necessarily finite) paths in the

graph of P. So the graph of a program r_{1} ; (r_{2} ∥ − r_{3}) is just {r_{1}} ⟶^{{r_{1}}} {r_{2}, r_{3}}, and so the program has just a single path, ⟨{r_{1}} {r_{1}} {r_{2}, r_{3}}⟩

The domain of paths (ranged over by p_{1}, p_{2} etc.) are the finite, nonempty odd-length sequences of sets of reduction relations. Writing concatenation of sequences by juxtaposition, if R, R_{1}, R_{2} etc. range over sets of reduction relations, then a path is either a sequence of length one, ⟨R⟩, or a sequence of the form ⟨R_{1}, R_{2}⟩p for some path p. Alternatively we will denote a path by ⟨n_{1}a_{1}n_{2}a_{2} … a_{k−1}n_{k}⟩ where the n_{i} (nodes) and a_{i} (arcs) are again sets of reduction relations.

The paths of a composed reduction system can be defined directly by induction on the passive steps:

Definition 9 The paths of a program P, paths(P), is the least set of nonempty sequences of sets of reduction relations, such that:

• if P ↓ then [P] ∈ paths(P)

• if P ⇝^{R} P′ and p′ ∈ paths(P′) then ⟨⌈P ⌉, R⟩p′ ∈ paths(P).

Now, in turn, the transition traces of a program can be defined in terms of its paths. This is given in the appendix.

The first implication of this is that if two programs have equivalent paths, then they must be strongly equivalent. We conjecture a tighter relationship, namely:

Conjecture 10 paths(P_{1}) = paths(P_{2}) if and only if (P_{1} ≡_{o} P_{2}) is provable from the equational theory generated by the laws:

(i) r ≡_{o} r ∥ − r (ii) ∥ − is associative and commutative (iii) ; is associative.

In fact, other than a few laws for the desynchroniser Δ, we have not found any other strong equivalences (than those derivable from the above). The inequational theory for ⊑_{o} is, however, much richer. But proving inequalities from the transition traces (so far the only method we have) is rather tedious. Now we consider how to reason about ⊑_{o} by building comparison relations on path-sets.

3.3 Path Comparisons

Each “node” represent the possible reductions possible at that node. The reductions on each “edge” represent the termination condition—a set of reductions which must be inapplicable for control to transfer along that edge. Comparing two paths of the same length, one path describes a broader range of behaviours than another, if it has at least as many reductions at each corresponding node (the odd elements of the sequence) but no more reductions on each edge (the even elements of the sequence). This leads to the following:

Definition 11 (Path Inclusion) Two paths of equal length,

p = ⟨n_{1}, a_{1}, n_{2} … a_{k−1}, n_{k}⟩ and p′ = ⟨n′_{1}, a′_{1}, n′_{2} … a′_{k−1}, n′_{k}⟩, are in the path-inclusion ordering, written p ≤ p′, if

1. n_{k} = n′_{k},

2. n_{i} ⊆ n′_{i}, for all i < k, and

3. a′_{i} ⊆ a_{i}, for all i ≤ k.

The path inclusion ordering is defined on composed reduction systems as:

P ≤ Q if and only if for all p ∈ paths(P) there exists a path q ∈ paths(Q) such that p ≤ q.

Note that there is a stronger condition on the last node of a path. This is because the last node carries additional significance, since it is also a termination condition.

Proposition 12 P ≤ Q ⇒ P ⊑_{o} Q proof Since the transition traces are easily constructed from the paths, the proposition can be proved by showing that if P ≤ Q then the transition traces of P are contained in those of Q. Given the fact that the behaviours are extractable from the paths, a more direct (and arguably more useful) proof can be given by a compositional definition of the paths of a program. A compositional construction of paths is given in the appendix. □ Consider, for example, the composed reduction system r_{1} ; r_{3} ; (r_{2} ∥ − r_{4}):

paths(r_{1} ; r_{3} ; (r_{2} ∥ − r_{4})) = {⟨{r_{1}} , {r_{1}} {r_{3}} {r_{3}} {r_{2}, r_{4}}⟩} .

Since we have ⟨{r_{1}, r_{3}} , {r_{1}} {r_{2}, r_{3}} {r_{3}} {r_{2}, r_{4}}⟩ ∈ paths((r_{1} ; r_{2}) ∥ − (r_{3} ; r_{4})) then we can conclude that r_{1} ; r_{3} ; (r_{2} ∥ − r_{4}) ⊑_{o} (r_{1} ; r_{2}) ∥ − (r_{3} ; r_{4}).

Path Stuttering

The main limitation of the path-inclusion ordering is that we can only compare paths of equal length. So, for example, we cannot prove the inequaility:

(r_{1} ∥ − r_{3}) ; (r_{2} ∥ − r_{4}) ⊑_{o} (r_{1} ; r_{2}) ∥ − (r_{3} ; r_{4})

since the path of (r_{1} ∥ − r_{3}) ; (r_{2} ∥ − r_{4}) (there is only one) is shorter than all the paths of (r_{1} ; r_{2}) ∥ − (r_{3} ; r_{4}).

The solution is to define an analogue of closure under stuttering, at the level of paths. We do not literally add stuttering paths, but rather, paths which give rise to stuttering. Consider a path of the form p_{1}⟨n, a⟩p_{2}. The arc a represents an internal termination step. Operationally, after this step is performed, we could offer some reductions from a, say n′, and none will be applicable—and hence we can converge for all reductions in n′. Hence the path p_{1}⟨n, a, n′, n′⟩p_{2} describes no more (but no fewer) behaviours than p_{1}⟨n, a⟩p_{2}. This leads us to a definition of path stuttering equivalence

Definition 13 Let path stuttering equivalence, =_{s}, be the least equivalence relation on paths such that

for all paths p_{1}, p_{2} (p_{1} possibly empty), and for all sets of reductions n, a, n′ such that n′ ⊆ a ⊆ n,

p_{1}⟨n, a⟩p_{2} =_{s} p_{1}⟨n, a, n′, n′⟩p_{2}

For example, ⟨{r_{1}, r_{2}} {r_{1}, r_{2}} {r_{3}}⟩ =_{s} ⟨{r_{1}, r_{2}} {r_{1}, r_{2}} {r_{1}} {r_{1}} {r_{3}}⟩. With the development that follows, we will be able to conclude that

(r_{1} ∥ − r_{2}) ; r_{3} ≡_{o} (r_{1} ∥ − r_{2}) ; r_{1} ; r_{3}

Now we use path stuttering equivalence to coarsen the path inclusion ordering. As before we define a preorder on paths, and extend this to programs in the obvious way:

Definition 14 (Stuttered Path Inclusion) Two paths, p and p′, are in the stuttered path-inclusion ordering, written p ≤_{s} p′ if there exists p_{1}, p_{2} such that

p =_{s} p_{1} ≤ p_{2} =_{s} p′.

On composed reduction systems we define P ≤_{s} Q if and only if for all p ∈ paths(P) there exists a path q ∈ paths(Q) such that p ≤_{s} q.

Proposition 15 P ≤_{s} Q ⇒ P ⊑_{o} Q

proof (Outline) It is sufficient to show that P ≤_{s} Q ⇒ ‡T[[P]] ⊆ ‡T[[Q]]. The main step is to show that the closed (‡) traces corresponding to a path p_{1}⟨n, a⟩p_{2} are equal to the closed traces of p_{1}⟨n, a, n′, n′⟩p_{2}, whenever n′ ⊆ a ⊆ n. We omit the details. □

References

[Abr79] K. Abrahamson. Modal logic of concurrent nondeterministic programs. In Proceedings of the International Symposium on Semantics of Concurrent Computation, volume 70, pages 21–33. Springer-Verlag, 1979.

[Bac89a] R. Back. A method for refining atomicity in parallel algorithms. In PARLE ’89, volume II, number 365 in LNCS. Springer-Verlag, 1989.

[Bac89b] R. Back. Refinement calculus, part ii: Parallel and reactive programs. In Stepwise Refinement of Distributed Systems: Models, Formalisms, Correctness, number 430 in LNCS. Springer-Verlag, 1989.

[BM92] J.-P. Banâtre and D. Le Métayer, editors. Research Directions in High-level Parallel Programming Languages. Springer-Verlag, LNCS 574, 1992.

[BM93] J.-P. Banâtre and D. Le Métayer. Programming by multiset transformation. CACM, January 1993. (INRIA research report 1205, April 1990).

[Bro93] S. Brookes. Full abstraction for a shared variable parallel language. In Logic In Computer Science (LICS). IEEE, 1993.

[CM88] K. M. Chandy and J. Misra. Parallel Program Design: A Foundation. Addison-Wesley, 1988.

[dBKPR91] F. S. de Boer, J. N. Kok, C. Palamidessi, and J. J. M. M. Rutten. The failure of failures in a paradigm for asynchronous communication. In CONCUR ’91, number 527 in Lecture Notes in Computer Science, pages 111–126. Springer-Verlag, 1991.

[Dij76] E. Dijkstra. A Discipline of Programming. Prentice-Hall, 1976.

[DJ89] N. Dershowitz and J-P. Jouannaud. Rewrite Systems, volume B, chapter 15. North-Holland, 1989.

[Hin69] R. Hindley. An abstract form of the Church-Rosser theorem. J. Symbolic Logic, 34(1), 1969.

[HMS92] C. Hankin, D. Le Métayer, and D. Sands. A calculus of Gamma programs. Research Report DOC 92/22 (28 pages), Department of Computing, Imperial College, 1992. (short version to appear in the Proceedings of the Fifth Annual Workshop on Languages and Compilers for Parallelism, Aug 1992, Springer-Verlag).

[HP79] M. Hennessy and G. D. Plotkin. Full abstraction for a simple parallel programming lanuage. In Mathematical Foundations of Computer Science, volume 74 of LNCS, pages 108–120. Springer-Verlag, 1979.

[Klo92] J. Klop. Term rewriting systems. In S. Abramsky, D. Gabbay, and T. Maibaum, editors, Handbook of Logic in Computer Science, volume II. OUP, 1992.

[Lam89] L. Lamport. A simple approach to specifying concurrent systems. C. ACM, 31(1):32–45, January 1989.

[Mes92] J. Meseguer. Conditional rewriting logic as a unified model of concurrency. TCS, 94, 1992.

[MW91] J. Meseguer and T. Winkler. Parallel programming in maude. In In [BM92], 1991.

[Par79] D. Park. On the semantics of fair parallelism. In Abstract Software Specifications (1979 Copenhagen Winter School Proceedings), number 86 in Lecture Notes in Computer Science, pages 504–526. Springer-Verlag, 1979.

[Plo76] G. D. Plotkin. A powerdomain construction. Siam J. Comput., 5(3):452–487, September 1976.

[Ros73] B. Rosen. Tree-manipulating systems and Church-Rosser theorems. J. ACM, 20(1):160–187, January 1973.

[San93a] D. Sands. A compositional semantics of combining forms for Gamma programs. In International Conference on Formal Methods in Programming and Their Applications. Springer-Verlag, 1993.

[San93b] D. Sands. Laws of parallel synchronised termination. In Theory and Formal Methods 1993: Proceedings of the First Imperial College, Department of Computing, Workshop on Theory and Formal Methods, Isle of Thorns, UK, 1993. Springer-Verlag Workshops in Computer Science.

[Sta74] J. Staples. Church-Rosser theorems for replacement systems. In Algebra and Logic: papers from the Summer research institute of the Australian Mathematical Society, number 450 in Lecture Notes in Mathematics. Springer-Verlag, 1974.

A Compositional Definition of Transition Traces

To give the compositional construction of transition traces we need to define the appropriate sequential and parallel composition operators over sets of traces.

Notation In what follows we will adopt the following notation. If S is a set, then S^{∗} will denote the set of finite sequences of elements from S, S^{+} will denote the finite non-empty sequences, and S^{∞} will denote the infinite sequences. The power-set is denoted by ℘(S).

Note in particular that for a reduction relation →_{r}, we will write (→_{r})^{∗} to denote the finite sequence of pairs contained in →_{r}, and not the transitivereflexive closure of the relation.

Sequential Composition Sequential composition has an easy definition. We just take all concatenations of the atomic traces of the components. As is usual, if α and β are traces, then αβ denotes their concatenation, which is just α when α is infinite. Define the following sequencing operation for trace sets:

T_{1} ⊙ T_{2} = {αβ | α ∈ T_{1}, β ∈ T_{2}}

End-synchronised Merge Not surprisingly, parallel composition is described with the use of a merging combinator which interleaves traces. The peculiarities of parallel composition are prominent in the definition. To define the transition traces of P_{1} ∥ − P_{2} we must ensure that the traces of P_{1} and P_{2} are interleaved, but not arbitrarily; the termination step of a parallel composition requires an agreement, or synchronisation, at the point of their termination. To build up the picture, suppose α and β in (U × U)^{+} are traces of some programs P_{1} and P_{2} respectively. The set of all interleavings of α and β which correspond to possible executions of P_{1} ∥ − P_{2} can be given inductively by:

(M, M) ♯ (N, N) = \{ \begin{matrix}\{(M, M)\} & if M = N \\ ∅ & otherwise \end{matrix}

(M, M′)α ♯ (N, N′)β = {(M, M′)γ | α ≠ ϵ, γ ∈ α ♯ (N, N′)β}
∪ {(N, N′)γ | β ≠ ϵ, γ ∈ (M, M′)α ♯ β}

if either α ≠ ϵ or β ≠ ϵ.

To generalise the definition to incorporate the infinite traces as well as the finite, we need to define the interleavings via a maximal fixed-point rather than a minimal fixed point as implicit in the above definition. There are many possible ways of presenting this construction. We choose an implicit definition of the required maximal fixed-point:

Definition 16 A function m, from pairs of nonempty traces to sets of nonempty traces, is an end-synchronised merger (ESM), if the following conditions are satisfied:

1. if (M, N) ∈ m(β, γ) then β = γ = (M, N);

2. if α ∈ m(β, γ) then \begin{matrix}(M, N)α ∈ m((M, N)β, γ) \\ & (M, N)α ∈ m(γ, (M, N)β) \end{matrix}

Definition 17 The generalised end-synchronised merge is given by the pointwise union of all end-synchronised mergers:

α ♯ β = ∪ {m(α, β) | m is an ESM}

Note that ♯ is an ESM (this follows from the Knaster-Tarski fixed-point theorem), and therefore the largest ESM. The corresponding relation on sets of traces will provide the denotation of parallel composition:

T_{1} ⊕ T_{2} = {γ | α ∈ T_{1}, β ∈ T_{2}, γ ∈ α ♯ β}

Definition 18 The compositional atomic trace mapping T_{c}[[ ]] : P → ℘((U × U)^{+} ∪ (U × U)^{∞}) is given by induction on the syntax as:

T_{c}[[r]] = ‡((→_{r})^{∗} ⊙ {(M, M) | M↓^{r}}) ∪ ‡((→_{r})^{∞})
T_{c}[[P_{1} ; P_{2}]] = ‡(T_{c}[[P_{2}]] ⊙ T_{c}[[P_{1}]])
T_{c}[[P_{1} ∥ − P_{2}]] = ‡(T_{c}[[P_{1}]] ⊕ T_{c}[[P_{2}]])

Soundness It is straightforward to show that T_{c}[[ ]] is sound with respect to behaviours of a program. The following lemma gives the basic operational correspondence:

Lemma 19 1. ⟨P, M⟩ → M ⇒ (M, M) ∈ T_{c}[[P]]

2. ⟨P, M⟩ → ⟨P′, N⟩ & α ∈ T_{c}[[P′]] ⟹ (M, N)α ∈ T_{c}[[P]]

Proposition 20 T_{c}[[P]] ⊆ T_{c}[[Q]] ⟹ P ⊑_{o} Q

proof From Lemma 19 it is easy to see that T_{c}[[P]] ⊆ T_{c}[[Q]] ⇒ B(P) ⊆ B(Q). The operations used to build the compositional definition are all monotone with respect to subset inclusion, and so a simple induction on contexts is sufficient to give

T_{c}[[P]] ⊆ T_{c}[[Q]] ⇒ ∀C. T_{c}[[C[P_{1}]]] ⊆ T_{c}[[C[P_{2}]]].

Putting these together we have

\begin{aligned}T_{c}[[P]] ⊆ T_{c}[[Q]] & ⇒ & ∀C. B(C[P_{1}]) ⊆ B(C[P_{2}]) \\ & ⟺ & P_{1} ⊑_{o} P_{2}. \end{aligned}

□

B Path Constructions

Transition Traces from Paths The transition traces can be constructed from the paths as follows (overloading the mapping T[[ ]]):

T[[⟨R⟩]] = (T_{R})^{∞} ∪ ((T_{R})^{∗} ⊙ {(M, M) | r ∈ R, M↓^{r}})
T[[⟨R, R′⟩σ]] = (T_{R})^{∞} ∪ ((T_{R})^{∗} ⊙ {(M, M) | r ∈ R′, M↓^{r}} ⊙ T[[σ]])
where T_{R} = {(M, N) | r ∈ R, M→_{r}N}

Paths Constructed Compositionally Proposition 21 The following equations uniquely characterise the paths of a program:

paths(r) = ⟨{r}⟩
paths(P ; Q) = {σ_{1}⟨R⟩σ_{2} | σ_{1} ∈ paths(P), σ_{2} ∈ paths(Q), R = last(σ_{1})}
paths(P ∥ − Q) = {σ_{1} ⊗ σ_{2} | σ_{1} ∈ paths(P), σ_{2} ∈ paths(Q)}
where \begin{aligned}⟨R⟩ ⊗ ⟨R′⟩ & = & ⟨R ∪ R′⟩ \\ ⟨R_{1}, R_{2}⟩σ ⊗ ⟨R′⟩ & = & ⟨R′⟩ ⊗ ⟨R_{1}R_{2}⟩σ \\ & = & \{⟨(R_{1} ∪ R′), R_{2}⟩σ′ | σ′ ∈ ⟨R′⟩ ⊗ σ\} \\ ⟨R_{1}, R_{2}⟩σ_{1} ⊗ ⟨R′_{1}, R′_{2}⟩σ′_{1} & = & \{⟨(R_{1} ∪ R′_{1}), R_{2}⟩σ | σ ∈ σ_{1} ⊗ ⟨R′_{1}, R′_{2}⟩σ′_{1}\} \\ & ∪ & \{⟨(R_{1} ∪ R′_{1}), R′_{2}⟩σ′ | σ′ ∈ ⟨R_{1}, R_{2}⟩σ_{1} ⊗ σ′_{1}\} \end{aligned}