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 条
  • [31] An equational theory for trilattices
    K. Biedermann
    algebra universalis, 1999, 42 : 253 - 268
  • [32] A FINITE AXIOMATISATION OF FINITE-STATE AUTOMATA USING STRING DIAGRAMS
    Piedeleu, Robin
    Zanasi, Fabio
    LOGICAL METHODS IN COMPUTER SCIENCE, 2023, 19 (01)
  • [33] A String Diagrammatic Axiomatisation of Finite-State Automata
    Piedeleu, Robin
    Zanasi, Fabio
    FOUNDATIONS OF SOFTWARE SCIENCE AND COMPUTATION STRUCTURES, FOSSACS 2021, 2021, 12650 : 469 - 489
  • [34] The equational theory of w-terms for finite R-trivial semigroups
    Almeida, J
    Zeitoun, M
    SEMIGROUPS AND LANGUAGES, 2004, : 1 - 22
  • [35] A Sound and Complete Equational Theory for 3-Qubit Toffoli-Hadamard Circuits
    Amy, Matthew
    Ross, Neil J.
    Wesley, Scott
    ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2024, (406): : 1 - 43
  • [36] A COMPLETE EQUATIONAL AXIOMATIZATION FOR PREFIX ITERATION
    FOKKINK, W
    INFORMATION PROCESSING LETTERS, 1994, 52 (06) : 333 - 337
  • [37] The structure of finite meadows
    Bethke, Inge
    Rodenburg, Piet
    Sevenster, Arjen
    JOURNAL OF LOGICAL AND ALGEBRAIC METHODS IN PROGRAMMING, 2015, 84 (02) : 276 - 282
  • [38] Oriented equational logic programming is complete
    Lynch, C
    JOURNAL OF SYMBOLIC COMPUTATION, 1997, 23 (01) : 23 - 45
  • [39] A complete axiomatisation of branching bisimulation for probabilistic systems with an application in protocol verification
    Andova, Suzana
    Baeten, Jos C. M.
    Willemse, Tim A. C.
    CONCUR 2006 - CONCURRENCY THEORY, PROCEEDINGS, 2006, 4137 : 327 - 342
  • [40] A complete axiomatisation for the inclusion of series-parallel partial orders
    Bechet, D
    de Groote, P
    Retore, C
    REWRITING TECHNIQUES AND APPLICATIONS, 1997, 1232 : 230 - 240