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

Liyi Li, Elsa Gunter

Research output: Contribution to journalConference article

Abstract

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.

Original languageEnglish (US)
Pages (from-to)20-34
Number of pages15
JournalElectronic Proceedings in Theoretical Computer Science, EPTCS
Volume265
DOIs
StatePublished - Feb 16 2018
Event4th International Workshop on Rewriting Techniques for Program Transformations and Evaluation, WPTE 2017 - Oxford, United Kingdom
Duration: Sep 8 2017 → …

Fingerprint

Algebra
Specification languages

ASJC Scopus subject areas

  • Software

Cite this

A method to translate order-sorted algebras to many-sorted algebras. / Li, Liyi; Gunter, Elsa.

In: Electronic Proceedings in Theoretical Computer Science, EPTCS, Vol. 265, 16.02.2018, p. 20-34.

Research output: Contribution to journalConference article

@article{e92d172fa8274b08b2bf210740b69bc1,
title = "A method to translate order-sorted algebras to many-sorted algebras",
abstract = "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.",
author = "Liyi Li and Elsa Gunter",
year = "2018",
month = "2",
day = "16",
doi = "10.4204/EPTCS.265.3",
language = "English (US)",
volume = "265",
pages = "20--34",
journal = "Electronic Proceedings in Theoretical Computer Science, EPTCS",
issn = "2075-2180",
publisher = "Open Publishing Association",

}

TY - JOUR

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

AU - Li, Liyi

AU - Gunter, Elsa

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

ER -