Настоящая качественная научно-исследовательская работа не столько отвечает на все вопросы и ставит точки над всеми i (хотя без этого ее и не существует), сколько задает вопросы новые и открывает новые области исследований и горизонты. Ярким представителем такой науки является работа Рода Берстала и Джона Дарлингтона "A Transformation System for Developing Recursive Programs" 1977 года, являющейся одной из самых часто цитируемых работ, посвященных преобразованиям программ. Текст статьи можно найти через
citeseerx и google
scholar, а заодно и посмотреть на другие работы, ссылающиеся на статью.
Немного об авторах. Авторы оставили большой след в информатике. Чего стоит то, что при документировании придуманного же ими языка NPL они придумали и использовали термин "set comprehension", ставший впоследствии "list comprehension" (
link1,
link2). Язык NPL и его потомок язык Hope были одними из первых языков, где использовались алгебраические типы данные и сопоставление с образцом (
"History of Haskell" by Paul Hudak, John Hughes, Simon Peyton Jones, Philip Wadler). Род Берсталл считает главным своим интересом тибетский буддизм (
автобиография), а Джон Дарлингтон последнее время занимается грид-вычислениями.
Как говорил Набоков в "Лекциях по зарубежной литературе", настоящее чтение - это перечитывание. Работу Берстала и Дарлингтона (БД) я пробежал года 3 назад без детального вглядывания, но читая различную литературу по методам преобразования программ, то там то сям натыкался на фразы, что это вот это вот соответствует тому, что БД называет "эврика" и что является самым главным шагом любого преобразования. Такое сравнение я встречал достаточно часто, поэтому у меня непроизвольно сложилось впечатление, что БД - некоторая магия, где самое главное - эврика. При перечитывании все оказалось более интересно.
В статье рассматривается система преобразований программ, которые записаны в виде рекурсивных уравнений. В статье вначале вводится система в виде отношения преобразования (или исчисления) - к системе уравнений можно применять следующие правила переписывания (в любом порядке):
- Definition - добавить к системе новое уравнение (конечно, добавляется так, что нет противоречия с существующими).
- Instantiation - специализация существующего уравнения. Например, есть уравнение f(x) = x. Можно добавить уравнение f(0) = 0;
- Unfolding - Пусть есть уравнение e1 = e2. Тогда в правой части некоторого уравнения e1 можно заменить на e2.
- Folding - Обратное развертке - e2 можно заменить на e1.
- Abstraction - ввести локальные определения (вроде let-выражений). Этот шаг позволяет избежать повторных вычислений. Например f(g(x), g(x)) можно заменить на f(y, y) where y = g(x).
- Laws - встроенные в систему свойства ассоциативности, коммутативности и т.д. операций.
Затем говорится, что такое отношение частично корректно. - Если преобразованная функция завершается и выдает какой-то результат, то этот результат соответствует тому, что выдает исходная функция. Свойства завершаемости в общем случае не сохраняются - преобразованная функция может не завершаться, тогда как исходная завершается.
Дальше самое интересное - надо задать стратегию применения этих правил.
Авторы предлагают простую стратегию:
- Make any necessary definitions.
- Instantiate
- For each instantiation unfold repeatedly. At each stage of unfolding execute 4, 5.
- Try to apply laws and where-abstraction
- Fold repeatedly
Stages (1) and (2) require some invention from the user, (4) requires his discretion, but (3) and (5), unfolding and folding, are routine symbol manipulation.
Гарантия корректности преобразовании - тоже часть стратегии. Затем они описывают реальную работающую систему, которая умеет делать шаги 3, 4, 5 автоматически. Но шаги 1 и 2 остаются за пользователем.
И система работает. Кстати написание такой системы (по статье) было бы хорошим упражнением для дипломника или для аспиранта.
И большую часть статьи авторы показывают, как такая стратегия работает. - На примерах, когда шаги 1 и 2 делаются "волшебным" образом. В рабочей системе БД (наверное, ее уже не найти и не запустить) шаги 1 и 2 должны быть сделаны пользователем ДО ТОГО, КАК СИСТЕМА НАЧНЕТ РАБОТАТЬ.
Смысл статьи в следующем: такая система и стратегия очень хорошо работает, при условии, что кто-то сделает правильно шаги 1 и 2. Поэтому содержательная работа в данном контексте - научиться механически делать шаги 1 и 2. Еще раз подчеркну, что в системе БД шаги 1 и 2 делаются пользователем ДО ТОГО, КАК СИСТЕМА НАЧНЕТ ПРЕОБРАЗОВАНИЯ. Почему это важно? Позволяет сделать набор "хороших примеров" и показать, что стратегия работает.
К сожалению, часто, когда ссылаются на БД (и из-за этого возникает непонимание) или когда сравнивают некоторую систему с БД, описывают, будто бы шаги 1 и 2 должны быть выполнены во время работы системы, ПОСЕРЕДИНЕ ПРЕОБРАЗОВАНИЙ.
Нет, шаги 1 и 2 выполняются до начала преобразований человеком - так в оригинальной статье.
Интересно изучить расширение системы БД, - метасистему по отношению к систему БД, которая по какой-то тактике или стратегии выполняет шаги 1 и 2 в автоматическом режиме, - наверное такие есть.
Так вот, работа Берстала и Дарлингтона как-раз и открывает новые области исследования - "как делать шаги 1 и 2, КАК ПРИДУМЫВАТЬ ЭВРИКИ?", и поэтому является настоящей наукой.
PS. В некоторой степени, система БД тестирует работоспособность эврик (под своим собственным углом зрения, конечно).
