The permutative lambda calculus
The permutative lambda calculus
复制标题
置换 lambda 演算
DOI：
--
复制
发表时间：
2012
期刊：
影响因子：
--
通讯作者：
D. Kesner
中科院分区：
文献类型：
--
作者：
Beniamino Accattoli;D. Kesner
我们引入置换 lambda 演算，这是 lambda 演算的扩展，具有三个方程和一个用于置换构造函数的约简规则，概括了文献中的许多演算，特别是 Regnier 的 sigma 等价和 Moggi 的 assoc 等价。我们通过辅助替代演算证明了方程的汇合模和β-强归一化（PSN）的保留。汇合证明依赖于 M-developments，这是 lambda 项的一种新的发展概念。
We introduce the permutative lambda-calculus, an extension of lambda-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 lambda-terms.