Отзыв ведущей организации (1150905), страница 2

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

Текст из файла (страница 2)

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

Основные результаты диссертации опубликованы в 5 научных работах, зарегистрированных в РИНЦ. При этом, две единоличные статьи изданы в журналах из "Перечня российских рецензируемых научных журналов, в которых должны быть опубликованы основные научные результаты диссертаций на соискание ученых степеней доктора и кандидата наук". Две статьи опубликованы в изданиях, входящих в базы цитирования 8сорцв и %еЬ оГЯс1епсе. Практическая ценность и рекомендации по использованию результатов диссертационной работы Результаты работы рекомендуются к использованию в Институте программных систем им.

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

На самом же деле, конечно, имеются в виду «вычисления, применяющие нормальный порядок редукции». 2. На стр. 21 пэворится, что «стратегия вычисления по имени сначала вычисляет функцию до значения. лямбда-абстракции, после чего...». Однако, в лямбдаисчислении вычисления происходят не над «функциями»„ а над лямбда-термами. Поэтому, очевидно, имелось в виду, что нужно выполнить вычисления не над «функцией», а над термом (который, в случае типизированного лямбда-исчислення должен иметь функциональный тип). И, если в результате вычисления получится лямбда-абстракция, ее уже можно будет применить к другому терму.

3. На стр. 27, в одном н том же абзаце, термы называются то «спинальными», то <сспинными». Не следует употреблять две формы одного и того же термина для обозначения одного и того же понятия. 4. На стр. 76, в заголовке раздела 5.3, используется словосочетание «компиляция нетипизированного лямбда-исчисления». На самом деле. конечно, компиляции подвергается не само исчисление, а лямбда-термы этого исчисления. Правильная формулировка звучала бы как «компиляция термов нетнпизированного лямбда- исчисления». 5. На стр.

55 описывается процесс построения нормализованного терма на основе анализа трассы обхода исходного терма, который включает в себя процедуру «очистки» трассы от «лишних» токенов. При этом, процесс «очистки» объясняется на примерах и пояснениях к этим примерам. Однако, в интересах полноты и единообразности стиля изложения, было бы лучше привести формальное описание алгоритма «очистки», позаимствовав его (с точностью до обозначений) из экспериментальной реализации нормализации (на которую есть ссылка в диссертации). Заключение Отмеченные недостатки не оказывают существенного влияния на общий уровень и основные результаты диссертации.

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

Автореферат достаточно полно отражает содержание работы. Таким образом, диссертационная работа соответствует паспорту специальности 05.13.П. удовлетворяет требованиям п.9 Положения о присуждении ученых степеней, утвержденного постановлением Правительства РФ от 24.09.2013 № 842 (ред. от 30.07.2014, от 21.04.20!б), а сам автор заслуживает присуждения ученой степени кандидата физико-математических наук по специальности 05.!З.П вЂ” «Математическое и программное обеспечение вычислительных машин, комплексов и компьютерных сетей». Работа была заслушана и одобрена, отзыв бьи рассмотрен и угвержден на семинаре Отдела инструментального и прикладного программного обеспечения ИПМ им.

М.В. Келдыша РАН, протокол № 7 от 2б.12.20! 7 г. Отзыв подготовил кандидат физико-математических наук (специальности 01.01.10 — математическое обеспечение вычислительных машин и систем), ведущий научный сотрудник Федерального государственного учреждения «Федеральный исследовательский центр Институт прикладной математики им. М.В. Келдыша Российской академии наук». 125047, г.

Москва„Миусская пл., д.4 Сайт: Ы:,"Ачиж.кеЫ зй.ги Тел.: +7 499 250-78-73 Эл. почта: гогпапза а)Ыс! зп.гц 7 7/' Сергей Анатольевич Романенко .

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

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