Paper dedicated to Jan Bergstra, at the occasion of his 65^{th}birthday and retirement.

\begin{matrix}c \\ ◯ \end{matrix} R.J. van Glabbeek

This work is licensed under the

Creative Commons Attribution License.

An Algebraic Treatment of Recursion

Rob van Glabbeek

Data61, CSIRO, Sydney, Australia School of Computer Science and Engineering, University of New South Wales, Sydney, Australia

Jan Bergstra has put his mark on theoretical computer science by a consistent stream of original ideas, controversial opinions, and novel approaches. He sometimes reorganised the arena, enabling others to follow. I, for one, might never have entered computer science if it wasn’t for Jan’s support and encouragement, and will never forget the team spirit in the early days of process algebra in his group at CWI. This paper is dedicated to Jan, at the occasion of his 65^{th}birthday and retirement.

I review the three principal methods to assign meaning to recursion in process algebra: the denotational, the operational and the algebraic approach, and I extend the latter to unguarded recursion.

1 Process Algebra

In process algebra, processes are often modelled as closed terms of single-sorted specification languages. Definition 1 Let Var be a set of variables. A signature is a set of pairs (f,n) of a function symbol f ∉ Var and an arity n ∈ ℕ. The set 𝕋(Σ) of terms over a signature Σ is generated by:

• Var ⊆ 𝕋(Σ),

• if (f,n) ∈ Σ and t_{1},...,t_{n} ∈ 𝕋(Σ) then f(t_{1},...,t_{n}) ∈ 𝕋(Σ),

• If V_{S} ⊆ Var, S : V_{S} → 𝕋(Σ) and X ∈ V_{S} , then ^{/} \X|S ^{\} / ∈ 𝕋(Σ). A function S as appears in the last clause is called a recursive specification. A recursive specification S is often displayed as {X =S_{X}| X ∈V_{S} }. An occurrence of a variable y in a term t is free if it does not occur in a subterm of the form ^{/} \X|S^{\} / with y∈V_{S} . A term is closed if it contains no free occurrences of variables. The semantics of such a language is a function [[ ]]: 𝕋(Σ) → (𝔻^{Var} → 𝔻). It assigns to every term t ∈ 𝕋(Σ) its meaning [[t]]∈ 𝔻^{Var}→ 𝔻. The meaning of a closed term is a value chosen from a class of values 𝔻, called a domain. The meaning of an open term is a Var-ary operator on 𝔻: a function of type 𝔻^{Var}→ 𝔻. It associates a value [[t]](ρ) ∈ 𝔻 to t that depends on the choice of a valuation ρ: Var → 𝔻.

Sometimes, only a subset of 𝕋(Σ) is given a semantics, for instance by restricting to terms satisfying a syntactic criterion of guardedness.

Another approach lacks the recursion construct itself, but declares a single recursive specification S : V_{S} → 𝕋(Σ) for the entire language [4]. A term t in such a language can be seen as a the term ^{/} \t|S ^{\} /, obtained from t by substituting, for each Y ∈ V_{S} , ^{/} \Y |S ^{\} / for each occurrence of Y. Conversely, each term in the general language of Definition 1 can be converted into the form ^{/} \t|S ^{\} / with t and S recursion-free.

2 Denotational, Operational and Algebraic Semantics

The standard (denotational) semantics assigns to each function (f,n) ∈ Σ an n-ary operator f_{n}^{𝔻} : 𝔻^{n}→ 𝔻. The semantics of a recursion-free expression t is then given by

• [[X]](ρ) = ρ(X) for X ∈ Var, and

• [[f(t_{1},...,t_{n})]](ρ) = f_{n}^{𝔻} ([[t_{1}]](ρ),...,[[t_{n}]](ρ)) for (f,n) ∈ Σ.

Three approaches appear in the literature to give semantics to recursion.

The denotational approach [2] recognises [[S ]]as having type 𝔻^{Var\V_{S}} → (𝔻^{V_{S}} → 𝔻^{V_{S}}) and defines [[^{/} \X|S ^{\} / ]](ρ) for ρ ∈ 𝔻^{Var\V_{S}} to be the X-component of the least fixed point of [[S ]](ρ). For this least fixed point to exists, either 𝔻, equipped with a suitable preorder ⊑, needs to be a complete lattice, with the operators f^{𝔻} monotonic, or (𝔻,⊑) be a c.p.o., with the f^{𝔻} continuous, or 𝔻 be a complete metric space, with the f^{𝔻} contracting (or some variation on this theme).

The operational approach [4] is based on a set of inference rules that derive a collection of (labelled) transitions between closed terms. The semantic domain is now the collection 𝔾 of process graphs (S,T,I), with S a set of states, T a set of transitions between states, and I ∈ S an initial state, possibly subject to some cardinality restrictions. The operational semantics [[P]]of a closed term P takes S to be the set of closed terms, I = P, and T the derivable transitions. The semantics of open terms can be dealt with by encoding the process graphs ρ(X) for X ∈ Var as constants in an appropriate extension of the process algebra. This approach covers the meaning of recursion constructs too.

Let guardedness be a criterion on recursive specifications, such that if S is guarded then is has a unique solution, meaning that if ρ_{i} for i = 1,2 are valuations with ρ_{1}(Z) = ρ_{2}(Z) for all Z ∈ Var\ V_{S} , and ρ_{i}(X) = [[S_{X}]](ρ_{i}) for all X ∈ V_{S} , then ρ_{1}(X) = ρ_{2}(X) for all X ∈ V_{S} . The algebraic approach [1] yields a semantics for terms with guarded recursion only, where [[^{/} \X|S ^{\} / ]](ρ) for ρ ∈ 𝔻^{Var\V_{S}} is the X-component of the unique solution of [[S ]](ρ).

3 Extending the Algebraic Approach to Unguarded Recursion

In [3] I proposed an extension of the algebraic approach to unguarded recursion. An expression ^{/} \X|S ^{\} / is seen as a kind of variable, only ranging over the solutions of S. Taking for example ACP [1], interpreted in a domain of process graphs modulo strong bisimilarity [1], then ^{/} \X|X = aX^{\} /is a case of guarded recursion and denotes a specific process, namely an a-loop. On the other hand, ^{/} \X|X = X^{\} /is an unguarded recursion, and seen a variable ranging over all processes, just like X itself. In between, ^{/} \X|X = X + aX^{\} / is a case of unguarded recursion, and seen as a variable ranging over all processes of the form a^{∗}P.

To avoid ambiguity in deciding when two, almost identical, processes ^{/} \X|S ^{\} / denote the same variable or different ones, here I formalise this approach only for terms ^{/} \t|S ^{\} / where no further recursion occurs in t or S, thus following the second approach of Section 1.

A valuation ρ : Var → 𝔻 is compatible with a recursive specification S iff ρ(Y) = [[S_{Y}]](ρ) for all Y ∈ V_{S} . The meaning [[t]]of a recursion-free term t in the context of a global recursive specification S is now a function into 𝔻 from the set of compatible valuations only. It is obtained from the semantics of t from Section 2 by restricting dom([[t]]) to the compatible valuations.

In particular, an equation t = u holds under this semantics iff [[t]](ρ) = [[u]](ρ) for all valuations ρ compatible with S. Hence it is equivalent to the conditional equation (⋀_{X∈V_{S}} X = S_{X}) ⇒ t = u.

The laws of process algebra remain valid in this approach, including the congruence property for recursion: if [[S_{X}]](ρ) = [[S′_{X}]](ρ) for all valuations ρ, and all X ∈ V_{S} = V_{S′} then [[^{/} \t|S ^{\} / ]]= [[^{/} \t|S′^{\} / ]].

References

[1] J.A. Bergstra & J.W. Klop (1986): Algebra of Communicating Processes. In de Bakker, Hazewinkel & Lenstra, editors: Mathematics & Computer Science I, CWI Monograph 1, North-Holland, pp. 89–138.

[2] S.D. Brookes, C.A.R. Hoare & A.W. Roscoe (1984): A theory of communicating sequential processes. Journal of the ACM 31(3), pp. 560–599, doi:10.1145/828.833.

[3] R.J. van Glabbeek (1987): Bounded nondeterminism and the approximation induction principle in process algebra. In F. Brandenburg, G. Vidal-Naquet & M. Wirsing, editors: Proc. STACS’87, LNCS 247, Springer,

   pp. 336–347, doi:10.1007/BFb0039617.

[4] R. Milner (1989): Communication and Concurrency. Prentice Hall, Englewood Cliffs.