Search

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.

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.

Both two-valued and three-valued conditional logic (CL), defined by Guzm\'an 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., Comment: 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

Sumterms are introduced as syntactic entities, and sumtuples are introduced as semantic entities. Equipped with these concepts a new description is obtained of the notion of a sum as (the name for) a role which can be played by a number. Sumterm splitting operators are introduced and it is argued that without further precautions the presence of these operators gives rise to instance of the so-called sum splitting paradox. A survey of solutions to the sum splitting paradox is given.

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., Comment: Sequel to arXiv:2001.01543 [cs.OH]

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

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., Comment: 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

Univariate fractions can be transformed to mixed fractions in the equational theory of meadows of characteristic zero., Comment: 12 pages

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., Comment: Based on reviewer's comments many minor improvements have been made

An equational axiomatisation of probability functions for one-dimensional event spaces in the language of signed meadows is expanded with conditional values. Conditional values constitute a so-called signed vector meadow. In the presence of a probability function, equational axioms are provided for expected value, variance, covariance, and correlation squared, each defined for conditional values. Finite support summation is introduced as a binding operator on meadows which simplifies formulating requirements on probability mass functions with finite support. Conditional values are related to probability mass functions and to random variables. The definitions are reconsidered in a finite dimensional setting., Comment: The notation has been somewhat simplified with reference to the notions of assimilation and dis-assimilation as have been put forward by Nicaud et. al. in 2001. Some typographical improvements were performed. An open problem statement has been removed

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., Comment: arXiv admin note: text overlap with arXiv:1406.3280

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., Comment: 11 pages

Fracterms are introduced as a proxy for fractions. A precise definition of fracterms is formulated and on that basis reasonably precise definitions of various classes of fracterms are given. In the context of the meadow of rational numbers viewing fractions as fracterms provides an adequate theory of fractions. A very different view on fractions is that fractions are values, i.e. rational numbers. Fracterms are used to provide a range of intermediate definitions between these two definitions of fractions, Comment: The paper has been completely rewritten. Now 48 pages, additional references from educational literature are included. The title has been adapted in order to highlight the central position of fracterms, of which the definition of fractions is now considered an application

$\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$., Comment: 5 pages, 2 tables

Poly-infix operators and operator families are introduced as an alternative for working modulo associativity and the corresponding bracket deletion convention. Poly-infix operators represent the basic intuition of repetitively connecting an ordered sequence of entities with the same connecting primitive., Comment: 8 pages

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., Comment: 34 pages, 1 table; main differences with v2: some proofs are corrected and/or simplified in S.3-6

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., Comment: 25 pages

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.

In the well-known construction of the field of fractions of an integral domain, division by zero is excluded. We introduce "fracpairs" as pairs subject to laws consistent with the use of the pair as a fraction, but do not exclude denominators to be zero. We investigate fracpairs over a reduced commutative ring (a commutative ring that has no nonzero nilpotent elements) and provide these with natural definitions for addition, multiplication, and additive and multiplicative inverse. We find that modulo a simple congruence these fracpairs constitute a "common meadow", which is a commutative monoid both for addition and multiplication, extended with a weak additive inverse, a multiplicative inverse except for zero, and an additional element "a" that is the image of the multiplicative inverse on zero and that propagates through all operations. Considering "a" as an error-value supports the intuition. The equivalence classes of fracpairs thus obtained are called common cancellation fractions (cc-fractions), and cc-fractions over the integers constitute a homomorphic pre-image of the common meadow Qa, the field Q of rational numbers expanded with an a-totalized inverse. Moreover, the initial common meadow is isomorphic to the initial algebra of cc-fractions over the integer numbers. Next, we define canonical term algebras for cc-fractions over the integers and some meadows that model the rational numbers expanded with a totalized inverse, and provide some negative results concerning their associated term rewriting properties. Then we consider reduced commutative rings in which the sum of two squares plus one cannot be a zero divisor: by extending the equivalence relation on fracpairs we obtain an initial algebra that is isomorphic to Qa. Finally, we express negative conjectures concerning alternative specifications for these (concrete) datatypes., Comment: 25 pages, 8 tables

We apply a paraconsistent logic to reason about fractions., Comment: 6 pages

Common meadows are fields expanded with a total inverse function. Division by zero produces an additional value denoted with "a" that propagates through all operations of the meadow signature (this additional value can be interpreted as an error element). We provide a basis theorem for so-called common cancellation meadows of characteristic zero, that is, common meadows of characteristic zero that admit a certain cancellation law., Comment: 17 pages, 4 tables; differences with v3: axiom (14) of Mda (Table 2) has been replaced by the stronger axiom (12), this appears to be necessary for the proof of Theorem 3.2.1

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., Comment: 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

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).

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., Comment: 55 pages

We consider the signatures $\Sigma_m=(0,1,-,+, \cdot, \ ^{-1})$ of meadows and $(\Sigma_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., Comment: 24 pages, 14 tables, revised, new Theorem 3.7

The Kolmogorov axioms for probability functions are placed in the context of signed meadows. A completeness theorem is stated and proven for the resulting equational theory of probability calculus. Elementary definitions of probability theory are restated in this framework., Comment: 20 pages, 6 tables, some minor errors are corrected

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., Comment: 29 pages

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., Comment: 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

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., Comment: 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

Motivated by an intention to remedy current complications with Dutch terminology concerning informatics, the term informaticology is positioned to denote an academic counterpart of informatics where informatics is conceived of as a container for a coherent family of practical disciplines ranging from computer engineering and software engineering to network technology, data center management, information technology, and information management in a broad sense. Informaticology escapes from the limitations of instrumental objectives and the perspective of usage that both restrict the scope of informatics. That is achieved by including fiction science in informaticology and by ranking fiction science on equal terms with computer science and data science, and framing (the study of) game design, evelopment, assessment and distribution, ranging from serious gaming to entertainment gaming, as a chapter of fiction science. A suggestion for the scope of fiction science is specified in some detail. In order to illustrate the coherence of informaticology thus conceived, a potential application of fiction to the ontology of instruction sequences and to software quality assessment is sketched, thereby highlighting a possible role of fiction (science) within informaticology but outside gaming.

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

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

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

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

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

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

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

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

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

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

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

Formalist positions towards money are considered from a perspective of formal methods in computing. The Formaleuro (FEUR) as a dimension for monetary quantities is proposed as well as the Formalbitcoin (FBTC) which represents an item ready for circulation in a model of informational money. An attempt is made to understand the concept of money from scratch. In order to provide a definition of money the need is felt to make use of a tailored theory of definition. To that end a theory of imaginative definitions is presented and its implications for definitions of money are sketched. It is argued that a theory of money may be dependent on the role of its holder. A survey of some roles is given, with the so-called subordinate administrative role (SAR) in a central position. The concepts of virtual memory and virtual machine are taken as the point of departure for a definition of the notion of virtual money. It is argued that from the perspective of a component (division) of a large organization (ORG) its local financial system (LFS) provides a virtual money vm(LFS, ORG) which may well fail to meet the most common general and acknowledged moneyness criteria. Inverse moneyness preference is coined as phrase to assert the tendency of top-management of ORG to make its virtual money deviate from these criteria., Comment: 98 pages. Revision of arXiv.org/abs/1008.0616v1. The revision involves bringing the paper up to date with the appearance of Bitcoin, a significant update of the section on Islamic finance and interest prohibition, deletion of fragments of minor importance, an update of references, moving the ad hoc theory of definitions to an appendix, and a small change of the title

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