The Permutative λ-Calculus
The Permutative λ-Calculus
复制标题
置换 λ 演算
DOI：
10.1007/978-3-642-28717-6_5
复制
发表时间：
2012
期刊：
影响因子：
--
通讯作者：
K. Nagahama
中科院分区：
文献类型：
--
作者：
Mai Oshio;Takuma Fujii;T. Kusaura;K. Nagahama
本文介绍了置换λ-演算，它是λ-演算的一个扩展，具有置换构造函数的三个方程和一个约简规则，推广了文献中的许多演算，特别是Regnier的sigma等价和Moggi的关联等价。利用辅助代换演算证明了方程的合流模和强归一化（PSN）的保存性。合流的证明依赖于m -发展，这是λ-项发展的新概念。
We introduce the permutativeλ-calculus, an extension ofλ-calculus with three equations and one reduction rule for permuting constructors, generalising many calculi in the literature, in particular Regnier’s sigma-equivalence and Moggi’s assoc-equivalence. We prove confluence modulo the equations and preservation of beta-strong normalisation (PSN) by means of an auxiliary substitution calculus. The proof of confluence relies on M-developments, a new notion of development forλ-terms.