SET CONSTRUCTORS, FINITE SETS, AND LOGICAL SEMANTICS

The use of sets in declarative programming has been advocated by sever al authors in the literature. A representation often chosen for finite sets is that of scons, parallel to the list constructor cons. The log ical theory for such constructors is usually tacitly assumed to be som e formal system of classical set theory. However, classical set theory is formulated for a general setting, dealing with both finite and inf inite sets, and not making any assumptions about particular set constr uctors. In giving logical-consequence semantics for programs with fini te sets, it is important to know exactly what connection exists betwee n sets and set constructors. The main contribution of this paper lies in establishing these connections rigorously. We give a formal system, called SetAx, designed around the scons constructor. We distinguish b etween two kinds of set constructors, scons(x,y) and dscons(x,y), wher e both represent {x} boolean OR y, but x is an element of y is possibl e in the former, while x is not an element of y holds in the latter. B oth constructors find natural uses in specifying sets in logic program s. The design of SetAx is guided by our choice of scons as a primitive symbol of our theory rather than as a defined one, and by the need to deduce non-membership relations between terms, to enable the use of d scons. After giving the axioms SetAx, we justify it as a suitable theo ry for finite sets in logic programming by (i) showing that the set co nstructors indeed behave like finite sets; (ii) providing a framework for establishing the correctness of set unification; and (iii) definin g a Herbrand structure and providing a basis for discussing logical co nsequence semantics for logic programs with finite sets. Together, the se results provide a rigorous foundation for the set constructors in t he context of logical semantics. (C) 1999 Elsevier Science Inc. All ri ghts reserved.