Ленивые вычисления

[EminentVictorians]

Хочу разобраться, что представляют собой ленивые вычисления. В целом вроде бы понял, но хочу убедиться, что правильно понял.

Если взять аналогию из математики. Пусть у нас есть, допустим, такая дробь:

$$\frac{8\sqrt{5+(1,2 - 2,2)^{cos(\pi)}}}{4\sqrt{5+(1,2 - 2,2)^{cos(\pi)}}}$$

Мы можем действовать двумя способами: либо сократить на корень, т.е. делать вот такую цепочку:

$$\frac{8\sqrt{5+(1,2 - 2,2)^{cos(\pi)}}}{4\sqrt{5+(1,2 - 2,2)^{cos(\pi)}}} = \frac{8}{4} = 2$$

либо вычислять сам корень:

$$\frac{8\sqrt{5+(1,2 - 2,2)^{cos(\pi)}}}{4\sqrt{5+(1,2 - 2,2)^{cos(\pi)}}} = \frac{8\sqrt{5+(-1)^{cos(\pi)}}}{4\sqrt{5+(-1)^{cos(\pi)}}} = \frac{8\sqrt{5+(-1)^{(-1)}}}{4\sqrt{5+(-1)^{(-1)}}} = \frac{8\sqrt{5+(-1)}}{4\sqrt{5+(-1)}} = \frac{8\sqrt{5-1}}{4\sqrt{5-1}} = \frac{8\sqrt{4}}{4\sqrt{4}} =$$

$$= \frac{8 \cdot 2}{4 \cdot 2} = \frac{16}{8} = 2 $$

На неформальном уровне это можно так описать: в первом случае мы упрощаем начиная сразу снаружи, а во втором идем "изнутри наружу". Правильно ли я понимаю, что именно в этом и заключается разница между ленивыми вычислениями (первый случай) и энергичными (второй)?

Кстати, даже здесь, в математическом примере, видно, что при энергичных вычислениях может возникнуть ситуация, когда мы дублируем (в случае выше - по 2 раза) одинаковые вычисления (дважды вычисляли (1,2 - 2,2), $cos(\pi)$ и все остальное).

Если это правда, тогда получается следующее. В лямбда исчислении мы тоже можем вычислять по-разному: либо начинать с каких-то внутренних редексов, либо с внешнего (левого). Пусть мы хотим, например, вычислить такое выражение: $(\lambda x. (\lambda y. y) x)((\lambda zt. z) g)$


Если начинать с внешнего редекса, то будет такая строчка:

$$(\lambda x. (\lambda y. y) x)((\lambda zt. z) g) = (\lambda y. y) ((\lambda zt. z) g) = ((\lambda zt. z) g) = (\lambda t. g)$$

А если начинать с внутренних редексов, то получится такое вычисление:

$$(\lambda x. (\lambda y. y) x)((\lambda zt. z) g) = (\lambda x. x)(\lambda t. g) = (\lambda t. g)$$

(результаты, понятное дело, обязаны совпасть в силу теоремы Черча-Россера и единственности нормальной формы с точностью до альфа эквивалетности).

Неужели все так просто? Получается, что вся разница между ленивыми и энергичными вычислениями - это с каких редексов стартовать, соответственно, с внешнего или с внутренних (первая строчка - ленивые вычисления, вторая - энергичные)

[dgwuqtj]

В целом всё так, если у вычислений нет побочных эффектов. Но избавление от повторного вычисления выражений — это уже другая задача.

[EminentVictorians]

dgwuqtj в сообщении #1687758 писал(а):

В целом всё так, если у вычислений нет побочных эффектов.

Да, речь про чистые функции.

До меня еще вот какой момент дошел. Есть модельный пример лямбда выражения:

$$ (\lambda x. y)((\lambda x. x x x)(\lambda x. x x x))$$

Если его вычислять энергично (с внутренних редексов), то программа будет вычислять его вечно:

$$(\lambda x. y)((\lambda x. x x x)(\lambda x. x x x)) = (\lambda x. y)((\lambda x. x x x)(\lambda x. x x x)(\lambda x. x x x)) = $$

$$ = (\lambda x. y)((\lambda x. x x x)(\lambda x. x x x)(\lambda x. x x x)(\lambda x. x x x)) = \text{и так далее до бесконечности}$$

А если вычислять лениво, то оно редуцируется в один шаг:

$$(\lambda x. y)((\lambda x. x x x)(\lambda x. x x x)) = y$$

(всего одна $\beta$-редукция).

Я при первом чтении как-то об этом не подумал, но по сути аналогичный пример можно ведь придумать и в математике. Например, хотим мы вычислить дробь $\frac{8\sqrt{2}}{4\sqrt{2}}$, где корень будет вычисляться через какую-нибудь итеративную процедуру. Для полных квадратов процедура заканчивалась бы, и дробь можно было бы вычислить обычным энергичным способом, но с корнем из 2 так не получится, потому что оно иррациональное число, и процедура будет считать его вечно. А ленивым методом - просто взяли сократили дробь на $\sqrt{2}$, поделили 8 на 4 и получили ответ. Та же самая идея: внутренний редекс считается бесконечно, но для результата он не нужен.