×

zbMATH — the first resource for mathematics

Proving semantical equivalence of data specifications. (English) Zbl 0867.68080
The paper deals with the problem of determining whether two given data specifications are equivalent. The equivalence is defined by the equivalence of the corresponding categories of finite models. The equivalence problem is undecidable because finite satisfiability in model theory can be reduced to it. There is a stronger concept of equivalence of data specifications which is given by the equivalence of the categories of all (also infinite) models. The authors reduce the strong equivalence problem (via sketches and their theories) to a deduction problem for essentially algebraic specification. Finally, they present a deduction system for these specifications which is claimed to be very suitable for an automated theorem prover. The paper seems to be an interesting application of category theory to computer science.
Reviewer: J.Rosický (Brno)

MSC:
68Q65 Abstract data types; algebraic specification
18C10 Theories (e.g., algebraic theories), structure, and semantics
18A35 Categories admitting limits (complete categories), functors preserving limits, completions
08A55 Partial algebras
68P15 Database theory
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
18A25 Functor categories, comma categories
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Abiteboul, S.; Hull, R.; Vianu, V., Foundations of databases, (1995), Addison-Wesley Reading, MA
[2] Adámek, J.; Rosický, J., Locally presentable and accessible categories, (1994), Cambridge Univ. Press Cambridge · Zbl 0795.18007
[3] Bagchi, A.; Wells, C., Graph-based logic and sketches I: the general framework, (1994), Preprint distributed on the category theory mailing list
[4] Barr, M.; Wells, C., Toposes, triples and theories, () · Zbl 0567.18001
[5] Barr, M.; Wells, C., Category theory for computing science, () · Zbl 1253.18001
[6] Batini, C.; Lenzerini, M.; Navathe, S.B., A comparitive analysis of methodologies for database schema integration, ACM comput. surveys, 15, 323-364, (1986)
[7] Borceux, F., ()
[8] Cadish, B.; Diskin, Z., Algebraic graph-based approach to management of multibase systems, I: schema integration via sketches and equations, (), 69-79
[9] Chen, P.P., The entity-relationship model — towards a unified view of data, ACM trans. database systems, 1, 9-36, (1976)
[10] Coad, P.; Yourdon, E., Object-oriented analysis, (1990), Yourdon Press NJ
[11] Coste, M., Localisation, spectra and sheaf representation, () · Zbl 0422.18007
[12] Dershowitz, N., Orderings for term-rewriting systems, Theoret. comput. sci., 17, 279-301, (1982) · Zbl 0525.68054
[13] Diskin, Z., Formalizing graphical schemas for conceptual modeling: sketch-based logic vs. heuristic pictures, ()
[14] Freyd, P., Aspects of topoi, Bull. austral. math. soc., 7, 1-72, (1972) · Zbl 0252.18001
[15] Ganzinger, H., A completion procedure for conditional equations, J. symbol. comput., 11, 51-81, (1991) · Zbl 0724.68053
[16] Kaplan, S., Conditional rewrite rules, Theoret. comput. sci., 33, 175-193, (1984) · Zbl 0577.03013
[17] Lambek, J.; Scott, P., Introduction to higher order categorical logic, () · Zbl 0596.03002
[18] Makkai, M., Generalized sketches as a framework for completeness theorems, (1993), McGill University, Preprint · Zbl 0871.03045
[19] Makkai, M.; Reyes, G.E., First order categorical logic, () · Zbl 0830.03036
[20] McLarty, C., Left exact logic, J. pure appl. algebra, 41, 63-66, (1986) · Zbl 0628.03042
[21] Padawitz, P., Computing in Horn clause theories, () · Zbl 0646.68004
[22] Piessens, F., Semantic data specifications: an analysis based on a categorical formalization, ()
[23] Piessens, F.; Steegmans, E., Categorical data-specifications, Theory appl. categories, 1, 156-173, (1995) · Zbl 0919.18001
[24] Reichel, H., Initial computability, algebraic specifications and partial algebras, (1987), Clarendon Press Oxford · Zbl 0634.68001
[25] Spaccapietra, S.; Parent, C., Conflicts and correspondence assertions in interoperable databases, SIGMOD record, 20, 49-54, (1991)
[26] Steegmans, E.; Lewi, J.; D’Haese, M.; Dockx, J.; Jehoul, D.; Swennen, B.; Van Baelen, S.; Van Hirtum, P., Eroos reference manual, ()
[27] Van Baelen, S.; Lewi, J.; Steegmans, E.; Van Riel, H., EROOS: an entity-relationship based object-oriented specification method, (), 103-117
[28] Wells, C., A generalization of the concept of sketch, Theoret. comput. sci., 70, 159-178, (1990) · Zbl 0704.18001
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.