Отзыв официального оппонента (Трассирующая нормализация)

ОТЗЫВ1Официального оппонентадоктора физико-математических наук профессораНепейвода Николая Николаевичана диссертацию Д.А. Березуна «Трассирующая нормализация», представленную на соискание ученой степени кандидата физико-математических наук поспециальности 05.13.11 — Математическое и программное обеспечение вычислительных машин, комплексов и компьютерных сетейДиссертация состоит из введения, шести глав и трёх приложений.Актуальность темы диссертации обусловлена тем, что нет практическойреализации блестящей теоретической находки Футамуры — Турчина —А.П. Ершова — Глюка: четыре проекции Футамуры. Она в принципе даётвозможнооть построить автоматически интерпретатор, транслятор и генератор компиляторов и тем же способом автоматически оптимизировать его. Дляэтого нужно всего-навсего иметь полный и корректный частичный вычислитель (специализатор) для реализуемого языка на любой внешней системе илюбого качества, позволяющего хотя бы один раз исполнить его сам на себе.А далее уже идут автоматические улучшения.

Беда в том, что до сих пор полный и корректный специализатор ни для одного достаточно широкого языка не запрограммирован. Одной из проблем является здесь исключительнонизкая эффективность существующих частичных специализаторов для полных языков. Для отдельных их фрагментов известны достаточно красивыеи эффективные программы-специализаторы, но из-за ограниченности обрабатываемого языка они не обладают свойством самоприменимости. Даннаяработа является красивым и эффективным шагом по направлению к решению давно назревшей проблемы.Во введении полностью адекватно описаны результаты работы, жаль лишь,что их взаимосвязь с проекциями Футамуры не отражена.В главе 1 «Обзор области исследований» описана история вопроса, ноне полностью. Важнейшее с точки зрения актуальности задач диссертациипонятие проекций Футамуры вводится лишь в пятой главе, и умалчиваетсяо возникших практических трудностях при их применении.

Но с чисто формальной точки зрения обзор литературы весьма полон и полностью адекватен нынешнему состоянию исследований, если забыть историю и перспективы. Впрочем, большего в кандидатской диссертации и не требуется.В этой главе сосредоточено наибольшее количество неаккуратностей инеточностей. Видно, что автор относился к изложению чужих результатовне слишком бережно, в отличие от своих, представленных в дальнейшем, часто скатываясь на цитирование «общеизвестных истин», которые обычно не2полностью верны, и часто не заглядывая пристально в исходные работы, которые апостолы слишком часто перевирают и упрощают, опуская «неприятные» оговорки и результаты.

Перечислим шероховатости.На стр. 14 неверно утверждение, что в данном языке скобки могут считаться лишь украшением. Если бы автор ввёл бинарную операцию применения @ в префиксной либо постфиксной польской записи, то, учитывая. чтоон часто её опускает, скобки действительно могли бы считаться украшениемдля удобства чтения, а в его определении они необходимый элемент синтаксиса.На той же станице вводится соглашение Барендрегта, а на стр. 15 нумерация де Брауна, которые кажутся отнюдь не необходимыми для данной работы, поскольку часто автор вынужден делать оговорки об отступлениях отних (см. далее стр. 38 и др.).На стр. 17, рис.

3. не указано, что требуется пересчёт номеров.На стр. 21 приведено недостаточно общее определение вызова по необходимости. Почти забыто, что фраза «без ограничения общности для простоты можно считать, что все функции одноместные» в исследовании программслишком часто приводит к ошибкам, если имеется возможность вылета программы или недетерменированности. Отсутствия побочных эффектов недостаточно.

И в этом случае определение, переписанное диссертантом, проваливается.А на стр. 22, наоборот, диссертантом даны свежие, прекрасные и полностью адекватные комментарии к аппликативному порядку.На стр. 24 нет точного определения η-длинной формы.На стр. 28 в примере описка: должно быть, видимо, λw, y вместо λz, y.Вызывает раздражение теорема 1, поскольку часть её доказательства отложена на неопределённое время и не дана ссылка, где же оно завершается.Её надо было бы переставить в гораздо более позднюю часть работы.

Кстати,теорема верна, я доказал её другим, более простым, способом.Глава 2 «Полная головная редукция» описывает главное понятие диссертации, давшее возможность автору существенно оптимизировать алгоритм частичных вычислений.Теорема 2 на стр. 39 сформулирована весьма неуклюже и может бытьнеправильно понята. Необходимо было ввести вспомогательное определение.На стр. 45 не указано, какие именно следствия из теоремы 2 нужно использовать.Глава 3 «Алгоритм трассирующей нормализации» написана наименеечётко в диссертации.

Алгоритм не выделен явно. Вместо алгоритма говорится о нескольких семантиках. В определении обхода не указано, последовательность это всех вершин дерева или части их. Как положительный момент3стоит отметить исключительно чёткое изложение идеи метода на стр. 52. Акак квинтэссенцию отрицательного, фразу со стр. 48: «Для краткости и наглядности изложения, она (семантика, уточнение ННН) симулирует все шаги вычислений, не возвращая реального результата». Тем самым автор показал свои основные практические находки.Глава 4 «Корректность алгоритма трассирующей нормализации» является основной технической главой в теории. Она практически вся посвящена одному большому доказательству, в середине которого постепенно всётаки частично определяется алгоритм.

За аргументами было исключительнотрудно следить, поскольку автор использовал цветные стрелки, а на чёрнобелой печати они все либо выглядят серыми, либо вообще практически невидны («прекрасный» пример здесь стр. 63). Перед теоремой 5 надо былоявно выделить начало и конец алгоритма, корректность которого утверждается, и лучше было записать его в квазиформальном языке. Ссылка в текстеквазиалгоритма «восстанавливается так же, как в случае BUNP» плоха потрём критериям. Нет точного указания на страницу или параграф, а лучшевсего было бы на конкретный пункт конкретного алгоритма,Глава 5 «Компиляция путём специализации» показывает, что алгоритмавтора наконец-то осуществляет проекции Футамуры для простейшего функционального языка. Это принципиальное достижение автора, которое, будьоно прилично изложено, безусловно было бы на уровне прекрасной кандидатской диссертации.Глава 6 «Трассирующая нормализация и стратегии вычислений» рассматривает взаимосвязь алгоритмов автора с известными дисциплинами вычислений в функциональных языках.

Сравнение чёткое, ясное, корректное,это лучшая глава диссертации.В Заключении корректно описаны результаты и перспективы работы стеоретической и практической точки зрения.В «Приложениях» приведена реализация алгоритма и пример её работы.4Итоги. Теоретические результаты работы новы, интересны, обоснованность их не представляется возможным окончательно проверить из-за бессвязного изложения, хотя проверки независимыми доказательствами отдельных результатов показали, что, видимо, они верны. Новый подход представляется перспективным для дальнейшего развития. Экспериментальная реализация показала, что он достаточно эффективный, общий и сильный.Работа полностью соответствует паспорту специальности.

Апробация еёи список публикаций выглядят весьма достойно.НедостаткиБессвязное изложение, в нескольких важнейших местах нарушающее критерии строгости.Отсутствие сравнения со специализаторами других авторов (и это приотличнейшем списке литературы и списке апробаций).Множество технических погрешностей, которые были бы простительныпри общем связном изложении..