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

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

А упрощение делается для того, чтобы можно было сосредоточиться на изучении самых сложных и глубоких проблем, касающихся синтаксиса и семантики языков программирования, не отвлекаясь и не тратя силы на второстепенные детали. В частности, лямбда-исчисление позволяет порождать в процессе вычислений новые функции, передавать функции в качестве параметров, и выдавать функции в качестве РвЬ~ Ф~„и,а. т,, ФР~Ш Ф1 ц Л у г, щддщ Вд щ всех практических языках программирования из-за сложностей, возникающих прн реализации возможностей такого рода. При этом, важно отметить, что бестиповое лямбда-исчисление обладает алго итмической полнотой гю Тью инг „и это означает, что на языке лямбда-исчисления (несмотря на его кажущуюся простоту) может быть записан любой алгоритм.

Таким образом, результаты, полученные в диссергации, могут найти применение при юа р р ру р пл рб программирования. Одной из ярких особенностей лямбда-исчисления является то, что операционная семантика лямбда-термов определяется в терминах «нормализации», которая заключается в приведении заданного лямбда-терма к нормальной форме в результате выполнения над ннм некоторой последовательности преобразований. В терминах, привычных для программистов, это означает, что в процессе исполнения программы, программа изменяет саму себя! С другой стороны, в большинстве других алгоритмических языков изменение программы в процессе ее исполнения не допускается. Это верно как в отношении «теоретических» языков (таких как алгоритмы Маркова или машина Тьюринга), так и практических (таких, как Фортран).

Это связано с тем, что неизменяемость программы значительно облегчает создание интерпретаторов, компиляторов, оптимизаторов и верификаторов для языков, обладающих таким свойством. Образно говоря, работа с неизменяемой программой - это «стрельба по неподвижной мишени», в то время как работа с изменяющейся программой - это «стрельба по движущейся мишени». Однако, возникает вопрос: а нельзя ли реорганизовать процесс нормализации лямбда-термов таким образом, чтобы исходный терм в процессе нормализации оставался неизменным? И именно эта проблема и рассматривается в диссертации применительно к языку нетипизированного лямбда-исчисления! И очевидно, что положительное решение этой проблемы может привести к устранению многих затруднений, возникающих в процессе создания реализаций для языков программирования, в которых допускается изменение программы во время ее исполнения.

Поэтому актуальность и практическая значимость диссертационной работы Березуна Д.А. не вызывает сомнений. Основные научные результаты Диссертация Березуна Д.А. состоит из введения, шести глав, заключения, списка литературы и двух приложений. Во введении обосновывается актуальность темы, определяются цели и задачи работы. В первой главе проведен анализ предшествующих работ в области нормализации 'р ю дд- м» . о д дд дд дддддд»ддд д~ддвдддддд, р р б р й р» д д: (1) обход исходного терма, результатом которого является построение трассы обхода и (2) построение нормальной формы исходного терма на основе анализа трассы.

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

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

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

Предложенный алгоритм не использует информацию о типах и, таким образом, в отличие от ранее известных алгоритмов, применим к термам нетипизнрованного лямбдаисчисления. Разумеется, при этом он остается применим и к термам простого типизированного лямбда-исчисления, поскольку при таком применение достаточно просто игнорировать информацию о типах. Хочется особо отметить мастерство, проявленное автором при изложении этого необычного и сложного для восприятия материала. Ведь он мог бы предъявить новый алгоритм чисто формально, как нечто «свалившееся с неба». Однако, тогда было бы непонятно, откуда взялся этот алгоритм, и как его нужно расширять в случае добавления к чистому лямбда-исчислению каких-то дополнительных конструкций. Но автор избрал другой стиль изложения: он показывает, как этот алгоритм может быть получен из традиционного алгоритма нормализации, основанного на подстановках путем нескольких преобразований этого алгоритма.

Конечным результатом является программа первого порядка с хвостовой рекурсией, которую, при желании, не составляет труда переписать на императивном языке программирования в виде программы с циклами. А это - существенно для некоторых возможных применений алгоритма. В четвертой главе доказывается корректность предложенного автором алгоритма трассирующей нормализации и устанавливается его связь с полной головной линейной редукцией (предложенной автором во второй главе). В пятой главе рассматривается одно из возможных применений предложенного автором алгоритма трассирующей нормализации. А именно, компиляция термов нетнпизированного лямбда исчисления посредством специализации алгоритма нормализации по отношению к терму; Как известно, если имеется интерпретатор какого-то языка, то можно проспециализировать его по отношению к входной программе, получив скомпилированную программу.

А проспециализировав сам специализатор по отношению к интерпретатору, можно сгенерировать и компилятор с того языка, программы на котором обрабатывает интерпретатор. Преобразования такого рода известны как «проекции Футамуры». Если специализатор программ основан на методе частичных вычислений, то специализация интерпретаторов приводит к нетривиальным результатам только в том случае, если интерпретатор удовлетворяет некоторым требованиям.

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

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

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