Сергей Романенко
3 июня 2009 г.
Похоже, что в заметке
некоторые мысли я сформулировал недостаточно вразумительно. Поэтому, захотелось остановиться на кое-каких деталях более подробно.
Верно ли, что я - “враг Рефала”? Неверно! Особенно, если вспомнить, что я являюсь соавтором Рефала Плюс и книги по Рефалу Плюс:
А также и соавтором нескольких реализаций Рефала. Например - Рефала Плюс.
Поэтому, для меня воевать с Рефалом - всё равно что рубить сук, на котором я сам же и сижу.
Настаиваю ли я на том, что различие между “строгими” и “ленивыми” языками существует и реально? А как же я на этом могу не настаивать? Иначе “испарился” бы и сам предмет нашего обсуждения.
(Естественно, если под языком понимать только некий синтаксис без семантики, то и различие между “строгими” и “ленивыми” по-определению исчезает. Поэтому, в рамках нашей дискуссии, подразумевается, что язык - это не только синтаксис, но ещё и семантика.)
Говоря по-простому, язык является “строгим”, если вычисление функции начинается только после того, как полностью вычислены ей аргументы. И, соответственно, “ленивым”, если вычисление функции может начинаться ещё до того, как её аргументы полностью вычислены.
Естественно, что разных разновидностей “ленивости” существует много, ибо конкретизировать это понятие можно только конкретизировав понятие “частично вычисленный аргумент”. Для языков вроде Хаскеля (Haskell) понятие “частичной вычисленности” определяется через “приведение к слабой головной нормальной форме”, но возможны и другие варианты (например, “fuller laziness”).
То, что различие между “строгой” и “ленивой” семантикой реально существует показывает хотя бы такая программка:
omega(x) = omega(x);
erase(x) = Stop;
f(u) = erase(omega(Nil));
В случае “строгого” исполнения вычисление f(Nil) никогда не завершается,
а в случае “ленивого” - завершается всегда. Надеюсь, все согласны с тем,
что между “никогда” и “всегда” всё-таки есть маленькое различие? :-)
Следующий вопрос такой: является ли Рефал “строгим” или “ленивым” языком? В абстрактной постановке ответить на него нельзя, поскольку никто никогда не запрещал всем желающим придумывать и реализовывать разные разновидности Рефала и вариации на тему Рефала. И семантика у этих вариаций может быть тоже разная.
Например, входным языком суперкомпилятора SCP4 является Рефал-5.
Является ли этот язык “строгим” или “ленивым” можно “методом научного тыка”: переписав вышеприведённую программу на Рефале-5:
Omega { e.X = <Omega e.X>; }
Erase { e.X = Stop; }
F { e.U = <Erase <Omega Nil>>; }
Запускаем вычисление <F Nil> и смотрим: зациклится программа или нет? Судя по
описанию Рефала-5 - зациклится (а я описанию верю :-) ). А то, что эта программа
зациклится в случае Рефала Плюс - я не только верю, но и знаю…
Следующий вопрос: верно ли, что я считаю “ленивые” языки “хорошими”, а “строгие” языки - “плохими”. И что, на этом основании, я считаю Рефал-5 и Рефал Плюс “плохими” языками?
Это - неверно! Суперкомпиляторы HOSC и SPSC хотя и обрабатывают программы на ленивых языках, но сами-то написаны на языке Скала (Scala). А язык Скала (если рассматривать его “функциональную” часть) - это типичный “строгий” язык. Если бы мы (я и Илья Ключников) свято верили в абсолютное превосходство “ленивых” языков над “строгими”, то HOSC и SPSC были бы написаны на “ленивом” языке (например, на Хаселе).
И вообще, абстрактные рассуждения по поводу того, какие языки лучше, “ленивые” или “строгие”, имеют не больше смысла, чем дискуссии на тему “Кто лучше: брюнетки или блондинки?” Зависит от того, какая именно блондинка/брюнетка, и в каких обстоятельствах…
В своей заметке я обсуждал достоинства “ленивости” для случая, когда суперкомпиляция используется как средство анализа программ, а не оптимизации программ. В этом случае удобнее использовать суперкомпилятор, который сохраняет семантику программ.
Например, нам хочется исследовать свойства завершаемости программы. Суперкомпилируем исходную программу и получаем остаточную программу, для которой можем легко показать, что она всегда завершается. Какой вывод мы можем на основании этого сделать по поводу исходной программы? Если суперкомпилятор сохраняет семантику программы, сразу же делаем заключение, что это верно и в отношении исходной программы. А если суперкомпилятор на обладает этим свойствам? Тогда мы о завершаемости исходной программы не узнаём НИЧЕГО.
Последний вопрос такой: если мы хотим, чтобы суперкомпилятор строго сохранял семантику программ, должен ли его входной язык быть обязательно “ленивым”? Ответ отрицательный: входной язык не обязательно должен быть “ленивым”! Если постараться, то можно обойтись и без этого. Вот статья на эту тему:
Но, если мы хотим использовать суперкомпилятор для анализа формальных систем, кодируя их в виде программ, написанных на входном языка суперкомпилятора, то зачем в качестве входного языка выбирать “строгий” язык?
Для того, чтобы обеспечить сохранение семантики в случае “строгого” языка, суперкомпилятор должен предпринимать какие-то дополнительные усилия: нужны дополнительные анализы, дополнительные проверки, рассмотрение разных особых случаев. От этого суперкомпилятор усложняется. А если суперкомпилятор используется как средство анализа или верификации, то “встаёт ребром” вопрос о корректности самого суперкомпилятора. Нужно доказывать теорему, что “всё чисто”, что метавычисления правильно имитируют обычные вычисления. Чем “толще” и запутаннее сам суперкомпилятор, тем “толще” и запутаннее будет доказательство его корректности. И тем выше вероятность, что само доказательство корректности будет содержать ошибки. :-)