No Cover Image

Journal article 321 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
Tags: Add Tag
No Tags, Be the first to tag this record!
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.
Keywords: Partial algebras, eager equality, Kleene equality, cautious equality, com-mon meadow, wheels, transrationals, fracterm calculus, flattening
College: Faculty of Science and Engineering
Issue: 3
Start Page: 1
End Page: 28