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.
翻译:我们提出了一种用于判定简单语法互模拟的算法,其复杂度关于文法的赋值为多项式(即产生式规则中最大半范数)。由于赋值最多关于文法规模呈指数级增长,因此该算法可实现(单一)指数级运行时间。此前仅存在双指数级算法。作为应用,我们提供了一种从上下文无关会话类型到简单文法的转换方法,其中文法的赋值与类型规模呈线性关系。由此,我们首次实现了用于判定上下文无关会话类型等价的多项式时间算法。