183
находятся в СЗНФ. Для таких выражений у нас будут различные
конструкторы для представления их в виде объектов типа Command и в
виде объектов типа WHNF.
Если считать, что типы Command и WHNF уже определены, то для
описания состояния SECD-машины в целом, нам достаточно описать типы,
представляющие объекты, хранящиеся в четырех
регистрах SECD-
машины. В стеке машины хранится последовательность (список) уже
вычисленных выражений в СЗНФ, так что тип этого регистра можно
описать как [WHNF]. Регистр контекста хранит контекст в том самом виде,
как мы его использовали при описании eval/apply-интерпретатора. Регистр
команд содержит последовательность исходных выражений-команд, так
что его тип может быть
выражен описателем [Command]. Наконец,
регистр хранения состояний содержит последовательность троек,
описывающих содержимое трех остальных регистров. Таким образом,
получаем следующее описание SECD-машины и всех ее регистров.
type Stack = [WHNF]
Environment = Context
Control = [Command]
Dump = [(Stack, Environment, Control)]
SECD = (Stack, Environment, Control, Dump)
Работа SECD-машины выполняется по шагам, при этом каждый шаг
работы определяется содержимым первой команды из регистра команд.
Исполнение команды обычно приводит к удалению ее из регистра
управления и модификации содержимого остальных регистров машины.
Во всех случаях исполнение команды-выражения приводит к вычислению
этого выражения и загрузке результата вычисления на вершину стека
результатов. Вообще, конечная цель работы машины состоит в исполнении
всех содержащихся в регистре управления команд и получению результата
в качестве первого элемента стека. Один шаг работы SECD-машины
можно записать в виде SECD -> SECD', где SECD и SECD' – состояния
SECD-машины до и после выполнения шага соответственно. Тогда всю
работу SECD-машины можно записать
в виде последовательности
состояний, причем последним состоянием будет такое, в котором регистр
управления пуст. Мы будем записывать состояния SECD-машины более
подробно в виде (s, e, c, d), где s, e, c и d описывают содержимое
отдельных регистров машины. В начальный момент работы все регистры
пусты, только в регистре управления содержится исходное выражение для
вычисления. Такое состояние можно записать в виде
([], [], [expr], []), где expr – исходное выражение типа
Command. Если программа нормально закончит работу, то в конечном
состоянии результат вычислений будет находиться в стеке, так что
состояние машины можно описать в виде ([res], [], [], []), где
res – результат вычислений типа WHNF – выражение в СЗНФ.