Разные мысли о метавычислениях, суперкомпиляции, специализации программ. И об их применениях. Желающие приглашаются в соавторы блога.

среда, 3 июня 2009 г.

Отнесёмся к "ленивости" со всей "строгостью"! (Или что лучше, блондинки или брюнетки?)

Похоже, что в заметке

некоторые мысли я сформулировал недостаточно вразумительно. Поэтому, захотелось остановиться на некоторых деталях более подробно.

Верно ли, что я - "враг Рефала"? Неверно! Особенно, если вспомнить, что я являюсь соавтором Рефала Плюс и книги по Рефалу Плюс:

Р.Гурин, С.Романенко. Язык программирования Рефал Плюс. Курс лекций. Учебное пособие для студентов университета города Переславля. - Переславль-Залесский: "Университет города Переславля" им.А.К.Айламазяна, 2006. - 222 с. PDF

А также и соавтором нескольких реализаций Рефала, например

Поэтому, для меня воевать с Рефалом - всё равно что рубить сук, на котором я сам же и сижу.

Настаиваю ли я на том, что различие между "строгими" и "ленивыми" языками существует и реально? А как же я на этом могу не настаивать? Иначе "испарился" бы и сам предмет нашего обсуждения.

(Естественно, если под языком понимать только некий синтаксис без семантики, то и различие между "строгими" и "ленивыми" по-определению исчезает. Поэтому, в рамках нашей дискуссии, подразумевается, что язык - это не только синтаксис, но ещё и семантика.)

Говоря по-простому, язык является "строгим", если вычисление функции начинается только после того, как полностью вычислены ей аргументы. И, соответственно, "ленивым", если вычисление функции может начинаться ещё до того, как её аргументы полностью вычислены.

Естественно, что разных разновидностей "ленивости" существует много, ибо конкретизировать это понятие можно только конкретизировав понятие "частично вычисленный аргумент". Для языков вроде Хаскеля (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 были бы написаны на "ленивом" языке (например, на Хаселе).

И вообще, абстрактные рассуждения по поводу того, какие языки лучше, "ленивые" или "строгие", имеют не больше смысла, чем дискуссии на тему "Кто лучше: брюнетки или блондинки?" Зависит от того, какая именно блондинка/брюнетка, и в каких обстоятельствах...

В своей заметке я обсуждал достоинства "ленивости" для случая, когда суперкомпиляция используется как средство анализа программ, а не оптимизации программ. В этом случае удобнее использовать суперкомпилятор, который сохраняет семантику программ.

Например, нам хочется исследовать свойства завершаемости программы. Суперкомпилируем исходную программу и получаем остаточную программу, для которой можем легко показать, что она всегда завершается. Какой вывод мы можем на основании этого сделать по поводу исходной программы? Если суперкомпилятор сохраняет семантику программы, сразу же делаем заключение, что это верно и в отношении исходной программы. А если суперкомпилятор на обладает этим свойствам? Тогда мы о завершаемости исходной программы не узнаём НИЧЕГО.

Последний вопрос такой: если мы хотим, чтобы суперкомпилятор строго сохранял семантику программ, должен ли его входной язык быть обязательно "ленивым"? Ответ отрицательный: входной язык не обязательно должен быть "ленивым"! Если постараться, то можно обойтись и без этого. Вот статья на эту тему:

Jonsson, P. A. and Nordlander, J. 2009. Positive supercompilation for a higher order call-by-value language. In Proceedings of the 36th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Savannah, GA, USA, January 21 - 23, 2009). POPL '09. ACM, New York, NY, 277-288. DOI=http://doi.acm.org/10.1145/1480881.1480916 PDF

Но, если мы хотим использовать суперкомпилятор для анализа формальных систем, кодируя их в виде программ, написанных на входном языка суперкомпилятора, то зачем в качестве входного языка выбирать "строгий" язык?

Для того, чтобы обеспечить сохранение семантики в случае "строгого" языка, суперкомпилятор должен предпринимать какие-то дополнительные усилия: нужны дополнительные анализы, дополнительные проверки, рассмотрение разных особых случаев. От этого суперкомпилятор усложняется. А если суперкомпилятор используется как средство анализа или верификации, то "встаёт ребром" вопрос о корректности самого суперкомпилятора. Нужно доказывать теорему, что "всё чисто", что метавычисления правильно имитируют обычные вычисления. Чем "толще" и запутаннее сам суперкомпилятор, тем "толще" и запутаннее будет доказательство его корректности. И тем выше вероятность, что само доказательство корректности будет содержать ошибки. :-)

4 комментария:

  1. Кажется, я тоже выразился не очень аккуратно. Мне меньше всего хотелось бы затевать дискуссии о том, что лучше, а что хуже. Вот основной смысл моего коммента:
    Известно, что суперкомпилятор рефала расширяет "семантику", в смысле - область терминируемости. Но это есть свойство SCP, а не недостаток. Оно вовсе не делает его бесполезным (и я, собственно, и пытался это обосновать). Его, конечно же, надо понимать и учитывать при применении. Да, наверно будет полезна и версия SCP для особых приложений (типа: анализ терминируемости в условиях строгого интерпретатора), которая "сохраняет семантику".
    Но это не значит, что суперкомпилятор обязан всегда "сохранять семантику" (и при оптимизации, и при анализе).

    ОтветитьУдалить
  2. Совершенно согласен с тем, что не обязательно требовать, чтобы специализатор (или суперкомпилятор, если он используется в качестве специализатора/оптимизатора) строго сохранял семантику исходной программы. Обязательно требуется только одно: чтобы семантика не изменялась "на области определения" исходной программы. Т.е. если исходная программа завершается и выдаёт результат для каких-то исходных данных, то и остаточная программа должна завершаться и выдавать _такой же_ результат для этих исходных данных.

    А если исходная программа "падает" или зацикливается для какого-то входа, то можно разрешить, чтобы остаточная программа делала что угодно.

    Почему выгодно делать такое послабление? Да потому, что это "развязывает руки" специализатору, и позволяет ему более "нахально" и агрессивно преобразовывать программу. Например, в исходной программе есть большой кусок Omega, который долго и упорно вычисляет некое X. И в общем случае, это X потом используется. Но при специализации программы вдруг выясняется, что при заданных ограничениях на входные данные, программа исполняет кусок Omega, получает X, а потом этот X выбрасывает на помойку. Оказалось, что он не нужен. Можно ли выкинуть кусок Omega? Если выкинем, то программа станет короче, и работать будет быстрее. Значит, вроде, выкинуть Omega - и приятно, и полезно. (Но "область определения" программы при этом может расшириться, если Omega иногда зацикливается или "падает".)

    Однако, есть случаи, когда семантику программ нужно сторого сохранять даже если специализация программы делается ради оптимизации (а не ради анализа программы). Например, в банке стоит компьютер, а в нём - программа, которая деньги считает. И вот, программа начинает деньги перекладывать с одного счёта на другой и при этом происходит какая-то гадость (переполнение, деление на нуль или null pointer exception). Программа "падает" и финансовая операция не выполняется. Прибегают люди, изучают, в чём дело, исправляют программу.

    А теперь представим, что программу "прооптимизатовали" и она начала благополучно исполнять то же самое действие (но неправильно). И занимается этим несколько дней. А когда замечают, что что-то не так, то она уже столько успела нагадить, что не приведи Господь!

    Вывод: при специализации можно смело расширять область определения программы, если есть возможность надёжно проверить корректность исходных данных ещё до запуска программы. Иногда это реально! Но во многих случаях корректность входных данных проверить практически невозможно. Например, в случае веб-приложений, когда приходят клиенты (или хакеры) и начинают "засовывать ломик" в приложение. И, с виду "бесполезный", кусок Omega может находиться в приложении как раз для того, чтобы заставить его "падать", когда создаётся нехорошая ситуация. Многие вещи трудно проверить на самом входе, но гораздо легче проконтролировать в середине вычислений.

    ОтветитьУдалить
  3. > А теперь представим, что программу "прооптимизатовали" и она начала благополучно исполнять то же самое действие

    такое возможно только, если семантика исходного языка была описана неправильно.
    если программа умеет падать, то это необходимо вносить в семантику языка.
    и к программе
    omega(x) = omega(x);
    erase(x) = Stop;
    f(u) = erase(omega(Nil));
    добавляется еще доп. семантика:
    результатом работы каждой функции является ее нормальный результат или ошибка(исключение).
    соответственно, если в исходной семантике при редукции выражения: c(f(x)),где c(y)=const - получалось, что c(f(x))=const,то в новой семантике будет:
    c(f(x))=const, для случая f(x)-норма, и error, для случая, когда f(x)-error

    и при анализе исходной программы мы получим частичный ответ:
    f(u)=stop, для случая, когда omega(x) - не падает, и f(u)=error, если omega(x)-падает.

    ps
    таким же образом можно вводить и зацикленность.
    с(f(x))=const, если f(x)-не зацикливается,
    c(f(x))=зацикливается, если f(x)-зацикливается

    ОтветитьУдалить
  4. В ленивом языке omega(x) не падает никогда, поскольку зацикливается для любого x (а значением x не интересуется и до попытки вычислить x дело не доходит). В строгом языке omega(x) может упасть в том смысле, что упадёт вычисления x и omega даже не успеет заработать (стало быть, не сможет и зациклиться).

    ОтветитьУдалить

Постоянные читатели