Proving semantical equivalence of data specifications Original Research Article

More than two decades ago, Peter Freyd introduced essentially algebraic specifications, a well-behaved generalization of algebraic specifications, allowing for equational partiality. These essentially algebraic specifications turn out to have a number of very interesting applications in computer science. In this paper, we present a deduction system for essentially algebraic specifications that is very suitable as the underlying deduction system of an automated theorem prover. Using the well-known fact that theories of sketches can be constructed as initial algebras of essentially algebraic specifications, we describe a semi-automatic procedure for proving the equivalence of the theories of two sketches. Next, we demonstrate that sketches are a very suitable formalism for making semantic data specifications, as used in database design and software engineering. Two such data specifications are semantically equivalent iff their model categories in FinSet are equivalent. Equivalence of theories is a sufficient condition for semantical equivalence, and hence the procedure to prove the equivalence of the theories of sketches can be used as a powerful tool to prove semantical equivalence of data specifications. Proving semantical equivalence of data specifications is an important component of the view integration process, i.e. the process of integrating a number of partly overlapping data specifications into one large data specification.