Abstract
Order-sorted specifications can be transformed into equivalent many-sorted ones by using injections to implement subsort relations. In this paper we improve a result of Goguen/Jouannaud/Meseguer about the relation between order-sorted and many-sorted rewriting. We then apply recent techniques in completion of many-sorted conditional equations to systems obtained from translating order-sorted conditional equations. Emphasis will be on ways to overcome some of the problems with non-sort-decreasing rules.
(Extended Abstract)
This work is partially supported by the ESPRIT-project PROSPECTRA, ref#390.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
6 References
Bachmair, L.: Proof methods for equational theories. PhD-Thesis, U. of Illinois, Urbana Champaign, 1987.
Bachmair, L., Dershowitz, N. and Hsiang, J.: Proof orderings for equational proofs. Proc. LICS 86, 346–357.
Bertling, H. and Ganzinger, H.: Completion-time optimization of rewrite-time goal solving. Report M.1.3-R-12.0, PROSPECTRA-Project, FB Informatik, U. Dortmund, 1988
Bertling, H. and Ganzinger, H.: Completion of application-restricted conditional equations. Report, FB Informatik, U. Dortmund, 1989, to appear.
Bertling, H., Ganzinger, H. and Schäfers, R.: CEC: A system for conditional equational completion. User Manual Version 1.4, PROSPECTRA-Report M.1.3-R-7.0, U. Dortmund, 1988.
Dershowitz, N., Okada, M. and Sivakumar, G.: Confluence of conditional rewrite systems. Proc. 1st Int'l Workshop on Conditional Term Rewriting, Orsay, 1987, Springer LNCS 308, 1988, 31–44.
Ganzinger, H.: A Completion procedure for conditional equations. Report 234, U. Dortmund, 1987, also in: Proc. 1st Int'l Workshop on Conditional Term Rewriting, Orsay, 1987, Springer LNCS 308, 1988, 62–83 (revised version to appear in J. Symb. Computation).
Ganzinger, H.: Completion with History-Dependent Complexities for Generated Equations. In Sannella, Tarlecki (eds.): Recent Trends in Data Type Specifications. Springer LNCS 332, 1988, 73–91.
Ganzinger, H.: Order-sorted completion: the many-sorted way (full version). Report 27, FB Informatik, Univ. Dortmund, 1988.
Goguen, J.A., Jouannaud, J.-P. and Meseguer, J.: Operational semantics for order-sorted algebra. Proc. 12th ICALP, 1985, 221–231.
Gnaedig, I., Kirchner, C. and Kirchner, H.: Equational completion in order-sorted algebra. Proc. CAAP '88, Springer LNCS 299, 1988, 165–184.
Goguen, J.A. and Meseguer, J.: Order-sorted algebra I: partial and overloaded operators, errors and inheritance. Comp. Sci. Lab, SRI International, 1987.
Goguen, J.A.: Order-sorted algebra. Semantics and theory of computation. Report No. 14, UCLA Computer Science Department, 1978.
Gogolla, M.: Partiell geordnete Sortenmengen und deren Answendung zur Fehlerbehandlung in abstrakten Datentypen. PhD Thesis, FB Informatik, U. Braunschweig, West Germany, 1986.
J. Hsiang, M. Rusinowitch: On word problems in equational theories, Int. Coll. on Automata Languages and Programming, Springer LNCS, 1987.
Jouannaud, J.P. and Waldmann, B.: Reductive conditional term rewriting systems. Proc. 3rd TC2 Working Conference on the Formal Description of Prog. Concepts, Ebberup, Denmark, Aug. 1986, North-Holland.
Kaplan, St.: Fair conditional term rewrite systems: unification, termination and confluence. Report 194, U. de Paris-Sud, Centre d'Orsay, Nov. 1984.
Kaplan, St.: A compiler for conditional term rewriting. Proc. RTA 1987, LNCS 256, 1987, 25–41.
Kaplan, St. and Remy J.-L.: Completion algorithms for conditional rewriting systems. MCC Workshop on Resolution of Equations in Algebraic Structures, Austin, May 1987.
Kirchner, C, Kirchner, H., and Meseguer, J.: Operational semantics of OBJ3. Proc. ICALP 88, Springer LNCS, 1988.
Kounalis, E. and Rusinowitch, M.: On word problems in Horn theories. Proc. 1st Int'l Workshop on Conditional Term Rewriting, Orsay, 1987, Springer LNCS 308, 1988, 144–160.
Poigné, A.: Partial algebras, subsorting, and dependent types. In Sannella, Tarlecki (eds.): Recent Trends in Data Type Specifications. Springer LNCS 332, 1988, 208–234.
Rusinowitch, M.: Theorem-proving with resolution and superposition: an extension of Knuth and Bendix procedure as a complete set of inference rules. Report 87-R-128, CRIN, Nancy, 1987.
Smolka, G., Nutt, W., Goguen, J.A. and Meseguer, J.: Order-sorted equational computation. SEKI Report SR-87-14, U. Kaiserslautern, 1987.
Winkler, F. and Buchberger, B.: A criterion for eliminating unnecessary reductions in the Knuth-Bendix algorithm. Coll. on Algebra, Combinatorics and Logic in Comp. Sci., Györ, 1983.
Zhang, H. and Remy, J.L.: Contextual rewriting. Conf. on Rewriting Techniques and Applications, Dijon 1985, Springer LNCS 202, 46–62.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1989 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ganzinger, H. (1989). Order-sorted completion: The many-sorted way. In: Díaz, J., Orejas, F. (eds) TAPSOFT '89. CAAP 1989. Lecture Notes in Computer Science, vol 351. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-50939-9_136
Download citation
DOI: https://doi.org/10.1007/3-540-50939-9_136
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-50939-4
Online ISBN: 978-3-540-46116-6
eBook Packages: Springer Book Archive