Отзыв научного руководителя (1150911)

Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла

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

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

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

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

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

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

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

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

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

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

Характеристики

Тип файла PDF

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

Например, если Вам нужно распечатать чертёж из автокада, Вы сохраните чертёж на флешку, но будет ли автокад в пункте печати? А если будет, то нужная версия с нужными библиотеками? Именно для этого и нужен формат PDF - в нём точно будет показано верно вне зависимости от того, в какой программе создали PDF-файл и есть ли нужная программа для его просмотра.

Список файлов диссертации