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.
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:
-
J.A. Bergstra, I. Bethke, and A. Ponse.
Equations for formally real meadows.
Journal of Applied Logic, 13:1-23, 2015.
Also available at arXiv:1310.5011v4
[math.RA, cs.LO], 18 Oct 2013, this version (v4): 13 Jan 2015.
We consider the signatures of meadows and of signed meadows. We give two complete axiomatizations of the equational theories of the real numbers with respect to these signatures. In the first case, we extend the axiomatization of zero-totalized fields by a single axiom scheme expressing formal realness; the second axiomatization presupposes an ordering. We apply these completeness results in order to obtain complete axiomatizations of the complex numbers.
-
J.A. Bergstra and A. Ponse.
Division by zero in common meadows.
In: R. de Nicola and R. Hennicker (editors), Software, Services, and Systems
(Wirsing Festschrift), LNCS 8950, pages 46-61, Springer, 2015.
Revised version:
arXiv:1406.6878v4
[math.RA], 22 March 2021.
In a "common meadow", the inverse of zero is defined as an additional element "a" that propagates through all operations (and can be seen as an error element). We provide a basis theorem for so-called common cancellation meadows of characteristic zero, that is, common meadows of characteristic zero that admit a certain cancellation law.
-
J.A. Bergstra and A. Ponse.
Fracpairs and fractions over a reduced commutative ring.
Indagationes Mathematicae, 27:727-748, 2016.
https://doi.org/10.1016/j.indag.2016.01.007.
Preprint available at arXiv:1411.4410v2
[math.RA], 22 Jan 2016.
We prove that the initial common meadow is isomorphic to the initial algebra of fracpairs over the integers, where fracpairs are pairs subject to laws consistent with the use of the pair as a fraction that do not exclude denominators to be zero. The definition of fracpairs is very close to that of the field of fractions of an integral domain: a facpair is defined over a reduced commutative ring as an expression p/q, and fracpairs are considered modulo the equivalence generated by xz/yzz=x/yz. The common meadow operations on fracpairs are defined in a natural way, in particular a=1/0, (p/q)+(r/s)= (ps+rq)/qs and (p/q)^-1= qq/pq.
-
J.A. Bergstra, I. Bethke, and A. Ponse.
Cancellation Meadows: A Generic Basis Theorem and Some
Applications.
The Computer Journal 56(1): 3-14, 2013.
https://doi.org/10.1093/comjnl/bxs02.
This paper contains some elementary results (PDF).
-
J.A. Bergstra, A. Ponse, and M.B. van der Zwaag.
Tuplix
calculus. Scientific Annals of Computer Science, 18:35-61,
2008. (Also available at arXiv:0712.3423.)
Tuplices are expressions that generalize matrices and vectors. Tuplices have an underlying data type for quantities that are taken from a zero-totalized field.
- J.A. Bergstra and J.V. Tucker. The rational numbers as an abstract data type. Journal of the ACM (JACM), Volume 54 Issue 2, Article No. 7, April 2007. https://doi.org/10.1145/1219092.1219095.
- J.A. Bergstra, Y. Hirshfeld, and J.V. Tucker. Meadows. Report PRG0705, University of Amsterdam, September 2007.
- J.A. Bergstra, Y. Hirshfeld, and J.V. Tucker. Meadows and the equational specification of division. Theoretical Computer Science, 410(12-13):1261-1271, 17 March 2009. https://doi.org/10.1016/j.tcs.2008.12.015.
Former research themes:
Computer viruses
- With Jan Bergstra
(since 2005).
Under construction.
Development of a theory on computer viruses.
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:
- Bergstra: Why (not) Program Algebra / Thread Algebra
- Diertens: PGA page (with a link to the PGA Toolset)
- Bergstra & Ponse: An Instruction Sequence Semigroup with Involutive Anti-Automorphisms (2009, PDF)
- Stephan Schroevers: Expressiveness and Extensions of an Instruction Sequence Semigroup (63 pp, Master of Logic thesis, 2010)
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.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):
[...]
[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.
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.More process algebra:
[...]
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.J. V. TUCKER
University of Wales Swansea
-
J.A. Bergstra and A. Ponse. Non-regular iterators in process
algebra. Theoretical Computer Science 269 (1-2):203-229,
2001.
In this paper, three forms of non-regular iteration in process algebra are considered (next to the binary Kleene-star operation): the push-down operation, the nesting operation, and the back and forth operation. PDF. -
J.A. Bergstra, A. Ponse and M.B. van der Zwaag. Branching time and
orthogonal bisimulation equivalence. Theoretical Computer
Science 309 (1-3):313-355, 2003.
This paper is about a refinement of branching bisimulation equivalence called orthogonal bisimulation equivalence. Typically, internal activity (the performance of tau-steps) may be compressed, but not completely discarded. PDF. - B. Diertens: Software Engineering with Process Algebra + Computational Models
Return to Former research themes
Last modified: May 3, 2022