An Algebraic Treatment of Recursion

TL;DR

This paper reviews the main methods for defining recursion in process algebra and extends the algebraic approach to handle unguarded recursion, providing a comprehensive algebraic framework.

Contribution

It introduces an extension of the algebraic method to accommodate unguarded recursion in process algebra.

Findings

Extended algebraic approach to unguarded recursion

Unified view of denotational, operational, and algebraic methods

Enhanced algebraic framework for recursion

Abstract

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.

Full text

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 65th birthday and retirement.

1 Process Algebra

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

Definition 1.1**.**

signatures Let ${\it Var}$ be a set of variables. A signature is a set of pairs $(f,n)$ of a function symbol $f\notin{\it Var}$ and an arity $n\in\mathbbm{N}$. The set $\mathbbm{T}(\Sigma)$ of terms over a signature $\Sigma$ is generated by:

• •

${\it Var}\subseteq\mathbbm{T}(\Sigma)$,

• •

if $(f,n)\in\Sigma$ and $t_{\_}1,\ldots,t_{\_}n\in\mathbbm{T}(\Sigma)$ then $f(t_{\_}1,\ldots,t_{\_}n)\in\mathbbm{T}(\Sigma)$,

• •

If $V_{\_}\mathcal{S}\subseteq{\it Var}$,  $\mathcal{S}:V_{\_}\mathcal{S}\rightarrow\mathbbm{T}(\Sigma)$ and $X\in V_{\_}\mathcal{S}$, then \raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny$/$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$\backslash$}}}!!X|\mathcal{S}!!\stackrel{{\scriptstyle\mbox{\tiny$\backslash$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$/$}}}}\in\mathbbm{T}(\Sigma).

A function $\mathcal{S}$ as appears in the last clause is called a recursive specification. A recursive specification $\mathcal{S}$ is often displayed as $\{X\mathbin{=}\mathcal{S}_{\_}{\!X\!}\mid X\mathbin{\in}V_{\_}{\!\mathcal{S}\!}\}$. An occurrence of a variable $y$ in a term $t$ is free if it does not occur in a subterm of the form \stackrel{{\scriptstyle\mbox{\tiny/}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny\backslash}}}\!\!X|\mathcal{S}\!\!\!\stackrel{{\scriptstyle\mbox{\tiny\backslash}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny/}}} with $y\mathbin{\in}V_{\_}{\!\mathcal{S}\!\!}$. A term is closed if it contains no free occurrences of variables.

The semantics of such a language is a function \mbox{[[}\,\_\,\mbox{]]}:\mathbbm{T}(\Sigma)\rightarrow(\mathbbm{D}^{\it Var}\rightarrow\mathbbm{D}). It assigns to every term $t\in\mathbbm{T}(\Sigma)$ its meaning \mbox{[[}\,t\,\mbox{]]}\in\mathbbm{D}^{\it Var}\!\rightarrow\mathbbm{D}. The meaning of a closed term is a value chosen from a class of values $\mathbbm{D}$, called a domain. The meaning of an open term is a ${\it Var}\!$-ary operator on $\mathbbm{D}$: a function of type $\mathbbm{D}^{\it Var}\!\rightarrow\mathbbm{D}$. It associates a value \mbox{[[}\,t\,\mbox{]]}(\rho)\mathbin{\in}\mathbbm{D} to $t$ that depends on the choice of a valuation $\rho\!:{\it Var}\rightarrow\mathbbm{D}$.

Sometimes, only a subset of $\mathbbm{T}(\Sigma)$ 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 $\mathcal{S}:V_{\_}\mathcal{S}\rightarrow\mathbbm{T}(\Sigma)$ for the entire language [5]. A term $t$ in such a language can be seen as a the term \stackrel{{\scriptstyle\mbox{\tiny/}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny\backslash}}}\!\!t|\mathcal{S}\!\!\stackrel{{\scriptstyle\mbox{\tiny\backslash}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny/}}}, obtained from $t$ by substituting, for each $Y\in V_{\_}\mathcal{S}$, \stackrel{{\scriptstyle\mbox{\tiny/}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny\backslash}}}\!\!Y|\mathcal{S}\!\!\stackrel{{\scriptstyle\mbox{\tiny\backslash}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny/}}} for each occurrence of $Y$. Conversely, each term in the general language of Definition LABEL:df:signatures can be converted into the form \stackrel{{\scriptstyle\mbox{\tiny/}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny\backslash}}}\!\!t|\mathcal{S}\!\!\stackrel{{\scriptstyle\mbox{\tiny\backslash}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny/}}} with $t$ and $\mathcal{S}$ recursion-free.

2 Denotational, Operational and Algebraic Semantics

The standard (denotational) semantics assigns to each function $(f,n)\in\Sigma$ an $n$-ary operator $f_{\_}n{D}:\mathbbm{D}^{n}\!\rightarrow\mathbbm{D}$. The semantics of a recursion-free expression $t$ is then given by

• •

\mbox{[[}\,X\,\mbox{]]}(\rho)=\rho(X)                                                for $X\in{\it Var}$, and

• •

\mbox{[[}\,f(t_{\_}1,\dots,t_{\_}n)\,\mbox{]]}(\rho)=f_{\_}n^{\mathbbm{D}}(\mbox{[[}\,t_{\_}1\,\mbox{]]}(\rho),\dots,\mbox{[[}\,t_{\_}n\,\mbox{]]}(\rho))   for $(f,n)\in\Sigma$.

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

The denotational approach [3] recognises \mbox{[[}\,\mathcal{S}\,\mbox{]]} as having type $\mathbbm{D}^{{\it Var}\setminus V_{\_}\mathcal{S}}\!\rightarrow(\mathbbm{D}^{V_{\_}\mathcal{S}}\!\rightarrow\mathbbm{D}^{V_{\_}\mathcal{S}})$ and defines \mbox{[[}\,\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny$/$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$\backslash$}}}!!X|\mathcal{S}!!\stackrel{{\scriptstyle\mbox{\tiny$\backslash$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$/$}}}}\,\mbox{]]}(\rho) for $\rho\in\mathbbm{D}^{{\it Var}\setminus V_{\_}\mathcal{S}}$ to be the $X$-component of the least fixed point of \mbox{[[}\,\mathcal{S}\,\mbox{]]}(\rho). For this least fixed point to exists, either $\mathbbm{D}$, equipped with a suitable preorder $\sqsubseteq$, needs to be a complete lattice, with the operators $f{D}$ monotonic, or $(\mathbbm{D},\sqsubseteq)$ be a c.p.o., with the $f{D}$ continuous, or $\mathbbm{D}$ be a complete metric space, with the $f{D}$ contracting (or some variation on this theme).

The operational approach [5] 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 $\mathbbm{G}$ of process graphs $(S,T,I)$, with $S$ a set of states, $T$ a set of transitions between states, and $I\in S$ an initial state, possibly subject to some cardinality restrictions. The operational semantics \mbox{[[}\,P\,\mbox{]]} 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 $\rho(X)$ for $X\in{\it 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 $\mathcal{S}$ is guarded then is has a unique solution, meaning that if $\rho_{\_}i$ for $i=1,2$ are valuations with $\rho_{\_}1(Z)=\rho_{\_}2(Z)$ for all $Z\in{\it Var}\setminus V_{\_}\mathcal{S}$, and \rho_{\_}i(X)=\mbox{[[}\,\mathcal{S}_{\_}X\,\mbox{]]}(\rho_{\_}i) for all $X\in V_{\_}\mathcal{S}$, then $\rho_{\_}1(X)=\rho_{\_}2(X)$ for all $X\in V_{\_}\mathcal{S}$. The algebraic approach [2] yields a semantics for terms with guarded recursion only, where \mbox{[[}\,\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny$/$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$\backslash$}}}!!X|\mathcal{S}!!\stackrel{{\scriptstyle\mbox{\tiny$\backslash$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$/$}}}}\,\mbox{]]}(\rho) for $\rho\in\mathbbm{D}^{{\it Var}\setminus V_{\_}\mathcal{S}}$ is the $X$-component of the unique solution of \mbox{[[}\,\mathcal{S}\,\mbox{]]}(\rho).

3 Extending the Algebraic Approach to Unguarded Recursion

In [4] I proposed an extension of the algebraic approach to unguarded recursion. An expression \stackrel{{\scriptstyle\mbox{\tiny/}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny\backslash}}}\!\!X|\mathcal{S}\!\!\stackrel{{\scriptstyle\mbox{\tiny\backslash}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny/}}} is seen as a kind of variable, only ranging over the solutions of $\mathcal{S}\!\!$. Taking for example ACP [2], interpreted in a domain of process graphs modulo strong bisimilarity [2], then \stackrel{{\scriptstyle\mbox{\tiny/}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny\backslash}}}\!\!X|X=aX\!\!\stackrel{{\scriptstyle\mbox{\tiny\backslash}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny/}}} is a case of guarded recursion and denotes a specific process, namely an $a$-loop. On the other hand, \stackrel{{\scriptstyle\mbox{\tiny/}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny\backslash}}}\!\!X|X=X\!\!\stackrel{{\scriptstyle\mbox{\tiny\backslash}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny/}}} is an unguarded recursion, and seen a variable ranging over all processes, just like $X$ itself. In between, \stackrel{{\scriptstyle\mbox{\tiny/}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny\backslash}}}\!\!X|X=X+aX\!\!\stackrel{{\scriptstyle\mbox{\tiny\backslash}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny/}}} 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 \stackrel{{\scriptstyle\mbox{\tiny/}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny\backslash}}}\!\!X|\mathcal{S}\!\!\stackrel{{\scriptstyle\mbox{\tiny\backslash}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny/}}} denote the same variable or different ones, here I formalise this approach only for terms \stackrel{{\scriptstyle\mbox{\tiny/}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny\backslash}}}\!\!t|\mathcal{S}\!\!\stackrel{{\scriptstyle\mbox{\tiny\backslash}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny/}}} where no further recursion occurs in $t$ or $\mathcal{S}$, thus following the second approach of Section 1.

A valuation $\rho:{\it Var}\rightarrow\mathbbm{D}$ is compatible with a recursive specification $\mathcal{S}$ iff \rho(Y)=\mbox{[[}\,\mathcal{S}_{\_}Y\,\mbox{]]}(\rho) for all $Y\in V_{\_}\mathcal{S}$. The meaning \mbox{[[}\,t\,\mbox{]]} of a recursion-free term $t$ in the context of a global recursive specification $\mathcal{S}$ is now a function into $\mathbbm{D}$ from the set of compatible valuations only. It is obtained from the semantics of $t$ from Section 2 by restricting {\it dom}(\mbox{[[}\,t\,\mbox{]]}) to the compatible valuations.

In particular, an equation $t=u$ holds under this semantics iff \mbox{[[}\,t\,\mbox{]]}(\rho)=\mbox{[[}\,u\,\mbox{]]}(\rho) for all valuations $\rho$ compatible with $\mathcal{S}$. Hence it is equivalent to the conditional equation $\left(\bigwedge_{\_}{X\in V_{\_}\mathcal{S}}X=\mathcal{S}_{\_}X\right)\Rightarrow t=u$.

The laws of process algebra remain valid in this approach, including the congruence property for recursion: if \mbox{[[}\,\mathcal{S}_{\_}X\,\mbox{]]}(\rho)=\mbox{[[}\,\mathcal{S}^{\prime}_{\_}X\,\mbox{]]}(\rho) for all valuations $\rho$, and all $X\in V_{\_}\mathcal{S}=V_{\_}{\mathcal{S}^{\prime}}$ then \mbox{[[}\,\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny$/$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$\backslash$}}}!!t|\mathcal{S}!!\stackrel{{\scriptstyle\mbox{\tiny$\backslash$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$/$}}}}\,\mbox{]]}=\mbox{[[}\,\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny$/$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$\backslash$}}}!!t|\mathcal{S}^{\prime}!!\stackrel{{\scriptstyle\mbox{\tiny$\backslash$}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny$/$}}}}\,\mbox{]]}.