No Cover Image

Journal article 238 views 16 downloads

A Complete Finite Axiomatisation of the Equational Theory of Common Meadows

Jan A. Bergstra Orcid Logo, John Tucker Orcid Logo

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

Swansea University Author: John Tucker Orcid Logo

  • 67357.AAM.pdf

    PDF | Accepted Manuscript

    Author accepted manuscript document released under the terms of a Creative Commons CC-BY licence using the Swansea University Research Publications Policy (rights retention).

    Download (318.02KB)

Check full text

DOI (Published version): 10.1145/3689211

Abstract

We analyse abstract data types that model numerical structures with a concept of error. Specifically, we focus on arithmetic data types that contain an error value whose main purpose is to alwaysreturn a value for division. To rings and fields, we add a division operatorx/y and study a class of alge...

Full description

Published in: ACM Transactions on Computational Logic
ISSN: 1529-3785 1557-945X
Published: Association for Computing Machinery (ACM) 2025
Online Access: Check full text

URI: https://cronfa.swan.ac.uk/Record/cronfa67357
first_indexed 2024-08-10T20:38:08Z
last_indexed 2024-11-26T19:45:36Z
id cronfa67357
recordtype SURis
fullrecord <?xml version="1.0"?><rfc1807><datestamp>2024-11-26T16:38:45.8592752</datestamp><bib-version>v2</bib-version><id>67357</id><entry>2024-08-10</entry><title>A Complete Finite Axiomatisation of the Equational Theory of Common Meadows</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>2024-08-10</date><deptcode>MACS</deptcode><abstract>We analyse abstract data types that model numerical structures with a concept of error. Specifically, we focus on arithmetic data types that contain an error value whose main purpose is to alwaysreturn a value for division. To rings and fields, we add a division operatorx/y and study a class of algebras called common meadows whereinx/0 is the error value. The set of equations true in all common meadows is namedthe equational theory of common meadows. We give a finite equationalaxiomatisation of the equational theory of common meadows and provethat it is complete and that the equational theory is decidable.</abstract><type>Journal Article</type><journal>ACM Transactions on Computational Logic</journal><volume>26</volume><journalNumber>1</journalNumber><paginationStart>1</paginationStart><paginationEnd>28</paginationEnd><publisher>Association for Computing Machinery (ACM)</publisher><placeOfPublication/><isbnPrint/><isbnElectronic/><issnPrint>1529-3785</issnPrint><issnElectronic>1557-945X</issnElectronic><keywords>arithmetical data type, division by zero, error value, common meadow, fracterm, fracterm calculus, equational theory</keywords><publishedDay>31</publishedDay><publishedMonth>1</publishedMonth><publishedYear>2025</publishedYear><publishedDate>2025-01-31</publishedDate><doi>10.1145/3689211</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/><funders/><projectreference/><lastEdited>2024-11-26T16:38:45.8592752</lastEdited><Created>2024-08-10T19:24:01.2452921</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><document><filename>67357__31375__7af56e840b044a68ac35f14ee7528c3c.pdf</filename><originalFilename>67357.AAM.pdf</originalFilename><uploaded>2024-09-19T11:24:13.2867367</uploaded><type>Output</type><contentLength>325650</contentLength><contentType>application/pdf</contentType><version>Accepted Manuscript</version><cronfaStatus>true</cronfaStatus><documentNotes>Author accepted manuscript document released under the terms of a Creative Commons CC-BY licence using the Swansea University Research Publications Policy (rights retention).</documentNotes><copyrightCorrect>true</copyrightCorrect><language>eng</language><licence>https://creativecommons.org/licenses/by/4.0/deed.en</licence></document></documents><OutputDurs/></rfc1807>
spelling 2024-11-26T16:38:45.8592752 v2 67357 2024-08-10 A Complete Finite Axiomatisation of the Equational Theory of Common Meadows 431b3060563ed44cc68c7056ece2f85e 0000-0003-4689-8760 John Tucker John Tucker true false 2024-08-10 MACS We analyse abstract data types that model numerical structures with a concept of error. Specifically, we focus on arithmetic data types that contain an error value whose main purpose is to alwaysreturn a value for division. To rings and fields, we add a division operatorx/y and study a class of algebras called common meadows whereinx/0 is the error value. The set of equations true in all common meadows is namedthe equational theory of common meadows. We give a finite equationalaxiomatisation of the equational theory of common meadows and provethat it is complete and that the equational theory is decidable. Journal Article ACM Transactions on Computational Logic 26 1 1 28 Association for Computing Machinery (ACM) 1529-3785 1557-945X arithmetical data type, division by zero, error value, common meadow, fracterm, fracterm calculus, equational theory 31 1 2025 2025-01-31 10.1145/3689211 COLLEGE NANME Mathematics and Computer Science School COLLEGE CODE MACS Swansea University 2024-11-26T16:38:45.8592752 2024-08-10T19:24:01.2452921 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 67357__31375__7af56e840b044a68ac35f14ee7528c3c.pdf 67357.AAM.pdf 2024-09-19T11:24:13.2867367 Output 325650 application/pdf Accepted Manuscript true Author accepted manuscript document released under the terms of a Creative Commons CC-BY licence using the Swansea University Research Publications Policy (rights retention). true eng https://creativecommons.org/licenses/by/4.0/deed.en
title A Complete Finite Axiomatisation of the Equational Theory of Common Meadows
spellingShingle A Complete Finite Axiomatisation of the Equational Theory of Common Meadows
John Tucker
title_short A Complete Finite Axiomatisation of the Equational Theory of Common Meadows
title_full A Complete Finite Axiomatisation of the Equational Theory of Common Meadows
title_fullStr A Complete Finite Axiomatisation of the Equational Theory of Common Meadows
title_full_unstemmed A Complete Finite Axiomatisation of the Equational Theory of Common Meadows
title_sort A Complete Finite Axiomatisation of the Equational Theory of Common Meadows
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 26
container_issue 1
container_start_page 1
publishDate 2025
institution Swansea University
issn 1529-3785
1557-945X
doi_str_mv 10.1145/3689211
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
document_store_str 1
active_str 0
description We analyse abstract data types that model numerical structures with a concept of error. Specifically, we focus on arithmetic data types that contain an error value whose main purpose is to alwaysreturn a value for division. To rings and fields, we add a division operatorx/y and study a class of algebras called common meadows whereinx/0 is the error value. The set of equations true in all common meadows is namedthe equational theory of common meadows. We give a finite equationalaxiomatisation of the equational theory of common meadows and provethat it is complete and that the equational theory is decidable.
published_date 2025-01-31T08:33:29Z
_version_ 1821393718395011072
score 11.048171

Similar Items