add Zero mul
Компилятор напомнит нам о том, что мы пытаемся подставить функцию mul на место обычного значения
типа Nat. Тогда мы исправим выражение на:
add Zero two
Компилятор согласится. И передаст выражение вычислителю. И тут мы говорили, что вычислитель начи-
нает проводить расшифровку нашего описания. Он подставляет на место синонимов их определения, правые
части из уравнений. Этот процесс мы называли редукцией. Вычислитель видит два синонима и одно значение.
С какого синонима начать? С add или two?
142 | Глава 9: Редукция выражений
9.1 Стратегии вычислений
Этот вопрос приводит нас к понятию стратегии вычислений. Поскольку вычисляем мы только константы,
то наше выражение также можно представить в виде дерева. Только теперь у нас в узлах записаны не только
конструкторы, но и синонимы. Процесс редукции можно представить как процесс очистки такого дерева от
синонимов. Посмотрим на дерево нашего значения:
Оказывается у нас есть две возможности очистки синонимов.
Cнизу-вверх начинаем с листьев и убираем все синонимы в листьях дерева выражения. Как только в данном
узле и всех дочерних узлах остались одни конструкторы можно переходить на уровень выше. Так мы
поднимаемся выше и выше пока не дойдём до корня.
Cверху-вниз начинаем с корня, самого внешнего синонима и заменяем его на определение (с помощью урав-
нения на правую часть от знака равно), если на верху снова окажется синоним, мы опять заменим его
на определение и так пока на верху не появится конструктор, тогда мы спустимся в дочерние деревья
и будем повторять эту процедуру пока не дойдём до листьев дерева.
Посмотрим как каждая из стратегий будет редуцировать наше выражение. Начнём со стратегии от ли-
стьев к корню (снизу-вверх):
add Zero two
-- видим два синонима add и two
-- раскрываем two, ведь он находится ниже всех синонимов
=>
add Zero (Succ one)
-- ниже появился ещё один синоним, раскроем и его
=>
add Zero (Succ (Succ zero))
-- появился синоним 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
=>