Abstract
In an algebraic framework, where equational, membership and existence formulas can be expressed, decorated terms and rewriting provide operational semantics and decision procedures for these formulas. We focus in this work on testing sort inheritance, an undecidable property of specifications, needed for unification in this context. A test and three specific processes, based on completion of a set of rewrite rules, are proposed to check sort inheritance. They depend on the kinds of membership formulas (t∶A) allowed in the specifications: flat and linear, shallow and general terms t are studied.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
H. Chen and J. Hsiang. Order-sorted equational specification and completion. Technical report, State University of New York at Stony Brook, November 1991.
H. Comon. Completion of rewrite systems with membership constraints. In W. Kuich, editor, Proceedings of ICALP 92, volume 623 of Lecture Notes in Computer Science. Springer-Verlag, 1992.
N. Dershowitz and J.-P. Jouannaud. Rewrite Systems. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, chapter 6, pages 244–320. Elsevier Science Publishers B. V. (North-Holland), 1990.
J. A. Goguen, J.-P. Jouannaud, and J. Meseguer. Operational semantics for order-sorted algebra. In W. Brauer, editor, Proceeding of the 12th International Colloquium on Automata, Languages and Programming, Nafplion (Greece), volume 194 of Lecture Notes in Computer Science, pages 221–231. Springer-Verlag, 1985.
I. Gnaedig, C. Kirchner, and H. Kirchner. Equational completion in order-sorted algebras. Theoretical Computer Science, 72:169–202, 1990.
J. A. Goguen and J. Meseguer. Order-sorted algebra I: equational deduction for multiple inheritance, overloading, exceptions and partial operations. Theoretical Computer Science, 2(105):217–273, 1992.
C. Hintermeier, C. Kirchner, and H. Kirchner. Dynamically-typed computations for order-sorted equational presentations-extended abstract-. In S. Abiteboul and E. Shamir, editors, Proc. 21st International Colloquium on Automata, Languages, and Programming, volume 820 of Lecture Notes in Computer Science, pages 450–461. Springer-Verlag, 1994.
C. Hintermeier, C. Kirchner, and H. Kirchner. Dynamically-typed computations for order-sorted equational presentations. research report 2208, INRIA, Inria Lorraine, March 1994. 114 p., also as CRIN report 93-R-309.
C. Hintermeier, H. Kirchner, and P. Mosses. R n-and G n-logics. Technical report, Centre de Recherche en Informatique de Nancy, 1994.
J.-P. Jouannaud and C. Kirchner. Solving equations in abstract algebras: a rule-based survey of unification. In J.-L. Lassez and G. Plotkin, editors, Computational Logic. Essays in honor of Alan Robinson, chapter 8, pages 257–321. The MIT press, Cambridge (MA, USA), 1991.
A. Mégrelis. Algèbre galactique — Un procédé de calcul formel, relatif aux semi-fonctions, à l'inclusion et à l'égalité. Thèse de Doctorat d'Université, Université de Nancy 1, 1990.
K. Meinke. Algebraic semantics of rewriting terms and types. In M. Rusinowitch and J. Rémy, editors, Proceedings 3rd International Workshop on Conditional Term Rewriting Systems, Pont-à-Mousson (France), volume 656 of Lecture Notes in Computer Science, pages 1–20. Springer-Verlag, 1992.
P. D. Mosses. Unified algebras and institutions. In Proceedings 4th IEEE Symposium on Logic in Computer Science, Pacific Grove, pages 304–312, 1989.
A. Oberschelp. Untersuchungen zur mehrsortigen Quantorenlogik. Math. Annalen, 145(1):297–333, 1962.
D. Scott. Identity and existence in intuitionistic logic. In M. P. Fourman and C. J. Mulvey, editors, Applications of Sheaves, volume 753 of Lecture Notes in Mathematics, pages 660–696. Springer-Verlag, 1977.
G. Smolka. Logic Programming over Polymorphically Order-Sorted Types. PhD thesis, FB Informatik, Universität Kaiserslautern, Germany, 1989.
G. Smolka, W. Nutt, J. A. Goguen, and J. Meseguer. Order-sorted equational computation. In H. Aït-Kaci and M. Nivat, editors, Resolution of Equations in Algebraic Structures, Volume 2: Rewriting Techniques, pages 297–367. Academic Press, 1989.
M. Schmidt-Schauß. Computational Aspects of an Order-Sorted Logic with Term Declarations. PhD thesis, Universität Kaiserslautern (Germany), 1987.
U. Waldmann. Semantics of order-sorted specifications. Theoretical Computer Science, 94(1):1–33, 1992.
P. Watson and J. Dick. Least sorts in order-sorted term rewriting. Technical report, Royal Holloway and Bedford New College, University of London, 1989.
A. Werner. A semantic approach to order-sorted rewriting. In C. Kirchner, editor, Proceedings 5th Conference on Rewriting Techniques and Applications, Montreal (Canada), volume 690 of Lecture Notes in Computer Science, pages 47–61. Springer-Verlag, 1993.
L. With. Completeness and confluence of order-sorted term rewriting. In M. Rusinowitch and J.-L. Rémy, editors, Proceedings 3rd International Workshop on Conditional Term Rewriting Systems, Pont-à-Mousson (France), number 656 in Lecture Notes in Computer Science, pages 393–407. Springer-Verlag, July 1992.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1995 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Hintermeier, C., Kirchner, C., Kirchner, H. (1995). Sort inheritance for order-sorted equational presentations. In: Astesiano, E., Reggio, G., Tarlecki, A. (eds) Recent Trends in Data Type Specification. ADT COMPASS 1994 1994. Lecture Notes in Computer Science, vol 906. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0014436
Download citation
DOI: https://doi.org/10.1007/BFb0014436
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-59132-0
Online ISBN: 978-3-540-49198-9
eBook Packages: Springer Book Archive