No Cover Image

Journal article 505 views 77 downloads

Partial arithmetical data types of rational numbers and their equational specification

Jan A. Bergstra, John Tucker Orcid Logo

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

Swansea University Author: John Tucker Orcid Logo

  • 60726_VoR.pdf

    PDF | Version of Record

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

    Download (478.88KB)

Check full text

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
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!
first_indexed 2022-08-26T10:54:07Z
last_indexed 2023-01-13T19:21:04Z
id cronfa60726
recordtype SURis
fullrecord <?xml version="1.0" encoding="utf-8"?><rfc1807 xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xmlns:xsd="http://www.w3.org/2001/XMLSchema"><bib-version>v2</bib-version><id>60726</id><entry>2022-08-04</entry><title>Partial arithmetical data types of rational numbers and their equational specification</title><swanseaauthors><author><sid>431b3060563ed44cc68c7056ece2f85e</sid><ORCID>0000-0003-4689-8760</ORCID><firstname>John</firstname><surname>Tucker</surname><name>John Tucker</name><active>true</active><ethesisStudent>false</ethesisStudent></author></swanseaauthors><date>2022-08-04</date><deptcode>MACS</deptcode><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.</abstract><type>Journal Article</type><journal>Journal of Logical and Algebraic Methods in Programming</journal><volume>128</volume><journalNumber/><paginationStart>100797</paginationStart><paginationEnd/><publisher>Elsevier BV</publisher><placeOfPublication/><isbnPrint/><isbnElectronic/><issnPrint>2352-2208</issnPrint><issnElectronic/><keywords>Partial data types; Rational numbers with division; Common meadows; Involutive meadows; Fracterm calculus</keywords><publishedDay>1</publishedDay><publishedMonth>8</publishedMonth><publishedYear>2022</publishedYear><publishedDate>2022-08-01</publishedDate><doi>10.1016/j.jlamp.2022.100797</doi><url/><notes/><college>COLLEGE NANME</college><department>Mathematics and Computer Science School</department><CollegeCode>COLLEGE CODE</CollegeCode><DepartmentCode>MACS</DepartmentCode><institution>Swansea University</institution><apcterm>SU Library paid the OA fee (TA Institutional Deal)</apcterm><funders>Swansea University</funders><projectreference/><lastEdited>2024-07-11T15:47:09.0237271</lastEdited><Created>2022-08-04T09:51:59.0012990</Created><path><level id="1">Faculty of Science and Engineering</level><level id="2">School of Mathematics and Computer Science - Computer Science</level></path><authors><author><firstname>Jan A.</firstname><surname>Bergstra</surname><order>1</order></author><author><firstname>John</firstname><surname>Tucker</surname><orcid>0000-0003-4689-8760</orcid><order>2</order></author></authors><documents><document><filename>60726__25022__43f50167cea1434589db85c298c9983a.pdf</filename><originalFilename>60726_VoR.pdf</originalFilename><uploaded>2022-08-26T11:54:48.1872997</uploaded><type>Output</type><contentLength>490371</contentLength><contentType>application/pdf</contentType><version>Version of Record</version><cronfaStatus>true</cronfaStatus><documentNotes>© 2022 The Author(s). This is an open access article under the CC BY license</documentNotes><copyrightCorrect>true</copyrightCorrect><language>eng</language><licence>http://creativecommons.org/licenses/by/4.0/</licence></document></documents><OutputDurs/></rfc1807>
spelling v2 60726 2022-08-04 Partial arithmetical data types of rational numbers and their equational specification 431b3060563ed44cc68c7056ece2f85e 0000-0003-4689-8760 John Tucker John Tucker true false 2022-08-04 MACS 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. Journal Article Journal of Logical and Algebraic Methods in Programming 128 100797 Elsevier BV 2352-2208 Partial data types; Rational numbers with division; Common meadows; Involutive meadows; Fracterm calculus 1 8 2022 2022-08-01 10.1016/j.jlamp.2022.100797 COLLEGE NANME Mathematics and Computer Science School COLLEGE CODE MACS Swansea University SU Library paid the OA fee (TA Institutional Deal) Swansea University 2024-07-11T15:47:09.0237271 2022-08-04T09:51:59.0012990 Faculty of Science and Engineering School of Mathematics and Computer Science - Computer Science Jan A. Bergstra 1 John Tucker 0000-0003-4689-8760 2 60726__25022__43f50167cea1434589db85c298c9983a.pdf 60726_VoR.pdf 2022-08-26T11:54:48.1872997 Output 490371 application/pdf Version of Record true © 2022 The Author(s). This is an open access article under the CC BY license true eng http://creativecommons.org/licenses/by/4.0/
title Partial arithmetical data types of rational numbers and their equational specification
spellingShingle Partial arithmetical data types of rational numbers and their equational specification
John Tucker
title_short Partial arithmetical data types of rational numbers and their equational specification
title_full Partial arithmetical data types of rational numbers and their equational specification
title_fullStr Partial arithmetical data types of rational numbers and their equational specification
title_full_unstemmed Partial arithmetical data types of rational numbers and their equational specification
title_sort Partial arithmetical data types of rational numbers and their equational specification
author_id_str_mv 431b3060563ed44cc68c7056ece2f85e
author_id_fullname_str_mv 431b3060563ed44cc68c7056ece2f85e_***_John Tucker
author John Tucker
author2 Jan A. Bergstra
John Tucker
format Journal article
container_title Journal of Logical and Algebraic Methods in Programming
container_volume 128
container_start_page 100797
publishDate 2022
institution Swansea University
issn 2352-2208
doi_str_mv 10.1016/j.jlamp.2022.100797
publisher Elsevier BV
college_str Faculty of Science and Engineering
hierarchytype
hierarchy_top_id facultyofscienceandengineering
hierarchy_top_title Faculty of Science and Engineering
hierarchy_parent_id facultyofscienceandengineering
hierarchy_parent_title Faculty of Science and Engineering
department_str School of Mathematics and Computer Science - Computer Science{{{_:::_}}}Faculty of Science and Engineering{{{_:::_}}}School of Mathematics and Computer Science - Computer Science
document_store_str 1
active_str 0
description 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.
published_date 2022-08-01T15:47:08Z
_version_ 1804294399564185600
score 11.035634

Similar Items