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

минобрндуки россии федеральное тосударстаенное аатономное Обрааоаательное унренсденйе аь|ссаесо Обрааоааййа кСанкт-Петербурсскйй нацйонааьный йссаедоаатеаьскйй уййаерсйтет йнфоратацйойных технолотйя, ккеканйкн н оотйкйа 1Унйаерсйтет МТМО1 Крснаеркскка арссаект, д, 49, с Скккс-Оетербусс Рссскаскак Федераьнк, 137101 таас (312) 232-97.04 ~ факс: ~81»,' 232-23-От оасйскаа КО~сна,: 'йнмя.сока на автореферат диссертации Березуна Даниила Андреевича «Трассирую1цая нормализацияа, ~редс~авлен~ой на соискание ученой степени кандидата физико-математических наук по специальности 05.13.11 — абяатематическое и программное обеспечение всачислмтельных машин, комплексов и компьютерных сетей ь Теория лямбда-исчисления является известной областью исследований и ведет начало от классических работ Алана Черча по теории вычислимости.

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

Блюмом. Эта стратегия позволяет оставлять после нормализации исходный терм без изменений, и зто оказывается важным при ее применении для создания средств обработки программ на функциональных языках. Не вдаваясь в детали, можно отметить, что последнее оказывается возможным путем применения теории частичных вычислений, в частности, известных проекций Футамуры — Ершова — Турчина.

Автор диссертационного исследования, Березун Д.А,, обобщил трассирующую нормализацию на случай нетипизированного лямбда-исчисления, которое, как известно, полно по Тьюрингу. Автор также показал, как разработанный им алгоритм трассирующей нормализации может быть использован для генерации компиляторов методом специализации предложенного алгоритма. Наконец, он выполнил программную реализацию своих теоретических результатов, которая находится в свободном доступе в Интернете. Таким образом, можно заключить, что данное диссертационное исследование выполнено на высоком научном уровне, полученные автором результаты обладают научной новизной и практической ценностью.

Диссертационная работа «Трассирующая Доцент кафедры компьютерных технологий, Университет ИТМО кандидат физико-математических наук Андрей Александрович Фильченков 26 марта 2018 г. Университет ИТМО, 197101, г, Санкт-Петербург, Кронверкский проспект, д.49, ай!спегйоч6)согр.Фгпо.ги тел.

+7 (950) 021-03-28 нормализация» удовлетворяет всем требованиям, изложенным в Постановлении правительства РФ от 24 сентября 2013 г. М 842 «О порядке присуждения ученых степеней» в редакции от 28 августа 2017 г., которым должны соответствовать диссертации на соискание ученой степени кандидата наук, а соискатель Березун Д.А., заслуживает присуждения ему ученой степени кандидата физико-математических наук по специальности 05,13,11 «Математическое и программное обеспечение вычислительных машин, комплексов и компьютерных сетей».

.