我在学习函数式编程时,看到了多个关于Church Rosser定理的参考资料,特别是钻石属性图,但我没有找到一个很好的代码示例。
如果像Haskell这样的语言可以被视为一种λ演算,那么使用该语言本身可以想出一些例子。
如果示例能够清晰地展示步骤或规约如何导致易于并行执行,我会给予额外加分。
如果像Haskell这样的语言可以被视为一种λ演算,那么使用该语言本身可以想出一些例子。
如果示例能够清晰地展示步骤或规约如何导致易于并行执行,我会给予额外加分。
这个定理的意义在于,一个可以通过多种方式简化的表达式必然会被进一步简化为一个公共乘积。
例如,以这段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
在这种特定的情况下,这种并行化实际上不会提供优势,因为两个简单的浮点数乘法按顺序执行比两个并行化乘法更有效率,因为存在调度开销,但对于更复杂的操作可能是值得的。
par
得到的并行性质。 - leftaroundabout
(5-1)*(1+1)
:你可以从简化5-1
或1+1
开始,但最终得到相同的结果。 - Riccardo T.