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

Question

我看到多次引用 Church Rosser theorem ，特别是钻石属性图，在学习函数式编程时，但我还没有遇到过很好的代码示例。

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

如果示例能够轻松地展示步骤或减少如何导致轻松并行执行，我会给予奖励点。

Answer 1

所有这些定理都表明，可以通过多个路径约简的表达式必然可以进一步约简为公共(public)乘积。

例如，以这段 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

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