Parallel Reduction in Type Free lambda/mu-Calculus
Parallel Reduction in Type Free lambda/mu-Calculus
复制标题
无类型 lambda/mu 微积分的并行归约
DOI：
10.1016/s1571-0661(04)80878-8
复制
发表时间：
2000
期刊：
影响因子：
--
通讯作者：
藤田 憲悦
中科院分区：
文献类型：
--
作者：
K. Baba;馬場 謙介;S. Hirokawa;廣川 佐千男;Ken;藤田 憲悦
类型λμ-演算已知是强正规化和弱Church-Rosser的，因此是融合的。事实上，Parigot用“Tait-and-Martin-Löf”方法构造了一个并行约简来证明类型λμ-演算的收敛性。然而，钻石属性并不适用于他的平行还原。无类型λμ-演算的合流性不能从有类型λμ-演算的合流性导出，也没有得到证实。我们分析了约简规则的粒度，然后引入了一种新的并行约简，使得重命名约简和连续结构约简都被认为是一步并行约简。证明了新的并行约化公式具有菱形性质，从而给出了无型λμ-演算的收敛性的正确证明.新的并行约简的菱形性质也适用于包含对称结构约简规则的按值调用版本的λμ演算。
The typed λμ-calculus is known to be strongly normalizing and weakly Church-Rosser, and hence becomes confluent. In fact, Parigot formulated a parallel reduction to prove confluence of the typed λμ-calculus by “Tait-and-Martin-Löf” method. However, the diamond property does not hold for his parallel reduction. The confluence for type-free λμ-calculus cannot be derived from that of the typed λμ-calculus and is not confirmed yet as far as we know. We analyze granularity of the reduction rules, and then introduce a new parallel reduction such that both renaming reduction and consecutive structural reductions are considered as one step parallel reduction. It is shown that the new formulation of parallel reduction has the diamond property, which yields a correct proof of the confluence for type free λμ-calculus. The diamond property of the new parallel reduction is also applicable to a call-by-value version of the λμ-calculus containing the symmetric structural reduction rule.