Inversive meadows and divisive meadows

被引:16
作者
Bergstra, J. A. [1 ]
Middelburg, C. A. [1 ]
机构
[1] Univ Amsterdam, Fac Sci, Inst Informat, NL-1098 XH Amsterdam, Netherlands
关键词
Inversive meadow; Divisive meadow; Arithmetical meadow; Partial meadow; Imperative meadow; Relevant division convention; ALGEBRA; LOGIC;
D O I
10.1016/j.jal.2011.03.001
中图分类号
TP18 [人工智能理论];
学科分类号
081104 ; 0812 ; 0835 ; 1405 ;
摘要
Inversive meadows are commutative rings with a multiplicative identity element and a total multiplicative inverse operation satisfying 0(-1) = 0. Divisive meadows are inversive meadows with the multiplicative inverse operation replaced by a division operation. We give finite equational specifications of the class of all inversive meadows and the class of all divisive meadows. It depends on the angle from which they are viewed whether inversive meadows or divisive meadows must be considered more basic. We show that inversive and divisive meadows of rational numbers can be obtained as initial algebras of finite equational specifications. In the spirit of Peacock's arithmetical algebra, we study variants of inversive and divisive meadows without an additive identity element and/or an additive inverse operation. We propose simple constructions of variants of inversive and divisive meadows with a partial multiplicative inverse or division operation from inversive and divisive meadows. Divisive meadows are more basic if these variants are considered as well. We give a simple account of how mathematicians deal with 1/0, in which meadows and a customary convention among mathematicians play prominent parts, and we make plausible that a convincing account, starting from the popular computer science viewpoint that 1/0 is undefined, by means of some logic of partial functions is not attainable. (C) 2011 Elsevier B.V. All rights reserved.
引用
收藏
页码:203 / 220
页数:18
相关论文
共 39 条
[1]  
[Anonymous], 1995, Journal of Applied Non-Classical Logics, DOI DOI 10.1080/11663081.1995.10510855
[2]   A LOGIC COVERING UNDEFINEDNESS IN PROGRAM PROOFS [J].
BARRINGER, H ;
CHENG, JH ;
JONES, CB .
ACTA INFORMATICA, 1984, 21 (03) :251-269
[3]  
Bergstra JA, 2008, SCI ANN COMPUT SCI, V18, P35
[4]   The rational numbers as an abstract data type [J].
Bergstra, J. A. ;
Tucker, J. V. .
JOURNAL OF THE ACM, 2007, 54 (02)
[5]   Meadows and the equational specification of division [J].
Bergstra, J. A. ;
Hirshfeld, Y. ;
Tucker, J. V. .
THEORETICAL COMPUTER SCIENCE, 2009, 410 (12-13) :1261-1271
[6]  
Bergstra J.A., 2008, ARXIV08033969V2MATHR
[7]   Equational specifications, complete term rewriting systems, and computable and semicomputable algebras [J].
Bergstra, JA ;
Tucker, JV .
JOURNAL OF THE ACM, 1995, 42 (06) :1194-1230
[8]   Program algebra for sequential code [J].
Bergstra, JA ;
Loots, ME .
JOURNAL OF LOGIC AND ALGEBRAIC PROGRAMMING, 2002, 51 (02) :125-156
[9]   MODULE ALGEBRA [J].
BERGSTRA, JA ;
HEERING, J ;
KLINT, P .
JOURNAL OF THE ACM, 1990, 37 (02) :335-372
[10]  
BERGSTRA JA, 2009, ARXIV09105564V3CSLO