Interoperability is the capability of two languages to interact within a single system: HTML, CSS, and JavaScript can work together to render webpages. Some object oriented languages have interoperability via a virtual machine host (.NET CLI compliant languages in the Common Language Runtime). A high-level language can be interoperable with a low-level one (Apple's Swift and Objective-C). While there has been some research in the foundations of interoperability there is little supporting theory. This paper is based upon our existing work on combining languages to produce so-called multi-languages. Here, we define an equational logic for deducing valid equations, from axioms that postulate properties of the multi-language. We define set-theoretic multi-language algebras as models, and provide algebraic constructions such as congruences and quotient algebras. Such models, and the constructions, provide the ingredients for the main deliverable, soundness and completeness for the equational logic. We illustrate the basic ideas with a running example.
Multi-languages arise by combining existing languages [
But what exactly are multi-languages? What is a good abstract definition of
a multi-language? How should we be thinking conceptually? The problem was
originally addressed in [
Commons License Attribution 4.0 International (CC BY 4.0).
constructs able to regulate the flow of values between the underlying languages.
Buro, Crole, and Mastroeni [
Here we focus on equational algebras [
Research on equational reasoning and logic has been prolific (see [
order-sorted equational logic [
Running Example: Throughout the paper we develop a small illustrative application example that lays the foundations for combining a core imperative language with a functional one (the simply-typed lambda-calculus). In particular, we show how we can provide a formal semantics to multi-language terms accompanied by an equational theory. For instance, we formally define the semantics of the multi-language term x = ( y:int . z * y) 5 obtained by blending a lambda-term into an imperative program. 2 2.1
assume readers are familiar with these ideas, but include definitions to set up notation.
triple Sg , (S; ; ), where (S; ) is a poset of sorts and is an (S S)sorted set , f w;s j (w; s) 2 S S g of operators. If 2 w;s we call an operator (symbol) and (w; s) the rank of . If w = ", we call the operator a constant, and otherwise a function symbol. Given , we write f : w ! s, for function symbols, and k : s for constants, as shorthands for the set memberships.
(1os) each constant has a unique rank ("; s): we abbreviate the rank to s and say sort as a synonym; and (2os) function symbols satisfy the following monotonicity condition: if we have f : w1 ! s1 and f : w2 ! s2 with w1 w2, then s1 s2.
an order-sorted signature Sg , (S; ; ) is specified by an S-sorted set A , ( JsKA , As j s 2 S ) of carrier sets, together with interpretation functions J : w ! sKA : JwKA ! JsKA for each operator : w ! s, where w , s1 : : : sn and JwKA , Js1KA JsnKA. In the case that w = ", so that is a constant k, we define J"KA , f g; then, instead of Jk : sKA : f g ! JsKA, we write Jk : sKA 2 JsKA. These data satisfy: w2, then Jf : w1 ! s1KA(a) = (1oa) s s0 implies JsKA Js0KA; and (2oa) if f : w1 ! s1 and f : w2 ! s2 with w1
Jf : w2 ! s2KA(a) for all a 2 Jw1KA.
From now on, we drop the algebra subscript and the ranks of operator symbols within the semantic brackets whenever they are clear from the context.
nature and let A and B be Sg-algebras. An order-sorted Sg-homomorphism h : A ! B is an S-sorted function h : A ! B such that (1oh) hs(JkKA) = JkKB for each k : s; (2oh) hs Jf : w ! sKA = Jf : w ! sKB hw for each f : w ! s; and (3oh) s s0 implies hs(a) = hs0 (a) for each a 2 JsKA.
Sg-homomorphisms form a category denoted by OSAlgSg .
Among the algebras in OSAlgSg , the term Sg-algebra TSg is freely generated
from Sg in the usual way. The carrier set JsKTSg consists of the (ground) terms
t of sort s. Function symbols f are modelled as interpretation functions which
build new terms from old ones by “applying f ”; for instance, Jf KTSg (t) , f (t).
Note that any term t can appear in several carrier sets of the term algebra:
terms are polymorphic. A key property of signatures, related to polymorphism, is
regularity (see [
Proposition 1. If Sg is a regular signature, the term Sg-algebra TSg is an initial object in OSAlgSg , that is, there is a unique homomorphism h : TSg ! A for any Sg-algebra A. The components (TSg )s are defined by (mutual, structural) induction, hence hs can be defined by structural recursion. Since we are seeking a homomorphism, we must have hs(f (t1; : : : ; tn)) = Jf KA(hw(t1; : : : ; tn)) and hs(k) = JsKA. But this is exactly a structural recursion, and the unique one yielding a homomorphism. As such, it makes sense to define the (unique) interpretation of a term t, by way of its least sort, as
JtKA , hst (t)
Since our paper focuses in entirety on how the syntax of languages is combined, term algebras such as this one, and others, will play a major role. 2.2
A key role of a multi-language specification is to specify which terms of one
language can be deployed in the other. As such, showing exactly how this is
done is a key milestone in the paper. Such a choice amounts, formally, to a
mapping between terms of one language and terms of the other, and it is usually
defined between syntactic categories (i.e., collection of terms) rather than single
terms [
SG , (Sg1; Sg2; n) is defined by a pair of signatures Sg1 , (S1; 1; 1) and Sg2 , (S2; 2; 2) and a binary interoperability relation n over S1 + S2 such that si n s0j with i; j 2 f1; 2g and i 6= j (thus, due to our notation, in relationships si n s0j we have s 2 Si and s0 2 Sj).
The idea is that if si n s0j and t is a term of sort s in Sgi, then t can be used
“as a term with with sort s0 in the language generated by Sgj”. A multi-language
algebra provides meaning to the underlying languages Sg1 and Sg2 and it specifies
exactly how terms of sort s may be converted to terms of sort s0 whenever si n s0j.
These specifications are called boundary functions [
Definition 5 (Multi-Language Algebra). Let SG , (Sg1; Sg2; n) be a multilanguage signature. An SG-algebra A is given by – a pair of order-sorted algebras A1 and A2 over Sg1 and Sg2; and – a boundary function Jsi n s0jKA : JsKAi ! Js0KAj for each constraint si n s0j. Example 1. Let Sg(Imp) and Sg( ) be the signatures of a small imperative language and the simply-typed lambda-calculus. We may want to define the interoperability relation between these two languages in order to use -terms as expressions in Imp and vice versa. As a result, we can achieve multi-language programs such as x = ( y:int . z * y) 5 (the multi-language terms are formally introduced in Definition 8). Note that, despite the simplicity, the evaluation of such a term requires a careful translation of meanings between the underlying languages: In order to obtain the value to assign to x, we first need to compute the application, which in turn needs the interpretation of 5 as a -term. Such conversions are specified by the boundary functions.
Homomorphisms between multi-language algebras are ordinary algebraic homomorphisms that also commute with the boundary functions.
multi-language SG , (Sg1; Sg2; n)-algebras. A SG-homomorphism h : A ! B is given by a pair of order-sorted homomorphisms h1 : A1 ! B1 and h2 : A2 ! B2 such that they commute with boundary functions, namely, if si n s0j, then (hj)s0 (hi)s.
Jsi n s0jKA = Jsi n s0jKB
We can define an S-sorted set A by setting Asi , JsKAi ; and given any such SG-homomorphism h, there is an S-sorted homomorphism h : A ! B given by hsi , (hi)s : Asi ! Bsi (which commutes with boundary functions). Lemma 1. The mapping h 7! h is well-defined, a bijection, and functorial in that h h0 = h h0. This is immediate from the definitions. Note that we will usually write h for h, thus identifying the two concepts, and regard h : A ! B and h : A ! B as inter-changeable throughout the paper.
A multi-language signature gives rise to an order-sorted one by adding conversion operators ,!si;s0j for each interoperability relation si n s0j: each conversion operator maps a term of type si (informally, a term built from Sgi) into a term of type s0j (informally, a term built from Sgj).
Definition 7 (Associated Signature). Let SG , (Sg1; Sg2; n) be a multilanguage signature. The associated signature SG , (S; ; SG ) of SG is the order-sorted signature defined as follows: – the poset (S; ) of sorts is given by S , S1 + S2 and by defining si rj if and only if i = j and s i r; and – the order-sorted set of operators SG is defined by the clauses if f : w ! s is a function symbol in i for some i , 1; 2, then fi : wi ! si is a function symbol in SG ; if k : s is a constant in i for some i , 1; 2, then ki : si is in SG ; and a conversion operator ,!si;s0j : si ! s0j in SG for each si n s0j.
A multi-language signature is defined regular if and only if the underlying signatures are regular. An immediate consequence is that if SG is regular, then so too is SG. In the multi-language context, the term SG-algebra TSG defines the terms resulting from the combination of the underlying languages: Definition 8 (Term SG-Algebra TSG ). Let SG , (Sg1; Sg2; n) be a multilanguage signature. The term SG-algebra TSG is defined as follows: – the order-sorted Sgi-algebra (TSG )i is specified by:
JsK(TSG)i , JsiKTSG for each s 2 Si; JkK(TSG)i , JkiKTSG for each k : s in i; and
Jf : w ! sK(TSG)i , Jfi : wi ! siKTSG for each f : w ! s in i; – boundary functions are defined by Jsi n s0jKTSG , J,!si;s0j KTSG for each si n s0j. A multi-language ground term t is any element of (TSG )si , JsK(TSG)i , JsiKTSG for some si; TSG is of course the “standard” term order-sorted algebra over order-sorted SG, and we will say that t has sort si.
It follows that each multi-language ground term t has a unique least sort st when the signature is regular, being the least sort of t over the associated signature (and of course t may inhabit many other carrier sets).
The category whose objects are multi-language SG-algebras and morphisms
are multi-language SG-homomorphisms is denoted by MLAlgSG . Moreover, as
in the order-sorted case, the multi-language term algebra TSG over a regular
multi-language signature SG is initial in MLAlgSG [
Universal Constructions in a Multi-Language Context
To formally define the terms of our multi-languages we shall make use of the concept of free algebras. First we review the abstract concept, and then we show that “terms built using variables” are a concrete instance of a free algebra. The universal property of a free algebra provides a convenient tool for defining and working with term substitutions.
A free algebra is the loosest algebra generated from an S-sorted X (whose
elements are understood as variables). As usual [
Definition 9 (Free SG -Algebra F(X) over X). Let X be an S-sorted set of variables. A free SG -algebra F(X) over X is an SG -algebra F(X) together with an S-sorted function X : X ! F (X) such that the following universal property is satisfied: – For each SG -algebra A, if a : X ! A is an S-sorted function, then there exists a unique multi-language SG -homomorphism a : F(X) ! A making the following diagram commute:
X
X a
F (X)
a A
F(X)
a A (1)
The previous definition does not guarantee the existence of such a free SG algebra over X. However, if it does exist it is unique up to a unique isomorphism. We now provide a two-step syntactic construction, establishing existence. See, for instance, [9, Definition 1.3.2], [13, p. 72], and [12, p. 14] for a free algebra construction in the one-sorted, many-sorted, and order-sorted worlds. We now define a specific instance of F(X), denoted by T(X), and constructed out of syntax.
Definition 10 (Syntactic Free SG -Algebra T(X) over X). 1. Let SG be a multi-language signature and X an S-sorted family of variables ( Xsi j si 2 S ), each component also disjoint from the symbols in SG . By setting Xi , ( (Xi)s , Xsi j s 2 Si ) we obtain an Si-sorted set of variables for i = 1; 2. The multi-language signature SG (X) , (Sg 1(X1); Sg 2(X2); n) over X has the same interoperability relation n as SG , along with order sorted signatures Sg i(Xi) , (Si; i; i(Xi)). These are defined with the same poset (Si; i) of sorts of Sg i, along with (Si Si)-sorted sets i(Xi) of operator symbols specified by – if operator : w ! s is in i, then : w ! s is also in i(Xi); and – if x 2 (Xi)s, then x : s is in i(Xi).
Informally, i(Xi) consists of all i operators and, for all s 2 Si, all variables of sort si.
SG (X)-algebra TSG(X) (use an instance of Definition 8). The order-sorted Sg i-algebras T(X)i, for i , 1; 2, are defined by – JsKT(X)i , JsK(TSG(X))i for each s 2 Si; – JkKT(X)i , JkK(TSG(X))i for each k : s in – Jf KT(X)i , Jf K(TSG(X))i for each f : w ! s in
And Jsi n s0jKT(X) : JsKT(X)i ! Js0KT(X)j is defined by
Jsi n s0jKTSG(X) : JsK(TSG(X))i ! Js0K(TSG(X))j Given X and SG, a multi-language term t is any element of the set T (X)si , JsKT(X)i , JsiKTSG(X) for some si; TSG(X) is of course the “standard” term order-sorted algebra over order-sorted SG(X), and we will say that t has sort si.
Example 3. Terms in the multi-language free algebra can be thought as ordinary multi-language terms with “holes”, where a hole is given by an algebraic variable. For instance, x = ( y:int . z * y) v is not ground since any Imp-expression can be plugged into v. Terms with free algebraic variables are the basis for axiomatizing signatures by equations, leading to fully-fledged algebraic theories.
T(X) is free over X in MLAlgSG . 3.2
The aim of this section is to introduce and extend well-known constructions of
universal algebra to multi-languages. Apart from this being interesting in its own
right, quotient algebras are central to our completeness proof. Indeed, we follow
the Birkhoff’s approach [
A congruence (relation) is an equivalence relation on the carrier sets of a given algebra which is compatible with its structure.
language SG-congruence , ( si JsiKA JsiKA j si 2 S ) is an S-sorted
family of equivalence relations such that
(1co) jSi , ( s , si j s 2 Si ) is an Sgi-congruence [
The next definition lifts the notion of quotient algebra to multi-languages. Intuitively, a quotient algebra is the outcome of the partitioning of an algebra through a congruence relation.
(1q) (A= )i is the order-sorted quotient Sg i-algebra [
For each quotient algebra A= of the multi-language algebra A, the homomorphic quotient map q : A ! A= is defined by q(a) = [a]. Moreover, the kernel of q is exactly . Following Definition 6 and Lemma 1 we shall also write q for the order-sorted homomorphism q : A ! A= . 4
We now give an equational logic for multi-language terms. We define equations between multi-language terms and show that our system is sound and complete for SG -algebras; we also show the existence of an initial algebra. Through conversion operators ,!, multi-language equations can usefully axiomatize boundary functions.
Definition 13 (Multi-Language Equations). Let SG , (Sg 1; Sg 2; n) be a coherent multi-language signature, X be an S-sorted set of variables, and T(X) the free SG -algebra over X. 1. An SG -equation over X is a judgement of the form t =X t0, such that t 2 T (X)si and t0 2 T (X)s0i for some s; s0 2 Si, where s and s0 are connected via i (equivalently, least sorts st and st0 are connected in Si). Note that t =X t is an SG -equation. The connectedness of st and st0 , and coherence which ensures both terms have a super-sort, is necessary to ensure that forthcoming definitions of equation satisfaction are well-defined. 2. A conditional SG-equation over X is a judgement of the form E ) t =X t0, such that t =X t0 is an SG -equation and E is a set of SG -equations over X.
An unconditional equation t =X t0 is ? ) t =X t0.
Example 4. In order to axiomatize the behaviour of boundary functions that allow the use of Imp-expressions in place of -terms and vice versa, we provide equations which define the conversion of values. Intuitively, we want to move the meaning of terms between the languages only when no more computational steps are possible. Let e be the sort of -terms and exp the sort of Imp-expressions: ,!e;exp (i) = i = ,!exp;e (i) ,!e;exp (x) = x = ,!exp;e (x) 8i 2 f: : : ; -1; 0; 1; : : :g 8x 2 Var ,!exp;e (true) = 1 ,!exp;e (false) = 0 The first equation allows the flow of integers between the imperative language and the simply-typed lambda-calculus. This is possible because both languages have the notion of integer values, but in more realistic cases, such a conversion should take into consideration different machine-integer implementations, overflow, etc. A variation on theme can be obtained by assuming a lambda-calculus that does not provide a primitive notion of integer numbers. In that case, the boundary functions can move Imp-integers to a suitable numeral encoding in the lambda-calculus, e.g., the Church encoding. The second equation establishes a correspondence between variable names of the two languages. Such a correspondence enables an implicit flow of values between Imp- and -environments. For instance, in Example 2, the free -variable z “becomes” an Imp-variable when we compute the semantics of the lambda term. Finally, the last two equations define the conversion of booleans to integers.
The next step is to show how new equations can be inductively generated (derived) from a set of axioms. The rules require the concept of substitution, namely a syntactic transformation that replaces variables with terms. Let X and Y be two sets of variables. A variable substitution is an S-sorted function : X ! T (Y ): for each variable x 2 Xsi we supply a term si (x), of sort si, involving variables from Y . Then by the freeness of T (X) (that is, freeness of T(X)), there is a unique substitution homomorphism : T (X) ! T (Y ) induced by such that X = : the idea is that for any t 2 T (X)si , recurses over t and then finally substitutes si (x) for each x occuring in t.
We shall adopt some further notation, used in the rules. If a : X ! A where X is a set of variables, then any x 2 Xsi has the unique sort si and we write a(x) , asi (x). Further, for any S-sorted homomorphism h : T (X) ! A, if t 2 T (X)si then of course hsi (t) 2 Asi . But, since there is a least sort st, also t 2 T (X)(st)i T (X)si , and since h is a homomorphism we have h(st)i (t) = hsi (t) 2 A(st)i Asi . From now on we write h(t) , h(st)i (t) (that is, h(t) = hsi (t) 2 Asi ) to reduce subscript notation.
ioms, the inductive rules of equational logic allow the derivation of new
unconditional equations. Our rules in Figure 1 are a modification of those in [
If t =X t0 is generated from AX then we write AX ` t =X t0. The rule (cong) intuitively says that replacing equals for equals yields new equalities, that is, term formation is a congruence. Thus we may build new equations using the “usual/informal” rules of equational reasoning. One easily proves admissible rule (sub), namely that if t =X t0 then (t) =Y (t0); but note that the proof requires the following fact. The composition of two substitution homomorphisms 1 : T (X) ! T (Y ) and 2 : T (Y ) ! T (Z) is still a substitution homomorphism, since it is induced by 2 1. To see that 2 1 = ( 2 1) note that 8x 2 Ssi2S Xsi : (x) =Y 0(x) (t) =Y 0 (t) (cong) 8u =X u0 2 E : (u) =Y
(u0) (t) =Y (t0) [E ) t =X t0 2 AX ] (axsub)
Fig. 1. Inference Rules for Inductively Defining Equational Logic.
multi-language signature SG . We refer to SG -equations as equations. A satisfies E ) t =X t0, denoted A E ) t =X t0, if for each assignment function a : X ! A such that a : T (X) ! A equalizes each equation in E , a also equalizes t and t0, i.e., a (t) = a (t0). Also, A t =X t0 just in case each a : X ! A equalizes t and t0. Let AX be a set of conditional and/or unconditional equations.
One may generalize the above fact about substitution homomorphisms to arbitrary assignment functions and SG -homomorphisms. We do so in the next lemma, which is used in the proof of soundeness and completeness.
signature SG , (Sg 1; Sg 2; n). If a : X ! A is an assignment function and h : A ! B is an SG -homomorphism, then (h a) = h a : F(X) ! B (or equivalently (h a) = h a : F (X) ! B).
and AX a set of axioms and t =X t0 any equation. Then AX ` t =X t0, just in case, for every SG -algebra A we have A AX implies A t =X t0.
Soundness is straightforward to prove. In order to prove completeness, we
build a quotient algebra (see [
Proposition 2. TAX (X) t =X t0 implies AX ` t =X t0.
The proof of completeness is then immediate if we can show that TAX (X) AX , for then TAX (X) t =X t0 follows by the assumption in the Theorem.
The class of the multi-language SG-algebras satisfying a set AX of axioms is denoted by MLMod AX , namely the class of models satisfying AX . If we take all the SG-homomorphisms between them, we have that MLMod AX is a full subcategory of MLAlgSG . In fact TAX (X) is free in MLMod AX , where the freeness is defined along the lines of Definition 9.
the quotient algebra TAX (X) is the free algebra over X in MLMod AX .
Since initiality is a special case of the freeness property and T(?) = T, then TAX = TAX (?) is an initial object in MLAlgAX . 5
Others have investigated issues that arise when combining languages: [
There is considerable work to explore in future. One might study language
combinations where the sort (type) and term structure is much richer. Here we
have looked only at equational logic, so the whole area of operational semantics
for multi-languages should be explored. And of course as well as the syntactic
languages we need also to explore suitable semantics (given as algebras in this
paper). Since equational theories give rise to free algebra monads [
As a final remark, we have further results about the categories of set-theoretic models mentioned within our paper, which are not presented here due to space limitations. However they would hopefully appear in a journal version.