On Algebraic Specifications of Abstract Data Types

摘要

In this paper we address long standing open problems of Bergstra and Tucker about specifications of abstract data types by means of equations and conditional equations. By an abstract data type we mean the isomorphism type of an algebra. An algebra is algebraically specified if the algebra can be defined uniquely, in a certain precise sense, in terms of a finite number of conditional equations by allowing functions that are not in the original language of the algebra. We provide full solutions to Bergtsra and Tucker problems, explain basic ideas, methods, and the logical dependencies between blocks of proofs used in our solutions.