Simple grammar bisimilarity, with an application to session type equivalence
For researchers in formal language theory and type systems, this provides a significant complexity improvement for a fundamental equivalence problem and its application to session types.
The paper presents a polynomial-time algorithm for deciding simple grammar bisimilarity, improving from the previously known double-exponential bound, and applies it to achieve the first polynomial-time algorithm for context-free session type equivalence.
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.