Bisimulations of enrichments

Krzysztof Worytkiewicz; Vincent Schmitt

REVIEW

Bisimulations of enrichments

Logic in Computer Science · Submitted 21 Feb 2006 · 15 references

Pith's verdict: A genuinely useful categorical unification of bisimulation, with one real gap in the span characterization that needs fixing before publication.

T0 · AI review

How this review was made: An AI referee (deepseek-v4-flash) read the paper on August 28, 2026 and answered a fixed list of questions about it. T0 is the starting level every paper gets. The levels describe how deeply Pith has checked the paper, never the authors.

T0 AI review An AI read the paper and answered a fixed list of questions.
T1 Audit Automatic checks that the references and files the paper relies on exist and match.
T2 Compute The paper's code or calculations re-run with the same results.
T3 Formal statement The claims written out in a formal math language a computer can read.
T4 Proof Those claims proved, and the proof checked by computer.

How Pith checks papers →

· 2 major objections · 4 minor · Ask about this paper · The compiled record · Read the full review →

Challenge this review Comment (0) Read on arXiv ↗

Cite ▾

arXiv IDcs/0602077 (version 1)

Pith ID5W6EOWFX, Pith's permanent record of this paper and its review

CitationKrzysztof Worytkiewicz, Vincent Schmitt. "Bisimulations of enrichments." arXiv:cs/0602077 (2006). https://pith.science/paper/5W6EOWFX

Cite this reviewBibTeX for Pith's review of this paper

Claim paper

Why Pith says this

Highlight any text to comment on it.

Editor's note

read the letter

You should know this one for what it is: a clean, category-theoretic generalization of simulation and bisimulation to enrichments over quantaloids, with a preservation theorem for change of base. The authors are not overselling the abstract claim—most classical properties do lift. The main results are Proposition 3.3 (bisimilarity is an equivalence), the cospan characterization in Proposition 3.5, and Proposition 5.1 giving sufficient conditions for change of base to preserve surjective functional bisimulations. That last theorem is the genuinely useful piece, and it is proved. The paper also does a real service by working through Betti's generalized automata and categorical transition systems as examples.

The strongest part is the change-of-base section. The argument that any two-sided enrichment with local right adjoints preserves the class O is straightforward and correct, and the applications to functors between categories and to refinements of specifications are sensible. The axioms for O, following Joyal–Moerdijk, are checked carefully; A1, A3, A4, and A6 look right for the stated hypotheses.

Now the weak spot, and it is real but localized. Lemma 3.2, used for the span characterization in Proposition 3.6 and for the stability axiom A2, swaps an arbitrary join with a meet:

⋁_{b'} (A(a,a') ∧ B(b,b')) = A(a,a') ∧ ⋁_{b'} B(b,b').

That equality is the frame law (infinite distributivity), not finite lattice distributivity. The paper only assumes V is locally distributive, which in the intended reading—finite meets distribute over finite joins—does not justify this step. Unless 'locally distributive' is meant in the stronger frame-theoretic sense, Lemma 3.2 is unproved, and with it Prop. 3.6 and A2. That matters, but note what it does not break: Proposition 3.5 (cospans) does not use this, and Proposition 5.1 does not use it. So the central change-of-base theorem survives.

Other soft spots are minor and typical: several examples (preorders, metric spaces) are left as exercises, and the proof of Prop. 3.5 handwaves the bijection between equivalence classes. I did not find circularity or parameter-fitting; the definitions are honest and the cited prior work by the authors is used for machinery, not for the bisimulation results.

Bottom line: this paper is worth refereeing. The idea is new and the main preservation theorem is probably correct. The fix is to either strengthen the hypothesis on V (require local frames) or weaken Lemma 3.2 accordingly and state what remains of Prop. 3.6. Send it out; the referee should focus on the distributivity question and on filling in the countable details, not on rejecting the paper.

Referee report

Major objections (2)

[Section 3, Lemma 3.2 and Proposition 3.6] The proof of Lemma 3.2 uses the equality ⋁_{b′:F(a′)=G(b′)} (A(a,a′) ∧ B(b,b′)) = A(a,a′) ∧ ⋁_{b′:F(a′)=G(b′)} B(b,b′) and justifies it as 'by distributivity.' The hypothesis introduced just before Proposition 3.6 is only that the local preorders V(a,b) are distributive, which in the context of complete lattices means finite lattice distributivity. The join in the displayed equality is arbitrary (it ranges over all b′ in the fiber), so the required law is the frame law (arbitrary joins distribute over binary meets), not finite distributivity. Unless 'locally distributive' is intended in this stronger, frame-theoretic sense, Lemma 3.2 is unproved, and consequently the span characterization of bisimilarity (Proposition 3.6) and the stability axiom A2 (Proposition 3.8) are not established. Please either restate the hypothesis as complete or frame distributivity, or provide a proof using only finite distributivity.
[Section 3, Proposition 3.5] The proof of the cospan characterization is incomplete. It asserts without proof that equivalence classes for ∼ on A correspond bijectively to equivalence classes for ∼ on B. Then, to show A/∼([a],[a′]) = B/∼([b],[b′]), it says 'one may suppose (a,b)∈R and (a′,b′)∈R.' This supposition is not justified: the equivalence relation is generated by R ∘ R⁻¹, so arbitrary representatives [a] and [b] need not be directly related by R. The displayed chain proves only one inequality, and only under the stronger direct-relation assumption. A complete proof should construct the stated bijection and establish both inequalities for arbitrary representatives of the equivalence classes.

Minor objections (4)

[Throughout] The manuscript contains many typos and corrupted symbols, e.g., 'functionnal', 'bismulation', 'enrichemnts', and the arrow 'm /d47/d47 b′' in Example 2 of Section 3. A thorough copy-edit is needed before publication.
[Section 3, Examples 3 and 4] The metric-space example is left to the reader, but the decoding is not immediate: the definition of simulation uses a join in the quantaloid, and for generalized metric spaces the order on [0,∞] must be made explicit (Lawvere's convention uses [0,∞]^{op}). Without that clarification the claimed form of simulation with '+ε' is ambiguous.
[Section 4, Theorem 4.2] Theorem 4.2 is stated without proof and without a precise pointer to the literature. Since it is used later for the examples, please either supply a proof or indicate exactly where it is proved in [2] or [9].
[Section 3, Proposition 3.9] The descent axiom proof shows C(gb,c) ≤ ⋁_{b′|g(b′)=c} B(b,b′), but the reverse inequality is left implicit. It follows from B(b,b′) ≤ C(g(b),g(b′)) for V-functors, but this step should be stated for completeness.

How Pith checks papers → · Full audit of this paper →

The paper

The paper claims

The paper proves that simulation and bisimulation generalize to categories enriched over a quantaloid, and that the standard properties of bisimulation — composition, transitivity, equivalence, quotienting — are preserved.

The reading

This paper tries to establish that simulation and bisimulation, the workhorse equivalences of automata theory, can be defined for any category enriched over a quantaloid — a partially ordered universe of computations in which every family of arrows has a least upper bound. The authors show that the classical properties of bisimulation are nearly all preserved: bisimilarity is an equivalence relation, bisimulation equivalences form complete lattices, and a bisimulation quotient exists, so minimization-style reasoning works in the enriched setting. They then study the $V$-functors that correspond to functional bisimulations surjective on objects, show that they form a class very close to the classical open maps of automata theory, and give sufficient conditions under which changing the base quantaloid preserves bisimilarity. This matters because enrichments encode generalized metric spaces, preorders, Betti's generalized automata, and categorical transition systems, so the same bisimulation concept applies across all these computational models.

What carries the argument

The machinery is the definition of simulation as an inequality between a hom and the join of homs over the relation's fiber: $A(a,a') \leq \bigvee_{(a',b')\in R} B(b,b')$. A functional bisimulation is the special case where the relation is a $V$-functor $f$ and the inequality is an equality, $A(f(b),a') = \bigvee_{b': f(b')=a'} B(b,b')$, i.e. each representable hom of $A$ is the colimit of the corresponding homs of $B$ over the fiber of $f$. The span characterization turns on Lemma 3.2, where local distributivity of the quantaloid lets a join be interchanged with the meet that defines pullbacks, and this is what makes the class $O$ of surjective functional bisimulations stable under pullback. Change of base is carried by two-sided enrichments in the tricategory Caten; the preservation theorem works because local right adjoints commute with the joins in the defining equality.

Extended reading notes

Core claim

On the paper's own terms, the discovery is that the automata-theoretic notion of bisimulation has a faithful translation into enriched category theory: a simulation from a $V$-category $A$ to $B$ is a relation $R$ between objects with matching base objects such that $A(a,a') \leq \bigvee_{(a',b')\in R} B(b,b')$, and a bisimulation is a relation whose inverse is also a simulation. With this definition, Proposition 3.3 shows that bisimilarity is an equivalence relation on $V$-Cat, Proposition 3.4 constructs the quotient $V$-category from a bisimulation equivalence, Proposition 3.5 characterizes bisimilarity by cospans of functional bisimulations, and Proposition 3.6, using local distributivity, adds the span characterization. The surjective functional bisimulations form a class $O$ satisfying the open-map axioms of [4] with a strengthened descent axiom (Proposition 3.12). Proposition 5.1 then shows that any two-sided enrichment $F: V \to W$ with local right adjoints induces a change of base $F_@$ that preserves $O$ and therefore preserves bisimilarity.

Load-bearing premise

The construction presupposes that the base V is a quantaloid, so the joins in the definition of simulation always exist; the span characterization additionally presupposes that the local homsets are distributive lattices.

Editorial extensions

If this is right

Bisimilarity in $V$-Cat is an equivalence relation, so every enriched process has a canonical quotient by bisimulation, just as automata do.
When the base quantaloid is locally distributive, two enrichments are bisimilar exactly when they are connected by a span of surjective functional bisimulations, making the categorical open-map picture available for process equivalence.
Any change of base induced by a two-sided enrichment with local right adjoints preserves bisimilarity; in particular, the inverse-image and left-adjoint change-of-base functors give safe refinement operations for Betti automata and categorical transition systems.
For categorical transition systems over a category with finite limits, a refinement induced by a functor between type categories preserves bisimilarity when the functor is right exact, so specification refinement can be performed within the enriched framework without losing process equivalences.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

The gap between the paper's descent axiom (surjectivity plus condition $(*)$) and the original open-map descent axiom (mere epi) suggests a natural test: find the exact class of quantaloids or maps for which the original epi descent holds, which would make the class $O$ genuinely open in the classical sense.
Since the span characterization needs local distributivity only to interchange a join with a meet in Lemma 3.2, a weaker condition on the particular joins involved might replace global distributivity; non-distributive quantaloids such as subspace lattices are a plausible place to look for counterexamples.
The change-of-base preservation theorem could be iterated to define bisimulation relative to a refinement: two processes could be compared after changing to a richer or poorer base, giving a more graded, typed notion of process equivalence.
Because the slice correspondence $V(A)$-Cat $\cong$ $V$-Cat $\downarrow A$ transposes simulations to simulations over an interface, the framework naturally supports interface-based refinement, connecting the paper's results to component/interface theories.

Original abstract

In this paper we show that classical notions from automata theory such as simulation and bisimulation can be lifted to the context of enriched categories. The usual properties of bisimulation are nearly all preserved in this new context. The class of enriched functors that correspond to functionnal bisimulations surjective on objects is investigated and appears "nearly" open in the sense of Joyal and Moerdijk. Seeing the change of base techniques as a convenient means to define process refinement/abstractions, we give sufficient conditions for the change of base categories to preserve bisimularity. We apply these concepts to Betti's generalized automata, categorical transition systems, and other exotic categories.

The compiled record

The paper's own sentences, arranged, kept beside the review and separate from it. Each label is drawn from a closed vocabulary; the number beside it is the probability the classifier gave that label. Numbers in the tables are the authors', checked by code. No sentence in this record was written by a model.

Compiled by classifier-1.13-20260917 via OpenRouter, question bank abstract-p1-20260923, 2026-09-23: 1 request, 4,226 input tokens, $0.0002 reported.

What the abstract itself states, as probabilities: claims first 0.05 · states limitation 0.71 · human participants 0.01 · controlled comparison 0.01 · randomized assignment 0.01 · states quantitative result 0.03 · compares with prior results 0.27 · mentions code or data availability 0.01.

The abstract, sentence by sentence

arXiv listing abstract v1. Results and the main claim are underlined; show every role.

In this paper we show that classical notions from automata theory such as simulation and bisimulation can be lifted to the context of enriched categories. The usual properties of bisimulation are nearly all preserved in this new context. The class of enriched functors that correspond to functionnal bisimulations surjective on objects is investigated and appears "nearly" open in the sense of Joyal and Moerdijk. Seeing the change of base techniques as a convenient means to define process refinement/abstractions, we give sufficient conditions for the change of base categories to preserve bisimularity. We apply these concepts to Betti's generalized automata, categorical transition systems, and other exotic categories.

background contribution method result interpretation main claim

What the classifier reports for each sentence. The number is the probability it gave the label.
#	sentence	role	the authors' own work	states the main conclusion	strength
s0	In this paper we show that classical notions from automata theory such as simulation and bisimulation can be lifted to the context of enriched categories.	contribution 0.97	0.93	0.69	asserted 1.00
s1	The usual properties of bisimulation are nearly all preserved in this new context.	result 0.99	0.83	0.27	asserted 0.92
s2	The class of enriched functors that correspond to functionnal bisimulations surjective on objects is investigated and appears "nearly" open in the sense of Joyal and Moerdijk.	result 0.59	0.86	0.11	hedged possibility 0.62
s3	Seeing the change of base techniques as a convenient means to define process refinement/abstractions, we give sufficient conditions for the change of base categories to preserve bisimularity.	contribution 0.61	0.90	0.10	asserted 0.99
s4	We apply these concepts to Betti's generalized automata, categorical transition systems, and other exotic categories.	contribution 0.95	0.91	0.08	asserted 0.99

What kind of paper the classifier reports this is: theoretical result 0.99 · evidence from proof or derivation 1.00.

What was examined, and what was not

sources read

arXiv listing abstract v1

not examined

full text
figures and tables
references and citing sentences
relations to other papers

levels run

P abstract

not run

S sections
T body sentences
C citations
R cross-paper relations

Every quoted sentence on this record is the authors'. Every label is from Pith's closed vocabulary, with the probability shown beside it. Every number in the measurements table is the authors', checked by code. Record as JSON

References

Works cited (15)

[1]

R. Betti, A. Carboni, R. Street, R. Walters: Variation through e nrichment, J. Pure Appl. Algebra 29 (1983) 109-127. [DaSt97] B. Day, R. Street: Monoidal bicategories and Hopf algebr oids, Ad- vance in maths. , 129 (1997) 99-157

View on Pith 1983
[2]

G.M. Kelly, A. Labella, V. Schmitt, R. Street: Categories enriched on two sides, Journal of Pure and Applied Algebra 168 (2002) 53-98

View on Pith 2002
[3]

[JoNiWi96] A. Joyal, M. Nielsen, and G. Winskel: Bisimulation and open maps, Information and Computation 127 (1996)

View on Pith 1996
[4]

A. Joyal, I. Moerdijk: A completeness theorem for open maps, Annals of Pure and Applied Logic 70 (1994)

View on Pith 1994
[5]

S. Kasangian, G.M. Kelly, and S. Rossi: Coﬁbrations and the realiza tion of non determistic automata, Cahiers Topo. et G´ eo. Diﬀ Cat´ eg.24 (1983)

View on Pith 1983
[6]

S. Kasangian, A. Labella: Observational trees as models for con currency, Math. Struct. in Comp. Sci. 9 (1999) 617-718

View on Pith 1999
[7]

[HPTW04] K. Hess, P.E.Parent, A.Tonks, and K. Worytkiewicz: Simu lations as homotopies, Elec. Notes in Theoret. Comp. Sci. 81 (2004). Forthcoming

View on Pith 2004
[8]

[Kos] J. Koslowski: Categorical transition systems and the comp rehension scheme, Talk at PSSL Cambridge, April 2004. Forthcoming

View on Pith 2004
[9]

A. Labella, V. Schmitt: Change of Base, Cauchy Completeness an d Re- versibility, Theory and Applications of Categories 10 (2002) 187-219

View on Pith 2002
[10]

F.W. Lawvere: Metric spaces, generalized logic, and closed cate gories, Rend. Sem. Mat. Fis. di Milano 43 (1973) 135-166. Reprints in Theory and Applications of Categories No. 1 (2002)

View on Pith 1973
[11]

V. Schmitt: Flatness, preorders and metric spaces. http://arxiv.org/abs/math.CT/0309209 22

View on Pith arXiv
[12]

V. Schmitt: Enriched categories and quasi-uniform spaces, Electronic Notes in Theoretical Computer Science V ol. 73 (2003). [SpWo04] C. Sprenger and K. Worytkiewicz: Formal methods and mo dels for system design, chapter A, veriﬁcation methodology for inﬁnite-st ate message- passing systems. Kluwer, 2004. Forthcoming

View on Pith 2003
[13]

R.F.C Walters: Sheaves and Cauchy-complete categories, Cahiers de Topo. et G´ eom. Diﬀ. Cat´ egoriques13 (1981) 217-264

View on Pith 1981
[14]

[KW02] K. Worytkiewicz: Concrete Process Categories. In A. K urz, editor, Electronic Notes in Theoretical Computer Science (2002)

View on Pith 2002
[15]

[KW03] K. Worytkiewicz: Paths and simulations. In R.Blute and P. Selinger editors, Electronic Notes in Theoretical Computer Science 69 (2003). 23

View on Pith 2003

Discussion

Disagree with the review, or know something it missed? Leave a comment, highlight any passage above to comment on it, or challenge this review formally.

[1] [1]

R. Betti, A. Carboni, R. Street, R. Walters: Variation through e nrichment, J. Pure Appl. Algebra 29 (1983) 109-127. [DaSt97] B. Day, R. Street: Monoidal bicategories and Hopf algebr oids, Ad- vance in maths. , 129 (1997) 99-157

View on Pith 1983

[2] [2]

G.M. Kelly, A. Labella, V. Schmitt, R. Street: Categories enriched on two sides, Journal of Pure and Applied Algebra 168 (2002) 53-98

View on Pith 2002

[3] [3]

[JoNiWi96] A. Joyal, M. Nielsen, and G. Winskel: Bisimulation and open maps, Information and Computation 127 (1996)

View on Pith 1996

[4] [4]

A. Joyal, I. Moerdijk: A completeness theorem for open maps, Annals of Pure and Applied Logic 70 (1994)

View on Pith 1994

[5] [5]

S. Kasangian, G.M. Kelly, and S. Rossi: Coﬁbrations and the realiza tion of non determistic automata, Cahiers Topo. et G´ eo. Diﬀ Cat´ eg.24 (1983)

View on Pith 1983

[6] [6]

S. Kasangian, A. Labella: Observational trees as models for con currency, Math. Struct. in Comp. Sci. 9 (1999) 617-718

View on Pith 1999

[7] [7]

[HPTW04] K. Hess, P.E.Parent, A.Tonks, and K. Worytkiewicz: Simu lations as homotopies, Elec. Notes in Theoret. Comp. Sci. 81 (2004). Forthcoming

View on Pith 2004

[8] [8]

[Kos] J. Koslowski: Categorical transition systems and the comp rehension scheme, Talk at PSSL Cambridge, April 2004. Forthcoming

View on Pith 2004

[9] [9]

A. Labella, V. Schmitt: Change of Base, Cauchy Completeness an d Re- versibility, Theory and Applications of Categories 10 (2002) 187-219

View on Pith 2002

[10] [10]

F.W. Lawvere: Metric spaces, generalized logic, and closed cate gories, Rend. Sem. Mat. Fis. di Milano 43 (1973) 135-166. Reprints in Theory and Applications of Categories No. 1 (2002)

View on Pith 1973

[11] [11]

V. Schmitt: Flatness, preorders and metric spaces. http://arxiv.org/abs/math.CT/0309209 22

View on Pith arXiv

[12] [12]

V. Schmitt: Enriched categories and quasi-uniform spaces, Electronic Notes in Theoretical Computer Science V ol. 73 (2003). [SpWo04] C. Sprenger and K. Worytkiewicz: Formal methods and mo dels for system design, chapter A, veriﬁcation methodology for inﬁnite-st ate message- passing systems. Kluwer, 2004. Forthcoming

View on Pith 2003

[13] [13]

R.F.C Walters: Sheaves and Cauchy-complete categories, Cahiers de Topo. et G´ eom. Diﬀ. Cat´ egoriques13 (1981) 217-264

View on Pith 1981

[14] [14]

[KW02] K. Worytkiewicz: Concrete Process Categories. In A. K urz, editor, Electronic Notes in Theoretical Computer Science (2002)

View on Pith 2002

[15] [15]

[KW03] K. Worytkiewicz: Paths and simulations. In R.Blute and P. Selinger editors, Electronic Notes in Theoretical Computer Science 69 (2003). 23

View on Pith 2003