JUCS - Journal of Universal Computer Science 30(3): 289-307, doi: 10.3897/jucs.107082
Synthetic Fracterm Calculus
expand article infoJan Bergstra, John V. Tucker§
‡ University of Amsterdam, Amsterdam, Netherlands§ University of Swansea, Swansea, United Kingdom
Open Access
Abstract
Previously, in [Bergstra and Tucker 2023], we provided a systematic description of elementary arithmetic concerning addition, multiplication, subtraction and division as it is practiced. Called the naive fracterm calculus, it captured a consensus on what ideas and options were widely accepted, rejected or varied according to taste. We contrasted this state of the practical art with a plurality of its formal algebraic and logical axiomatisations, some of which were motivated by computer arithmetic. We identified a significant gap between the wide embrace of the naive fracterm calculus and the narrow precisely defined formalisations. In this paper, we introduce a new intermediate and informal axiomatisation of elementary arithmetic to bridge that gap; it is called the synthetic fracterm calculus. Compared with naive fracterm calculus, the synthetic fracterm calculus is more systematic, resolves several ambiguities and prepares for reasoning underpinned by logic; indeed, it admits direct formalisations, which the naive fracterm calculus does not. The methods of these papers may have wider application, wherever formalisations are needed to analyse and standardise practices.
Keywords
fracterm calculus, partial meadow, common meadow, abstract data type