How to prove decidablity of equational theories with second-order computation analyser SOL
How to prove decidablity of equational theories with second-order computation analyser SOL
复制标题
如何使用二阶计算分析器 SOL 证明方程理论的可判定性
DOI：
10.1017/s0956796819000157
复制
发表时间：
2019
影响因子：
1.1
通讯作者：
M.Hamana
中科院分区：
文献类型：
--
作者：
Ferenc Nagy;Norimasa Yoshida;M.Hamana
在二阶代数理论的框架下，我们给出了一种证明程序设计语言概念的方程式理论可判定性的一般方法。我们提出了一个基于Haskell的分析工具，即二阶实验室，它帮助证明从二阶代数理论得到的计算规则的合流性和强规范性。为了涵盖编程语言理论中的各种例子，我们以一种非平凡的方式组合和扩展了二阶计算的语法和语义结果。我们在文献中演示了如何证明各种代数理论的可判定性。它包括单子和λ演算的方程理论，普洛特金和鲍尔的状态和比特理论，以及斯塔克的π演算理论。我们还演示了这种方法如何解决一元范畴的连贯性。
We present a general methodology of proving the decidability of equational theory of programming language concepts in the framework of second-order algebraic theories. We propose a Haskell-based analysis tool, i.e. Second-Order Laboratory, which assists the proofs of confluence and strong normalisation of computation rules derived from second-order algebraic theories. To cover various examples in programming language theory, we combine and extend both syntactical and semantical results of the second-order computation in a non-trivial manner. We demonstrate how to prove decidability of various algebraic theories in the literature. It includes the equational theories of monad and λ-calculi, Plotkin and Power’s theory of states and bits, and Stark’s theory of π-calculus. We also demonstrate how this methodology can solve the coherence of monoidal categories.