No Cover Image

Journal article 456 views

Eager Equality for Rational Number Arithmetic

Jan A. Bergstra Orcid Logo, John Tucker Orcid Logo

ACM Transactions on Computational Logic, Volume: 24, Issue: 3, Pages: 1 - 28

Swansea University Author: John Tucker Orcid Logo

Full text not available from this repository: check for access using links below.

Check full text

DOI (Published version): 10.1145/3580365

Abstract

Eager equality for algebraic expressions over partial algebras distinguishes or separates terms only if both have defined values and they are different. We consider arithmetical algebras with division as a partial oper- ator, called meadows, and focus on algebras of rational numbers. To study eager...

Full description

Published in: ACM Transactions on Computational Logic
ISSN: 1529-3785 1557-945X
Published: New York, NY, United States Association for Computing Machinery (ACM) 2023
Online Access: Check full text

URI: https://cronfa.swan.ac.uk/Record/cronfa63639
first_indexed 2023-06-13T14:35:26Z
last_indexed 2024-11-15T18:02:00Z
id cronfa63639
recordtype SURis
fullrecord <?xml version="1.0"?><rfc1807><datestamp>2024-07-11T14:58:04.8259132</datestamp><bib-version>v2</bib-version><id>63639</id><entry>2023-06-13</entry><title>Eager Equality for Rational Number Arithmetic</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>2023-06-13</date><deptcode>MACS</deptcode><abstract>Eager equality for algebraic expressions over partial algebras distinguishes or separates terms only if both have defined values and they are different. We consider arithmetical algebras with division as a partial oper- ator, called meadows, and focus on algebras of rational numbers. To study eager equality, we use common meadows, which are totalisations of partial meadows by means of absorptive elements. An axiomatisation of common meadows is the basis of an axiomatisation of eager equality as a predicate on a common meadow. Applied to the rational numbers, we prove completeness and decidability of the equational theory of eager equality. To situate eager equality theoretically, we consider two other partial equalities of increasing strict- ness: Kleene equality, which is equivalent to the native equality of common meadows, and one we call cautious equality. Our methods of analysis for eager equality are quite general, and so we apply them to these two other partial equalities; and, in addition to common meadows, we use three other kinds of algebra designed to totalise division. In summary, we are able to compare 13 forms of equality for the partial meadow of rational numbers. We focus on the decidability of the equational theories of these equalities. We show that for the four total algebras, eager and cautious equality are decidable. We also show that for others the Diophantine Prob- lem over the rationals is one-one computably reducible to their equational theories. The Diophantine Problem for rationals is a longstanding open problem. Thus, eager equality has substantially less complex semantics.</abstract><type>Journal Article</type><journal>ACM Transactions on Computational Logic</journal><volume>24</volume><journalNumber>3</journalNumber><paginationStart>1</paginationStart><paginationEnd>28</paginationEnd><publisher>Association for Computing Machinery (ACM)</publisher><placeOfPublication>New York, NY, United States</placeOfPublication><isbnPrint/><isbnElectronic/><issnPrint>1529-3785</issnPrint><issnElectronic>1557-945X</issnElectronic><keywords>Partial algebras, eager equality, Kleene equality, cautious equality, com-mon meadow, wheels, transrationals, fracterm calculus, flattening</keywords><publishedDay>7</publishedDay><publishedMonth>4</publishedMonth><publishedYear>2023</publishedYear><publishedDate>2023-04-07</publishedDate><doi>10.1145/3580365</doi><url>http://dx.doi.org/10.1145/3580365</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/><funders/><projectreference/><lastEdited>2024-07-11T14:58:04.8259132</lastEdited><Created>2023-06-13T15:23:05.6279025</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><orcid>0000-0003-2492-506x</orcid><order>1</order></author><author><firstname>John</firstname><surname>Tucker</surname><orcid>0000-0003-4689-8760</orcid><order>2</order></author></authors><documents/><OutputDurs/></rfc1807>
spelling 2024-07-11T14:58:04.8259132 v2 63639 2023-06-13 Eager Equality for Rational Number Arithmetic 431b3060563ed44cc68c7056ece2f85e 0000-0003-4689-8760 John Tucker John Tucker true false 2023-06-13 MACS Eager equality for algebraic expressions over partial algebras distinguishes or separates terms only if both have defined values and they are different. We consider arithmetical algebras with division as a partial oper- ator, called meadows, and focus on algebras of rational numbers. To study eager equality, we use common meadows, which are totalisations of partial meadows by means of absorptive elements. An axiomatisation of common meadows is the basis of an axiomatisation of eager equality as a predicate on a common meadow. Applied to the rational numbers, we prove completeness and decidability of the equational theory of eager equality. To situate eager equality theoretically, we consider two other partial equalities of increasing strict- ness: Kleene equality, which is equivalent to the native equality of common meadows, and one we call cautious equality. Our methods of analysis for eager equality are quite general, and so we apply them to these two other partial equalities; and, in addition to common meadows, we use three other kinds of algebra designed to totalise division. In summary, we are able to compare 13 forms of equality for the partial meadow of rational numbers. We focus on the decidability of the equational theories of these equalities. We show that for the four total algebras, eager and cautious equality are decidable. We also show that for others the Diophantine Prob- lem over the rationals is one-one computably reducible to their equational theories. The Diophantine Problem for rationals is a longstanding open problem. Thus, eager equality has substantially less complex semantics. Journal Article ACM Transactions on Computational Logic 24 3 1 28 Association for Computing Machinery (ACM) New York, NY, United States 1529-3785 1557-945X Partial algebras, eager equality, Kleene equality, cautious equality, com-mon meadow, wheels, transrationals, fracterm calculus, flattening 7 4 2023 2023-04-07 10.1145/3580365 http://dx.doi.org/10.1145/3580365 COLLEGE NANME Mathematics and Computer Science School COLLEGE CODE MACS Swansea University 2024-07-11T14:58:04.8259132 2023-06-13T15:23:05.6279025 Faculty of Science and Engineering School of Mathematics and Computer Science - Computer Science Jan A. Bergstra 0000-0003-2492-506x 1 John Tucker 0000-0003-4689-8760 2
title Eager Equality for Rational Number Arithmetic
spellingShingle Eager Equality for Rational Number Arithmetic
John Tucker
title_short Eager Equality for Rational Number Arithmetic
title_full Eager Equality for Rational Number Arithmetic
title_fullStr Eager Equality for Rational Number Arithmetic
title_full_unstemmed Eager Equality for Rational Number Arithmetic
title_sort Eager Equality for Rational Number Arithmetic
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 ACM Transactions on Computational Logic
container_volume 24
container_issue 3
container_start_page 1
publishDate 2023
institution Swansea University
issn 1529-3785
1557-945X
doi_str_mv 10.1145/3580365
publisher Association for Computing Machinery (ACM)
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
url http://dx.doi.org/10.1145/3580365
document_store_str 0
active_str 0
description Eager equality for algebraic expressions over partial algebras distinguishes or separates terms only if both have defined values and they are different. We consider arithmetical algebras with division as a partial oper- ator, called meadows, and focus on algebras of rational numbers. To study eager equality, we use common meadows, which are totalisations of partial meadows by means of absorptive elements. An axiomatisation of common meadows is the basis of an axiomatisation of eager equality as a predicate on a common meadow. Applied to the rational numbers, we prove completeness and decidability of the equational theory of eager equality. To situate eager equality theoretically, we consider two other partial equalities of increasing strict- ness: Kleene equality, which is equivalent to the native equality of common meadows, and one we call cautious equality. Our methods of analysis for eager equality are quite general, and so we apply them to these two other partial equalities; and, in addition to common meadows, we use three other kinds of algebra designed to totalise division. In summary, we are able to compare 13 forms of equality for the partial meadow of rational numbers. We focus on the decidability of the equational theories of these equalities. We show that for the four total algebras, eager and cautious equality are decidable. We also show that for others the Diophantine Prob- lem over the rationals is one-one computably reducible to their equational theories. The Diophantine Problem for rationals is a longstanding open problem. Thus, eager equality has substantially less complex semantics.
published_date 2023-04-07T20:22:49Z
_version_ 1821347749410373632
score 11.04748

Similar Items