Nonaxiomatisability of Equivalences over Finite State Processes. Peter Sewell. Annals of Pure and Applied Logic, 90:163--191, December 1997. Invited submission from LICS '94. [ bib | doi | ps | pdf | http ]
This paper considers the existence of finite equational axiomatisations of behavioural equivalences over a calculus of finite state processes. To express even simple properties such as mu x E = mu x E[E/x] some notation for substitutions is required. Accordingly the calculus is embedded in a simply typed lambda calculus, allowing such schemas to be expressed as equations between terms containing first order variables. A notion of first order trace congruence over such terms is introduced and used to show that no finite set of such equations is sound and complete for any reasonable equivalence finer than trace equivalence. The intermediate results are then applied to give two nonaxiomatisability results over calculi of regular expressions.
 
The Algebra of Finite State Processes. Peter Michael Sewell. PhD thesis, University of Edinburgh, October 1995. Dept. of Computer Science technical report CST-118-95, also published as LFCS-95-328. [ bib | ps (cmr) | ps | pdf ]
This thesis is concerned with the algebraic theory of finite state processes. The processes we focus on are those given by a signature with prefix, summation and recursion, considered modulo strong bisimulation. We investigate their equational and implicational theories.

We first consider the existence of finite equational axiomatisations. In order to express an interesting class of equational axioms we embed the processes into a simply typed lambda calculus, allowing equation schemes with metasubstitutions to be expressed by pure equations. Two equivalences over the lambda terms are defined, an extensional equality and a higher order bisimulation. Under a restriction to first order variables these are shown to coincide and an examination of the coincidence shows that no finite equational axiomatisation of strong bisimulation can exist. We then encode the processes of Basic Process Algebra with iteration and zero (BPA_δ^*) into this lambda calculus and show that it too is not finitely equationally axiomatisable, in sharp contrast to the extant positive result for the fragment without zero.

For the implicational theory, we show the existence of finite computable complete sets of unifiers for finite sets of equations between processes (with zero order variables). It follows that the soundness of sequents over these is decidable.

Some applications to the theories of higher order process calculi and non-well-founded sets are made explicit.

 
Bisimulation is Not Finitely (First-Order) Equationally Axiomatisable. Peter M. Sewell. In LICS 1994, Subsumed by the APAL 1997 paper. [ bib | doi | ps | pdf | http ]
This paper considers the existence of finite equational axiomatisations of bisimulation over a calculus of finite state processes. To express even simple properties such as mu X E=mu X E[E/X] equationally it is necessary to use some notation for substitutions. Accordingly the calculus is embedded in a simply typed lambda calculus, allowing axioms such as the above to be written as equations of higher type rather than as equation schemes. Notions of higher order transition system and bisimulation are then defined and using them the nonexistence of finite axiomatisations containing at most first order variables is shown.

The same technique is then applied to calculi of star expressions containing a zero process --- in contrast to the positive result given in [FZ93] for BPA*, which differs only in that it does not contain a zero.