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 doubly-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.
翻译:我们提出了一种判定简单文法互模拟的算法,其复杂度在文法估值(产生式规则中的最大半范数)上呈多项式。由于估值至多是文法规模的指数函数,该算法具有单指数运行时间。此前已知的算法仅具有双指数复杂度。作为应用,我们提出了一种将上下文无关会话类型转换为简单文法的方法,其估值在类型规模上呈线性。通过这种方式,我们首次提出了判定上下文无关会话类型等价性的多项式时间算法。