arXiv subjects

J. A. Bergstra

Publications and source records attributed to J. A. Bergstra.

At least 55 records · Page 3Linked to original sources

arXiv2011

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.

q-fin.GN↗

arXiv2010

Business Mereology: Imaginative Definitions of Insourcing and Outsourcing Transformations

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.

cs.SE↗

arXiv2010

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.

q-fin.GN↗

arXiv2010

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.

math.RA↗

arXiv2010

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.

math.RA↗

arXiv2010

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.

cs.PL↗

arXiv2010

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.

cs.LO↗

arXiv2010

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.

cs.CC↗

arXiv2010

On the definition of a theoretical concept of an operating system

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.

cs.OS↗

arXiv2010

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.

cs.LO↗

arXiv2010

Proposition Algebra with Projective Limits

Sequential propositional logic deviates from ordinary propositional logic by taking into account that during the sequential evaluation of a propositional statement,atomic propositions may yield different Boolean values at repeated occurrences. We introduce `free valuations' to capture this dynamics of a propositional statement's environment. The resulting logic is phrased as an equationally specified algebra rather than in the form of proof rules, and is named `proposition algebra'. It is strictly more general than Boolean algebra to the extent that the classical connectives fail to be expressively complete in the sequential case. The four axioms for free valuation congruence are then combined with other axioms in order define a few more valuation congruences that gradually identify more propositional statements, up to static valuation congruence (which is the setting of conventional propositional logic). Proposition algebra is developed in a fashion similar to the process algebra ACP and the program algebra PGA, via an algebraic specification which has a meaningful initial algebra for which a range of coarser congruences are considered important as well. In addition infinite objects (that is propositional statements, processes and programs respectively) are dealt with by means of an inverse limit construction which allows the transfer of knowledge concerning finite objects to facts about infinite ones while reducing all facts about infinite objects to an infinity of facts about finite ones in return.

cs.LO↗

arXiv2009

Partial Komori fields and imperative Komori fields

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.

math.RA↗

arXiv2009

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.

cs.PL↗

arXiv2009

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.

cs.PL↗

arXiv2009

A protocol for instruction stream processing

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.

cs.PL↗

arXiv2009

Machine structure oriented control code logic

Control code is a concept that is closely related to a frequently occurring practitioner's view on what is a program: code that is capable of controlling the behaviour of some machine. We present a logical approach to explain issues concerning control codes that are independent of the details of the behaviours that are controlled. Using this approach, such issues can be explained at a very abstract level. We illustrate this among other things by means of an example about the production of a new compiler from an existing one. The approach is based on abstract machine models, called machine structures. We introduce a model of systems that provide execution environments for the executable codes of machine structures and use it to go into portability of control codes.

cs.SE↗

arXiv2009

Transmission protocols for instruction streams

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.

cs.PL↗

arXiv2009

Meadow enriched ACP process algebras

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.

math.RA↗