Sponsor: Engineering and Physical Sciences Research Council
Local Organisers: Chris Tofts, Iain Stewart, Karen Stephenson and Savita Chauhan.
The 11th meeting of the British Colloquium for Theoretical Computer Science was held at the University of Wales Swansea at the beginning of April 1995. The next meeting (BCTCS12) is being organised by Simon Thompson at the University of Kent at Canterbury.
by J Stell, Keele University
As appeared in the Bulletin of the EATCS, Number 56, pp222-231, February 1996.
This was the eleventh annual meeting of the British Colloquium for Theoretical Computer Science, and the first time it had been held in Wales. The meeting was held at Clyne Castle, a nineteenth century house now owned by the University of Wales, Swansea. This provided an ideal location for the conference; besides the academic presentations the participants could enjoy the nearby park, originally the grounds of the house, with its remarkable collection of mature trees and interesting plants, as well as views over Swansea Bay.
There were about 80 participants in total coming from all parts of the British Isles as well as visitors from continental Europe and those based as far afield as Brazil, Canada, and South Africa.
The meeting followed the usual format of a small number of one hour presentations by invited speakers combined with a much larger number of 25 minute presentations accepted without any refereeing process from the other participants. This format made the meeting well suited to informal interaction and provided a useful context in which ongoing research could be exposed to reactions from the audience. Altogether there were about 40 short presentations covering the whole field of theoretical computer science.
There were eight invited talks from
J R Hindley (Swansea), J W de Bakker (CWI, the Netherlands), M Hennessey (Sussex), F Moller (SICS, Sweden) J V Tucker (Swansea), J Heering (CWI, the Netherlands), I A Stewart (Swansea), and D E Rydeheard (Manchester).
These invited presentations included some of a tutorial nature, giving a general overview of some area of work, and some more directed towards describing details of current research.
While all the invited presentations were of a high standard, one, that by David Rydeheard on Categories, Proofs and Games was particularly memorable for its highly original use of models of wood and elastic. We were introduced to `Penny the pushout square' and `Coco the coequalizer' to illustrate category theoretic constructions. These models provided an entertainment worthy of Emmett or Heath Robinson, but formed the introductory part of a tutorial which concluded by outlining how proofs in intuitionistic mathematics correspond to winning strategies in dialogue games.
The organization of the meeting was carried out very smoothly by the team of local organizers headed by Chris Tofts. Overall this was a most enjoyable and useful meeting; the next in the series will be BCTCS12 at the University of Kent at Canterbury in 1996.
For about a decade, we have been working in Amsterdam on semantics based on (complete) metric spaces. Strong points of the metric approach are
We have applied the methodology to several language paradigms (imperative, parallel OO, LP) and numerous language notions, culminating in a large number (> 25) of precise relationships between their operational and denotational models. We shall present a representative selection of these.
Literature: J W de Bakker, J J M M Rutten, Ten Years of Concurrency Semantics - selected papers of the Amsterdam Concurrency Group, World Scientific, 1992 (a collection of 12 reprinted papers)
J W de Bakker, E P de Vink, Control Flow Semantics, MIT Press, to appear (a 500 pp text in the final stages of preparation)
J Heering (CWI): Algebraic Specifications and Proofs by Induction
This is a tutorial on proofs by induction in the context of algebraic specifications and term rewriting systems. It will address:
These approaches aim at minimizing user interaction. Examples of their application to program verification, symbolic execution, and program optimization will be given.
M Hennessy (Sussex): Higher-Order Processes and their Models
A higher-order process algebra in which processes can be sent and received as data along channels is investigated. Using a simple operational semantics two behavioural preorders are defined. The first, based on may testing, is in terms of the ability of processes to offer communications on channels while the second, based on must testing, depends on the communications which processes can guarantee.
The first behavioural preorder can be modelled by a denotational semantics which uses a notion of higher-order traces while for the second we develop a denotational model using higher-order Acceptance Trees.
J R Hindley (Swansea): Counting the Inhabitants of a Type
In simple type theory there is a very neat algorithm, due to C.-B. Ben-Yelles, for counting the number of lambda-terms in normal form that have a given type. As a special case the algorithm decides in finite time whether this number is infinite. This algorithm will be described and motivated and the reason why it works will be sketched.
F Moller (SICS, Sweden): The Computational complexity of Bisimularity
In his Turing Award lecture, Juris Hartmanis eloquently discusses the fundamental role which computational complexity theory plays in computer science, highlighting some of the results obtained on the computational complexity of problems in formal language theory; e.g., all context-free languages are contained in TIME[n^3] and SPACE[log^2 n]. We argue that the computational complexity of formal language theory takes on a new and interesting light when the languages involved are interpreted as describing (concurrent) processes rather than sequential machines or programs, and the traditional notion of language equivalence is replaced by bisimulation equivalence.
Bisimilarity is the cornerstone of a number of theories of concurrent and distributed computing, notably Robin Milner's Calculus of Communicating Systems (CCS). Given that Milner received the 1991 Turing Award and that bisimilarity figured prominently in his Turing Award lecture, we believe it is particularly apropos to re-examine the field of computational complexity --- whose inception is due to Hartmanis and Stearns --- in this setting. Bisimilarity has also drawn the attention of modal logicians, who called it the "zig-zag" relation almost 20 years ago, as well as set theorists, as it forms the basis of Aczel's Anti Foundation Axiom for non-well-founded set theory. Finally, it has an elegant game-theoretic interpretation.
Processes can be described either as automata or as terms of an algebra. Concurrent systems are then specified by introducing a composition operation on automata or by adding a composition operator to the algebra. Many such composition operators have been proposed including those capturing synchrony synchrony, asynchrony, or something in between. By viewing recursive algebraic specifications as a process grammar, we have the three main ingredients of a formal language theory in a new setting: automata, grammars and equivalence (bisimilarity).
The computational complexity of bisimulation equivalence in this formal language framework differs greatly from its classical counterpart, with a number of surprising twists and turns. We concentrate here on the inner layers of the Chomsky hierarchy, viz. regular and context-free processes, and note in passing that a language like CCS is easily shown to be Turing-powerful.
In the case of regular processes devoid of any kind of concurrent composition operator, Kanellakis and Smolka showed that bisimilarity can be decided in polynomial time. This is in stark contrast to the case of language equivalence, where the problem is PSPACE-complete.
The situation is even more dramatic in the context-free case where the resulting processes are no longer finite-state. In the classical setting, the equivalence problem for languages generated by nondeterministic context-free grammars is undecidable. Taking advantage of the periodic structure exhibited by bisimilar processes, Baeten, Bergstra and Klop were able to show that bisimilarity of normed context-free processes --- those processes in which the underlying context-free grammar contains no redundant nonterminals --- is decidable. Moreover, this result was recently generalized by Christensen, Huttel and Stirling to all context-free processes. To cap things off, in the normed case, Hirshfeld, Jerrum and Moller showed that bisimilarity is once again decidable in polynomial time! Restricting to simple (i.e., deterministic) normed grammars, where language equivalence and bisimilarity coincide, we find that language equivalence is polynomially decidable, improving vastly on the doubly exponential algorithm of Korenjak and Hopcroft.
It is worthwhile to ask what are the practical ramifications of this computational dichotomy? Happily, the answer is only positive for computer scientists interested in bisimilarity, as is often the case in concurrency theory and for verification tools based on this theory. In this case, one is confronted with a tractable problem even for processes of a highly expressive nature.
D Rydeheard (Manchester): Categories, Proofs and Games
This talk is to be a celebration of some aspects of category theory and its applications in Computer Science. Supermodels will help with the exposition, part of which is to be a game show.
I A Stewart (Swansea): Descriptive Complexity Theory
This tutorial will explain how complexity classes, traditionally defined by bounding the resources used by some model of computation, can be considered as classes of problems definable by the sentences of some logic. That is, we define or describe or specify problems as opposed to solving or accepting them. Descriptive complexity theory forms part of a wider field known as finite model theory which is the consideration of definability on classes of finite structures and which at present is very underdeveloped. As we illustrate, adopting a logical approach to complexity theory enables new purely complexity-theoretic results to be obtained and highlights new concepts and notions, not available in the traditional setting, which may help to provide insight into some of the existing open problems in complexity theory.