简单文法双射,及其在会话类型等价中的应用
Simple grammar bisimilarity, with an application to session type equivalence
AI总结:
本文提出了一种决定简单文法双射的算法,其复杂度与文法的估值(生产规则的最大半范数)成多项式关系,从而实现单指数时间复杂度。该方法将上下文无关会话类型转换为简单文法,首次实现了会话类型等价的多项式时间算法。
摘要:
我们提供了一种决定简单文法双射的算法,其复杂度与文法的估值(生产规则的最大半范数)成多项式关系。由于估值最多与文法大小呈指数关系,这导致了单指数运行时间。此前仅知双指数算法。作为应用,我们提供了一种将上下文无关会话类型转换为简单文法的方法,其估值与类型大小成线性关系。因此,我们首次实现了会话类型等价的多项式时间算法。
英文摘要:
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.
机构、总结、中文摘要均由AI分析而来,可能存在错误,请以论文正文为准。