25 citations · 637 across the 113 of their papers we have counts for
38 papers · 1 filter
Fracterm Calculus for Partial Meadows
Jan A. Bergstra, Alban Ponse
Partial algebras and datatypes are discussed with the use of signatures that allow partial functions, and a three-valued short-circuit (sequential) first order logic with a Tarski…
Space-time process algebra with asynchronous communication
J. A. Bergstra, C. A. Middelburg
We introduce a process algebra that concerns the timed behaviour of distributed systems with a known spatial distribution. This process algebra provides a communication mechanism t…
Rings with common division, common meadows and their conditional equational theories
Jan A Bergstra, John V Tucker
We examine the consequences of having a total division operation on commutative rings. We consider two forms of binary division, one derived from a unary inverse, the…
A Complete Finite Axiomatisation of the Equational Theory of Common Meadows
Jan A Bergstra, John V Tucker
We analyse abstract data types that model numerical structures with a concept of error. Specifically, we focus on arithmetic data types that contain an error value whose mai…
Conditional logic as a short-circuit logic
Jan A. Bergstra, Alban Ponse
Three-valued conditional logic (CL) is defined by Guzmán and Squier (1990), and based on McCarthy's noncommutative connectives, axiomatises a short-circuit logic (SCL) that defines…
Using Hoare logic in a process algebra setting
J. A. Bergstra, C. A. Middelburg
This paper concerns the relation between process algebra and Hoare logic. We investigate the question whether and how a Hoare logic can be used for reasoning about how data change…
Propositional logic with short-circuit evaluation: a non-commutative and a commutative variant
Jan A. Bergstra, Alban Ponse, Daan J. C. Staudt
Short-circuit evaluation denotes the semantics of propositional connectives in which the second argument is evaluated only if the first argument does not suffice to determine the v…
On the complexity of the correctness problem for non-zeroness test instruction sequences
J. A. Bergstra, C. A. Middelburg
This paper concerns the question to what extent it can be efficiently determined whether an arbitrary program correctly solves a given problem. This question is investigated with p…
Process algebra with strategic interleaving
J. A. Bergstra, C. A. Middelburg
In process algebras such as ACP (Algebra of Communicating Processes), parallel processes are considered to be interleaved in an arbitrary way. In the case of multi-threading as fou…
Datatype defining rewrite systems for naturals and integers
Jan A. Bergstra, Alban Ponse
A datatype defining rewrite system (DDRS) is an algebraic (equational) specification intended to specify a datatype. When interpreting the equations from left-to-right, a DDRS defi…
Contradiction-tolerant process algebra with propositional signals
J. A. Bergstra, C. A. Middelburg
In a previous paper, an ACP-style process algebra was proposed in which propositions are used as the visible part of the state of processes and as state conditions under which proc…
Evaluation trees for proposition algebra
Jan A. Bergstra, Alban Ponse
Proposition algebra is based on Hoare's conditional connective, which is a ternary connective comparable to if-then-else and used in the setting of propositional logic. Conditional…
Note on paraconsistency and reasoning about fractions
Jan A. Bergstra, Inge Bethke
We apply a paraconsistent logic to reason about fractions.
Probabilistic thread algebra
J. A. Bergstra, C. A. Middelburg
We add probabilistic features to basic thread algebra and its extensions with thread-service interaction and strategic interleaving. Here, threads represent the behaviours produced…
A Hoare-like logic of asserted single-pass instruction sequences
J. A. Bergstra, C. A. Middelburg
We present a formal system for proving the partial correctness of a single-pass instruction sequence as considered in program algebra by decomposition into proofs of the partial co…
Three Datatype Defining Rewrite Systems for Datatypes of Integers each extending a Datatype of Naturals
Jan A. Bergstra, Alban Ponse
Integer arithmetic is specified according to three views: unary, binary, and decimal notation. The binary and decimal view have as their characteristic that each normal form resemb…
On algorithmic equivalence of instruction sequences for computing bit string functions
J. A. Bergstra, C. A. Middelburg
Every partial function from bit strings of a given length to bit strings of a possibly different given length can be computed by a finite instruction sequence that contains only in…
Network algebra for synchronous dataflow
J. A. Bergstra, C. A. Middelburg, Gh. Stefanescu
We develop an algebraic theory of synchronous dataflow networks. First, a basic algebraic theory of networks, called BNA (Basic Network Algebra), is introduced. This theory capture…
Process algebra with conditionals in the presence of epsilon
J. A. Bergstra, C. A. Middelburg
In a previous paper, we presented several extensions of ACP with conditional expressions, including one with a retrospection operator on conditions to allow for looking back on con…
Turing Impossibility Properties for Stack Machine Programming
J. A. Bergstra, C. A. Middelburg
The strong, intermediate, and weak Turing impossibility properties are introduced. Some facts concerning Turing impossibility for stack machine programming are trivially adapted fr…
Real Islamic Logic
Jan Aldert Bergstra
Four options for assigning a meaning to Islamic Logic are surveyed including a new proposal for an option named "Real Islamic Logic" (RIL). That approach to Islamic Logic should se…
On Hoare-McCarthy algebras
Jan A. Bergstra, Alban Ponse
We discuss an algebraic approach to propositional logic with side effects. To this end, we use Hoare's conditional [1985], which is a ternary connective comparable to if-then-else.…
Short-circuit logic
Jan A. Bergstra, A. Ponse, D. J. C. Staudt
Short-circuit evaluation denotes the semantics of propositional connectives in which the second argument is evaluated only if the first argument does not suffice to determine the v…
On the contribution of backward jumps to instruction sequence expressiveness
Jan A. Bergstra, Inge Bethke
We investigate the expressiveness of backward jumps in a framework of formalized sequential programming called program algebra. We show that - if expressiveness is measured in term…