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

Question

在学习函数式编程时，我看到过多次引用Church Rosser 定理，尤其是菱形属性图，但我没有遇到过很好的代码示例。

如果像 Haskell 这样的语言可以被视为一种 lambda 演算，那么一定可以使用该语言本身来举出一些例子。

如果该示例很容易显示步骤或减少如何导致易于并行化的执行，我会给予奖励积分。

Answer 1

所有这些定理都表明，一个可以通过多条路径归约的表达式必然会进一步归约为一个共同的产品。

例如，以这段 Haskell 代码为例：

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

在 Lambda 演算中，此函数大致相当于（为清楚起见添加了括号，运算符假定为原始）：

λ 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

这种并行化实际上不会在这种特殊情况下提供优势，因为由于调度开销，按顺序执行的两个简单浮点乘法比两个并行乘法更有效，但对于更复杂的操作可能是值得的。