Showing 51–100 of 121 results for author: Bergstra, J A

Decision Taking for Selling Thread Startup

Authors: Jan A. Bergstra

Abstract: Decision Taking is discussed in the context of the role it may play for a selling agent in a search market, in particular for agents involved in the sale of valuable and relatively unique items, such as a dwelling, a second hand car, or a second hand recreational vessel. Detailed connections are made between the architecture of decision making processes and a sample of software technology based… ▽ More Decision Taking is discussed in the context of the role it may play for a selling agent in a search market, in particular for agents involved in the sale of valuable and relatively unique items, such as a dwelling, a second hand car, or a second hand recreational vessel. Detailed connections are made between the architecture of decision making processes and a sample of software technology based concepts including instruction sequences, multi-threading, and thread algebra. Ample attention is paid to the initialization or startup of a thread dedicated to achieving a given objective, and to corresponding decision taking. As an application, the selling of an item is taken as an objective to be achieved by running a thread that was designed for that purpose. △ Less

Submitted 12 August, 2012; originally announced August 2012.

Decision Taking versus Action Determination

Authors: Jan A. Bergstra

Abstract: Decision taking is discussed in the context of the role it may play for various types of agents, and it is contrasted with action determination. Some remarks are made about the role of decision taking and action determination in the ongoing debate concerning the reverse polder development of the hertogin Hedwige polder. Decision taking is discussed in the context of the role it may play for various types of agents, and it is contrasted with action determination. Some remarks are made about the role of decision taking and action determination in the ongoing debate concerning the reverse polder development of the hertogin Hedwige polder. △ Less

Submitted 28 May, 2012; originally announced May 2012.

Decision Taking as a Service

Authors: Jan A. Bergstra

Abstract: Decision taking can be performed as a service to other parties and it is amenable to outtasking rather than to outsourcing. Outtasking decision taking is compatible with selfsourcing of decision making activities carried out in preparation of decision taking. Decision taking as a service (DTaaS) is viewed as an instance of so-called decision casting. Preconditions for service casting are examined,… ▽ More Decision taking can be performed as a service to other parties and it is amenable to outtasking rather than to outsourcing. Outtasking decision taking is compatible with selfsourcing of decision making activities carried out in preparation of decision taking. Decision taking as a service (DTaaS) is viewed as an instance of so-called decision casting. Preconditions for service casting are examined, and compliance of decision taking with these preconditions is confirmed. Potential advantages and disadvantages of using decision taking as a service are considered. △ Less

Submitted 10 August, 2014; v1 submitted 18 May, 2012; originally announced May 2012.

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

Four Conceptions of Instruction Sequence Faults

Authors: Jan A. Bergstra

Abstract: The notion of an instruction sequence fault is considered from various perspectives. Four different viewpoints on what constitutes a fault, or how to use the notion of a fault, are formulated. An integration of these views is proposed. The notion of an instruction sequence fault is considered from various perspectives. Four different viewpoints on what constitutes a fault, or how to use the notion of a fault, are formulated. An integration of these views is proposed. △ Less

Submitted 9 April, 2012; originally announced April 2012.

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

About Instruction Sequence Testing

Authors: J. A. Bergstra

Abstract: Software testing is presented as a so-called theme within which different authors and groups have defined different subjects each of these subjects having a different focus on testing. A uniform concept of software testing is non-existent and the space of possible coherent perspectives on software testing, each fitting within the theme, is viewed as being spanned by five dimensions, each dimension… ▽ More Software testing is presented as a so-called theme within which different authors and groups have defined different subjects each of these subjects having a different focus on testing. A uniform concept of software testing is non-existent and the space of possible coherent perspectives on software testing, each fitting within the theme, is viewed as being spanned by five dimensions, each dimension representing two opposite views with a variety of intermediate views in between. Instruction sequences are used as a simple theoretical conceptualization of computer programs. A theory of instruction sequence testing may serve as a model for a theory of software testing. Instruction sequences testing is considered a new topic for which definitions may be freely contemplated without being restricted by existing views on software testing. The problem of develo** a theory of instruction sequence testing is posed. A survey is given of motivations and scenarios for develo** a theory of instruction sequence testing. △ Less

Submitted 18 January, 2012; originally announced January 2012.

Informatics Perspectives on Decision Taking, a Case Study on Resolving Process Product Ambiguity

Authors: J. A. Bergstra

Abstract: A decision is an act or event of decision taking. Decision making always includes decision taking, the latter not involving significant exchanges with non-deciding agents. A decision outcome is a piece of storable information constituting the result of a decision. Decision outcomes are typed, for instance: plan, command, assertion, or boolean reply to a question. Decision outcomes are seen by an a… ▽ More A decision is an act or event of decision taking. Decision making always includes decision taking, the latter not involving significant exchanges with non-deciding agents. A decision outcome is a piece of storable information constituting the result of a decision. Decision outcomes are typed, for instance: plan, command, assertion, or boolean reply to a question. Decision outcomes are seen by an audience and autonomous actions from the audience is supposed to realize the putting into effect of a decision outcome, thus leading to so-called decision effects. Decision outcomes are supposedly expected by the decider. Using a model or a theory concerning the causal chain leading from a decision outcome to one or more decision effects may support a decision taker decision taker in predicting plausible decision effects for candidate decision outcomes. Decision taking is positioned amidst many related notions including: decision making, decision process, decision making process, decision process making, decision engineering, decision progression, and decision progression production. △ Less

Submitted 10 August, 2014; v1 submitted 26 December, 2011; originally announced December 2011.

Comments: First revision; many minior improvements have been made, concluding section has been replaced

Stratified Outsourcing Theory

Authors: J. A. Bergstra, G. P. A. J. Delen, S. F. M. van Vlijmen

Abstract: The terminology of sourcing, outsourcing and insourcing is developed in detail on the basis of the preliminary definitions of outsourcing and insourcing and related activities and competences as given in our three previous papers on business mereology, on the concept of a sourcement, and on outsourcing competence respectively. Besides providing more a detailed semantic analysis we will introduce… ▽ More The terminology of sourcing, outsourcing and insourcing is developed in detail on the basis of the preliminary definitions of outsourcing and insourcing and related activities and competences as given in our three previous papers on business mereology, on the concept of a sourcement, and on outsourcing competence respectively. Besides providing more a detailed semantic analysis we will introduce, explain, and illustrate a number of additional concepts including: principal unit of a sourcement, theme of a sourcement, current sourcement, (un)stable sourcement, and sourcement transformation. A three level terminology is designed: (i) factual level: operational facts that hold for sourcements including histories thereof, (ii) business level: roles and objectives of various parts of the factual level description, thus explaining each partner's business process and business objectives, (iii) contract level: specification of intended facts and intended business models as found at the business level. Orthogonal to these three conceptual levels, are four temporal aspects: history, now (actuality), transformation, and transition. A detailed description of the well-known range of sourcement transformations is given. △ Less

Submitted 10 October, 2011; originally announced October 2011.

ACM Class: K.6.0; J.4; H.4.0; D.0

Putting Instruction Sequences into Effect

Authors: Jan A. Bergstra

Abstract: An attempt is made to define the concept of execution of an instruction sequence. It is found to be a special case of directly putting into effect of an instruction sequence. Directly putting into effect of an instruction sequences comprises interpretation as well as execution. Directly putting into effect is a special case of putting into effect with other special cases classified as indirectly p… ▽ More An attempt is made to define the concept of execution of an instruction sequence. It is found to be a special case of directly putting into effect of an instruction sequence. Directly putting into effect of an instruction sequences comprises interpretation as well as execution. Directly putting into effect is a special case of putting into effect with other special cases classified as indirectly putting into effect. △ Less

Submitted 9 October, 2011; originally announced October 2011.

Outsourcing Competence

Authors: J. A. Bergstra, G. P. A. J. Delen, S. F. M. van Vlijmen

Abstract: The topic of this paper, competences needed for outsourcing, is organized by first providing a generic competence scheme, which is subsequently instantiated to the area of sourcing and outsourcing. Sourcing and outsourcing are positioned as different areas of activity, neither one of which is subsumed under the other one. It is argued that competences relevant for outsourcing are mainly community… ▽ More The topic of this paper, competences needed for outsourcing, is organized by first providing a generic competence scheme, which is subsequently instantiated to the area of sourcing and outsourcing. Sourcing and outsourcing are positioned as different areas of activity, neither one of which is subsumed under the other one. It is argued that competences relevant for outsourcing are mainly community based rather than evidence based. Subjective ability and objective ability are distinguished as categories, together making up ability, which are distinct but not necessarily disjoint from competence. Conjectural ability is introduced as a form of subjective ability. A person's competence profile includes competences as well as abilities, including subjective ones. Competence assessment and acquisition as well as the impact of assessed competence on practical work is described. The analysis of competence and ability thus developed is used as standpoint from which to extract a specification of an audience for a theory of outsourcing, yet to be written. Moreover, it allows to formulate requirements for and in preparation of the development of an outsourcing theory. Formulating these requirements is done under the assumption that a person's awareness of a theory of outsourcing is expected to strengthen that person's outsourcing competence profile. △ Less

Submitted 29 September, 2011; originally announced September 2011.

ACM Class: K.6.0; J.4; H.4.0; D.0

Introducing Sourcements

Authors: J. A. Bergstra, G. P. A. J. Delen, S. F. M. van Vlijmen

Abstract: Sourcing processes are discussed at a high abstraction level. A dedicated terminology is developed concerning general aspects of sourcing. The term sourcement is coined to denote a building block for sourcing. No- tions of allocation, functional architecture and allocational architecture, equilibrium, and configuration are discussed. Limitations of the concept of outsourcing are outlined. This the… ▽ More Sourcing processes are discussed at a high abstraction level. A dedicated terminology is developed concerning general aspects of sourcing. The term sourcement is coined to denote a building block for sourcing. No- tions of allocation, functional architecture and allocational architecture, equilibrium, and configuration are discussed. Limitations of the concept of outsourcing are outlined. This theoretical work is meant to serve as a point of departure for the subsequent development of a detailed theory of sourcing and sourcing transformations, which can be a tool for dealing with practical applica- tions. △ Less

Submitted 23 July, 2011; originally announced July 2011.

ACM Class: K.6.0; J.4; H.4.0; D.0

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

Dialectical Roots for Interest Prohibition Theory

Authors: Jan Aldert Bergstra

Abstract: It is argued that arguments for strict prohibition of interests must be based on the use of arguments from authority. This is carried out by first making a survey of so-called dialectical roots for interest prohibition and then demonstrating that for at least one important positive interest bearing financial product, the savings account with interest, its prohibition cannot be inferred from a matc… ▽ More It is argued that arguments for strict prohibition of interests must be based on the use of arguments from authority. This is carried out by first making a survey of so-called dialectical roots for interest prohibition and then demonstrating that for at least one important positive interest bearing financial product, the savings account with interest, its prohibition cannot be inferred from a match with any of these root cases. △ Less

Submitted 14 May, 2011; originally announced May 2011.

Interest prohibition and financial product innovation

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

Abstract: We give a rough sketch of the Judaic, Greek, Islamic and Christian positions in the matter of interest prohibition during the last few millennia and discuss the way in which interest prohibition is dealt with in Islamic finance, the problems with authority-based arguments for interest prohibition, and the prospects of interest prohibition with the advent of electronic money. We give a rough sketch of the Judaic, Greek, Islamic and Christian positions in the matter of interest prohibition during the last few millennia and discuss the way in which interest prohibition is dealt with in Islamic finance, the problems with authority-based arguments for interest prohibition, and the prospects of interest prohibition with the advent of electronic money. △ Less

Submitted 13 April, 2011; originally announced April 2011.

Comments: 9 pages

Journal ref: Finance Islamique: Regard(s) sur une Finance Alternative, pages 274--284, Mazars Hadj Ali, 2011

An Application Specific Informal Logic for Interest Prohibition Theory

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

Abstract: 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 sugg… ▽ More 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. △ Less

Submitted 2 April, 2011; originally announced April 2011.

Comments: 8 pages

Real Islamic Logic

Authors: Jan Aldert Bergstra

Abstract: Four options for assigning a meaning to Islamic Logic are surveyed including a new proposal for an option named "Real Islamic Logic" (RIL). That approach to Islamic Logic should serve modern Islamic objectives in a way comparable to the functionality of Islamic Finance. The prospective role of RIL is analyzed from several perspectives: (i) parallel distributed systems design, (ii) reception by a c… ▽ More Four options for assigning a meaning to Islamic Logic are surveyed including a new proposal for an option named "Real Islamic Logic" (RIL). That approach to Islamic Logic should serve modern Islamic objectives in a way comparable to the functionality of Islamic Finance. The prospective role of RIL is analyzed from several perspectives: (i) parallel distributed systems design, (ii) reception by a community structured audience, (iii) informal logic and applied non-classical logics, and (iv) (in)tractability and artificial intelligence. △ Less

Submitted 23 March, 2011; originally announced March 2011.

Business Mereology: Imaginative Definitions of Insourcing and Outsourcing Transformations

Authors: J. A. Bergstra, S. F. M. van Vlijmen

Abstract: Outsourcing, the passing on of tasks by organizations to other organizations, often including the personnel and means to perform these tasks, has become an important IT-business strategy over the past decades. We investigate imaginative definitions for outsourcing relations and outsourcing transformations. Abstract models of an extreme and unrealistic simplicity are considered in order to invest… ▽ More Outsourcing, the passing on of tasks by organizations to other organizations, often including the personnel and means to perform these tasks, has become an important IT-business strategy over the past decades. We investigate imaginative definitions for outsourcing relations and outsourcing transformations. Abstract models of an extreme and unrealistic simplicity are considered in order to investigate possible definitions of outsourcing. Rather than covering all relevant practical cases an imaginative definition of a concept provides obvious cases of its instantiation from which more refined or liberal definitions may be derived. A definition of outsourcing induces to a complementary definition of insourcing. Outsourcing and insourcing have more complex variations in which multiple parties are involved. All of these terms both refer to state transformations and to state descriptions pertaining to the state obtained after such transformations. We make an attempt to disambiguate the terminology in that respect and we make an attempt to characterize the general concept of sourcing which captures some representative cases. Because mereology is the most general theory of parthood relations we coin business mereology as the general theory in business studies which concerns the full variety of sourcing relations and transformations. △ Less

Submitted 28 December, 2010; originally announced December 2010.

ACM Class: K.6.0; J.4; H.4.0; D.0

On Hoare-McCarthy algebras

Authors: Jan A. Bergstra, Alban Ponse

Abstract: We discuss an algebraic approach to propositional logic with side effects. To this end, we use Hoare's conditional [1985], which is a ternary connective comparable to if-then-else. Starting from McCarthy's notion of sequential evaluation [1963] we discuss a number of valuation congruences and we introduce Hoare-McCarthy algebras as the structures that characterize these congruences. We discuss an algebraic approach to propositional logic with side effects. To this end, we use Hoare's conditional [1985], which is a ternary connective comparable to if-then-else. Starting from McCarthy's notion of sequential evaluation [1963] we discuss a number of valuation congruences and we introduce Hoare-McCarthy algebras as the structures that characterize these congruences. △ Less

Submitted 22 December, 2010; originally announced December 2010.

Comments: 29 pages, 1 table

ACM Class: F.3.2

Preliminaries to an investigation of reduced product set finance

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

Abstract: 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 o… ▽ More 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. △ Less

Submitted 20 December, 2010; originally announced December 2010.

Comments: 32 pages

Journal ref: JKAU: Islamic Economics, 24(1):175-210, 2011

Short-circuit logic

Authors: Jan A. Bergstra, A. Ponse, D. J. C. Staudt

Abstract: Short-circuit evaluation denotes the semantics of propositional connectives in which the second argument is evaluated only if the first argument does not suffice to determine the value of the expression. In programming, short-circuit evaluation is widely used, with sequential conjunction and disjunction as primitive connectives. A short-circuit logic is a variant of propositional logic (PL) that… ▽ More Short-circuit evaluation denotes the semantics of propositional connectives in which the second argument is evaluated only if the first argument does not suffice to determine the value of the expression. In programming, short-circuit evaluation is widely used, with sequential conjunction and disjunction as primitive connectives. A short-circuit logic is a variant of propositional logic (PL) that can be defined with help of Hoare's conditional, a ternary connective comparable to if-then-else, and that implies all identities that follow from four basic axioms for the conditional and can be expressed in PL (e.g., axioms for associativity of conjunction and double negation shift). In the absence of side effects, short-circuit evaluation characterizes PL. However, short-circuit evaluation admits the possibility to model side effects and gives rise to various different short-circuit logics. The first extreme case is FSCL (free short-circuit logic), which characterizes the setting in which evaluation of each atom (propositional variable) can yield a side effect. The other extreme case is MSCL (memorizing short-circuit logic), the most identifying variant we distinguish below PL. In MSCL, only a very restricted type of side effects can be modelled, while sequential conjunction is non-commutative. We provide axiomatizations for FSCL and MSCL. Extending MSCL with one simple axiom yields SSCL (static short-circuit logic, or sequential PL), for which we also provide a completeness result. We briefly discuss two variants in between FSCL and MSCL, among which a logic that admits contraction of atoms and of their negations. △ Less

Submitted 12 March, 2013; v1 submitted 18 October, 2010; originally announced October 2010.

Comments: 59 pages, 7 tables, 3 figures; Daan Staudt is added as an extra author; normal forms for FSCL are defined and completeness of its axiomatization is proved

ACM Class: F.3.2

Steering Fragments of Instruction Sequences

Authors: Jan A. Bergstra

Abstract: A steering fragment of an instruction sequence consists of a sequence of steering instructions. These are decision points involving the check of a propositional statement in sequential logic. The question is addressed why composed propositional statements occur in steering fragments given the fact that a straightforward transformation allows their elimination. A survey is provided of constraints t… ▽ More A steering fragment of an instruction sequence consists of a sequence of steering instructions. These are decision points involving the check of a propositional statement in sequential logic. The question is addressed why composed propositional statements occur in steering fragments given the fact that a straightforward transformation allows their elimination. A survey is provided of constraints that may be implicitly assumed when composed propositional statements occur in a meaningful instruction sequence. △ Less

Submitted 14 October, 2010; originally announced October 2010.

Informal Control code logic

Authors: Jan A. Bergstra

Abstract: General definitions as well as rules of reasoning regarding control code production, distribution, deployment, and usage are described. The role of testing, trust, confidence and risk analysis is considered. A rationale for control code testing is sought and found for the case of safety critical embedded control code. General definitions as well as rules of reasoning regarding control code production, distribution, deployment, and usage are described. The role of testing, trust, confidence and risk analysis is considered. A rationale for control code testing is sought and found for the case of safety critical embedded control code. △ Less

Submitted 15 September, 2010; originally announced September 2010.

Formaleuros, Formalbitcoins, and Virtual Monies

Authors: Jan A. Bergstra

Abstract: Formalist positions towards money are considered from a perspective of formal methods in computing. The Formaleuro (FEUR) as a dimension for monetary quantities is proposed as well as the Formalbitcoin (FBTC) which represents an item ready for circulation in a model of informational money. An attempt is made to understand the concept of money from scratch. In order to provide a definition of mon… ▽ More Formalist positions towards money are considered from a perspective of formal methods in computing. The Formaleuro (FEUR) as a dimension for monetary quantities is proposed as well as the Formalbitcoin (FBTC) which represents an item ready for circulation in a model of informational money. An attempt is made to understand the concept of money from scratch. In order to provide a definition of money the need is felt to make use of a tailored theory of definition. To that end a theory of imaginative definitions is presented and its implications for definitions of money are sketched. It is argued that a theory of money may be dependent on the role of its holder. A survey of some roles is given, with the so-called subordinate administrative role (SAR) in a central position. The concepts of virtual memory and virtual machine are taken as the point of departure for a definition of the notion of virtual money. It is argued that from the perspective of a component (division) of a large organization (ORG) its local financial system (LFS) provides a virtual money vm(LFS, ORG) which may well fail to meet the most common general and acknowledged moneyness criteria. Inverse moneyness preference is coined as phrase to assert the tendency of top-management of ORG to make its virtual money deviate from these criteria. △ Less

Submitted 25 April, 2013; v1 submitted 3 August, 2010; originally announced August 2010.

Comments: 98 pages. Revision of arXiv.org/abs/1008.0616v1. The revision involves bringing the paper up to date with the appearance of Bitcoin, a significant update of the section on Islamic finance and interest prohibition, deletion of fragments of minor importance, an update of references, moving the ad hoc theory of definitions to an appendix, and a small change of the title

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

On the contribution of backward jumps to instruction sequence expressiveness

Authors: Jan A. Bergstra, Inge Bethke

Abstract: We investigate the expressiveness of backward jumps in a framework of formalized sequential programming called program algebra. We show that - if expressiveness is measured in terms of the computability of partial Boolean functions - then backward jumps are superfluous. If we, however, want to prevent explosion of the length of programs, then backward jumps are essential. We investigate the expressiveness of backward jumps in a framework of formalized sequential programming called program algebra. We show that - if expressiveness is measured in terms of the computability of partial Boolean functions - then backward jumps are superfluous. If we, however, want to prevent explosion of the length of programs, then backward jumps are essential. △ Less

Submitted 31 May, 2010; originally announced May 2010.

Comments: 16 pages

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

A progression ring for interfaces of instruction sequences, threads, and services

Authors: Jan A. Bergstra, Alban Ponse

Abstract: We define focus-method interfaces and some connections between such interfaces and instruction sequences, giving rise to instruction sequence components. We provide a flexible and practical notation for interfaces using an abstract datatype specification comparable to that of basic process algebra with deadlock. The structures thus defined are called progression rings. We also define thread and… ▽ More We define focus-method interfaces and some connections between such interfaces and instruction sequences, giving rise to instruction sequence components. We provide a flexible and practical notation for interfaces using an abstract datatype specification comparable to that of basic process algebra with deadlock. The structures thus defined are called progression rings. We also define thread and service components. Two types of composition of instruction sequences or threads and services (called `use' and `apply') are lifted to the level of components. △ Less

Submitted 15 September, 2009; originally announced September 2009.

Comments: 12 pages

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

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

Straight-line instruction sequence completeness for total calculation on cancellation meadows

Authors: Jan A. Bergstra, Inge Bethke

Abstract: A combination of program algebra with the theory of meadows is designed leading to a theory of computation in algebraic structures which use in addition to a zero test and copying instructions the instruction set $\{x \Leftarrow 0, x \Leftarrow 1, x\Leftarrow -x, x\Leftarrow x^{-1}, x\Leftarrow x+y, x\Leftarrow x\cdot y\}$. It is proven that total functions on cancellation meadows can be compute… ▽ More A combination of program algebra with the theory of meadows is designed leading to a theory of computation in algebraic structures which use in addition to a zero test and copying instructions the instruction set $\{x \Leftarrow 0, x \Leftarrow 1, x\Leftarrow -x, x\Leftarrow x^{-1}, x\Leftarrow x+y, x\Leftarrow x\cdot y\}$. It is proven that total functions on cancellation meadows can be computed by straight-line programs using at most 5 auxiliary variables. A similar result is obtained for signed meadows. △ Less

Submitted 29 May, 2009; v1 submitted 28 May, 2009; originally announced May 2009.

Comments: 24 pages

A protocol for instruction stream processing

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

Abstract: The behaviour produced by an instruction sequence under execution is a behaviour to be controlled by some execution environment: each step performed actuates the processing of an instruction by the execution environment and a reply returned at completion of the processing determines how the behaviour proceeds. In this paper, we are concerned with the case where the processing takes place remotel… ▽ More The behaviour produced by an instruction sequence under execution is a behaviour to be controlled by some execution environment: each step performed actuates the processing of an instruction by the execution environment and a reply returned at completion of the processing determines how the behaviour proceeds. In this paper, we are concerned with the case where the processing takes place remotely. We describe a protocol to deal with the case where the behaviour produced by an instruction sequence under execution leads to the generation of a stream of instructions to be processed and a remote execution unit handles the processing of that stream of instructions. △ Less

Submitted 14 May, 2009; originally announced May 2009.

Comments: 15pages

Report number: PRG0905 ACM Class: D.2.1; D.2.4; F.1.1; F.3.1

A process calculus with finitary comprehended terms

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

Abstract: 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 mea… ▽ More 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. △ Less

Submitted 28 March, 2013; v1 submitted 17 March, 2009; originally announced March 2009.

Comments: 25 pages, combined with arXiv:0901.3012 [math.RA]; presentation improved, mistakes in Table 5 corrected

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

Journal ref: Theory of Computing Systems, 53(4):645--668, 2013

An Instruction Sequence Semigroup with Involutive Anti-Automorphisms

Authors: Jan A. Bergstra, Alban Ponse

Abstract: We introduce an algebra of instruction sequences by presenting a semigroup C in which programs can be represented without directional bias: in terms of the next instruction to be executed, C has both forward and backward instructions and a C-expression can be interpreted starting from any instruction. We provide equations for thread extraction, i.e., C's program semantics. Then we consider threa… ▽ More We introduce an algebra of instruction sequences by presenting a semigroup C in which programs can be represented without directional bias: in terms of the next instruction to be executed, C has both forward and backward instructions and a C-expression can be interpreted starting from any instruction. We provide equations for thread extraction, i.e., C's program semantics. Then we consider thread extraction compatible (anti-)homomorphisms and (anti-)automorphisms. Finally we discuss some expressiveness results. △ Less

Submitted 7 November, 2009; v1 submitted 7 March, 2009; originally announced March 2009.

Comments: 36 pages, 1 table

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

Journal ref: Scientific Annals of Computer Science, 19:57-92, 2009

Transmission protocols for instruction streams

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

Abstract: Threads as considered in thread algebra model behaviours to be controlled by some execution environment: upon each action performed by a thread, a reply from its execution environment -- which takes the action as an instruction to be processed -- determines how the thread proceeds. In this paper, we are concerned with the case where the execution environment is remote: we describe and analyse so… ▽ More Threads as considered in thread algebra model behaviours to be controlled by some execution environment: upon each action performed by a thread, a reply from its execution environment -- which takes the action as an instruction to be processed -- determines how the thread proceeds. In this paper, we are concerned with the case where the execution environment is remote: we describe and analyse some transmission protocols for passing instructions from a thread to a remote execution environment. △ Less

Submitted 17 February, 2009; originally announced February 2009.

Comments: 13 pages

Report number: PRG0903 ACM Class: D.2.1; D.2.4; F.1.1; F.3.1

Journal ref: In ICTAC 2009, pages 127--139. Springer-Verlag, LNCS 5684, 2009

Square root meadows

Authors: Jan A. Bergstra, I. Bethke

Abstract: Let Q_0 denote the rational numbers expanded to a meadow by totalizing inversion such that 0^{-1}=0. Q_0 can be expanded by a total sign function s that extracts the sign of a rational number. In this paper we discuss an extension Q_0(s ,\sqrt) of the signed rationals in which every number has a unique square root. Let Q_0 denote the rational numbers expanded to a meadow by totalizing inversion such that 0^{-1}=0. Q_0 can be expanded by a total sign function s that extracts the sign of a rational number. In this paper we discuss an extension Q_0(s ,\sqrt) of the signed rationals in which every number has a unique square root. △ Less

Submitted 29 January, 2009; originally announced January 2009.

Comments: 9 pages

Meadow enriched ACP process algebras

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

Abstract: We introduce the notion of an ACP process algebra. The models of the axiom system ACP are the origin of this notion. ACP process algebras have to do with processes in which no data are involved. We also introduce the notion of a meadow enriched ACP process algebra, which is a simple generalization of the notion of an ACP process algebra to processes in which data are involved. In meadow enriched… ▽ More We introduce the notion of an ACP process algebra. The models of the axiom system ACP are the origin of this notion. ACP process algebras have to do with processes in which no data are involved. We also introduce the notion of a meadow enriched ACP process algebra, which is a simple generalization of the notion of an ACP process algebra to processes in which data are involved. In meadow enriched ACP process algebras, the mathematical structure for data is a meadow. △ Less

Submitted 4 February, 2009; v1 submitted 20 January, 2009; originally announced January 2009.

Comments: 8 pages; correction in Table 3

Report number: PRG0902

Timed tuplix calculus and the Wesseling and van den Bergh equation

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

Abstract: 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 d… ▽ More 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. △ Less

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

Comments: 17 pages; phrasing improved, references updated; substantially improved; remarks added

Report number: PRG0901

Journal ref: Scientific Annals of Computer Science 23(2):169--190, 2013

Meadows and the equational specification of division

Authors: J. A. Bergstra, Y. Hirshfeld, J. V. Tucker

Abstract: The rational, real and complex numbers with their standard operations, including division, are partial algebras specified by the axiomatic concept of a field. Since the class of fields cannot be defined by equations, the theory of equational specifications of data types cannot use field theory in applications to number systems based upon rational, real and complex numbers. We study a new axiomat… ▽ More The rational, real and complex numbers with their standard operations, including division, are partial algebras specified by the axiomatic concept of a field. Since the class of fields cannot be defined by equations, the theory of equational specifications of data types cannot use field theory in applications to number systems based upon rational, real and complex numbers. We study a new axiomatic concept for number systems with division that uses only equations: a meadow is a commutative ring with a total inverse operator satisfying two equations which imply that the inverse of zero is zero. All fields and products of fields can be viewed as meadows. After reviewing alternate axioms for inverse, we start the development of a theory of meadows. We give a general representation theorem for meadows and find, as a corollary, that the conditional equational theory of meadows coincides with the conditional equational theory of zero totalized fields. We also prove representation results for meadows of finite characteristic. △ Less

Submitted 7 January, 2009; originally announced January 2009.

Skew Meadows

Authors: J. A. Bergstra, Y. Hirshfeld, J. V. Tucker

Abstract: A skew meadow is a non-commutative ring with an inverse operator satisfying two special equations and in which the inverse of zero is zero. All skew fields and products of skew fields can be viewed as skew meadows. Conversely, we give an embedding of non-trivial skew meadows into products of skew fields, from which a completeness result for the equational logic of skew fields is derived. The rel… ▽ More A skew meadow is a non-commutative ring with an inverse operator satisfying two special equations and in which the inverse of zero is zero. All skew fields and products of skew fields can be viewed as skew meadows. Conversely, we give an embedding of non-trivial skew meadows into products of skew fields, from which a completeness result for the equational logic of skew fields is derived. The relationship between regularity conditions on rings and skew meadows is investigated. △ Less

Submitted 7 January, 2009; originally announced January 2009.

Instruction sequences for the production of processes

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

Abstract: Single-pass instruction sequences under execution are considered to produce behaviours to be controlled by some execution environment. Threads as considered in thread algebra model such behaviours: upon each action performed by a thread, a reply from its execution environment determines how the thread proceeds. Threads in turn can be looked upon as producing processes as considered in process al… ▽ More Single-pass instruction sequences under execution are considered to produce behaviours to be controlled by some execution environment. Threads as considered in thread algebra model such behaviours: upon each action performed by a thread, a reply from its execution environment determines how the thread proceeds. Threads in turn can be looked upon as producing processes as considered in process algebra. We show that, by apposite choice of basic instructions, all processes that can only be in a finite number of states can be produced by single-pass instruction sequences. △ Less

Submitted 18 November, 2008; v1 submitted 4 November, 2008; originally announced November 2008.

Comments: 23 pages; acknowledgement corrected, reference updated

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

A static theory of promises

Authors: Jan A. Bergstra, Mark Burgess

Abstract: We discuss for the concept of promises within a framework that can be applied to either humans or technology. We compare promises to the more established notion of obligations and find promises to be both simpler and more effective at reducing uncertainty in behavioural outcomes. We discuss for the concept of promises within a framework that can be applied to either humans or technology. We compare promises to the more established notion of obligations and find promises to be both simpler and more effective at reducing uncertainty in behavioural outcomes. △ Less

Submitted 30 January, 2014; v1 submitted 18 October, 2008; originally announced October 2008.

Comments: 36 pages. Revision of v4. In v5 some remarks about the institution of promising in the philosophy of Law have been included as well as a comment concerning the anthropology of promising. Several minor mistakes were found and remedied

Periodic Single-Pass Instruction Sequences

Authors: Jan A. Bergstra, Alban Ponse

Abstract: A program is a finite piece of data that produces a (possibly infinite) sequence of primitive instructions. From scratch we develop a linear notation for sequential, imperative programs, using a familiar class of primitive instructions and so-called repeat instructions, a particular type of control instructions. The resulting mathematical structure is a semigroup. We relate this set of programs to… ▽ More A program is a finite piece of data that produces a (possibly infinite) sequence of primitive instructions. From scratch we develop a linear notation for sequential, imperative programs, using a familiar class of primitive instructions and so-called repeat instructions, a particular type of control instructions. The resulting mathematical structure is a semigroup. We relate this set of programs to program algebra (PGA) and show that a particular subsemigroup is a carrier for PGA by providing axioms for single-pass congruence, structural congruence, and thread extraction. This subsemigroup characterizes periodic single-pass instruction sequences and provides a direct basis for PGA's toolset. △ Less

Submitted 16 April, 2013; v1 submitted 7 October, 2008; originally announced October 2008.

Comments: 16 pages, 3 tables, New title

ACM Class: D.3.1; F.3.2

On the expressiveness of single-pass instruction sequences

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

Abstract: 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 instructi… ▽ More 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. △ Less

Submitted 13 January, 2009; v1 submitted 7 October, 2008; originally announced October 2008.

Comments: 14 pages; error corrected, acknowledgement added; another error corrected, another acknowledgement added

Report number: PRG0813 ACM Class: D.1.4; D.3.3; F.1.1; F.3.3

Journal ref: Theory of Computing Systems, 50(2):313--328, 2012

Mechanistic Behavior of Single-Pass Instruction Sequences

Authors: Jan A. Bergstra, Mark B. van der Zwaag

Abstract: Earlier work on program and thread algebra detailed the functional, observable behavior of programs under execution. In this article we add the modeling of unobservable, mechanistic processing, in particular processing due to jump instructions. We model mechanistic processing preceding some further behavior as a delay of that behavior; we borrow a unary delay operator from discrete time process… ▽ More Earlier work on program and thread algebra detailed the functional, observable behavior of programs under execution. In this article we add the modeling of unobservable, mechanistic processing, in particular processing due to jump instructions. We model mechanistic processing preceding some further behavior as a delay of that behavior; we borrow a unary delay operator from discrete time process algebra. We define a mechanistic improvement ordering on threads and observe that some threads do not have an optimal implementation. △ Less

Submitted 26 September, 2008; originally announced September 2008.

Comments: 12 pages

ACM Class: D.1.4; F.3.2; F.3.3