Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

• Username
• Password
• Remember me

• Sign in using OpenID
• Remember me

• Forgot your password?
• Apply for membership

2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry book bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology colimits combinatorics complex complex-geometry computable-mathematics computer-science constructive cosmology deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration foundation foundations functional-analysis functor gauge-theory gebra geometric-quantization geometry graph graphs gravity grothendieck group group-theory harmonic-analysis higher higher-algebra higher-category-theory higher-differential-geometry higher-geometry higher-lie-theory higher-topos-theory homological homological-algebra homotopy homotopy-theory homotopy-type-theory index-theory integration integration-theory k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure-theory modal modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology nforum nlab noncommutative noncommutative-geometry number-theory of operads operator operator-algebra order-theory pages pasting philosophy physics pro-object probability probability-theory quantization quantum quantum-field quantum-field-theory quantum-mechanics quantum-physics quantum-theory question representation representation-theory riemannian-geometry scheme schemes set set-theory sheaf sheaves simplicial space spin-geometry stable-homotopy-theory stack string string-theory superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory tqft type type-theory universal variational-calculus

1. • CommentRowNumber1.
   • CommentAuthorTobyBartels
   • CommentTimeSep 4th 2011
   • PermaLink
   Author: TobyBartels
   Format: MarkdownItexInspired by Todd's work at [[well-founded relation]], I've written [[simulation]].

   Inspired by Todd’s work at well-founded relation, I’ve written simulation.

2. • CommentRowNumber2.
   • CommentAuthorDavid_Corfield
   • CommentTimeSep 5th 2011
   • PermaLink
   Author: David_Corfield
   Format: MarkdownItexWhat'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.

   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.

3. • CommentRowNumber3.
   • CommentAuthorTobyBartels
   • CommentTimeSep 5th 2011
   • PermaLink
   Author: TobyBartels
   Format: MarkdownItexI'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$).

   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$).

4. • CommentRowNumber4.
   • CommentAuthorDavid_Corfield
   • CommentTimeSep 5th 2011
   • PermaLink
   Author: David_Corfield
   Format: MarkdownItexThis paper should be useful - [Relating coalgebraic notions of bisimulation](http://arxiv.org/abs/1101.4223). > 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 > defining 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](http://www.cs.unibo.it/~sangio/DOC_public/history_bis_coind.pdf) seems interesting too.

   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

   defining 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.

5. • CommentRowNumber5.
   • CommentAuthorTodd_Trimble
   • CommentTimeSep 5th 2011
   • (edited Sep 5th 2011)
   • PermaLink
   Author: Todd_Trimble
   Format: MarkdownItexI 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.

   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.

6. • CommentRowNumber6.
   • CommentAuthorTobyBartels
   • CommentTimeSep 5th 2011
   • (edited Sep 5th 2011)
   • PermaLink
   Author: TobyBartels
   Format: MarkdownItexIf 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](http://en.wikipedia.org/wiki/Simulation_preorder). As for a *bi*simulation, 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.)

   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.)

7. • CommentRowNumber7.
   • CommentAuthorTodd_Trimble
   • CommentTimeSep 5th 2011
   • (edited Sep 5th 2011)
   • PermaLink
   Author: Todd_Trimble
   Format: MarkdownItexI 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.

   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.

8. • CommentRowNumber8.
   • CommentAuthorDavid_Corfield
   • CommentTimeSep 5th 2011
   • PermaLink
   Author: David_Corfield
   Format: MarkdownItexBisimulation 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](http://blog.sigfpe.com/2006/04/mongruences.html). 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](http://ncatlab.org/nlab/show/corecursion). 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.

   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.

9. • CommentRowNumber9.
   • CommentAuthorTodd_Trimble
   • CommentTimeSep 5th 2011
   • (edited Sep 5th 2011)
   • PermaLink
   Author: Todd_Trimble
   Format: MarkdownItexHm, 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.

   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.

10. • CommentRowNumber10.
    • CommentAuthorTodd_Trimble
    • CommentTimeSep 5th 2011
    • PermaLink
    Author: Todd_Trimble
    Format: MarkdownItexI 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.

    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.

11. • CommentRowNumber11.
    • CommentAuthorMike Shulman
    • CommentTimeSep 6th 2011
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexAs David pointed out in his [comment](http://blog.sigfpe.com/2006/04/mongruences.html?showComment=1253286262790#c1774155624376898219) 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?

    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?

12. • CommentRowNumber12.
    • CommentAuthorTobyBartels
    • CommentTimeSep 7th 2011
    • PermaLink
    Author: TobyBartels
    Format: MarkdownItexThat sounds good.

    That sounds good.