Showing 1–50 of 123 results for author: Bergstra, J

Revisiting Constant Negative Rewards for Goal-Reaching Tasks in Robot Learning

Authors: Gautham Vasan, Yan Wang, Fahim Shahriar, James Bergstra, Martin Jagersand, A. Rupam Mahmood

Abstract: Many real-world robot learning problems, such as pick-and-place or arriving at a destination, can be seen as a problem of reaching a goal state as soon as possible. These problems, when formulated as episodic reinforcement learning tasks, can easily be specified to align well with our intended goal: -1 reward every time step with termination upon reaching the goal state, called minimum-time tasks.… ▽ More Many real-world robot learning problems, such as pick-and-place or arriving at a destination, can be seen as a problem of reaching a goal state as soon as possible. These problems, when formulated as episodic reinforcement learning tasks, can easily be specified to align well with our intended goal: -1 reward every time step with termination upon reaching the goal state, called minimum-time tasks. Despite this simplicity, such formulations are often overlooked in favor of dense rewards due to their perceived difficulty and lack of informativeness. Our studies contrast the two reward paradigms, revealing that the minimum-time task specification not only facilitates learning higher-quality policies but can also surpass dense-reward-based policies on their own performance metrics. Crucially, we also identify the goal-hit rate of the initial policy as a robust early indicator for learning success in such sparse feedback settings. Finally, using four distinct real-robotic platforms, we show that it is possible to learn pixel-based policies from scratch within two to three hours using constant negative rewards. △ Less

Submitted 29 June, 2024; originally announced July 2024.

Comments: In Proceedings of Reinforcement Learning Conference 2024. For video demo, see https://drive.google.com/file/d/1O8D3oCWq5xf2hi1JOlMBbs6W1ClrvUFb/view?usp=sharing

Rings with common division, common meadows and their conditional equational theories

Authors: Jan A Bergstra, John V Tucker

Abstract: We examine the consequences of having a total division operation $\frac{x}{y}$ on commutative rings. We consider two forms of binary division, one derived from a unary inverse, the other defined directly as a general operation; each are made total by setting $1/0$ equal to an error value $\bot$, which is added to the ring. Such totalised divisions we call common divisions. In a field the two forms… ▽ More We examine the consequences of having a total division operation $\frac{x}{y}$ on commutative rings. We consider two forms of binary division, one derived from a unary inverse, the other defined directly as a general operation; each are made total by setting $1/0$ equal to an error value $\bot$, which is added to the ring. Such totalised divisions we call common divisions. In a field the two forms are equivalent and we have a finite equational axiomatisation $E$ that is complete for the equational theory of fields equipped with common division, called common meadows. These equational axioms $E$ turn out to be true of commutative rings with common division but only when defined via inverses. We explore these axioms $E$ and their role in seeking a completeness theorem for the conditional equational theory of common meadows. We prove they are complete for the conditional equational theory of commutative rings with inverse based common division. By adding a new proof rule, we can prove a completeness theorem for the conditional equational theory of common meadows. Although, the equational axioms $E$ fail with common division defined directly, we observe that the direct division does satisfies the equations in $E$ under a new congruence for partial terms called eager equality. △ Less

Submitted 26 May, 2024; v1 submitted 2 May, 2024; originally announced May 2024.

A Statistical Guarantee for Representation Transfer in Multitask Imitation Learning

Authors: Bryan Chan, Karime Pereida, James Bergstra

Abstract: Transferring representation for multitask imitation learning has the potential to provide improved sample efficiency on learning new tasks, when compared to learning from scratch. In this work, we provide a statistical guarantee indicating that we can indeed achieve improved sample efficiency on the target task when a representation is trained using sufficiently diverse source tasks. Our theoretic… ▽ More Transferring representation for multitask imitation learning has the potential to provide improved sample efficiency on learning new tasks, when compared to learning from scratch. In this work, we provide a statistical guarantee indicating that we can indeed achieve improved sample efficiency on the target task when a representation is trained using sufficiently diverse source tasks. Our theoretical results can be readily extended to account for commonly used neural network architectures with realistic assumptions. We conduct empirical analyses that align with our theoretical findings on four simulated environments$\unicode{x2014}$in particular leveraging more data from source tasks can improve sample efficiency on learning in the new task. △ Less

Submitted 2 November, 2023; originally announced November 2023.

Comments: Accepted by NeurIPS 2023 Workshop on Robot Learning

A Complete Finite Axiomatisation of the Equational Theory of Common Meadows

Authors: Jan A Bergstra, John V Tucker

Abstract: We analyse abstract data types that model numerical structures with a concept of error. Specifically, we focus on arithmetic data types that contain an error value $\bot$ whose main purpose is to always return a value for division. To rings and fields, we add a division operator $x/y$ and study a class of algebras called common meadows wherein $x/0 = \bot$. The set of equations true in all common… ▽ More We analyse abstract data types that model numerical structures with a concept of error. Specifically, we focus on arithmetic data types that contain an error value $\bot$ whose main purpose is to always return a value for division. To rings and fields, we add a division operator $x/y$ and study a class of algebras called common meadows wherein $x/0 = \bot$. The set of equations true in all common meadows is named the equational theory of common meadows. We give a finite equational axiomatisation of the equational theory of common meadows and prove that it is complete and that the equational theory is decidable. △ Less

Submitted 26 May, 2024; v1 submitted 9 July, 2023; originally announced July 2023.

Conditional logic as a short-circuit logic

Authors: Jan A. Bergstra, Alban Ponse

Abstract: Both two-valued and three-valued conditional logic (CL), defined by Guzmán and Squier (1990) and based on McCarthy's non-commutative connectives, axiomatise a short-circuit logic (SCL) that defines more identities than MSCL (Memorising SCL), which also has a two- and a three-valued variant. This follows from the fact that the definable connective that prescribes full left-sequential conjunction is… ▽ More Both two-valued and three-valued conditional logic (CL), defined by Guzmán and Squier (1990) and based on McCarthy's non-commutative connectives, axiomatise a short-circuit logic (SCL) that defines more identities than MSCL (Memorising SCL), which also has a two- and a three-valued variant. This follows from the fact that the definable connective that prescribes full left-sequential conjunction is commutative in CL. We show that in CL, the full left-sequential connectives and negation define Bochvar's three-valued strict logic. In two-valued CL, the full left-sequential connectives and negation define a commutative logic that is weaker than propositional logic because the absorption laws do not hold. Next, we show that the original, equational axiomatisation of CL is not independent and give several alternative, independent axiomatisations. △ Less

Submitted 28 September, 2023; v1 submitted 28 April, 2023; originally announced April 2023.

Comments: 20 pages, 4 tables. Differences with v1: 1) Definitions 3.7 and 3.8 - the normal forms are more elegantly defined, based on a set of strings A^s which now includes the empty string: nicer proofs of La.3.10 and Thm.3.11; the same goes for the related definitions and proofs in the setting with U. 2) Thm.5.1 - best Prover9 results tightened

MSC Class: 03C90 ACM Class: F.3.1; F.3.2

Active Perception and Representation for Robotic Manipulation

Authors: Youssef Zaky, Gaurav Paruthi, Bryan Tripp, James Bergstra

Abstract: The vast majority of visual animals actively control their eyes, heads, and/or bodies to direct their gaze toward different parts of their environment. In contrast, recent applications of reinforcement learning in robotic manipulation employ cameras as passive sensors. These are carefully placed to view a scene from a fixed pose. Active perception allows animals to gather the most relevant informa… ▽ More The vast majority of visual animals actively control their eyes, heads, and/or bodies to direct their gaze toward different parts of their environment. In contrast, recent applications of reinforcement learning in robotic manipulation employ cameras as passive sensors. These are carefully placed to view a scene from a fixed pose. Active perception allows animals to gather the most relevant information about the world and focus their computational resources where needed. It also enables them to view objects from different distances and viewpoints, providing a rich visual experience from which to learn abstract representations of the environment. Inspired by the primate visual-motor system, we present a framework that leverages the benefits of active perception to accomplish manipulation tasks. Our agent uses viewpoint changes to localize objects, to learn state representations in a self-supervised manner, and to perform goal-directed actions. We apply our model to a simulated gras** task with a 6-DoF action space. Compared to its passive, fixed-camera counterpart, the active model achieves 8% better performance in targeted gras**. Compared to vanilla deep Q-learning algorithms, our model is at least four times more sample-efficient, highlighting the benefits of both active perception and representation learning. △ Less

Submitted 14 March, 2020; originally announced March 2020.

Candidate Software Process Flaws for the Boeing 737 Max MCAS Algorithm and Risks for a Proposed Upgrade

Authors: Jan A. Bergstra, Mark Burgess

Abstract: By reasoning about the claims and speculations promised as part of the public discourse, we analyze the hypothesis that flaws in software engineering played a critical role in the Boeing 737 MCAS incidents. We use promise-based reasoning to discuss how, from an outsider's perspective, one may assemble clues about what went wrong. Rather than looking for a Rational Alternative Design (RAD), as sugg… ▽ More By reasoning about the claims and speculations promised as part of the public discourse, we analyze the hypothesis that flaws in software engineering played a critical role in the Boeing 737 MCAS incidents. We use promise-based reasoning to discuss how, from an outsider's perspective, one may assemble clues about what went wrong. Rather than looking for a Rational Alternative Design (RAD), as suggested by Wendel, we look for candidate flaws in the software process. We describe four such potential flaws. Recently, Boeing has circulated information on its envisaged MCAS algorithm upgrade. We cast this as a promise to resolve the flaws, i.e. to provide a RAD for the B737 Max. We offer an assessment of B-Max-New based on the public discourse. △ Less

Submitted 16 January, 2020; originally announced January 2020.

Comments: Sequel to arXiv:2001.01543 [cs.OH]

ACM Class: D.2.m; K.4.0; A.1

A Promise Theoretic Account of the Boeing 737 Max MCAS Algorithm Affair

Authors: J. A. Bergstra, M. Burgess

Abstract: Many public controversies involve the assessment of statements about which we have imperfect information. Without a structured approach, it is quite difficult to develop an approach to reasoning which is not based on ad hoc choices. Forms of logic have been used in the past to try to bring such clarity, but these fail for a variety of reasons. We demonstrate a simple approach to bringing a standar… ▽ More Many public controversies involve the assessment of statements about which we have imperfect information. Without a structured approach, it is quite difficult to develop an approach to reasoning which is not based on ad hoc choices. Forms of logic have been used in the past to try to bring such clarity, but these fail for a variety of reasons. We demonstrate a simple approach to bringing a standardized approach to semantics, in certain discourse, using Promise Theory. As a case, we use Promise Theory (PT) to collect and structure publicly available information about the case of the MCAS software component for the Boeing 737 Max flight control system. △ Less

Submitted 24 December, 2019; originally announced January 2020.

ACM Class: D.2.m; K.4.0; A.1

Using Hoare logic in a process algebra setting

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

Abstract: This paper concerns the relation between process algebra and Hoare logic. We investigate the question whether and how a Hoare logic can be used for reasoning about how data change in the course of a process when reasoning equationally about that process. We introduce an extension of ACP (Algebra of Communicating Processes) with features that are relevant to processes in which data are involved, pr… ▽ More This paper concerns the relation between process algebra and Hoare logic. We investigate the question whether and how a Hoare logic can be used for reasoning about how data change in the course of a process when reasoning equationally about that process. We introduce an extension of ACP (Algebra of Communicating Processes) with features that are relevant to processes in which data are involved, present a Hoare logic for the processes considered in this process algebra, and discuss the use of this Hoare logic as a complement to pure equational reasoning with the equational axioms of the process algebra. △ Less

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

Comments: 24 pages; presentation improved, examples added

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

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

Quantitative Expressiveness of Instruction Sequence Classes for Computation on Single Bit Registers

Authors: Jan A. Bergstra

Abstract: The number of instructions of an instruction sequence is taken for its logical SLOC, and is abbreviated with LLOC. A notion of quantitative expressiveness is based on LLOC and in the special case of operation over a family of single bit registers a collection of elementary properties are established. A dedicated notion of interface is developed and is used for stating relevant properties of classe… ▽ More The number of instructions of an instruction sequence is taken for its logical SLOC, and is abbreviated with LLOC. A notion of quantitative expressiveness is based on LLOC and in the special case of operation over a family of single bit registers a collection of elementary properties are established. A dedicated notion of interface is developed and is used for stating relevant properties of classes of instruction sequences △ Less

Submitted 18 April, 2019; originally announced April 2019.

ACM Class: F.1.1; F.2.1

Autoregressive Policies for Continuous Control Deep Reinforcement Learning

Authors: Dmytro Korenkevych, A. Rupam Mahmood, Gautham Vasan, James Bergstra

Abstract: Reinforcement learning algorithms rely on exploration to discover new behaviors, which is typically achieved by following a stochastic policy. In continuous control tasks, policies with a Gaussian distribution have been widely adopted. Gaussian exploration however does not result in smooth trajectories that generally correspond to safe and rewarding behaviors in practical tasks. In addition, Gauss… ▽ More Reinforcement learning algorithms rely on exploration to discover new behaviors, which is typically achieved by following a stochastic policy. In continuous control tasks, policies with a Gaussian distribution have been widely adopted. Gaussian exploration however does not result in smooth trajectories that generally correspond to safe and rewarding behaviors in practical tasks. In addition, Gaussian policies do not result in an effective exploration of an environment and become increasingly inefficient as the action rate increases. This contributes to a low sample efficiency often observed in learning continuous control tasks. We introduce a family of stationary autoregressive (AR) stochastic processes to facilitate exploration in continuous control domains. We show that proposed processes possess two desirable features: subsequent process observations are temporally coherent with continuously adjustable degree of coherence, and the process stationary distribution is standard normal. We derive an autoregressive policy (ARP) that implements such processes maintaining the standard agent-environment interface. We show how ARPs can be easily used with the existing off-the-shelf learning algorithms. Empirically we demonstrate that using ARPs results in improved exploration and sample efficiency in both simulated and real world domains, and, furthermore, provides smooth exploration trajectories that enable safe operation of robotic hardware. △ Less

Submitted 27 March, 2019; originally announced March 2019.

Comments: Submitted to 28th International Joint Conference on Artificial Intelligence (IJCAI 2019). Video: https://youtu.be/NCpyXBNqNmw Code: https://github.com/dkorenkevych/arp

Program algebra for Turing-machine programs

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

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

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

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

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

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

Propositional logic with short-circuit evaluation: a non-commutative and a commutative variant

Authors: Jan A. Bergstra, Alban Ponse, Daan 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. Short-circuit evaluation is widely used in programming, with sequential conjunction and disjunction as primitive connectives. We study the question which logical laws axiomatize short-circuit ev… ▽ 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. Short-circuit evaluation is widely used in programming, with sequential conjunction and disjunction as primitive connectives. We study the question which logical laws axiomatize short-circuit evaluation under the following assumptions: compound statements are evaluated from left to right, each atom (propositional variable) evaluates to either true or false, and atomic evaluations can cause a side effect. The answer to this question depends on the kind of atomic side effects that can occur and leads to different "short-circuit logics". The basic case is FSCL (free short-circuit logic), which characterizes the setting in which each atomic evaluation can cause a side effect. We recall some main results and then relate FSCL to MSCL (memorizing short-circuit logic), where in the evaluation of a compound statement, the first evaluation result of each atom is memorized. MSCL can be seen as a sequential variant of propositional logic: atomic evaluations cannot cause a side effect and the sequential connectives are not commutative. Then we relate MSCL to SSCL (static short-circuit logic), the variant of propositional logic that prescribes short-circuit evaluation with commutative sequential connectives. We present evaluation trees as an intuitive semantics for short-circuit evaluation, and simple equational axiomatizations for the short-circuit logics mentioned that use negation and the sequential connectives only. △ Less

Submitted 4 October, 2018; originally announced October 2018.

Comments: 34 pages, 6 tables. Considerable parts of the text below stem from arXiv:1206.1936, arXiv:1010.3674, and arXiv:1707.05718. Together with arXiv:1707.05718, this paper subsumes most of arXiv:1010.3674

MSC Class: 03C90 ACM Class: F.3.1; F.3.2

Benchmarking Reinforcement Learning Algorithms on Real-World Robots

Authors: A. Rupam Mahmood, Dmytro Korenkevych, Gautham Vasan, William Ma, James Bergstra

Abstract: Through many recent successes in simulation, model-free reinforcement learning has emerged as a promising approach to solving continuous control robotic tasks. The research community is now able to reproduce, analyze and build quickly on these results due to open source implementations of learning algorithms and simulated benchmark tasks. To carry forward these successes to real-world applications… ▽ More Through many recent successes in simulation, model-free reinforcement learning has emerged as a promising approach to solving continuous control robotic tasks. The research community is now able to reproduce, analyze and build quickly on these results due to open source implementations of learning algorithms and simulated benchmark tasks. To carry forward these successes to real-world applications, it is crucial to withhold utilizing the unique advantages of simulations that do not transfer to the real world and experiment directly with physical robots. However, reinforcement learning research with physical robots faces substantial resistance due to the lack of benchmark tasks and supporting source code. In this work, we introduce several reinforcement learning tasks with multiple commercially available robots that present varying levels of learning difficulty, setup, and repeatability. On these tasks, we test the learning performance of off-the-shelf implementations of four reinforcement learning algorithms and analyze sensitivity to their hyper-parameters to determine their readiness for applications in various real-world tasks. Our results show that with a careful setup of the task interface and computations, some of these implementations can be readily applicable to physical robots. We find that state-of-the-art learning algorithms are highly sensitive to their hyper-parameters and their relative ordering does not transfer across tasks, indicating the necessity of re-tuning them for each task for best performance. On the other hand, the best hyper-parameter configuration from one task may often result in effective learning on held-out tasks even with different robots, providing a reasonable default. We make the benchmark tasks publicly available to enhance reproducibility in real-world reinforcement learning. △ Less

Submitted 20 September, 2018; originally announced September 2018.

Comments: Appears in Proceedings of the Second Conference on Robot Learning (CoRL 2018). Companion video at https://youtu.be/ovDfhvjpQd8 and source code at https://github.com/kindredresearch/SenseAct

A short introduction to program algebra with instructions for Boolean registers

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

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

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

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

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

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

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

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

Abstract: This paper concerns the question to what extent it can be efficiently determined whether an arbitrary program correctly solves a given problem. This question is investigated with programs of a very simple form, namely instruction sequences, and a very simple problem, namely the non-zeroness test on natural numbers. The instruction sequences concerned are of a kind by which, for each $n > 0$, each… ▽ More This paper concerns the question to what extent it can be efficiently determined whether an arbitrary program correctly solves a given problem. This question is investigated with programs of a very simple form, namely instruction sequences, and a very simple problem, namely the non-zeroness test on natural numbers. The instruction sequences concerned are of a kind by which, for each $n > 0$, each function from $\{0,1\}^n$ to $\{0,1\}$ can be computed. The established results include the time complexities of the problem of determining whether an arbitrary instruction sequence correctly implements the restriction to $\{0,1\}^n$ of the function from $\{0,1\}^*$ to $\{0,1\}$ that models the non-zeroness test function, for $n > 0$, under several restrictions on the arbitrary instruction sequence. △ Less

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

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

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

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

Setting up a Reinforcement Learning Task with a Real-World Robot

Authors: A. Rupam Mahmood, Dmytro Korenkevych, Brent J. Komer, James Bergstra

Abstract: Reinforcement learning is a promising approach to develo** hard-to-engineer adaptive solutions for complex and diverse robotic tasks. However, learning with real-world robots is often unreliable and difficult, which resulted in their low adoption in reinforcement learning research. This difficulty is worsened by the lack of guidelines for setting up learning tasks with robots. In this work, we d… ▽ More Reinforcement learning is a promising approach to develo** hard-to-engineer adaptive solutions for complex and diverse robotic tasks. However, learning with real-world robots is often unreliable and difficult, which resulted in their low adoption in reinforcement learning research. This difficulty is worsened by the lack of guidelines for setting up learning tasks with robots. In this work, we develop a learning task with a UR5 robotic arm to bring to light some key elements of a task setup and study their contributions to the challenges with robots. We find that learning performance can be highly sensitive to the setup, and thus oversights and omissions in setup details can make effective learning, reproducibility, and fair comparison hard. Our study suggests some mitigating steps to help future experimenters avoid difficulties and pitfalls. We show that highly reliable and repeatable experiments can be performed in our setup, indicating the possibility of reinforcement learning research extensively based on real-world robots. △ Less

Submitted 19 March, 2018; originally announced March 2018.

Comments: Submitted to 2018 IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS)

Universality of Univariate Mixed Fractions in Divisive Meadows

Authors: Jan A. Bergstra, Inge Bethke, Dimitri Hendriks

Abstract: Univariate fractions can be transformed to mixed fractions in the equational theory of meadows of characteristic zero. Univariate fractions can be transformed to mixed fractions in the equational theory of meadows of characteristic zero. △ Less

Submitted 3 July, 2017; originally announced July 2017.

Comments: 12 pages

Process algebra with strategic interleaving

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

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

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

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

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

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

Axioms for behavioural congruence of single-pass instruction sequences

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

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

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

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

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

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

Adams Conditioning and Likelihood Ratio Transfer Mediated Inference

Authors: Jan A. Bergstra

Abstract: Bayesian inference as applied in a legal setting is about belief transfer and involves a plurality of agents and communication protocols. A forensic expert (FE) may communicate to a trier of fact (TOF) first its value of a certain likelihood ratio with respect to FE's belief state as represented by a probability function on FE's proposition space. Subsequently FE communicates its recently acquir… ▽ More Bayesian inference as applied in a legal setting is about belief transfer and involves a plurality of agents and communication protocols. A forensic expert (FE) may communicate to a trier of fact (TOF) first its value of a certain likelihood ratio with respect to FE's belief state as represented by a probability function on FE's proposition space. Subsequently FE communicates its recently acquired confirmation that a certain evidence proposition is true. Then TOF performs likelihood ratio transfer mediated reasoning thereby revising their own belief state. The logical principles involved in likelihood transfer mediated reasoning are discussed in a setting where probabilistic arithmetic is done within a meadow, and with Adams conditioning placed in a central role. △ Less

Submitted 16 August, 2019; v1 submitted 26 November, 2016; originally announced November 2016.

Comments: Based on reviewer's comments many minor improvements have been made

Datatype defining rewrite systems for naturals and integers

Authors: Jan A. Bergstra, Alban Ponse

Abstract: A datatype defining rewrite system (DDRS) is an algebraic (equational) specification intended to specify a datatype. When interpreting the equations from left-to-right, a DDRS defines a term rewriting system that must be ground-complete. First we define two DDRSs for the ring of integers, each comprising twelve rewrite rules, and prove their ground-completeness. Then we introduce natural number an… ▽ More A datatype defining rewrite system (DDRS) is an algebraic (equational) specification intended to specify a datatype. When interpreting the equations from left-to-right, a DDRS defines a term rewriting system that must be ground-complete. First we define two DDRSs for the ring of integers, each comprising twelve rewrite rules, and prove their ground-completeness. Then we introduce natural number and integer arithmetic specified according to unary view, that is, arithmetic based on a postfix unary append constructor (a form of tallying). Next we specify arithmetic based on two other views: binary and decimal notation. The binary and decimal view have as their characteristic that each normal form resembles common number notation, that is, either a digit, or a string of digits without leading zero, or the negated versions of the latter. Integer arithmetic in binary and decimal notation is based on (postfix) digit append functions. For each view we define a DDRS, and in each case the resulting datatype is a canonical term algebra that extends a corresponding canonical term algebra for natural numbers. Then, for each view, we consider an alternative DDRS based on tree constructors that yields comparable normal forms, which for that view admits expressions that are algorithmically more involved. For all DDRSs considered, ground-completeness is proven. △ Less

Submitted 17 February, 2021; v1 submitted 22 August, 2016; originally announced August 2016.

Comments: arXiv admin note: text overlap with arXiv:1406.3280

ACM Class: D.3.1

Journal ref: Logical Methods in Computer Science, Volume 17, Issue 1 (February 18, 2021) lmcs:6031

Theano: A Python framework for fast computation of mathematical expressions

Authors: The Theano Development Team, Rami Al-Rfou, Guillaume Alain, Amjad Almahairi, Christof Angermueller, Dzmitry Bahdanau, Nicolas Ballas, Frédéric Bastien, Justin Bayer, Anatoly Belikov, Alexander Belopolsky, Yoshua Bengio, Arnaud Bergeron, James Bergstra, Valentin Bisson, Josh Bleecher Snyder, Nicolas Bouchard, Nicolas Boulanger-Lewandowski, Xavier Bouthillier, Alexandre de Brébisson, Olivier Breuleux, Pierre-Luc Carrier, Kyunghyun Cho, Jan Chorowski, Paul Christiano , et al. (88 additional authors not shown)

Abstract: Theano is a Python library that allows to define, optimize, and evaluate mathematical expressions involving multi-dimensional arrays efficiently. Since its introduction, it has been one of the most used CPU and GPU mathematical compilers - especially in the machine learning community - and has shown steady performance improvements. Theano is being actively and continuously developed since 2008, mu… ▽ More Theano is a Python library that allows to define, optimize, and evaluate mathematical expressions involving multi-dimensional arrays efficiently. Since its introduction, it has been one of the most used CPU and GPU mathematical compilers - especially in the machine learning community - and has shown steady performance improvements. Theano is being actively and continuously developed since 2008, multiple frameworks have been built on top of it and it has been used to produce many state-of-the-art machine learning models. The present article is structured as follows. Section I provides an overview of the Theano software and its community. Section II presents the principal features of Theano and how to use them, and compares them with other similar projects. Section III focuses on recently-introduced functionalities and improvements. Section IV compares the performance of Theano against Torch7 and TensorFlow on several machine learning models. Section V discusses current limitations of Theano and potential ways of improving it. △ Less

Submitted 9 May, 2016; originally announced May 2016.

Comments: 19 pages, 5 figures

Transformation of fractions into simple fractions in divisive meadows

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

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

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

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

MSC Class: 12E12; 12L12; 68Q65

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

Subvarieties of the variety of meadows

Authors: Jan A. Bergstra, Inge Bethke

Abstract: Meadows - commutative rings equipped with a total inversion operation - can be axiomatized by purely equational means. We study subvarieties of the variety of meadows obtained by extending the equational theory and expanding the signature. Meadows - commutative rings equipped with a total inversion operation - can be axiomatized by purely equational means. We study subvarieties of the variety of meadows obtained by extending the equational theory and expanding the signature. △ Less

Submitted 19 April, 2016; v1 submitted 14 October, 2015; originally announced October 2015.

Comments: 11 pages

Contradiction-tolerant process algebra with propositional signals

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

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

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

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

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

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

A negative result on algebraic specifications of the meadow of rational numbers

Authors: Jan A. Bergstra, Inge Bethke

Abstract: $\mathbb{Q}_0$ - the involutive meadow of the rational numbers - is the field of the rational numbers where the multiplicative inverse operation is made total by imposing $0^{-1}=0$. In this note, we prove that $\mathbb{Q}_0$ cannot be specified by the usual axioms for meadows augmented by a finite set of axioms of the form $(1+ \cdots +1+x^2)\cdot (1+ \cdots +1 +x^2)^{-1}=1$. $\mathbb{Q}_0$ - the involutive meadow of the rational numbers - is the field of the rational numbers where the multiplicative inverse operation is made total by imposing $0^{-1}=0$. In this note, we prove that $\mathbb{Q}_0$ cannot be specified by the usual axioms for meadows augmented by a finite set of axioms of the form $(1+ \cdots +1+x^2)\cdot (1+ \cdots +1 +x^2)^{-1}=1$. △ Less

Submitted 22 January, 2016; v1 submitted 2 July, 2015; originally announced July 2015.

Comments: 5 pages, 2 tables

MSC Class: 12D15

Evaluation trees for proposition algebra

Authors: Jan A. Bergstra, Alban Ponse

Abstract: Proposition algebra is based on Hoare's conditional connective, which is a ternary connective comparable to if-then-else and used in the setting of propositional logic. Conditional statements are provided with a simple semantics that is based on evaluation trees and that characterizes so-called free valuation congruence: two conditional statements are free valuation congruent if, and only if, they… ▽ More Proposition algebra is based on Hoare's conditional connective, which is a ternary connective comparable to if-then-else and used in the setting of propositional logic. Conditional statements are provided with a simple semantics that is based on evaluation trees and that characterizes so-called free valuation congruence: two conditional statements are free valuation congruent if, and only if, they have equal evaluation trees. Free valuation congruence is axiomatized by the four basic equational axioms of proposition algebra that define the conditional connective. Valuation congruences that identify more conditional statements than free valuation congruence are repetition-proof, contractive, memorizing, and static valuation congruence. Each of these valuation congruences is characterized using a transformation on evaluation trees: two conditional statements are C-valuation congruent if, and only if, their C-transformed evaluation trees are equal. These transformations are simple and natural, and only for static valuation congruence a slightly more complex transformation is used. Also, each of these valuation congruences is axiomatized in proposition algebra. A spin-off of our approach can be called "normalization functions for proposition algebra": for each valuation congruence C considered, two conditional statements are C-valuation congruent if, and only if, the C-normalization function returns equal images. △ Less

Submitted 28 August, 2017; v1 submitted 30 April, 2015; originally announced April 2015.

Comments: 34 pages, 1 table; main differences with v2: some proofs are corrected and/or simplified in S.3-6

MSC Class: 03B05; 03B70 ACM Class: F.3.2

Architectural Adequacy and Evolutionary Adequacy as Characteristics of a Candidate Informational Money

Authors: Jan A. Bergstra

Abstract: For money-like informational commodities the notions of architectural adequacy and evolutionary adequacy are proposed as the first two stages of a moneyness maturity hierarchy. Then three classes of informational commodities are distinguished: exclusively informational commodities, strictly informational commodities, and ownable informational commodities. For each class money-like instances of tha… ▽ More For money-like informational commodities the notions of architectural adequacy and evolutionary adequacy are proposed as the first two stages of a moneyness maturity hierarchy. Then three classes of informational commodities are distinguished: exclusively informational commodities, strictly informational commodities, and ownable informational commodities. For each class money-like instances of that commodity class, as well as monies of that class may exist. With the help of these classifications and making use of previous assessments of Bitcoin, it is argued that at this stage Bitcoin is unlikely ever to evolve into a money. Assessing the evolutionary adequacy of Bitcoin is perceived in terms of a search through its design hull for superior design alternatives. An extensive comparison is made between the search for superior design alternatives to Bitcoin and the search for design alternatives to a specific and unconventional view on the definition of fractions. △ Less

Submitted 27 April, 2015; originally announced April 2015.

Comments: 25 pages

On instruction sets for Boolean registers in program algebra

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

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

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

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

ACM Class: F.1.1; F.1.3

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

Instruction sequence size complexity of parity

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

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

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

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

ACM Class: F.1.1; F.1.3

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

Personal Multi-threading

Authors: Jan A. Bergstra

Abstract: Multi-threading allows agents to pursue a heterogeneous collection of tasks in an orderly manner. The view of multi-threading that emerges from thread algebra is applied to the case where a single agent, who may be human, maintains a hierarchical multithread as an architecture of its own activities. Multi-threading allows agents to pursue a heterogeneous collection of tasks in an orderly manner. The view of multi-threading that emerges from thread algebra is applied to the case where a single agent, who may be human, maintains a hierarchical multithread as an architecture of its own activities. △ Less

Submitted 11 December, 2014; originally announced December 2014.

Note on paraconsistency and reasoning about fractions

Authors: Jan A. Bergstra, Inge Bethke

Abstract: We apply a paraconsistent logic to reason about fractions. We apply a paraconsistent logic to reason about fractions. △ Less

Submitted 6 March, 2015; v1 submitted 31 October, 2014; originally announced October 2014.

Comments: 6 pages

Report number: report TCS1413, October 2014 ACM Class: F.4.1

Probabilistic thread algebra

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

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

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

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

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

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

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

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

Abstract: We present a formal system for proving the partial correctness of a single-pass instruction sequence as considered in program algebra by decomposition into proofs of the partial correctness of segments of the single-pass instruction sequence concerned. The system is similar to Hoare logics, but takes into account that, by the presence of jump instructions, segments of single-pass instruction seque… ▽ More We present a formal system for proving the partial correctness of a single-pass instruction sequence as considered in program algebra by decomposition into proofs of the partial correctness of segments of the single-pass instruction sequence concerned. The system is similar to Hoare logics, but takes into account that, by the presence of jump instructions, segments of single-pass instruction sequences may have multiple entry points and multiple exit points. It is intended to support a sound general understanding of the issues with Hoare-like logics for low-level programming languages. △ Less

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

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

ACM Class: D.2.4; F.3.1

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

Three Datatype Defining Rewrite Systems for Datatypes of Integers each extending a Datatype of Naturals

Authors: Jan A. Bergstra, Alban Ponse

Abstract: Integer arithmetic is specified according to three views: unary, binary, and decimal notation. The binary and decimal view have as their characteristic that each normal form resembles common number notation, that is, either a digit, or a string of digits without leading zero, or the negated versions of the latter. The unary view comprises a specification of integer arithmetic based on 0, successor… ▽ More Integer arithmetic is specified according to three views: unary, binary, and decimal notation. The binary and decimal view have as their characteristic that each normal form resembles common number notation, that is, either a digit, or a string of digits without leading zero, or the negated versions of the latter. The unary view comprises a specification of integer arithmetic based on 0, successor function $S$, and predecessor function, with negative normal forms $-S^i(0)$. Integer arithmetic in binary and decimal notation is based on (postfix) digit append functions. For each view we define a ground-confluent and terminating datatype defining rewrite system (DDRS), and in each case the resulting datatype is a canonical term algebra that extends a corresponding canonical term algebra for natural numbers. Then, for each view, we consider an alternative DDRS based on tree constructors that yield comparable normal forms, which for that binary and decimal view admits expressions that are algorithmically more involved. These DDRSes are incorporated because they are closer to existing literature. For these DDRSes we also provide ground-completeness results. Finally, we define a DDRS for the ring of Integers (comprising fifteen rewrite rules) and prove its ground-completeness. △ Less

Submitted 18 July, 2016; v1 submitted 12 June, 2014; originally announced June 2014.

Comments: 33 pages; 19 tables. All DDRSes in S.2 are proven ground-complete (gc). In S.3, the DDRS for Z_{ut} contains 16 equations and is proven gc; the DDRS for Z_{bt} has one more equation ([bt22]) and is proven gc; the DDRSes for N_{dt} (Table 14) and Z_{dt} (Table 16) are proven gc in [13]. In Appendix C, corrected versions of the DDRSes for N_{u'} and Z_{u'} are proven gc

ACM Class: D.3.1

Division by zero in non-involutive meadows

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

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

Submitted 9 June, 2014; originally announced June 2014.

Comments: 14 pages

MSC Class: 12E12; 12L12; 68Q65

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

On algorithmic equivalence of instruction sequences for computing bit string functions

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

Abstract: Every partial function from bit strings of a given length to bit strings of a possibly different given length can be computed by a finite instruction sequence that contains only instructions to set and get the content of Boolean registers, forward jump instructions, and a termination instruction. We look for an equivalence relation on instruction sequences of this kind that captures to a reasonabl… ▽ More Every partial function from bit strings of a given length to bit strings of a possibly different given length can be computed by a finite instruction sequence that contains only instructions to set and get the content of Boolean registers, forward jump instructions, and a termination instruction. We look for an equivalence relation on instruction sequences of this kind that captures to a reasonable degree the intuitive notion that two instruction sequences express the same algorithm. △ Less

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

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

ACM Class: F.1.1; F.2.0

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

Bitcoin: a Money-like Informational Commodity

Authors: Jan A. Bergstra, Peter Weijland

Abstract: The question "what is Bitcoin" allows for many answers depending on the objectives aimed at when providing such answers. The question addressed in this paper is to determine a top-level classification, or type, for Bitcoin. We will classify Bitcoin as a system of type money-like informational commodity (MLIC). The question "what is Bitcoin" allows for many answers depending on the objectives aimed at when providing such answers. The question addressed in this paper is to determine a top-level classification, or type, for Bitcoin. We will classify Bitcoin as a system of type money-like informational commodity (MLIC). △ Less

Submitted 19 February, 2014; originally announced February 2014.

Report number: Report TCS 1402

Promises, Impositions, and other Directionals

Authors: Jan A. Bergstra, Mark Burgess

Abstract: Promises, impositions, proposals, predictions, and suggestions are categorized as voluntary co-operational methods. The class of voluntary co-operational methods is included in the class of so-called directionals. Directionals are mechanisms supporting the mutual coordination of autonomous agents. Notations are provided capable of expressing residual fragments of directionals. An extensive examp… ▽ More Promises, impositions, proposals, predictions, and suggestions are categorized as voluntary co-operational methods. The class of voluntary co-operational methods is included in the class of so-called directionals. Directionals are mechanisms supporting the mutual coordination of autonomous agents. Notations are provided capable of expressing residual fragments of directionals. An extensive example, involving promises about the suitability of programs for tasks imposed on the promisee is presented. The example illustrates the dynamics of promises and more specifically the corresponding mechanism of trust updating and credibility updating. Trust levels and credibility levels then determine the way certain promises and impositions are handled. The ubiquity of promises and impositions is further demonstrated with two extensive examples involving human behaviour: an artificial example about an agent planning a purchase, and a realistic example describing technology mediated interaction concerning the solution of pay station failure related problems arising for an agent intending to leave the parking area. △ Less

Submitted 14 January, 2014; originally announced January 2014.

Comments: 55 pages

Long multiplication by instruction sequences with backward jump instructions

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

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

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

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

ACM Class: F.1.1; F.2.1

Instruction sequences expressing multiplication algorithms

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

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

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

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

ACM Class: F.1.1; F.2.1

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

Equations for formally real meadows

Authors: Jan A. Bergstra, Inge Bethke, Alban Ponse

Abstract: We consider the signatures $Σ_m=(0,1,-,+, \cdot, \ ^{-1})$ of meadows and $(Σ_m, {\mathbf s})$ of signed meadows. We give two complete axiomatizations of the equational theories of the real numbers with respect to these signatures. In the first case, we extend the axiomatization of zero-totalized fields by a single axiom scheme expressing formal realness; the second axiomatization presupposes an o… ▽ More We consider the signatures $Σ_m=(0,1,-,+, \cdot, \ ^{-1})$ of meadows and $(Σ_m, {\mathbf s})$ of signed meadows. We give two complete axiomatizations of the equational theories of the real numbers with respect to these signatures. In the first case, we extend the axiomatization of zero-totalized fields by a single axiom scheme expressing formal realness; the second axiomatization presupposes an ordering. We apply these completeness results in order to obtain complete axiomatizations of the complex numbers. △ Less

Submitted 13 January, 2015; v1 submitted 18 October, 2013; originally announced October 2013.

Comments: 24 pages, 14 tables, revised, new Theorem 3.7

MSC Class: 12D15

Pylearn2: a machine learning research library

Authors: Ian J. Goodfellow, David Warde-Farley, Pascal Lamblin, Vincent Dumoulin, Mehdi Mirza, Razvan Pascanu, James Bergstra, Frédéric Bastien, Yoshua Bengio

Abstract: Pylearn2 is a machine learning research library. This does not just mean that it is a collection of machine learning algorithms that share a common API; it means that it has been designed for flexibility and extensibility in order to facilitate research projects that involve new or unusual use cases. In this paper we give a brief history of the library, an overview of its basic philosophy, a summa… ▽ More Pylearn2 is a machine learning research library. This does not just mean that it is a collection of machine learning algorithms that share a common API; it means that it has been designed for flexibility and extensibility in order to facilitate research projects that involve new or unusual use cases. In this paper we give a brief history of the library, an overview of its basic philosophy, a summary of the library's architecture, and a description of how the Pylearn2 community functions socially. △ Less

Submitted 19 August, 2013; originally announced August 2013.

Comments: 9 pages

Instruction sequence expressions for the secure hash algorithm SHA-256

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

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

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

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

ACM Class: E.3; F.1.1

Challenges in Representation Learning: A report on three machine learning contests

Authors: Ian J. Goodfellow, Dumitru Erhan, Pierre Luc Carrier, Aaron Courville, Mehdi Mirza, Ben Hamner, Will Cukierski, Yichuan Tang, David Thaler, Dong-Hyun Lee, Yingbo Zhou, Chetan Ramaiah, Fangxiang Feng, Ruifan Li, Xiaojie Wang, Dimitris Athanasakis, John Shawe-Taylor, Maxim Milakov, John Park, Radu Ionescu, Marius Popescu, Cristian Grozea, James Bergstra, **g**g Xie, Lukasz Romaszko , et al. (3 additional authors not shown)

Abstract: The ICML 2013 Workshop on Challenges in Representation Learning focused on three challenges: the black box learning challenge, the facial expression recognition challenge, and the multimodal learning challenge. We describe the datasets created for these challenges and summarize the results of the competitions. We provide suggestions for organizers of future challenges and some comments on what kin… ▽ More The ICML 2013 Workshop on Challenges in Representation Learning focused on three challenges: the black box learning challenge, the facial expression recognition challenge, and the multimodal learning challenge. We describe the datasets created for these challenges and summarize the results of the competitions. We provide suggestions for organizers of future challenges and some comments on what kind of knowledge can be gained from machine learning competitions. △ Less

Submitted 1 July, 2013; originally announced July 2013.

Comments: 8 pages, 2 figures

Decision Taking versus Promise Issuing

Authors: Jan A. Bergstra

Abstract: An alignment is developed between the terminology of outcome oriented decision taking and a terminology for promise issuing. Differences and correspondences are investigated between the concepts of decision and promise. For decision taking, two forms are distinguished: the external outcome delivering form and internalized decision taking. Internalized decision taking is brought in connection wit… ▽ More An alignment is developed between the terminology of outcome oriented decision taking and a terminology for promise issuing. Differences and correspondences are investigated between the concepts of decision and promise. For decision taking, two forms are distinguished: the external outcome delivering form and internalized decision taking. Internalized decision taking is brought in connection with Marc Slors' theory of self-programming. Examples are produced for decisions and promises in four different several settings each connected with software technology: instruction sequence effectuation, informational money transfer, budget announcement, and division by zero. △ Less

Submitted 27 June, 2013; originally announced June 2013.

Comments: 29 pages

Hyperparameter Optimization and Boosting for Classifying Facial Expressions: How good can a "Null" Model be?

Authors: James Bergstra, David D. Cox

Abstract: One of the goals of the ICML workshop on representation and learning is to establish benchmark scores for a new data set of labeled facial expressions. This paper presents the performance of a "Null" model consisting of convolutions with random weights, PCA, pooling, normalization, and a linear readout. Our approach focused on hyperparameter optimization rather than novel model components. On the… ▽ More One of the goals of the ICML workshop on representation and learning is to establish benchmark scores for a new data set of labeled facial expressions. This paper presents the performance of a "Null" model consisting of convolutions with random weights, PCA, pooling, normalization, and a linear readout. Our approach focused on hyperparameter optimization rather than novel model components. On the Facial Expression Recognition Challenge held by the Kaggle website, our hyperparameter optimization approach achieved a score of 60% accuracy on the test data. This paper also introduces a new ensemble construction variant that combines hyperparameter optimization with the construction of ensembles. This algorithm constructed an ensemble of four models that scored 65.5% accuracy. These scores rank 12th and 5th respectively among the 56 challenge participants. It is worth noting that our approach was developed prior to the release of the data set, and applied without modification; our strong competition performance suggests that the TPE hyperparameter optimization algorithm and domain expertise encoded in our Null model can generalize to new image classification data sets. △ Less

Submitted 14 June, 2013; originally announced June 2013.

Comments: Presented at the Workshop on Representation and Learning, ICML 2013

Questions related to Bitcoin and other Informational Money

Authors: Jan A. Bergstra, Karl de Leeuw

Abstract: A collection of questions about Bitcoin and its hypothetical relatives Bitguilder and Bitpenny is formulated. These questions concern technical issues about protocols, security issues, issues about the formalizations of informational monies in various contexts, and issues about forms of use and misuse. Some questions are formulated in the more general setting of informational monies and near-monie… ▽ More A collection of questions about Bitcoin and its hypothetical relatives Bitguilder and Bitpenny is formulated. These questions concern technical issues about protocols, security issues, issues about the formalizations of informational monies in various contexts, and issues about forms of use and misuse. Some questions are formulated in the more general setting of informational monies and near-monies. We also formulate questions about legal, psychological, and ethical aspects of informational money. Finally we formulate a number of questions concerning the economical merits of and outlooks for Bitcoin. △ Less

Submitted 26 December, 2013; v1 submitted 25 May, 2013; originally announced May 2013.

Comments: 31 pages. In v2 the section on patterns for use and misuse has been improved and expanded with so-called contaminations. Other small improvements were made and 13 additional references have been included

Bitcoin and Beyond: Exclusively Informational Monies

Authors: Jan A. Bergstra, Karl de Leeuw

Abstract: The famous new money Bitcoin is classified as a technical informational money (TIM). Besides introducing the idea of a TIM, a more extreme notion of informational money will be developed: exclusively informational money (EXIM). The informational coins (INCOs) of an EXIM can be in control of an agent but are not owned by any agent. INCOs of an EXIM cannot be stolen, but they can be lost, or throw… ▽ More The famous new money Bitcoin is classified as a technical informational money (TIM). Besides introducing the idea of a TIM, a more extreme notion of informational money will be developed: exclusively informational money (EXIM). The informational coins (INCOs) of an EXIM can be in control of an agent but are not owned by any agent. INCOs of an EXIM cannot be stolen, but they can be lost, or thrown away. The difference between an EXIM and a TIM shows up when considering a user perspective on security matters. Security for an EXIM user is discussed in substantial detail, with the remarkable conclusion that computer security (security models, access control, user names, passwords, firewalls etc.) is not always essential for an EXIM, while the application of cryptography based information security is unavoidable for the use of an EXIM. Bitcoin seems to meet the criteria of an EXIM, but the assertion that "Bitcoin is an EXIM", might also be considered problematic. As a thought experiment we will contemplate Bitguilder, a hypothetical copy of Bitcoin that qualifies as an EXIM. A business ethics assessment of Bitcoin is made which reveals a number of worries. By combining Bitguilder with a so-called technical informational near-money (TINM) a dual money system, having two units with a fluctuating rate, may be obtained. It seems that a dual money can remedy some, but not all, of the ethical worries that arise when contemplating Bitcoin after hypothetically having become a dominant form of money. The contributions that Bitcoin's designers can potentially make to the evolution of EXIMs and TIMs is analyzed in terms of the update of the portfolio of money related natural kinds that comes with Bitcoin. △ Less

Submitted 30 December, 2013; v1 submitted 17 April, 2013; originally announced April 2013.

Comments: 82 pages. Revision of v2: the Paragraph on monopresence and pseudomonopresence has been improved and extended; the paragraph on units for monies of account has been extended; several minor clarifications have been included; 8 additional references were added; improvements were made of small errors throughout the paper