An Algebraic Treatment of Recursion
Rob van Glabbeek

             
           

nolistsep  




                         
Ubbmmn          
                         
                         
                         
                         



defiDefinition
definition[1]  



 
  

                          
                      


An Algebraic Treatment of Recursion


R.J. van Glabbeek



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


    December 30, 2023
====================================================================================================================================================



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.

13.6 pt
13.6 pt
13.6 pt



§ PROCESS ALGEBRA


In process algebra, processes are often modelled as closed terms of
single-sorted specification languages.

signatures
Let  be a set of variables.
A signature is a set of pairs (f,n) of a function symbol f∉ and an arity n ∈.
The set (Σ) of terms over a signature Σ is generated by:


  * ⊆(Σ),

  * if (f,n) ∈Σ and t_1,…,t_n ∈(Σ) then
f(t_1,…,t_n) ∈(Σ),

  * If V_⊆,  :V_→(Σ) and X∈ V_,
then X|∈(Σ).

A function  as appears in the last clause is called a recursive specification.  A
recursive specification  is often displayed as {X=_X| X ∈ V_}.
An occurrence of a variable y in a term t is free if it does not
occur[3] in a subterm of the form X| with y ∈ V_.  A term
is closed if it contains no free occurrences of variables.

The semantics of such a language is a function _:(Σ) → (^→).
It assigns to every term t∈(Σ) its meaning t∈^→.
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 -ary operator on : a function of
type ^→. It associates a value t(ρ)∈ to t that
depends on the choice of a valuation ρ:→.

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 :V_→(Σ)
for the entire language <cit.>. A term t in such a language can be seen as a the term t|,
obtained from t by substituting, for each Y∈ V_, Y| for each occurrence of Y.
Conversely, each term in the general language of signatures can be converted into the form
t| with t and  recursion-free.



§ 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 ∈, and

  * f(t_1,…,t_n)(ρ)=f_n^(t_1(ρ),…,t_n(ρ))
      for (f,n)∈Σ.
[3]

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

The denotational approach <cit.> recognises  as having type
^∖ V_→ (^V_→^V_) and
defines X|(ρ) for ρ∈^∖ V_
to be the X-component of the least fixed point of (ρ).
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 <cit.> 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∈ 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  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∈∖ V_, and 
ρ_i(X) = _X(ρ_i) for all X∈ V_,
then ρ_1(X)=ρ_2(X) for all X∈ V_.
The algebraic approach <cit.> yields a semantics for terms with guarded recursion only,
where X|(ρ) for ρ∈^∖ V_
is the X-component of the unique solution of (ρ).




§ EXTENDING THE ALGEBRAIC APPROACH TO UNGUARDED RECURSION


In <cit.> I proposed an extension of the algebraic approach to unguarded recursion.
An expression X| is seen as a kind of variable, only ranging over the solutions of .
Taking for example ACP <cit.>, interpreted in a domain of process graphs modulo strong
bisimilarity <cit.>,
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| denote the same
variable or different ones, here I formalise this approach only for terms t| where no
further recursion occurs in t or , thus following the second approach of pa.

A valuation ρ:→ is compatible with a recursive specification 
iff ρ(Y) = _Y(ρ) for all Y∈ V_.
The meaning t of a recursion-free term t in the context of a global recursive
specification  is now a function into  from the set of compatible valuations only.
It is obtained from the semantics of t from den by restricting (t) to the
compatible valuations.

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

The laws of process algebra remain valid in this approach, including the
congruence property for recursion: if _X(ρ)='_X(ρ) for all valuations
ρ, and all X ∈ V_=V_' then t|=t|'.

eptcsini


