Сергей Романенко
6 января 2010 г.
В посланиях
рассматривался (в частности) такой способ реализации проблемно ориентированных (ПО) языков: в рамках функционального языка высшего порядка определяем набор “комбинаторов” (т.е. функций, отображающих одни функции в другие). Каждый комбинатор при этом соответствует какой-то конструкции определяемого языка. А применение суперкомпиляции при этом позволяет изгнать комбинаторы из программы, “скомпилировав” ПО-программу на тот язык, на котором определены комбинаторы.
Суперкомпиляцию чаще всего рассматривают как средство “оптимизации” программ, но она может использоваться и как средство анализа, т.е. выявления и доказательства свойств различных процессов и систем.
Понятно, что для применения формальных методов для анализа некоторой системы нужно, прежде всего, иметь некоторую формальную же модель этой системы. А как должна выглядеть такая модель? С точки зрения программиста, самый “естественный” подход - взять, да и написать программу, поведение которой должно “моделировать” поведение изучаемой системы. Или, говоря более абстрактным и напыщенным языком, “использовать программу, как средство представления знания”. А потом эту программу можно подвергнуть анализу (например, с помощью суперкомиляции), выявить её скрытые свойства и узнать что-то интересное про ту систему, которую изображает программа.
В некоторых случаях написать программу, формализующую некую систему, труда не составляет. Это в тех случаях, когда язык программирования уже содержит в готовом виде те понятия, которые нужны для описания системы. А если нет? Тогда может оказаться, что изготовление такой программы превращается в занудное и трудоёмкое дело.
Вот типичный пример. Моделируемая система является недетерминированной, а её нужно смоделировать с помощью языка программирования, в котором нет никакого недетерминизма: какую программу ни напиши, она оказывается детерминированной. Что же делать? Один из подходов - расширить язык программирования новыми понятиями (реализовав в его рамках некоторый проблемно-ориентированный язык) и писать программу-модель на ПО-языке, предоставляющем систему понятий адекватную решаемой задаче.
В предыдущих посланиях рассматривались различные варианты реализации λ-исчисления, не содержавшего какие-либо конструкции, связанные с недетерминизмом. А давайте-ка теперь попробуем добавить к λ-исчислению недетерминизм, реализовав “конструкцию выбора”
choice2 e1 e2
которая дожна исполняться следующим образом. При вычислении
choice2 e1 e2 следует произвольно выбрать одно из выражений
e1 или e2 и вычислить
выбранное выражение. И результат этого вычисления должен считаться
результатом вычисления всей конструкции choice2 e1 e2.
Как и в предыдущих посланиях, мы реализуем “недетерминированное” λ-исчисление как расширение языка HLL. HLL - это подмножество языка Haskell, являющееся входным языком суперкомпилятора HOSC.
Итак, нам нужно реализовать недетерминизм, а любая программа на языке
HLL - детерминированная. Откуда же может взяться недетерминизм? Ответ
прост: из внешнего мира. Используем следующий тривиальный приём: будем
считать, что при запуске программы ей на вход подаётся бесконечная
последовательность, которая говорит, какое из выражений в choice2 e1 e2
нужно выбрать: левое или правое. Будем считать, что эта
последовательность имеет следующий тип:
data Choice = L Choice | R Choice;
А когда возникает необходимость вычислить choice2 e1 e2, программа
должна заглянуть в эту последовательность и посмотреть на верхний
конструктор. Если наверху конструктор L (left), нужно выбрать левое
выражение, а если конструктор R (right) - то правое.
Понятно, что всегда можно просто сесть и написать функциональную программу, явно работающую с потоком выборов. Так часто и поступают. Например, вот здесь можно найти богатую коллекцию программ, моделирующую поведение протоколов “кеш-когерентности”:
Но писание таких программ - дело занудное, поскольку, в случае функционального языка, нужно “протаскивать” последовательность выборов через все места в программе, которые могут содержать недетерминизм. При этом программа сильно загромождается и смысл её затемняется (а значит - увеличивается вероятность ошибок).
Но можно реализовать проблемно-ориентированный (ПО) язык, в котором вся возня с последовательностью выборов будет запрятана в глубину реализации этого языка.
Начнём мы с реализации “детерминированного”, статически-типизированного λ-исчисления, а потом добавим к нему недетерминизм.
В послании
была рассмотрена реализация λ-исчисления через набор комбинаторов. При этом даже имена переменных (точнее, индексы де Брёйна) были реализованы через комбинаторы (т.е. функции высшего порядка). Впрочем, сделано это было не по необходимости, а, так сказать, “для понта” и “для прикола”. Ну, хотя бы для того, чтобы комбинаторная реализация была похожа на реализацию через интерпретатор первого порядка. Поэтому, например, в комбинаторной реализации присутствовала “среда”. А, так сказать, спортивное достижение состояло в том, что среда связывала со значениями переменные разных типов (что не получалось без введения тегов в случае интерпретатора первого порядка).
Но, как оказывается, интерпретатор такого рода можно реализовать ещё проще, вообще не используя среду! (А нет среды - нет и порождаемых ею проблем.)
А именно, в качестве “переменных” реализуемого ПО-языка можно использовать прямо переменные того языка, поверх которого реализуется ПО-язык. В литературе этот трюк известен под именем “использование абстрактного синтаксиса высшего порядка”. Суть дела проще всего объяснить на конкретном примере, посмотрев следующее задание на суперкомпиляцию: Lambda: higher-order syntax (transparent).
Будем считать, что в нашем λ-исчислении имеются булевские значения и натуральные числа, которые определяются так
data Bool = True | False;
data Nat = Z | S Nat;
После чего определяются комбинаторы var (переменная), lam
(λ-абстракция), app (аппликация) и cst (константа). Основная идея
заключается в том, что переменную x можно представлять прямо в виде
var x, а λ-абстракцию \x -> e в виде lam (\x -> e). При этом
x - это, одновременно, и переменная реализуемого языка, и переменная
языка реализации (т.е. HLL). Тогда, например, выражение (\x -> x) True
изображается следующим образом: app (lam (\x -> var x)) (cst True).
А теперь посмотрим, как определяются комбинаторы:
var = \x -> x;
lam = \f -> f;
app = \e1 e2 -> e1 e2;
cst = \a -> a
Простота и краткость этих определений (в сравнении с интерпретатором первого порядка) прямо-таки потрясает воображение (и пробуждает подозрение, что что-то тут не так, что есть в этом какое-то надувательство и обман). Но никакого обмана как раз и нет: просто все эти понятия λ-исчисления уже присутствуют в языке HLL, поэтому и нет ничего удивительного, что они столь тривиально “реализовались” на HLL.
Для полноты картины определим ещё fix, if и прибавление единицы к числу:
fix = \f -> f (fix f);
if = \e0 e1 e2 ->
case e0 of {
True -> e1;
False -> e2;
};
natS = \n -> S n;
Ну, ежели по-честному fix определять, то его следовало бы определить как
fix = \f -> app (lam f) (fix f)
но, выполнив пару редукций вручную, убеждаемся, что app (lam f) (fix f)
быстро превращается в f (fix f). Поэтому я и не удержался от искушения,
и подоптимизировал определение fix.
Теперь пробуем просуперкомпилировать несколько выражений. Получается:
cst (S (S Z)) ⟹ (S (S Z))
app (lam (\x -> var x)) (cst True) ⟹ True
lam (\x -> if x False True) ⟹
(\r-> case r of { True -> False; False -> True; })
fix (\x -> natS x) ⟹ (letrec f=(S f) in f)
Ну что же, что должно было получиться, то и получилось. Ничего неожиданного! На первый взгляд даже непонятно, зачем нужно было “весь этот огород городить”. Но эта реализация λ-исчисления - только исходная точка. Наша цель - добавить к реализуемому языку недетерминизм! При этом внешний вид программ, закодированных с помощью комбинаторов, не изменится, но изменится их семантика (и изменится реализация комбинаторов)!
Переопределим комбинаторы так, чтобы они “потихоньку” передавали друг-другу дополнительный параметр типа Choice, содержащий последовательность выборов.
data Choice = L Choice | R Choice;
Тогда комбинатор choice2 можно будет реализовать так:
choice2 = \e1 e2 c ->
case c of {
L c1 -> e1;
R c2 -> e2;
};
Есть, правда, одна проблема: в некоторых случаях вычисление
“разветвляется”: нужно вычислить два разных выражения e1 и e2. При этом,
поскольку язык “ленивый”, e1 и e2 могут вычисляться не сразу, а
постепенно по мере надобности. Немного e1 повычисляли, а потом
повычисляли e2, и т.д. Хорошо было бы снабдить e1 и e2 независимыми
последовательностями выборов: передать в e1 и e2 две последовательности
выборов - и не заботиться о взаимодействии этих двух вычислений.
Мы можем добиться возможности “разветвлять” последовательности выборов
переопределив тип данных Choice следующим образом:
data Choice = L Choice | R Choice | D Choice Choice;
Теперь L - “левый” выбор, R - “правый” выбор, а D - “разделение”
последовательности на две независимые последовательности.
После этого мы переписываем комбинаторы так, как это сделано в задании на суперкомпиляцию Lambda: non-determinism (direct).
И вот что получается.
Каждый из комбинаторов получает дополнительный параметр c. Комбинаторы
cst и natZ его просто игнорируют:
cst = \a c -> a;
natZ = \c -> Z;
Комбинатор natS должен вычислить свой аргумент и надеть на результат
конструктор S. Он так и делает, но передаёт c своему аргументу:
natS = \e c -> S (e c);
var x c передаёт c в x, поскольку значением переменной является
выражение, которое нуждается в аргументе c.
var = \x c -> x c;
lam f с просто отбрасывает c (как и cst a c):
lam = \f c -> f;
Самые интересные случаи - app e1 e2 с и choice2 e1 e2.
В случае с app e1 e2 c проблема в том, что сначала нужно вычислить
e1, а потом применить то, что получится к e2. При этом мы не знаем,
какую часть последовательности выборов “съест” e1. Поэтому, мы требуем,
чтобы последовательность выборов c разветвилась на c1 и c2:
app = \e1 e2 c ->
case c of {
D c1 c2 -> (e1 c1) e2 c2;
};
c1 используется при вычислении e1, а e2 - при применении результата
вычисления e1 к e2.
Ну, а определение choice2 e1 e2 c говорит само за себя:
choice2 = \e1 e2 c ->
case c of {
L c1 -> e1 c1;
R c2 -> e2 c2;
};
Есть, правда, в определениях app и choice2 одна тонкость: используются
case-выражения, в которых набор конструкторов - неполный. До какого-то
момента так делать не разрешалось, но недавно это ограничение в HOSC
было снято. Семантика неполных case-выражений такая. Если в процессе
исполнения программы требуется выполнить редукцию выражения вида
case C ... of { ... }
а конструктор C не указан ни в одной из ветвей case-выражения,
считается, что возникла фатальная ошибка, и выполнение программы
завершается.
Поэтому, если в app попадает c, у которого на верхнем уровне не D, то
программа просто “грохается”. А если в choice2 попадает c, у которого на
верхнем уровне не L и не R, то и тогда программа аварийно завершается.
Конечно, такой странный дизайн программы плохо подходит для “нормального” исполнения программ. Но в данном случае мы намереваемся использовать программы для моделирования поведения каких-то систем: описываем поведение системы в виде программы, а потом подвергаем программу суперкомпиляции, чтобы что-то узнать о её поведении. При этом одной из типичных задач является “проблема достижимости”. Например, нужно доказать, что какие исходные данные на вход программы ни подавай, её не удастся загнать в некоторые “нехорошие” состояния. Тогда, если выполнение программы аварийно завершается для каких-то исходных данных, это просто означает, что программа не сумела попасть в “нехорошее” состояние. Ну и слава Богу!
А суперкомпиляция, в отличие от обычного исполнения, методически исследует все возможные способы исполнения программы. И то, что на каких-то ветвях выполнение программы аварийно завершается, проблем при суперкомпиляции не создаёт.
В определении комбинатора if используется тот же приём, что и в
реализации app: разделение последовательности выборов:
if = \e0 e1 e2 c ->
case c of {
D c1 c2 ->
case e0 c1 of {
True -> e1 c2;
False -> e2 c2;
};
};
И, наконец, определение комбинатора fix:
//fix = \f c -> app (lam f) (fix f) c;
fix = \f c -> f (fix f) c;
Выражение f (fix f) c является слегка оптимизированной версией выражения
app (lam f) (fix f) c, учитывающей, что lam f просто игнорирует c.
Ну вот, а теперь попробуем посуперкомпилировать некоторые λ-выражения и посмотрим, что получается.
(choice2 (cst True) (cst False)) c ⟹
case c of { L c1 -> True; R c2 -> False; }
(choice2 (cst Z) (choice2 (cst (S Z)) (cst (S(S Z))))) c ⟹
case c of { L c1 -> Z;
R c2 -> case c2 of { L c3 -> (S Z);
R c4 -> (S (S Z)); }; }
(app (lam (\x -> if (var x) (cst False) (cst True))) (cst True)) c ⟹
case c of { D c1 c2 -> case c2 of { D c3 c4 -> False; }; }
(fix (\x -> choice2 natZ (natS (var x)))) c ⟹
(letrec f=(\c1 ->
case c1 of {
L c2 -> Z;
R c3 -> S (f c3); })
in (f c))
Наиболее интересен последний пример, показывающий генерацию
“недетерминированного” натурального числа произвольной величины. Если
развернуть fix, то получится бесконечная последовательность вложенных
конструкций choice2:
choice2 natZ (natS (
choice2 natZ (natS (
choice2 natZ (natS ( ... )) )) ))
Происходит выбор между Z и S(x), где x - “недетерминированное”
натуральное число. Вот и получается, что может породиться любое
натуральное число. Красота!