A Method to Translate Order-Sorted Algebras to
Many-Sorted Algebras
Liyi Li and Elsa Gunter
Department of Computer Science,
University of Illinois at Urbana-Champaign
{liyili2,egunter}@illinois.edu

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.

1

Motivation

Currently, order-sorted algebras are used widely in defining specifications and programs. Maude [4]
and K [25] are successful programming languages for defining order-sorted algebras. The specifications
of a lot of popular programming languages, such as Java [3], Javascript [23], PHP [10], C [9, 13] and
LLVM [15] semantics, have been defined in K. Experience shows that order-sorted algebras allow users
to define specifications easily. In the paper [23], Park et al. show how they can define the full semantics
of Javascript by using K in only three months.
On the other hand, many-sorted algebras also have wide usage. Many people define pieces of popular
programming languages such as C, Java, LLVM and Javascript in forms of many-sorted algebras. For
example, people define specifications based on many-sorted algebras in some interactive theorem provers,
such as Isabelle/HOL [24] and Coq [6], where people commonly use their many-sorted type theories
to prove properties about language specifications. The advantage of using many-sorted algebra based
frameworks is that they usually associate with a large amount of tools and applications for users to prove
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.
H. Cirstea, D. Sabel (Eds.): Fourth International Workshop on Rewriting
Techniques for Program Transformations and Evaluation (WPTE 2017)
EPTCS 265, 2018, pp. 20–34, doi:10.4204/EPTCS.265.3

c Liyi Li and Elsa Gunter
This work is licensed under the
Creative Commons Attribution License.

Liyi Li and Elsa Gunter

21

properties about the programs or language specifications they define, such as the tools set of Isabelle/HOL
[24], Coq [6] and FDR [27].
In order to connect these two worlds, especially to connect the existing programming language semantic specifications defined in the order-sorted algebra K with the traditional theorem provers such as
Isabelle/HOL and Coq, the key is to discover a way to translate an order-sorted algebra into a manysorted algebra. The reason we want to do this is to use the theorem proving engines and their existing
toolsets to develop theories about specifications defined in the order-sorted world. Please note that the
syntax of the specification that we are interested in translating from a order-sorted form to a many-sorted
form is an abstract syntax, not a concrete syntax of a language. Even though users are allowed to define
mixfix syntax in order-sorted programming languages such as K or Maude, they are still representing the
abstract syntax and not the concrete syntax of a specification because the mixfix syntax forms are just
syntactic sugars in K and Maude to write abstract syntax for a specification. For example, both K and
Maude do not allow users to create overloaded constants.
To the best of our knowledge, the most recent and relevant work on defining a translation mechanism
is that of Meseguer and Skeirik [21], who created an algorithm to translate an initial free order-sorted
algebra (algebras without equations and rules) to a many-sorted one. They only propose a naive algorithm
to translate a general and sensible order-sorted algebra (an order-sorted algebra are usually sensible) to
a many-sorted one. However, this naive algorithm deals with the most general cases, so it adds a lot
more sorts and rewrite rules than needed in more restricted cases. In some order-sorted algebras, if some
rewrite rules have many sorts and the sorts have many subsorts, it can cause their algorithm to generate
exponentially many rewrite rules. Even though the chance of this extreme situation is rare for a normal
order-sorted algebra, their algorithm squares or cubes the number of equations and rewrite rules when
they translate an order-sorted algebra to a many-sorted one, which is not desirable.
Our main goal is to marry the world of people defining language specifications using order-sorted
algebras with that of people using theorem provers to develop theories about language specifications
by using many-sorted algebras. In order to succeed, our translation of an order-sorted algebra must
be understood by the people who are using the theorem provers. Making a many-sorted algebra with
relatively the same number of rewrite rules would significantly reduce the users’ efforts to understand
the translated language specifications. That is the reason for us to present a way to translate an interesting
subset of order-sorted algebras into many-sorted algebras that increase the number of the equations by
less than a linear factor and keep the number of rewrite rules the same.
By requiring the target order-sorted algebra to be strictly sensible, the basic idea of our algorithm is
to view the subsort relation s ≤ s′ defined in an order-sorted algebra as the implicit coercion of a term in
the subsort s to a term in the supersort s′ . Then, we borrow the idea of constructors as a way of explicit
coercion from other functional programming languages, such as Standard ML [22]. We add an explicit
coercion with a constructor for each subsort relation and view these subsort relations as unary operators
in the translated many-sorted algebra. After that, we add a new equivalence relation for operators, which
we call core equality. Core equality allows users to equate two terms as long as their core parts (not
counting the generated subsort unary operator parts) are the same. By this translation process, we are able
to translate a valuable subset of order-sorted algebras into many-sorted ones. Specifically, we are able to
translate all those valuable language specifications in K mentioned above into ones in Isabelle/HOL.
It is worth noting that the reason for us to require the target order-sorted algebra to be strictly sensible
is that we want to outline a subset of order-sorted algebras that can be translated into some many-sorted
algebras easily and concisely, as well as being able to prove the bi-simulation between the order-sorted
algebras and the translated many-sorted ones in this case. Since there is a naive algorithm proposed by
Meseguer and Skeirik to translate a general and sensible order-sorted algebra to a many-sorted one, by a

22

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

little engineering work, one can always divide an order-sorted algebra into a part that is strictly sensible
and another part that is not strictly sensible but sensible, and translate the first part by using our algorithm
and the second part by using the naive algorithm. We do not specify the engineering task in this paper,
because we want to focus on the theories of discovering a subset of order-sorted algebras that can be
translated into many-sorted ones easily and concisely.

2

The Scope of the Solution

In this section, we describe the preliminaries related to the problem. The basic idea is to find a translation
function tr to translate an order-sorted algebra to a many-sorted one and preserve the meaning of the
former one in the latter one. We first define term algebras for many-sorted algebras and order sorted
algebras in Definitions 2.1 and 2.2, respectively. A term algebra is a trivial algebra that defines the terms
allowed in an algebra without variables.
Definition 2.1. A sorted signature is a tuple of (S, Φ, Σ), where S is a set of sorts, Φ is a finite set
of constructors, and Σ is the set of all operators in the system, where an operator is of the form f :
s1 × ... × sn → s, where f is a constructor defined in set Φ, s1 , ..., sn is a list of argument sorts and s is the
target sort. Sorts s1 , ..., sn and s are elements of set S. Sometimes we use Σ to refer to the signature. The
sorted ground term algebra of (S, Φ, Σ) is the set of terms TΣ equal to ∪s∈S (TΣ,s ), where the sets (TΣ,s )
are mutually defined by:
(1) For each operator a : nil → s ∈ Σ, the constructor a ∈ TΣ,s , where nil means that the argument sort
list of the operator is an empty list.
(2) For each non-zero arity operator f : w → s ∈ Σ, where w = s1 × ... × sn and n > 0, and for each
(t1 , ...tn ) ∈ TΣ,s1 × ... × TΣ,sn , the term f (t1 , ...,tn ) ∈ TΣ,s .
Definition 2.2. An order-sorted signature is a tuple (S, O, Φ, Σ), where (S, Φ, Σ) is a sorted signature
and the set O is a set of pairs of sorts, such that its reflexive and transitive closure ≤ forms a partial order.
This means that O cannot have cycles if we view the pairs of O as defining a directed graph. The poset
(S, ≤) represents the subsort relations of the system. The order-sorted ground term algebra of (S, Φ, Σ)
is the least set of terms TΣ equal to ∪s∈S (TΣ,s ), where the sets (TΣ,s ) are mutually defined by:
(1) For each operator a : nil → s ∈ Σ, the constructor a ∈ TΣ,s , where nil means that the argument sort
list of the operator is an empty list.
(2) For each non-zero arity operator f : w → s ∈ Σ, where w = s1 × ... × sn and n > 0, and for each
(t1 , ...tn ) ∈ TΣ,s1 × ... × TΣ,sn , the term f (t1 , ...,tn ) ∈ TΣ,s .
(3) If s ≤ s′ , then TΣ,s ⊆ TΣ,s′ .
In Figure 1, we show an example of an order-sorted signature: IMP, and list the sets of S, O, Φ
and Σ accordingly. Based on the signature, the order-sorted ground term algebra TΣ can be generated
by the rules in Definition 2.2. If we drop the O set, the signature becomes a sorted signature, and we
can generate the sorted ground term algebra TΣ by the rules in Definition 2.1. In our version of the IMP
language, we assume that all identifiers in a given term have been initialized. To make the IMP language
simple enough, we do not provide semantics for how to lookup the value for an identifier. Instead, we
assume that there is a guess function that will guess a value for an identifier, which happens to be the
same as the value previously defined for the identifier. Finally, we use the operator − to mean both
an integer negative sign and a negation of a boolean formula, as well as + to mean both an arithmetic
addition operator and a conjunctive boolean operator, in order to show how we deal with overloaded
operators.

Liyi Li and Elsa Gunter

23

S : {nat, int, AExp, Id, bool, BExp, Block, Stmt, Map, Pgm}
O : {nat < int, int < AExp, Id < AExp, bool < BExp, Block < Stmt}
Φ : {vv, true
true, f alse
alse, 0, s , + , − , <=
<=, {}
{}, {_}
{_}, _ = _;
_;, _ __, i f _else
_else, _, __, .Map
.Map,
guess
guess, < _, _ >
>, _[_/_]
_[_/_], _ 7→ __}
true :→ bool, f alse :→ bool, 0 :→ nat, s : nat → nat, − : int → int, − : nat → int,
Σ : {true
+ : AExp ∗ AExp → AExp, + : nat ∗ nat → AExp, + : int ∗ int → AExp, {} :→ Block,
<=
<=: AExp ∗ AExp → BExp, − : BExp → BExp, − : bool → BExp, + : bool ∗ bool → BExp,
v : nat → Id, {_} : Stmt → Block, _ = _; : Id ∗ AExp → Stmt, _ _ : Stmt ∗ Stmt → Stmt,
i f _else : BExp ∗ Block ∗ Block → Stmt, guess : Id → int,
< _, _ >
>: Map ∗ Stmt → Pgm, _, _ : Map ∗ Map → Map, .Map :→ Map, + : BExp ∗ BExp → BExp,
_[_/_] : Map ∗ int ∗ Id → Map, _ 7→ _ : Id ∗ int → Map}
Figure 1: IMP Signature
Based on the ground term algebra TΣ , we define the terms with variables as TΣ (X ). Given a term with
variables t(X ) ∈ TΣ (X ), where all variables in t(X ) are contained in X , term t ∈ TΣ is an instance of t(X )
if there exists a substitution h mapping X to TΣ such that t is the result of replacing each variable x in
t(X ) by h(x). Every variable in a term in TΣ (X ) is represented by a name. Even though we refer to TΣ
and TΣ (X ) as term algebras in both many-sorted algebras and order sorted algebras, They are sorted term
algebras in the many-sorted world and order sorted term algebras in the order sorted world. It is worth
noting that, while Σ contains sort information, TΣ and TΣ (X ) do not. A mapping function x : s maps a
variable x to a sort s representing the target sort of x. We now define a many-sorted algebra and an order
sorted-algebra in Definitions 2.3 and 2.4, respectively.
Definition 2.3. A many-sorted algebra B is defined by a tuple (S, Φ, Σ, E, R), where S is a set of sorts,
Φ is the finite set of constructors allowed in the system, Σ represents all operators in the system and
(S, Φ, Σ) is the many-sorted signature, which we refer to as Σ. The equation set E is a set of pairs of
terms in TΣ (X ). and partitions the terms of B, TΣ , into equivalence classes, denoted T(Σ,E) . The terms
allowed to construct each equation in E are in sorted term algebra TΣ (X ), while the equations are applied
on the terms in the sorted ground term algebra TΣ . We introduce the quotient structure T(Σ,E) , which we
call terms TΣ modulo equations E. For two terms t and t ′ in TΣ , if we can prove they are equal through
the equations E, we say these two terms are equivalent modulo E, which partitions TΣ into different
equivalence classes and forms T(Σ,E) . A set of rewrite rules R defines the semantics of system B. The
rule set R is a set of pairs of terms in TΣ (X ), while the rules are applied on the terms in T(Σ,E) . If a rule
r ∈ R is applied to a term t, it means that the rule r is applied on the class c ∈ T(Σ,E) where t ∈ c and t
is the representative of c. The transition c −→r c′ means that for t(X ) as the left hand side and t ′ (X ) as
the right hand side of rule r, there is a substitution h mapping X to TΣ such that t and t ′ are the result of
replacing each variable x in t(X ) and t ′ (X ) by h(x) and t ∈ c and t ′ ∈ c′ , respectively. The rule r generates
an endomorphic relation, and applications of rules are closed under applications of constructors.
Definition 2.4. An order-sorted algebra A is a tuple (S, O, Φ, Σ, E, R), where (S, Φ, Σ) is a many-sorted
signature, and O is a set of pairs of sorts, such that the reflexive and transitive closure ≤ forms a partial
order. The poset (S, ≤) represents the subsort relations of the system. We call (S, O, Φ, Σ) the signature
of the system, which we refer to as Σ. The terms allowed to construct each equation in E are in the
order-sorted term algebra TΣ (X ), while the equations are applied on the terms in the order-sorted ground
term algebra TΣ . A set of rewrite rules R defines the semantics of system B. The rule set R is a set of pairs

24

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

of terms in TΣ (X ), while the rules are applied on the terms in T(Σ,E) . The two elements of a pair in E are
required to have the same sort, while for any pair (t,t ′ ) in R, the sort of t ′ is a subsort of the sort of t. This
property is called sort decreasing. We introduce the quotient structure T(Σ,E) , which we call terms TΣ
modulo equations E. For two terms t and t ′ in TΣ , if we can prove they are equal through the equations E,
we say these two terms are equivalent modulo E, which partitions TΣ into different equivalence classes
and forms T(Σ,E) . A set of rewrite rules R defines the semantics of system B. The rule set R is a set of
pairs of terms in the order-sorted term algebra TΣ (X ), while the rules are applied on the terms in T(Σ,E) .
If a rule r ∈ R is applied to a term t, it means that the rule r is applied on the class c ∈ T(Σ,E) where t ∈ c
and t is the representative of c. The transition c −→r c′ means that for t(X ) as the left hand side and t ′ (X )
as the right hand side of rule r, there is a substitution h mapping X to TΣ such that t and t ′ are the result of
replacing each variable x in t(X ) and t ′ (X ) by h(x) and t ∈ c and t ′ ∈ c′ , respectively. The rule r generates
an endomorphic relation, and applications of rules are closed under applications of constructors.
The ≤ relation can be viewed as a directed graph where each relation is an edge. The graph may
have different connected components. For any two sorts in a connected component in an order-sorted
algebra, we require there is a unique top supersort of them.
In Figure 2, we show the equations and rules for the order-sorted algebra IMP. With the information
in Figure 1, this information constructs a well-defined order-sorted algebra. A many-sorted algebra is
similar to this one with more restrictions. For example, the left hand side and right hand side of a rule
need to be sort equivalent in a many-sorted algebra. In order to write an equation for the operator + , we
need to write three versions of equations: one for + with argument sorts AExp ∗ AExp, one for it with
argument sorts int ∗ int and one for argument sorts nat ∗ nat.
In a many-sorted algebra and order-sorted algebra, even though the terms that are used to construct
an equation or a rule is in the form of TΣ (X ), they are representatives of equivalence classes in T(Σ,E) . One
thing to keep in mind is that we are defining algebras in this paper, not transition systems. The rewrite
rules in an algebra can be applied to any subterm of a given term, not only to its top-most operator. This
idea is similar to the rewrite rules in Rewriting Logic [16]. Based on the order-sorted algebra definition,
the only input restriction of our translation function tr is that the order-sorted algebra A should be, not
just sensible, but strictly sensible. The former term is defined in Definition 2.6, while the latter is defined
in Definition 2.7. One thing about overloaded operators (two operators having the same constructor) in
an algebra is that if the two overloaded operators f and f ′ have argument sorts that have no common
supersorts, we treat them as different operators since they can be easily distinguished by combining the
constructor and the list of argument sorts.
Definition 2.5. We define two overloaded operators f and f ′ to be argument compatible, if they have
the same arities, and f has argument sorts s1 , ..., sn , and f ′ has argument sorts s′1 , ..., s′n , and si ≡≤ s′i for
i = 1, ..., n, where ≡≤ means that the two given sorts have a common supersort.
Definition 2.6. (Goguen and Meseguer [12]) An order-sorted algebra is sensible, if for any pair of argument compatible constructors f and f ′ with target sorts s and s′ , respectively, we have s ≡≤ s′ .
Definition 2.7. An order-sorted algebra is strictly sensible if:
(1) Whenever there are two argument compatible operators f and f ′ with target sorts s and s′ , respectively, then we have s = s′ . We then call the order-sorted algebra being strong sensible. It is worth noting
that a strong sensible algebra cannot have overloaded constant operators.
(2) For each operator f , there exists an operator f ′ : s1 × ... × sn → s, such that for every operator
f ′′ being argument compatible with f , f ′ is argument compatible with f ′′ , and if f ′′ has argument sorts
s′1 × ... × s′n , then s′i ≤ si for all i = 1, ..., n. We then call the order-sorted algebra being maximal argumentbounding.

Liyi Li and Elsa Gunter

25

+ A : AExp = A : AExp, s(A : nat)+
+ B : nat = A : nat+
+ s(B : nat), − − A : int = A : int,
E : {0+
+ B : AExp = B : AExp+
+ A : AExp,
A : AExp+
+ −s (B : nat) = A : nat+
+ B : nat, true + A : BExp = A; BExp,
s (A : nat)+
+ B : BExp = B : BExp+
+ A : BExp, _, __(A : Map, B : Map) = _, __(B : Map, A : Map),
A : BExp+
+ −s (A : nat), _, __(A : Map,.Map
.Map
s (A : nat) <= B : AExp = 0 <= B : AExp+
.Map) = A : Map,
−s(A : nat) <= B : AExp = 0 <= B : AExp+
+ s(A : nat),
_, __(B : Map,C : Map)) = _, __(_,
_, __(A : Map, B : Map),C : Map),
_, __(A : Map,_,
.Map
_[_/_]
_[_/_](.Map
.Map, A : int, B : Id) = B : Id 7→ A : int,
_, __(A : Id 7→ B : int,C : Map), D : int, A : Id) = _, __(A : Id 7→ D : int,C : Map),
_[_/_]
_[_/_](_,
_, __(A : Id 7→ B : int,C : Map), D : int, E : Id)
_[_/_]
_[_/_](_,
_[_/_]
{}
= _, __(A : Id 7→ B : int,_[_/_]
_[_/_](C : Map, D : int, E : Id)), _ __({}
{}, A : Stmt) = A : Stmt,
{_}
_ __({_}
{_}(A : Stmt), B : Stmt) = _ __(A : Stmt, B : Stmt) }
−0 ⇒ 0, A : AExp+
+ v (B : Id) ⇒ A : AExp+
+ guess
R : {−
guess(B : Id), −true ⇒ f alse
alse, − f alse ⇒ true
true,
A : AExp <= v (B : Id) ⇒ A : AExp <= guess
guess(B : Id), 0 <= A : nat ⇒ true
true,
0 <= −s (A : nat) ⇒ f alse
alse, v (A : Id) <= B : AExp ⇒ guess
guess(A : Id) <= B : AExp,
< _, _ > (A : Map,__ __(ii f _else
_else( f alse
alse, B : Block,C : Block), D : Stmt))
⇒ < _, _ > (A : Map,__ __(C : Block, D : Stmt)),
true
< _, _ > (A : Map,__ __(ii f _else
_else(true
true, B : Block,C : Block), D : Stmt))
<
_,
_
>
_
_
⇒
(A : Map,_ _(B : Block, D : Stmt)),
< _, _ > (A : Map,__ __(__ = _;
_;(B : Id,C : int), D : Stmt))
_[_/_]
⇒ < _, _ > (_[_/_]
_[_/_](A : Map,C : int, B : Id), D : Stmt),
+ − B : int ⇒ − (A : int+
+ B : int), f alse + A : BExp ⇒ f alse }
− A : int+
Figure 2: IMP Order-Sorted Equations and Rules

The order-sorted algebra in Figures 1 and 2 is strictly sensible, but if we change the operator + :
nat ∗ nat → AExp to be + : nat ∗ nat → nat, the algebra becomes sensible but not strictly sensible.
The second condition of the strictly sensible definition is not necessary for the translation algorithm in
this paper, but it ensures that the translated many-sorted algebra from a strictly sensible order-sorted
algebra are bisimilar. Without the condition, the translated many-sorted algebra simulates the ordersorted algebra, but there might be some behaviors in the translated many-sorted algebra that cannot
be observed in the original order-sorted algebra. The first condition is the key distinction between a
sensible order-sorted algebra and a strictly sensible order-sorted algebra. In the translation algorithm
described in this paper, we rule out the possibility for users to define overloaded operator pairs like
+ : AExp ∗ AExp → AExp and + : nat ∗ nat → nat.
The reason that we are willing to accept the strictly sensible restriction is that users only need the
limited world in defining language specifications from scratch usually. This is a real restriction that will
affect some situations, because without the restriction of strictly sensible, we can define two overloaded
+ operators + : int ∗ int → int and + : nat ∗ nat → nat, where int and nat have a subsort
relation. However, there are no such operators in the order-sorted specifications of C [9], PHP [10],
JavaScriptv[23], and Java [3] in K. In addition, the operators, such as + : int ∗ nat → int and + :
nat ∗ int → nat, are usually defined as different operators with different names by users. Even though
we are able to solve them easily by adding more rules and creating more sorts, such as what the algorithm
of Meseguer and Skeirik [21] does, we do not want to take that approach because the whole point of the

26

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

translation is to have a many-sorted algebra that is concise enough for users to use and read the translated
language specifications. Squaring or cubing the size of the rewrite rules is quite undesirable.
On the other hand, it does not mean that we cannot translate order-sorted algebras that are sensible
but not strictly sensible to many-sorted algebras. The paper by Meseguer and Skeirik [21] gives us an
naive solution to cover all interesting translation cases. By giving an order-sorted algebra, people can
divide it by collecting all operators that do not match with the strictly sensible requirements and translate
these operators by using the naive algorithm introduced by Meseguer and Skeirik, and then translate
the rest of the algebra by using our algorithm, and it will reduce the size of the translated many-sorted
algebra disregarding the set of operators that do not match with the strictly sensible requirements. We
do not research in deep in this path because this is just an engineering task which requires a little careful
design. The paper mainly focuses on coming up with a subset of the order-sorted algebras that can be
translated to many-sorted ones easily and proving their bi-simulation to the translated many-sorted ones.
Now, we can formally state the properties of the translation function tr to be: given a strictly sensible
order-sorted algebra A and a translation function tr applied on A, we have a many-sorted algebra B such
that B = tr(A), and for any rule rA in A, if term tA in A can transition to tA′ through rule rA , such that
tA −→rA tA′ , then we have tr(rA ) is a rule in B and tr(tA ) −→tr(rA ) tr(tA′ ). The output of our translation is
a many-sorted algebra: B, where the rewrite rules of A and B have the above relation.

3

Translation and Proofs

In this section, a description of the translation function tr and some theories about it are given. For a
given order-sorted algebra A with (S, O, Φ, Σ, E, R), we do not need to translate the sort set S because our
translation does not change sorts at all. We eliminate the relation O, and we have the functions trΣ , trE
and trR for translating operator definitions, equations and rewrite rules.
Translating Operators. Operators are translated in two steps, such that trΣ = trΣ# ◦ trΣ′ . The first step
trΣ′ is to find a maximal argument-bounding operator f for every operator f ′ . Since the strictly sensible
assumptions require any pair of argument compatible operators f ′ and f ′′ to have the same target sort, we
restrict the nature of the argument sorts in these overloaded operators by picking its maximal argumentbounding operator f as a representative for any argument compatible operator f ′ . We then eliminate the
operator f ′ if f is different from f ′ . Hence, if Σ′ = trΣ′ , then Σ′ has fewer operators than Σ and for every
overloaded operator set, whose elements are argument compatible, Σ′ picks exactly one representative
operator for it. If the overloaded operators are not argument compatible, then we distinguish them by
picking different constructors in the translated many-sorted algebra.
For example, in the order-sorted algebra in Figures 1 and 2, there are five different overloaded operators with + constructor, where + : AExp∗AExp → AExp, + : nat∗nat → AExp and + : int∗int → AExp
are argument compatible, while + : bool ∗ bool → BExp and + : BExp ∗ BExp → BExp are also argument compatible. These two groups of + operators are not argument compatible cross groups. When
translating these operators, we first pick + : AExp ∗ AExp → AExp and + : BExp ∗ BExp → BExp as the
representatives for the first and second group, then we change the name of the first one to +AExp and
the second one to +BExp to avoid conflicts in constructor names. Finally, in the translated many-sorted
signature, we have two translated operators for the original overloaded operators with + constructor, they
are: +AExp : AExp ∗ AExp → AExp and +BExp : BExp ∗ BExp → BExp.
The translation trΣ# translates a given Σ′ (a signature translated by trΣ′ on an order-sorted signature Σ)
by adding operators. For each pair defined in set O as (s, s′ ), which is a subsort relation s ≤ s′ , we create

Liyi Li and Elsa Gunter

27

one more unary operator Cast_s_to_s’ : s → s′ that does not appear in Σ′ . This operator has argument sort
s and target sort s′ . The result signature Σ# = trΣ# (Σ′ ) contains a set of newly generated unary operators
being bijective with the pairs in O.
For example, when translating the order-sorted algebra in Figures 1 and 2, we add the following five
unary operators: Cast_nat_to_int : nat → int, Cast_int_to_AExp : int → AExp, Cast_Id_to_AExp :
Id → AExp, Cast_bool_to_BExp : bool → BExp and Cast_Block_to_Stmt : Block → Stmt, since there
are exactly five tuples in the set O: nat < int, int < AExp, Id < AExp, bool < BExp and Block < Stmt.
Similar to the theorems in the signature translation of the paper of Meseguer and Skeirik, we also
have the following theorem about the final result Σ# . The proof of the theorem about is similar to the
one in the paper of Meseguer and Skeirik, and is a direct result of the strictly sensible requirement of an
order-sorted algebra and our translation of the operators in the algebra.
Theorem 3.1. Let Σ be an order-sorted signature, Σ# is the translated many-sorted algebra of it. All
overloaded operators (viewing +AExp and +BExp to be overloaded operators) in Σ# have at least one
argument position having distinct argument sorts that have no common supersort in the original ordersorted algebra.
Proof. The proof of the theorem about our translation is similar to the one in the paper of Meseguer and
Skeirik [21]. Here, we only sketch why it is true. The theorem is a direct result of the strictly sensible
requirement of an order-sorted algebra and our translation of the operators in the algebra. If an ordersorted algebra is strictly sensible, then two overloaded operators are argument compatible. After the
translation, only one representing operator is selected, so there cannot be two operators being argument
compatible in the original order-sorted algebra.

Translating Terms and Equations. After translating order-sorted signatures to many-sorted ones,
we generate terms for the translated many-sorted algebras as the same way to generate sorted ground term
algebras in Definition 2.1. Once we have all valid terms for the translated many-sorted algebras, we can
define a function trE to translate every equation in E to E # and also add a set of core equality equations
to E # . After the translation, the terms in the translated many-sorted algebra with the new equation set
E # form a term algebra T(Σ# ,E # ) , and T(Σ# ,E # ) also represents the union of term sets for each sort s ∈ S
as T(Σ# ,E # ,s) . In the quotient structure T(Σ# ,E # ) , the equivalence classes are partitioned by the combination
effects of equations E # and sorts S.
First, the translation trE adds equations to the equation set E to generate E # . The new equations are
related to the idea of the core of a term. In order to define the core of a term, we first define non-core
constructors as the new constructors generated during the operator translation trΣ# . The core constructors
are the constructors of the normal operators of Σ. The core part of a term is the top most t of a term
C1 (...(Cn (t))...), where C1 , ...,Cn are unary non-core constructors. We now show the definition of core
equality.
Definition 3.1. If there are two lists of unary non-core constructors C1 , ...,Cn and K1 , ..., Km , such that
t = C1 (...(Cn (x))...) and t ′ = K1 (...(Km (x))...) are well-formed, i.e., the input sort of Ci is equal to the
output sort of Ci+1 for all i = 1, ..., n − 1, ... and the input sort of K j is equal to the output sort of K j+1 for
all j = 1, ..., m − 1, ..., as well as C1 and K1 has target sort s, Cn and Km has input sort s′ , then for each pair
of directed paths from s′ to s in the graph of ≤ in the original order-sorted algebra, i.e., s′ ≤ s, if there
are two different paths from s′ to s in the graph, we have an equation C1 (...(Cn (x : s′ ))...) = K1 (...(Km (x :
s′ ))...). The congruence closure of all these equations is core equality.

28

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

Theorem 3.2. Core equality is an equivalence relation.
Proof. The proof of reflexivity and symmetricity of core equality is simple. Here, we only show the transitivity proof. By giving t =core t ′ and t ′ =core t ′′ , we have t = C1 (...(Cn (tc ))...), t ′ = K1 (...(Km (tk ))...) and
t ′′ = G1 (...(G p (tg ))...) being well formed, C1 , ...,Cn , K1 , ..., Km and G1 , ..., G p are lists of non-core unary
constructors, and C1 (...(Cn (tc ))...) =core K1 (...(Km (tk ))...) and K1 (...(Km (tk ))...) =core G1 (...(G p (tg ))...),
then tc = tk = tg under the assumption of E # , and the output sorts of C1 , K1 and G1 are the same as well
as the input sort of Cn , Km and G p are the same; hence, C1 (...(Cn (tc ))...) =core G1 (...(G p (tg ))...) and core
equality is transitive. Thus, core equality is an equivalence relation.

The reason of having core equality is that we have new generated terms due to inserting non-core
operators to generate terms in a sort by terms in the subsorts of the sort. Semantically, these new terms
are translated from the same term in the original order-sorted algebra. If we cannot equate them, it means
that after the translation, we have some terms with different meanings that originally belong to the same
term. The way to equate these terms is to put them into the same equivalence classes by using equations
defined by core equality.
For example, when translating the order-sorted algebra in Figures 1 and 2, the generated unary operators, Cast_nat_to_int : nat → int, Cast_int_to_AExp : int → AExp, Cast_Id_to_AExp : Id → AExp,
Cast_bool_to_BExp : bool → BExp and Cast_Block_to_Stmt : Block → Stmt, are non-core constructors and operators, while the original operators are core ones. To generate the set of core equality
equations for the order-sorted algebra, we have a practical way to do it; that is to examine the ≤ relation. For every two nodes in ≤, if there is more than one path from the first node to the second
one, we add equations to connect them. In the order-sorted algebra in Figures 1 and 2, if we have
one more sort real and two more subsort relations, nat < real and real < AExp, then two paths
Cast_nat_to_int
can go from nat to AExp in ≤. We add an equation Cast_int_to_AExp
Cast_int_to_AExp(Cast_nat_to_int
Cast_nat_to_int(A : nat)) =
#
Cast_nat_to_real
Cast_real_to_AExp
Cast_real_to_AExp(Cast_nat_to_real
Cast_nat_to_real(A : nat)) to E . By doing a rough counting, we can see that
the number of new equations adding into the set E # is less than |S|2 , since the number of elements in
set O is bound to |S|2 , and we add an core equality equation if and only if there is a diamond relation
in the set O: there exist different sorts D, E, A1 , ..., An , C1 , ...,Cm such that, D < A1 < ... < An < E,
D < C1 < ... < Cm < E and Ai 6= Ci for all i = 1...min(n, m).
After we have core equality, we can translate terms of two sides of an equation in E. The two
sides belong to TΣ (X ). We define a translation function trterm to translate a term in TΣ (X ) to a term in
TΣ# (X ) for every side of an equation in E. For every sub-term, having the form f (t1 , ...,ti , ...,tm ), of
a term t in TΣ (X ), if we compare the constructor f with the set of operators in the translated manysorted signature Σ# , there is a unique operator f : (s1 , ...si , ..., sm ) (the translated many-sorted signature only keeps one operator if there is a set of argument compatible operators, and if there are overloaded operators that are not argument compatible in the original order-sorted algebra, we can also
find the unique f ′ that is translated from the original f by comparing the sort of si with the sort of
ti , because overloaded operators that are not argument compatible are translated into two different operators by distinguishing them with more information in the constructors, and they must have at least
one argument position with different sorts). If the sort of a position i in the sub-term f (t1 , ...,ti , ...,tm )
is defined with sort s according to the operator signature above, but ti actually has target sort s′ and
s′ ≤ s, then we find a list of non-core unary constructors C1 , ...,Cn to cast the sub-term to sort s as
f (t1 , ...,C1 (...(Cn (ti ))...), ...,tm ) in a well-formed way. If s′ = s, then we do not need to find the constructors. We know that such a sequence of unary constructors must exist because the set of non-core

Liyi Li and Elsa Gunter

29

unary constructors is bijective with the pairs in O, and ≤ is the reflexive and transitive closure of O.
If s′ ≤ s, there is a list of pairs in O as (s′ , s1 ), ..., (sn−1 , s). Through the list, s′ reaches s. For each
pair in the list, we have generated a unary constructor. Hence, the sequence of constructors C1 , ...,Cn is
exactly the constructors generated for pairs (s′ , s1 ), ..., (sn−1 , s). For example, when translating the order+ s(B : nat) is translated
sorted algebra in Figures 1 and 2, the equation s(A : nat) + B : nat = A : nat+
Cast_nat_to_int
Cast_nat_to_int
to Cast_int_to_AExp
Cast_int_to_AExp(Cast_nat_to_int
Cast_nat_to_int(ss(A : nat))) + Cast_int_to_AExp (Cast_nat_to_int
Cast_nat_to_int(B : nat))
Cast_nat_to_int
+ Cast_int_to_AExp
Cast_nat_to_int
= Cast_int_to_AExp
Cast_int_to_AExp(Cast_nat_to_int
Cast_nat_to_int(A : nat))+
Cast_int_to_AExp(Cast_nat_to_int
Cast_nat_to_int(ss(B : nat))).
In defining trterm , for each pair of relation (s′ , s) in ≤, we pick a well-formed constructor sequence
C1 , ...,Cn , such that the target sort of C1 is s and the input sort of Cn is s′ . The sequence defines the way of
translating a sub-term t having sort s′ to a sort s by constructing C1 (...(Cn (t))...) in trterm . Because of the
core equality relation, the choice does not affect the construction of the equivalence classes in T(Σ# ,E # ) ,
and not affect the represented equivalence classes by a term in TΣ# (X ). We have three theorems about the
translation function trterm and term in T(Σ# ,E # ) and TΣ# (X ).
Theorem 3.3. Let Σ be an order-sorted signature, TΣ be the term algebra of it, E be the equation set of
the order-sorted algebra, TΣ,E be the terms TΣ modulo equations E, TΣ (X ) be the terms with variables in
the order-sorted algebra, Σ# be the translated many-sorted algebra of signature Σ, TΣ# , E # , T(Σ# ,E # ) and
TΣ# (X ) are the corresponding translations of items in the order-sorted algebra, and trterm be the translation
function of terms.
(1) If a term t has least sort s in Σ, then its translation t ′ has the target sort s.
′
(2) For a term t in TΣ,E , for any two term translation functions trterm and trterm
having difference in
′
picking different sequences of constructors for pairs in ≤, if c ∈ T(Σ# ,E # ) and trterm (t) ∈ c, then trterm
(t) ∈
c.
′
(3) For a term t(X ) in TΣ (X ), for two translation functions trterm and trterm
having difference in pick′
ing different sequences of constructors for pairs in ≤, we have two terms trterm (t(X )) and trterm
(t(X )),
#
′
for any substitution h mapping X to TΣ such that t and t are the result of replacing each variable x in
′
(t(X )) by h(x), if c ∈ T(Σ# ,E # ) and t ∈ c, then t ′ ∈ c.
trterm (t(X )) and trterm
Proof. Part (1) is trivial because after we require our operators to be strictly sensible, so any term must
have a unique least target sort in the original order-sorted algebra and the target sort is also the target sort
of the translated term in TΣ# without converting it to other supersort s′ by adding non-core constructors
on top of it.
′
cast it into a
To show (2), if for a term t having sort s′ , and the translation functions trterm and trterm
term in sort s without the need of translating the subterms of t, then the two resulting terms trterm (t) and
′
trterm
(t ′ ) are trivially in the same equivalence class based on the definition of core equality. The sorts s′
and s must be the same because the order-sorted definition in this paper requires sort equivalence in two
sides of an equation.
If there is a term t having a subterm f (t1 , ...,tn ), if the position i of the list t1 , ...,tn has target sort s
according to the signature, the term ti has sort s′ and s′ ≤ s, then a given translation function generates
well-formed non-core constructor sequences having the form C1 , ...,Cn to translate the term ti . We refer
to the number of the non-core constructors in this sequence as n, which is the same as one of the distances
between s′ and s in O. We induct on maximal numbers of the non-core constructors in each argument
position in a term t. If the maximal number of argument non-core constructors is zero, it means that trterm
′
do not translate the direct subterms of f (t1 , ...,tn ), so any translations on f (t1 , ...,tn ) to a target
and trterm
′′
sort s generate terms in the same equivalence class. Assuming that when the maximal numbers of non′
′
′
core constructors are less than k, trterm ( f (trterm (t1 ), ...,trterm (tn ))) and trterm
( f (trterm
(t1 ), ...,trterm
(tn )))
generate terms in the same equivalence class; if the position i in f (t1 , ...,tn ) has sort s, the term ti has sort

30

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

s′ , s′ ≤ s and the maximal distance between s′ and s is k + 1, if there is only one path from s to reach
′
s′ , then trterm (ti ) must be the same as trterm
(ti ) since we generate only one non-core constructor for each
pair in O. If there are at least two paths, without losing generality, assuming that trterm has the longest
′
path, trterm picks the well-formed sequence C1 , ...,Ck+1 to translate ti to a term having sort s and trterm
picks the well-formed sequence K1 , ..., Km to translate ti to a term having sort s, where m ≤ k + 1. Based
on the definition of core equality, C1 (...(Ck+1 (ti ))...) =core K1 (...(Km (ti ))...), hence, any argument ti of
′
into terms in the same equivalence class and f (t1 , ...,tn ) are
f (t1 , ...,tn ) is translated by trterm and trterm
′
also translated by trterm and trterm into terms in the same equivalence class.
To show (3), the proof basically modifies the proof of part (2) to allow variables in the term and by
′
are in
any substitution on the same variables in two terms t and t ′ that are generated by trterm and trterm
the same equivalence class.

Translating Semantic Rules. Translating semantic rules R to R# is very straight forward and similar to the one in translating equations in E to E # . For each pair (t(X ),t ′ (X )) in R, the first step
is to apply the term translation on t(X ) and t ′ (X ), to be terms in TΣ# (X ). Then, we add one rule
(trterm (t(X )),trterm (t ′ (X ))) to R# . Since we assume that all order-sorted algebra are sort decreasing,
the right hand side of a rule might have a top-most target sort being a subsort of the left hand side of
the rule. After they are translated into many-sorted algebras, the two sides of a rule must have the same
top-most target sort. We solve this problem by casting the right hand side of a rule to have the top-most
sort equal to the left hand side. For example, in translating the rule − 0 ⇒ 0 in the order-sorted algebra
in Figures 1 and 2, we make a new rule − 0 ⇒ Cast_nat_to_int
Cast_nat_to_int(0) in the translated many-sorted algebra.
For a given order-sorted algebra A as (S, O, Φ, Σ, E, R), our translation produces the many-sorted
algebra (S,trΣ (Σ),trE (E),trR (R)). We show that our many-sorted algebra maintains a bi-simulation
relation as the original order-sorted algebra. The bi-simulation proof is based on structural inductions on
the signature (S, O, Φ, Σ) and (S,trΣ (Σ)).
Theorem 3.4 (Bi-simulation between A and tr(A)). Let (S,trΣ (Σ),trE (E),trR (R)) be the translated
many-sorted algebra of a given order-sorted algebra (S, O, Φ, Σ, E, R), For any r in R and term t in T(Σ,E) ,
if t −→r t ′ , then we have trΣ (t) −→trR (r) trΣ (t ′ ). For any p in T(Σ# ,E # ) , if p −→trR (r) p′ , then there are
terms t and t ′ such that p = trΣ (t), p′ = trΣ (t ′ ) and t −→r t ′ .
Proof. Since all argument compatible operators are required to be strong sensible and maximal argumentbounding, all argument compatible operators with the same constructor should be translated into one
specific operator in the many-sorted algebra. Hence, the proof of the bi-simulation relation can be divided into three parts. The first part is to show that for every term t in T(Σ) , after we translate it to T(Σ# ) ,
it might have many instances t1 , ...,tn , but they are equivalent under core equality, and vice versa.
We only show one direction of the proof of the first part. We can structurally induct on term t. t
can be expressed as f (t1 , ...,tn ), after it is translated into a term in T(Σ# ) , we inductively assume that all
subterms of t1 , ...,tn are in the same equivalence class under core equality. For a term ti , if there is a
list of constructors C1 , ...,Cq and K1 , ..., Km such that term ti can be translated into C1 (...(Cq (ti ))...) and
K1 (...(Km (ti ))...), then C1 (...(Cq (ti ))...) and K1 (...(Km (ti ))...) are equivalent under core equality, because
the translation function translates a term t to terms in T(Σ# ) by adding non-core constructions which are
corresponding to the subsort relations in set O, and if it is translated into two different terms, then there
are two paths from the target sort of C1 to the argument sort of Cq (the target sort of C1 must be the same
as the target sort of K1 and the argument sort of Cq must be the same as the argument sort of Km ), and the
core equality equations should equate these two terms according to its definition.

Liyi Li and Elsa Gunter

31

The second part is to show that every class c in T(Σ,E) , when the terms of c are translated to terms in
T(Σ# ,E # ) , these terms are still in the same equivalence classes, and for every class c′ T(Σ# ,E # ) , and for all
terms t ′ in c′ , all the terms t that satisfy the relation trterm (t) = t ′ where t ′ ∈ c′ , are in a unique class c in
T(Σ,E) .
In the proof of the second part, we only show one direction. For a class c in T(Σ,E) , all its terms
are t1 , ...,ti , ..., for all these terms, when they are translated into terms in T(Σ# ) , we know that one term ti
might be translated into different terms s1 , ..., sn , but all these terms are equivalent under core equality.
In addition, when we translate equations, we only translate the two sides of equations, which are terms in
T(Σ# ) (X ), and the translated two sides have have different representations but they are all equivalent under
core equality. So for any two terms ti and tk in c, when they are translated into u1 , ..., un and v1 , ..., vm in
T(Σ# ) ; first, u1 , ..., un and v1 , ..., vm are equivalent under core equality, respectively. Second, for any two
terms ua and ub where a ∈ [1, n] and b ∈ [1, m], these two terms can be proved to be equivalent through
set E # , so they are in the same equivalence class in T(Σ# ,E # ) .
The third part is to show that for any r in R and term t in T(Σ,E) , if t −→r t ′ , then we have trΣ (t) −→trR (r)
trΣ (t ′ ). For any p in T(Σ# ,E # ) , if p −→trR (r) p′ , then there are terms t and t ′ such that p = trΣ (t), p′ = trΣ (t ′ )
and t −→r t ′ .
We also only show one direction here. For any r in R, it can be expressed as (t1 ,t2 ), where t1 and t2
are in T(Σ) (X ), there are two situations. First, if the target sorts of t1 and t2 are the same, then the argument
will be the same as the equation proof in the second part above. If the target sort s′ of t2 is a subsort of
s of t1 , we need to show that for any context C[], and for any term t −→r t ′ , and trΣ (t) −→trR (r) trΣ (t ′ ),
we have C[t ′ ] and trΣ (C[trΣ (t ′ )]) to be both valid (well-formed) terms. The notation trΣ (C[]) means that
we have a way to translate the context C[] such that if we put a redex a of T(Σ# ) in the context, the whole
expression is valid in T(Σ# ) . Recall that we have the condition that C[t] must be a valid term. Hence, the
hole in the context C[] must at least be able to hold a term with target sort s, and the target sort of trΣ (t ′ )
is also s, then trΣ (C[trΣ (t ′ )]) is also a valid term as long as C[t] is a valid term.

4

Related Work

The idea of order-sorted algebras was first systematically introduced into the programming language
field by Goguen et al. [11]. The main contribution of the work is to introduce subtyping relations for the
syntactic constructs so that operators do not only belong to one sort, but also act as constructs in supersort
of the defined sort. In addition, it defines a general operational semantic model for order-sorted algebras.
Many people tried to define rewriting strategies, unifications and equational rules on top of order-sorted
algebras and further extended the operational semantics of order-sorted algebras [1, 5, 12, 14, 20]. Stell
[26] tried to introduce a general framework to contain all existing order-sorted algebra semantics in his
work. In the paper of Goguen et al. [11], they introduce a way of translating initial free (algebras
that have no equations and rules) order-sorted algebras to many-sorted ones. Their way of translation
is similar to our work by adding non-core constructors. However, their work is solely on dealing with
initial free algebras without mentioning how to translate a general order-sorted algebra to a many-sorted
one because the purpose of their translation is to translate their order-sorted logic into a first order logic
in a many-sorted world, so that they can show their order-sorted logic is decidable. Obviously, they also
do not need to investigate a bi-simulation relation between their order-sorted algebras and the translated
many-sorted ones.
Based on the order-sorted algebras, Meseguer et al. [17, 18] developed rewriting logic. The biggest

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

32

contribution of rewriting logic is to contain the operational semantics of order-sorted algebras and distinguish equations and rewriting rules so that equations partition the terms into equivalence classes while
rewriting rules act like traditional transition rules in structural operational semantics. Based on rewriting
logic, Maude [4] implements the syntax and semantics of rewriting logic and provides several useful
tools and applications [19, 7, 8]. Other implementation of order-sorted algebras include PROTOS(L) [2]
which has an operational semantics based on polymorphic order-sorted resolution. K [25] is a framework
based on order-sorted algebras, which provides language developers a convenient way to write language
specifications. A lot of specifications have specified in K, including the semantics of Java [3], Javascript
[23], PHP [10], C [9, 13] and LLVM [15].
On the other hand, the study and exploration of many sorted algebra has a long history. Its logic
system has been explored by Wang [28]. Many well-known programming languages such as C, Java,
LLVM and Python are based on many-sorted algebras. One of the most prominent and mathematical
of programming language specifications, Standard ML by Milner, Tofte, Harper, and Macqueen [22]
is based on many sorted algebras. The simple type systems of the two famous theorem provers: Isabelle/HOL [24] and Coq [6] are also based on them, which motivates us to provide a translation from
order-sorted algebras into many-sorted ones.
As far as we know, the most recent attempt of translating order-sorted algebras into many-sorted
ones is given by Meseguer and Skeirik [21]. The purpose of the paper is to prove the decidability of the
order-sorted logic defined in their paper by translating it to a many-sorted world, so their translation still
focuses initial free order-sorted algebras (algebras that have no equations and rules), and only provide a
naive translation to translate order-sorted equations and rules to many-sorted ones. In their translation, by
adding possible more sorts, they calculate the least sorts of constructs and put them under corresponding
sorts to create the signature of a many-sorted algebra. For any given rule, they add more rules if variables
of the rule have subsorts in the original order-sorted algebra. They need to add one more rule for each
subsort of a variable in a rule.
For example, in dealing with the order-sorted algebra in Figures 1 and 2, to translate the equation
+ B : AExp = B : AExp+
+ A : AExp, they generate three different equations: A : nat+
+ B : nat = B :
A : AExp+
+ A : nat, A : int+
+ B : int = B : int+
+ A : int and A : AExp+
+ B : AExp = B : AExp+
+ A : AExp. The
nat+
original rule involves only one sort AExp. if there is a rule involving AExp, BExp and Stmt, which all have
subsorts, then the algorithm generates sixteen different equations in the translated many-sorted algebra.
In fact, if there is a rule or an equation involving n variables having different sorts and each of them
have m different subsorts, the algorithm generates mn different rules or equations in the translated manysorted algebra. On the other hand, our translation does not change their sorts. We view subsort relations
as implicit coercions, while our translation makes them into explicit ones by inserting a constructor for
each relation and making the relation into a unary operator in the given order-sorted algebra. We insert
a new equational rule named core equality to introduce new partitions on the equivalence classes of the
terms allowed in the algebra. Because of these features, our translation is of similar size of equations and
rewrite rules in the translated many-sorted algebra (adding no more than |S|2 new equations) and gives
users a simpler final description of the language specifications.

5

Conclusion.

In this paper, we propose an algorithm to translate an order-sorted algebra into 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.

Liyi Li and Elsa Gunter

33

By defining this relation, we reduce the complexity in translating a strictly sensible order-sorted algebra
to a many-sorted one, and increase the translated many-sorted algebra equations by a number less than
|S|2 , which is the square of the size of the sort set and is a very small number compared to the number
of equations and rules in an algebra. We also keep the number of rewrite rules in the algebra in the same
amount. We then prove the order-sorted algebra and the translated many-sorted algebra to be bisimilar
(Section 3). We also showed that core equality is indeed an equivalence relation and other properties of
our translated many-sorted algebras. Along with showing our algorithm and theories, an IMP language
is introduced as an example of the algorithm. We believe that our translation facilitates transformations
of order-sorted specifications in K or Maude into many-sorted systems in Isabelle/HOL or Coq, which
will empower users to prove theorems about large and popular language specifications.
This work is a important part of building a compilation relation between the K framework and a
functional programming language. We intend to build a transformation to translate specifications defined
in K to specifications defined in Isabelle automatically and correctly. The translated specifications should
be human readable and user friendly because the ultimate goal of the project is to use the translated
specifications to prove properties about programming languages.

References
[1] María Alpuente, Santiago Escobar, Javier Espert & José Meseguer (2014): A Modular Order-sorted Equational Generalization Algorithm. Inf. Comput. 235, pp. 98–136, doi:10.1016/j.ic.2014.01.006.
[2] Christoph Beierle & Gregor Meyer (1994): Run-time type computations in the Warren Abstract machine. The
Journal of Logic Programming 18(2), pp. 123 – 148, doi:10.1016/0743-1066(94)90049-3. Available at
http://www.sciencedirect.com/science/article/pii/0743106694900493.
[3] Denis Bogdănaş & Grigore Roşu (2015): K-Java: A Complete Semantics of Java. In: Proceedings of the
42nd Symposium on Principles of Programming Languages (POPL’15), ACM, pp. 445–456, doi:10.1145/
2676726.2676982.
[4] Manuel Clavel, Steven Eker, Patrick Lincoln & José Meseguer (1996): Principles of Maude. In J. Meseguer,
editor: Electronic Notes in Theoretical Computer Science, 4, Elsevier Science Publishers, doi:10.1016/
S1571-0661(04)00034-9.
[5] Hubert Comon (1990): Equational formulas in order-sorted algebras, pp. 674–688. Springer Berlin Heidelberg, Berlin, Heidelberg, doi:10.1007/BFb0032066.
[6] Pierre Corbineau (2008): A Declarative Language for the Coq Proof Assistant, pp. 69–84. Springer Berlin
Heidelberg, Berlin, Heidelberg, doi:10.1007/978-3-540-68103-8_5.
[7] Steven Eker, Merrill Knapp, Keith Laderoute, Patrick Lincoln & Carolyn Talcott (2002): Pathway Logic:
Executable Models of Biological Networks. In: Fourth International Workshop on Rewriting Logic and Its
Applications (WRLA 2002), Pisa, Italy, September 19 — 21, 2002, Electronic Notes in Theoretical Computer
Science 71, Elsevier, doi:10.1016/S1571-0661(05)82533-2.
[8] Steven Eker, José Meseguer & Ambarish Sridharanarayanan (2003): The Maude LTL Model Checker and
Its Implementation. In: Proceedings of the 10th International Conference on Model Checking Software,
SPIN’03, Springer-Verlag, Berlin, Heidelberg, pp. 230–234, doi:10.1007/3-540-44829-2_16.
[9] Chucky Ellison & Grigore Rosu (2012): An Executable Formal Semantics of C with Applications. In:
Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
(POPL’12), ACM, pp. 533–544, doi:10.1145/2103656.2103719.
[10] Daniele Filaretti & Sergio Maffeis (2014): An Executable Formal Semantics of PHP, pp. 567–592. Springer
Berlin Heidelberg, Berlin, Heidelberg, doi:10.1007/978-3-662-44202-9_23.

34

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

[11] Joseph A. Goguen, Jean-Pierre Jouannaud & José Meseguer (1985): Operational Semantics for Order-Sorted
Algebra. In: Proceedings of the 12th Colloquium on Automata, Languages and Programming, SpringerVerlag, London, UK, UK, pp. 221–231, doi:10.1007/BFb0015747.
[12] Joseph A. Goguen & José Meseguer (1992): Order-sorted Algebra I: Equational Deduction for Multiple
Inheritance, Overloading, Exceptions and Partial Operations. Theor. Comput. Sci. 105(2), pp. 217–273,
doi:10.1016/0304-3975(92)90302-V.
[13] Chris Hathhorn, Chucky Ellison & Grigore Roşu (2015): Defining the Undefinedness of C. In: Proceedings
of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI’15),
ACM, pp. 336–345, doi:10.1145/2813885.2737979.
[14] Claude Kirchner, Hélène Kirchner & José Meseguer (1988): Operational semantics of OBJ-3, pp. 287–301.
Springer Berlin Heidelberg, Berlin, Heidelberg, doi:10.1007/3-540-19488-6_123.
[15] Liyi Li & Elsa Gunter (2016): LLVM Semantics. Available at https://github.com/kframework/
llvm-semantics.
[16] Narciso Martí-Oliet & José Meseguer (2002): Rewriting Logic as a Logical and Semantic Framework, pp.
1–87. Springer Netherlands, Dordrecht, doi:10.1007/978-94-017-0464-9_1.
[17] Narciso Martí-Oliet & José Meseguer (2002): Rewriting logic: roadmap and bibliography. Theoretical Computer Science 285(2), pp. 121 – 154, doi:10.1016/S0304-3975(01)00357-7. Available at http://www.
sciencedirect.com/science/article/pii/S0304397501003577. Rewriting Logic and its Applications.
[18] José Meseguer (1999): Research Directions in Rewriting Logic. In Ulrich Berger & Helmut Schwichtenberg,
editors: Computational Logic, Springer Berlin Heidelberg, Berlin, Heidelberg, pp. 347–398, doi:10.1007/
978-3-642-58622-4_10.
[19] José Meseguer (2003): Software specification and verification in rewriting logic. NATO SCIENCE SERIES
SUB SERIES III COMPUTER AND SYSTEMS SCIENCES 191, pp. 133–194.
[20] José Meseguer, Joseph A. Goguen & Gert Smolka (1989): Order-sorted Unification. J. Symb. Comput. 8(4),
pp. 383–413, doi:10.1016/S0747-7171(89)80036-7.
[21] José Meseguer & Stephen Skeirik (2017): Equational formulas and pattern operations in initial order-sorted
algebras. Formal Aspects of Computing 29(3), pp. 423–452, doi:10.1007/s00165-017-0415-5.
[22] Robin Milner, Mads Tofte & David Macqueen (1997): The Definition of Standard ML. MIT Press, Cambridge, MA, USA.
[23] Daejun Park, Andrei Ştefănescu & Grigore Roşu (2015): KJS: A Complete Formal Semantics of JavaScript.
In: Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI’15), ACM, pp. 346–356, doi:10.1145/2737924.2737991.
[24] Lawrence C. Paulson (1990): Isabelle: The Next 700 Theorem Provers. In P. Odifreddi, editor: Logic and
Computer Science, Academic Press, pp. 361–386.
[25] Grigore Roşu & Traian Florin Şerbănuţă (2010): An Overview of the K Semantic Framework. Journal of
Logic and Algebraic Programming 79(6), pp. 397–434, doi:10.1016/j.jlap.2010.03.012.
[26] John G. Stell (2002): A Framework for Order-Sorted Algebra. In: Proceedings of the 9th International
Conference on Algebraic Methodology and Software Technology, AMAST ’02, Springer-Verlag, London,
UK, UK, pp. 396–410, doi:10.1007/3-540-45719-4_27.
[27] Alexandre Boulgakov A.W. Roscoe Thomas Gibson-Robinson, Philip Armstrong (2014): FDR3 — A Modern
Refinement Checker for CSP. In Erika Ábrahám & Klaus Havelund, editors: Tools and Algorithms for the
Construction and Analysis of Systems, Lecture Notes in Computer Science 8413, pp. 187–201, doi:10.1007/
978-3-642-54862-8_13.
[28] Hao Wang (1952): Logic of many-sorted theories. Journal of Symbolic Logic 17(2), pp. 105–116, doi:10.
2307/2266241.

