函数式编程语言中的Church-Rosser定理示例

Question

我已经看到了教会Rosser定理的多个参考,特别是钻石属性图,同时学习函数式编程,但我没有遇到过一个很好的代码示例.

如果像Haskell这样的语言可以被视为一种lambda演算,那么必须能够使用语言本身来演示一些例子.

如果示例轻松地显示步骤或减少如何导致易于并行执行,我会给予奖励积分.

Answer 1

所有这些定理都表明,可以通过多条路径减少的表达式必然会进一步简化为一个共同的产品.

例如,取这段Haskell代码:

vecLenSq :: Float -> Float -> Float
vecLenSq x y =
  xsq + ysq
  where
    xsq = x * x
    ysq = y * y

在Lambda微积分中,此函数大致相当于(为了清晰起见而添加了parens,运算符假定为原始):

? x . (? y . (? xsq . (? ysq . (xsq + ysq)) (y * y)) (x * x))

可以通过首先应用β还原xsq或通过应用β还原来减少表达ysq,即"评估顺序"是任意的.可以按以下顺序减少表达式:

? x . (? y . (? xsq . (xsq + (y * y))) (x * x))
? x . (? y . ((x * x) + (y * y)))

......或按以下顺序:

? x . (? y . (? ysq . ((x * x) + ysq)) (y * y))
? x . (? y . ((x * x) + (y * y)))

结果显然是一样的.

这意味着术语xsq和ysq可独立减少,并且它们的减少可以并行化.事实上,人们可以将Haskell中的减少并行化:

vecLenSq :: Float -> Float -> Float
vecLenSq x y =
  (xsq `par` ysq) `pseq` xsq + ysq
  where
    xsq = x * x
    ysq = y * y

这种并行将在现实中无法提供的优势,在这种特殊情况,因为按顺序执行两个简单的浮动乘法是不是因为的调度开销2个paralellized乘法更有效,但它可能是值得更复杂的操作.