Showing 1–50 of 70 results for author: Middelburg, C A

On the formalization of the notion of an interactive algorithm

Authors: C. A. Middelburg

Abstract: An earlier paper gives an account of a quest for a satisfactory formalization of the classical informal notion of an algorithm. In this paper, an attempt is made to generalize the results of that quest to the informal notion of an interactive algorithm. The notion of an interactive proto-algorithm is introduced. Interactive algorithms are expected to be equivalence classes of interactive proto-alg… ▽ More An earlier paper gives an account of a quest for a satisfactory formalization of the classical informal notion of an algorithm. In this paper, an attempt is made to generalize the results of that quest to the informal notion of an interactive algorithm. The notion of an interactive proto-algorithm is introduced. Interactive algorithms are expected to be equivalence classes of interactive proto-algorithms under an appropriate equivalence relation. As in the non-interactive case, three equivalence relations are defined. Two of them are deemed to be bounds for an appropriate equivalence relation and the third is likely an appropriate one. △ Less

Submitted 29 May, 2024; originally announced May 2024.

Comments: 16 pages, in Sections 2 and 3 there is text overlap with arXiv:2401.08366

ACM Class: F.1.1; F.2.0

The interdefinability of expansions of Belnap-Dunn logic

Authors: C. A. Middelburg

Abstract: Belnap-Dunn logic, also knows as the logic of First-Degree Entailment, is a logic that can serve as the underlying logic of theories that are inconsistent or incomplete. For various reasons, different expansions of Belnap-Dunn logic with non-classical connectives have been studied. This paper investigates the question whether those expansions are interdefinable with an expansion whose connectives… ▽ More Belnap-Dunn logic, also knows as the logic of First-Degree Entailment, is a logic that can serve as the underlying logic of theories that are inconsistent or incomplete. For various reasons, different expansions of Belnap-Dunn logic with non-classical connectives have been studied. This paper investigates the question whether those expansions are interdefinable with an expansion whose connectives include only classical connectives. This is worth knowing because it is difficult to say how close a logic with non-classical connectives is related to classical logic. The notion of interdefinability of logics used is based on a general notion of definability of a connective in a logic that seems to have been forgotten. △ Less

Submitted 7 March, 2024; originally announced March 2024.

Comments: 18 pages. arXiv admin note: text overlap with arXiv:2301.10555

MSC Class: 03B50 (Primary)

On the formalization of the notion of an algorithm

Authors: C. A. Middelburg

Abstract: The starting point of this paper is a collection of properties of an algorithm that have been distilled from the informal descriptions of what an algorithm is that are given in standard works from the mathematical and computer science literature. Based on that, the notion of a proto-algorithm is introduced. The thought is that algorithms are equivalence classes of proto-algorithms under some equiv… ▽ More The starting point of this paper is a collection of properties of an algorithm that have been distilled from the informal descriptions of what an algorithm is that are given in standard works from the mathematical and computer science literature. Based on that, the notion of a proto-algorithm is introduced. The thought is that algorithms are equivalence classes of proto-algorithms under some equivalence relation. Three equivalence relations are defined. Two of them give bounds between which an appropriate equivalence relation must lie. The third lies in between these two and is likely an appropriate equivalence relation. A sound method is presented to prove, using an imperative process algebra based on ACP, that this equivalence relation holds between two proto-algorithms. △ Less

Submitted 26 April, 2024; v1 submitted 16 January, 2024; originally announced January 2024.

Comments: 22 pages, revision of v1, presentation improved at several places and some minor errors corrected

ACM Class: F.1.1; F.2.0

Belnap-Dunn logic and query answering in inconsistent databases with null values

Authors: C. A. Middelburg

Abstract: This paper concerns an expansion of first-order Belnap-Dunn logic, named $\mathrm{BD}^{\supset,\mathsf{F}}$, and an application of this logic in the area of relational database theory. The notion of a relational database, the notion of a query applicable to a relational database, and several notions of an answer to a query with respect to a relational database are considered from the perspective o… ▽ More This paper concerns an expansion of first-order Belnap-Dunn logic, named $\mathrm{BD}^{\supset,\mathsf{F}}$, and an application of this logic in the area of relational database theory. The notion of a relational database, the notion of a query applicable to a relational database, and several notions of an answer to a query with respect to a relational database are considered from the perspective of this logic, taking into account that a database may be an inconsistent database or a database with null values. The chosen perspective enables among other things the definition of a notion of a consistent answer to a query with respect to a possibly inconsistent database without resort to database repairs. For each of the notions of an answer considered, being an answer to a query with respect to a database of the kind considered is decidable. △ Less

Submitted 1 July, 2023; v1 submitted 9 March, 2023; originally announced March 2023.

Comments: 26 pages; revision of v1, presentation improved at several places and DOIs added to the papers in the references. arXiv admin note: text overlap with arXiv:2301.10555

ACM Class: F.4.1; H.2.3; H.2.4

Journal ref: Scientific Annals of Computer Science vol. 33(2):159-192 (2023)

A conventional expansion of first-order Belnap-Dunn logic

Authors: C. A. Middelburg

Abstract: This paper concerns an expansion of first-order Belnap-Dunn logic whose connectives and quantifiers are all familiar from classical logic. The language and logical consequence relation of the logic are defined, a proof system for the defined logic is presented, and the soundness and completeness of the presented proof system is established. The close relationship between the logical consequence re… ▽ More This paper concerns an expansion of first-order Belnap-Dunn logic whose connectives and quantifiers are all familiar from classical logic. The language and logical consequence relation of the logic are defined, a proof system for the defined logic is presented, and the soundness and completeness of the presented proof system is established. The close relationship between the logical consequence relations of the defined logic and the version of classical logic with the same language is illustrated by the minor differences between the presented proof system and a sound and complete proof system for the version of classical logic with the same language. Moreover, fifteen classical laws of logical equivalence are given by which the logical equivalence relation of the defined logic distinguishes itself from the logical equivalence relation of many logics that are closely related at first glance. △ Less

Submitted 8 March, 2024; v1 submitted 25 January, 2023; originally announced January 2023.

Comments: 18 pages, major revision of version v5 (the study of the interdefinability of expansions of Belnap-Dunn logic moved to arXiv:2403.04641)

MSC Class: 03B50 (Primary)

Paraconsistent logic and query answering in inconsistent databases

Authors: C. A. Middelburg

Abstract: This paper concerns the paraconsistent logic LPQ$^{\supset,\mathsf{F}}$ and an application of it in the area of relational database theory. The notions of a relational database, a query applicable to a relational database, and a consistent answer to a query with respect to a possibly inconsistent relational database are considered from the perspective of this logic. This perspective enables among… ▽ More This paper concerns the paraconsistent logic LPQ$^{\supset,\mathsf{F}}$ and an application of it in the area of relational database theory. The notions of a relational database, a query applicable to a relational database, and a consistent answer to a query with respect to a possibly inconsistent relational database are considered from the perspective of this logic. This perspective enables among other things the definition of a consistent answer to a query with respect to a possibly inconsistent database without resort to database repairs. In a previous paper, LPQ$^{\supset,\mathsf{F}}$ is presented with a sequent-style natural deduction proof system. In this paper, a sequent calculus proof system is presented because it is common to use a sequent calculus proof system as the basis of proof search procedures and such procedures may form the core of algorithms for computing consistent answers to queries. △ Less

Submitted 11 March, 2023; v1 submitted 27 August, 2022; originally announced August 2022.

Comments: 21 pages; revision of v4, some inaccuracies removed and material streamlined at several places. arXiv admin note: substantial text overlap with arXiv:2303.05264

ACM Class: F.4.1; H.2.3; H.2.4

Journal ref: Journal of Applied Non-Classical Logics 34(1):133-154 (2024)

Imperative process algebra and models of computation

Authors: C. A. Middelburg

Abstract: Studies of issues related to computability and computational complexity involve the use of a model of computation. Pivotal to such a model are the computational processes considered. Processes of this kind can be described using an imperative process algebra based on ACP (Algebra of Communicating Processes). In this paper, it is investigated whether the imperative process algebra concerned can pla… ▽ More Studies of issues related to computability and computational complexity involve the use of a model of computation. Pivotal to such a model are the computational processes considered. Processes of this kind can be described using an imperative process algebra based on ACP (Algebra of Communicating Processes). In this paper, it is investigated whether the imperative process algebra concerned can play a role in the field of models of computation.It is demonstrated that the process algebra is suitable to describe in a mathematically precise way models of computation corresponding to existing models based on sequential, asynchronous parallel, and synchronous parallel random access machines as well as time and work complexity measures for those models. A probabilistic variant of the model based on sequential random access machines and complexity measures for it are also described. △ Less

Submitted 12 July, 2023; v1 submitted 6 June, 2022; originally announced June 2022.

Comments: 47 pages; revision of v2, presentation improved at many places and section on probabilistic computation added

ACM Class: D.1.3; F.1.1; F.1.2; F.1.3

Journal ref: Theory of Computing Systems, 68(3):529--570, 2024

Dormancy-aware timed branching bisimilarity, with an application to communication protocol analysis

Authors: C. A. Middelburg

Abstract: A variant of the standard notion of branching bisimilarity for processes with discrete relative timing is proposed which is coarser than the standard notion. Using a version of ACP (Algebra of Communicating Processes) with abstraction for processes with discrete relative timing, it is shown that the proposed variant allows of both the functional correctness and the performance properties of the PA… ▽ More A variant of the standard notion of branching bisimilarity for processes with discrete relative timing is proposed which is coarser than the standard notion. Using a version of ACP (Algebra of Communicating Processes) with abstraction for processes with discrete relative timing, it is shown that the proposed variant allows of both the functional correctness and the performance properties of the PAR (Positive Acknowledgement with Retransmission) protocol to be analyzed. In the version of ACP concerned, the difference between the standard notion of branching bisimilarity and its proposed variant is characterized by a single axiom schema. △ Less

Submitted 9 August, 2023; v1 submitted 19 July, 2021; originally announced July 2021.

Comments: 39 pages, revision of v3, presentation improved at several places

ACM Class: C.2.2; D.1.3; D.2.4; F.1.2; F.3.1

Journal ref: Theoretical Computer Science vol. 2008, 2024

Imperative process algebra with abstraction

Authors: C. A. Middelburg

Abstract: This paper introduces an imperative process algebra based on ACP (Algebra of Communicating Processes). Like other imperative process algebras, this process algebra deals with processes of the kind that arises from the execution of imperative programs. It distinguishes itself from already existing imperative process algebras among other things by supporting abstraction from actions that are conside… ▽ More This paper introduces an imperative process algebra based on ACP (Algebra of Communicating Processes). Like other imperative process algebras, this process algebra deals with processes of the kind that arises from the execution of imperative programs. It distinguishes itself from already existing imperative process algebras among other things by supporting abstraction from actions that are considered not to be visible. The support of abstraction of this kind opens interesting application possibilities of the process algebra. This paper goes briefly into the possibility of information-flow security analysis of the kind that is concerned with the leakage of confidential data. For the presented axiomatization, soundness and semi-completeness results with respect to a notion of branching bisimulation equivalence are established. △ Less

Submitted 21 May, 2022; v1 submitted 14 March, 2021; originally announced March 2021.

Comments: 33 pages, a polished revision of v4

ACM Class: D.2.4; D.4.6; F.1.1; F.1.2; F.3.1

Journal ref: Scientific Annals of Computer Science 32(1):137--179, 2022

A classical-logic view of a paraconsistent logic

Authors: C. A. Middelburg

Abstract: This paper is concerned with the first-order paraconsistent logic LPQ$^{\supset,\mathsf{F}}$. A sequent-style natural deduction proof system for this logic is presented and, for this proof system, both a model-theoretic justification and a logical justification by means of an embedding into first-order classical logic is given. For no logic that is essentially the same as LPQ… ▽ More This paper is concerned with the first-order paraconsistent logic LPQ$^{\supset,\mathsf{F}}$. A sequent-style natural deduction proof system for this logic is presented and, for this proof system, both a model-theoretic justification and a logical justification by means of an embedding into first-order classical logic is given. For no logic that is essentially the same as LPQ$^{\supset,\mathsf{F}}$, a natural deduction proof system is currently available in the literature. The given embedding provides both a classical-logic explanation of this logic and a logical justification of its proof system. The major properties of LPQ$^{\supset,\mathsf{F}}$ are also treated. △ Less

Submitted 12 January, 2023; v1 submitted 17 August, 2020; originally announced August 2020.

Comments: 17 pages, error in the distinguishing laws of logical equivalence corrected

MSC Class: 03B53 (Primary) 03B10; 03B50 (Secondary)

Program algebra for random access machine programs

Authors: C. A. Middelburg

Abstract: This paper presents an algebraic theory of instruction sequences with instructions for a random access machine (RAM) as basic instructions, the behaviours produced by the instruction sequences concerned under execution, and the interaction between such behaviours and RAM memories. This theory provides a setting for the development of theory in areas such as computational complexity and analysis of… ▽ More This paper presents an algebraic theory of instruction sequences with instructions for a random access machine (RAM) as basic instructions, the behaviours produced by the instruction sequences concerned under execution, and the interaction between such behaviours and RAM memories. This theory provides a setting for the development of theory in areas such as computational complexity and analysis of algorithms that distinguishes itself by offering the possibility of equational reasoning to establish whether an instruction sequence computes a given function and being more general than the setting provided by any known version of the RAM model of computation. In this setting, a semi-realistic version of the RAM model of computation and a bit-oriented time complexity measure for this version are introduced. Under the time measure concerned, semi-realistic RAMs can be simulated by multi-tape Turing machines with quadratic time overhead. △ Less

Submitted 22 November, 2022; v1 submitted 20 July, 2020; originally announced July 2020.

Comments: 27 pages, revision of v2 with presentation improved. arXiv admin note: substantial text overlap with arXiv:1901.08840, arXiv:1808.04264

ACM Class: D.1.4; E.3; F.1.1; F.1.3

Journal ref: Scientific Annals of Computer Science 32(2):285-319 (2022)

On infinite guarded recursive specifications in process algebra

Authors: R. J. van Glabbeek, C. A. Middelburg

Abstract: In most presentations of ACP with guarded recursion, recursive specifications are finite or infinite sets of recursion equations of which the right-hand sides are guarded terms. The completeness with respect to bisimulation equivalence of the axioms of ACP with guarded recursion has only been proved for the special case where recursive specifications are finite sets of recursion equations of which… ▽ More In most presentations of ACP with guarded recursion, recursive specifications are finite or infinite sets of recursion equations of which the right-hand sides are guarded terms. The completeness with respect to bisimulation equivalence of the axioms of ACP with guarded recursion has only been proved for the special case where recursive specifications are finite sets of recursion equations of which the right-hand sides are guarded terms of a restricted form known as linear terms. In this note, we widen this completeness result to the general case. △ Less

Submitted 2 May, 2020; originally announced May 2020.

Comments: 9 pages, there is text overlap with earlier papers (arXiv:1703.06822, arXiv:1912.10041, arXiv:2003.00473)

ACM Class: F.1.2; F.4.1

Process algebra, process scheduling, and mutual exclusion

Authors: C. A. Middelburg

Abstract: In the case of multi-threading as found in contemporary programming languages, parallel processes are interleaved according to what is known as a process-scheduling policy in the field of operating systems. In a previous paper, we extend ACP with this form of interleaving. In the current paper, we do so with the variant of ACP known as ACP$_ε$. The choice of ACP$_ε$ stems from the need to cover mo… ▽ More In the case of multi-threading as found in contemporary programming languages, parallel processes are interleaved according to what is known as a process-scheduling policy in the field of operating systems. In a previous paper, we extend ACP with this form of interleaving. In the current paper, we do so with the variant of ACP known as ACP$_ε$. The choice of ACP$_ε$ stems from the need to cover more process-scheduling policies. We show that a process-scheduling policy supporting mutual exclusion of critical subprocesses is now covered. △ Less

Submitted 21 April, 2020; v1 submitted 1 March, 2020; originally announced March 2020.

Comments: 15 pages, there is noticeable text overlap with earlier papers (arXiv:1912.10041, arXiv:1703.06822); 15 pages, Section 3.2 improved; 15 pages, minor improvements including replacement of reference at end Section 3.2

ACM Class: D.1.3; D.4.1; F.1.2

Probabilistic process algebra and strategic interleaving

Authors: C. A. Middelburg

Abstract: We first present a probabilistic version of ACP that rests on the principle that probabilistic choices are always resolved before choices involved in alternative composition and parallel composition are resolved and then extend this probabilistic version of ACP with a form of interleaving in which parallel processes are interleaved according to what is known as a process-scheduling policy in the f… ▽ More We first present a probabilistic version of ACP that rests on the principle that probabilistic choices are always resolved before choices involved in alternative composition and parallel composition are resolved and then extend this probabilistic version of ACP with a form of interleaving in which parallel processes are interleaved according to what is known as a process-scheduling policy in the field of operating systems. We use the term strategic interleaving for this more constrained form of interleaving. The extension covers probabilistic process-scheduling policies. △ Less

Submitted 8 September, 2020; v1 submitted 20 December, 2019; originally announced December 2019.

Comments: 30 pages, major revision with adaptation of example from arXiv:2003.00473 incorporated (also text overlap with arXiv:1703.06822)

ACM Class: D.1.3; D.4.1; F.1.2

Journal ref: Scientific Annals of Computer Science 30(2):205--243 (2020)

Using Hoare logic in a process algebra setting

Authors: J. A. Bergstra, C. A. Middelburg

Abstract: 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 in the course of a process when reasoning equationally about that process. We introduce an extension of ACP (Algebra of Communicating Processes) with features that are relevant to processes in which data are involved, pr… ▽ More 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 in the course of a process when reasoning equationally about that process. We introduce an extension of ACP (Algebra of Communicating Processes) with features that are relevant to processes in which data are involved, present a Hoare logic for the processes considered in this process algebra, and discuss the use of this Hoare logic as a complement to pure equational reasoning with the equational axioms of the process algebra. △ Less

Submitted 13 October, 2020; v1 submitted 11 June, 2019; originally announced June 2019.

Comments: 24 pages; presentation improved, examples added

ACM Class: D.1.3; D.1.4; D.2.4; F.1.2; F.3.1

Journal ref: Fundamenta Informaticae 179(4):321--344, 2021

Program algebra for Turing-machine programs

Authors: J. A. Bergstra, C. A. Middelburg

Abstract: This paper presents an algebraic theory of instruction sequences with instructions for Turing tapes as basic instructions, the behaviours produced by the instruction sequences concerned under execution, and the interaction between such behaviours and Turing tapes provided by an execution environment. This theory provides a setting for the development of theory in areas such as computability and co… ▽ More This paper presents an algebraic theory of instruction sequences with instructions for Turing tapes as basic instructions, the behaviours produced by the instruction sequences concerned under execution, and the interaction between such behaviours and Turing tapes provided by an execution environment. This theory provides a setting for the development of theory in areas such as computability and computational complexity that distinguishes itself by offering the possibility of equational reasoning and being more general than the setting provided by a known version of the Turing-machine model of computation. The theory is essentially an instantiation of a parameterized algebraic theory which is the basis of a line of research in which issues relating to a wide variety of subjects from computer science have been rigorously investigated thinking in terms of instruction sequences. △ Less

Submitted 7 December, 2019; v1 submitted 25 January, 2019; originally announced January 2019.

Comments: 19 pages, Sect. 2--4 are largely shortened versions of Sect. 2--4 of arXiv:1808.04264, which, in turn, draw from preliminary sections of several earlier papers; 21 pages, some remarks in Sect.1 and Sect.10 added

ACM Class: F.1.1; F.1.3; F.4.1

Journal ref: Scientific Annals of Computer Science 29(2):113--139 (2019)

A short introduction to program algebra with instructions for Boolean registers

Authors: J. A. Bergstra, C. A. Middelburg

Abstract: A parameterized algebraic theory of instruction sequences, objects that represent the behaviours produced by instruction sequences under execution, and objects that represent the behaviours exhibited by the components of the execution environment of instruction sequences is the basis of a line of research in which issues relating to a wide variety of subjects from computer science have been rigoro… ▽ More A parameterized algebraic theory of instruction sequences, objects that represent the behaviours produced by instruction sequences under execution, and objects that represent the behaviours exhibited by the components of the execution environment of instruction sequences is the basis of a line of research in which issues relating to a wide variety of subjects from computer science have been rigorously investigated thinking in terms of instruction sequences. In various papers that belong to this line of research, use is made of an instantiation of this theory in which the basic instructions are instructions to read out and alter the content of Boolean registers and the components of the execution environment are Boolean registers. In this paper, we give a simplified presentation of the most general such instantiated theory. △ Less

Submitted 2 September, 2018; v1 submitted 13 August, 2018; originally announced August 2018.

Comments: 21 pages, this paper is to a large extent a compilation of material from several earlier publications; 23 pages, presentation improved and section on uses for the theory added. arXiv admin note: text overlap with arXiv:1702.03511

ACM Class: F.1.1; F.3.2; F.4.1

Journal ref: Computer Science Journal of Moldova, 26(3):199--232, 2018

On the complexity of the correctness problem for non-zeroness test instruction sequences

Authors: J. A. Bergstra, C. A. Middelburg

Abstract: 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 programs of a very simple form, namely instruction sequences, and a very simple problem, namely the non-zeroness test on natural numbers. The instruction sequences concerned are of a kind by which, for each $n > 0$, each… ▽ More 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 programs of a very simple form, namely instruction sequences, and a very simple problem, namely the non-zeroness test on natural numbers. The instruction sequences concerned are of a kind by which, for each $n > 0$, each function from $\{0,1\}^n$ to $\{0,1\}$ can be computed. The established results include the time complexities of the problem of determining whether an arbitrary instruction sequence correctly implements the restriction to $\{0,1\}^n$ of the function from $\{0,1\}^*$ to $\{0,1\}$ that models the non-zeroness test function, for $n > 0$, under several restrictions on the arbitrary instruction sequence. △ Less

Submitted 26 February, 2019; v1 submitted 15 May, 2018; originally announced May 2018.

Comments: 32 pages, minor revision with several obscurities made clear

ACM Class: D.2.4; F.1.1; F.1.3

Journal ref: Theoretical Computer Science, 802:1--18, 2020

Process algebra with strategic interleaving

Authors: J. A. Bergstra, C. A. Middelburg

Abstract: 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 found in contemporary programming languages, parallel processes are actually interleaved according to some interleaving strategy. An interleaving strategy is what is called a process-scheduling policy in the field of operat… ▽ More 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 found in contemporary programming languages, parallel processes are actually interleaved according to some interleaving strategy. An interleaving strategy is what is called a process-scheduling policy in the field of operating systems. In many systems, for instance hardware/software systems, we have to do with both parallel processes that may best be considered to be interleaved in an arbitrary way and parallel processes that may best be considered to be interleaved according to some interleaving strategy. Therefore, we extend ACP in this paper with the latter form of interleaving. The established properties of the extension concerned include an elimination property, a conservative extension property, and a unique expansion property. △ Less

Submitted 21 April, 2020; v1 submitted 20 March, 2017; originally announced March 2017.

Comments: 19 pages, this version is a revision of the published version

ACM Class: D.1.3; D.4.1; F.1.2

Journal ref: Theory of Computing Systems, 63(3):488--505, 2019

Axioms for behavioural congruence of single-pass instruction sequences

Authors: J. A. Bergstra, C. A. Middelburg

Abstract: In program algebra, an algebraic theory of single-pass instruction sequences, three congruences on instruction sequences are paid attention to: instruction sequence congruence, structural congruence, and behavioural congruence. Sound and complete axiom systems for the first two congruences were already given in early papers on program algebra. The current paper is the first one that is concerned w… ▽ More In program algebra, an algebraic theory of single-pass instruction sequences, three congruences on instruction sequences are paid attention to: instruction sequence congruence, structural congruence, and behavioural congruence. Sound and complete axiom systems for the first two congruences were already given in early papers on program algebra. The current paper is the first one that is concerned with an axiom system for the third congruence. The presented axiom system is especially notable for its axioms that have to do with forward jump instructions. △ Less

Submitted 22 November, 2017; v1 submitted 12 February, 2017; originally announced February 2017.

Comments: 19 pages, this paper draws somewhat from the preliminaries of arXiv:1502.00238 [cs.PL] and some earlier papers; some remarks added and some remarks reformulated

ACM Class: D.3.1; F.3.1; F.3.2

Journal ref: Scientific Annals of Computer Science 27(2):111--135 (2017)

On the strongest three-valued paraconsistent logic contained in classical logic and its dual

Authors: C. A. Middelburg

Abstract: LP$^{\supset,\mathsf{F}}$ is a three-valued paraconsistent propositional logic which is essentially the same as J3. It has most properties that have been proposed as desirable properties of a reasonable paraconsistent propositional logic. However, it follows easily from already published results that there are exactly 8192 different three-valued paraconsistent propositional logics that have the pr… ▽ More LP$^{\supset,\mathsf{F}}$ is a three-valued paraconsistent propositional logic which is essentially the same as J3. It has most properties that have been proposed as desirable properties of a reasonable paraconsistent propositional logic. However, it follows easily from already published results that there are exactly 8192 different three-valued paraconsistent propositional logics that have the properties concerned. In this paper, properties concerning the logical equivalence relation of a logic are used to distinguish LP$^{\supset,\mathsf{F}}$ from the others. As one of the bonuses of focussing on the logical equivalence relation, it is found that only 32 of the 8192 logics have a logical equivalence relation that satisfies the identity, annihilation, idempotent, and commutative laws for conjunction and disjunction. For most properties of LP$^{\supset,\mathsf{F}}$ that have been proposed as desirable properties of a reasonable paraconsistent propositional logic, its paracomplete analogue has a comparable property. In this paper, properties concerning the logical equivalence relation of a logic are also used to distinguish the paracomplete analogue of LP$^{\supset,\mathsf{F}}$ from the other three-valued paracomplete propositional logics with those comparable properties. △ Less

Submitted 1 December, 2020; v1 submitted 11 February, 2017; originally announced February 2017.

Comments: 17 pages, version that is accepted for publication, there is some text overlap between this paper and arXiv:1508.06899 [cs.LO]

MSC Class: 03B53 (Primary) 03B50; 03B70 (Secondary)

Journal ref: Journal of Logic and Computation, 31(2):597--611, 2021

A short introduction to process theory

Authors: C. A. Middelburg

Abstract: These lecture notes concern the basics of the theory of process behaviour. First the concept of a (labelled) transition system receives ample treatment and then the following issues concerning process behaviour are elaborated in the setting of transition systems: (i) concurrency and interaction, (ii) abstraction, (iii) sequential composition, alternative composition, and iteration, (iv) expression… ▽ More These lecture notes concern the basics of the theory of process behaviour. First the concept of a (labelled) transition system receives ample treatment and then the following issues concerning process behaviour are elaborated in the setting of transition systems: (i) concurrency and interaction, (ii) abstraction, (iii) sequential composition, alternative composition, and iteration, (iv) expressions that represent process behaviours, and (v) structural operational semantics and equational laws for such expressions. To quicken an intuitive understanding, direct connections with programs and automata are established wherever appropriate. For the interested reader, direct connections with Petri nets are also established. In each chapter, except the last one, it shows that what has been dealt with so far still has certain limitations. Each time, the next chapter is devoted to reducing the limitations concerned. △ Less

Submitted 3 October, 2016; originally announced October 2016.

Comments: 130 pages

Transformation of fractions into simple fractions in divisive meadows

Authors: J. A. Bergstra, C. A. Middelburg

Abstract: Meadows are alternatives for fields with a purely equational axiomatization. At the basis of meadows lies the decision to make the multiplicative inverse operation total by imposing that the multiplicative inverse of zero is zero. Divisive meadows are meadows with the multiplicative inverse operation replaced by a division operation. Viewing a fraction as a term over the signature of divisive mead… ▽ More Meadows are alternatives for fields with a purely equational axiomatization. At the basis of meadows lies the decision to make the multiplicative inverse operation total by imposing that the multiplicative inverse of zero is zero. Divisive meadows are meadows with the multiplicative inverse operation replaced by a division operation. Viewing a fraction as a term over the signature of divisive meadows that is of the form p / q, we investigate which divisive meadows admit transformation of fractions into simple fractions, i.e. fractions without proper subterms that are fractions. △ Less

Submitted 25 February, 2016; v1 submitted 21 October, 2015; originally announced October 2015.

Comments: 23 pages; one theorem and two corollaries of it added at end of Sect. 5; some minor errors corrected

MSC Class: 12E12; 12L12; 68Q65

Journal ref: Journal of Applied Logic, 16:92--110, 2016

Contradiction-tolerant process algebra with propositional signals

Authors: J. A. Bergstra, C. A. Middelburg

Abstract: 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 processes may proceed. This process algebra, called ACPps, is built on classical propositional logic. In this paper, we present a version of ACPps built on a paraconsistent propositional logic which is essentially the same a… ▽ More 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 processes may proceed. This process algebra, called ACPps, is built on classical propositional logic. In this paper, we present a version of ACPps built on a paraconsistent propositional logic which is essentially the same as CLuNs. There are many systems that would have to deal with self-contradictory states if no special measures were taken. For a number of these systems, it is conceivable that accepting self-contradictory states and dealing with them in a way based on a paraconsistent logic is an alternative to taking special measures. The presented version of ACPps can be suited for the description and analysis of systems that deal with self-contradictory states in a way based on the above-mentioned paraconsistent logic. △ Less

Submitted 19 March, 2017; v1 submitted 27 August, 2015; originally announced August 2015.

Comments: 25 pages; 26 pages, occurrences of wrong symbol for bisimulation equivalence replaced; 26 pages, Proposition 1 added; 27 pages, explanation of the phrase 'in contradiction' added to section 2 and presentation of the completeness result in section 2 improved; 27 pages, uniqueness result in section 2 revised; 27 pages, last paragraph of section 8 revised

ACM Class: D.2.1; D.2.4; F.3.1; F.4.1

Journal ref: Fundamenta Informaticae, 153(1-2): 29-55 (2017)

On instruction sets for Boolean registers in program algebra

Authors: J. A. Bergstra, C. A. Middelburg

Abstract: In previous work carried out in the setting of program algebra, including work in the area of instruction sequence size complexity, we chose instruction sets for Boolean registers that contain only instructions of a few of the possible kinds. In the current paper, we study instruction sequence size bounded functional completeness of all possible instruction sets for Boolean registers. We expect th… ▽ More In previous work carried out in the setting of program algebra, including work in the area of instruction sequence size complexity, we chose instruction sets for Boolean registers that contain only instructions of a few of the possible kinds. In the current paper, we study instruction sequence size bounded functional completeness of all possible instruction sets for Boolean registers. We expect that the results of this study will turn out to be useful to adequately assess results of work that is concerned with lower bounds of instruction sequence size complexity. △ Less

Submitted 6 June, 2016; v1 submitted 1 February, 2015; originally announced February 2015.

Comments: 18 pages, the preliminaries are largely the same as the preliminaries in arXiv:1402.4950 [cs.PL] and some earlier papers; 21 pages, presentation improved

ACM Class: F.1.1; F.1.3

Journal ref: Scientific Annals of Computer Science 26(1):1--26, 2016

Instruction sequence size complexity of parity

Authors: J. A. Bergstra, C. A. Middelburg

Abstract: Each Boolean function can be computed by a single-pass instruction sequence that contains only instructions to set and get the content of Boolean registers, forward jump instructions, and a termination instruction. Auxiliary Boolean registers are not necessary for this. In the current paper, we show that, in the case of the parity functions, shorter instruction sequences are possible with the use… ▽ More Each Boolean function can be computed by a single-pass instruction sequence that contains only instructions to set and get the content of Boolean registers, forward jump instructions, and a termination instruction. Auxiliary Boolean registers are not necessary for this. In the current paper, we show that, in the case of the parity functions, shorter instruction sequences are possible with the use of an auxiliary Boolean register in the presence of instructions to complement the content of auxiliary Boolean registers. This result supports, in a setting where programs are instruction sequences acting on Boolean registers, a basic intuition behind the storage of auxiliary data, namely the intuition that this makes possible a reduction of the size of a program. △ Less

Submitted 15 July, 2016; v1 submitted 21 December, 2014; originally announced December 2014.

Comments: 12 pages, the preliminaries are largely the same as the preliminaries in arXiv:1312.1812 [cs.PL] and some earlier papers; 13 pages, minor errors corrected; 13 pages, presentation improved; 14 pages, remarks about related work added; 14 pages, presentation improved

ACM Class: F.1.1; F.1.3

Journal ref: Fundamenta Informaticae, 149(3):297--309, 2016

Probabilistic thread algebra

Authors: J. A. Bergstra, C. A. Middelburg

Abstract: We add probabilistic features to basic thread algebra and its extensions with thread-service interaction and strategic interleaving. Here, threads represent the behaviours produced by instruction sequences under execution and services represent the behaviours exhibited by the components of execution environments of instruction sequences. In a paper concerned with probabilistic instruction sequence… ▽ More We add probabilistic features to basic thread algebra and its extensions with thread-service interaction and strategic interleaving. Here, threads represent the behaviours produced by instruction sequences under execution and services represent the behaviours exhibited by the components of execution environments of instruction sequences. In a paper concerned with probabilistic instruction sequences, we proposed several kinds of probabilistic instructions and gave an informal explanation for each of them. The probabilistic features added to the extension of basic thread algebra with thread-service interaction make it possible to give a formal explanation in terms of non-probabilistic instructions and probabilistic services. The probabilistic features added to the extensions of basic thread algebra with strategic interleaving make it possible to cover strategies corresponding to probabilistic scheduling algorithms. △ Less

Submitted 22 July, 2015; v1 submitted 24 September, 2014; originally announced September 2014.

Comments: 25 pages (arXiv admin note: text overlap with arXiv:1408.2955, arXiv:1402.4950); some simplifications made; substantially revised

ACM Class: D.3.3; D.4.1; F.1.1; F.1.2

Journal ref: Scientific Annals of Computer Science 25(2):211--243, 2015

A Hoare-like logic of asserted single-pass instruction sequences

Authors: J. A. Bergstra, C. A. Middelburg

Abstract: 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 correctness of segments of the single-pass instruction sequence concerned. The system is similar to Hoare logics, but takes into account that, by the presence of jump instructions, segments of single-pass instruction seque… ▽ More 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 correctness of segments of the single-pass instruction sequence concerned. The system is similar to Hoare logics, but takes into account that, by the presence of jump instructions, segments of single-pass instruction sequences may have multiple entry points and multiple exit points. It is intended to support a sound general understanding of the issues with Hoare-like logics for low-level programming languages. △ Less

Submitted 3 May, 2017; v1 submitted 13 August, 2014; originally announced August 2014.

Comments: 22 pages, the preliminaries have textual overlaps with the preliminaries in arXiv:1402.4950 [cs.LO] and earlier papers; introduction and conclusions rewritten, explanatory remarks added; introduction partly rewritten; 24 pages, clarifying examples added

ACM Class: D.2.4; F.3.1

Journal ref: Scientific Annals of Computer Science, 26(2):125--156 (2016)

Division by zero in non-involutive meadows

Authors: J. A. Bergstra, C. A. Middelburg

Abstract: Meadows have been proposed as alternatives for fields with a purely equational axiomatization. At the basis of meadows lies the decision to make the multiplicative inverse operation total by imposing that the multiplicative inverse of zero is zero. Thus, the multiplicative inverse operation of a meadow is an involution. In this paper, we study `non-involutive meadows', i.e.\ variants of meadows in… ▽ More Meadows have been proposed as alternatives for fields with a purely equational axiomatization. At the basis of meadows lies the decision to make the multiplicative inverse operation total by imposing that the multiplicative inverse of zero is zero. Thus, the multiplicative inverse operation of a meadow is an involution. In this paper, we study `non-involutive meadows', i.e.\ variants of meadows in which the multiplicative inverse of zero is not zero, and pay special attention to non-involutive meadows in which the multiplicative inverse of zero is one. △ Less

Submitted 9 June, 2014; originally announced June 2014.

Comments: 14 pages

MSC Class: 12E12; 12L12; 68Q65

Journal ref: Journal of Applied Logic, 13(1):1--12, 2015

On algorithmic equivalence of instruction sequences for computing bit string functions

Authors: J. A. Bergstra, C. A. Middelburg

Abstract: 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 instructions to set and get the content of Boolean registers, forward jump instructions, and a termination instruction. We look for an equivalence relation on instruction sequences of this kind that captures to a reasonabl… ▽ More 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 instructions to set and get the content of Boolean registers, forward jump instructions, and a termination instruction. We look for an equivalence relation on instruction sequences of this kind that captures to a reasonable degree the intuitive notion that two instruction sequences express the same algorithm. △ Less

Submitted 5 February, 2015; v1 submitted 20 February, 2014; originally announced February 2014.

Comments: 27 pages, the preliminaries have textual overlaps with the preliminaries in arXiv:1308.0219 [cs.PL], arXiv:1312.1529 [cs.PL], and arXiv:1312.1812 [cs.PL]; 27 pages, three paragraphs about Milner's algorithmic equivalence hypothesis added to concluding remarks; 26 pages, several minor improvements of the presentation made

ACM Class: F.1.1; F.2.0

Journal ref: Fundamenta Informaticae, 138(4):411--434, 2015

Long multiplication by instruction sequences with backward jump instructions

Authors: J. A. Bergstra, C. A. Middelburg

Abstract: For each function on bit strings, its restriction to bit strings of any given length can be computed by a finite instruction sequence that contains only instructions to set and get the content of Boolean registers, forward jump instructions, and a termination instruction. Backward jump instructions are not necessary for this, but instruction sequences can be significantly shorter with them. We tak… ▽ More For each function on bit strings, its restriction to bit strings of any given length can be computed by a finite instruction sequence that contains only instructions to set and get the content of Boolean registers, forward jump instructions, and a termination instruction. Backward jump instructions are not necessary for this, but instruction sequences can be significantly shorter with them. We take the function on bit strings that models the multiplication of natural numbers on their representation in the binary number system to demonstrate this by means of a concrete example. The example is reason to discuss points concerning the halting problem and the concept of an algorithm. △ Less

Submitted 6 April, 2014; v1 submitted 6 December, 2013; originally announced December 2013.

Comments: 17 pages, the preliminaries are about the same as the preliminaries in arXiv:1308.0219 [cs.PL] and arXiv:1312.1529 [cs.PL]; minor errors corrected, references added; section on indirect addressing added

ACM Class: F.1.1; F.2.1

Instruction sequences expressing multiplication algorithms

Authors: J. A. Bergstra, C. A. Middelburg

Abstract: For each function on bit strings, its restriction to bit strings of any given length can be computed by a finite instruction sequence that contains only instructions to set and get the content of Boolean registers, forward jump instructions, and a termination instruction. We describe instruction sequences of this kind that compute the function on bit strings that models multiplication on natural n… ▽ More For each function on bit strings, its restriction to bit strings of any given length can be computed by a finite instruction sequence that contains only instructions to set and get the content of Boolean registers, forward jump instructions, and a termination instruction. We describe instruction sequences of this kind that compute the function on bit strings that models multiplication on natural numbers less than $2^N$ with respect to their binary representation by bit strings of length $N$, for a fixed but arbitrary $N > 0$, according to the long multiplication algorithm and the Karatsuba multiplication algorithm. We find among other things that the instruction sequence expressing the former algorithm is longer than the one expressing the latter algorithm only if the length of the bit strings involved is greater than $2^8$. We also go into the use of an instruction sequence with backward jump instructions for expressing the long multiplication algorithm. This leads to an instruction sequence that it is shorter than the other two if the length of the bit strings involved is greater than $2$. △ Less

Submitted 1 July, 2018; v1 submitted 5 December, 2013; originally announced December 2013.

Comments: 14 pages, the preliminaries of this paper and arXiv:1308.0219 are the same; 16 pages, results sharpened and presentation improved; 22 pages, combined with arXiv:1312.1812; 22 pages, typos corrected and explanation added

ACM Class: F.1.1; F.2.1

Journal ref: Scientific Annals of Computer Science 28(1):39--66, 2018

Instruction sequence expressions for the secure hash algorithm SHA-256

Authors: J. A. Bergstra, C. A. Middelburg

Abstract: The secure hash function SHA-256 is a function on bit strings. This means that its restriction to the bit strings of any given length can be computed by a finite instruction sequence that contains only instructions to set and get the content of Boolean registers, forward jump instructions, and a termination instruction. We describe such instruction sequences for the restrictions to bit strings of… ▽ More The secure hash function SHA-256 is a function on bit strings. This means that its restriction to the bit strings of any given length can be computed by a finite instruction sequence that contains only instructions to set and get the content of Boolean registers, forward jump instructions, and a termination instruction. We describe such instruction sequences for the restrictions to bit strings of the different possible lengths by means of uniform terms from an algebraic theory. △ Less

Submitted 18 November, 2017; v1 submitted 1 August, 2013; originally announced August 2013.

Comments: 14 pages; several minor errors corrected; counting error corrected; instruction sequence fault repaired; misunderstanding cleared up; a minor error corrected; 15 pages, presentation improved, a minor error corrected. preliminaries have text overlap with arXiv:1301.3297

ACM Class: E.3; F.1.1

Network algebra for synchronous dataflow

Authors: J. A. Bergstra, C. A. Middelburg, Gh. Stefanescu

Abstract: 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 captures the basic algebraic properties of networks. For synchronous dataflow networks, it is subsequently extended with additional constants for the branching connections that occur between the cells of synchronous dataflow ne… ▽ More 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 captures the basic algebraic properties of networks. For synchronous dataflow networks, it is subsequently extended with additional constants for the branching connections that occur between the cells of synchronous dataflow networks and axioms for these additional constants. We also give two models of the resulting theory, the one based on stream transformers and the other based on processes as considered in process algebra. △ Less

Submitted 2 March, 2013; originally announced March 2013.

Comments: 24 pages

ACM Class: F.1.1; F.1.2

Instruction sequence based non-uniform complexity classes

Authors: J. A. Bergstra, C. A. Middelburg

Abstract: We present an approach to non-uniform complexity in which single-pass instruction sequences play a key part, and answer various questions that arise from this approach. We introduce several kinds of non-uniform complexity classes. One kind includes a counterpart of the well-known non-uniform complexity class P/poly and another kind includes a counterpart of the well-known non-uniform complexity cl… ▽ More We present an approach to non-uniform complexity in which single-pass instruction sequences play a key part, and answer various questions that arise from this approach. We introduce several kinds of non-uniform complexity classes. One kind includes a counterpart of the well-known non-uniform complexity class P/poly and another kind includes a counterpart of the well-known non-uniform complexity class NP/poly. Moreover, we introduce a general notion of completeness for the non-uniform complexity classes of the latter kind. We also formulate a counterpart of the well-known complexity theoretic conjecture that NP is not included in P/poly. We think that the presented approach opens up an additional way of investigating issues concerning non-uniform complexity. △ Less

Submitted 19 July, 2013; v1 submitted 15 January, 2013; originally announced January 2013.

Comments: 33 pages, supersedes arXiv:0809.0352 [cs.CC] in many respects (see end of introduction); remarks added

ACM Class: F.1.1; F.1.3

Journal ref: Scientific Annals of Computer Science 24(1):47--89, 2014

Process algebra with conditionals in the presence of epsilon

Authors: J. A. Bergstra, C. A. Middelburg

Abstract: 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 conditions under which preceding actions have been performed. In this paper, we add a constant for a process that is only capable of terminating successfully to those extensions of ACP, which can be very useful in applicati… ▽ More 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 conditions under which preceding actions have been performed. In this paper, we add a constant for a process that is only capable of terminating successfully to those extensions of ACP, which can be very useful in applications. It happens that in all cases the addition of this constant is unproblematic. △ Less

Submitted 15 April, 2012; originally announced April 2012.

Comments: 41 pages

ACM Class: D.1.3; D.2.1; D.2.4; F.1.2; F.3.1; F.3.2

Turing Impossibility Properties for Stack Machine Programming

Authors: J. A. Bergstra, C. A. Middelburg

Abstract: The strong, intermediate, and weak Turing impossibility properties are introduced. Some facts concerning Turing impossibility for stack machine programming are trivially adapted from previous work. Several intriguing questions are raised about the Turing impossibility properties concerning different method interfaces for stack machine programming. The strong, intermediate, and weak Turing impossibility properties are introduced. Some facts concerning Turing impossibility for stack machine programming are trivially adapted from previous work. Several intriguing questions are raised about the Turing impossibility properties concerning different method interfaces for stack machine programming. △ Less

Submitted 29 January, 2012; originally announced January 2012.

Comments: arXiv admin note: substantial text overlap with arXiv:0910.5564

On the behaviours produced by instruction sequences under execution

Authors: J. A. Bergstra, C. A. Middelburg

Abstract: We study several aspects of the behaviours produced by instruction sequences under execution in the setting of the algebraic theory of processes known as ACP. We use ACP to describe the behaviours produced by instruction sequences under execution and to describe two protocols implementing these behaviours in the case where the processing of instructions takes place remotely. We also show that all… ▽ More We study several aspects of the behaviours produced by instruction sequences under execution in the setting of the algebraic theory of processes known as ACP. We use ACP to describe the behaviours produced by instruction sequences under execution and to describe two protocols implementing these behaviours in the case where the processing of instructions takes place remotely. We also show that all finite-state behaviours considered in ACP can be produced by instruction sequences under execution. △ Less

Submitted 11 June, 2012; v1 submitted 30 June, 2011; originally announced June 2011.

Comments: 36 pages, consolidates material from arXiv:0811.0436 [cs.PL], arXiv:0902.2859 [cs.PL], and arXiv:0905.2257 [cs.PL]; abstract and introduction rewritten, examples and proofs added

MSC Class: 68N19; 68N30; 68Q05; 68Q10; 68Q55; 68Q85 ACM Class: D.1.4; D.2.1; F.1.1; F.1.2; F.3.2

Journal ref: Fundamenta Informaticae, 120(2):111--144, 2012

A survey of paraconsistent logics

Authors: C. A. Middelburg

Abstract: A survey of paraconsistent logics that are prominent representatives of the different approaches that have been followed to develop paraconsistent logics is provided. The paraconsistent logics that will be discussed are an enrichment of Priest's logic LP, the logic RM3 from the school of relevance logic, da Costa's logics Cn, Jaskowski's logic D2, and Subrahmanian's logics Ptau. A deontic logic ba… ▽ More A survey of paraconsistent logics that are prominent representatives of the different approaches that have been followed to develop paraconsistent logics is provided. The paraconsistent logics that will be discussed are an enrichment of Priest's logic LP, the logic RM3 from the school of relevance logic, da Costa's logics Cn, Jaskowski's logic D2, and Subrahmanian's logics Ptau. A deontic logic based on the first of these logics will be discussed as well. Moreover, some proposed adaptations of the AGM theory of belief revision to paraconsistent logics will be mentioned. △ Less

Submitted 14 November, 2017; v1 submitted 22 March, 2011; originally announced March 2011.

Comments: 20 pages; references made up-to-date; presentation of properties of enrichment of LP improved, remark added to concluding remarks

ACM Class: F.4.1

Searching publications on software testing

Authors: C. A. Middelburg

Abstract: This note concerns a search for publications in which the pragmatic concept of a test as conducted in the practice of software testing is formalized, a theory about software testing based on such a formalization is presented or it is demonstrated on the basis of such a theory that there are solid grounds to test software in cases where in principle other forms of analysis could be used. This note… ▽ More This note concerns a search for publications in which the pragmatic concept of a test as conducted in the practice of software testing is formalized, a theory about software testing based on such a formalization is presented or it is demonstrated on the basis of such a theory that there are solid grounds to test software in cases where in principle other forms of analysis could be used. This note reports on the way in which the search has been carried out and the main outcomes of the search. The message of the note is that the fundamentals of software testing are not yet complete in some respects. △ Less

Submitted 16 August, 2010; originally announced August 2010.

Comments: 7 pages

ACM Class: D.2.5

On the definition of a theoretical concept of an operating system

Authors: J. A. Bergstra, C. A. Middelburg

Abstract: We dwell on how a definition of a theoretical concept of an operating system, suitable to be incorporated in a mathematical theory of operating systems, could look like. This is considered a valuable preparation for the development of a mathematical theory of operating systems. We dwell on how a definition of a theoretical concept of an operating system, suitable to be incorporated in a mathematical theory of operating systems, could look like. This is considered a valuable preparation for the development of a mathematical theory of operating systems. △ Less

Submitted 4 June, 2010; originally announced June 2010.

Comments: 8 pages

ACM Class: D.4.0

Searching publications on operating systems

Authors: C. A. Middelburg

Abstract: This note concerns a search for publications in which one can find statements that explain the concept of an operating system, reasons for introducing operating systems, a formalization of the concept of an operating system or theory about operating systems based on such a formalization. It reports on the way in which the search has been carried out and the outcome of the search. The outcome inclu… ▽ More This note concerns a search for publications in which one can find statements that explain the concept of an operating system, reasons for introducing operating systems, a formalization of the concept of an operating system or theory about operating systems based on such a formalization. It reports on the way in which the search has been carried out and the outcome of the search. The outcome includes not only what the search was meant for, but also some added bonuses. △ Less

Submitted 29 March, 2010; originally announced March 2010.

Comments: 8 pages

ACM Class: D.4.m

Autosolvability of halting problem instances for instruction sequences

Authors: J. A. Bergstra, C. A. Middelburg

Abstract: We position Turing's result regarding the undecidability of the halting problem as a result about programs rather than machines. The mere requirement that a program of a certain kind must solve the halting problem for all programs of that kind leads to a contradiction in the case of a recent unsolvability result regarding the halting problem for programs. In this paper, we investigate this autosol… ▽ More We position Turing's result regarding the undecidability of the halting problem as a result about programs rather than machines. The mere requirement that a program of a certain kind must solve the halting problem for all programs of that kind leads to a contradiction in the case of a recent unsolvability result regarding the halting problem for programs. In this paper, we investigate this autosolvability requirement in a setting in which programs take the form of instruction sequences. △ Less

Submitted 17 October, 2010; v1 submitted 26 November, 2009; originally announced November 2009.

Comments: 18 pages; notational mistakes in tables 5 and 6 corrected; erroneous definition in last paragraph of page 11 corrected

Report number: PRG0914 ACM Class: F.1.1; F.4.1

Functional units for natural numbers

Authors: J. A. Bergstra, C. A. Middelburg

Abstract: Interaction with services provided by an execution environment forms part of the behaviours exhibited by instruction sequences under execution. Mechanisms related to the kind of interaction in question have been proposed in the setting of thread algebra. Like thread, service is an abstract behavioural concept. The concept of a functional unit is similar to the concept of a service, but more concre… ▽ More Interaction with services provided by an execution environment forms part of the behaviours exhibited by instruction sequences under execution. Mechanisms related to the kind of interaction in question have been proposed in the setting of thread algebra. Like thread, service is an abstract behavioural concept. The concept of a functional unit is similar to the concept of a service, but more concrete. A state space is inherent in the concept of a functional unit, whereas it is not inherent in the concept of a service. In this paper, we establish the existence of a universal computable functional unit for natural numbers and related results. △ Less

Submitted 17 October, 2010; v1 submitted 10 November, 2009; originally announced November 2009.

Comments: 17 pages; notational mistakes in tables 5 and 6 corrected; erroneous definition at bottom of page 9 corrected

Report number: PRG0913 ACM Class: F.1.1; F.4.1

Instruction sequence processing operators

Authors: J. A. Bergstra, C. A. Middelburg

Abstract: Instruction sequence is a key concept in practice, but it has as yet not come prominently into the picture in theoretical circles. This paper concerns instruction sequences, the behaviours produced by them under execution, the interaction between these behaviours and components of the execution environment, and two issues relating to computability theory. Positioning Turing's result regarding the… ▽ More Instruction sequence is a key concept in practice, but it has as yet not come prominently into the picture in theoretical circles. This paper concerns instruction sequences, the behaviours produced by them under execution, the interaction between these behaviours and components of the execution environment, and two issues relating to computability theory. Positioning Turing's result regarding the undecidability of the halting problem as a result about programs rather than machines, and taking instruction sequences as programs, we analyse the autosolvability requirement that a program of a certain kind must solve the halting problem for all programs of that kind. We present novel results concerning this autosolvability requirement. The analysis is streamlined by using the notion of a functional unit, which is an abstract state-based model of a machine. In the case where the behaviours exhibited by a component of an execution environment can be viewed as the behaviours of a machine in its different states, the behaviours concerned are completely determined by a functional unit. The above-mentioned analysis involves functional units whose possible states represent the possible contents of the tapes of Turing machines with a particular tape alphabet. We also investigate functional units whose possible states are the natural numbers. This investigation yields a novel computability result, viz. the existence of a universal computable functional unit for natural numbers. △ Less

Submitted 7 March, 2012; v1 submitted 29 October, 2009; originally announced October 2009.

Comments: 37 pages; missing equations in table 3 added; combined with arXiv:0911.1851 [cs.PL] and arXiv:0911.5018 [cs.LO]; introduction and concluding remarks rewritten; remarks and examples added; minor error in proof of theorem 4 corrected

ACM Class: D.3.3; F.1.1; F.4.1

Journal ref: Acta Informatica, 49(3):139--172, 2012

Partial Komori fields and imperative Komori fields

Authors: J. A. Bergstra, C. A. Middelburg

Abstract: This paper is concerned with the status of 1/0 and ways to deal with it. These matters are treated in the setting of Komori fields, also known as non-trivial cancellation meadows. Different viewpoints on the status of 1/0 exist in mathematics and theoretical computer science. We give a simple account of how mathematicians deal with 1/0 in which a customary convention among mathematicians plays a… ▽ More This paper is concerned with the status of 1/0 and ways to deal with it. These matters are treated in the setting of Komori fields, also known as non-trivial cancellation meadows. Different viewpoints on the status of 1/0 exist in mathematics and theoretical computer science. We give a simple account of how mathematicians deal with 1/0 in which a customary convention among mathematicians plays a prominent part, and we make plausible that a convincing account, starting from the popular computer science viewpoint that 1/0 is undefined, by means of some logic of partial functions is not attainable. △ Less

Submitted 29 September, 2009; originally announced September 2009.

Comments: 10 pages

Report number: PRG0911 MSC Class: 12E99; 12L99

Indirect jumps improve instruction sequence performance

Authors: J. A. Bergstra, C. A. Middelburg

Abstract: Instruction sequences with direct and indirect jump instructions are as expressive as instruction sequences with direct jump instructions only. We show that, in the case where the number of instructions is not bounded, we are faced with increases of the maximal internal delays of instruction sequences on execution that are not bounded by a linear function if we strive for acceptable increases of t… ▽ More Instruction sequences with direct and indirect jump instructions are as expressive as instruction sequences with direct jump instructions only. We show that, in the case where the number of instructions is not bounded, we are faced with increases of the maximal internal delays of instruction sequences on execution that are not bounded by a linear function if we strive for acceptable increases of the lengths of instruction sequences on elimination of indirect jump instructions. △ Less

Submitted 17 August, 2012; v1 submitted 11 September, 2009; originally announced September 2009.

Comments: 10 pages, definition of maximal internal delay and theorem 1 are stated more precise; presentation improved

Report number: PRG0910 ACM Class: D.3.3; F.1.1; F.3.3

Journal ref: Scientific Annals of Computer Science, 22(2):253--265, 2012

Arithmetical meadows

Authors: J. A. Bergstra, C. A. Middelburg

Abstract: An inversive meadow is a commutative ring with identity equipped with a multiplicative inverse operation made total by choosing 0 as its value at 0. Previously, inversive meadows were shortly called meadows. A divisive meadow is an inversive meadows with the multiplicative inverse operation replaced by a division operation. In the spirit of Peacock's arithmetical algebra, we introduce variants of… ▽ More An inversive meadow is a commutative ring with identity equipped with a multiplicative inverse operation made total by choosing 0 as its value at 0. Previously, inversive meadows were shortly called meadows. A divisive meadow is an inversive meadows with the multiplicative inverse operation replaced by a division operation. In the spirit of Peacock's arithmetical algebra, we introduce variants of inversive and divisive meadows without an additive identity element and an additive inverse operation. We give equational axiomatizations of several classes of such variants of inversive and divisive meadows as well as of several instances of them. △ Less

Submitted 2 November, 2010; v1 submitted 11 September, 2009; originally announced September 2009.

Comments: 14 pages; sections 4 and 5 permuted

Report number: PRG0909 MSC Class: 12E12; 12E30; 12L05

Inversive Meadows and Divisive Meadows

Authors: J. A. Bergstra, C. A. Middelburg

Abstract: Inversive meadows are commutative rings with a multiplicative identity element and a total multiplicative inverse operation whose value at 0 is 0. Divisive meadows are inversive meadows with the multiplicative inverse operation replaced by a division operation. We give finite equational specifications of the class of all inversive meadows and the class of all divisive meadows. It depends on the an… ▽ More Inversive meadows are commutative rings with a multiplicative identity element and a total multiplicative inverse operation whose value at 0 is 0. Divisive meadows are inversive meadows with the multiplicative inverse operation replaced by a division operation. We give finite equational specifications of the class of all inversive meadows and the class of all divisive meadows. It depends on the angle from which they are viewed whether inversive meadows or divisive meadows must be considered more basic. We show that inversive and divisive meadows of rational numbers can be obtained as initial algebras of finite equational specifications. In the spirit of Peacock's arithmetical algebra, we study variants of inversive and divisive meadows without an additive identity element and/or an additive inverse operation. We propose simple constructions of variants of inversive and divisive meadows with a partial multiplicative inverse or division operation from inversive and divisive meadows. Divisive meadows are more basic if these variants are considered as well. We give a simple account of how mathematicians deal with 1 / 0, in which meadows and a customary convention among mathematicians play prominent parts, and we make plausible that a convincing account, starting from the popular computer science viewpoint that 1 / 0 is undefined, by means of some logic of partial functions is not attainable. △ Less

Submitted 2 November, 2010; v1 submitted 3 July, 2009; originally announced July 2009.

Comments: 18 pages; error corrected; 29 pages, combined with arXiv:0909.2088 [math.RA] and arXiv:0909.5271 [math.RA]

MSC Class: 12E12; 12L05; 12L12; 16E50; 68Q65

Journal ref: Journal of Applied Logic, 9(3):203--220, 2011

Instruction sequence notations with probabilistic instructions

Authors: J. A. Bergstra, C. A. Middelburg

Abstract: This paper concerns instruction sequences that contain probabilistic instructions, i.e. instructions that are themselves probabilistic by nature. We propose several kinds of probabilistic instructions, provide an informal operational meaning for each of them, and discuss related work. On purpose, we refrain from providing an ad hoc formal meaning for the proposed kinds of instructions. We also dis… ▽ More This paper concerns instruction sequences that contain probabilistic instructions, i.e. instructions that are themselves probabilistic by nature. We propose several kinds of probabilistic instructions, provide an informal operational meaning for each of them, and discuss related work. On purpose, we refrain from providing an ad hoc formal meaning for the proposed kinds of instructions. We also discuss the approach of projection semantics, which was introduced in earlier work on instruction sequences, in the light of probabilistic instruction sequences. △ Less

Submitted 1 October, 2014; v1 submitted 17 June, 2009; originally announced June 2009.

Comments: 15 pages, revised because arxiv:1409.6873v1 [cs.LO] has come out

Report number: PRG0906 ACM Class: D.1.4; F.1.1; F.1.2