— появился синоним zero раскроем его
=>
add Zero (Succ (Suсс Zero))
— все узлы ниже содержат конструкторы, поднимаемся вверх до синонима
— заменяем add на его правую часть
=>
foldNat Succ Zero (Succ (Succ Zero))
— самый нижний синоним foldNat, раскроем его
— сопоставление с образцом проходит во втором уравнении для foldNat
=>
Succ (foldNat Succ Zero (Succ Zero))
— снова раскрываем foldNat
=>
Succ (Succ (foldNat Zero Zero))
— снова раскрываем foldNat, но на этот раз нам подходит
— первое уравнение из определения foldNat
=>
Succ (Succ Zero)
— синонимов больше нет можно вернуть значение
— результат:
Succ (Succ Zero)
В этой стратегии для каждой функции мы сначала вычисляем до конца все аргументы, потом подставляем
расшифрованные значения в определение функции.
Теперь посмотрим на вычисление от корня к листьям (сверху-вниз):
add Zero two
— видим два синонима add и two, начинаем с того, что ближе всех к корню
=>
foldNat Succ Zero two
— теперь выше всех foldNat, раскроем его
Но для того чтобы раскрыть foldNat нам нужно узнать какое уравнение выбрать для этого нам нужно
понять какой конструктор находится в корне у второго аргумента, если это Zero, то мы выберем первое
уравнение, а если это Succ, то второе:
— в уравнении для foldNat видим декомпозицию по второму
— аргументу. Узнаем какой конструктор в корне у two
=>
foldNat Succ Zero (Succ one)
— Это Succ нам нужно второе уравнение:
=>
Succ (foldNat Succ Zero one)
— В корне м ыполучили конструктор, можем спуститься ниже.
— Там мы видим foldNat, для того чтобы раскрыть его нам
— снова нужно понять какой конструктор в корне у второго аргумента:
=>
Succ (foldNat Succ Zero (Succ zero))
— Это опять Succ переходим ко второму уравнению для foldNat
Стратегии вычислений | 143
=>
Succ (Succ (foldNat Succ Zero zero))
— Снова раскрываем второй аргумент у foldNat
=>
Succ (Succ (foldNat Succ Zero Zero))
— Ага это Zero, выбираем первое уравнение
=>
Succ (Succ Zero)
— Синонимов больше нет можно вернуть значение
— результат:
Succ (Succ Zero)
В этой стратегии мы всегда раскрываем самый верхний уровень выражения, можно представить как мы
вытягиваем конструкторы от корня по цепочке. У этих стратегий есть специальные имена:
• вычисление по значению (call by value), когда мы идём от листьев к корню.
• вычисление по имени (call by name), когда мы идём от корня к листьям.
Отметим, что стратегию вычисления по значению также принято называть энергичными вычислениями
(eqger evaluation) или аппликативной (applicative) стратегией редукции. Вычисление по имени также принято
называть нормальной (normal) стратегией редукции.
Преимущества и недостатки стратегий
В чём преимущества, той и другой стратегии.
Если выражение вычисляется полностью, первая стратегия более эффективна по расходу памяти.
Вычисляется полностью означает все компоненты выражения участвуют в вычислении. Например то вы-
ражении, которое мы рассмотрели так подробно, вычисляется полностью. Приведём пример выражения, при
вычислении которого нужна лишь часть аргументов, для этого определим функцию:
isZero :: Nat -> Bool
isZero Zero
= True
isZero _
= False
Она проверяет является ли нулём данное число, теперь представим как будет вычисляться выражение, в
той и другой стратегии:
isZero (add Zero two)
Первая стратегия сначала вычислит все аргументы у add потом расшифрует add и только в самом конце
доберётся до isZero. На это уйдёт восемь шагов (семь на вычисление add Zero two). В то время как вто-
рая стратегия начнёт с isZero. Для вычисления isZero ей потребуется узнать какой конструктор в корне у
выражения add Zero two. Она узнает это за два шага. Итого три шага. Налицо экономия усилий.
Почему вторая стратегия экономит память? Поскольку мы всегда вычисляем аргументы функции, мы
можем не хранить описания в памяти а сразу при подстановке в функцию начинать редукцию. Эту ситуацию
можно понять на таком примере, посчитаем сумму чисел от одного до четырёх с помощью такой функции:
sum :: Int -> [Int] -> Int
sum []
res = res
sum (x:xs)
res = sum xs (res + x)
Посмотрим на то как вычисляет первая стратегия, с учётом того что мы вычисляем значения при подста-
новке:
sum [1,2,3,4] 0
=>
sum [2,3,4]
(0 + 1)
=>
sum [2,3,4]
1
=>
sum [3,4]
(1 + 2)
=>
sum [3,4]
3
=>
sum [4]
(3+3)
=>
sum [4]
6
=>
sum []
(6+4)
=>
sum []
10
=>
10
144 | Глава 9: Редукция выражений
Теперь посмотрим на вторую стратегию:
sum [1,2,3,4] 0
=>
sum [2,3,4]
0+1
=>
sum [3,4]
(0+1)+2
=>
sum [4]
((0+1)+2)+3
=>
sum []
(((0+1)+2)+3)+4
=>
(((0+1)+2)+3)+4
=>
((1+2)+3)+4
=>
(3+3)+4
=>
6+4
=>
10
А теперь представьте, что мы решили посчитать сумму чисел от 1 до миллиона. Сколько вычислений
нам придётся накопить! В этом недостаток второй стратегии. Но есть и ещё один недостаток, рассмотрим
выражение:
(x -> add (add x x) x) (add Zero two)
Первая стратегия сначала редуцирует выражение add Zero two в то время как вторая подставит это
выражение в функцию и утроит свою работу!
Но у второй стратегии есть одно очень веское преимущество, она может вычислять больше выражений
чем вторая. Определим значение бесконечность:
infinity
:: Nat