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

Question

14

我在学习函数式编程时，看到了多个关于Church Rosser定理的参考资料，特别是钻石属性图，但我没有找到一个很好的代码示例。

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

如果示例能够清晰地展示步骤或规约如何导致易于并行执行，我会给予额外加分。

- user1411349

2

我不熟悉那个定理，但是初看起来似乎更有理论意义而非实际编写代码时有用。它是重写系统可能具有的“好”属性之一，以确保可合流性。一个愚蠢的例子可能是（我不确定）表达式(5-1)*(1+1)：你可以从简化5-1或1+1开始，但最终得到相同的结果。 - Riccardo T.

这里解释了并行约简的概念：http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.42.5081 第4节，第12页。 - Riccardo T.

1个回答

网页内容由stack overflow 提供, 点击上面的

可以查看英文原文，
原文链接

- dflemstr · Accepted Answer

这个定理的意义在于，一个可以通过多种方式简化的表达式必然会被进一步简化为一个公共乘积。

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

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