A Method to Translate Order-Sorted Algebras to Many-Sorted Algebras

Liyi Li
(University of Illinois at Urbana-Champaign)
Elsa Gunter
(University of Illinois at Urbana-Champaign)

Order-sorted algebras and many sorted algebras exist in a long history with many different implementations and applications. A lot of language specifications have been defined in order-sorted algebra frameworks such as the language specifications in K (an order-sorted algebra framework). The biggest problem in a lot of the order-sorted algebra frameworks is that even if they might allow developers to write programs and language specifications easily, but they do not have a large set of tools to provide reasoning infrastructures to reason about the specifications built on the frameworks, which are very common in some many-sorted algebra framework such as Isabelle/HOL, Coq and FDR. This fact brings us the necessity to marry the worlds of order-sorted algebras and many sorted algebras. In this paper, we propose an algorithm to translate a strictly sensible order-sorted algebra to a many-sorted one in a restricted domain by requiring the order-sorted algebra to be strictly sensible. The key idea of the translation is to add an equivalence relation called core equality to the translated many-sorted algebras. By defining this relation, we reduce the complexity of translating a strictly sensible order-sorted algebra to a many-sorted one, make the translated many-sorted algebra equations only increasing by a very small amount of new equations, and keep the number of rewrite rules in the algebra in the same amount. We then prove the order-sorted algebra and its translated many-sorted algebra are bisimilar. To the best of our knowledge, our translation and bisimilar proof is the first attempt in translating and relating an order-sorted algebra with a many-sorted one in a way that keeps the size of the translated many-sorted algebra relatively small.

In Horatiu Cirstea and David Sabel: Proceedings Fourth International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2017), Oxford, UK, 8th September 2017, Electronic Proceedings in Theoretical Computer Science 265, pp. 20–34.
Published: 16th February 2018.

ArXived at: http://dx.doi.org/10.4204/EPTCS.265.3 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org