A decision procedure for semantical equivalence of thin FM specifications (Q1818643)

The paper starts with the observation that mathematical structures manipulated by computer programs can often be subdivided in a finite, variable part and a possibly infinite fixed part, where the elements of the variable part are labelled (again in a variable way) by elements of the fixed part. Such structures have been called metafinite structures. An example is a relational database, which consists of a finite set of finite relations over a number of (possibly) infinite domains. Hence, the tables containing the tuples of the relations are the finite variable part, and the domains are the infinite fixed part. Even though at any given moment of time only a finite part of these possibly infinite domains is actually present in the database, the authors argue that it is convenient to consider them in their entirety when reasoning about the database. In the sketch-based approach to semantic data specifications a clear separation is made between the entities (the finite part) and the attributes (the infinite part), and the approach extends very naturally to specifying metafinite structures. The idea is to use, for the finite part, finitary sketches as the specification logic, and for the infinite part to consider products of unstructured sets. Elements of the finite part are then labelled with tuples of elements from unstructured sets. A number of undecidability results concerning finite finitary sketches are proven to show that the semantical equivalence problem of specifications is, in general, undecidable. The main result of the paper regards the class of thin FM specifications. For this class of specifications the semantical equivalence is shown to be decidable.