TY - JOUR

T1 - A method to translate order-sorted algebras to many-sorted algebras

AU - Li, Liyi

AU - Gunter, Elsa

N1 - Funding Information:
Acknowledgments. This material is based upon work supported in part by NSF Grant 0917218. Any opinions, findings, and conclusions or recommendations expressed in this material are those of the authors and do not necessarily reflect the views of the NSF.
Publisher Copyright:
© Liyi Li and Elsa Gunter

PY - 2018/2/16

Y1 - 2018/2/16

N2 - 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 [24], Coq [6] and FDR [27]. 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.

AB - 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 [24], Coq [6] and FDR [27]. 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.

UR - http://www.scopus.com/inward/record.url?scp=85048408649&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85048408649&partnerID=8YFLogxK

U2 - 10.4204/EPTCS.265.3

DO - 10.4204/EPTCS.265.3

M3 - Conference article

AN - SCOPUS:85048408649

VL - 265

SP - 20

EP - 34

JO - Electronic Proceedings in Theoretical Computer Science, EPTCS

JF - Electronic Proceedings in Theoretical Computer Science, EPTCS

SN - 2075-2180

T2 - 4th International Workshop on Rewriting Techniques for Program Transformations and Evaluation, WPTE 2017

Y2 - 8 September 2017

ER -