Set-theoretic foundations of data-structure representation

摘要

A formal set-theoretic model for the computer representation of data is developed. The key idea of the model is the concept of the distinguished urelement. A Zermelo-Fraenkel set theory ZF is the starting point. This theory contains all the fundamental sets which are required. A new Zermelo-Fraenkel theory ZF' is then formed which is identical to ZF except that it contains an additional constant a, interpreted as a urelement.Working in ZF', new definitions for the usual constructions in mathematics (e.g. permutation, projection, join, composition) are developed for the elements in ZF. These definitions are far better suited for computer representations than are the usual definitions. In particular, the new definition of ordered n-tuple possesses a symmetry not found in the usual definition.To insure rapid and accurate computer implementation of common set-theoretic operations such as union, intersection, difference, etc., it is extremely useful to have a canonical well ordering on the set of computer-representable elements. Using an extremely large class of sets from ZF' (one which contains ZF) as the basic sets, such an ordering theory is developed. Computation of the ordering involves simple checks on trees in a top-down manner.Finally, using the framework developed, a new definition of Codd's first normal form is presented. In contrast to previous definitions, this one allows sets as well as urelements as domain elements, while being perfectly consistent with the axioms of ZF'.