Journal article 160 views 9 downloads
Partial arithmetical data types of rational numbers and their equational specification
Journal of Logical and Algebraic Methods in Programming, Volume: 128, Start page: 100797
Swansea University Author: John Tucker
PDF | Version of Record
© 2022 The Author(s). This is an open access article under the CC BY licenseDownload (478.88KB)
DOI (Published version): 10.1016/j.jlamp.2022.100797
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...
|Published in:||Journal of Logical and Algebraic Methods in Programming|
Check full text
No Tags, Be the first to tag this record!
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