A Complete Finite Axiomatisation of the Equational Theory of Common Meadows

被引:1
|
作者
Bergstra, Jan A. [1 ]
Tucker, John v [2 ]
机构
[1] Univ Amsterdam, Informat Inst, Amsterdam, Netherlands
[2] Swansea Univ, Dept Comp Sci, Swansea, Wales
关键词
arithmetical data type; division by zero; error value; common meadow; fracterm; fracterm calculus; equational theory; FRACTIONS;
D O I
10.1145/3689211
中图分类号
TP301 [理论、方法];
学科分类号
081202 ;
摘要
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 perpendicular to whose main purpose is to always return a value for division. To rings and fields, we add a division operator x/y and study a class of algebras called common meadows wherein x/0 = perpendicular to. The set of equations true in all common meadows is named the equational theory of common meadows. We give a finite equational axiomatisation of the equational theory of common meadows and prove that it is complete and that the equational theory is decidable.
引用
收藏
页数:28
相关论文
共 50 条
  • [21] The equational theory of the weak Bruhat order on finite symmetric groups
    Santocanale, Luigi
    Wehrung, Friedrich
    JOURNAL OF THE EUROPEAN MATHEMATICAL SOCIETY, 2018, 20 (08) : 1959 - 2003
  • [22] A complete and decidable axiomatisation for deontic interpreted systems
    Lomuscio, Alessio
    Wozna, Boena
    DEONTIC LOGIC AND ARTIFICIAL NORMATIVE SYSTEMS, PROCEEDINGS, 2006, 4048 : 238 - 254
  • [23] A Complete Axiomatisation for the Logic of Lattice Effect Algebras
    Rad, Soroush Rafiee
    Sharafi, Amir Hossein
    Smets, Sonja
    INTERNATIONAL JOURNAL OF THEORETICAL PHYSICS, 2021, 60 (02) : 696 - 709
  • [24] FINITE EQUATIONAL BASES FOR FINITE ALGEBRAS IN A CONGRUENCE-DISTRIBUTIVE EQUATIONAL CLASS
    BAKER, KA
    ADVANCES IN MATHEMATICS, 1977, 24 (03) : 207 - 243
  • [25] A Complete Axiomatisation for the Logic of Lattice Effect Algebras
    Soroush Rafiee Rad
    Amir Hossein Sharafi
    Sonja Smets
    International Journal of Theoretical Physics, 2021, 60 : 696 - 709
  • [26] A COMPLETE AXIOMATISATION FOR QUANTIFIER-FREE SEPARATION LOGIC
    Demri, Stephane
    Lozes, Etienne
    Mansutti, Alessio
    LOGICAL METHODS IN COMPUTER SCIENCE, 2021, 17 (03)
  • [27] An equational theory for transactions
    Black, AP
    Cremet, V
    Guerraoui, R
    Odersky, M
    FST TCS 2003: FOUNDATIONS OF SOFTWARE TECHNOLOGY AND THEORETICAL COMPUTER SCIENCE, 2003, 2914 : 38 - 49
  • [28] EQUATIONAL THEORY OF JUSTICE
    FOSTER, JF
    JOURNAL OF ECONOMIC ISSUES, 1991, 25 (04) : 1155 - 1160
  • [29] An equational theory for trilattices
    Biedermann, K
    ALGEBRA UNIVERSALIS, 1999, 42 (04) : 253 - 268
  • [30] THE EQUATIONAL THEORY OF POMSETS
    GISCHER, JL
    THEORETICAL COMPUTER SCIENCE, 1988, 61 (2-3) : 199 - 224