Showing 1–20 of 20 results for author: Ponse, A

Fully Evaluated Left-Sequential Logics

Authors: Alban Ponse, Daan J. C. Staudt

Abstract: We consider a family of two-valued "fully evaluated left-sequential logics" (FELs), of which Free FEL (defined by Staudt in 2012) is most distinguishing (weakest) and immune to atomic side effects. Next is Memorising FEL, in which evaluations of subexpressions are memorised. The following stronger logic is Conditional FEL (inspired by Guzmán and Squier's Conditional logic, 1990). The strongest FEL… ▽ More We consider a family of two-valued "fully evaluated left-sequential logics" (FELs), of which Free FEL (defined by Staudt in 2012) is most distinguishing (weakest) and immune to atomic side effects. Next is Memorising FEL, in which evaluations of subexpressions are memorised. The following stronger logic is Conditional FEL (inspired by Guzmán and Squier's Conditional logic, 1990). The strongest FEL is static FEL, a sequential version of propositional logic. We use evaluation trees as a simple, intuitive semantics and provide complete axiomatisations for closed terms (left-sequential propositional expressions). For each FEL except Static FEL, we also define its three-valued version, with a constant U for "undefinedness" and again provide complete, independent aziomatisations, each one containing two additional axioms for U on top of the axiomatisations of the two-valued case. In this setting, the strongest FEL is equivalent to Bochvar's strict logic. △ Less

Submitted 21 March, 2024; originally announced March 2024.

Comments: 40 pages, 5 tables, three appendices. As mentioned, the text of Section 2 on pp.6-14, the quote on p.30 and Appendix A are taken from arXiv:1206.1936 (written by Staudt)

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

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

Non-commutative propositional logic with short-circuited biconditional and NAND

Authors: Dalia Papuc, Alban Ponse

Abstract: Short-circuit evaluation denotes the semantics of propositional connectives in which the second argument is evaluated only if the first argument does not suffice to determine the value of the expression. In programming, short-circuit evaluation is widely used, with left-sequential conjunction and disjunction as primitive connectives. We consider left-sequential, non-commutative propositional logic… ▽ More Short-circuit evaluation denotes the semantics of propositional connectives in which the second argument is evaluated only if the first argument does not suffice to determine the value of the expression. In programming, short-circuit evaluation is widely used, with left-sequential conjunction and disjunction as primitive connectives. We consider left-sequential, non-commutative propositional logic, also known as MSCL (memorising short-circuit logic), and start from a previously published, equational axiomatisation. First, we extend this logic with a left-sequential version of the biconditional connective, which allows for an elegant axiomatisation of MSCL. Next, we consider a left-sequential version of the NAND operator (the Sheffer stroke) and again give a complete, equational axiomatisation of the corresponding variant of MSCL. Finally, we consider these logical systems in a three-valued setting with a constant for `undefined', and again provide completeness results. △ Less

Submitted 17 March, 2022; originally announced March 2022.

Comments: 21 pages, 6 tables

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

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

An independent axiomatisation for free short-circuit logic

Authors: 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. Free short-circuit logic is the equational logic in which compound statements are evaluated from left to right, while atomic evaluations are not memorised throughout the evaluation, i.e., evaluati… ▽ 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. Free short-circuit logic is the equational logic in which compound statements are evaluated from left to right, while atomic evaluations are not memorised throughout the evaluation, i.e., evaluations of distinct occurrences of an atom in a compound statement may yield different truth values. We provide a simple semantics for free SCL and an independent axiomatisation. Finally, we discuss evaluation strategies, some other SCLs, and side effects. △ Less

Submitted 30 July, 2018; v1 submitted 17 July, 2017; originally announced July 2017.

Comments: 36 pages, 4 tables. Differences with v2: Section 2.1: theorem Thm.2.1.5 and further are renumbered; corrections: p.23, line -7, p.24, lines 3 and 7. arXiv admin note: substantial text overlap with arXiv:1010.3674

ACM Class: F.3.1

Journal ref: Journal of Applied Non-Classical Logics, 28(1):35-71, 2018

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

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

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

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

On Hoare-McCarthy algebras

Authors: Jan A. Bergstra, Alban Ponse

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

Submitted 22 December, 2010; originally announced December 2010.

Comments: 29 pages, 1 table

ACM Class: F.3.2

Short-circuit logic

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

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

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

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

ACM Class: F.3.2

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

Authors: Jan A. Bergstra, Alban Ponse

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

Submitted 15 September, 2009; originally announced September 2009.

Comments: 12 pages

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

An Instruction Sequence Semigroup with Involutive Anti-Automorphisms

Authors: Jan A. Bergstra, Alban Ponse

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

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

Comments: 36 pages, 1 table

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

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

Periodic Single-Pass Instruction Sequences

Authors: Jan A. Bergstra, Alban Ponse

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

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

Comments: 16 pages, 3 tables, New title

ACM Class: D.3.1; F.3.2

Proposition Algebra with Projective Limits

Authors: J. A. Bergstra, A. Ponse

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

Submitted 18 February, 2010; v1 submitted 23 July, 2008; originally announced July 2008.

Comments: 43 pages, 3 tables

ACM Class: F.3.2

Journal ref: ACM Transactions on Computational Logic, 12 (3), Article 21, 2011

Differential Meadows

Authors: Jan A. Bergstra, Alban Ponse

Abstract: A meadow is a zero totalised field (0^{-1}=0), and a cancellation meadow is a meadow without proper zero divisors. In this paper we consider differential meadows, i.e., meadows equipped with differentiation operators. We give an equational axiomatization of these operators and thus obtain a finite basis for differential cancellation meadows. Using the Zariski topology we prove the existence of a… ▽ More A meadow is a zero totalised field (0^{-1}=0), and a cancellation meadow is a meadow without proper zero divisors. In this paper we consider differential meadows, i.e., meadows equipped with differentiation operators. We give an equational axiomatization of these operators and thus obtain a finite basis for differential cancellation meadows. Using the Zariski topology we prove the existence of a differential cancellation meadow. △ Less

Submitted 21 April, 2008; originally announced April 2008.

Comments: 8 pages, 2 tables

MSC Class: AC; RA

Cancellation Meadows: a Generic Basis Theorem and Some Applications

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

Abstract: Let Q_0 denote the rational numbers expanded to a "meadow", that is, after taking its zero-totalized form (0^{-1}=0) as the preferred interpretation. In this paper we consider "cancellation meadows", i.e., meadows without proper zero divisors, such as $Q_0$ and prove a generic completeness result. We apply this result to cancellation meadows expanded with differentiation operators, the sign functi… ▽ More Let Q_0 denote the rational numbers expanded to a "meadow", that is, after taking its zero-totalized form (0^{-1}=0) as the preferred interpretation. In this paper we consider "cancellation meadows", i.e., meadows without proper zero divisors, such as $Q_0$ and prove a generic completeness result. We apply this result to cancellation meadows expanded with differentiation operators, the sign function, and with floor, ceiling and a signed variant of the square root, respectively. We give an equational axiomatization of these operators and thus obtain a finite basis for various expanded cancellation meadows. △ Less

Submitted 22 May, 2013; v1 submitted 27 March, 2008; originally announced March 2008.

Comments: 24 pages, 6 tables; Inge Bethke is added as an extra author; new title (previous title: A Generic Basis Theorem for Cancellation Meadows)

MSC Class: AC; RA

Journal ref: The Computer Journal 56(1): 3-14, 2013

Tuplix Calculus

Authors: J. A. Bergstra, A. Ponse, M. B. van der Zwaag

Abstract: We introduce a calculus for tuplices, which are expressions that generalize matrices and vectors. Tuplices have an underlying data type for quantities that are taken from a zero-totalized field. We start with the core tuplix calculus CTC for entries and tests, which are combined using conjunctive composition. We define a standard model and prove that CTC is relatively complete with respect to it… ▽ More We introduce a calculus for tuplices, which are expressions that generalize matrices and vectors. Tuplices have an underlying data type for quantities that are taken from a zero-totalized field. We start with the core tuplix calculus CTC for entries and tests, which are combined using conjunctive composition. We define a standard model and prove that CTC is relatively complete with respect to it. The core calculus is extended with operators for choice, information hiding, scalar multiplication, clearing and encapsulation. We provide two examples of applications; one on incremental financial budgeting, and one on modular financial budget design. △ Less

Submitted 20 December, 2007; originally announced December 2007.

Comments: 22 pages

Report number: PRG0713

Journal ref: Scientific Annals of Computer Science, 18:35--61, 2008

Interface groups and financial transfer architectures

Authors: Jan A. Bergstra, Alban Ponse

Abstract: Analytic execution architectures have been proposed by the same authors as a means to conceptualize the cooperation between heterogeneous collectives of components such as programs, threads, states and services. Interface groups have been proposed as a means to formalize interface information concerning analytic execution architectures. These concepts are adapted to organization architectures wi… ▽ More Analytic execution architectures have been proposed by the same authors as a means to conceptualize the cooperation between heterogeneous collectives of components such as programs, threads, states and services. Interface groups have been proposed as a means to formalize interface information concerning analytic execution architectures. These concepts are adapted to organization architectures with a focus on financial transfers. Interface groups (and monoids) now provide a technique to combine interface elements into interfaces with the flexibility to distinguish between directions of flow dependent on entity naming. The main principle exploiting interface groups is that when composing a closed system of a collection of interacting components, the sum of their interfaces must vanish in the interface group modulo reflection. This certainly matters for financial transfer interfaces. As an example of this, we specify an interface group and within it some specific interfaces concerning the financial transfer architecture for a part of our local academic organization. Financial transfer interface groups arise as a special case of more general service architecture interfaces. △ Less

Submitted 11 July, 2007; originally announced July 2007.

Comments: 22 pages

Report number: PRG0702 ACM Class: D.2.2

Projection semantics for rigid loops

Authors: Jan A. Bergstra, Alban Ponse

Abstract: A rigid loop is a for-loop with a counter not accessible to the loop body or any other part of a program. Special instructions for rigid loops are introduced on top of the syntax of the program algebra PGA. Two different semantic projections are provided and proven equivalent. One of these is taken to have definitional status on the basis of two criteria: `normative semantic adequacy' and `indic… ▽ More A rigid loop is a for-loop with a counter not accessible to the loop body or any other part of a program. Special instructions for rigid loops are introduced on top of the syntax of the program algebra PGA. Two different semantic projections are provided and proven equivalent. One of these is taken to have definitional status on the basis of two criteria: `normative semantic adequacy' and `indicative algorithmic adequacy'. △ Less

Submitted 6 July, 2007; originally announced July 2007.

Comments: 20 pages

Report number: PRG0604 ACM Class: D.2.4; D.3.1; F.3.2