# Bisimilarity of Open Terms in Stream GSOS

Filippo Bonchi, Matias David Lee, Jurriaan Rot

► To cite this version:

Filippo Bonchi, Matias David Lee, Jurriaan Rot. Bisimilarity of Open Terms in Stream GSOS. 7th International Conference on Fundamentals of Software Engineering (FSEN), Apr 2017, Teheran, Iran. pp.35-50, 10.1007/978-3-319-68972-2_3. hal-01760851

HAL Id: hal-01760851

https://inria.hal.science/hal-01760851

Submitted on 6 Apr 2018

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.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# Bisimilarity of Open Terms in Stream GSOS*

Filippo Bonchi¹, Matias David Lee¹ and Jurriaan Rot²

¹ Univ Lyon, ENS de Lyon, CNRS, UCB Lyon 1, LIP, France
[filippo.bonchi,matias-david.lee]@ens-lyon.fr

² Radboud University, Nijmegen, The Netherlands
jrot@cs.ru.nl

**Abstract.** Stream GSOS is a specification format for operations and calculi on infinite sequences. The notion of bisimilarity provides a canonical proof technique for equivalence of closed terms in such specifications. In this paper, we focus on *open terms*, which may contain variables, and which are equivalent whenever they denote the same stream for every possible instantiation of the variables. Our main contribution is to capture equivalence of open terms as bisimilarity on certain Mealy machines, providing a concrete proof technique. Moreover, we introduce an enhancement of this technique, called bisimulation up-to substitutions, and show how to combine it with other up-to techniques to obtain a powerful method for proving equivalence of open terms.

## 1 Introduction

Structural operational semantics (SOS) can be considered the de facto standard to define programming languages and process calculi. The SOS framework relies on defining a *specification* consisting of a set of operation symbols, a set of labels or actions and a set of inference rules. The inference rules describe the behaviour of each operation, typically depending on the behaviour of the parameters. The semantics is then defined in terms of a labelled transition system over (*closed*) terms constructed from the operation symbols. *Bisimilarity* of closed terms ($\sim$) provides a canonical notion of behavioural equivalence.

It is also interesting to study equivalence of *open terms*, for instance to express properties of program constructors, like the commutativity of a non-deterministic choice operator. The latter can be formalised as the equation $\mathcal{X} + \mathcal{Y} = \mathcal{Y} + \mathcal{X}$, where the left and right hand sides are terms with variables $\mathcal{X}, \mathcal{Y}$. Equivalence of open terms ($\sim_o$) is usually based on $\sim$: for all open terms $t_1, t_2$

$$t_1 \sim_o t_2 \text{ iff for all closed substitutions } \phi, \phi(t_1) \sim \phi(t_2). \quad (1)$$

The main problem of such a definition is the quantification over all substitutions: one would like to have an alternative characterisation, possibly amenable to the

<footnote>* The research leading to these results has received funding from the European Research Council (FP7/2007-2013, grant agreement nr. 320571; as well as from the LABEX MILYON (ANR-10-LABX-0070, ANR-11-IDEX-0007), the project PACE (ANR-12IS02001) and the project REPAS (ANR-16-CE25-0011).</footnote>
coinduction proof principle. This issue has been investigated in several works, like [7, 15, 3, 1, 11, 13, 20].

<figure><img src="image_2.png" /><figcaption>**Figure 1.** A stream GSOS specification (a) is transformed first into a monadic specification (b), then in a Mealy specification (c) and finally in a specification for open terms (d). In these rules, $n$ and $m$ range over real numbers, $b$ over an arbitrary set $B$, $\mathcal{X}$ over variables and $\zeta$ over substitutions of variables into reals.</figcaption></figure>

In this paper, we continue this line of research, focusing on the simpler setting of *streams*, which are infinite sequences over a fixed data type. More precisely, we consider stream languages specified in the *stream GSOS format* [10], a syntactic rule format enforcing several interesting properties. We show how to transform a stream specification into a *Mealy machine* specification that defines the operational semantics of open terms. Moreover, a notion of bisimulation – arising in a canonical way from the theory of coalgebras [16] – exactly characterises $\sim_o$ as defined in (1).

Our approach can be illustrated by taking as running example the fragment of the stream calculus [18] presented in Figure 1(a). The first step is to transform a stream GSOS specification (Section 2) into a *monadic* one (Section 3). In this variant of GSOS specifications, no variable in the source of the conclusion appears in the target of the conclusion. For example, in the stream specification in Figure 1(a), the rule associated to $\otimes$ is not monadic. The corresponding monadic specification is illustrated in Figure 1(b). Notice this process requires the inclusion of a family of prefix operators (on the right of Figure 1(b)) that satisfy the imposed restriction.

The second step – based on [8] – is to compute the *pointwise extension* of the obtained specification (Section 4). Intuitively, we transform a specification of streams with outputs in a set $A$ into a specification of Mealy machines with inputs in an arbitrary set $B$ and outputs in $A$, by replacing each transition $\xrightarrow{a}$ (for $a \in A$) with a transition $\xrightarrow{b|a}$ for each input $b \in B$. See Figure 1(c).
In the last step (Section 5), we fix $B = \mathcal{V} \to A$, the set of functions assigning
outputs values in $A$ to variables in $\mathcal{V}$. To get the semantics of open terms, it
only remains to specify the behaviours of variables in $\mathcal{V}$. This is done with the
leftmost rule in Figure 1(d).

As a result of this process, we obtain a notion of bisimilarity over open terms,
which coincides with behavioural equivalence of all closed instances, and provides
a concrete proof technique for equivalence of open terms. By relating open terms
rather than all its possible instances, this novel technique often enables to use
finite relations, while standard bisimulation techniques usually require relations
of infinite size on closed terms. In Section 6 we further enhance this novel proof
technique by studying bisimulation up-to [14]. We combine known up-to tech-
niques with a novel one which we call bisimulation up-to substitutions.

## 2 Preliminaries

We define the two basic models that form the focus of this paper: stream systems, that generate infinite sequences (streams), and Mealy machines, that generate output streams given input streams.

**Definition 2.1.** A stream system with outputs in a set $A$ is a pair $(X, \langle o, d \rangle)$
where $X$ is a set of states and $\langle o, d \rangle: X \to A \times X$ is a function, which maps a
state $x \in X$ to both an output value $o(x) \in A$ and to a next state $d(x) \in X$.
We write $x \xrightarrow{a} y$ whenever $o(x) = a$ and $d(x) = y$.

**Definition 2.2.** A Mealy machine with inputs in a set $B$ and outputs in a set $A$ is a pair $(X, m)$ where $X$ is a set of states and $m: X \to (A \times X)^B$ is a function assigning to each $x \in X$ a map $m(x) = \langle o_x, d_x \rangle: B \to A \times X$. For all inputs $b \in B$, $o_x(b) \in A$ represents an output and $d_x(b) \in X$ a next state. We write $x \xrightarrow{b|a} y$ whenever $o_x(b) = a$ and $d_x(b) = y$.

We recall the notion of bisimulation for both models.

**Definition 2.3.** Let $(X, \langle o, d \rangle)$ be a stream system. A relation $\mathcal{R} \subseteq X \times X$ is a bisimulation if for all $(x, y) \in \mathcal{R}$, $o(x) = o(y)$ and $(d(x), d(y)) \in \mathcal{R}$.

**Definition 2.4.** Let $(X, m)$ be a Mealy machine. A relation $\mathcal{R} \subseteq X \times X$ is a bisimulation if for all $(x, y) \in \mathcal{R}$ and $b \in B$, $o_x(b) = o_y(b)$ and $(d_x(b), d_y(b)) \in \mathcal{R}$.

For both kind of systems, we say that $x$ and $y$ are *bisimilar*, notation $x \sim y$,
if there is a bisimulation $\mathcal{R}$ s.t. $x \in \mathcal{R}, y \in \mathcal{R}$.

Stream systems and Mealy machines, as well as the associated notions of
bisimulation, are instances of the theory of coalgebras [16]. Coalgebras provide a
suitable mathematical framework to study state-based systems and their seman-
tics at a high level of generality. In the current paper, the theory of coalgebras
underlies and enables our main results.
**Definition 2.5.** Given a functor $F: \text{Set} \to \text{Set}$, an F-coalgebra is a pair $(X, d)$, where $X$ is a set (called the carrier) and $d: X \to FX$ is a function (called the structure). An F-coalgebra morphism from $d: X \to FX$ to $d': Y \to FY$ is a map $h: X \to Y$ such that $Fh \circ d = d' \circ h$.

Stream systems and Mealy machines are F-coalgebras for the functors $FX = A \times X$ and $FX = (A \times X)^B$, respectively.

The semantics of systems modelled as coalgebras for a functor $F$ is provided by the notion of final coalgebra. A coalgebra $\zeta: Z \to FZ$ is called final if for every $F$-coalgebra $d: X \to FX$ there is a unique morphism $\llbracket - \rrbracket: X \to Z$ such that $\llbracket - \rrbracket$ is a morphism from $d$ to $\zeta$. We call $\llbracket - \rrbracket$ the coinductive extension of $d$.

Intuitively, a final coalgebra $\zeta: Z \to FZ$ defines all possible behaviours of $F$-coalgebras, and $\llbracket - \rrbracket$ assigns behaviour to all states $x, y \in X$. This motivates to define $x$ and $y$ to be behaviourally equivalent iff $\llbracket x \rrbracket = \llbracket y \rrbracket$. Under the condition that $F$ preserves weak pullbacks, behavioural equivalence coincides with bisimilarity, i.e., $x \sim y$ iff $\llbracket x \rrbracket = \llbracket y \rrbracket$ (see [16]). This condition is satisfied by (the functors for) stream systems and Mealy machines. In the sequel, by $\sim$ we hence refer both to bisimilarity and behavioural equivalence.

Final coalgebras for stream systems and Mealy machines will be pivotal for our exposition. We briefly recall them, following [16, 9]. The set $A^\omega$ of streams over $A$ carries a final coalgebra for the functor $FX = A \times X$. For every stream system $(o, d): X \to A \times X$, the coinductive extension $\llbracket - \rrbracket: X \to A^\omega$ assigns to a state $x \in X$ the stream $a_0a_1a_2\dots$ whenever $x \xrightarrow{a_0} x_1 \xrightarrow{a_1} x_2 \xrightarrow{a_2} \dots$

Recalling a final coalgebra for Mealy machines requires some more care. Given a stream $\beta \in B^\omega$, we write $\beta \upharpoonright_n$ for the prefix of $\beta$ of length $n$. A function $c: B^\omega \to A^\omega$ is causal if for all $n \in \mathbb{N}$ and all $\beta, \beta' \in B^\omega$: $\beta \upharpoonright_n = \beta' \upharpoonright_n$ entails $c(\beta) \upharpoonright_n = c(\beta') \upharpoonright_n$. The set $\Gamma(B^\omega, A^\omega) = \{c: B^\omega \to A^\omega \mid c \text{ is causal}\}$ carries a final coalgebra for the functor $FX = (A \times X)^B$. For every Mealy machine $m: X \to (A \times X)^B$, the coinductive extension $\llbracket - \rrbracket: X \to \Gamma(B^\omega, A^\omega)$ assigns to each state $x \in X$ and each input stream $b_0b_1b_2\dots \in B^\omega$ the output stream $a_0a_1a_2\dots \in A^\omega$ whenever $x \xrightarrow{b_0|a_0} x_1 \xrightarrow{b_1|a_1} x_2 \xrightarrow{b_2|a_2} \dots$

## 2.1 System Specifications

Different kinds of transition systems, like stream systems or Mealy machines, can be specified by means of algebraic specification languages. The syntax is given by an *algebraic signature* $\Sigma$, namely a collection of operation symbols $\{f_i \mid i \in I\}$ where each operator $f_i$ has a (finite) arity $n_i \in \mathbb{N}$. For a set $X$, $T_\Sigma X$ denotes the set of $\Sigma$-terms with variables over $X$. The set of closed $\Sigma$-terms is denoted by $T_\Sigma \emptyset$. We omit the subscript when $\Sigma$ is clear from the context.

A standard way to define the operational semantics of these languages is by means of structural operational semantics (SOS) [12]. In this approach, the semantics of each of the operators is described by syntactic rules, and the behaviour of a composite system is given in terms of the behaviour of its components. We recall stream GSOS [10], a specification format for stream systems.
**Definition 2.6.** A stream GSOS rule $r$ for a signature $\Sigma$ and a set $A$ is a rule

$$ \frac{x_1 \xrightarrow{a_1} x'_1 \cdots x_n \xrightarrow{a_n} x'_n}{f(x_1, \dots, x_n) \xrightarrow{a} t} \qquad (2) $$

where $f \in \Sigma$ with arity $n$, $x_1, \dots, x_n, x'_1, \dots, x'_n$ are pairwise distinct variables, $t$ is a term built over variables $\{x_1, \dots, x_n, x'_1, \dots, x'_n\}$ and $a, a_1, \dots, a_n \in A$. We say that $r$ is triggered by $(a_1, \dots, a_n) \in A^n$.

A stream GSOS specification is a tuple $(\Sigma, A, R)$ where $\Sigma$ is a signature, $A$ is a set of actions and $R$ is a set of stream GSOS rules for $\Sigma$ and $A$ s.t. for each $f \in \Sigma$ of arity $n$ and each tuple $(a_1, \dots, a_n) \in A^n$, there is only one rule $r \in R$ for $f$ that is triggered by $(a_1, \dots, a_n)$.

A stream GSOS specification allows us to extend any given stream system $\langle o, d \rangle: X \to A \times X$ to a stream system $\overline{\langle o, d \rangle}: TX \to A \times TX$, by induction: the base case is given by $\langle o, d \rangle$, and the inductive cases by the specification. This construction can be defined formally in terms of proof trees, or by coalgebraic means; we adopt the latter approach, which is recalled later in this section.

There are two important uses of the above construction: (A) applying it to the (unique) stream system carried by the empty set $\emptyset$ yields a stream system over closed terms, i.e., of the form $T\emptyset \to A \times T\emptyset$; (B) applying the construction to the final coalgebra yields a stream system of the form $TA^\omega \to A \times TA^\omega$. The coinductive extension $\llbracket - \rrbracket: TA^\omega \to A^\omega$ of this stream system is, intuitively, the interpretation of the operations in $\Sigma$ on streams in $A^\omega$.

$$ \frac{\overline{a \xrightarrow{a} a}}{\forall a \in A} \quad \frac{x \xrightarrow{a} x' \quad y \xrightarrow{b} y'}{\operatorname{alt}(x, y) \xrightarrow{a} \operatorname{alt}(y', x')} \quad \forall a, b \in A \qquad \begin{array}{l} \operatorname{alt}(a, \operatorname{alt}(b, c)) \\ a \xrightarrow{c} b \\ \operatorname{alt}(\operatorname{alt}(c, b), a) \end{array} $$

<caption>**Figure 2.** The GSOS-rules of our running example</caption>

**Figure 3.** A stream system

*Example 2.1.* Let $(\Sigma, A, R)$ be a stream GSOS specification where the signature $\Sigma$ consists of constants $\{a | a \in A\}$ and a binary operation $\operatorname{alt}$. The set $R$ contains the rules in Figure 2. For an instance of (A), the term $\operatorname{alt}(a, \operatorname{alt}(b, c)) \in T\emptyset$ defines the stream system depicted in Figure 3. For an instance of (B), the operation $\operatorname{alt}: A^\omega \times A^\omega \to A^\omega$ maps streams $a_0 a_1 a_2 \dots, b_0 b_1 b_2 \dots$ to $a_0 b_1 a_2 b_2 \dots$.

*Example 2.2.* We now consider the specification $(\Sigma, \mathbb{R}, R)$ which is the fragment of the stream calculus [17, 18] consisting of the constants $n \in \mathbb{R}$ and the binary operators $\text{sum} \oplus$ and $(\text{convolution}) \text{product} \otimes$. The set $R$ is defined in Figure 1 (a). For an example of (A), consider $n \oplus m \xrightarrow{n+m} 0 \oplus 0 \xrightarrow{0} 0 \oplus 0 \xrightarrow{0} \dots$. For (B), the induced operation $\oplus: \mathbb{R}^\omega \times \mathbb{R}^\omega \to \mathbb{R}^\omega$ is the pointwise sum of streams, i.e., it maps any two streams $n_0 n_1 \dots, m_0 m_1 \dots$ to $(n_0 + m_0)(n_1 + m_1)\dots$.
**Definition 2.7.** We say that a stream GSOS rule $r$ as in (2) is monadic if $t$ is a term built over variables $\{x'_1, \dots, x'_n\}$. A stream GSOS specification is monadic if all its rules are monadic.

The specification of Example 2.1 satisfies the monadic stream GSOS format, while the one of Example 2.2 does not since, in the rules for $\otimes$, the variable $y$ occurs in the arriving state of the conclusion.

The notions introduced above for stream GSOS, as well as the analogous ones for standard (labeled transition systems) GSOS [5], can be reformulated in an abstract framework – the so-called abstract GSOS [19, 10] – that will be pivotal for the proof of our main result.

In this setting, signatures are represented by polynomial functors: a signature $\Sigma$ corresponds to the polynomial functor $\Sigma X = \coprod_{i \in I} X^{n_i}$. For instance, the signature $\Sigma$ in Example 2.1 corresponds to the functor $\Sigma X = A + (X \times X)$, while the signature of Example 2.2 corresponds to the functor $\Sigma X = \mathbb{R} + (X \times X) + (X \times X)$. Models of a signature are seen as algebras for the corresponding functor.

**Definition 2.8.** Given a functor $F: \mathbf{Set} \to \mathbf{Set}$, an $F$-algebra is a pair $(X, d)$, where $X$ is the carrier set and $d: FX \to X$ is a function. An algebra homomorphism from an $F$-algebra $(X, d)$ to an $F$-algebra $(Y, d')$ is a map $h: X \to Y$ such that $h \circ d = d' \circ Fh$.

Particularly interesting are initial algebras: an $F$-algebra is called initial if there exists a unique algebra homomorphism from it to every $F$-algebra. For a functor corresponding to a signature $\Sigma$, the initial algebra is $(T\emptyset, \kappa)$ where $\kappa: \Sigma T\emptyset \to T\emptyset$ maps, for each $i \in I$, the tuple of closed terms $t_1, \dots, t_{n_i}$ to the closed term $f_i(t_1, \dots, t_{n_i})$. For every set $X$, we can define in a similar way $\kappa_X: \Sigma TX \to TX$. The free monad over $\Sigma$ consists of the endofunctor $T: \mathbf{Set} \to \mathbf{Set}$, mapping every set $X$ to $TX$, together with the natural transformations $\eta: \mathrm{Id} \implies T$ (interpretation of variables as terms) and $\mu: TT \implies T$ (glueing terms built of terms). Given an algebra $\sigma: \Sigma Y \to Y$, for any function $f: X \to Y$ there is a unique algebra homomorphism $f^\dagger: TX \to Y$ from $(TX, \kappa_X)$ to $(Y, \sigma)$. In particular, the identity function $\mathrm{id}: X \to X$ induces a unique algebra homomorphism from $TX$ to $X$, which we denote by $\sigma^\sharp: TX \to X$; this is the interpretation of terms in $\sigma$.

**Definition 2.9.** An abstract GSOS specification (of $\Sigma$ over $F$) is a natural transformation $\lambda: \Sigma(\mathrm{Id} \times F) \Rightarrow FT$. A monadic abstract GSOS specification (in short, monadic specification) is a natural transformation $\lambda: \Sigma F \Rightarrow FT$.

By instantiating the functor $F$ in the above definition to the functor for streams $(FX = A \times X)$ one obtains all and only the stream GSOS specifications. Instead, by taking the functor for Mealy machines $(FX = (A \times X)^B)$ one obtains the Mealy GSOS format [10]: for the sake of brevity, we do not report the concrete definition here but this notion will be important in Section 5 where, to deal with open terms, we transform stream specifications into Mealy GSOS specifications.
*Example 2.3.* For every set $X$, the rules in Example 2.1 define a function $\lambda_X : A + (A \times X) \times (A \times X) \to (A \times T_\Sigma X)$ as follows: each $a \in A$ is mapped to $(a, a)$ and each pair $(a, x')$, $(b, y') \in (A \times X) \times (A \times X)$ is mapped to $(a, \text{alt}(y', x'))$ [10].

We focus on monadic distributive laws for most of the paper, and since they are slightly simpler than abstract GSOS specifications, we only recall the relevant concepts for monadic distributive laws. However, we note that the concepts below can be extended to abstract GSOS specifications; see, e.g., [4, 10] for details.

A monadic abstract GSOS specification induces a distributive law $\rho: TF \implies FT$. This distributive law allows us to extend any $F$-coalgebra $d: X \to FX$ to an $F$-coalgebra on terms:

$$TX \xrightarrow{Td} TFX \xrightarrow{\rho_X} FTX$$

This construction generalises and formalises the aforementioned extension of stream systems to terms by means of a stream GSOS specification. In particular, (A) the unique coalgebra on the empty set !: $\emptyset \to F\emptyset$ yields an $F$-coalgebra on closed terms $T\emptyset \to FT\emptyset$. If $F$ has a final coalgebra $(Z, \zeta)$, the unique morphism $[[\cdot]]_c: T\emptyset \to Z$ defines the semantics of closed terms.

<figure><img src="image_3.png" /></figure>

Further (B), the final coalgebra $(Z, \zeta)$ yields a coalgebra on $TZ$. By finality, we then obtain a $T$-algebra over the final $F$-coalgebra, which we denote by $[[\cdot]]_a: TZ \to Z$ and we call it the abstract semantics. We define the algebra induced by $\lambda$ as the $\Sigma$-algebra $\sigma: \Sigma Z \to Z$ given by

$$\Sigma Z \xrightarrow{\Sigma \eta_Z} \Sigma T Z \xrightarrow{\kappa_Z} T Z \xrightarrow{[[\cdot]]_a} Z. \quad (3)$$

## 3 Making arbitrary stream GSOS specifications monadic

The results presented in the next section are restricted to monadic specifications, but one can prove them for arbitrary GSOS specifications by exploiting some auxiliary operators, introduced in [8] with the name of buffer. Theorem 6.1 in Section 6 only holds for monadic GSOS specifications. This does not restrict the applicability of our approach: as we show below, arbitrary stream GSOS specifications can be turned into monadic ones.

Let $(\Sigma, A, R)$ be a stream GSOS specification. The extended signature $\tilde{\Sigma}$ is given by $\{\tilde{f} | f \in \Sigma\} \cup \{a_{-} | a \in A\}$. The set of rules $\tilde{R}$ is defined as follows:

- For all $a, b \in A$, $\tilde{R}$ contains the following rule

$$\frac{x \xrightarrow{b} x'}{a.x \xrightarrow{a} b.x'} \quad (4)$$
- For each rule $r = \frac{x_1 \xrightarrow{a_1} x'_1 \cdots x_n \xrightarrow{a_n} x'_n}{f(x_1, \dots, x_n) \xrightarrow{a} t(x_1, \dots, x_n, x'_1, \dots, x'_n)} \in R$, the set $\tilde{R}$ contains

$$ \tilde{r} = \frac{x_1 \xrightarrow{a_1} x'_1 \cdots x_n \xrightarrow{a_n} x'_n}{\tilde{f}(x_1, \dots, x_n) \xrightarrow{a} \tilde{t}(a_1 x'_1, \dots, a'_n x'_n, x'_1, \dots, x'_n)} \quad (5) $$

where $\tilde{t}$ is the term obtained from $t$ by replacing each $g \in \Sigma$ by $\tilde{g} \in \tilde{\Sigma}$.

The specification $(\tilde{\Sigma}, A, \tilde{R})$ is now monadic and preserves the original semantics as stated by the following result.

**Theorem 3.1.** Let $(\Sigma, A, R)$ be a stream GSOS specification and $(\tilde{\Sigma}, A, \tilde{R})$ be the corresponding monadic one. Then, for all $t \in T_{\Sigma}\emptyset$, $t \sim \tilde{t}$.

*Example 3.1.* Consider the non-monadic specification in Example 2.2. The corresponding monadic specification consists of the rules in Figure 1 (b) where, to keep the notation light, we used operation symbols $f$ rather than $\tilde{f}$.

# 4 Pointwise Extensions of Monadic GSOS Specifications

The first step to deal with the semantics of open terms induced by a stream GSOS specification is to transform the latter into a Mealy GSOS specification. We follow the approach in [8] which is defined for arbitrary GSOS but, as motivated in Section 3, we restrict our attention to monadic specifications.

Let $(\Sigma, A, R)$ be a monadic stream GSOS specification and $B$ some input alphabet. The corresponding monadic Mealy GSOS specification is a tuple $(\Sigma, A, B, \bar{R})$, where $\bar{R}$ is the least set of Mealy rules which contains, for each stream GSOS rule $r = \frac{x_1 \xrightarrow{a_1} x'_1 \cdots x_n \xrightarrow{a_n} x'_n}{f(x_1, \dots, x_n) \xrightarrow{a} t(x'_1, \dots, x'_n)} \in R$ and $b \in B$, the Mealy rule $\bar{r}_b$ defined by

$$ \bar{r}_b = \frac{x_1 \xrightarrow{b|a_1} x'_1 \cdots x_n \xrightarrow{b|a_n} x'_n}{f(x_1, \dots, x_n) \xrightarrow{b|a} t(x'_1, \dots, x'_n)} \quad (6) $$

An example of this construction is shown in Figure 1 (c).

Recall from Section 2 that any abstract GSOS specification induces a $\Sigma$-algebra on the final $F$-coalgebra. Let $\sigma: \Sigma A^\omega \to A^\omega$ be the algebra induced by the stream specification and $\bar{\sigma}: \Sigma \Gamma(B^\omega, A^\omega) \to \Gamma(B^\omega, A^\omega)$ the one induced by the corresponding Mealy specification. Theorem 4.1, at the end of this section, informs us that $\bar{\sigma}$ is the pointwise extension of $\sigma$.

**Definition 4.1.** Let $g: (A^\omega)^n \to A^\omega$ and $\bar{g}: (\Gamma(B^\omega, A^\omega))^n \to \Gamma(B^\omega, A^\omega)$ be two functions. We say that $\bar{g}$ is the pointwise extension of $g$ iff for all $c_1, \dots, c_n \in \Gamma(B^\omega, A^\omega)$ and $\beta \in B^\omega$, $\bar{g}(c_1, \dots, c_n)(\beta) = g(c_1(\beta), \dots, c_n(\beta))$. This notion is lifted in the obvious way to $\Sigma$-algebras for an arbitrary signature $\Sigma$.
**Example 4.1.** Recall the operation $\oplus: A^\omega \times A^\omega \to A^\omega$ from Example 2.2 that arises from the specification in Figure 1 (a) (it is easy to see that the same operation also arises from the monadic specification in Figure 1 (b)). Its pointwise extension $\oplus: \Gamma(B^\omega, \mathbb{R}^\omega) \times \Gamma(B^\omega, \mathbb{R}^\omega) \to \Gamma(B^\omega, \mathbb{R}^\omega)$ is defined for all $c_1, c_2 \in \Gamma(B^\omega, \mathbb{R}^\omega)$ and $\beta \in B^\omega$ as $(c_1 \oplus c_2)(\beta) = c_1(\beta) \oplus c_2(\beta)$. Theorem 4.1 tells us that $\oplus$ arises from the corresponding Mealy GSOS specification (Figure 1(c)).

In [8], the construction in (6) is generalised from stream specifications to arbitrary abstract GSOS. The key categorical tool is the notion of costrength for an endofunctor $F: \mathbf{Set} \to \mathbf{Set}$. Given two sets $B$ and $X$, we first define $\epsilon^b: X^B \to X$ as $\epsilon^b(f) = f(b)$ for all $b \in B$. Then, $cs_{B,X}^F: F(X^B) \to (FX)^B$ is a natural map in $B$ and $X$, given by $cs_{B,X}^F(t)(b) = (F\epsilon^b)(t)$.

Now, given a monadic specification $\lambda: \Sigma F \implies FT$, we define $\bar{\lambda}: \Sigma(F^B) \implies (FT)^B$ as the natural transformation that is defined for all sets $X$ by

$$ \Sigma(FX)^B \xrightarrow{cs_{B,FX}^{\Sigma}} (\Sigma FX)^B \xrightarrow{\lambda_X^B} (FTX)^B. \quad (7) $$

Observe that $\bar{\lambda}$ is also a monadic specification, but for the functor $F^B$ rather than the functor $F$. The reader can easily check that for $F$ being the stream functor $FX = A \times X$, the resulting $\bar{\lambda}$ is indeed the Mealy specification corresponding to $\lambda$ as defined in (6).

It is worth to note that the construction of $\bar{\lambda}$ for an arbitrary abstract GSOS $\lambda: \Sigma(\mathit{Id} \times F) \implies FT$, rather than a monadic one, would not work as in (7). The solution devised in [8] consists of introducing some auxiliary operators as already discussed in Section 3. The following result has been proved in [8] for arbitrary abstract GSOS, with these auxiliary operators. Our formulation is restricted to monadic specifications.

**Theorem 4.1.** Let $F$ be a functor with a final coalgebra $(Z, \zeta)$, and let $(\bar{Z}, \bar{\zeta})$ be a final $F^B$-coalgebra. Let $\lambda: \Sigma F \implies FT$ be a monadic distributive law, and $\sigma: \Sigma Z \to Z$ the algebra induced by it. The algebra $\bar{\sigma}: \Sigma \bar{Z} \to \bar{Z}$ induced by $\bar{\lambda}$ is a pointwise extension of $\sigma$.

In the theorem above, the notion of pointwise extension should be understood as a generalisation of Definition 4.1 to arbitrary final $F$ and $F^B$-coalgebras. This generalised notion, that has been introduced in [8], will not play a role for our paper where $F$ is fixed to be the stream functor $FX = A \times X$.

# 5 Mealy Machines over Open Terms

We now consider the problem of defining a semantics for the set of open terms $TV$ for a fixed set of variables $V$. Our approach is based on the results in the previous sections: we transform a monadic GSOS specification for streams with outputs in $A$ into a Mealy machine with inputs in $A^V$ and outputs in $A$, i.e., a coalgebra for the functor $FX = (A \times X)^A$. The coinductive extension of this
Mealy machine provides the open semantics: for each open term $t \in TV$ and variable assignment $\psi: V \to A^\omega$, it gives an appropriate output stream in $A^\omega$. This is computed in a stepwise manner: for an input $\zeta: V \to A$, representing "one step" of a variable assignment $\psi$, we obtain one step of the output stream.

We start by defining a Mealy machine $c: V \to (A \times V)^{A^\nu}$ on the set of variables $V$ as on the left below, for all $\mathcal{X} \in V$ and $\zeta \in A^\nu$:

$$c(\mathcal{X})(\zeta) = (\zeta(\mathcal{X}), \mathcal{X}) \qquad \mathcal{X} \mathrel{\substack{\rightleftharpoons \\ \leftarrow}}^{\zeta|\zeta}(\mathcal{X}) \qquad (8)$$

Concretely, this machine has variables as states and for each $\zeta: V \to A$ a self-loop, as depicted on the right. Now, let $\lambda: \Sigma(A \times -) \Rightarrow A \times T$ be a monadic stream specification and $\bar{\lambda}: \Sigma((A \times -)^{A^\nu}) \Rightarrow (A \times T(-))^{A^\nu}$ be the induced Mealy specification, as defined in (7). As mentioned in Section 2, $\bar{\lambda}$ defines a distributive law $\rho: T((A \times -)^{A^\nu}) \Rightarrow (A \times T(-))^{A^\nu}$, which allows to extend $c$ (see (8)) to a coalgebra $m_\lambda: TV \to (A \times TV)^{A^\nu}$, given by

$$TV \xrightarrow{Tc} T(A \times V)^{A^\nu} \xrightarrow{\rho_\nu} (A \times TV)^{A^\nu}. \qquad (9)$$

This is the Mealy machine of interest.

**Example 5.1.** Consider the stream specification $\lambda$ of the operation $\text{alt}$, given in Example 2.1. The states of the Mealy machine $m_\lambda$ are the open terms $TV$. The transitions of terms are defined by the set of rules

$$\begin{array}{c} \xrightarrow{\substack{\leftarrow \\ a}} \\ \xrightarrow{\substack{\leftarrow \\ \zeta|a}} \end{array} \qquad \begin{array}{c} x \xrightarrow{\zeta|a} x' \qquad y \xrightarrow{\zeta|b} y' \\ \text{alt}(x, y) \xrightarrow{\zeta|a} \text{alt}(y', x') \end{array} \qquad \text{for all } \zeta: V \to A \text{ and } a, b \in A$$

together with the transitions for the variables as in (8). For instance, for each $\mathcal{X}, \mathcal{Y}, \mathcal{Z} \in V$ and all $\zeta, \zeta': V \to A$, we have the following transitions in $m_\lambda$:

$$\begin{array}{c} \text{alt}(\mathcal{X}, \text{alt}(\mathcal{Y}, \mathcal{Z})) \\ \zeta|\zeta(\mathcal{X}) \stackrel{\sim}{\leftrightarrow} \zeta'|\zeta'(\mathcal{Z}) \\ \text{alt}(\text{alt}(\mathcal{Z}, \mathcal{Y}), \mathcal{X}) \end{array}$$

**Example 5.2.** For the fragment of the stream calculus introduced in Example 2.2, the Mealy machine over open terms is defined by the rules in Figure 1(d). Below we draw the Mealy machines of some open terms that will be useful later.

$$\begin{array}{c} \xrightarrow{\substack{\leftarrow \\ \zeta|\zeta(\mathcal{X})+\zeta(\mathcal{Y}) \\ \mathcal{X} \oplus \mathcal{Y}}} \\ \xrightarrow{\substack{\leftarrow \\ \mathcal{Y} \oplus \mathcal{X}}} \end{array} \qquad \begin{array}{c} \xrightarrow{\substack{\leftarrow \\ \zeta|\zeta(\mathcal{Y})+\zeta(\mathcal{X}) \\ \mathcal{Y} \oplus \mathcal{X}}} \\ \xrightarrow{\substack{\leftarrow \\ (\mathcal{X} \oplus \mathcal{Y}) \oplus \mathcal{Z}}} \end{array} \qquad \begin{array}{c} \xrightarrow{\substack{\leftarrow \\ \zeta|\zeta(\mathcal{X})+\zeta(\mathcal{Y})+\zeta(\mathcal{Z}) \\ (\mathcal{X} \oplus \mathcal{Y}) \oplus \mathcal{Z}}} \\ \xrightarrow{\substack{\leftarrow \\ \mathcal{X} \oplus (\mathcal{Y} \oplus \mathcal{Z})}} \end{array}$$

We define the open semantics below by the coinductive extension of $m_\lambda$. Let $\tilde{\Gamma} = \Gamma((A^\nu)^\omega, A^\omega)$ be the set of causal functions $c: (A^\nu)^\omega \to A^\omega$, which is the carrier of the final coalgebra for the functor $FX = (A \times X)^{A^\nu}$. Notice
**Theorem 5.1.** For all $t_1, t_2 \in TV$, $\llbracket t_1 \rrbracket_o = \llbracket t_2 \rrbracket_o$ iff for all $\psi: V \to A^\omega$: $\llbracket T\psi(t_1) \rrbracket_a = \llbracket T\psi(t_2) \rrbracket_a$.

This is one of the main results of this paper: $T\psi(t_1)$ and $T\psi(t_2)$ are expressions in $TA^\omega$ built from symbols of the signature $\Sigma$ and streams $\alpha_1, \dots, \alpha_n \in A^\omega$. By checking $t_1 \sim_o t_2$ one can prove that the two expressions are equivalent for all possible streams $\alpha_1, \dots, \alpha_n \in A^\omega$.

**Example 5.3.** By using the Mealy machine $m_\lambda$ in Example 5.1, the relation

$$R = \{(\mathrm{alt}(\mathcal{X}, \mathrm{alt}(\mathcal{Y}, \mathcal{Z})), \mathrm{alt}(\mathcal{X}, \mathrm{alt}(\mathcal{W}, \mathcal{Z}))), (\mathrm{alt}(\mathrm{alt}(\mathcal{Z}, \mathcal{Y}), \mathcal{X}), \mathrm{alt}(\mathrm{alt}(\mathcal{Z}, \mathcal{W}), \mathcal{X})))\}$$

is easily verified to be a bisimulation (Definition 2.4). In particular this shows that $\llbracket (\mathrm{alt}(\mathcal{X}, \mathrm{alt}(\mathcal{Y}, \mathcal{Z}))) \rrbracket_o = \llbracket (\mathrm{alt}(\mathcal{X}, \mathrm{alt}(\mathcal{W}, \mathcal{Z}))) \rrbracket_o$. By Theorem 5.1, we have that $\llbracket T\psi(\mathrm{alt}(\mathcal{X}, \mathrm{alt}(\mathcal{Y}, \mathcal{Z}))) \rrbracket_a = \llbracket T\psi(\mathrm{alt}(\mathcal{X}, \mathrm{alt}(\mathcal{W}, \mathcal{Z}))) \rrbracket_a$ for all $\psi: V \to A^\omega$, i.e.,

$$\mathrm{alt}(\alpha_1, \mathrm{alt}(\alpha_2, \alpha_3)) \sim \mathrm{alt}(\alpha_1, \mathrm{alt}(\alpha_4, \alpha_3)) \text{ for all } \alpha_1, \alpha_2, \alpha_3, \alpha_4 \in A^\omega.$$

The above law can be understood as an equivalence of program schemes stating that one can always replace the stream $\alpha_2$ by an arbitrary stream $\alpha_4$, without changing the result.

**Example 5.4.** By using the Mealy machines in Example 5.2, it is easy to check that both $\{((\mathcal{X} \oplus \mathcal{Y}) \oplus \mathcal{Z}, \mathcal{X} \oplus (\mathcal{Y} \oplus \mathcal{Z}))\}$ and $\{(\mathcal{X} \oplus \mathcal{Y}, \mathcal{Y} \oplus \mathcal{X})\}$ are bisimulations. This means that $\llbracket (\mathcal{X} \oplus \mathcal{Y}) \oplus \mathcal{Z} \rrbracket_o = \llbracket (\mathcal{X} \oplus (\mathcal{Y} \oplus \mathcal{Z})) \rrbracket_o$ and $\llbracket (\mathcal{X} \oplus \mathcal{Y}) \rrbracket_o = \llbracket (\mathcal{Y} \oplus \mathcal{X}) \rrbracket_o$. By Theorem 5.1 we obtain associativity and commutativity of $\oplus$:

$$(\alpha_1 \oplus \alpha_2) \oplus \alpha_3 \sim \alpha_1 \oplus (\alpha_2 \oplus \alpha_3) \text{ and } \alpha_1 \oplus \alpha_2 \sim \alpha_2 \oplus \alpha_1 \text{ for all } \alpha_1, \alpha_2, \alpha_3 \in A^\omega.$$

**Example 5.5.** In a similar way, one can check that $\{((a+b).(\mathcal{X} \oplus \mathcal{Y}), a.(\mathcal{X} \oplus b.\mathcal{Y})) | a, b \in \mathbb{R}\}$ is a bisimulation. This means that $\llbracket (a+b).(\mathcal{X} \oplus \mathcal{Y}) \rrbracket_o = \llbracket a.(\mathcal{X} \oplus b.\mathcal{Y}) \rrbracket_o$ for all $a, b \in \mathbb{R}$ and, using again Theorem 5.1, we conclude that $(a+b).(\alpha_1 \oplus \alpha_2) \sim a.\alpha_1 \oplus b.\alpha_2$ for all $\alpha_1, \alpha_2 \in A^\omega$.

Often, equivalence of open terms is defined by relying on the equivalence of closed terms: two open terms are equivalent iff under all possible closed substitutions, the resulting closed terms are equivalent. For $\sim_o$, this property does not follow immediately by Theorem 5.1, where variables range over streams, i.e., elements of the final coalgebra. One could assume that all the behaviours of the final coalgebra are denoted by some term, however this restriction would rule out most of the languages we are aware of: in particular, the stream calculus that can express only the so-called rational streams [18].

The following theorem, that is the second main result of this paper, only requires that the stream GSOS specification is sufficiently expressive to describe arbitrary finite prefixes. We use that any closed substitution $\phi: V \to T\emptyset$ defines $\phi^\dagger: TV \to T\emptyset$ (see Section 2.1).

**Theorem 5.2.** Suppose $\lambda: \Sigma(A \times -) \Rightarrow A \times T_\Sigma$ is a monadic stream GSOS specification which contains, for each $a \in A$, the prefix operator $a.$ – as specified in (4) in Section 3. Further, assume $T\emptyset$ is non-empty.

Let $\llbracket - \rrbracket_c$ and $\llbracket - \rrbracket_o$ be the closed and open semantics respectively of $\lambda$. Then for all $t_1, t_2 \in TV$: $\llbracket t_1 \rrbracket_o = \llbracket t_2 \rrbracket_o \text{ iff } \llbracket \phi^\dagger(t_1) \rrbracket_c = \llbracket \phi^\dagger(t_2) \rrbracket_c \text{ for all } \phi: V \to T\emptyset$.
$$ \frac{x \xrightarrow{a} x'}{f(x) \xrightarrow{a} f(x' \oplus x')} \qquad \frac{x \xrightarrow{a} x'}{g(x) \xrightarrow{a} g(x' \oplus x')} \qquad \frac{x \xrightarrow{\zeta|a} x'}{f(x) \xrightarrow{\zeta|a} f(x' \oplus x')} \qquad \frac{x \xrightarrow{\zeta|a} x'}{g(x) \xrightarrow{\zeta|a} g(x' \oplus x')} $$

<caption>**Figure 4.** $f$ and $g$, operators over streams **Figure 5.** Pointwise extensions of $f$ and $g$.</caption>

*Example 5.6.* The specification in Figure 2 does not include the prefix operator, therefore it does not meet the assumptions of Theorem 5.2. Instead, the monadic GSOS specification in Figure 1(b) contains the prefix. Recall from Example 5.5 that $(a+b).(\mathcal{X} \oplus \mathcal{Y}) \sim_o a.\mathcal{X} \oplus b.\mathcal{Y}$. Using Theorem 5.2, we can conclude that $(a+b).(t_1 \oplus t_2) \sim a.t_1 \oplus b.t_2$ for all $t_1, t_2 \in T\emptyset$.

# 6 Bisimulation up-to substitutions

In the previous section, we have shown that bisimulations on Mealy machines can be used to prove equivalences of open terms specified in the stream GSOS format. In this section we introduce *up-to substitutions*, an enhancement of the bisimulation proof method that allows to deal with smaller, often finite, relations. We also show that up-to substitutions can be effectively combined with other well-known up-to techniques such as up-to bisimilarity and up-to context.

Intuitively, in a bisimulation up-to substitutions $\mathcal{R}$, the states reached by a pair of states do not need to be related by $\mathcal{R}$, but rather by $\theta(\mathcal{R})$, for some substitution $\theta: \mathcal{V} \to T\mathcal{V}$. We give a concrete example. Suppose we extend the stream calculus of Example 2.2 with the operators $f$ and $g$ defined by the rules in Figure 4. In Figure 5, we have the pointwise extensions of these new operators. It should be clear that $f(\mathcal{X}) \sim g(\mathcal{X})$. To try to formally prove $f(\mathcal{X}) \sim g(\mathcal{X})$, consider the relation $\mathcal{R} = \{(f(\mathcal{X}), g(\mathcal{X}))\}$. For all $\zeta: \mathcal{V} \to A$, there are transitions $f(\mathcal{X}) \xrightarrow{\zeta|\zeta(\mathcal{X})} f(\mathcal{X} \oplus \mathcal{X})$ and $g(\mathcal{X}) \xrightarrow{\zeta|\zeta(\mathcal{X})} g(\mathcal{X} \oplus \mathcal{X})$. The outputs of both transitions coincide but the reached states are not in $\mathcal{R}$, hence $\mathcal{R}$ is not a bisimulation. However it is a bisimulation up-to substitutions, since the arriving states are related by $\theta(\mathcal{R})$, for some substitution $\theta$ mapping $\mathcal{X}$ to $\mathcal{X} \oplus \mathcal{X}$. In fact, without this technique, any bisimulation relating $f(\mathcal{X})$ and $g(\mathcal{X})$ should contain infinitely many pairs.

In order to prove the soundness of this technique, as well as the fact that it can be safely combined with other known up-to techniques, we need to recall some notions of the theory of up-to techniques in lattices from [14]. Given a Mealy machine $(X, m)$, we consider the lattice $(\mathcal{P}(X \times X), \subseteq)$ of relations over $X$, ordered by inclusion, and the monotone map $\mathbf{b}: \mathcal{P}(X \times X) \to \mathcal{P}(X \times X)$ defined for all $\mathcal{R} \subseteq X \times X$ as

$$ \mathbf{b}(\mathcal{R}) = \{(s, t) \in X \times X \mid \forall b \in B, o_s(b) = o_t(b) \text{ and } d_s(b) \in \mathcal{R} \mid d_t(b)\}. \quad (11) $$

It is easy to see that post fixed points of $\mathbf{b}$, i.e., relations $\mathcal{R}$ such that $\mathcal{R} \subseteq \mathbf{b}(\mathcal{R})$, are exactly bisimulations for Mealy machines (Definition 2.4) and that its greatest fixed point is $\sim$.
For a monotone map $f: P(X \times X) \to P(X \times X)$, a bisimulation up-to $f$ is a relation $\mathcal{R}$ such that $\mathcal{R} \subseteq \mathbf{bf}(\mathcal{R})$. We say that $f$ is compatible with $b$ if $\mathbf{fb}(\mathcal{R}) \subseteq \mathbf{bf}(\mathcal{R})$ for all relations $\mathcal{R}$. Two results in [14] are pivotal for us: first, if $f$ is compatible and $\mathcal{R} \subseteq \mathbf{bf}(\mathcal{R})$ then $\mathcal{R} \subseteq \sim$; second if $f_1$ and $f_2$ are compatible with $b$ then $f_1 \circ f_2$ is compatible with $b$. The first result informs us that bisimilarity can be proved by means of bisimulations up-to $f$, whenever $f$ is compatible. The second result states that compatible up-to techniques can be composed.

We now consider up-to techniques for the Mealy machine over open terms $(TV, m_\lambda)$ as defined in Section 5. Recall that bisimilarity over this machine is called open bisimilarity, denoted by $\sim_o$. Up-to substitutions is the monotone function $(-)_{\sim_o}: P(TV \times TV) \to P(TV \times TV)$ mapping every $\mathcal{R} \subseteq TV \times TV$ to

$$ (\mathcal{R})_{\sim_o} = \{(\theta(t_1), \theta(t_2)) \mid \theta: V \to TV \text{ and } t_1 \mathcal{R} t_2\}. $$

Similarly, we define up-to context as the monotone function mapping every relation $\mathcal{R} \subseteq TV \times TV$ to its contextual closure $\mathcal{C}(\mathcal{R})$ and up-to (open) bisimilarity as the function mapping $\mathcal{R}$ to $\sim_o \mathcal{R} \sim_o = \{(t_1, t_2) \mid \exists t'_1, t'_2 \text{ s.t. } t_1 \sim_o t'_1 \mathcal{R} t'_2 \sim_o t_2\}$.

Compatibility with $b$ of up-to context and up-to bisimilarity hold immediately by the results in [6]. For the novel technique, up-to substitutions, we have:

**Theorem 6.1.** The function $(-)_{\sim_o}$ is compatible with $b$.

As a consequence of the above theorem and the results in [14], up-to substitutions can be used in combination with up-to bisimilarity and up-to context (as well as any another compatible up-to technique) to prove open bisimilarity. We will show this in the next, concluding example, for which a last remark is useful: the theory in [14] also ensures that if $f$ is compatible with $b$, then $f(\sim) \subseteq \sim$. By Theorem 6.1, this means that $(\sim_o)_{\sim_o} \subseteq \sim_o$. The same obviously holds for the contextual closure: $\mathcal{C}(\sim_o) \subseteq \sim_o$.

**Example 6.1.** We prove that the convolution product $\otimes$ distributes over the sum $\oplus$, i.e., $\alpha_1 \otimes (\alpha_2 \oplus \alpha_3) \sim (\alpha_1 \otimes \alpha_2) \oplus (\alpha_1 \otimes \alpha_3)$ for all streams $\alpha_1, \alpha_2, \alpha_3 \in \mathbb{R}^\omega$. By Theorems 5.1 and 6.1, to prove our statement it is enough to show that $\mathcal{R} = \{(\mathcal{X} \otimes (\mathcal{Y} \oplus \mathcal{Z})), (\mathcal{X} \otimes \mathcal{Y}) \oplus (\mathcal{X} \otimes \mathcal{Z})\}$ is a bisimulation up-to $\sim_o \mathcal{C}(\sim_o (-)_{\sim_o} \sim_o) \sim_o$.

By rules in Figure 1(d), for all $\zeta: V \to \mathbb{R}$, the transitions of the open terms are

$$ \begin{aligned} & - \mathcal{X} \otimes (\mathcal{Y} \oplus \mathcal{Z}) \xrightarrow{\zeta|\zeta(\mathcal{X}) \times (\zeta(\mathcal{Y}) + \zeta(\mathcal{Z}))} (\zeta(\mathcal{X}) \otimes (\mathcal{Y} \oplus \mathcal{Z})) \oplus (\mathcal{X} \otimes (\zeta(\mathcal{Y}) + \zeta(\mathcal{Z})).(\mathcal{Y} \oplus \mathcal{Z})) \\ & - (\mathcal{X} \otimes \mathcal{Y}) \oplus (\mathcal{X} \otimes \mathcal{Z}) \xrightarrow{\zeta|\zeta(\mathcal{X}) \times \zeta(\mathcal{Y}) + \zeta(\mathcal{X}) \times \zeta(\mathcal{Z})} ((\zeta(\mathcal{X}) \otimes \mathcal{Y}) \oplus (\mathcal{X} \otimes \zeta(\mathcal{Y}).\mathcal{Y})) \oplus ((\zeta(\mathcal{X}) \otimes \mathcal{Z}) \oplus (\mathcal{X} \otimes \zeta(\mathcal{Z}).\mathcal{Z})) \end{aligned} $$

For the outputs, it is evident that $\zeta(\mathcal{X}) \times (\zeta(\mathcal{Y}) + \zeta(\mathcal{Z})) = \zeta(\mathcal{X}) \times \zeta(\mathcal{Y}) + \zeta(\mathcal{X}) \times \zeta(\mathcal{Z})$. For the arriving states we need a few steps, where for all $\zeta: V \to \mathbb{R}$ and $\mathcal{X} \in V$, $\zeta(\mathcal{X})$ denotes either a real number (used as a prefix) or a constant of the syntax (Example 2.2).

$$ (a) \mathcal{X} \otimes (\zeta(\mathcal{Y}).\mathcal{Y} \oplus \zeta(\mathcal{Z}).\mathcal{Z}) \mathcal{R}_{\sim_o} (\mathcal{X} \otimes (\zeta(\mathcal{Y}).\mathcal{Y}) \oplus (\mathcal{X} \otimes \zeta(\mathcal{Z}).\mathcal{Z}).\mathcal{Z}). $$
(b) By Example 5.5 and $C(\sim_o) \subseteq \sim_o$, we have that:
$$ \mathcal{X} \otimes (\varsigma(\mathcal{Y}) + \varsigma(\mathcal{Z})).(\mathcal{Y} \oplus \mathcal{Z}) \sim_o \mathcal{X} \otimes (\varsigma(\mathcal{Y}).\mathcal{Y} \oplus \varsigma(\mathcal{Z})).\mathcal{Z}. $$

(c) By (b) and (a):
$$ \mathcal{X} \otimes (\varsigma(\mathcal{Y}) + \varsigma(\mathcal{Z})).(\mathcal{Y} \oplus \mathcal{Z}) \sim_o \mathcal{R}_{\forall \theta} \sim_o (\mathcal{X} \otimes \varsigma(\mathcal{Y}).\mathcal{Y}) \oplus (\mathcal{X} \otimes \varsigma(\mathcal{Z}).\mathcal{Z}). $$

(d) $\varsigma(\mathcal{X}) \otimes (\mathcal{Y} \oplus \mathcal{Z}) \mathcal{R}_{\forall \theta} (\varsigma(\mathcal{X}) \otimes \mathcal{Y}) \oplus (\varsigma(\mathcal{X}) \otimes \mathcal{Z}).$

(e) Using (d) and (c) with context $C = \oplus$:
$$ (\varsigma(\mathcal{X}) \otimes (\mathcal{Y} \oplus \mathcal{Z})) \oplus (\mathcal{X} \otimes (\varsigma(\mathcal{Y}) + \varsigma(\mathcal{Z})).(\mathcal{Y} \oplus \mathcal{Z})) \\ C(\sim_o \mathcal{R}_{\forall \theta} \sim_o) ((\varsigma(\mathcal{X}) \otimes \mathcal{Y}) \oplus (\varsigma(\mathcal{X}) \oplus \mathcal{Z})) \oplus ((\mathcal{X} \otimes \varsigma(\mathcal{Y}).\mathcal{Y}) \oplus (\mathcal{X} \otimes \varsigma(\mathcal{Z}).\mathcal{Z})). $$

(f) By Example 5.4 (associativity and commutativity of $\oplus$) and $(\sim_o)_{\forall \rho} \subseteq \sim_o$:
$$ ((\varsigma(\mathcal{X}) \otimes \mathcal{Y}) \oplus (\varsigma(\mathcal{X}) \oplus \mathcal{Z})) \oplus ((\mathcal{X} \otimes \varsigma(\mathcal{Y}).\mathcal{Y}) \oplus (\mathcal{X} \otimes \varsigma(\mathcal{Z}).\mathcal{Z})) \\ \sim_o ((\varsigma(\mathcal{X}) \otimes \mathcal{Y}) \oplus (\mathcal{X} \otimes \varsigma(\mathcal{Y}).\mathcal{Y})) \oplus ((\varsigma(\mathcal{X}) \otimes \mathcal{Z}) \oplus (\mathcal{X} \otimes \varsigma(\mathcal{Z}).\mathcal{Z})). $$

(g) By (e) and (f):
$$ (\varsigma(\mathcal{X}) \otimes (\mathcal{Y} \oplus \mathcal{Z})) \oplus (\mathcal{X} \times (\varsigma(\mathcal{Y}) + \varsigma(\mathcal{Z})).(\mathcal{Y} \oplus \mathcal{Z})) \\ \sim_o C(\sim_o \mathcal{R}_{\forall \theta} \sim_o) ((\varsigma(\mathcal{X}) \otimes \mathcal{Y}) \oplus (\mathcal{X} \otimes \varsigma(\mathcal{Y}).\mathcal{Y})) \oplus ((\varsigma(\mathcal{X}) \otimes \mathcal{Z}) \oplus (\mathcal{X} \otimes \varsigma(\mathcal{Z}).\mathcal{Z})). $$

# 7 Final remarks

In this paper we have studied the semantics of open terms specified in the stream GSOS format. Our recipe consists in translating the stream specification into a Mealy specification giving semantics to all open terms. Remarkably, this semantics equates two open terms if and only if they are equivalent under all possible interpretations of variables as streams (Theorem 5.1) or under the interpretation of variables as closed terms (Theorem 5.2). Furthermore, semantic equivalence can be checked by means of the bisimulation proof method enhanced with a technique called up-to substitutions (Theorem 6.1).

Our work can be considered as a first step toward a (co)algebraic understanding of the semantics of open terms in the general setting of abstract GSOS [19, 10]. While our approach exploits several peculiarities of the final coalgebra for stream systems, several intermediate results hold in the general setting: for instance, the construction in Section 3 transforming arbitrary stream GSOS specifications into monadic ones, seems to hold for arbitrary abstract GSOS. Another promising clue in this direction comes from the way we specified the semantics of variables in Section 5: it is reminiscent of the technique adopted in [2] for dealing with open terms of process calculi denoting labeled transition systems.

# References

1. L. Aceto, M. Cimini, and A. Ingólfsdóttir. Proving the validity of equations in GSOS languages using rule-matching bisimilarity. *MSCS*, 22(2):291–331, 2012.

2. L. Aceto, W. Fokkink, A. Ingólfsdóttir, and B. Luttik. Finite equational bases in process algebra: Results and open questions. In *Processes, Terms and Cycles*, volume 3838 of LNCS, pages 338–367. Springer, 2005.

3. P. Baldan, A. Bracciali, and R. Bruni. A semantic framework for open processes. *Theor. Comput. Sci.*, 389(3):446–483, 2007.
4. F. Bartels. *On generalised coinduction and probabilistic specification formats*. PhD thesis, CWI, Amsterdam, 2004.

5. B. Bloom, S. Istrail, and A. R. Meyer. Bisimulation can't be traced. *J. ACM*, 42(1):232–268, January 1995.

6. F. Bonchi, D. Petrisan, D. Pous, and J. Rot. A general account of coinduction up-to. *Acta Informatica*, pages 1–64, 2016.

7. R. de Simone. Higher-level synchronising devices in Meije-SCCS. *Theor. Comput. Sci.*, 37:245–267, 1985.

8. H. H. Hansen and B. Klin. Pointwise extensions of GSOS-defined operations. *Mathematical Structures in Computer Science*, 21(2):321–361, 2011.

9. H. H. Hansen and J. J. M. M. Rutten. Symbolic synthesis of mealy machines from arithmetic bitstream functions. *Sci. Ann. Comp. Sci.*, 20:97–130, 2010.

10. B. Klin. Bialgebras for structural operational semantics: An introduction. *Theor. Comput. Sci.*, 412(38):5043–5069, 2011.

11. D. Lucanu, E. Goriac, G. Caltais, and G. Rosu. CIRC: A behavioral verification tool based on circular coinduction. In *CALCO 2009. Proc.*, pages 433–442, 2009.

12. M. Mousavi, M. Reniers, and J. Groote. SOS formats and meta-theory: 20 years after. *Theor. Comput. Sci.*, 373(3):238–272, 2007.

13. A. Popescu and E. L. Gunter. Incremental pattern-based coinduction for process algebra and its isabelle formalization. In *FOSSACS, Proc.*, pages 109–127, 2010.

14. D. Pous and D. Sangiorgi. Enhancements of the bisimulation proof method. In *Advanced Topics in Bisimulation and Coinduction*. Cambridge, 2012.

15. A. Rensink. Bisimilarity of open terms. *Inf. Comput.*, 156(1-2):345–385, 2000.

16. J. Rutten. Universal coalgebra: a theory of systems. *TCS*, 249(1):3–80, 2000.

17. J. Rutten. Elements of stream calculus (an extensive exercise in coinduction). *ENTCS*, 45:358–423, 2001.

18. J. Rutten. A tutorial on coinductive stream calculus and signal flow graphs. *TCS*, 343(3):443–481, 2005.

19. D. Turi and G. D. Plotkin. Towards a mathematical operational semantics. In *LICS 1997, Proceedings*, pages 280–291, 1997.

20. H. Zantema and J. Endrullis. Proving equality of streams automatically. In *Proceedings of RTA 2011, Novi Sad, Serbia*, pages 393–408, 2011.