pith. sign in

arxiv: 2407.04063 · v3 · submitted 2024-07-04 · 💻 cs.FL · cs.LO

Simple grammar bisimilarity, with an application to session type equivalence

Diogo Po\c{c}as , Gil Silva , Vasco T. Vasconcelos This is my paper

Pith reviewed 2026-05-23 23:11 UTC · model grok-4.3

classification 💻 cs.FL cs.LO
keywords simple grammar bisimilaritycontext-free session typestype equivalencepolynomial-time algorithmformal languagesbisimulationsession typesgrammar algorithms
0
0 comments X

The pith

An algorithm decides simple grammar bisimilarity in time polynomial in the grammar valuation, yielding the first polynomial-time procedure for context-free session type equivalence.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper introduces a decision procedure for bisimilarity of simple grammars that runs in time polynomial in the valuation of the grammar, where valuation is the maximum seminorm among production rules. This bound improves the previous double-exponential complexity to single exponential overall. The authors then construct a conversion from context-free session types to simple grammars in which the valuation grows linearly with the size of the type. The combination produces the first polynomial-time algorithm for deciding equivalence of context-free session types.

Core claim

We provide an algorithm for deciding simple grammar bisimilarity whose complexity is polynomial in the valuation of the grammar. Since the valuation is at most exponential in the size of the grammar, this gives rise to a single exponential running time. As an application, we provide a conversion from context-free session types to simple grammars whose valuation is linear in the size of the type. In this way, we provide the first polynomial-time algorithm for deciding context-free session type equivalence.

What carries the argument

The polynomial-time decision procedure for bisimilarity on simple grammars, which uses the valuation (maximum seminorm of production rules) to bound the search.

If this is right

  • Equivalence of context-free session types is decidable in polynomial time.
  • Simple grammar bisimilarity is decidable in single-exponential time.
  • Verification tools for concurrent systems can use the conversion to check protocol equivalence efficiently.
  • Any system reducible to simple grammars with bounded valuation inherits the polynomial decision procedure.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The linear valuation conversion may extend to other type systems that generate recursive protocols.
  • Implementations could exploit the valuation measure directly to prune search in practical type checkers.
  • If session types admit tighter seminorm bounds than the worst-case linear conversion, effective complexity could drop further.

Load-bearing premise

The conversion from context-free session types to simple grammars produces a grammar whose valuation is linear in the size of the type.

What would settle it

A pair of equivalent context-free session types whose equivalence is not detected by the converted grammar check, or an instance where the running time grows faster than polynomial in the valuation.

Figures

Figures reproduced from arXiv: 2407.04063 by Diogo Po\c{c}as, Gil Silva, Vasco T. Vasconcelos.

Figure 1
Figure 1. Figure 1: Left: relevant results on language equivalence pr [PITH_FULL_IMAGE:figures/full_fig_p003_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Coinductive congruence. Right-hand rules omitte [PITH_FULL_IMAGE:figures/full_fig_p012_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: Derivation trees for determining that XC 6∼ Y C. A superscript on a node identifies the step in which it was visited. A subscript on a node identifies whether it corresponds to a loop, pair of identical words, BPA1 guess, BPA2 guess, partial failure, or total failure. Each edge is labeled by a terminal symbol (corresponding to a matching transition), BPA1 or BPA2 (corresponding to a congruence rule). 4. Ex… view at source ↗
Figure 4
Figure 4. Figure 4: Derivation tree for determining that XC ∼ Y C, in the case that C ∼ D. Superscripts, subscripts and edge labels are as in fig. 3. 13’. Examining (C, D), we see that there is no corresponding pair in B, the transitions match, and C, D are both unnormed. By case 5.7, we update B by adding pair (C, D). We mark node (C, D) as a BPA1 guess and add a children (C, D) corresponding to the only matching transition.… view at source ↗
Figure 5
Figure 5. Figure 5: Session types: rules for termination (T X), contractivity (T contr), and type formation (∆ ⊢ T). Type formation (∆ ⊢ T) states that T is a type under context ∆. A context is an (unordered) set of type variables, and the comma operator ∆, x extends a context by adding a new variable. Recursion µ x.T binds variable X. We say that T is a type if ⊢ T, i.e., if T is a type under the empty context (this is only … view at source ↗
Figure 6
Figure 6. Figure 6: Inductive congruence. Right-hand rules omitted. [PITH_FULL_IMAGE:figures/full_fig_p035_6.png] view at source ↗
read the original abstract

We provide an algorithm for deciding simple grammar bisimilarity whose complexity is polynomial in the valuation of the grammar (maximum seminorm among production rules). Since the valuation is at most exponential in the size of the grammar, this gives rise to a (single) exponential running time. Previously only a double-exponential algorithm was known. As an application, we provide a conversion from context-free session types to simple grammars whose valuation is linear in the size of the type. In this way, we provide the first polynomial-time algorithm for deciding context-free session type equivalence.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

0 major / 1 minor

Summary. The paper presents an algorithm for deciding bisimilarity of simple grammars whose running time is polynomial in the grammar valuation (defined as the maximum seminorm over production rules). Since valuation is at most exponential in grammar size, this yields single-exponential time overall, improving on the previous double-exponential bound. As an application, the paper gives a conversion from context-free session types to simple grammars that preserves equivalence and produces a grammar whose valuation is linear in the size of the input type, thereby obtaining the first polynomial-time procedure for deciding equivalence of context-free session types.

Significance. If the algorithm and the linear-valuation conversion are correct, the result is significant: it improves the complexity of grammar bisimilarity from double- to single-exponential time and supplies the first polynomial-time decision procedure for context-free session type equivalence. The polynomial dependence on valuation and the explicit linear conversion are technically noteworthy contributions to the theory of session types and grammar equivalence.

minor comments (1)
  1. The abstract states the complexity claims and the linear-valuation conversion but the full manuscript should ensure all definitions (e.g., seminorm, valuation, simple grammar) and the equivalence-preserving property of the conversion are stated with explicit proofs or references to lemmas.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for the positive report, the accurate summary of our contributions, and the recommendation to accept. We are gratified that the single-exponential algorithm for simple grammar bisimilarity and the linear-valuation conversion for context-free session types are viewed as significant.

Circularity Check

0 steps flagged

No circularity in derivation chain

full rationale

The paper presents two explicit constructions: (1) an algorithm deciding simple grammar bisimilarity in time polynomial in the grammar valuation, and (2) a conversion from context-free session types to simple grammars whose valuation is linear in type size. The polynomial-time claim for session-type equivalence is obtained by composing these constructions. Neither step reduces to a fitted parameter, self-definition, or self-citation chain; both are algorithmic results whose complexity bounds are derived from the constructions themselves rather than presupposing the target bound. The derivation is therefore self-contained.

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 0 invented entities

Abstract-only review supplies no explicit free parameters, axioms, or invented entities; ledger left empty pending full text.

pith-pipeline@v0.9.0 · 5621 in / 881 out tokens · 17088 ms · 2026-05-23T23:11:11.553596+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

50 extracted references · 50 canonical work pages · 1 internal anchor

  1. [1]

    Vasconcelos

    Bernardo Almeida, Andreia Mordido, Peter Thiemann, and Vasco T. Vasconcelos. Polymorphic context-free session types. CoRR, 2021. arXiv:2106.06658

    work page arXiv 2021

  2. [2]

    Vasconc elos

    Bernardo Almeida, Andreia Mordido, and Vasco T. Vasconc elos. FreeST, a programming language with context-free session types. https://freest-lang.github.io/, 2019

    work page 2019

  3. [3]

    Vasconc elos

    Bernardo Almeida, Andreia Mordido, and Vasco T. Vasconc elos. FreeST: Context-free ses- sion types in a functional language. In PLACES, volume 291 of EPTCS, pages 12–23, 2019. doi:10.4204/EPTCS.291.2

    work page doi:10.4204/eptcs.291.2 2019

  4. [4]

    Vasconc elos

    Bernardo Almeida, Andreia Mordido, and Vasco T. Vasconc elos. Deciding the bisimilarity of context-free session types. In TACAS, volume 12079 of LNCS, pages 39–56. Springer, 2020. doi:10.1007/978-3-030-45237-7\_3

    work page doi:10.1007/978-3-030-45237-7 2020

  5. [5]

    Jos C. M. Baeten, Jan A. Bergstra, and Jan Willem Klop. Dec idability of bisimulation equivalence for processes generating context-free languages. In PARLE, volume 259 of LNCS, pages 94–111. Springer, 1987. doi:10.1007/3-540-17945-3\_5

    work page doi:10.1007/3-540-17945-3 1987

  6. [6]

    On fo rmal properties of simple phrase struc- ture grammars

    Yehoshua Bar-Hillel, Micha Perles, and Eli Shamir. On fo rmal properties of simple phrase struc- ture grammars. Sprachtypologie und Universalienforschung , 14:143–172, 1961

    work page 1961

  7. [7]

    Murawski

    Michael Benedikt, Stefan G¨ oller, Stefan Kiefer, and An drzej S. Murawski. Bisimilarity of push- down automata is nonelementary. In LICS, pages 488–498. IEEE Computer Society, 2013. doi:10.1109/LICS.2013.55

    work page doi:10.1109/lics.2013.55 2013

  8. [8]

    Bergstra and Jan Willem Klop

    Jan A. Bergstra and Jan Willem Klop. Process theory based on bisimulation semantics. In Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency, volume 354 of LNCS, pages 50–122. Springer, 1988. doi:10.1007/BFB0013021

    work page doi:10.1007/bfb0013021 1988

  9. [9]

    An elem entary bisimulation decision proce- dure for arbitrary context-free processes

    Olaf Burkart, Didier Caucal, and Bernhard Steffen. An elem entary bisimulation decision proce- dure for arbitrary context-free processes. In MFCS, volume 969 of LNCS, pages 423–433. Springer,

    work page

  10. [10]

    doi:10.1007/3-540-60246-1\_148

    work page doi:10.1007/3-540-60246-1

  11. [11]

    A fast algorithm to decide on simple gram mars equivalence

    Didier Caucal. A fast algorithm to decide on simple gram mars equivalence. In Optimal Algorithms, volume 401 of LNCS, pages 66–85. Springer, 1989. doi:10.1007/3-540-51859-2\_8

    work page doi:10.1007/3-540-51859-2 1989

  12. [12]

    Graphes canoniques de graphes alg´ ebri ques

    Didier Caucal. Graphes canoniques de graphes alg´ ebri ques. RAIRO - Theoretical Informatics and Applications, 24(4):339–352, 1990. doi:10.1051/ita/1990240403391

    work page doi:10.1051/ita/1990240403391 1990

  13. [13]

    B isimulation equivalence is decidable for all context-free processes

    Søren Christensen, Hans H¨ uttel, and Colin Stirling. B isimulation equivalence is decidable for all context-free processes. Inf. Comput. , 121(2):143–148, 1995. doi:10.1006/inco.1995.1129

    work page doi:10.1006/inco.1995.1129 1995

  14. [14]

    Vasconcelos

    Diana Costa, Andreia Mordido, Diogo Po¸ cas, and Vasco T . Vasconcelos. Polymor- phic higher-order context-free session types. Theor. Comput. Sci. , 1001:114582, 2024. doi:10.1016/J.TCS.2024.114582

    work page doi:10.1016/j.tcs.2024.114582 2024

  15. [15]

    Vasconcelos

    Diana Costa, Andreia Mordido, Diogo Po¸ cas, and Vasco T. Vasconcelos. Higher-order context-free session types in system F. Electronic Proceedings in Theoretical Computer Science , 356:24–35,

    work page

  16. [16]

    doi:10.4204/eptcs.356.3. 32

    work page doi:10.4204/eptcs.356.3

  17. [17]

    Fast equival ence-checking for normed context-free processes

    Wojciech Czerwinski and Slawomir Lasota. Fast equival ence-checking for normed context-free processes. In FSTTCS, volume 8 of LIPIcs, pages 260–271. Schloss Dagstuhl - Leibniz-Zentrum f¨ ur Informatik, 2010.doi:10.4230/LIPIcs.FSTTCS.2010.260

    work page doi:10.4230/lipics.fsttcs.2010.260 2010

  18. [18]

    Symbolic Model Checking for Real-Time Systems

    Rob J. van Glabbeek. The linear time-branching time spe ctrum (extended abstract). In CON- CUR, volume 458 of LNCS, pages 278–297. Springer, 1990. doi:10.1007/BFB0039066

    work page doi:10.1007/bfb0039066 1990

  19. [19]

    Greibach

    Sheila A. Greibach. A new normal-form theorem for conte xt-free phrase structure grammars. J. ACM, 12(1):42—52, 1965. doi:10.1145/321250.321254

    work page doi:10.1145/321250.321254 1965

  20. [20]

    A polyn omial algorithm for deciding bisimilarity of normed context-free processes

    Yoram Hirshfeld, Mark Jerrum, and Faron Moller. A polyn omial algorithm for deciding bisimilarity of normed context-free processes. Theor. Comput. Sci. , 158(1):143–159, 1996. doi:10.1016/0304-3975(95)00064-X

    work page doi:10.1016/0304-3975(95)00064-x 1996

  21. [21]

    Types for dyadic interaction

    Kohei Honda. Types for dyadic interaction. In CONCUR, volume 715 of LNCS, pages 509–523. Springer, 1993. doi:10.1007/3-540-57208-2\_35

    work page doi:10.1007/3-540-57208-2 1993

  22. [22]

    Language primitives and type discipline for structured communication-based programming

    Kohei Honda, Vasco Thudichum Vasconcelos, and Makoto K ubo. Language primitives and type discipline for structured communication-based programmi ng. In ESOP, volume 1381 of LNCS, pages 122–138. Springer, 1998. doi:10.1007/BFb0053567

    work page doi:10.1007/bfb0053567 1998

  23. [23]

    John E Hopcroft and Richard M. Karp. A linear algorithm f or testing equivalence of finite automata. Technical report, Cornell University, 1971

    work page 1971

  24. [24]

    On the Equivalence, Containment, and Covering Problems for the Regular and Context-Free Languages

    Harry B. Hunt III, Daniel J. Rosenkrantz, and Thomas G. S zymanski. On the equivalence, containment, and covering problems for the regular and cont ext-free languages. J. Comput. Syst. Sci., 12(2):222–268, 1976. doi:10.1016/S0022-0000(76)80038-4

    work page doi:10.1016/s0022-0000(76)80038-4 1976

  25. [25]

    A Short Decidability Proof for DPDA Language Equivalence via First-Order Grammars

    Petr Janˇ car. A short decidability proof for DPDA langu age equivalence via first-order grammars. CoRR, 2010. arXiv:1010.4760

    work page internal anchor Pith review Pith/arXiv arXiv 2010

  26. [26]

    Bisimilarity on basic process algebra is in 2-EXPTIME (an explicit proof)

    Petr Janˇ car. Bisimilarity on basic process algebra is in 2-EXPTIME (an explicit proof). Log. Methods Comput. Sci. , 9(1), 2012. doi:10.2168/LMCS-9(1:10)2013

    work page doi:10.2168/lmcs-9(1:10)2013 2012

  27. [27]

    Equivalence of pushdown automata via firs t-order grammars

    Petr Janˇ car. Equivalence of pushdown automata via firs t-order grammars. J. Comput. Syst. Sci. , 115:86–112, 2021. doi:10.1016/J.JCSS.2020.07.004

    work page doi:10.1016/j.jcss.2020.07.004 2021

  28. [28]

    Techniques for decidabi lity and undecidability of bisimilarity

    Petr Janˇ car and Faron Moller. Techniques for decidabi lity and undecidability of bisimilarity. In CONCUR, volume 1664 of LNCS, pages 30–45. Springer, 1999. doi:10.1007/3-540-48320-9\_5

    work page doi:10.1007/3-540-48320-9 1999

  29. [29]

    Kanellakis and Scott A

    Paris C. Kanellakis and Scott A. Smolka. CCS expression s, finite state processes, and three problems of equivalence. Inf. Comput., 86(1):43–68, 1990. doi:10.1016/0890-5401(90)90025-d

    work page doi:10.1016/0890-5401(90)90025-d 1990

  30. [30]

    BPA bisimilarity is EXPTIME-hard

    Stefan Kiefer. BPA bisimilarity is EXPTIME-hard. Inf. Process. Lett. , 113(4):101–106, 2013. doi:10.1016/j.ipl.2012.12.004

    work page doi:10.1016/j.ipl.2012.12.004 2013

  31. [31]

    R. Milner. Communication and Concurrency . Prentice Hall, 1989

    work page 1989

  32. [32]

    An algebraic definition of simulation bet ween programs

    Robin Milner. An algebraic definition of simulation bet ween programs. In IJCAI, pages 481–489. William Kaufmann, 1971. URL: http://ijcai.org/Proceedings/71/Papers/044.pdf

    work page 1971

  33. [33]

    Lecture Notes in Computer Science92, Springer, doi:10.1007/3-540-10235-3

    Robin Milner. A Calculus of Communicating Systems , volume 92 of LNCS. Springer, 1980. doi:10.1007/3-540-10235-3

    work page doi:10.1007/3-540-10235-3 1980

  34. [34]

    A calculus of mobile processes, I

    Robin Milner, Joachim Parrow, and David Walker. A calcu lus of mobile processes, I. Inf. Comput., 100(1):1–40, 1992. doi:10.1016/0890-5401(92)90008-4

    work page doi:10.1016/0890-5401(92)90008-4 1992

  35. [35]

    A calculus of mobile processes, II

    Robin Milner, Joachim Parrow, and David Walker. A calcu lus of mobile processes, II. Inf. Comput., 100(1):41–77, 1992. doi:10.1016/0890-5401(92)90009-5. 33

    work page doi:10.1016/0890-5401(92)90009-5 1992

  36. [36]

    Smolka, and Jir ´ ı Srba

    Faron Moller, Scott A. Smolka, and Jir ´ ı Srba. On the com putational complexity of bisimulation, redux. Inf. Comput. , 194(2):129–143, 2004. doi:10.1016/J.IC.2004.06.003

    work page doi:10.1016/j.ic.2004.06.003 2004

  37. [37]

    In: CIAA, Lecture Notes in Computer Science 4094, Springer, pp

    Robert Paige and Robert Endre Tarjan. Three partition r efinement algorithms. SIAM J. Comput. , 16(6):973–989, 1987. doi:10.1137/0216062

    work page doi:10.1137/0216062 1987

  38. [38]

    Concurrency and automata on infinite sequences

    David Michael Ritchie Park. Concurrency and automata o n infinite sequences. In Confer- ence on Theoretical Computer Science , volume 104 of LNCS, pages 167–183. Springer, 1981. doi:10.1007/BFB0017309

    work page doi:10.1007/bfb0017309 1981

  39. [39]

    Vasconcelos

    Diogo Po¸ cas, Diana Costa, Andreia Mordido, and Vasco T . Vasconcelos. System F µ ω with context-free session types. In ESOP, volume 13990 of LNCS, pages 392–420. Springer, 2023. doi:10.1007/978-3-031-30044-8\_15

    work page doi:10.1007/978-3-031-30044-8 2023

  40. [40]

    Decidability of bisimulation e quivalence for equational graphs of finite out-degree

    G´ eraud S´ enizergues. Decidability of bisimulation e quivalence for equational graphs of finite out-degree. In FOCS, pages 120–129. IEEE Computer Society, 1998. doi:10.1109/SFCS.1998.743435

    work page doi:10.1109/sfcs.1998.743435 1998

  41. [41]

    L(A)=L(B)? decidability resul ts from complete formal systems

    G´ eraud S´ enizergues. L(A)=L(B)? decidability resul ts from complete formal systems. Theor. Comput. Sci. , 251(1-2):1–166, 2001. doi:10.1016/S0304-3975(00)00285-1

    work page doi:10.1016/s0304-3975(00)00285-1 2001

  42. [42]

    Roadmap of infinite results

    Jir ´ ı Srba. Roadmap of infinite results. Bull. EATCS , 78:163–175, 2002. doi:10.1142/9789812562494_0054

    work page doi:10.1142/9789812562494_0054 2002

  43. [44]

    Decidability of bisimulation equival ence for normed pushdown processes

    Colin Stirling. Decidability of bisimulation equival ence for normed pushdown processes. Theor. Comput. Sci. , 195(2):113–131, 1998. doi:10.1016/S0304-3975(97)00216-8

    work page doi:10.1016/s0304-3975(97)00216-8 1998

  44. [45]

    Deciding DPDA equivalence is primitiv e recursive

    Colin Stirling. Deciding DPDA equivalence is primitiv e recursive. In ICALP, volume 2380 of LNCS, pages 821–832. Springer, 2002. doi:10.1007/3-540-45465-9\_70

    work page doi:10.1007/3-540-45465-9 2002

  45. [46]

    An interac tion-based language and its typing system

    Kaku Takeuchi, Kohei Honda, and Makoto Kubo. An interac tion-based language and its typing system. In PARLE, volume 817 of LNCS, pages 398–413. Springer, 1994. doi:10.1007/3-540-58184-7\_118

    work page doi:10.1007/3-540-58184-7 1994

  46. [47]

    In 21st ACM SIGPLAN International Conference on Functional Programming (ICFP)

    Peter Thiemann and Vasco T. Vasconcelos. Context-free session types. In ICFP, pages 462–475. ACM, 2016. doi:10.1145/2951913.2951926. 34 ε ≡ i B ε ε-Ax γα ≡ i B β (X, Y γ ) ∈ B Xα ≡ i B Y β BPA1-L α ≡ i B α ′ β ≡ i B β ′ (Xα, Y β ) ∈ B Xα ′ ≡ i B Y β ′ BPA2-L Figure 6: Inductive congruence. Right-hand rules omitted. A Alternative notions of congruences In ...

    work page doi:10.1145/2951913.2951926 2016

  47. [48]

    if γ a→ γ′ for some γ′, then there exists some δ′ such that δ a→ δ′ and γ′ ≡ x B δ′

    work page

  48. [49]

    Lemma 39

    if δ a→ δ′ for some δ′, then there exists some γ′ such that γ a→ γ′ and γ′ ≡ x B δ′. Lemma 39. Let B be a basis for some given context-free grammar without dead s ymbols

    work page

  49. [50]

    If B is a self-bisimulation with respect to ≡ ℓ B, then ≡ ℓ B is a bisimulation; in particular, ≡ ℓ B ⊆ ∼

    work page

  50. [51]

    36 Proof

    If B is a self-bisimulation with respect to ≡ i B, then ≡ i B ⊆ ∼ . 36 Proof. Let us first consider the least congruence ≡ ℓ B. Given γ ≡ ℓ B δ, we need to show that any transition γ a→ γ′ has a matching transition δ a→ δ′ with γ′ ≡ ℓ B δ′, and vice-versa. The proof is by structural induction on the (finite) proof of γ ≡ ℓ B δ. (inclusion): then ( γ, δ ) ∈ ...

    work page