A second order theory of data types (Q1092657)

Many axiom systems have been proposed for specifying data types. But few guideline has been given for writing the axioms. In the present paper the data types are specified by categorical many-sorted second order theories called data logics. A data logic consists of two parts. The first part is a second order theory whose axioms have schematic forms. Some conditions are given for guaranteeing it to be categorical and therefore it specifies a set of objects with some operations. The second part specifies arbitrary number of augmenting operations and constitutes a definitional extension. Data logic reflects the viewpoint that a data type is a set of objects with an arbitrary number of operations but not a universal algebra. Thus stacks and queues are specified by one data logic. Some other data logics such as those for sets and bags of natural numbers are also given. The whole theory can be regarded as a generalization of second order arithmetic.