Categorical Data-Specifications

Abstract

. We introduce MD-sketches, which are a particular kind of Finite Sum sketches. Two interesting results about MD-sketches are proved. First, we show that, given two MD-sketches, it is algorithmically decidable whether their model categories are equivalent. Next we show that data-specifications, as used in database-design and software engineering, can be translated to MD-sketches. As a corollary, we obtain that equivalence of data-specifications is decidable. 1. Introduction This paper is about the correspondence between two kinds of specification mechanisms: sketches and data-specifications. Sketches were invented by Charles Ehresmann in the late sixties, for the purpose of specifying algebraic structures. Since then, they have been studied intensively. An outline of the theory of sketches, with a large number of references, can be found in [17]. It is well-known that the categories of models of sketches (in Set) are exactly the accessible categories. An accessible category is complet...