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

отзыв на автореферат диссертации БЕРЕЗУНА Даниила Андреевича "ТРАССИРУЮЩАЯ НОРМАЛИЗАЦИЯ", представленной на соискание ученой степени кандидата физико-математических наук по специальности 05.13.11 - "Математическое и программное обеспечение вычислительных машин, комплексов и компьютерных сетей". Актуальность работы В своей работе автор дает конкретный ответ на долгое время остававшийся открытым вопрос о возможности применения трассирующей нормализации для алгоритмически полных языков (таких как нетипизированное лямбда исчисление). Большое количество работ, посвященное различным аспектам трассирующей нормализации для алгоритмически неполных языков, также подчеркивает актуальность данной работы.

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

Наличие работающих реализаций на языках Назке!! и Яасхе1 выгодно смотрится на фоне многих работ, где авторы не затрудняют себя реализациями описываемых алгоритмов и моделей. Замечания В работе приведен метод компиляции термов нетипизированного лямбда-исчисления в низкоуровневое представление (Ш.), что позволяет получить интерпретатор лямбдаисчисления, сильно отличающихся от классических интерпретаторов (без манипуляций с окружением, без передачи аргументов). Было бы интересно рассмотреть плюсы и минусы такого низкоуровневого представления с практической точки зрения.

Заключение Результаты диссертационной работы Д.А. Березуна могут использоваться в системах преобразования программ, доказательства теорем, компьютерной алгебре, где проводятся манипуляции с лямбда-термами. Считаю, что работа выполнена на высоком научном уровне, получены результаты, обладающие новизной, а Березун Д.А. заслуживает присуждения ему ученой степени кандидата физико-математических наук по специальности 05.13.11 — "Математическое и программное обеспечение вычислительных машин, комплексов и компьютерных сетей". К.ф.-м.н., разработчик ПО, РасеЬооМ ЦК, ! опооп 09.03.2013 И.Г.

Ключников .