### Partial arithmetical data types of rational numbers and their equational specification

Jan A. Bergstra, John Tucker

Journal of Logical and Algebraic Methods in Programming, Volume: 128, Start page: 100797

Swansea University Author:

• PDF | Version of Record

© 2022 The Author(s). This is an open access article under the CC BY license

DOI (Published version): 10.1016/j.jlamp.2022.100797

Abstract

Upon adding division to the operations of a field we obtain a meadow. It is conventional toview division in a field as a partial function, which complicates considerably its algebra andlogic. But partiality is one out of a plurality of possible design decisions regarding division.Upon adding a parti...

Full description

Published in: Journal of Logical and Algebraic Methods in Programming 2352-2208 Elsevier BV 2022 https://cronfa.swan.ac.uk/Record/cronfa60726 No Tags, Be the first to tag this record!
Abstract: Upon adding division to the operations of a field we obtain a meadow. It is conventional toview division in a field as a partial function, which complicates considerably its algebra andlogic. But partiality is one out of a plurality of possible design decisions regarding division.Upon adding a partial division function ÷ to a field Q of rational numbers we obtain apartial meadow Q (÷) of rational numbers that qualifies as a data type. Partial data typesbring problems for specifying and programming that have led to complicated algebraicand logical theories – unlike total data types. We discuss four different ways of providingan algebraic specification of this important arithmetical partial data type Q (÷) via thealgebraic specification of a closely related total data type. We argue that the specificationmethod that uses a common meadow of rational numbers as the total algebra is themost attractive and useful among these four options. We then analyse the problem ofequality between expressions in partial data types by examining seven notions of equalitythat arise from our methods alone. Finally, based on the laws of common meadows, wepresent an equational calculus for working with fracterms that is of general interest outsideprogramming theory. Partial data types; Rational numbers with division; Common meadows; Involutive meadows; Fracterm calculus Faculty of Science and Engineering Swansea University 100797