A Complete Logic for Behavioural Equivalence in Coalgebras of Finitary Set Functors

Abstract

This paper presents a sound and complete sequent-style deduction system for determining behavioural equivalence in coalgebras of finitary set functors preserving weak pullbacks. We select finitary set functors because they are quotients of polynomial functors: the polynomial functor provides a ready-made signature and the quotient provides necessary additional axioms. We also show that certain operations on functors can be expressed with uniform changes to the presentations of the input functors, making this system compositional for a range of widely-studied classes of functors, such as the Kripke polynomial functors. Our system has roots in the $FLR_0$ proof system of Moschovakis et al., particularly as used by Moss, Wennstrom, and Whitney for non-wellfounded sets. Similarities can also be drawn to expression calculi in the style of Bonsangue, Rutten, and Silva.

1 Introduction

In this paper, we propose a logic for detecting bisimilar states in coalgebras of finitary Set-endofunctors. We focus on finitary functors because they have presentations whereby they can be represented as the quotient of a signature functor by a collection of equations.¹ The signature provides a syntax in which the coalgebras can be expressed, and the equations add the axioms necessary to distinguish reasoning among functors of similar syntax.

In particular, we will consider specifications on sets of variables in the signature of finitary functors. These are total assignments of variables to terms which serve as definitions, and may be considered a recasting of the longstanding tradition of systems of simultaneous equations going back to Kahn, Manna and Vuillemin, and Lawvere. We show every coalgebra of a finitary functor has at least one corresponding specification.

Our system is comparable to $FLR_0$, as considered by Moss in [2] and Moss et al. in [3]. $FLR_0$ has distinctive terms of the form $x_i\ \mathbf where \ \{x_1 = A_1, \ldots , x_n = A_n\}$. This where operator binds variables, but also allows terms to carry their context. As a consequence, many of the $FLR_0$ rules concern moving a definition in and out of a subscope or evolving the term before the where clause. We avoid these issues by fixing a specification sending $x_i$ to $A_i$, roughly, and considering terms with this context backgrounded. Additionally, $FLR_0$ and the full FLR language are intended as general languages of recursion with semantics of various flavors. The application here to coalgebras distinguishes our version somewhat.

We might also compare this work to that of Bonsangue et al. in [4, 5] or Milius’ related work in the setting of vector spaces [6], where a $\mu$ operator provides a similar variable binding. The work of Bonsangue et al. feature an inductive class of functors, the so-called Kripke polynomial functors, and a syntax of expressions based on the inductive class. They build a sound and complete axiomatization for these expressions which is compositional, meaning the laws involved are built in parallel with the definition of the functor and the expressions. We show that the presentations involved in our setting enjoy similar compositional properties.

In Chap. 5 of Silva’s PhD thesis [7] and the related paper [8], she gives an extension of this $\mu$ calculus to finitary functors, demonstrating that the expressions of this calculus exactly coincide with the behaviours of locally finite coalgebras. However, at the end of this work, questions regarding axiomatization and uniform proofs of soundness and completeness for the system are left open.

We are able to prove soundness and completeness for our logic for the finitary functors which preserve weak pullbacks, a common condition with numerous pleasant coalgebraic consequences including that bisimilarity and behavioural equivalence coincide, see Rutten [9]. In particular, polynomial functors and the finite powerset functor preserve weak pullbacks, so the functors in our setting properly include those of Bonsangue et al. and Moss et al.

Outline. In Sect. 2, we briefly recall some background on coalgebras, signatures, and finitary functors. This section introduces the interplay between coalgebras of a finitary functor and coalgebras of its related signature functor that are of central importance to later sections. In Sect. 3, we introduce bisimulation up-to-presentation, a novel up-to technique which permits expressing bisimulations for finitary functors in terms of bisimulations for their signatures. In Sect. 4, we present a formal proof system capturing the notion of bisimulation-up-to. We show this system is sound and complete in the sense that it detects the bisimilarity of states in coalgebras for finitary functors preserving weak pullbacks. In Sect. 5, we note that signatures for previously studied inductive classes of these functors–including the Kripke polynomial functors–can be constructed compositionally. This allows the proof system developed in Sect. 4 to be constructed compositionally as well.

2 Background

In this section, we recall definitions and basic results about coalgebras, finitary signatures, finitary functors, and introduce the notion of a specification. Our setting is the category Set, and all functors are assumed to be Set-endofunctors. Additionally, we will often assume functors preserve weak pullbacks, but make a special note when this assumption is needed.

2.1 Coalgebras

Given a Set-endofunctor F, an F -coalgebra is a set X together with a map $f: X \rightarrow FX$. The set is often called the carrier of the coalgebra, while f gives its structure or dynamics.

A coalgebra morphism from an F-coalgebra (X, f) to another F-coalgebra (Y, g) is a map $\varphi : X \rightarrow Y$ such that the following diagram commutes:

F-coalgebras together with coalgebra morphisms between them form a category, often denoted Coalg $_F$. Of particular interest are the F where Coalg $_F$ has a final object. This final coalgebra has a natural interpretation as a semantic object: since there is a unique coalgebra morphism from any F-coalgebra into it, points in coalgebras which have the same image in the final coalgebra can be considered (behaviourally) equivalent to one another.

A related notion is that of an (Aczel-Mendler) F -bisimulation on a coalgebra. An F-bisimulation is a relation $R \subseteq X \times X$ such that there is an F-coalgebra structure on R, $\rho$, such that the following diagram holds:²

Roughly speaking, a relation is a bisimulation if two points in a coalgebra being related implies their structures are also related. This gives a different notion of equivalence, which is known to coincide with the behavioural equivalence for weak pullback preserving functors. For more details, we refer the reader to Rutten [9].

2.2 Finitary Signatures and Functors

A finitary signature is a set $\varSigma$ with a map $ar: \varSigma \rightarrow \omega$. In the sequel, we often abbreviate “finitary signature” to “signature” and refer to the signature as $\varSigma$ instead of $(\varSigma , ar)$ when there is no risk of confusion. The elements of $\varSigma$ are the symbols of the signature, and each symbol $f \in \varSigma$ has the arity ar(f). The collection of all symbols with arity n is denoted $\varSigma _n$.

Each finitary signature has an associated signature functor, $H_\varSigma$, given by $\coprod _n \varSigma _n \times X^n$. We denote a typical element of $H_\varSigma X$ by $f(x_1, \ldots , x_{ar(f)})$ if $x_i \in X$ or $f(\varvec{x})$ if $\varvec{x}: ar(f) \rightarrow X$. $H_\varSigma X$ is often referred to as the set of all “flat terms” using symbols from $\varSigma$ with variables from X.

F is a finitary functor if there is a finitary signature $\varSigma$ together with a (pointwise) epic natural transformation $\epsilon : H_\varSigma \twoheadrightarrow F$.³ If F is a finitary functor, we say ($\varSigma$, $\epsilon$) is a presentation of F. Finitary functors have a number of alternate characterizations, including functors which preserve $\omega$-filtered colimits [1].

Example 1

For each set A, the constant functor $FX = A$ is finitary with signature $\varSigma = \varSigma _0 = A$ and the transformation $\epsilon$ with components $\epsilon _X: a() \mapsto a$.

Example 2

The identity functor is finitary with signature $\varSigma = \varSigma _1 = \{*\}$ and the transformation $\epsilon$ with components $\epsilon _X: *(x) \mapsto x$.

Example 3

The finite powerset functor $\mathcal{P}_\omega$ is finitary with signature $\varSigma _n = \{\sigma _n\}$ and the transformation $\epsilon _X: \sigma _n(x_1, \ldots , x_n) \mapsto \{x_1, \ldots , x_n\}$. Note that unlike the previous two transformations, this $\epsilon$ is not an isomorphism.

Example 4

The 3 powerset functor $\mathcal{P}_3$, which assigns each set to the set of its subsets of cardinality $< 3$, is finitary with signature $\varSigma _n = \{\sigma _n\}$ for $0 \le n < 3$ and the same $\epsilon$ as in $P_\omega$, restricted to the smaller set of terms.

Example 5

The functor $ZX = \{0, 1\} \times X \times X$ is finitary with signature $\varSigma = \varSigma _2 = \{0:\text {zip}, 1:\text {zip}\}$ and transformation given by

$$\begin{aligned} \epsilon _X(i:\text {zip}(x_1, x_2)) = (i, x_1, x_2). \end{aligned}$$

We call this the “zip functor” in the sequel, though this is not standard terminology.

A specification in the signature $\varSigma$ is an $H_\varSigma$-coalgebra, a set X together with a function $d: X \rightarrow H_\varSigma X$. Elements of X are called variables, and d gives their definition. Every specification in the signature of a finitary functor F gives rise to an F-coalgebra: given $d: X \rightarrow H_\varSigma X$ postcomposing with $\epsilon _X$ yields $\epsilon _X \circ d: X \rightarrow FX$.

A single F-coalgebra (X, f) will correspond to potentially many specifications in its signature. For each section s of $\epsilon _X$, the composition $s\circ f: X \rightarrow H_\varSigma X$ is a specification in $\varSigma$. The F-coalgebra related to each of these specifications will be, not surprisingly, (X, f). Note at least one section of $\epsilon _X$ is guaranteed to exist since Set has split epis.

At a broad level, this paper could be seen as an attempt to use the quotient relationship $\epsilon : H_\varSigma \twoheadrightarrow F$ between the functors $H_\varSigma$ and F to understand the relationships between $H_\varSigma$- and F-coalgebras and particularly the relationships between $H_\varSigma$- and F-bisimulations. Rather than constantly clarifying which functor we are considering, we hereafter reserve “specification” to mean an $H_\varSigma$-coalgebra, and the undecorated “coalgebra” to mean F-coalgebra.

Since we can readily recast specifications and coalgebras for finitary Set functors, we translate standard notions from coalgebras to specifications. For example, R is an F-bisimulation on the specification (X, d) when it is an F-bisimulation on the coalgebra $(X, \epsilon _X\circ d)$, the standard semantics for a variable in a specification is its image in a given final F-coalgebra, and two variables are behaviourally equivalent when they have the same standard semantics. Note that though the standard semantics of a variable depends on the final coalgebra under consideration, whether two variables are behaviourally equivalent is independent of this choice.

We write $\vDash _{(X, d)} x = y$ when x and y are behaviourally equivalent states in the specification. When the specification is clear from context, we write $\vDash x = y$. (This notation will be relevant mostly in Sect. 4.)

Example 6

We can give a specification for the zip functor with $X=\{x, y, z, w\}$ and

$$\begin{aligned} d(x) = 0:\text {zip}(y, z) \, \,&\qquad d(y) = 1:\text {zip}(x, w) \\ d(z) = 1:\text {zip}(z, w) \, \,&\qquad d(w) = 0:\text {zip}(w, z) \end{aligned}$$

As shown by Kupke and Rutten in [11] and Grabmayer et al. in [12], a final coalgebra for this functor is the set of streams in $\{0, 1\}$.⁴ With this final coalgebra in mind the standard semantics for x is the Thue-Morse sequence.

Example 7

Another zip specification for $Y = \{x, y, z, w, u, v, q\}$ is given by

$$\begin{aligned} d(x) = 0:\text {zip}(y, z) \quad&d(y) = 1:\text {zip}(x, v) \quad&d(v) = 0:\text {zip}(w, u) \\ d(w) = 0:\text {zip}(w, z) \quad&d(z) = 1:\text {zip}(z, w) \quad&d(u) = 1:\text {zip}(u, v) \\&d(q) = 0:\text {zip}(y, u)&\end{aligned}$$

In this specification, the states x and q are behaviourally equivalent. Our goal is to give a uniform account for detecting this behavioural equivalence.

Note also x in this example and x in Example 6 are behaviourally equivalent. We could consider the problem of showing the equivalence of two variables in two separate specifications, but by taking the disjoint union of the two specifications and determining equivalence within this single joint specification we get the same effect.

3 Bisimulation Up to Presentation

In this section, we introduce the notion of bisimulation up to presentation. Roughly, bisimulations up to presentation are $H_\varSigma$-bisimulations relaxed up to the kernel of $\epsilon$ in such a way that they correspond nicely to F-bisimulations. This allows us to detect F-bisimulations using the more syntactic $H_\varSigma$-bisimulations and so-called $\epsilon$ laws. We also give an alternate characterization of bisimulation up to presentation and several related sufficient criteria to conclude that a relation is a subset of the bisimilarity relation.

Since bisimulation up to presentation provides an alternate criterion which suffices for detecting bisimulations, we have intentionally named this type of relation in the style of enhanced coalgebraic bisimulations studied recently by Rot et al. [13] with veins of research going back to Milner, Park, Sangiorgi, and others. We are also struck by the similarities between the results in Sect. 3.2 and the flavor of standard up-to results. However, we are unaware of a formal connection between these bodies of work since our setting relates bisimulations of two related functors, and the standard literature deals with bisimulations of a single functor. We would be very glad to learn of a connection, though.

Recall the standard (Aczel-Mendler) bisimulation diagram for an $H_\varSigma$-bisimulation on X:

We say $R \subseteq X \times X$ is a bisimulation up to the presentation $(\varSigma , \epsilon )$ if there is a $\rho : R \rightarrow H_\varSigma R$ such that $\epsilon _X \circ d \circ \pi _i = \epsilon _X \circ H_\varSigma \pi _i \circ \rho$ for $i \in \{1, 2\}$. That is, $\rho$ nearly gives R a $H_\varSigma$-coalgebra structure except that the paths in the diagram above are coequalized by $\epsilon _X$ instead of commuting outright.

Theorem 1

For all specifications (X, d) for a finitary set functor with presentation $(\varSigma , \epsilon )$, a relation $R \subseteq X \times X$ is an F-bisimulation if and only if it is a bisimulation up to the presentation $(\varSigma , \epsilon )$.

Proof

($\Leftarrow$) Let $\rho$ give R the structure of a bisimulation up to the presentation $(\varSigma , \epsilon )$. Then $\epsilon _R \circ \rho$ gives R an F-coalgebra structure such that

commutes, so R is an F-bisimulation.

($\Rightarrow$) Given an F-bisimulation structure $\phi$ on R, we claim $s\circ \phi$ gives a bisimulation up to presentation structure to R where s is any section of $\epsilon _R$. To see this, note $\epsilon _X \circ H_\varSigma \pi _i \circ s\circ \phi = F\pi _i \circ \epsilon _R \circ s \circ \phi = F\pi _i \circ \phi = \epsilon _X \circ d \circ \pi _i$

We note that this statement is not that the F-bisimulation structures are in 1-1 correspondence with the bisimulation up to presentation structures, but that the carriers are in a 1-1 correspondence. Much like the correspondence between coalgebras and specifications, there is a possibly distinct bisimulation up to presentation structure for each section of $\epsilon _R$.

Corollary 1

The biggest F-bisimulation on a coalgebra is the biggest bisimulation up to the presentation $(\varSigma , \epsilon )$ on that coalgebra.

We denote bisimilarity, the biggest F-bisimulation on a coalgebra, by $\sim$. The bisimilarity relation is known to be an equivalence relation on all coalgebras for all Set functors preserving weak pullbacks, see e.g. Rutten [9].

3.1 An Explicit Characterization

We defined a bisimulation up to presentation using a variation of the Aczel-Mendler diagram, but there is a more concrete characterization for bisimulations up to presentation which we describe in this section.

For flat terms $\alpha , \beta \in H_\varSigma X$ we write $\alpha =_{\epsilon } \beta$ to mean $\epsilon _X(\alpha ) = \epsilon _X(\beta )$. If $\alpha =_{\epsilon } \beta$ we say this is an $\epsilon$ law, or that $\alpha$ may be rewritten to $\beta$ using $\epsilon$ laws. Note the $=_\epsilon$ relation on $H_\varSigma X$ is an equivalence relation.

Definition 1

( c(R)). The flat contextual closure of a relation $R \subseteq X \times X$ is the relation $c(R) \subseteq H_\varSigma X \times H_\varSigma X$ defined by $f(x_1, \ldots x_{ar(f)})\ c(R)\ f(y_1, \ldots , y_{ar(f)})$ if and only if $x_i\ R\ y_i$ for all $1 \le i \le ar(f)$.

We denote the pointwise composition of relations R and S by $R \bullet S$. That is, $x (R \bullet S) z$ iff there exists a y such that xR y and yS z.

Definition 2

( $\sim _R$ ). Given a relation R on X, we define $\sim _R$ to be $=_\epsilon \bullet \ c(R)\ \bullet =_\epsilon$, a relation on $H_\varSigma X$.

Since $\sim _R$ also depends on the transformation $\epsilon$ it would be more proper to denote it $\sim _{R, \epsilon }$, but since $\epsilon$ is standard for each functor we elide it from the notation.

Here we also emphasize the distinction between two very similar symbols: $\sim$ denotes bisimilarity on X, and has no direct relationship with the symbol $\sim _R$ just defined.

Theorem 2

Given a finitary functor F and a specification (X, d) in that functor’s signature, $R \subseteq X \times X$ is a bisimulation up to the presentation $(\varSigma , \epsilon )$ if and only if xR y implies $d(x) \sim _R d(y)$. More explicitly, for each $(x, y) \in R$, there is an $f \in \varSigma _n$ and $(x_1, y_1), \ldots , (x_{n}, y_{n}) \in R$ such that:

• 1. $d(x) =_\epsilon f(x_1, \ldots , x_{n})$

• 2. $d(y) =_\epsilon f(y_1, \ldots , y_{n})$

Proof

($\Rightarrow$) Suppose we have $\rho : R \rightarrow H_\varSigma R$ such that $\epsilon _X \circ d \circ \pi _i = \epsilon _X \circ H_\varSigma \pi _i \circ \rho$. Let $(x, y) \in R$ and write $\rho (x, y) = f((x_1, y_1), \ldots , (x_{n}, y_{n}))$ where $f \in \varSigma$ and $(x_i, y_i) \in R$. Then $(H_\varSigma \pi _1 \circ \rho )(x,y) = f(x_1, \ldots , x_{n})$, so by the hypothesis on $\rho$, $d(x) =_\epsilon f(x_1, \ldots , x_{n})$, as desired. Similarly considering $(H_\varSigma \pi _2 \circ \rho )(x,y)$ yields item 2.

($\Leftarrow$) Suppose we have a relation satisfying the latter condition, and define $\rho : R \rightarrow H_\varSigma R$ by $\rho (x, y) = f((x_1, y_1), \ldots , (x_{n}, y_{n}))$. Then by item 1, $\epsilon _X \circ d \circ \pi _1 = \epsilon _X \circ H_\varSigma \pi _1 \circ \rho$, and similarly for item 2.

Theorem 2 gives an explicit characterization for bisimulations up to presentation. To check that a relation is a bisimulation up to presentation, for each pair (x, y) in the relation we need to rewrite d(x) and d(y) using $\epsilon$ laws so that they have the same symbol and all corresponding variables are related.

We can now show x and q from Example 7 are related by a bisimulation up to presentation.

Example 8

Recall that the zip functor has function symbols $\varSigma = \varSigma _2 = \{0:\text {zip}, 1:\text {zip}\}$ with no nontrivial $\epsilon$ laws. Then for the specification

$$\begin{aligned} d(x) = 0:\text {zip}(y, z) \quad&d(y) = 1:\text {zip}(x, v)&d(v) = 0:\text {zip}(w, u) \\ d(w) = 0:\text {zip}(w, z) \quad&d(z) = 1:\text {zip}(z, w)&d(u) = 1:\text {zip}(u, v) \\&d(q) = 0:\text {zip}(y, u)&\end{aligned}$$

we propose $R = \{(x, q), (z, u), (w, v)\} \cup \varDelta _X$ as a bisimulation up to presentation. The diagonal part clearly satisfies the required properties. Then

• $0:\text {zip}(y, z) \sim _R 0:\text {zip}(y, u)$ since yRy and zRu.

• $1:\text {zip}(z, w) \sim _R 1:\text {zip}(u, v)$ since zRu and wRv.

• $0:\text {zip}(w, z) \sim _R 0:\text {zip}(w, u)$ since wRw and zRu.

Since the zip functor has no nontrivial $\epsilon$ laws this is just an ordinary $H_\varSigma$ bisimulation. Matters are more complicated for non-polynomial functors.

Example 9

Recall that the functor $\mathcal{P}_3$ from Example 4 has a presentation with three function symbols, $\{\sigma _i\}_{i < 3}$, each with arity i and $\epsilon$ laws of the forms $\sigma _2(x, y) =_\epsilon \sigma _2(y, x)$ and $\sigma _2(x, x) =_\epsilon \sigma _1(x)$.

An example specification in this signature for $X = \{x, y, z\}$ might be

$$\begin{aligned} d(x) = \sigma _2(x, y)&d(y) = \sigma _1(z)&d(z) = \sigma _2(z, z) \end{aligned}$$

All of these are behaviourally equivalent, so they should be related by a bisimulation up to presentation. We propose $R = \{(x, y), (y, z), (x, z), (z, z)\}$. For this we need to check four things:

• $\sigma _2(x, y) \sim _R \sigma _1(z)$: we use $\sigma _1(z) =_\epsilon \sigma _2(z, z)$ to rewrite the RHS and note xRz and yRz.

• $\sigma _1(z) \sim _R \sigma _2(z,z)$: uses the same rewrite and zRz twice.

• $\sigma _2(x, y) \sim _R \sigma _2(z, z)$: immediate from xRz and yRz.

• $\sigma _2(z, z) \sim _R \sigma _2(z, z)$: immediate from zRz.

Therefore all three of these variables are related by a bisimulation up to presentation.

3.2 Enhanced Bisimulation Up to Presentation

In Example 8, we showed two variables in a specification were related by a bisimulation up to presentation, but in the course of this proof we added in the diagonal relation to make the bisimulation hypothesis go through. This is reminiscent of other combination bisimulation up to techniques, such as those studied by Rot et al. in [13]. In this section, we provide several enhancements to the bisimulation up to presentation technique which will be useful in the sequel.

First we note bisimulation up to presentation interacts well with union of bisimulations.

Lemma 1

Suppose (X, d) is a specification for a finitary functor presented by $(\varSigma , \epsilon )$. Let S be any bisimulation on X, T be a relation containing S, and R be a relation on X such that xR y implies $d(x) \sim _T d(y)$. Then $R\cup S$ also has the property that $(x, y) \in R \cup S$ implies $d(x) \sim _T d(y)$.

Proof

Since S is a bisimulation on X, it is also a bisimulation up to presentation by Theorem 1. Then by Theorem 2, xSy implies $d(x) \sim _S d(y)$. Since $S \subseteq T$, we have $c(S) \subseteq c(T)$ and therefore $\sim _S\ \subseteq \ \sim _T$. Hence xSy implies $d(x) \sim _T d(y)$. Combining this with the hypothesis on R, we have the desired result.

Corollary 2

Recall that $\sim$ is the biggest F-bisimulation on X. If R is a relation on a specification such that any of the following hold:

• $x R y \rightarrow d(x) \sim _{R \cup \varDelta _X} d(y)$

• $x R y \rightarrow d(x) \sim _{R \cup \sim } d(y)$

then $R \subseteq \ \sim$.

Proof

Both $\varDelta _X$ and $\sim$ are bisimulations so by Lemma 1, taking $T = R \cup B$ where $B \in \{\varDelta _X, \sim \}$, we get a relation T such that $xTy \rightarrow d(x) \sim _T d(y)$. Then T is a bisimulation up to presentation by Theorem 2, so $R \subseteq T \subseteq \ \sim$.

Bisimulation up to presentation also behaves well with respect to symmetric closures:

Lemma 2

Suppose (X, d) is a specification for a finitary functor presented by $(\varSigma , \epsilon )$. Let T be any symmetric relation and R be any relation on X such that xR y implies $d(x) \sim _T d(y)$. Then s(R), the symmetric closure of R, also has the property $x\ s(R)\ y$ implies $d(x) \sim _T d(y)$.

Proof

It is easy to check that T symmetric implies c(T) symmetric, which in turn implies $\sim _T$ symmetric. Then if $x\ s(R)\ y$, either xR y or yR x by definition of s(R). The hypothesis on R yields $d(x) \sim _T d(y)$ or $d(y) \sim _T d(x)$, respectively. Then $\sim _T$ symmetric allows us to conclude that in either case $d(x) \sim _T d(y)$, as desired.

Corollary 3

If R is a relation such that $x R y \rightarrow d(x) \sim _{s(R)} d(y)$, then $R \subseteq \ \sim$.

Bisimulation up to presentation for functors preserving weak pullbacks also plays well with equivalence closures. Preservation of weak pullbacks is a critical assumption here. We recall the following definition and theorem from [14, p. 14], slightly recast to use our notation:

Definition 3

A presentation is dominated if for every $\epsilon$ law $f(\varvec{x}) =_\epsilon g(\varvec{y})$ where $f \in \varSigma _n$, $g \in \varSigma _m$, $\varvec{x}: n \rightarrow X$, $\varvec{y}: m \rightarrow X$, there is a symbol $h \in \varSigma _k$ and functions $u: k \rightarrow n$ and $v: k \rightarrow m$ such that $h(u) =_\epsilon f(id_n)$, $h(v) =_\epsilon g(id_m)$, and $\varvec{x}\circ u = \varvec{y}\circ v$.

To give some intuition for dominated presentations, consider the presentation for $\mathcal{P}_\omega$ from Example 3. We could say the symbol $\sigma _4$ dominates the symbol $\sigma _2$ since there is a $u: 4 \rightarrow 2$, namely $u(i) = \lfloor \frac{i}{2}\rfloor$, such that $\sigma _4(u) = \sigma _4(0, 0, 1, 1) =_\epsilon \sigma _2(0, 1) = \sigma _2(id_2)$. Then any time we have a term using $\sigma _2$, we could replace $\sigma _2$ with $\sigma _4$, following the substitution scheme hinted at by u, and remain in the same component of the kernel of $\epsilon$. So, for example, this domination would imply $\sigma _2(x, y) =_\epsilon \sigma _4(x, x, y, y)$.

Note $\sigma _3$ is also dominated by $\sigma _4$, for example by $\sigma _3(0, 1, 2) = \sigma _4(0, 2, 1, 1)$. This would allow us to rewrite $\sigma _3(x, y, x) =_\epsilon \sigma _4(x, x, y, y)$. Combining with the previous paragraph would allow us to derive $\sigma _3(x, y, x) = \sigma _2(x, y)$ via rewrites to $\sigma _4$. We can then say that $\sigma _3(x, y, x) =_\epsilon \sigma _2(x, y)$ is a consequence of the joint domination of $\sigma _2$ and $\sigma _3$ by $\sigma _4$.⁵

The verbiage for all this notation then is that a presentation is dominated means for every $\epsilon$ law $f(\varvec{x}) =_\epsilon g(\varvec{y})$ there is a dominating symbol h with two variable substitutions u and v such that the $\epsilon$ law is a consequence of the joint domination of f and g by h via the substitutions u and v. We will be relying on facts about dominated presentations only in the proof of Lemma 3.

Theorem 3

(Adámek, Gumm, Trnková). A finitary functor weakly preserves pullbacks if and only if it has a dominated presentation.

As a result of this theorem, for the next lemmas we can assume our presentation is dominated without loss of generality.

Lemma 3

Suppose T is an equivalence relation and $(\varSigma , \epsilon )$ is a dominated presentation. Then $\sim _T$ is an equivalence relation.

Proof

Reflexivity and symmetry are straightforward. T is reflexive and symmetric, therefore c(T) is reflexive and symmetric, and so $=_\epsilon \bullet \ c(T)\ \bullet =_\epsilon$ is reflexive and symmetric.

Transitivity requires the dominated presentation. Suppose $\alpha \sim _T \beta \sim _T \gamma$. Then we can write

$$\begin{aligned} \alpha =_\epsilon \alpha '\ c(T)\ \beta ' =_\epsilon \beta =_\epsilon \beta ''\ c(T)\ \gamma ' =_\epsilon \gamma \end{aligned}$$

Let $\beta ' = f(\varvec{x})$ and $\beta '' = g(\varvec{y})$. Then the above relations become:

$$\begin{aligned} \alpha =_\epsilon f(\varvec{x'})\ c(T)\ f(\varvec{x}) =_\epsilon g(\varvec{y})\ c(T)\ g(\varvec{y'}) =_\epsilon \gamma \end{aligned}$$

Since we have a dominated presentation, we get h, u, and v such that $h(u) =_\epsilon f(id_n)$, $h(v) =_\epsilon g(id_m)$ and $\varvec{x} \circ u = \varvec{y} \circ v$. The first two statements imply $f(\varvec{x'}) =_\epsilon h(\varvec{x'}\circ u)$ and $g(\varvec{y'}) =_\epsilon h(\varvec{y'}\circ v)$.

We also know $\varvec{x'}(i)\ T\ \varvec{x}(i)$ for all $i \in [1, n]$ and $\varvec{y}(i)\ T\ \varvec{y'}(i)$ for $i \in [1, m]$. Therefore, $(\varvec{x'} \circ u)(i)\ T\ (\varvec{x}\circ u)(i) = (\varvec{y}\circ v)(i)\ T\ (\varvec{y'}\circ v)(i)$ for $i \in [1,k]$, where the middle equality is by the last condition guaranteed by the dominated presentation. Then since T is transitive we know $(\varvec{x'}\circ u)(i)\ T\ (\varvec{y'}\circ v)(i)$ for $i \in [1, k]$.

Therefore we have produced terms such that

$$\begin{aligned} \alpha =_\epsilon h(\varvec{x'}\circ u)\ c(T)\ h(\varvec{y'}\circ v) =_\epsilon \gamma \end{aligned}$$

and so $\sim _T$ is transitive and hence is an equivalence relation.

Lemma 4

Suppose (X, d) is a specification for a finitary functor preserving weak pullbacks with the dominated presentation $(\varSigma , \epsilon )$. Let T be any equivalence relation on X and R be any relation on X such that xR y implies $d(x) \sim _T d(y)$. Then e(R), the equivalence closure of R, has the property $x\ e(R)\ y$ implies $d(x) \sim _T d(y)$.

Proof

By Lemmas 1 and 2, we know immediately that x sr(R) y implies $d(x)~\sim _T~d(y)$, where sr(R) is the symmetric reflexive closure of R. Hence we only have to consider $(x, y) \in e(R) \backslash sr(R)$. Therefore, suppose we have $x\ sr(R)\ z\ sr(R)\ y$. Then by the noted property of sr(R) we get $d(x) \sim _T d(z) \sim _T d(y)$. By the previous Lemma, since T is an equivalence relation and we have a dominated presentation, $\sim _T$ is an equivalence relation and hence $d(x) \sim _T d(y)$.

Corollary 4

Suppose F preserves weak pullbacks and its presentation $(\varSigma , \epsilon )$ is dominated. If R is a relation such that xRy implies $d(x) \sim _{e(R)} d(y)$, then $R \subseteq \ \sim$.

The following corollary follows directly from the results above, but is of critical importance to our proof of soundness.

Corollary 5

Suppose F preserves weak pullbacks and its presentation $(\varSigma , \epsilon )$ is dominated. If R is a relation such that xRy implies $d(x) \sim _{e(R\cup \sim )} d(y)$, then $R \subseteq \ \sim$.

4 A Proof System for Bisimulation Up to Presentation

In this section, we outline a formal proof system to capture the notion of bisimulation up to presentation. For this whole section, we assume F preserves weak pullbacks. We then prove this system to be sound and complete. Our system has judgements of the form $R \vdash \sigma = \tau$ where $R \subseteq X \times X$ and $(\sigma , \tau ) \in X \times X + H_\varSigma X \times H_\varSigma X$. The inference rules are as follows:

As usual, we say $R \vdash \varphi$ when there is a proof tree using the above rules with the judgement $R \vdash \varphi$ as the root. The notation $\vdash \varphi$ is shorthand for $\varnothing \vdash \varphi$. Recall that $\vDash x = y$ means that x and y are behaviourally equivalent (have the same image in the final coalgebra).

We should point out that R on the left side of the turnstile does not have the usual force of a full assumption. Rather, this R should be thought of as tracking unverified bisimulation hypotheses. In most rules this unverified bisimulation remains on both sides, except the axioms and the b rule, which essentially discharges a verified bisimulation from the left hand side. This b rule is probably the least intuitive, but is really just the coinductive proof principle. We also note its similarity to the Recursion Inference Rule from FLR$_0$, which was in mind as the system was constructed. [15]

Before we prove soundness and completeness, we give two example proofs using the system. This first example is based on Example 4.2 in Moss et al. [3].

Example 10

Consider the specification on $X = \{x, y, r, s\}$ for $\mathcal{P}_3$ defined by

$$\begin{aligned} d(x) = \sigma _2(x, y)&d(y) = \sigma _0&d(r) = \sigma _2(r, s)&d(s) = \sigma _0 \end{aligned}$$

Let $R = \{(x, r), (y, s)\}$. The proof tree below witnesses $\vdash x = r$.

The next example is adapted from Example 9 in this paper and showcases how some rules allow for shorter proofs.

Example 11

Consider the specification on $X = \{x, y\}$ for $\mathcal{P}_3$ defined by

$$\begin{aligned} d(x) = \sigma _2(x, y)&d(y) = \sigma _1(x) \end{aligned}$$

Let $R = \{(x, y)\}$. The proof tree below witnesses $\vdash x = y$.

Note that R contains a single pair though an unenhanced bisimulation proof would require three: the r rule allows us to omit (x, x), and the s rule elides the mirror-image proof that $d(y) = d(x)$ thereby allowing us to omit (y, x).

4.1 Soundness

To help with our soundness proof, we define a new relational closure which we call the presentational closure of a relation $R \subseteq X \times X$ on the carrier of a specification (X, d). Recall from Sect. 3 that $\sim _R$ is defined to be $=_\epsilon \bullet \ c(R)\ \bullet =_\epsilon$. That is, $\alpha \sim _R \beta$ if we can rewrite $\alpha$ and $\beta$ using $\epsilon$ laws so they have the same function symbol and all corresponding variables are related by R. The presentational closure of R, denoted pr(R), is defined to be $pr(R) \triangleq e(R\cup {\sim }) + \sim _{e(R\cup \sim )}$, a relation on $X + H_\varSigma X$.

We note that $e(R\cup {\sim })$ is an equivalence relation on X, and $\sim _{e(R\cup \sim )}$ is an equivalence relation on $H_\varSigma X$ as a consequence. Since X and $H_\varSigma X$ are disjoint, pr(R) is also an equivalence relation.

Proposition 1

If $R \vdash \varphi$, then $\varphi \in pr(R)$.

Proof

By induction on the proof tree. The base cases are r, $\epsilon$, and a. We know pr(R) is an equivalence relation, hence r. The relation $e(R\cup {\sim })$ is reflexive, hence $\sim _{e(R\cup {\sim })}$ contains the relation $=_\epsilon$, hence $\epsilon$. All pairs in R are included in $e(R\cup {\sim })$, hence a.

The induction steps are s, t, c, and b. s and t follow easily from the fact that pr(R) is an equivalence relation.

Suppose for all $1 \le i \le ar(f)$, we know $(x_i, y_i) \in pr(R)$ and hence $(x_i, y_i) \in$ $e(R\cup {\sim })$. By definition of the flat contextual closure, $f(x_1, \ldots , x_{ar(f)})$ $c(e(R \cup {\sim }))\ f(y_1, \ldots , y_{ar(f)})$. Since $=_\epsilon$ is a reflexive relation, pr(R) contains c(R) and hence these two terms are related by pr(R). Therefore the induction holds across the c rule.

Finally we consider the b rule, which allows one to discharge bisimulations from the left hand side. The induction hypothesis gives $\varphi \in pr(R)$ and $(d(x), d(y)) \in pr(R)$ for each $(x, y) \in R$. Since $d(x), d(y) \in H_\varSigma X$ we know $d(x) \sim _{e(R\cup \sim )} d(y)$. Then by Corollary 5, we know $R \subseteq \ \sim$. Therefore, $pr(R) = e(R\cup {\sim }) + \sim _{e(R\cup \sim )} = e(\sim ) + \sim _{e(\sim )} = pr(\varnothing )$. Then $\varphi \in pr(\varnothing )$ since $\varphi \in pr(R)$.

Corollary 6

(Soundness). If $\vdash x = y$, then $\vDash x = y$.

Proof

If $\vdash x = y$, then $(x, y) \in e({\sim }\cup \varnothing )$ by the previous proposition. However, clearly $e({\sim } \cup \varnothing ) = e(\sim ) =\ \sim$, so $x \sim y$. A standard fact about functors preserving weak pullbacks is that two states in a coalgebra are bisimilar if and only if they are behaviourally equivalent [9], so $x \sim y$ implies $\vDash x = y$.

4.2 Completeness

Lemma 5

If $\alpha \sim _R \beta$, then $R \vdash \alpha = \beta$.

Proof

$\alpha \sim _R \beta$ means there are $f \in \varSigma _n$ and $(x_1, y_1), \ldots , (x_n, y_n) \in R$ such that

$$\begin{aligned} \alpha =_\epsilon f(x_1, \ldots , x_n)\ c(R)\ f(y_1, \ldots , y_n) =_\epsilon \beta . \end{aligned}$$

then

is a witness for $R \vdash \alpha = \beta$.

Corollary 7

(Completeness). If $\vDash x = y$, then $\vdash x = y$.

Proof

Recall that $\vDash x = y$ iff $x \sim y$. Since x and y are bisimilar, they are related by a bisimulation up to presentation, which we call R. By Theorem 2, $uRv \rightarrow d(u) \sim _R d(v)$. Syllogizing with the previous lemma yields $uRv \rightarrow (R \vdash d(u) = d(v))$. Trivially, $R \vdash x = y$ by the a rule. Therefore, $\vdash x = y$ by the b rule.

5 Compositionality of Presentations

Bisimulations up to presentation give a uniform way to reason about behavioural equivalence of variables in specifications for finitary functors, but there is a potential disadvantage. Certain inductive classes of functors have sound, complete, and compositional proof systems. That is, the rules for reasoning about coalgebras of a functor are built inductively in a manner corresponding to the definition of the functor. The prime example of this situation is that of the polynomial functors and the Kripke polynomial functors.

A functor is called polynomial if it is generated by the following BNF grammar:

$$\begin{aligned} P {:}{:}= A\ |\ Id\ |\ P + P\ |\ P \times P\ |\ P^B \end{aligned}$$

where A is the constant functor having value $A \in Set$ and B is a finite set. The Kripke polynomial class of functors adds the finite powerset functor:

$$\begin{aligned} K {:}{:}= A\ |\ Id\ |\ P_\omega (K) |\ K + K\ |\ K \times K\ |\ K^B \end{aligned}$$

Bonsangue et al. build a sound, complete and compositional expression calculus to represent coalgebras of Kripke polynomial functors in [5]. We show presentations are similarly compositional, in that both the signature and the $\epsilon$ transformation can be built inductively to parallel the construction of the functor. For the following three constructions, suppose F and G are finitary functors with presentations $(\varSigma , \epsilon )$ and $(\varSigma ', \epsilon ')$.

5.1 Products

Let $J = F \times G$. Then we claim J has a presentation $(\varSigma '', \epsilon '')$ where $\varSigma ''$ has all pairs of symbols, $\varSigma _n'' = \{(f, g): f \in \varSigma , g \in \varSigma ', ar(f) + ar(g) = n\}$, and $\epsilon '': H_{\varSigma ''} \rightarrow J$ has components

$$\begin{aligned} \epsilon _X'': (f, g)(x_1, \ldots , x_n) \mapsto (\epsilon _X(f(x_1, \ldots , x_{ar(f)})), \epsilon _X'(g(x_{ar(f)+1}, \ldots , x_n))). \end{aligned}$$

Then $\epsilon ''$ is an epic natural transformation as a consequence of $\epsilon$ and $\epsilon '$ being epic natural transformations.

We single out this particular presentation because it allows us to state the $\epsilon ''$ laws in terms of $\epsilon$ and $\epsilon '$ laws. By definition $\epsilon ''((f, g)(x_1, \ldots , x_n)) = \epsilon ''((f', g')(y_1, \ldots y_m))$ means

$$\begin{aligned} \epsilon (f(x_1, \ldots , x_{ar(f)}))&= \epsilon (f'(y_1, \ldots , y_{ar(f')})) \text { and} \\ \epsilon '(g(x_{ar(f)+1}, \ldots , x_n))&= \epsilon '(g'(y_{ar(f')+1}, \ldots , y_m)). \end{aligned}$$

Therefore, $\epsilon ''$ laws in this presentation are pairs of $\epsilon$ and $\epsilon '$ laws.

We note here that we could represent finite powers with a similar construction. If B is a finite set, a signature for $F^B$ has symbols |B| tuples of symbols from $\varSigma$ with arity the sum of the arities through the tuple. Then the $\epsilon ''$ laws are |B| tuples of $\epsilon$ laws.

5.2 Coproducts

Let $J = F + G$. We write $S + T = \{\mathsf {inl}s: s \in S\}\cup \{\mathsf {inr}t: t \in T\}$. Then J has a presentation $(\varSigma '', \epsilon '')$ where $\varSigma _n'' = \varSigma _n + \varSigma '_n$ and $\epsilon ''$ has components $\epsilon _X''$ such that ${\left\{ \begin{array}{ll} \epsilon _X''(\mathsf {inl}f(\varvec{x})) = \mathsf {inl}\epsilon _X(f(\varvec{x})) \\ \epsilon _X''(\mathsf {inr}g(\varvec{x})) = \mathsf {inr}\epsilon _X'(g(\varvec{x}))\end{array}\right. }$. Since $\epsilon$ and $\epsilon '$ are epic natural transformations, $\epsilon ''$ is also an epic natural transformation.

Again, we can state the $\epsilon ''$ laws in terms of the $\epsilon$ and $\epsilon '$ laws. By definition, $\epsilon ''\alpha = \epsilon ''\beta$ means $\alpha$ and $\beta$ are both labelled $\mathsf {inl}$ or are both labelled $\mathsf {inr}$. In the former case, we have $\mathsf {inl}\epsilon (f(\varvec{x})) = \mathsf {inl}\epsilon (g(\varvec{y}))$, which is an $\mathsf {inl}$-labelled instance of an $\epsilon$-law. Similarly, the latter case gives an $\mathsf {inr}$-labelled instance of an $\epsilon '$-law.

5.3 Compositions

Let $J = G\circ F$. Then J has a presentation with symbols from the set $\varSigma '' = \{(\sigma ', (\sigma _1, \ldots , \sigma _{ar(\sigma ')})) : \sigma ' \in \varSigma ' \text { and } \sigma _i \in \varSigma \}$. For each symbol $\sigma '' \in \varSigma ''$ define $w_{\sigma ''}(i) = \sum _{j = 1}^i ar(\sigma _i)$ for $0 \le i \le ar(\sigma ')$ and define $\sigma ''$ to have arity $w_{\sigma ''} = w_{\sigma ''}(ar(\sigma '))$. Given an $ar(\sigma '')$ tuple from X, we let $\varvec{x}_i = (x_{w_{\sigma ''}(i-1)+1}, \ldots , x_{w_{\sigma ''}(i)})$ for $1 \le i \le ar(\sigma ')$, the slice of the variables corresponding to $\sigma _i$. The natural transformation $\epsilon ''$ has components given by

$$\begin{aligned} \epsilon '': \sigma ''(x_1, \ldots , x_{ar(\sigma '')}) \mapsto \epsilon '(\sigma '(\epsilon (\sigma _1(\varvec{x}_1)), \ldots , \epsilon (\sigma _{ar(\sigma ')}(\varvec{x}_{ar(\sigma '')})))). \end{aligned}$$

This is an epic natural transformation and the $\epsilon ''$ laws can be stated again in terms of the $\epsilon$ and $\epsilon '$ laws.

5.4 Kripke Polynomial Functors and Other Polynomial-Like Classes of Functors

We have presentations for constant functors (Example 1), the identity functor (Example 2) and the finite power set functor (Example 3), which means the above constructions give a compositional presentation for each of the Kripke polynomial functors. Due to the previous section, we know bisimulation up to those presentations is a sound and complete proof system.

Example 12

Consider the functor $F = A \times \text {Id}^B$ where B is finite. Following the constructions above, F has a presentation with function symbols $\varSigma = \varSigma _{|B|} = \{(a, \beta ): a \in A, \beta : B \rightarrow \{*\}\}$ and equations $\epsilon ((a,\beta )(\varvec{x})) = \epsilon ((a', \beta ')(\varvec{x'}))$ iff $a = a'$ and $\varvec{x} = \varvec{x'}$. Since there is only one function $\beta : B \rightarrow \{*\}$, we might as well omit that part of the function symbol and abbreviate $(a, \beta )$ by just a, still with arity |B|.

Suppose we had a specification in this signature, like

$$\begin{aligned} d(x) = a(\overbrace{x, \ldots , x}^{|B|})&d(y) = a(\overbrace{z, \ldots , z}^{|B|})&d(z) = a(\overbrace{y, \ldots , y}^{|B|}) \end{aligned}$$

The complete relation on $\{x, y , z\}$ is a bisimulation up to presentation for this specification, since for each pair of variables, all corresponding variable pairs in the definitions are in the relation. Hence we can conclude these variables all have the same image in the final coalgebra.

The constructions above generalize previous results about inductive classes of functors since they assure us a compositional proof system exists for any inductive class using any of those formation rules.

6 Conclusion and Future Directions

In this paper, we presented a sequent-style deduction system for reasoning about behavioural equivalence of points in coalgebras and specifications of finitary functors in Set. This system was based on a relaxed version of $H_\varSigma$-bisimulations which nicely coincide with F-bisimulations called bisimulations up to presentation. We demonstrated this proof system was sound and complete for finitary functors preserving weak pullbacks. We also demonstrated that three common operations on functors have uniform effects on both the signature and equations in a presentation.

One restriction in our setting we would like to remove is the totality restriction. Since our specifications are defined with a (total) function, there is exactly one related coalgebra and each variable has exactly one interpretation in a final coalgebra. This makes strong soundness and completeness results decidedly less satisfying—either the assumptions are true or false of the single model of the specification. By removing the totality restriction, we could get more meaningful strong soundness and completeness.

Another more practical advantage of partial specifications is the ability to detect equality even in circumstances where values of certain variables are not known or are irrelevant. For example, from

$$\begin{aligned} d(x) = 1:\text {zip}(y, z)&d(y) = 1:\text {zip}(x, z) \end{aligned}$$

we would like to be able to conclude $\vDash x = y$ even if the value of z is not specified.

We implicitly used the fact that finitary functors have flat presentations. That is, each point in FX is an image of a point in $H_\varSigma X$ and all equations necessary for the presentation are between flat terms. Flat signatures are not always the most natural though, sometimes one would like to use zip terms like $0:\text {zip}(1:x, \text {zip}(y, y))$, where we have three function symbols: $\varSigma _1 = \{0:, 1:\}$ and $\varSigma _2 = \{\text {zip}\}$. Then some non-flat equations are necessary to capture all the truths of the system. How many more modifications are necessary to deal successfully with specifications in $X \rightarrow T_\varSigma X$ instead of $X \rightarrow H_\varSigma X$?

We are also interested in contexts beyond Set, particularly Vect. Milius [6] extended the expression calculi of Bonsangue et al. [4, 5] to vector space coalgebras of the functor $FX = \mathbb R\times X$, providing a sound and complete system for reasoning about stream circuits. We have some hope that by combining our approach with the general definition of signature from Kelly and Power [16] we might be able to devise a system usable in more categories than Set.

There are also a couple of generic questions suggested by this work. Here we utilized the quotient relationship $\epsilon : H_\varSigma \twoheadrightarrow F$ to relate $H_\varSigma$- and F-bisimulations. Do other relationships between functors yield interesting interplay between their coalgebras? Additionally, many of the results here suggest a connection to bisimulation up to literature. How does bisimulation up to presentation fit into the theory of enhanced bisimulations?