Ответ 1
Вся эта теорема утверждает, что выражение, которое может быть уменьшено с помощью нескольких путей, обязательно будет приводимо к совместному произведению.
Например, возьмите этот фрагмент кода Haskell:
vecLenSq :: Float -> Float -> Float
vecLenSq x y =
xsq + ysq
where
xsq = x * x
ysq = y * y
В исчислении лямбда эта функция примерно эквивалентна (добавлены парены для ясности, операторы предположили примитив):
λ 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
Эта параллелизация на самом деле не обеспечит преимущества в этой конкретной ситуации, поскольку два простых умножения по платам, выполняемые последовательно, более эффективны, чем два параллелизированных умножения из-за накладных расходов на планирование, но это может быть полезно для более сложных операций.