1 Кубенский А.А. Функциональное программирование. Глава 5. Системы исполнения функциональных программ. Глава 5. Системы исполнения функциональных программ 5.3. SECD-машина. Попробуем транслировать конструкции лямбда-исчисления в еще более простой язык, интерпретатор которого допускает простое и однозначное толкование. S – Stack – содержит промежуточные результаты вычислений в СЗНФ E – Environment – содержит контекст вычислений C – Control – содержит последовательность команд D – Dump – содержит состояния машины data Stack = [WHNF] data Environment = [(String, WHNF)] data Control = [Command] data Dump = [(Stack, Environment, Control)] data WHNF = C_Int Integer | C_Bool Bool | Closure String Environment Command | Oper String Int [WHNF] data Command = Integral Integer | Boolean Bool | Function String | Variable String | Lambda String Command | Application Command Command | If Command Command Command | Let String Command Command | Letrec [(String, Command)] Command data SECD = (Stack, Environment, Control, Dump)

2 Кубенский А.А. Функциональное программирование. Глава 5. Системы исполнения функциональных программ. Работа SECD-машины. Переход из состояния в состояние: (s, e, c, d) (s', e', c', d') Функциональное выражение для процесса переходов: evaluate :: SECD -> SECD Уравнения функции evaluate будут иметь следующий вид: evaluate (s, e, c, d) = evaluate (s', e', c', d') или, в случае, когда состояние (s, e, c, d) заключительное: evaluate (s, e, c, d) = (s, e, c, d) Интерпретатор создает SECD-машину в начальном состоянии, запускает ее, вызывая функцию evaluate, и извлекает результат вычислений из SECD-машины в конечном состоянии: interpret :: Command -> WHNF interpret com = res where (res:_, _, _, _) = evaluate ([], [], [com], []) то есть исходная программа помещается в регистр управления, а результат извлекается с вершины стека выражений.

3 Кубенский А.А. Функциональное программирование. Глава 5. Системы исполнения функциональных программ. Уравнения функции evaluate, описывающей работу SECD-машины. evaluate (s, e, (Integral n):c, d) = evaluate ((C_Int n):s, e, c, d) evaluate (s, e, (Boolean b):c, d) = evaluate ((C_Bool b):s, e, c, d) evaluate (s, e, (Lambda x body):c, d) = evaluate ((Closure x body e):s, e, c, d) evaluate (s, e, (Function f):c, d) = evaluate ((Oper (arity f) f []):s, e, c, d) evaluate (s, e, (Variable x):c, d) = evaluate ((assoc x e):s, e, c, d) Команды, представляющие выражения, уже находящиеся в СЗНФ, просто перекладывают эти выражения на вершину стека вычислений, изменяя их представление. evaluate (s, e, (If cond the els):c, d) = evaluate (s, e, cond:(Select the els):c, d) evaluate ((C_Bool True):s, e, (Select the els):c, d) = evaluate (s, e, the:c, d) evaluate ((C_Bool False):s, e, (Select the els):c, d) = evaluate (s, e, els:c, d) Исполнение команды условного вычисления If : data Command =... | Select Command Command Здесь Select – это новая специальная команда условного перехода:

4 Кубенский А.А. Функциональное программирование. Глава 5. Системы исполнения функциональных программ. Уравнения функции evaluate для более сложных команд. evaluate (s, e, (Application f a):c, d) = evaluate (s, e, a:f:Apply:c, d) Применение функции: data Command =... | Apply Здесь Apply – это новая специальная команда применения функции: evaluate ((Oper n f args):arg:s, e, Apply:c, d) | n == 1 = evaluate ((intrinsic f newArgs):s, e, c, d) | otherwise = evaluate ((Oper (n-1) f newArgs):s, e, c, d) where newArgs = args ++ [arg] Исполнение команды Apply для случая примитивной функции: evaluate ((Closure x body ctx):a:s, e, Apply:c, d) = evaluate ([], (x, a):ctx, [body], (s, e, c):d) evaluate (x:_, _, [], (s, e, c):d) = evaluate (x:s, e, c, d) Исполнение команды Apply для замыкания (вход в функцию и выход из нее): evaluate (s, e, (Let x exp body):c, d) = evaluate (s, e, exp:(LetApply x body):c, d) evaluate (arg:s, e, (LetApply x body):c, d) = evaluate ([], (x,arg):e, [body], (s, e, c):d) Аналогично для простого (нерекурсивного) блока: data Command =... | LetApply String Command

5 Кубенский А.А. Функциональное программирование. Глава 5. Системы исполнения функциональных программ. Интерпретация простого и рекурсивного блоков. Рассмотрим последовательность состояний при исполнении простого блока: evaluate (s, e, (Letrec pairs body):c, d) = evaluate (s, newPairs ++ e, (reverse exprs) ++ ((LetrecApply n body):c), d) where (newPairs, n) = (map (\n -> (n, ?)) names, length names) (names, exprs) = unzip pairs STK, ENV, (Let x exp body):COM, DUMP STK, ENV, exp:(LetApply x body):COM, DUMP exp':STK, ENV, (LetApply x body):COM, DUMP [], (x,exp'):ENV, [body], (STK, ENV, COM):DUMP [body'], (x,exp'):ENV, [], (STK, ENV, COM):DUMP body':STK, ENV, COM, DUMP Последовательность состояний при исполнении рекурсивного блока должна отличаться тем, что вычисление связываемых значений должно проводиться в уже пополненном контексте: STK, ENV, (Letrec [(x1,e1),(x2,e2),...(xn,en)] body):COM, DUMP STK, (x1,?):(x2,?):...(xn,?):ENV, en:...e2:e1:(LetrecApply body):COM, DUMP e1':e2':...en':STK, (x1,?):(x2,?):...(xn,?):ENV, (LetrecApply body):COM, DUMP [], (x1,e1'):(x2,e2'):...(xn,en'):ENV, [body], (STK,ENV,COM):DUMP [body'], (x1,e1'):(x2,e2'):...(xn,en'):ENV, [], (STK,ENV,COM):DUMP body':STK, ENV, COM, DUMP Здесь самый тонкий момент – это замена значений в уже сформированном контексте. evaluate (s, e, (LetrecApply n body):c, d) = evaluate ([], replaceValues n s e, [body], (drop n s, drop n e, c):d)

6 Кубенский А.А. Функциональное программирование. Глава 5. Системы исполнения функциональных программ. Реализация псевдо-функции replaceValues. e1':e2':...en':STK, (x1, ):(x2, ):...(xn, ):ENV, (LetrecApply body):COM, DUMP ? ? ? e1' e2' en' Если в выражениях e1', e2', en' имеются копии контекста, то замена значений с помощью псевдо-функции replaceValues повлияет сразу на все копии. Реализованная SECD-машина – энергичная, однако, и здесь ленивый инструментальный язык реализации привносит «ленивость» в процесс интерпретации. Например, помещаемые в стек результаты вычислений функции intrinsic на самом деле будут получены, только если они реально потребуются для представления результата.

7 Ленивая версия SECD-машины. Кубенский А.А. Функциональное программирование. Глава 5. Системы исполнения функциональных программ. Введем понятие задержанного результата для того, чтобы задержать вычисление значения выражения до момента первого обращения к нему. data WHNF = C_Int Integer | C_Bool Bool | Closure String Environment Command | Oper String Int [WHNF] | Delay Environment Command evaluate (s, e, (Application f a):c, d) = evaluate ((Delay e a):s, e, f:Apply:c, d) Применение функции для случая ленивых вычислений: Вычисление задержанного результата будет происходить при выполнении встроенных операций, таких как арифметические операторы или индексация кортежа. evaluate n f args):(Delay env com):s, e, Apply:c, d) = evaluate ([], env, [com], (func:s, e, c):d) При возврате вычисленное значение выражения помещается на место аргумента функции, и применение функции повторяется уже к вычисленному значению: evaluate ([res], _, [], (func:s, e, c):d) = evaluate (func:res:s, e, Apply:c, d) Для того, чтобы избежать повторного вычисления одних и тех же значений, задержки помещаются в отдельную область памяти, а в стек вместо нее помещается указатель. Когда значение будет вычислено, результат должен быть помещен на место задержки с помощью присваивания.

8 Реализация рекурсивного блока в ленивой версии SECD-машины. evaluate (s, e, (Letrec pairs body):c, d) = evaluate ([], newEnv, [body], (s, e, c):d) where newEnv = (map (\(n, v) -> (n, (Delay newEnv v)) pairs) ++ e Здесь в новом контексте newEnv появятся задержки, содержащие ссылку на тот же самый контекст. Реализация простого блока Let остается без изменений. Выводы: SECD-машина удобна для описания последовательности команд для вычислений. Энергичная SECD-машина хорошо реализуется в энергичном языке, однако реализация рекурсивного блока требует исполнения присваиваний; для ленивого инструментального языка требуется моделирование энергичных вычислений. Реализация ленивой SECD-машины требует реализации механизма задержанных вычислений с присваиванием.