Current themes:

(Former research themes)

Proposition algebra and Short-circuit logic - With Jan Bergstra (since 2009) and Daan Staudt (since 2012)

We start from Hoare's ternary connective P <| Q |> R (in LaTeX we use \triangleleft and \triangleright, respectively) that first evaluates Q, and upon result true continues with P, and upon false with R. Observe that this connective can be characterized by "if Q then P else R" and that evaluaton is a deterministic, sequential process. With constants T for true and F for false, the common propositional connectives are definable:

    ¬ x = F <| x |> T
  x ∧ y = y <| x |> F
  x ∨ y = T <| x |> y
Note that this definition enforces left-sequential evaluation of the binary connectives, this type of evaluation is also called short-circuit evaluation: the second argument is only evaluated is the first argument does not suffice to determine the value of the expression; a common notation for these connectives prescribing such evaluation (as used in programming) is && and ||, respectively.

We axiomatize various valuation congruences, from "free valuation congruence" up to "static valuation congruence" (the latter represents a sequential version of propositional logic). A proposition algebra is a model of four simple equational axioms that define the basic properties of

  x <| y |> z
(no other connectives are involved).

A short-circuit logic (SCL) is a logic that implies all identities valid in free valuation congruence that are expressed with T, F, ¬, && and || only. In this manner, each valuation congruence defines its associated SCL as the smallest set of such identities. Introductory slide deck about SCL (29 slides), presented 4 November 2013 in the Minor Programming at UvA.

More information.

Return to Top

Meadows - With Jan Bergstra and Inge Bethke (since 2007).

Advantages and disadvantages of the algebraic specification of abstract data types and number systems have been amply discussed in the computer science literature. The primary algebraic properties of the rational, real and complex numbers are captured by the operations and axioms of fields consisting of the equations that define a commutative ring and two axioms, which are not equations, that define the inverse operator and the distinctness of the two constants 0 and 1. In particular, fields are partial algebras - because inversion is undefined at 0 - and do not possess an equational axiomatization. Meadows (the term is inspired by "fields") originate as the design decision to turn inversion (or division) into a total operator by means of the assumption that the inverse of 0 is 0. By doing so the investigation of number systems as abstract data types can be carried out within the original framework of algebraic specifications without taking any precautions for partial functions or for empty sorts. The equational specification of the variety of meadows has been proposed in 2007 by Bergstra, Hirshfeld and Tucker and has subsequently been elaborated on in detail.

Selected papers:

Initial papers:

Return to Top

Former research themes:

Return to Top

Computer viruses - With Jan Bergstra (since 2005).
Under construction. Development of a theory on computer viruses.

More information.

Return to Former research themes

Instruction sequences and Thread algebra - With Jan Bergstra, Inge Bethke, Bob Diertens (since 1998).

Instruction sequences are viewed as underlying the semantics of (computer) programs. We consider various algebraic settings to specify and analyse aspects of instruction sequences. Some of these aspects are not preserved in program transformations or after abstraction to behaviour, while others are. For example, in the setting of PGA (i.e., "program algebra") where programs are at basic level represented by instruction sequences with jump instructions, termination, and simple basic and test instructions, both the projection semantics from higher dialects to this level and the behavioural semantics that map PGA-programs to threads are not compositional. On the other hand, certain algebras of instruction sequences admit various types of behaviour preserving homomorphisms. Behavioural semantics for instruction sequences is defined in "thread algebra", an algebraic theory about sequential program behaviors especially developed for this purpose. Research on thread algebra itself addresses in particular the construction of models for various forms of multi-threading and the development of tools, and also the further development of our theory on computer viruses.

More information:

Return to Former research themes

Process algebra - With Jan Bergstra, Inge Bethke, Bob Diertens (since 25+ years).

Under construction. Quote from a Wikipedia page:

The Algebra of Communicating Processes (ACP) is an algebraic approach to reasoning about concurrent systems. It is a member of the family of mathematical theories of concurrency known as process algebras or process calculi. ACP was initially developed by Jan Bergstra and Jan Willem Klop in 1982 [1], as part of an effort to investigate the solutions of unguarded recursive equations. More so than the other seminal process calculi (CCS and CSP), the development of ACP focused on the algebra of processes, and sought to create an abstract, generalized axiomatic system for processes [2], and in fact the term process algebra was coined during the research that led to ACP.
[1] J.C.M. Baeten, A brief history of process algebra. Theoretical Computer Science, 335(2-3):131-146, 23 May 2005.
[2] Bas Luttik. What is algebraic in process theory? In: Luca Aceto, editor, The Concurrency Column, Bulletin of the EATCS 88, February 2006. This is an extended version of an essay that appeared in: Luca Aceto and Andrew Gordon, editors, Proceedings of the Workshop Algebraic Process Calculi: The First Twenty Five Years and Beyond (APC 25), ENTCS 162, pp. 227-231, September 2006.
Quote from a review by J.V. Tucker (The Computer Journal 45(1):68-69, 2002) on the Handbook of Process Algebra (Elsevier Science, 2001):  
Process algebra is a standard subject in Theoretical Computer Science, one that can be introduced to undergraduates in their first year and applied in projects in their final year. There is a massive amount of theory, some acceptable software tools and a decent tradition of applications and case studies. Process algebra is also being used to solve computational problems in several industries.
It is a subject that computer scientists invented to solve their own fundamental problems. It is a subject with huge potential. It is making its mark in the pop culture of design technologies, of course. However, I think it will grow in its intellectual influence and will secure the glittering prizes of applications in science. But before it makes its mark in one of the classical cultures of physics or biology, its theoretical development has a long way to go.

University of Wales Swansea

More process algebra:

Return to Former research themes

Return to Top

  Last modified: May 3, 2022