Компиляция из MLC в RAM0
May. 15th, 2013 03:23 pmПрограммы на языке MLC (Macro Lambda Calculus) - пример доступен на GitHub - имеют следующий вид:
N1 = M1;
...
Nm = Mm;
M0.
Выражение M0 может содержать произвольное число вхождений имен макросов N1, ... , Nm, а также свободных переменных - обозначим их x1, ... , xn. Комбинатор M, нормальную форму которого мы фактически ищем, получается из программы следующим образом:
M = x1, ... , xn: (N1, ... , Nm: M0) M1 ... Mm.
Комбинатор M, в свою очередь, представим в исчислении взаимодействия, воспользовавшись направленной версией компактной кодировки λ-выражений. Заметим, что конфигурация <x | Γ(M, x)>, как можно видеть из определения, содержит только редексы по левому разыменованию. Следовательно, чтобы инициализировать нашу систему слепой перезаписи графов, достаточно все уравнения конфигурации положить в стек, соответствующий левому разыменованию.
Полученную в результате структуру памяти можно восстановить некоторой последовательностью I инструкций Z, A, L, N и S машины RAM0. Основной цикл работы нашей системы слепой перезаписи графов, реализующей редукцию сетей взаимодействия, также может быть представлен некоторой последовательностью R инструкций Z, A, L, N и S, которая не зависит от вычисляемого выражения. Таким образом, исходный код на языке MLC может быть скомпилирован в следующую программу RAM0:
I;
loop: R;
goto loop;
Данная программа не содержит инструкцию C для условного перехода. Такие детали, как стратегия вычисления, остановка машины, обработка дна стеков и механизм "read-back" во время стягивания конфигурации, были здесь намеренно опущены, чтобы не нагромождать и без того уже объемное изложение.
N1 = M1;
...
Nm = Mm;
M0.
Выражение M0 может содержать произвольное число вхождений имен макросов N1, ... , Nm, а также свободных переменных - обозначим их x1, ... , xn. Комбинатор M, нормальную форму которого мы фактически ищем, получается из программы следующим образом:
M = x1, ... , xn: (N1, ... , Nm: M0) M1 ... Mm.
Комбинатор M, в свою очередь, представим в исчислении взаимодействия, воспользовавшись направленной версией компактной кодировки λ-выражений. Заметим, что конфигурация <x | Γ(M, x)>, как можно видеть из определения, содержит только редексы по левому разыменованию. Следовательно, чтобы инициализировать нашу систему слепой перезаписи графов, достаточно все уравнения конфигурации положить в стек, соответствующий левому разыменованию.
Полученную в результате структуру памяти можно восстановить некоторой последовательностью I инструкций Z, A, L, N и S машины RAM0. Основной цикл работы нашей системы слепой перезаписи графов, реализующей редукцию сетей взаимодействия, также может быть представлен некоторой последовательностью R инструкций Z, A, L, N и S, которая не зависит от вычисляемого выражения. Таким образом, исходный код на языке MLC может быть скомпилирован в следующую программу RAM0:
I;
loop: R;
goto loop;
Данная программа не содержит инструкцию C для условного перехода. Такие детали, как стратегия вычисления, остановка машины, обработка дна стеков и механизм "read-back" во время стягивания конфигурации, были здесь намеренно опущены, чтобы не нагромождать и без того уже объемное изложение.
