DISJOINT-UNION PARTIAL ALGEBRAS

被引:6
作者
Hirsch, Robin [1 ]
McLean, Brett [1 ]
机构
[1] UCL, Dept Comp Sci, Gower St, London WC1E 6BT, England
关键词
DOMAIN;
D O I
10.23638/LMCS-13(2:10)2017
中图分类号
TP301 [理论、方法];
学科分类号
081202 ;
摘要
Disjoint union is a partial binary operation returning the union of two sets if they are disjoint and undefined otherwise. A disjoint-union partial algebra of sets is a collection of sets closed under disjoint unions, whenever they are defined. We provide a recursive first-order axiomatisation of the class of partial algebras isomorphic to a disjointunion partial algebra of sets but prove that no finite axiomatisation exists. We do the same for other signatures including one or both of disjoint union and subset complement, another partial binary operation we de fine. Domain-disjoint union is a partial binary operation on partial functions, returning the union if the arguments have disjoint domains and undefined otherwise. For each signature including one or both of domain-disjoint union and subset complement and optionally including composition, we consider the class of partial algebras isomorphic to a collection of partial functions closed under the operations. Again the classes prove to be axiomatisable, but not finitely axiomatisable, in first-order logic. We define the notion of pairwise combinability. For each of the previously considered signatures, we examine the class isomorphic to a partial algebra of sets/partial functions under an isomorphism mapping arbitrary suprema of pairwise combinable sets to the corresponding disjoint unions. We prove that for each case the class is not closed under elementary equivalence. However, when intersection is added to any of the signatures considered, the isomorphism class of the partial algebras of sets is finitely axiomatisable and in each case we give such an axiomatisation.
引用
收藏
页数:31
相关论文
共 18 条
[1]  
[Anonymous], 1854, The London, Edinburgh, and Dublin Philosophical Magazine and Journal of Science
[2]  
[Anonymous], 1979, Universal Algebra
[3]  
Berdine J, 2006, LECT NOTES COMPUT SC, V4111, P115
[4]  
BOOLE G, 1947, MATH ANAL LOGIC BEIN
[5]   Undecidability of propositional separation logic and its neighbours [J].
Brotherston, James ;
Kanovich, Max .
25TH ANNUAL IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE (LICS 2010), 2010, :130-139
[6]   Moving Fast with Software Verification [J].
Calcagno, Cristiano ;
Distefano, Dino ;
Dubreil, Jeremy ;
Gabi, Dominik ;
Hooimeijer, Pieter ;
Luca, Martino ;
O'Hearn, Peter ;
Papakonstantinou, Irene ;
Purbrick, Jim ;
Rodriguez, Dulma .
NASA FORMAL METHODS (NFM 2015), 2015, 9058 :3-11
[7]  
Chang C.C., 1990, Model Theory
[8]  
Hirsch R., 2002, STUDIES LOGIC FDN MA
[9]   The algebra of functions with antidomain and range [J].
Hirsch, Robin ;
Jackson, Marcel ;
Mikulas, Szabolcs .
JOURNAL OF PURE AND APPLIED ALGEBRA, 2016, 220 (06) :2214-2239
[10]   Agreeable semigroups [J].
Jackson, M ;
Stokes, T .
JOURNAL OF ALGEBRA, 2003, 266 (02) :393-417