Эврика!! - "A Transformation System for Developing Recursive Programs" by Rod Burstall & John Darlington

Настоящая качественная научно-исследовательская работа не столько отвечает на все вопросы и ставит точки над всеми 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 назад без детального вглядывания, но читая различную литературу по методам преобразования программ, то там то сям натыкался на фразы, что это вот это вот соответствует тому, что БД называет "эврика" и что является самым главным шагом любого преобразования. Такое сравнение я встречал достаточно часто, поэтому у меня непроизвольно сложилось впечатление, что БД - некоторая магия, где самое главное - эврика. При перечитывании все оказалось более интересно.

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

1. Definition - добавить к системе новое уравнение (конечно, добавляется так, что нет противоречия с существующими).
2. Instantiation - специализация существующего уравнения. Например, есть уравнение f(x) = x. Можно добавить уравнение f(0) = 0; 
3. Unfolding - Пусть есть уравнение e1 = e2. Тогда в правой части некоторого уравнения e1 можно заменить на e2.
4. Folding - Обратное развертке - e2 можно заменить на e1.
5. Abstraction - ввести локальные определения (вроде let-выражений). Этот шаг позволяет избежать повторных вычислений. Например f(g(x), g(x)) можно заменить на f(y, y) where y = g(x).
6. Laws - встроенные в систему свойства ассоциативности, коммутативности и т.д. операций.

Затем говорится, что такое отношение частично корректно. - Если преобразованная функция завершается и выдает какой-то результат, то этот результат соответствует тому, что выдает исходная функция. Свойства завершаемости в общем случае не сохраняются - преобразованная функция может не завершаться, тогда как исходная завершается.

Дальше самое интересное - надо задать стратегию применения этих правил.

Авторы предлагают простую стратегию:

1. Make any necessary definitions.
2. Instantiate
3. For each instantiation unfold repeatedly. At each stage of unfolding execute 4, 5. 
4. Try to apply laws and where-abstraction
5. 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. В некоторой степени, система БД тестирует работоспособность эврик (под своим собственным углом зрения, конечно).