Source author record

C. A. Middelburg

C. A. Middelburg appears in the imported research catalog. Authorship, coauthor and topic links are available while profile ownership is still unclaimed.

ResearcherUnclaimed source record

Catalog footprint

What is connected

42works
10topics
3close collaborators

Actions

Connect this record

Log in to claim

Research graph

See the researcher in context

Open full explorer

Inspect adjacent papers, topics, institutions and collaborators without losing the researcher page.

Building this map preview

BZPEER is loading the nearby papers, people, topics and institutions for this page.

Published work

42 published item(s)

preprint2022arXiv

Imperative process algebra with abstraction

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.

preprint2020arXiv

On infinite guarded recursive specifications in process algebra

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.

preprint2020arXiv

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

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.

preprint2020arXiv

Process algebra with strategic interleaving

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.

preprint2020arXiv

Process algebra, process scheduling, and mutual exclusion

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.

preprint2019arXiv

Program algebra for Turing-machine programs

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.

preprint2016arXiv

Instruction sequence size complexity of parity

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.

preprint2016arXiv

On instruction sets for Boolean registers in program algebra

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.

preprint2016arXiv

Transformation of fractions into simple fractions in divisive meadows

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.

preprint2015arXiv

On algorithmic equivalence of instruction sequences for computing bit string functions

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.

preprint2015arXiv

Probabilistic thread algebra

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.

preprint2014arXiv

Division by zero in non-involutive meadows

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.

preprint2014arXiv

Instruction sequence notations with probabilistic instructions

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.

preprint2014arXiv

Long multiplication by instruction sequences with backward jump instructions

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.

preprint2013arXiv

A process calculus with finitary comprehended terms

We introduce the notion of an ACP process algebra and the notion of a meadow enriched ACP process algebra. The former notion originates from the models of the axiom system ACP. The latter notion is a simple generalization of the former notion to processes in which data are involved, the mathematical structure of data being a meadow. Moreover, for all associative operators from the signature of meadow enriched ACP process algebras that are not of an auxiliary nature, we introduce variable-binding operators as generalizations. These variable-binding operators, which give rise to comprehended terms, have the property that they can always be eliminated. Thus, we obtain a process calculus whose terms can be interpreted in all meadow enriched ACP process algebras. Use of the variable-binding operators can have a major impact on the size of terms.

preprint2013arXiv

Data linkage algebra, data linkage dynamics, and priority rewriting

We introduce an algebra of data linkages. Data linkages are intended for modelling the states of computations in which dynamic data structures are involved. We present a simple model of computation in which states of computations are modelled as data linkages and state changes take place by means of certain actions. We describe the state changes and replies that result from performing those actions by means of a term rewriting system with rule priorities. The model in question is an upgrade of molecular dynamics. The upgrading is mainly concerned with the features to deal with values and the features to reclaim garbage.

preprint2013arXiv

Instruction sequence based non-uniform complexity classes

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.

preprint2013arXiv

Network algebra for synchronous dataflow

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.

preprint2013arXiv

Timed tuplix calculus and the Wesseling and van den Bergh equation

We develop an algebraic framework for the description and analysis of financial behaviours, that is, behaviours that consist of transferring certain amounts of money at planned times. To a large extent, analysis of financial products amounts to analysis of such behaviours. We formalize the cumulative interest compliant conservation requirement for financial products proposed by Wesseling and van den Bergh by an equation in the framework developed and define a notion of financial product behaviour using this formalization. We also present some properties of financial product behaviours. The development of the framework has been influenced by previous work on the process algebra ACP.

preprint2012arXiv

Indirect jumps improve instruction sequence performance

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.

preprint2012arXiv

Instruction sequence processing operators

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.

preprint2012arXiv

On the behaviours produced by instruction sequences under execution

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.

preprint2012arXiv

Process algebra with conditionals in the presence of epsilon

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.

preprint2011arXiv

An Application Specific Informal Logic for Interest Prohibition Theory

Interest prohibition theory concerns theoretical aspects of interest prohibition. We attempt to lay down some aspects of interest prohibition theory wrapped in a larger framework of informal logic. The reason for this is that interest prohibition theory has to deal with a variety of arguments which is so wide that a limitation to so-called correct arguments in advance is counterproductive. We suggest that an application specific informal logic must be developed for dealing with the principles of interest prohibition theory.

preprint2010arXiv

Arithmetical meadows

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.

preprint2010arXiv

Autosolvability of halting problem instances for instruction sequences

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.

preprint2010arXiv

Data linkage dynamics with shedding

We study shedding in the setting of data linkage dynamics, a simple model of computation that bears on the use of dynamic data structures in programming. Shedding is complementary to garbage collection. With shedding, each time a link to a data object is updated by a program, it is determined whether or not the link will possibly be used once again by the program, and if not the link is automatically removed. Thus, everything is made garbage as soon as it can be viewed as garbage. By that, the effectiveness of garbage collection becomes maximal.

preprint2010arXiv

Functional units for natural numbers

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.

preprint2010arXiv

Instruction sequences and non-uniform complexity theory

We develop theory concerning non-uniform complexity in a setting in which the notion of single-pass instruction sequence considered in program algebra is the central notion. We define counterparts of the complexity classes P/poly and NP/poly and formulate a counterpart of the complexity theoretic conjecture that NP is not included in P/poly. In addition, we define a notion of completeness for the counterpart of NP/poly using a non-uniform reducibility relation and formulate complexity hypotheses which concern restrictions on the instruction sequences used for computation. We think that the theory developed opens up an additional way of investigating issues concerning non-uniform complexity.

preprint2010arXiv

Inversive Meadows and Divisive Meadows

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.

preprint2010arXiv

Preliminaries to an investigation of reduced product set finance

Principles of financial product synthesis from a few basic financial products constitute an interesting research topic inspired by Islamic finance. We make an effort to answer general questions that should be answered before starting to investigate the main issues concerning this topic with the formalization of financial products and principles of financial product synthesis. We also outline the outcome of some preparatory explorations, which have been conducted with the purpose to form a reasonable preliminary picture of the details of financial products that are relevant to the study of the principles of financial product synthesis.

preprint2010arXiv

Searching publications on operating systems

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.

preprint2010arXiv

Searching publications on software testing

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.

preprint2009arXiv

Instruction sequences with dynamically instantiated instructions

We study sequential programs that are instruction sequences with dynamically instantiated instructions. We define the meaning of such programs in two different ways. In either case, we give a translation by which each program with dynamically instantiated instructions is turned into a program without them that exhibits on execution the same behaviour by interaction with some service. The complexity of the translations differ considerably, whereas the services concerned are equally simple. However, the service concerned in the case of the simpler translation is far more powerful than the service concerned in the other case.

preprint2009arXiv

On the expressiveness of single-pass instruction sequences

We perceive programs as single-pass instruction sequences. A single-pass instruction sequence under execution is considered to produce a behaviour to be controlled by some execution environment. Threads as considered in basic thread algebra model such behaviours. We show that all regular threads, i.e. threads that can only be in a finite number of states, can be produced by single-pass instruction sequences without jump instructions if use can be made of Boolean registers. We also show that, in the case where goto instructions are used instead of jump instructions, a bound to the number of labels restricts the expressiveness.

preprint2009arXiv

Thread extraction for polyadic instruction sequences

In this paper, we study the phenomenon that instruction sequences are split into fragments which somehow produce a joint behaviour. In order to bring this phenomenon better into the picture, we formalize a simple mechanism by which several instruction sequence fragments can produce a joint behaviour. We also show that, even in the case of this simple mechanism, it is a non-trivial matter to explain by means of a translation into a single instruction sequence what takes place on execution of a collection of instruction sequence fragments.

preprint2008arXiv

A thread calculus with molecular dynamics

We present a theory of threads, interleaving of threads, and interaction between threads and services with features of molecular dynamics, a model of computation that bears on computations in which dynamic data structures are involved. Threads can interact with services of which the states consist of structured data objects and computations take place by means of actions which may change the structure of the data objects. The features introduced include restriction of the scope of names used in threads to refer to data objects. Because that feature makes it troublesome to provide a model based on structural operational semantics and bisimulation, we construct a projective limit model for the theory.

preprint2008arXiv

An interface group for process components

We take a process component as a pair of an interface and a behaviour. We study the composition of interacting process components in the setting of process algebra. We formalize the interfaces of interacting process components by means of an interface group. An interesting feature of the interface group is that it allows for distinguishing between expectations and promises in interfaces of process components. This distinction comes into play in case components with both client and server behaviour are involved.

preprint2008arXiv

On the operating unit size of load/store architectures

We introduce a strict version of the concept of a load/store instruction set architecture in the setting of Maurer machines. We take the view that transformations on the states of a Maurer machine are achieved by applying threads as considered in thread algebra to the Maurer machine. We study how the transformations on the states of the main memory of a strict load/store instruction set architecture that can be achieved by applying threads depend on the operating unit size, the cardinality of the instruction set, and the maximal number of states of the threads.

preprint2008arXiv

Thread algebra for poly-threading

Threads as considered in basic thread algebra are primarily looked upon as behaviours exhibited by sequential programs on execution. It is a fact of life that sequential programs are often fragmented. Consequently, fragmented program behaviours are frequently found. In this paper, we consider this phenomenon. We extend basic thread algebra with the barest mechanism for sequencing of threads that are taken for fragments. This mechanism, called poly-threading, supports both autonomous and non-autonomous thread selection in sequencing. We relate the resulting theory to the algebraic theory of processes known as ACP and use it to describe analytic execution architectures suited for fragmented programs. We also consider the case where the steps of fragmented program behaviours are interleaved in the ways of non-distributed and distributed multi-threading.