Simple grammar bisimilarity, with an application to session type equivalence

TL;DR

This work resolves the simple grammar bisimilarity problem with a basis-updating algorithm whose running time is polynomial in the grammar size, valuation, and input seminorms, yielding a single-exponential overall bound since the valuation is at most exponential in the grammar size. It also provides a linear-valuation translation from context-free session types to simple grammars, yielding the first polynomial-time algorithm for context-free session type equivalence. The core theoretical contributions include a unique tail-recursion characterization, a coinductive congruence framework via self-bisimulation bases, and a concrete algorithm with proven YES/NO soundness and termination. Practical impact is demonstrated by numerical experiments showing competitive performance against prior 2-EXPTIME approaches, and the methodology enables efficient type equivalence checking in compilers and tooling for session-typed languages. The work leaves open the question of a possible polynomial-time algorithm in general and motivates further study of coinductive congruence structures in infinite-state bisimilarity problems.

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.

Figures (6)

• Figure 1: Left: relevant results on language equivalence problems. Right: relevant results on bisimilarity problems over context-free grammars (CFG). Prior to our work (contribution in bold), the best known algorithm for simple grammar bisimilarity was the 2-EXPTIME algorithm for CFG.
• Figure 2: Coinductive congruence. The symmetric rules of BPA1, BPA2 are assumed implicitly.
• Figure 3: Derivation trees for determining that ${{XC}} \; {\not\sim} \; {{YC}}$. Double boundaries indicate finished leaves. A superscript on a node identifies the step in which it was visited. A subscript on an internal node indicates whether it corresponds to a BPA1 or BPA2 guess. A subscript on a finished leaf indicates whether it corresponds to a loop, pair of identical words, partial failure, or total failure. For convenience of the reader, each edge is also labeled by either a terminal symbol (corresponding to a matching transition), BPA1 or BPA2 (corresponding to a congruence rule).
• Figure 4: Derivation tree for determining that ${{XC}} \; {\sim} \; {{YC}}$, in the case that ${{C}} \; {\sim} \; {{D}}$. Superscripts, subscripts and edge labels are as in \ref{['fig:XCYC-no']}.
• Figure 5: Session types: rules for termination (${{\color{RoyalBlue}{T}}} \: \mathrm{\checkmark}$), contractivity (${{\color{RoyalBlue}{T}}} \: \mathrm{contr}$), and type formation (${\Delta} \vdash {\color{RoyalBlue}{T}}$).

Theorems & Definitions (66)

• Theorem 1.1
• Theorem 1.2
• Definition 2.1: Context-free grammar, simple grammar
• Definition 2.2: Labeled transition system
• Definition 2.3: Bisimulation, bisimilarity
• Proposition 2.4: Dead nonterminal removal
• proof
• Proposition 2.4: Congruence
• proof
• Definition 2.5: Bisimilarity approximations