{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,27]],"date-time":"2025-09-27T08:31:47Z","timestamp":1758961907176,"version":"3.41.0"},"reference-count":41,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2023,4,7]],"date-time":"2023-04-07T00:00:00Z","timestamp":1680825600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2023,7,31]]},"abstract":"<jats:p>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 operator, 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 strictness: 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 Problem 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.<\/jats:p>","DOI":"10.1145\/3580365","type":"journal-article","created":{"date-parts":[[2023,1,17]],"date-time":"2023-01-17T11:57:58Z","timestamp":1673956678000},"page":"1-28","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Eager Equality for Rational Number Arithmetic"],"prefix":"10.1145","volume":"24","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2492-506X","authenticated-orcid":false,"given":"Jan A.","family":"Bergstra","sequence":"first","affiliation":[{"name":"Informatics Institute, University of Amsterdam, Amsterdam, The Netherlands"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4689-8760","authenticated-orcid":false,"given":"John V.","family":"Tucker","sequence":"additional","affiliation":[{"name":"Department of Computer Science, Swansea University, Swansea, Wales, United Kingdom"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2023,4,7]]},"reference":[{"key":"e_1_3_2_2_2","doi-asserted-by":"publisher","DOI":"10.1007\/11812289_17"},{"key":"e_1_3_2_3_2","doi-asserted-by":"crossref","unstructured":"James A. Anderson Norbert V\u00f6lker and Andrew A. Adams. 2007. Perspecx machine VIII axioms of transreal arithmetic. In Proceedings of the SPIE Conference on Vision Geometry (SPIE\u201907) . J. Latecki D. M. Mount and A. Y. Wu (Eds.) 649902.","DOI":"10.1117\/12.698153"},{"key":"e_1_3_2_4_2","doi-asserted-by":"publisher","DOI":"10.36285\/tm.53"},{"key":"e_1_3_2_5_2","doi-asserted-by":"publisher","DOI":"10.2307\/2274574"},{"key":"e_1_3_2_6_2","doi-asserted-by":"publisher","DOI":"10.36285\/tm.v0i0.17"},{"key":"e_1_3_2_7_2","doi-asserted-by":"publisher","DOI":"10.36285\/tm.33"},{"key":"e_1_3_2_8_2","unstructured":"Jan A. Bergstra. 2021. Division by zero in logic and computing. HAL Archives Ouvertes. Retrieved from https:\/\/hal.archives-ouvertes.fr\/hal-03184956."},{"key":"e_1_3_2_9_2","doi-asserted-by":"publisher","DOI":"10.36285\/tm.19"},{"key":"e_1_3_2_10_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2008.12.015"},{"key":"e_1_3_2_11_2","doi-asserted-by":"publisher","DOI":"10.1093\/comjnl\/bxs028"},{"key":"e_1_3_2_12_2","article-title":"Transformation of fractions into simple fractions in divisive meadows","author":"Bergstra Jan A.","year":"2015","unstructured":"Jan A. Bergstra and Cornelis A. Middelburg. 2015. Transformation of fractions into simple fractions in divisive meadows. 2015. J. Appl. Logic 16 (2015), 92\u2013110. Also https:\/\/arxiv.org\/abs\/1510.06233.","journal-title":"J. Appl. Logic"},{"key":"e_1_3_2_13_2","doi-asserted-by":"crossref","unstructured":"Jan A. Bergstra and Alban Ponse. 2015. Division by zero in common meadows. In Software Services and Systems: Wirsing Festschrift Lecture Notes in Computer Science 8950 R. de Nicola and R. Hennicker (Eds.). Springer 46\u201361.","DOI":"10.1007\/978-3-319-15545-6_6"},{"key":"e_1_3_2_14_2","unstructured":"Jan A. Bergstra and Alban Ponse. 2021. Division by zero in common meadows. Retrieved from https:\/\/arXiv:1406.6878v4; modified (and stronger) version of Reference [12]."},{"key":"e_1_3_2_15_2","article-title":"Fracpairs and fractions over a reduced commutative ring","volume":"27","author":"Bergstra Jan A.","year":"2016","unstructured":"Jan A. Bergstra and Alban Ponse. 2016. Fracpairs and fractions over a reduced commutative ring. Indigationes Mathematicae 27 (2016), 727\u2013748. Also https:\/\/arxiv.org\/abs\/1411.4410.","journal-title":"Indigationes Mathematicae"},{"key":"e_1_3_2_16_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-019-00352-8"},{"key":"e_1_3_2_17_2","doi-asserted-by":"publisher","DOI":"10.1145\/1219092.1219095"},{"key":"e_1_3_2_18_2","doi-asserted-by":"publisher","DOI":"10.36285\/tm.47"},{"key":"e_1_3_2_19_2","doi-asserted-by":"crossref","unstructured":"Jan A. Bergstra and John V. Tucker. 2021. The wheel of rational numbers as an abstract data type. In Proceedings of the Conference on Recent Trends in Algebraic Development Techniques (WADT\u201920) . Lecture Notes in Computer Science 12669. M. Roggenbach (Ed.) Springer 13\u201330.","DOI":"10.1007\/978-3-030-73785-6_2"},{"key":"e_1_3_2_20_2","doi-asserted-by":"publisher","DOI":"10.1093\/comjnl\/bxac026"},{"key":"e_1_3_2_21_2","doi-asserted-by":"publisher","DOI":"10.36285\/tm.57"},{"key":"e_1_3_2_22_2","unstructured":"Jonas Betzendahl. 2020. Undefinedness and soft typing in formal mathematics. PhD Research proposal. FAU Erlangen-N\u00fcrnberg. Retrieved from https:\/\/kwarc.info\/public\/proposal_jbetzendahl.pdf."},{"key":"e_1_3_2_23_2","doi-asserted-by":"crossref","unstructured":"Jesper Carlstr\u00f6m. 2004. Wheels\u2014On division by zero. Math. Struct. Comput. Sci. 14 1 (2004) 143\u2013184.","DOI":"10.1017\/S0960129503004110"},{"key":"e_1_3_2_24_2","unstructured":"Claudio Sacerdoti Cohen and Enrico Zoli. 2007. A note on formalising undefined terms in real analysis. In Proceedings of the Conference on Proof Assistants and Types in Education (PATE\u201907) . 3\u201315. Retrieved from http:\/\/citeseerx.ist.psu.edu\/viewdoc\/download?doi=10.1.1.215.8010&rep=rep1&type=pdf."},{"key":"e_1_3_2_25_2","unstructured":"Tiago S. dos Reis Walter Gomide and James A. Anderson. 2016. Construction of the transreal numbers and algebraic transfields. IAENG Int. J. Appl. Math. 46 1 (2016) 11\u201323. Retrieved from http:\/\/www.iaeng.org\/IJAM\/issues_v46\/issue_1\/IJAM_46_1_03.pdf."},{"key":"e_1_3_2_26_2","unstructured":"James Dugundji. 1966. Topology. Allyn and Bacon."},{"key":"e_1_3_2_27_2","unstructured":"Hans-Dieter Ehrich Markus Wolf and Jacques Loeckx. 1997. Specification of Abstract Data Types. Vieweg Teubner."},{"key":"e_1_3_2_28_2","doi-asserted-by":"crossref","unstructured":"William M. Farmer. 2004. Formalizing undefinedness arising in calculus. In Proceedings of the 2nd International Joint Conference on Automated Reasoning (IJCAR\u201904) Lecture Notes in Computer Science 3097. Springer 475\u2013489.","DOI":"10.1007\/978-3-540-25984-8_35"},{"key":"e_1_3_2_29_2","unstructured":"Peter Gylys-Colwell. 2016. Hilbert\u2019s 10th problem extended to \\(\\mathbb {Q}\\) . Retrieved from https:\/\/sites.math.washington.edu\/morrow\/336_17\/2016papers\/peter."},{"key":"e_1_3_2_30_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF02945120"},{"key":"e_1_3_2_31_2","doi-asserted-by":"crossref","unstructured":"Manfred Kerber and Michael Kohlhase. 1994. A mechanization of strong Kleene logic for partial functions. In Proceedings of the 12th International Conference on Automated Deduction (CADE\u201912) Lecture Notes in Artificial Intelligence 814. Springer Berlin 371\u2013385.","DOI":"10.1007\/3-540-58156-1_26"},{"key":"e_1_3_2_32_2","unstructured":"Stephen C. Kleene. 1952. Introduction to Metamathematics. North-Holland Amsterdam."},{"key":"e_1_3_2_33_2","doi-asserted-by":"crossref","unstructured":"Yu Manin. 1977. A Course in Mathematical Logic (2nd ed.). Springer.","DOI":"10.1007\/978-1-4757-4385-2"},{"key":"e_1_3_2_34_2","doi-asserted-by":"crossref","unstructured":"Hiroakira Ono. 1983. Equational theories and universal theories of fields. J. Math. Soc. Japan 35 2 (1983) 289\u2013306.","DOI":"10.2969\/jmsj\/03520289"},{"key":"e_1_3_2_35_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45455-1_4"},{"key":"e_1_3_2_36_2","unstructured":"Bjorn Poonen. 2008. Undecidability in number theory Notices AMS 55 3 (2008) 344\u2013350."},{"key":"e_1_3_2_37_2","doi-asserted-by":"crossref","unstructured":"Anthony Robinson. 1989. Equational logic of partial functions under Kleene equality: A complete and an incomplete set of rules. J. Symbol. Logic 54 2 (1989) 354\u2013362.","DOI":"10.2307\/2274852"},{"key":"e_1_3_2_38_2","doi-asserted-by":"crossref","unstructured":"Leszek Rudak. 1983. A completeness theorem for weak equational logic. Algebra Universalis 16 (1983) 331\u2013337.","DOI":"10.1007\/BF01191787"},{"key":"e_1_3_2_39_2","unstructured":"Anton Setzer. 1997. Wheels (Draft). Retrieved from http:\/\/www.cs.swan.ac.uk\/csetzer\/articles\/wheel.pdf."},{"key":"e_1_3_2_40_2","doi-asserted-by":"crossref","unstructured":"Viggo Stoltenberg-Hansen and John V. Tucker. 1995. Effective algebras. Handbook of Logic in Computer Science. Volume IV: Semantic Modelling . Samson Abramsky Dov Gabbay and Tom Maibaum (Eds.) Oxford University Press 357\u2013526.","DOI":"10.1093\/oso\/9780198537809.003.0004"},{"key":"e_1_3_2_41_2","doi-asserted-by":"crossref","unstructured":"Viggo Stoltenberg-Hansen and John V. Tucker. 1999. Computable rings and fields in Handbook of Computability Theory . Edward Griffor (Ed.) Elsevier 363\u2013447.","DOI":"10.1016\/S0049-237X(99)80028-7"},{"key":"e_1_3_2_42_2","unstructured":"Patrick Suppes. 1957. Introduction to Logic . Van Nostrand Reinhold."}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3580365","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3580365","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:37:42Z","timestamp":1750178262000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3580365"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,4,7]]},"references-count":41,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2023,7,31]]}},"alternative-id":["10.1145\/3580365"],"URL":"https:\/\/doi.org\/10.1145\/3580365","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"type":"print","value":"1529-3785"},{"type":"electronic","value":"1557-945X"}],"subject":[],"published":{"date-parts":[[2023,4,7]]},"assertion":[{"value":"2022-01-12","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2023-01-04","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2023-04-07","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}