Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
Inspired by Todd’s work at well-founded relation, I’ve written simulation.
What’s the best way to define the important bisimulation notion? A morphism with an inverse for which both are simulations? We have an uninformative bisimulation page.
I’m not sure, but I’ll note that the two times that we define the term in the Lab, at pure set and at extensional relation, the former is more general (but both are for the case for the functor is the power set functor on $Set$).
This paper should be useful - Relating coalgebraic notions of bisimulation.
In this article, we identify four notions of bisimulation that have been proposed in the coalgebraic context
and there are two more notions not treated
deﬁning an equivalence relation on the class of all coalgebras, by setting two coalgebras as bisimilar if there is a span of surjective homomorphisms between them. Others work with relations as bimodules.
On the Origins of Bisimulation and Coinduction seems interesting too.
I haven’t satisfactorily worked out these discrepancies either, but I had noted some of them also (Paul Taylor in his book uses one notion, and Joyal-Moerdijk in Algebraic Set Theory use a different one).
I haven’t looked at Sam Staton’s paper yet (mentioned by David Corfield). But in pondering the discrepancy between Taylor and Joyal-Moerdijk, my impression is that J-M were passing from (well-founded) trees to extensional material sets by localizing with respect to the class of surjective simulations understood in Taylor’s sense, and this would give a way to reconcile the discrepancies.
In more detail, J-M in effect (but using different language) define a simulation from a tree $S$ to a tree $T$ to be a span
$S \leftarrow E \to T$where the left arrow is a surjective coalgebra map and the right arrow is a coalgebra map. (Coalgebras over/of $P$, of course.) This looks like a way of describing the category of fractions of the category of coalgebras, localized at the class of surjective coalgebra maps. Note that this definition looks more like the one given at pure set – at pure set one defines a bisimulation to be a certain relation, not a span, but if I’m not mistaken, one can factor a bisimulation span through a bisimulation relation. (Here, a bisimulation span is a span where both arrows are surjective coalgebra maps. Or, if you prefer, where both the span and its opposite are simulations in the J-M sense.) The point is that this localization would give a way of identifying, for example, $\{a, a, b, c\}$ with $\{a, b, c, c\}$ – both map surjectively to the same thing, $\{a, b, c\}$.
In an extensional conception of set, where $\{a, a, b, c\}$ is already identified with $\{a, b, c\}$, we don’t have to perform the localization trick, so there we can straight away describe a simulation as just a coalgebra map.
If the coalgebras in question are coalgebras of the power-set functor $\mathcal{P}$, then already $\{a,a,b,c\}$ and $\{a,b,c,c\}$ are identified with $\{a,b,c\}$ as elements of $\mathcal{P}(X)$, so that explains why I wanted to say at simulation that a simulation is simply a coalgebra morphism. Perhaps I should have said something more general. (I don’t know how to fit into this framework, nor understand what’s going with in the first place, the simulations in state transition systems.
As for a bisimulation, that still feels more like a relation or span, thus rather different from a simulation. Offhand, Staton’s first definition seems the most natural. But I don’t really know what they’re for in general. (I have now put Staton’s paper on the page bisimulation without comment.)
I think what I meant was that the two $a$’s are to be two copies of the same tree, so that $\{a, a, b, c\}$ would admit a nontrivial automorphism.
But let me think some more – while thinking over this reply, I think I uncovered an internal confusion in myself.
Bisimulation is an equivalence relation for processes, which you can use to prove things by coinduction. You can see Dan Piponi struggle with the asymmetry of induction and coinduction here. In a comment at the end, I mention a proof that in the extended natural numbers $m + n = n + m$. You can define predecessor behaviour for terms of each form, i.e., define ’add’ in two ways here. Then as the extended natural numbers are the classes of the coarsest equivalence relation under predecessor, you know that commutativity must hold, as $m+n$ and $n+m$ must fall into the same class with its single element since there can’t be further coarsening.
Hm, I think my confusion might have been this. The category of trees is a topos, so has a covariant power-object functor $P$. I was stupidly thinking of a tree $T$ as having a canonical “membership” relation of the form $T \to P(T)$. (Of course for any object in any topos we do have such a map, for example the classifying map of the diagonal subobject $T \to T \times T$. But that’s not the thing I meant to consider.)
The membership relation on a tree is actually a subobject of $T \times s^\ast(T)$. Here I am identifying the category of trees with the category of forests $Set^{\omega^{op}}$ where $\omega$ is the first infinite ordinal. We have a successor operation $s: \omega \to \omega$, and $s^\ast$ denotes the pullback functor $Set^{s^{op}}$. The subobject $R \hookrightarrow T \times s^{\ast}(T)$ I wanted to consider consists of subsets $R(n) \hookrightarrow T(n) \times T(n+1)$, consisting of pairs of nodes $(x, y)$ where $y$ at height $n+1$ is an immediate predecessor of $x$ at height $n$ in the tree $T$.
Thus, I want to think of each tree as having a canonical coalgebra structure not over the endofunctor $P$, but rather over the endofunctor $P s^\ast$. With that replacement, I hope that repairs what I was saying earlier.
I have now added a new subsection to simulation, Open maps in algebraic set theory, to record part of what I was saying in comments above (mostly, my last comment). Please have a look.
As David pointed out in his comment on Dad Piponi’s blog, induction and coinduction are dual once you remember that the dual of a subobject is a quotient, and that (in an exact category) quotients can be identified with equivalence relations.
In particular, we could consider dualizing everything at well-founded coalgebra. If T is an endofunctor and $\theta\colon T X \to X$ a T-algebra, then a quotient $e\colon X\twoheadrightarrow Q$ is coinductive if in the pushout
$\array{ T X & \overset{T e}{\to} & T Q\\ ^\theta \downarrow & & \downarrow\\ X & \underset{p}{\to} & K}$the map $p$ factors through $e$. If the category is exact, then $e$ and $p$ are determined respectively by equivalence relations $\sim_e$ and $\sim_p$, and $p$ factors through $e$ just when $\sim_e$ is contained in $\sim_p$. Finally, $X$ is well-cofounded if the only coinductive quotient is itself.
If X is a fixed point of T, so that $\theta$ is an isomorphism, then $\theta^{-1}\colon X\to T X$ tells us how to deconstruct an element of X into a constructor applied to some arguments, and the morphism $T e\colon T X \to T Q$ applies $e$ to each of the arguments of a constructor-with-arguments. Therefore, $\sim_e$ is contained in $\sim_p$ if whenever two elements of X are $\sim_e$-related, then upon destructing them into a constructor applied to arguments, each corresponding pair of arguments is also $\sim_e$-related.
This looks to me exactly like a bisimulation (plus the assumption of being an equivalence relation) – thus “well-cofounded” could also be called “extensional”. Maybe this is one good general definition of “bisimulation”? It does require us to consider only equivalence relations, but does one frequently encounter bisimulations that are not equivalence relations?
That sounds good.
1 to 12 of 12