Journal article 372 views 48 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 license
Download (478.88KB)
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...
| Published in: | Journal of Logical and Algebraic Methods in Programming |
|---|---|
| ISSN: | 2352-2208 |
| Published: |
Elsevier BV
2022
|
| Online Access: |
Check full text
|
| URI: | https://cronfa.swan.ac.uk/Record/cronfa60726 |
| Tags: |
Add Tag
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. |
|---|---|
| Keywords: |
Partial data types; Rational numbers with division; Common meadows; Involutive meadows; Fracterm calculus |
| College: |
Faculty of Science and Engineering |
| Funders: |
Swansea University |
| Start Page: |
100797 |