# A Theoretical Foundation for Programming Languages
## Aggregation

Stefan Ciobaca, Dorel Lucanu, Vlad Rusu, Grigore Rosu

► To cite this version:

Stefan Ciobaca, Dorel Lucanu, Vlad Rusu, Grigore Rosu. A Theoretical Foundation for Programming Languages Aggregation. 22nd International Workshop on Algebraic Development Techniques, 2015, Sinaia, Romania. hal-01076641v2

HAL Id: hal-01076641

https://inria.hal.science/hal-01076641v2

Submitted on 4 May 2015

**HAL** is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.
# A Theoretical Foundation for Programming Languages Aggregation *

Ştefan Ciobăcă¹, Dorel Lucanu¹, Vlad Rusu², and Grigore Roşu¹,³

¹ “Alexandru Ioan Cuza” University, Romania

² Inria Lille, France

³ University of Illinois at Urbana-Champaign, USA

**Abstract.** Programming languages should be formally specified in order to reason about programs written in them. We show that, given two formally specified programming languages, it is possible to construct the formal semantics of an aggregated language, in which programs consist of pairs of programs from the initial languages. The construction is based on algebraic techniques and it can be used to reduce relational properties (such as equivalence of programs) to reachability properties (in the aggregated language).

## 1 Introduction

In this paper we are concerned with the problem of language aggregation: given two programming languages (in some formalism), construct a new language in which programs consist of pairs of programs from the original languages. Furthermore, a program $(P, Q)$ in the aggregated language should behave as if the programs $P$ and $Q$ (in the initial languages) would run interleaved or in parallel.

The main motivation behind the construction of the aggregated language is to be able to reduce reasoning about relational properties of programs (such as the equivalence of two programs $P$ and $Q$) to reasoning about a single program (the aggregated program $(P, Q)$). We have shown [6] for example that partial equivalence of programs reduces to partial correctness in an aggregated language. In general, aggregation is important because there are fewer results and tools for relational properties (e.g. equivalence of programs) than single program properties (e.g. partial correctness). All of our constructions are effective and therefore aggregation can be implemented as a module in a language framework such as K [15].

The main difficulty in aggregating two languages is making sure that there is a link between the datatypes being shared by the two languages. For example, if both languages have variables of type natural numbers, it is important that the naturals be interpreted consistently in the aggregated language in order to be able to express properties such as the equality of a variable in the first

<footnote>* This paper is supported by the Sectorial Operational Programme Human Resource Development (SOP HRD), financed from the European Social Fund and by the Romanian Government under the contract number POSDRU/159/1.5/S/137750.</footnote>
<figure><img src="image_1.png" /><figcaption>**Fig. 1.** (_CfgI*, S<sub>I</sub>, Σ<sub>I</sub>, Π<sub>I</sub>) and (_CfgF*, S<sub>F</sub>, Σ<sub>F</sub>, Π<sub>F</sub>), the signatures of IMP and FUN, detailed in Example 1. Only the function symbols are detailed in the figure; the predicates consist of the arithmetic comparison operators: Π<sub>I</sub> = Π<sub>F</sub> = {=Int, <Int, ≤Int}. The difference between the operators _+_, _-*_, etc. and their correspondants _+_, _-*_, etc. is that the former are the syntactic language constructs for addition, etc., while the latter are the actual function symbols denoting integer addition, etc.</figcaption></figure>

The functions above are written in Maude-like notation [4], the underscore (_) denoting the position of an argument. Although not written explicitly above, the signatures also include the one-argument injections needed to inject sorts like Int and Id into ExpI.

## 2.2 Syntax

Given a matching logic signature (_Cfg, S, Σ, Π), the set of matching logic formulas is given by the following grammar:

$$ \varphi ::= P(t_1, \dots, t_n), \neg \varphi, \varphi \wedge \varphi, \exists x. \varphi, \pi, $$

where P ranges over Π, t₁, ..., tₙ are terms of the appropriate sort for the predicate P, x ∈ Var is a variable and π ∈ T_Cfg(Var) is a term of sort Cfg.

Matching logic formulae include the classical constructs in first-order logic (predicates P(t₁, ..., tₙ), negation, conjunction and existential quantifier) and also a new construct π, called *basic pattern*, which allows to use terms of sort Cfg as atomic formulae. We also assume that the other first-order connectives (disjunction - ∨, implication - →, universal quantifier - ∀) are available and interpreted as usual as syntactic sugar over the existing connectives.

**Example 2.** The expression

$$ \langle \mathbf{while} (E) S, x \mapsto a, y \mapsto b \rangle \wedge a <_{I \text{nt}} b $$

is a (_CfgI*, S<sub>I</sub>, Σ<sub>I</sub>, Π<sub>I</sub>)-matching logic formula, where (_CfgI*, S<sub>I</sub>, Σ<sub>I</sub>, Π<sub>I</sub>) is that given in Figure 1.

We distinguish two particular types of matching logic formulae:

**Definition 1.** A matching logic formula is patternless if it conforms to the following grammar:

$$ \varphi_{\text{pless}} ::= P(t_1, \dots, t_n), \neg \varphi_{\text{pless}}, \varphi_{\text{pless}} \wedge \varphi_{\text{pless}}, \exists x. \varphi_{\text{pless}}. $$
Patternless matching logic formulae simply do not contain basic patterns.

Therefore they can be identified with FOL formulae. The second particular type of formulae we consider are pure formulae:

**Definition 2.** A matching logic formula is pure if it conforms to the following grammar:

$$ \varphi_{\text{pure}} ::= \pi, \varphi_{\text{pure}} \wedge \varphi_{\text{pless}}, \exists x. \varphi_{\text{pure}}. $$

Pure formulae contain at least one basic pattern and no basic pattern appears under negation.

## 2.3 Semantics

We denote by $\mathcal{T}$ a first-order model for the many-sorted first-order signature $(S, \Sigma, \Pi)$ that assigns sets to sorts, functions to function symbols and predicates to predicate symbols. By $\mathcal{T}_o$ we denote the interpretation of the object $o$ in the model $\mathcal{T}$. Well-sorted valuations are denoted by $\rho: \text{Var} \to \mathcal{T}$. Elements of $\mathcal{T}_{\text{Cfg}}$ (the set interpreting the sort of configurations) are denoted by the greek letter $\gamma \in \mathcal{T}_{\text{Cfg}}$ and are called configurations.

Matching logic formulae are interpreted in the presence of a (first-order) model $\mathcal{T}$, a (well-sorted) valuation $\rho$ and an element $\gamma \in \mathcal{T}_{\text{Cfg}}$.

**Definition 3.** The satisfaction relation $\models$ for matching logic is defined as follows:

1. $\mathcal{T}, \gamma, \rho \models P(t_1, \dots, t_n)$ if $(\rho(t_1), \dots, \rho(t_n)) \in \mathcal{T}_P$;

2. $\mathcal{T}, \gamma, \rho \models \neg \varphi$ if $\mathcal{T}, \gamma, \rho \not\models \varphi$;

3. $\mathcal{T}, \gamma, \rho \models \varphi_1 \wedge \varphi_2$ if $\mathcal{T}, \gamma, \rho \models \varphi_1$ and $\mathcal{T}, \gamma, \rho \models \varphi_2$;

4. $\mathcal{T}, \gamma, \rho \models \exists x. \varphi$, where $x$ is a variable of sort $s$, if there exists an element $u \in \mathcal{T}_s$ such that $\mathcal{T}, \gamma, \rho[x \mapsto u] \models \varphi$;

5. $\mathcal{T}, \gamma, \rho \models \pi$ for a basic pattern $\pi \in \mathcal{T}_{\text{Cfg}}(\text{Var})$ if $\rho(\pi) = \gamma$.

The first four cases are as in first-order logic and the last case (for basic patterns) is new. The semantics of basic patterns is given by matching the element $\gamma$ in the presence of which matching logic formulae are evaluated. This is where the name of matching logic comes from. When two basic patterns are connected by a logical and ($\wedge$) in the formula, the element $\gamma$ has to match both basic patterns, hence $\wedge$ plays the role of intersection. Using basic patterns under implications, logical or and existential/universal quantifiers makes it possible to express several interesting properties, but this is outside the scope of the current article.

**Example 3.** Let $\mathcal{T}_I$ denote the model for $\Sigma_I$ that interprets Int as the set of integers, the function and the predicate symbols over Int with the usual functions and predicates, respectively, and the function symbols corresponding to the BNF productions as term constructors. If

$$ \gamma = \langle \text{while} (x<y) x := x+1;, x \mapsto 2 y \mapsto 5 \rangle $$
$$
\begin{align*}
\langle x, \sigma \rangle &\Rightarrow \langle \text{eval}(\sigma, x), \sigma \rangle \\
\langle i_1 \text{ op } i_2, \sigma \rangle &\Rightarrow \langle i_1 \text{ op}_{\text{Int}} i_2, \sigma \rangle \\
\langle X := I, \sigma \rangle &\Rightarrow \langle \text{skip}, \sigma[I/X] \rangle \\
\langle \text{skip}; S, \sigma \rangle &\Rightarrow \langle S, \sigma \rangle \\
\langle \text{if } I \text{ then } S_1 \text{ else } S_2, \sigma \rangle \wedge I \neq 0 &\Rightarrow \langle S_1, \sigma \rangle \\
\langle \text{if } 0 \text{ then } S_1 \text{ else } S_2, \sigma \rangle &\Rightarrow \langle S_2, \sigma \rangle \\
\langle \text{while } E \text{ do } S, \sigma \rangle &\Rightarrow \langle \text{if } E \text{ then } S; \text{ while } E \text{ do } S \text{ else skip}, \sigma \rangle \\
\langle C[\text{code}], \sigma \rangle &\Rightarrow \langle C[\text{code}'], \sigma' \rangle \quad \text{if } \langle \text{code}, \sigma \rangle \Rightarrow \langle \text{code}', \sigma' \rangle \\
\text{where } C ::= - &| C \text{ op } E \mid i \text{ op } C \mid \text{if } C \text{ then } S_1 \text{ else } S_2 \mid v ::= C \mid C; S
\end{align*}
$$

<caption>**Fig. 2.** Specifying the semantics of IMP as a set $\mathcal{A}_I$ of reachability rules (schemata). $op$ ranges over the binary function symbols and $op_{\text{Int}}$ is their denotation in $\mathcal{T}_I$.</caption>

and $\rho(E) = x<y$, $\rho(S) = x := x+1$, $\rho(a) = 2$, $\rho(b) = 5$ then
$$ \mathcal{T}_I, \gamma, \rho \models \langle \mathbf{while} (E) S, x \mapsto a, y \mapsto b \rangle \wedge a < \mathcal{I}_{\text{nt}} b. $$

The $\Sigma_F$-model $\mathcal{T}_F$ is defined in a similar way. If

$$ \gamma' = \langle \text{letrec } f \ x = \text{ if } (x<1) \ \text{then} \ 1 \ \text{else} \ x*f(x-1) \ \text{in} \ f(5) \rangle $$

and $\rho'(F) = f$, $\rho'(X) = x$ and

$$ \rho'(E_1) = \text{if } (x<1) \text{ then } 1 \text{ else } x*f(x-1), \rho'(E_2) = f(5), $$

then

$$ \mathcal{T}_F, \gamma', \rho' \models \langle \text{letrec } F \ X = E_1 \ \text{in} \ E_2 \rangle \wedge \text{true.} $$

# 3 Reachability Logic

While matching logic allows to reason about individual configurations (of a program), reachability logic builds on matching logic to allow to reason and define the dynamic behaviour of programs.

## 3.1 Syntax

Reachability logic formulae are constructed in the presence of a matching logic signature $(\mathcal{C}fg, S, \Sigma, \Pi)$ as pairs of matching logic formulae:

**Definition 4.** A reachability logic formula (or equivalently, a reachability rule) $\varphi \Rightarrow \varphi'$ is a pair of matching logic formulae.

The intuition behind reachability formulae is that a configuration matching $\varphi$ advances into a configuration matching $\varphi'$.

*Example 4.* The set of reachability logic formulas $\mathcal{A}_I$ given in Figure 2 are specifying the semantics of IMP and the set of reachability logic formulas $\mathcal{A}_F$ given in Figure 3 are specifying the semantics of FUN. The specification

$$ \langle C[\text{code}], \sigma \rangle \Rightarrow \langle C[\text{code}'], \sigma' \rangle \quad \text{if } \langle \text{code}, \sigma \rangle \Rightarrow \langle \text{code}', \sigma' \rangle, $$

(resp. $\langle C[c] \rangle \Rightarrow \langle C[c'] \rangle$ if $\langle c \rangle \Rightarrow \langle c' \rangle$) is a rule schemata that defines an infinite set of reachability logic formulas.
$$
\begin{align*}
\langle I_1 \circ p, I_2 \rangle &\Rightarrow \langle I_1 \circ p, \mathit{Int} I_2 \rangle \\
\langle \mathit{if} \ I \ \mathit{then} \ E_1 \ \mathit{else} \ E_2 \rangle &\wedge i \neq 0 \Rightarrow \langle E_1 \rangle \\
\langle \mathit{if} \ 0 \ \mathit{then} \ E_1 \ \mathit{else} \ E_2 \rangle &\Rightarrow \langle E_2 \rangle \\
\langle \mathit{letrec} \ F \ X = E \ \mathit{in} \ E' \rangle &\Rightarrow \langle E'[f \mapsto (\mu F.\lambda X.E)] \rangle \\
\langle (\lambda X.E) \ V \rangle &\Rightarrow \langle E[V/X] \rangle \\
\langle \mu X.E \rangle &\Rightarrow \langle E[X \mapsto (\mu X.E)] \rangle \\
\langle C[c] \rangle &\Rightarrow \langle C[c'] \rangle \quad \text{if } \langle c \rangle \Rightarrow \langle c' \rangle \\
\text{where } C ::= &\ - \mid C \ \circ p \ e \mid \mathit{if} \ C \ \mathit{then} \ e_1 \ \mathit{else} \ e_2 \mid C \ e \mid v \ C
\end{align*}
$$

<caption>Fig. 3. Specifying the semantics of FUN as a set $\mathcal{A}_F$ of reachability rules schemata. op ranges over the binary function symbols and $op_{Int}$ is their denotation in $\mathcal{T}_F$</caption>

## 3.2 Semantics

Reachability logic formulae are interpreted in the presence of a first-order model $\mathcal{T}$ and a (well-sorted) valuation $\rho : \mathcal{Var} \to \mathcal{T}$ as in the case of matching logic, and also in the presence of a transition relation $\to \subseteq \mathcal{T}_{\mathit{Cfg}} \times \mathcal{T}_{\mathit{Cfg}}$ over the set of configurations $\mathcal{T}_{\mathit{Cfg}}$.

Intuitively, a reachability logic formula $\varphi \Rightarrow \varphi'$ holds if any configuration matched by $\varphi$ reaches (in one step) a configuration matched by the formula $\varphi'$. Note that the one-step requirement we work with in this article defines a satisfaction relation that is different from the ones used in the previous presentations [13, 8] of reachability logic. The satisfaction relation defined here is mainly used to specify transition systems.

**Definition 5.** Formally, the satisfaction relation $\models$ of reachability logic is defined as follows:

$$ \mathcal{T}, \to, \rho \models \varphi \Rightarrow \varphi' $$

if for any $\gamma \in \mathcal{T}_{\mathit{Cfg}}$ such that $\mathcal{T}, \gamma, \rho \models \varphi$ there exists a $\gamma' \in \mathcal{T}_{\mathit{Cfg}}$ such that $\gamma \to \gamma'$ and $\mathcal{T}, \gamma', \rho \models \varphi'$.

Note that the free variables of $\varphi$ and the free variables of $\varphi'$ are “shared” in the reachability formula, in the sense that both are interpreted by the same valuation.

**Example 5.** If

$$ \langle \mathit{if} \ (1) \ \mathit{then} \ x=x+y \ \mathit{else} \ x := 0, x \mapsto 2 \ y \mapsto 5 \rangle \Rightarrow \langle x=x+y, x \mapsto 2 \ y \mapsto 5 \rangle $$

and $\varphi \Rightarrow \varphi'$ is

$$ \langle \mathit{if} \ (I) \ \mathit{then} \ S_1 \ \mathit{else} \ S_2, \sigma \rangle \wedge I \neq \mathit{Int} \ 0 \Rightarrow \langle S_1, \sigma \rangle, $$

then we have $\mathcal{T}_I$, $\to, \rho \models \varphi \Rightarrow \varphi'$, where $\rho(I) = 1$, $\rho(S_1) = x := x+y$, $\rho(S_2) = x := 0$, and $\rho(\sigma) = x \mapsto 2 \ y \mapsto 5$.

If the valuation $\rho$ is missing, the free variables of reachability rules are interpreted universally:
**Definition 6.** Given a first-order model $\mathcal{T}$ and a transition relation $\rightarrow$, we say that the pair $(\mathcal{T}, \rightarrow)$ is a model of $\varphi \Rightarrow \varphi'$, written

$$ \mathcal{T}, \rightarrow \models \varphi \Rightarrow \varphi' $$

if, for all (well-sorted) valuations $\rho: \text{Var} \rightarrow \mathcal{T}$, we have that $\mathcal{T}, \rightarrow, \rho \models \varphi \Rightarrow \varphi'$.

The universal interpretation of the free variables is justified in the following section, but note that it is not unusual to do so: for example, the same happens with first-oder clauses, where the variables are (implicitly) universally quantified.

# 4 Language Semantics

In this section, we show that reachability formulae can be used to formally define the operational semantics of a programming language. We consider that a matching logic signature $(\mathit{Cfg}, S, \Sigma, \Pi)$ is fixed.

**Definition 7.** A $(\mathit{Cfg}, S, \Sigma, \Pi)$-programming language is a pair $(\mathcal{T}, \rightarrow)$ of a first-order model $\mathcal{T}$ of $(\mathit{Cfg}, S, \Sigma, \Pi)$ and a transition relation $\rightarrow \subseteq \mathcal{T}_{\mathit{Cfg}} \times \mathcal{T}_{\mathit{Cfg}}$.

When $(\mathit{Cfg}, S, \Sigma, \Pi)$ is understood from the context, we omit it and write programming language instead of $(\mathit{Cfg}, S, \Sigma, \Pi)$-programming language.

The matching logic signature defines the syntax of the language, the model $\mathcal{T}$ mainly defines program configurations and $\rightarrow$ defines the (one-step) transition relation between configurations. Let $A$ be a set of reachability formulae (the axioms of the language).

**Definition 8.** We say that $(\mathcal{T}, \rightarrow)$ is a model of $A$, and we write $(\mathcal{T}, \rightarrow) \models A$ if $(\mathcal{T}, \rightarrow) \models \varphi \Rightarrow \varphi'$ for every reachability formula $\varphi \Rightarrow \varphi' \in A$.

*Example 6.* If $(\mathcal{T}_I, \rightarrow_I)$ gives the semantics of IMP, then we have $(\mathcal{T}_F, \rightarrow_F) \models \mathcal{A}_I$, i.e., $(\mathcal{T}_I, \rightarrow_I)$ is a model of $\mathcal{A}_I$. Similarly, if $(\mathcal{T}_F, \rightarrow_F)$ gives the semantics of FUN, then we must have $(\mathcal{T}_F, \rightarrow_F) \models \mathcal{A}_F$, i.e., $(\mathcal{T}_F, \rightarrow_F)$ is a model of $\mathcal{A}_F$.

Therefore, the set $A$ of reachability rules are considered to be the specification (the formal semantics) of any language $(\mathcal{T}, \rightarrow)$ that is a model of the rules. In [18] it is shown that any operational semantics (small-step SOS, big-step SOS, reduction contexts, etc) can be faithfully captured by a (possibly infinite) set of reachability rules. Moreover, all such reachability rules from the semantics are pure:

**Definition 9.** A reachability formula $\varphi \Rightarrow \varphi'$ is pure if both $\varphi$ and $\varphi'$ are pure.

From here on, we assume that the formal semantics of any language is given as a (possibly infinite) set of pure reachability formulae.
# 5 Language Aggregation

We assume two signatures $(Cfg_1, S_1, \Sigma_1, \Pi_1)$ and $(Cfg_2, S_2, \Sigma_2, \Pi_2)$ for two languages $(\mathcal{T}_1, \to_{1})$ and $(\mathcal{T}_2, \to_{2})$ specified by the sets $A_1$ and $A_2$ of reachability rules.

In this section, we construct the aggregated signature $(Cfg, S, \Sigma, \Pi)$ of the aggregated language from the signature of the first language and the signature of the second language. Also, we define the aggregated language $(\mathcal{T}, \to)$ itself and show how to constructively give the aggregated axioms $A$ of the new language from the initial languages.

## 5.1 Signature Aggregation

This subsection is dedicated to showing how to construct the aggregated signature $(Cfg, S, \Sigma, \Pi)$ from the individual signature $(Cfg_1, S_1, \Sigma_1, \Pi_1)$ (of the first language) and $(Cfg_2, S_2, \Sigma_2, \Pi_2)$ (of the second language).

The most delicate part is to make sure that the sorts, function and predicate symbols “shared” between the two language are identified in the aggregated configuration, even if their names are not the same in the first and in the second language.

Therefore, we assume that there exists a first-order signature $(S_0, \Sigma_0, \Pi_0)$ that the two languages have in common. This means there exist two morphisms $h_1 : (S_0, \Sigma_0, \Pi_0) \to (S_1, \Sigma_1, \Pi_1)$ and $h_2 : (S_0, \Sigma_0, \Pi_0) \to (S_2, \Sigma_2, \Pi_2)$.

**Example 7.** For the signatures of the two languages, IMP and FUN, we have $S_0 = \{\text{Int}, \text{Id}, \text{Exp}\}$, $\Sigma_0$ that was defined on Page 1, and $\Pi_0 = \Pi_1, \Pi_2$. The morphisms $h_1$ and $h_2$ are given by the component inclusions.

The following theorem (the pushout theorem) allows us to combine the two signatures into a single signature, while identifying the objects shared between them. This result is not new, see, for example, [9].

**Theorem 1 (Pushout of Signatures).** Let $(S_1, \Sigma_1, \Pi_1)$, $(S_2, \Sigma_2, \Pi_2)$ and $(S_0, \Sigma_0, \Pi_0)$ be many-sorted FOL signatures, $h_1$ a morphism from $(S_0, \Sigma_0, \Pi_0)$ to $(S_1, \Sigma_1, \Pi_1)$ and $h_2$ a morphism from $(S_0, \Sigma_0, \Pi_0)$ to $(S_2, \Sigma_2, \Pi_2)$.

Then the diagram $(S_1, \Sigma_1, \Pi_1) \stackrel{h_1}{\leftarrow} (S_0, \Sigma_0, \Pi_0) \stackrel{h_2}{\rightarrow} (S_2, \Sigma_2, \Pi_2)$ admits a pushout, i.e., there exists a tuple $(h'_1, (S', \Sigma', \Pi'), h'_2)$ with $h'_1$ a morphism from $(S_1, \Sigma_1, \Pi_1)$ to $(S', \Sigma', \Pi')$ and $h'_2$ a morphism from $(S_2, \Sigma_2, \Pi_2)$ to $(S', \Sigma', \Pi')$ such that:

1. (commutativity) $h'_1(h_1(x)) = h'_2(h_2(x))$ for any object $x$ from the signature $(S_0, \Sigma_0, \Pi_0)$ and

2. (minimality) if there exist $(S'', \Sigma'', \Pi'')$ and morphisms $h''_1$ from $(S_1, \Sigma_1, \Pi_1)$ to $(S'', \Sigma'', \Pi'')$ and $h''_2$ from $(S_2, \Sigma_2, \Pi_2)$ to $(S'', \Sigma'', \Pi'')$ with $h''_1(h_1(x)) = h''_2(h_2(x))$ for all $x \in S_0, \cup \Sigma_0 \cup \Pi_0$, then there exists a morphism $h$ from $(S', \Sigma', \Pi')$ to $(S'', \Sigma'', \Pi'')$.
$$ \begin{array}{ccc} (S_0, \Sigma_0, \Pi_0) & \xrightarrow{h_2} & (S_2, \Sigma_2, \Pi_2) \\ \hline h_1 \downarrow & & h_2' \downarrow \\ (S_1, \Sigma_1, \Pi_1) & \xrightarrow{h_1'} & (S', \Sigma', \Pi') \end{array} $$

<caption>Fig. 4. Push-out diagram assumed throughout the paper.</caption>

Furthermore, the pushout is unique (up to isomorphisms). The push-out is summarised in Figure 4.

The first step to obtain the aggregated signature is to apply the push-out theorem in order to obtain the intermediate signature $(S', \Sigma', \Pi')$ and the two morphisms $h_1' : (S_1, \Sigma_1, \Pi_1) \to (S', \Sigma', \Pi')$ and $h_2' : (S_2, \Sigma_2, \Pi_2) \to (S', \Sigma', \Pi')$.

The first-order signature $(S', \Sigma', \Pi')$ contains all of the objects from the initial signatures (properly renamed to account for shared objects), but it does not yet have a sort for aggregated configurations. Let $\mathit{Cfg}' = h_1(\mathit{Cfg}_1)$ and $\mathit{Cfg}'_2 = h_2(\mathit{Cfg}_2)$ be the names of the sorts of configurations in the new signature.

We therefore choose a fresh sort $\mathit{Cfg}$ for aggregated configurations and we let $S = S' \uplus \{\mathit{Cfg}\}$ be the set of sorts. The signature $\Sigma$ contains, in addition to the symbols in $\Sigma'$, a pairing symbol and the respective projections. Formally,

$$ \Sigma = \Sigma' \uplus \{\langle-, -\rangle : \mathit{Cfg}'_1 \times \mathit{Cfg}'_2 \to \mathit{Cfg}, \mathit{pr}_1 : \mathit{Cfg} \to \mathit{Cfg}'_1, \mathit{pr}_2 : \mathit{Cfg} \to \mathit{Cfg}'_2\}. $$

The pairing symbol $\langle-, -\rangle$ takes as input two configurations of the initial languages and returns a configuration of the aggregated language. The projection operations $\mathit{pr}_1$ and $\mathit{pr}_2$ take an aggregated configuration and deconstruct it into the initial configurations. Finally, we let $\Pi = \Pi'$.

The signature $(\mathit{Cfg}, S, \Sigma, \Pi)$ is the aggregated signature of the language and its construction is summarised in Figure 5.

If $h : (S, \Sigma, \Pi) \to (S', \Sigma', \Pi')$ is a morphism between the two first order signatures, we extend $h$ to terms as expected: if $t \in T_s(\Sigma)$, then $h(t) \in T_{h(s)}(\Sigma')$. We also extend $h$ to transform matching logic formula in the signature $(\mathit{Cfg}, S, \Sigma, \Pi)$ to matching logic formula in the signature $(h(\mathit{Cfg}), S', \Sigma', \Pi')$ as follows:

1. $h(\varphi_1 \wedge \varphi_2) = h(\varphi_1) \wedge h(\varphi_2)$,

2. $h(\exists x.\varphi_1) = \exists x. h(\varphi_1)$,

3. $h(\neg \varphi_1) = \neg h(\varphi_1)$ and

4. $h(P(t_1, \dots, t_n)) = P(h(t_1), \dots, h(t_n))$).

Note that there is no need to have a case for computing $h(\pi)$, since a basic pattern $\pi$ is nothing but a term. Therefore $h(\pi)$ is already defined. We also extend $h$ to transform reachability formulae over the signature $(\mathit{Cfg}, S, \Sigma, \Pi)$ into reachability formulae over the signature $(h(\mathit{Cfg}), S', \Sigma', \Pi')$:

$$ h(\varphi \Rightarrow \varphi') = h(\varphi) \Rightarrow h(\varphi'). $$
<figure><img src="image_2.png" /><figcaption>Fig. 5. The aggregation of the two signatures.</figcaption></figure>

## 5.2 Model Amalgamation

In this subsection, given two models $\mathcal{T}_1$ and $\mathcal{T}_2$ for the matching logic signatures $(\mathcal{C}fg_1, S_1, \Sigma_1, \Pi_1)$ and $(\mathcal{C}fg_2, S_2, \Sigma_2, \Pi_2)$, we show how to construct a model $\mathcal{T}$ for the aggregated signature $(\mathcal{C}fg, S, \Sigma, \Pi)$ above.

In order to construct such a model, we need to make sure that the two models $\mathcal{T}_1$ and $\mathcal{T}_2$ agree on the common part of the signature. Formally, we assume that there exists a model $\mathcal{T}_0$ of the signature $(S_0, \Sigma_0, \Pi_0)$ such that $\mathcal{T}_1 \upharpoonright_{h_1} = \mathcal{T}_0 = \mathcal{T}_2 \upharpoonright_{h_2}$ (i.e. the reduct of $\mathcal{T}_1$ through $h_1$ is the same as the reduct of $\mathcal{T}_2$ through $h_2$). Figure 6 below summarizes the construction of $\mathcal{T}$.

We can combine the two languages through the model amalgamation theorem. The theorem is not new (see for example [17]). A proof can also be found in our technical report [5].

**Theorem 2 (Amalgamation).**

If $\mathcal{T}_1, \mathcal{T}_2$ and $\mathcal{T}_0$ are models of $(S_1, \Sigma_1, \Pi_1)$, $(S_2, \Sigma_2, \Pi_2)$ and respectively $(S_0, \Sigma_0, \Pi_0)$ such that $\mathcal{T}_1 \upharpoonright_{h_1} = \mathcal{T}_0 = \mathcal{T}_2 \upharpoonright_{h_2}$, there exists a unique model $\mathcal{T}'$ of $(S', \Sigma', \Pi')$ such that $\mathcal{T}' \upharpoonright_{h_2'} = \mathcal{T}_2$ and $\mathcal{T}' \upharpoonright_{h_1'} = \mathcal{T}_1$.

In order to obtain the model $\mathcal{T}$ for the aggregated signature $(\mathcal{C}fg, S, \Sigma, \Pi)$, we need to augment $\mathcal{T}'$ to interpret the $\mathcal{C}fg$ sort, the pairing symbol $\langle -, -$\rangle and the projection symbols $pr_1$ and $pr_2$. Formally, we define $\mathcal{T}$ as follows:

1. $\mathcal{T}_{\mathcal{C}fg} = \mathcal{T}'_{\mathcal{C}fg_1} \times \mathcal{T}'_{\mathcal{C}fg_2'}$,

2. $\mathcal{T}_{\langle -, - \rangle}(\gamma_1, \gamma_2) = (\gamma_1, \gamma_2)$ for any $\gamma_1 \in \mathcal{T}'_{\mathcal{C}fg_1'}$ and any $\gamma_2 \in \mathcal{T}'_{\mathcal{C}fg_2'}$,

3. $\mathcal{T}_{pr_1}((\gamma_1, \gamma_2)) = \gamma_1$ for any $(\gamma_1, \gamma_2) \in \mathcal{T}_{\mathcal{C}fg} = \mathcal{T}'_{\mathcal{C}fg_1'} \times \mathcal{T}'_{\mathcal{C}fg_2'}$,

4. $\mathcal{T}_{pr_2}((\gamma_1, \gamma_2)) = \gamma_2$ for any $(\gamma_1, \gamma_2) \in \mathcal{T}_{\mathcal{C}fg} = \mathcal{T}'_{\mathcal{C}fg_1'} \times \mathcal{T}'_{\mathcal{C}fg_2'}$, and
<figure><img src="image_3.png" /><figcaption>Fig. 6. Construction of amalgamated model</figcaption></figure>

5. $T_o = T'_o$ for any other object $o \in S \cup \Sigma \cup \Pi$.

The aggregated signature and model have the following properties:

**Lemma 1.** For any basic patterns $\pi_1 \in T_{\text{Cfg}_1}(\text{Var})$ and $\pi_2 \in T_{\text{Cfg}_2}(\text{Var})$, for any aggregated configuration $(\gamma_1, \gamma_2) \in T_{\text{Cfg}}$, for any (well-sorted) valuation $\rho$, we have that

$$T, (\gamma_1, \gamma_2), \rho \models \langle \pi_1, \pi_2 \rangle \text{ iff } T_1, \gamma_1, \rho \upharpoonright_{h'_1(S_1)} \models \pi_1 \text{ and } T_2, \gamma_2, \rho \upharpoonright_{h'_2(S_2)} \models \pi_2.$$

*Proof.* We show the direct implication first. Assume $T, (\gamma_1, \gamma_2), \rho \models \langle \pi_1, \pi_2 \rangle$. By definition, we have that $\rho(\langle \pi_1, \pi_2 \rangle) = (\gamma_1, \gamma_2)$. By the interpretation of $\langle -, -$ \rangle$ in the model $T$, we have that $\rho \upharpoonright_{h'_1(S_1)}(\pi_1) = \gamma_1$ and $\rho \upharpoonright_{h'_2(S_2)}(\pi_2) = \gamma_2$. But this is equivalent to $T_1, \gamma_1, \rho \upharpoonright_{h'_1(S_1)} \models \pi_1$ and $T_2, \gamma_2, \rho \upharpoonright_{h'_2(S_2)} \models \pi_2$, which is what we had to show.

For the reverse direction, we assume that $T_1, \gamma_1, \rho \upharpoonright_{h'_1(S_1)} \models \pi_1$ and that $T_2, \gamma_2, \rho \upharpoonright_{h'_2(S_2)} \models \pi_2$. Therefore $\rho \upharpoonright_{h'_1(S_1)}(\pi_1) = \pi_1$ and $\rho \upharpoonright_{h'_2(S_2)}(\pi_2) = \pi_2$, which implies, by the interpretation of $\langle -, -$ \rangle$ in $T$, that $\rho(\langle \pi_1, \pi_2 \rangle) = (\gamma_1, \gamma_2)$. But this is equivalent to $T, (\gamma_1, \gamma_2), \rho \models \langle \pi_1, \pi_2 \rangle$, which is what we had to prove.

## 5.3 Language Aggregation

Having shown how to construct the matching logic signature $(\text{Cfg}, S, \Sigma, \Pi)$ and model $T$ for the aggregated language, we now show how the transition relation
→ for the aggregated language is defined and how to construct the axioms A of the aggregated language from the axioms A₁ and A₂ of the initial languages.

We identify three types of language aggregations, depending on how the → transition relation is defined from →₁ and →₂. Each of the three constructions could be useful in various contexts:

1. →₁ ⊗ₐ →₂ is the asynchronous interleaving product of the two transition relations, i.e.

$$ (γ₁, γ₂) → (γ'₁, γ'₂) \text{ if } \\ γ₁ = γ'₁ \text{ and } γ₂ →₂ γ'₂ \text{ or } γ₁ →₁ γ'₁ \text{ and } γ₂ = γ'₂, $$

2. →₁ ⊗ₚ →₂ is the parallel product of the two transition relations, i.e.

$$ (γ₁, γ₂) → (γ'₁, γ'₂) \text{ if } \\ γ₁ →₁ γ'₁ \text{ and } γ₂ →₂ γ'₂, $$

3. finally, →₁ ⊗ →₂ = (→₁ ⊗ₐ →₂) ∪ (→₁ ⊗ₚ →₂) is the (general) product of →₁ and →₂.

The asynchronous product with interleaving semantics means that in one step of the aggregated language, either the left-hand side takes a step (in the first language) or the right-hand side takes a step (in the second language). The parallel product forces both sides to take steps simultaneously. The (general) product requires at least one side to take a step and it allows (but not requires) the other side to do the same.

## 5.4 Constructing the Axioms for the Three Products

We next show how to construct a set of axioms A for the aggregated language from the set of axioms A₁ and A₂ of the initial languages, depending on which of the three constructions is chosen for the aggregated transition relation. The main result is that, for each of the three constructions, the transition relation is a model of the aggregated axioms. This means that we can construct the formal semantics of the aggregated language directly from the formal semantics of the initial languages.

Let A₁ be a set of pure reachability rules over the signature (*Cfg*₁, *S*₁, *Σ*₁, *Π*₁) that capture the semantics of the first language (the axioms of the first language): *T*₁, →₁ |= A₁. Let A₂ be a set of pure reachability rules over the signature (*Cfg*₂, *S*₂, *Σ*₂, *Π*₂) that capture the semantics of the second language (the axioms of the second language): *T*₂, →₂ |= A₂.

In order to define the axioms for the aggregated language, we need a way to transform reachability formulae from the two initial signatures into reachability formulae of the target signature. This is performed with the help of the following function:
**Definition 10.** We define the function $\iota_x^i$ (for $i \in \{1, 2\}$ and $x$ a distinguished variable in Var of sort $\text{Config}_i$) that takes as input a matching logic formula over $(\text{Config}_1, S_1, \Sigma_1, \Pi_1)$ (respectively $(\text{Config}_2, S_2, \Sigma_2, \Pi_2)$) and changes all basic patterns $\pi$ into $\langle\pi, x\rangle$ (respectively $\langle x, \pi\rangle$) in order to obtain a formula over $(\text{Config}, S, \Sigma, \Pi)$:

1. $\iota_x^1(\pi) = \langle h'_1(\pi), x \rangle$

2. $\iota_x^2(\pi) = \langle x, h'_2(\pi) \rangle$

3. $\iota_x^i(\varphi_1 \wedge \varphi_2) = \iota_x^i(\varphi_1) \wedge \iota_x^i(\varphi_2)$,

4. $\iota_x^i(\exists y.\varphi_1) = \exists y.\iota_x^i(\varphi_1)$,

5. $\iota_x^i(\neg\varphi_1) = \neg\iota_x^i(\varphi_1)$ and

6. $\iota_x^i(P(t_1, \dots, t_n)) = P(h'_i(t_1), \dots, h'_i(t_n))$.

**Example 8.** If $\varphi_1$ is the matching formula $\langle \mathbf{while}(E) S, \sigma \rangle \wedge \mathbf{eval}(\sigma, E) \neq \mathbf{Int} 0$ and $\varphi_2$ is $\langle \mathbf{letrec} \ f \ x = \mathbf{if} \ (I) \ \mathbf{then} \ E_1 \ \mathbf{else} \ E_2 \ \mathbf{in} \ f(x) \rangle \wedge I < \mathbf{Int} 5$, then $\iota_x^i(\varphi_1)$ is $\langle \langle \mathbf{while}(E) S, \sigma \rangle, x \rangle \wedge \mathbf{eval}(\sigma, E) \neq \mathbf{Int} 0$ and $\iota_x^i(\varphi_2)$ is the aggregate formula $\langle x, \langle \mathbf{letrec} \ f \ x = \mathbf{if} \ (I) \ \mathbf{then} \ E_1 \ \mathbf{else} \ E_2 \ \mathbf{in} \ f(x) \rangle \rangle \wedge I < \mathbf{Int} 5$.

Next, we show the link, in terms of matching logic formulae, between the aggregated model and the initial model.

**Lemma 2.** Let $\varphi_1$ and $\varphi_2$ be matching logic formulae over $(\text{Config}_1, S_1, \Sigma_1, \Pi_1)$ and respectively $(\text{Config}_2, S_2, \Sigma_2, \Pi_2)$. For any aggregated configuration $(\gamma_1, \gamma_2) \in \mathcal{T}_{\text{Config}}$, for any (well-sorted) valuation $\rho$, if $x$ is a fresh variable, we have that

$$ \mathcal{T}, (\gamma_1, \gamma_2), \rho \models \iota_x^i(\varphi_i) \text{ iff } \mathcal{T}_i, \gamma_i, \rho \upharpoonright_{\mathcal{T}_i(S_i)} \models \varphi_i. $$

*Proof.* For simplicity, we assume that $i=1$ (since the case with $i=2$ is analogous). We prove the lemma by structural induction on $\varphi_1$. We only show the case of negation, the other cases being similar:

- if $\varphi_1 = \neg\varphi'_1$, then

$$ \mathcal{T}, (\gamma_1, \gamma_2), \rho \models \iota_x^1(\varphi_1) \text{ iff} $$

$$ \mathcal{T}, (\gamma_1, \gamma_2), \rho \models \neg\iota_x^1(\varphi'_1) \text{ iff} $$

$$ \mathcal{T}, (\gamma_1, \gamma_2), \rho \models \iota_x^1(\varphi'_1) \text{ iff} $$

$$ \mathcal{T}_1, \gamma_1, \rho \upharpoonright_{\mathcal{T}_1(S_1)} \models \varphi'_1 \text{ iff} $$

$$ \mathcal{T}_1, \gamma_1, \rho \upharpoonright_{\mathcal{T}_1(S_1)} \models \neg\varphi'_1 $$

**Lemma 3.** For any pure matching logic formulae $\varphi_1$ over $(\text{Config}_1, S_1, \Sigma_1, \Pi_1)$ and $\varphi_2$ over $(\text{Config}_2, S_2, \Sigma_2, \Pi_2)$, for any aggregated configuration $(\gamma_1, \gamma_2) \in \mathcal{T}_{\text{Config}}$, for any (well-sorted) valuation $\rho$, if $x$ is a fresh variable, we have that

$$ \mathcal{T}, (\gamma_1, \gamma_2), \rho \models \iota_x^i(\varphi_i) \text{ iff } \mathcal{T}_i, \gamma_i, \rho \upharpoonright_{\mathcal{T}_i(S_i)} \models \varphi_i \text{ and } \rho(x) = \gamma_{3-i}. $$

*Proof.* For simplicity, we assume that $i=1$ (since the case with $i=2$ is analogous). We prove the lemma by structural induction on $\varphi_1$, showing that

$$ \mathcal{T}, (\gamma_1, \gamma_2), \rho \models \iota_x^1(\varphi_1) \text{ iff } \mathcal{T}_1, \gamma_1, \rho \upharpoonright_{\mathcal{T}_1(S_1)} \models \varphi_1 \text{ and } \rho(x) = \gamma_2. $$

We distinguish the following cases:
1. if $\varphi_1 = \pi$, then $\iota_x^1(\varphi_1) = (h'_1(\pi), x)$. We have that

$$
\begin{align*}
\mathcal{T}, (\gamma_1, \gamma_2), \rho \models \iota_x^1(\varphi_1) &\quad \text{iff} \\
\mathcal{T}, (\gamma_1, \gamma_2), \rho \models (h'_1(\pi), x) &\quad \text{iff} \\
(\gamma_1, \gamma_2) = \rho(h'_1(\pi), x) &\quad \text{iff} \\
\gamma_1 = \rho(h'_1(\pi)) \text{ and } \gamma_2 = \rho(x) &\quad \text{iff} \\
\gamma_1 = \rho^{\upharpoonright h'_1(S_1)}(\pi) \text{ and } \gamma_2 = \rho(x) &\quad \text{iff} \\
\mathcal{T}_1, \gamma_1, \rho^{\upharpoonright h'_1(S_1)} \models \pi \text{ and } \gamma_2 = \rho(x). &\quad \text{iff}
\end{align*}
$$

2. if $\varphi_1 = \exists y.\varphi'_1$ for a variable $y$ of sort $s$ (with $y \neq x$ since $x$ is a fresh variable) then $\iota_x^1(\varphi_1) = \exists y.\iota_x^1(\varphi'_1)$. We have that

$$
\begin{align*}
\mathcal{T}, (\gamma_1, \gamma_2), \rho \models \iota_x^1(\varphi_1) &\qquad \text{iff} \\
\mathcal{T}, (\gamma_1, \gamma_2), \rho \models \exists y.\iota_x^1(\varphi'_1) &\qquad \text{iff} \\
\text{there is } u \in \mathcal{T}_{1s} \text{ s.t. } \mathcal{T}, (\gamma_1, \gamma_2), \rho[y \mapsto u] \models \iota_x^1(\varphi'_1) &\qquad \text{iff} \\
\text{there is } u \in \mathcal{T}_{1s} \text{ s.t. } \mathcal{T}_1, \gamma_1, \rho[y \mapsto u]^{\upharpoonright h'_1(S_1)} \models \varphi'_1 \text{ and } \gamma_2 = \rho[y \mapsto u](x) &\qquad \text{iff} \\
\mathcal{T}_1, \gamma_1, \rho^{\upharpoonright h'_1(S_1)} \models \exists y.\varphi'_1 \text{ and } \gamma_2 = \rho(x) &\qquad \text{iff} \\
\mathcal{T}_1, \gamma_1, \rho^{\upharpoonright h'_1(S_1)} \models \varphi_1 \text{ and } \gamma_2 = \rho(x). &\qquad \text{iff}
\end{align*}
$$

3. if $\varphi_1 = \varphi'_1 \wedge \varphi'_2$ for a pure formula $\varphi'_1$ and a patternless formula $\varphi'_2$, then
$\iota_x^1(\varphi_1) = \iota_x^1(\varphi'_1) \wedge \iota_x^1(\varphi'_2)$. We have that

$$
\begin{align*}
\mathcal{T}, (\gamma_1, \gamma_2), \rho \models \iota_x^1(\varphi_1) &\qquad \text{iff} \\
\mathcal{T}, (\gamma_1, \gamma_2), \rho \models \iota_x^1(\varphi'_1) \wedge \iota_x^1(\varphi'_2) &\qquad \text{iff} \\
\mathcal{T}, (\gamma_1, \gamma_2), \rho \models \iota_x^1(\varphi'_1) \text{ and } \mathcal{T}, (\gamma_1, \gamma_2), \rho \models \iota_x^1(\varphi'_2) &\qquad \text{iff} \\
\mathcal{T}_1, \gamma_1, \rho^{\upharpoonright h'_1(S_1)} \models \varphi'_1 \text{ and } \rho(x) = \gamma_2 \text{ and } \mathcal{T}_1, \gamma_1, \rho^{\upharpoonright h'_1(S_1)} \models \varphi'_2 &\qquad \text{iff} \\
\mathcal{T}_1, \gamma_1, \rho^{\upharpoonright h'_1(S_1)} \models \varphi'_1 \wedge \varphi'_2 \text{ and } \rho(x) = \gamma_2 &\qquad \text{iff} \\
\mathcal{T}_1, \gamma_1, \rho^{\upharpoonright h'_1(S_1)} \models \varphi_1 \text{ and } \rho(x) = \gamma_2. &\qquad \text{iff}
\end{align*}
$$

In the following subsections, we define three types of aggregations for these
sets of axioms, for each type of language aggregation.

**The Axioms for the Asynchronous Product with Interleaving Semantics** We let

$$
A_1 \otimes_a A_2 = \{ \iota_y^1(\varphi_1) \Rightarrow \iota_y^1(\varphi'_1) \mid \varphi_1 \Rightarrow \varphi'_1 \in A_1 \} \cup \\
\{ \iota_x^2(\varphi_2) \Rightarrow \iota_x^2(\varphi'_2) \mid \varphi_2 \Rightarrow \varphi'_2 \in A_2 \}
$$

where $x$ is a fresh variable of sort $\mathit{Cfg}'_1$ and $y$ is a fresh variable of sort $\mathit{Cfg}'_2$.
The intuition is that $x$ captures any left-hand side and allow the right-hand to
take a step while $y$ captures any right-hand side and allow the left-hand side to
take a step. We show formally that $A_1 \otimes_a A_2$ is indeed a formal specification of
the language $(\mathcal{T}, \rightarrow_1 \otimes_a \rightarrow_2)$:

**Theorem 3 (correctness for asynchronous product).**

Let $A = A_1 \otimes_a A_2$ and $\longrightarrow = \longrightarrow_1 \otimes_a \longrightarrow_2$. We have that

$$
(\mathcal{T}, \rightarrow) \models A.
$$
*Proof.* We have to show that $(\mathcal{T}, \rightarrow) \models A$. By definition, $(\mathcal{T}, \rightarrow) \models A$ if, for any reachability rule $\varphi \Rightarrow \varphi' \in A$, we have that $(\mathcal{T}, \rightarrow) \models \varphi \Rightarrow \varphi'$. Let $\varphi \Rightarrow \varphi' \in A$ be an arbitrary reachability rule. We show that $(\mathcal{T}, \rightarrow) \models \varphi \Rightarrow \varphi'$.

As $\varphi \Rightarrow \varphi' \in A = A_1 \otimes_a A_2$, it follows that $\varphi \Rightarrow \varphi' = \iota_y^1(\varphi_1) \Rightarrow \iota_y^1(\varphi_1')$ for some $\varphi_1 \Rightarrow \varphi_1' \in A_1$ and a fresh variable $y$ or that $\varphi \Rightarrow \varphi' = \iota_x^2(\varphi_2) \Rightarrow \iota_x^2(\varphi_2')$ for some $\varphi_2 \Rightarrow \varphi_2' \in A_2$ and a fresh variable $x$. Since the two cases are analogous, we deal only with the first and we assume therefore that $\varphi \Rightarrow \varphi' = \iota_y^1(\varphi_1) \Rightarrow \iota_y^1(\varphi_1')$ for some $\varphi_1 \Rightarrow \varphi_1' \in A_1$ and a fresh variable $y$. Therefore it remains to show that $(\mathcal{T}, \rightarrow) \models \iota_y^1(\varphi_1) \Rightarrow \iota_y^1(\varphi_1')$.

Let $\rho$ be an arbitrary valuation. Let $(\gamma_1, \gamma_2) \in \mathcal{T}_{\text{Cfg}}$ be an arbitrary configuration such that $\mathcal{T}, (\gamma_1, \gamma_2), \rho \models \iota_y^1(\varphi_1)$. By Lemma 3, we have $\mathcal{T}_1, \gamma_1, \rho \upharpoonright_{\mathcal{T}_1(S_1)} \models \varphi_1$ and $\rho(x) = \gamma_2$. Given that $\varphi_1 \Rightarrow \varphi_1' \in A_1$ and $\mathcal{T}_1, \rightarrow_1 \models A_1$, there exists $\gamma'_1 \in \mathcal{T}_{\text{Cfg}}$ such that $\gamma_1 \rightarrow_1 \gamma'_1$ and $\mathcal{T}_1, \gamma'_1, \rho \upharpoonright_{\mathcal{T}_1(S_1)} \models \varphi'_1$. By Lemma 3, we have that $\mathcal{T}, (\gamma'_1, \gamma_2), \rho \models \iota_y^1(\varphi'_1)$. But, by the definition of $\rightarrow$ ($\rightarrow = \rightarrow_1 \otimes_a \rightarrow_2$), we also have that $(\gamma_1, \gamma_2) \rightarrow (\gamma'_1, \gamma_2)$.

We have shown that for an arbitrary valuation $\rho$ and for an arbitrary configuration $(\gamma_1, \gamma_2) \in \mathcal{T}_{\text{Cfg}}$ such that $\mathcal{T}, (\gamma_1, \gamma_2), \rho \models \iota_y^1(\varphi_1)$, there exists a configuration $(\gamma'_1, \gamma_2)$ such that $(\gamma_1, \gamma_2) \rightarrow (\gamma'_1, \gamma_2)$ and $\mathcal{T}, (\gamma'_1, \gamma_2), \rho \models \iota_y^1(\varphi'_1)$. But this means that $(\mathcal{T}, \rightarrow) \models \iota_y^1(\varphi_1) \Rightarrow \iota_y^1(\varphi'_1)$, which is what we had to show.

## The Axioms for the Parallel Product

$$A_1 \otimes_p A_2 = \{ \iota_y^1(\varphi_1) \wedge \iota_x^2(\varphi_2) \Rightarrow \exists x. \exists y. (\iota_y^1(\varphi'_1) \wedge \iota_x^2(\varphi'_2)) \mid \\ \qquad \varphi_1 \Rightarrow \varphi'_1 \in A_1, \varphi_2 \Rightarrow \varphi'_2 \in A_2 \}$$

where $x$ is a fresh variable of sort $\text{Cfg}'_1$ and $y$ is a fresh variable of sort $\text{Cfg}'_2$. The intuition is that $x$ captures any left-hand side and $y$ captures any right-hand side. We show formally that $A_1 \otimes_p A_2$ is indeed a formal specification of the language $(\mathcal{T}, \rightarrow_1 \otimes_p \rightarrow_2)$:

## Theorem 4 (correctness for parallel product).

Let $A = A_1 \otimes_p A_2$ and $\rightarrow = \rightarrow_1 \otimes_p \rightarrow_2$. We have that

$$(\mathcal{T}, \rightarrow) \models A.$$

*Proof.* We have to show that $(\mathcal{T}, \rightarrow) \models A$. By definition, $(\mathcal{T}, \rightarrow) \models A$ if, for any reachability rule $\varphi \Rightarrow \varphi' \in A$, we have that $(\mathcal{T}, \rightarrow) \models \varphi \Rightarrow \varphi'$. Let $\varphi \Rightarrow \varphi' \in A$ be an arbitrary reachability rule. We show that $(\mathcal{T}, \rightarrow) \models \varphi \Rightarrow \varphi'$.

As $\varphi \Rightarrow \varphi' \in A = A_1 \otimes_p A_2$, it follows that there exist $\varphi_1 \Rightarrow \varphi_1 \in A_1$, $\varphi_2 \Rightarrow \varphi_2' \in A_2$, fresh variables $x$ and $y$ such that $\varphi \Rightarrow \varphi' = \iota_y^1(\varphi_1) \wedge \iota_x^2(\varphi_2) \Rightarrow \iota_y^1(\varphi'_1) \wedge \iota_x^2(\varphi'_2)$.

Let $\rho$ be an arbitrary valuation. Let $(\gamma_1, \gamma_2)$ be an arbitrary configuration such that $\mathcal{T}, (\gamma_1, \gamma_2), \rho \models \iota_y^1(\varphi_1) \wedge \iota_x^2(\varphi_2)$. By the semantics of $\wedge$, we have that $\mathcal{T}, (\gamma_1, \gamma_2), \rho \models \iota_y^1(\varphi_1)$ and $\mathcal{T}, (\gamma_1, \gamma_2), \rho \models \iota_x^2(\varphi_2)$. By Lemma 3 it follows that $\mathcal{T}_1, \gamma_1, \rho \upharpoonright_{\mathcal{T}_1(S_1)} \models \varphi_1, \rho(y) = \gamma_2, \mathcal{T}_2, \gamma_2, \rho \upharpoonright_{\mathcal{T}_2(S_2)} \models \varphi_2$ and $\rho(x) = \gamma_1$.
Because $\mathcal{T}_1, \gamma_1, \rho \upharpoonright_{h'_1(S_1)} \models \varphi_1, \varphi_1 \Rightarrow \varphi'_1 \in A_1$ and $\mathcal{T}_1, \dashrightarrow_1 \models A_1$, we obtain that there exists $\gamma'_1$ such that $\gamma_1 \dashrightarrow_1 \gamma'_1$ and $\mathcal{T}_1, \gamma'_1, \rho \upharpoonright_{h'_1(S_1)} \models \varphi'_1$. Similarly, there exists $\gamma'_2$ such that $\gamma_2 \dashrightarrow_2 \gamma'_2$ and $\mathcal{T}_2, \gamma'_2, \rho \upharpoonright_{h'_2(S_2)} \models \varphi'_2$.

By Lemma 3, it follows that $\mathcal{T}, (\gamma'_1, \gamma'_2), \rho[x \mapsto \gamma_1][y \mapsto \gamma_2] \models \iota_y^1(\varphi'_1)$ and $\mathcal{T}, (\gamma'_1, \gamma'_2), \rho[x \mapsto \gamma_1][y \mapsto \gamma_2] \models \iota_y^2(\varphi'_2)$, which implies that $\mathcal{T}, (\gamma'_1, \gamma'_2), \rho \models \exists x. \exists y. (\iota_y^1(\varphi'_1) \land \iota_y^2(\varphi'_2))$. By the definition of $\dashrightarrow$, we also have $(\gamma_1, \gamma_2) \dashrightarrow (\gamma'_1, \gamma'_2)$.

We have started with an arbitrary valuation $\rho$ and an arbitrary configuration $(\gamma_1, \gamma_2)$ such that $\mathcal{T}, (\gamma_1, \gamma_2), \rho \models \iota_y^1(\varphi_1) \land \iota_x^2(\varphi_2)$ and we have shown that there exists a configuration $(\gamma'_1, \gamma'_2)$ such that $(\gamma_1, \gamma_2) \dashrightarrow (\gamma'_1, \gamma'_2)$ and $\mathcal{T}, (\gamma'_1, \gamma'_2), \rho \models \exists x. \exists y. \iota_y^1(\varphi'_1) \land \iota_y^2(\varphi'_2)$. Therefore $(\mathcal{T}, \dashrightarrow) \models \iota_y^1(\varphi_1) \land \iota_x^2(\varphi_2) \Rightarrow \exists x. \exists y. \iota_y^1(\varphi'_1) \land \iota_y^2(\varphi'_2)$, which is what we had to show.

**The Axioms for the General Product** For the general product, which allows for both interleaving and parallel steps, we define

$$A_1 \otimes A_2 = A_1 \otimes_a A_2 \cup A_1 \otimes_p A_2.$$

The correctness result for the general product follows quickly from Theorem 3 and Theorem 4.

**Theorem 5 (correctness for the general product).**

Let $A = A_1 \otimes A_2$ and $\dashrightarrow = \dashrightarrow_1 \otimes \dashrightarrow_2$. We have that

$$(\mathcal{T}, \dashrightarrow) \models A.$$

*Proof.* Let $\varphi \Rightarrow \varphi' \in A$ be an arbitrary rule. We show that $(\mathcal{T}, \dashrightarrow) \models \varphi \Rightarrow \varphi'$. Let $\gamma \in \mathcal{T}_{Cfg}$ be an arbitrary configuration and let $\rho$ be an arbitrary valuation such that $\mathcal{T}, \gamma, \rho \models \varphi$.

We distinguish two cases:

1. if $\varphi \Rightarrow \varphi' \in A_1 \otimes_a A_2$, then, by Theorem 3, there exists $\gamma'$ such that $\gamma(\dashrightarrow_1 \otimes_a \dashrightarrow_2)\gamma'$ and $\mathcal{T}, \gamma', \rho \models \varphi'$. But, by definition, $\dashrightarrow_1 \otimes_a \dashrightarrow_2 \subseteq \dashrightarrow$. Therefore there exists $\gamma'$ such that $\gamma \dashrightarrow \gamma'$ and $\mathcal{T}, \gamma', \rho \models \varphi'$, which implies $(\mathcal{T}, \dashrightarrow) \models \varphi \Rightarrow \varphi'$.

2. if $\varphi \Rightarrow \varphi' \in A_1 \otimes_p A_2$, then, by Theorem 4, there exists $\gamma'$ such that $\gamma(\dashrightarrow_1 \otimes_p \dashrightarrow_2)\gamma'$ and $\mathcal{T}, \gamma', \rho \models \varphi'$. But, by definition, $\dashrightarrow_1 \otimes_p \dashrightarrow_2 \subseteq \dashrightarrow$. Therefore there exists $\gamma'$ such that $\gamma \dashrightarrow \gamma'$ and $\mathcal{T}, \gamma', \rho \models \varphi'$, which implies $(\mathcal{T}, \dashrightarrow) \models \varphi \Rightarrow \varphi'$.

# 6 Conclusion and Future Work

In this paper we have shown that if two programming languages are defined using reachability logic axioms and matching-logic based semantics, then we can effectively construct products of the two languages, such that a pair of programs belonging to the product can be executed asynchronously with interleaving, in
parallel (synchronised), or a combination of the two. The construction can be
automated in definitional frameworks like K [15].

A programming language definition consists of a signature and a semantics.
In our approach, the signature is a many-sorted first-order signature, that in-
cludes both the syntax of the programming languages and the data structures
required by the semantics. The category of the many sorted first-order signatures
has colimits, in particular pushouts. Moreover, this category has the amalgama-
tion property [9, 16]. The semantics of the programming languages is given by
transitions systems. The category of the transition systems has also several nice
constructions [19]. We combine these constructions in order to get the defini-
tion for aggregated languages. The approach is flexible enough to allow various
aggregations. The semantics of a programming language can be specified with
(one-step) reachability logic formulae. We show that the specification of the
aggregated language can be obtained from the specifications of the components.

We used many-sorted first-order signatures in order to make the presenta-
tion easier to follow. However, the syntax of programming languages is usually
given by BNF rules, which correspond to order-sorted first-order signatures. Un-
fortunately, order-sorted first-order logic does not have pushouts of signatures
and the amalgamation property. There are several approaches dealing with this
issue, see, e.g., [17, 1, 10]. It is challenging to see which one of these is the best
candidate for programming languages products and this will be investigated in
the future. It is also interesting to see if the formalisation of the matching logic
and reachability logic as institutions [2, 3] could help.

An interesting observation can be made for the case where $\rightarrow = \rightarrow_1 \otimes \rightarrow_2$.
The transition system $(\mathcal{T}, \rightarrow)$ is a product in the category of the transitions
systems [19]. So, the syntax of the aggregation of the language is defined by a
pushout (which is a shared sum) and the semantics by a product.

Language aggregation has uses in proving equivalence properties [7, 6]. We
intend to explore its use in proving other kinds of relations and in compiler
verification.

References

1. M. Alpuente, S. Escobar, J. Meseguer, and P. Ojeda. Order-Sorted Generalization. *Electr. Notes Theor. Comput. Sci.*, 246:27–38, 2009.

2. C. E. Chiriţă. An Institutional Foundation for the K Semantic Framework. Master's thesis, University of Bucharest, 2014.

3. C. E. Chiriţă and T. F. Şerbănuţă. An Institutional Foundation for the K Semantic Framework. In *this volume*.

4. M. Clavel, F. Durán, S. Eker, P. Lincoln, N. Martí-Oliet, J. Meseguer, and C. L. Talcott. *All About Maude, A High-Performance Logical Framework*, volume 4350 of *Lecture Notes in Computer Science*. Springer, 2007.

5. Ş. Ciobâcă, D. Lucanu, V. Rusu, and G. Roşu. A Language-Independent Proof System for Mutual Program Equivalence. Technical Report 14-01, Al. I. Cuza Univ., 2014.
6. Ştefan Ciobăcă. Reducing Partial Equivalence to Partial Correctness. In *Symbolic and Numeric Algorithms for Scientific Computing (SYNASC), 2014 16th International Symposium on*, pages 164–171, Sept 2014.

7. Ştefan Ciobăcă, D. Lucanu, V. Rusu, and G. Roşu. A Language-Independent Proof System for Mutual Program Equivalence. In *ICFEM 2014, Luxembourg, Luxembourg, November 3-5, 2014. Proceedings*, pages 75–90, 2014.

8. A. Ştefanescu, Ştefan Ciobăcă, R. Mereuta, B. M. Moore, T. Serbanuta, and G. Roşu. All-Path Reachability Logic. In *RTA-TLCA 2014, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings*, pages 425–440, 2014.

9. R. Diaconescu. *Institution-independent Model Theory*. Birkhauser Basel, 2008.

10. A. E. Haxthausen and F. Nickl. Pushouts of Order-Sorted Algebraic Specifications. In *AMAST*, pages 132–147, 1996.

11. G. Roşu. Matching Logic: A Logic for Structural Reasoning. Technical Report http://hdl.handle.net/2142/47004, University of Illinois, Jan 2014.

12. G. Roşu. Matching Logic (invited talk). In *26th International Conference on Rewriting Techniques and Applications, RTA 2015, 29 June - 1 July, Warsaw, Poland*, 2015. to appear.

13. G. Roşu, A. Ştefanescu, Ştefan Ciobăcă, and B. M. Moore. One-Path Reachability Logic. In *28th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2013, New Orleans, LA, USA, June 25-28, 2013*, pages 358–367, 2013.

14. G. Roşu, C. Ellison, and W. Schulte. Matching Logic: An Alternative to Hoare/Floyd Logic. In *AMAST, LNCS 6486*, pages 142–162, 2010.

15. G. Roşu and T.-F. Şerbănuţă. An overview of the K semantic framework. *J. Log. Algebr. Program.*, 79(6):397–434, 2010.

16. D. Sannella and A. Tarlecki. *Foundations of Algebraic Specification and Formal Software Development*. Monographs in Theoretical Computer Science. An EATCS Series. Springer, 2012.

17. L. Schröder, T. Mossakowski, A. Tarlecki, P. Hoffman, and B. Klin. Amalgamation in the semantics of CASL. *Theoretical Computer Science*, 331(1):215–247, 2005.

18. T.-F. Şerbănuţă, G. Roşu, and J. Meseguer. A rewriting logic approach to operational semantics. *Inf. Comput.*, 207(2):305–340, 2009.

19. G. Winskel and M. Nielsen. Categories in Concurrency. In *Semantics and Logics of Computation, Publications of the Newton Institute*, pages 299–354. Cambridge University Press, 1997.