Отзыв научного руководителя (Трассирующая нормализация)

ОТЗЫВ научного руководителя на диссертацию Даниила Андреевича Березуна <<Трассирующая нормализация», представленную на соискание ученой степени кандидата физико-математических наук по специальности 05.13.11 — математическое и программное обеспечение вычислительных машин, комплексов и компьютерных сетей Лямбда-исчисление является классической моделью вычислений и используется, наряду с машиной Тьюринга, алгоритмами Поста и другими формализмами, в сфере исследований по теории вычислимости, а также в теоретическом программировании.

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

В недавних работах С.-НЛ..Опя и ЖВ1шп был введен подход под названием трассирующая нормализация, позволяющий выполнять нормализацию без стандартных средств — бета-редукции, окружений и сохраняющий анализируемый терм неизменным. Ценность данного подхода заключается, помимо чисто теоретических перспектив, также еще и в том, что с его разработкой становится возможным использовать смешанные вычисления для автоматического порождения компиляторов функциональных языков. Однако трассирующая нормализация оставалась слабо изученным подходом. Даниил Андреевич расширил подход трассирующей нормализации до нетипизированного лямбда-исчисления (то есть до модели вычислений, которая является полной по Тьюрингу).

Он также показал, что при этом сохраняется полукомпозициональность. Последнее свойство позволяет успешно специализировать процедуру трассирующей нормализации на входной лямбда-терм. Была построена дополнительная модель под названием полная головная линейная редукция, и с ее помощью доказана корректность процедуры трассирующей нормализации. Диссертантом было также показано, что трассирующая нормализация может успешно применяться для нормализации лямбда-термов в рамках других стратегий вычислений— аппликативного порядка редукций и вызова по необходимости ~са11 Ьу пеед).

Наконец, Даниил Андреевич предложил новый метод компиляции термов нетипизированного лямбда-исчисления в низкоуровневый нефункциональный язык, применяя идеи смешанных вычислений. Что немаловажно, диссертант выполнил экспериментальную реализацию предложенного им алгоритма трассирующей нормализации нетипизированного лямбда-исчисления ~языки Нав1се11 и й.ас1се1). Это показывает, что он помимо теоретического аппарата, владеет также программистскими навыками. Различные варианты сочетания теории и практики очень важны для работ в области информатики и, в частности, для работ по специальности 05.13.11; тем не менее, здесь часто наблюдается перекос то в одну, то в другой сторону.

Следует отметить, что диссертация Даниила Андреевича является очень добротной работой. Доказательства и формулировки тщательно выверены, хорошо определены и активно используются различные «тонкие» понятия, работа снабжена большим количеством ссылок как на классическую, так и на современную литературу. Диссертант глубоко разбирается в данном вопросе — думаю„что он стал одним из ведущих специалистов по лямбда-исчислению в России. При этом его исследование глубоко интегрировано в международный научный контекст и опирается на последние работы в данной области.

Даниил Андреевич лично общался с известными учеными и выступал на семинарах в ведущих европейских школах по данной тематике: в университете Оксфорда и в университете Копенгагена, а также посетил с докладами многочисленные семинары и конференции — в Швеции, Франции, Нидерландах. Такая встроенность в международный научный контекст, к сожалению, не часто встречается в исследованиях, представленных в кандидатских работах в России в области информатики. Вместе с тем автор активно представлял свое исследование и в Российском научном сообществе, причем именно там, где разбираются в данной тематике — в Московском государственном университете (Москва), Институте прикладной математики им. М.В.

Келдыша РАН (Москва), Институте программных систем им. А.К. Айламазяна РАН (Переславль-Залесский), на конференции "Языки программирования и компиляторы" (2017, Ростов-на-Дону). Следует отметить также хорошую работоспособность диссертанта, и даже страстность, с которой он занимается данной тематикой, считая свои исследования важным делом в своей жизни. Такая поглощенность и сосредоточенность на науке нечасто встречается в настоящее время. Хотя также необходимо отметить, что Даниилу Андреевичу еще пока не хватает опыта командной работы и коммуникативных навыков, что, как мне кажется, является важным для исследователя в области информатики.

Тем не менее Профессор кафедры системного программирования Санкт-петербургского государственного университета, Д.В.Кознов М Ю7'л~'7 доктор технических наук Даниил Андреевич быстро прогрессирует, совершив значительные шаги в формировании себя как ученого даже по сравнению еще с прошлым годом. Подводя итоги, сделаем следующий вывод. Диссертацию можно считать законченной научно-исследовательской работой, ее тематика и полученные научные результаты полностью соответствуют паспорту специальности 05.13.11 «Математическое и программное обеспечение вычислительных машин, комплексов и компьютерных сетей».

Работа соответствует требованиям Положения о порядке присуждения ученых степеней, а ее автор, Даниил Андреевич Березун, заслуживает присуждения ему ученой степени кандидата физико-математических наук по специальности 05.13.11. .