Отзыв на автореферат (Трассирующая нормализация)
Описание файла
Файл "Отзыв на автореферат" внутри архива находится в папке "Трассирующая нормализация". PDF-файл из архива "Трассирующая нормализация", который расположен в категории "". Всё это находится в предмете "физико-математические науки" из Аспирантура и докторантура, которые можно найти в файловом архиве СПбГУ. Не смотря на прямую связь этого архива с СПбГУ, его также можно найти и в других разделах. , а ещё этот архив представляет собой кандидатскую диссертацию, поэтому ещё представлен в разделе всех диссертаций на соискание учёной степени кандидата физико-математических наук.
Просмотр PDF-файла онлайн
Текст из PDF
Федеральное государственное автономное образовательное учреждение высшего образования «ЮЖНЫИ ФЕДЕРАЛЬНЫЙ УНИВЕРСИТЕТ» ИНСТИТУТ МАТЕМАТИКИ. МЕХАНИКИ И КОМПЬЮТЕРНЫХ НАУК ИМ. И.И.ВОРОВИЧА Ьп гкдпппсв.егепп.га' ло Г ОТЗЫВ на автореферат диссертации БЕРЕЗУНА Даниила Андреевича "ТРАССИРУЮЩАЯ НОРМАЛИЗАЦИЯ", представленной на соискание ученой степени кандидата физико-математических наук по специальности 05.13.11 - "Математическое и программное обеспечение вычислительных машин, комплексов и компьютерных сетей".
Заведующий кафедрой Алгебры и дискретной математики Института математики, механики и компьютерный наук им. И.И. Воровича Южноы1'.;, федерального университета, доктор техническ)ех,:,.на (05.13.11), старший научный сотрудник (05.,:'.Й"И)1 ' Ростов-н/Д, ул. Мильчакова 8а, ИММиКН ЮФУ нберг Борис Яковлевич Подпись Б.Я. Штейнберга удостоверяю Диссертация Березуна Д.А. оТносится к актуальному направлению теоретической информатики — лямбда-исчислению. В работе исследован новый подход к нормализации термов нетипизированного лямбда-исчисления под названием трассируюи1ая нормализация. Автор на примере нетипизированного лямбда-исчисления представил ответ на открытый до этого вопрос об обобщении трассирующей нормализации до алгоритмически полного варианта лямбда-исчисления. Для доказательства корректности предложенного алгоритма автор разработал модель полной головной линейной редукции, обобщая известныс модели головной линейной редукции, предложенной У.Валов и 1..Ке8шег, и установил соответствие между предложенным алгоритмом трассирующей нормализации и разработанной моделью.
Автор также показал, как разработанный им алгоритм трассирующей нормализации может быть использован для генерации компиляторов методом специализации предложенного алгоритма. Этот алгоритм обладает важным для генерации компиляторов свойством: в процессе нормализации исходный терм остается неизменным. Считаю, что диссертационное исследование Березуна Д.А. выполнено на высоком научном уровне, полученные автором результаты обладают научной новизной и практической ценностью, полностью опубликованы, а сам автор, Березун Д.А., заслуживает присуждения ему ученой степени кандидата физико-математических наук по специальности 05.13.11 — "Математическое и программное обеспечение вычислительных машин, комплексов и компьютерных сетей". 21.03.18 .