RE: V совместное совещание ИПС РАН — МГТУ по Рефалу
Александр Коновалов a.v.konovalov87_AT_mail.ru
Добрый день всем!
В четверг, 16 июня в МГТУ имени Н. Э. Баумана пройдёт традиционное
V совместное рабочее совещание
ИПС имени А.К. Айламазяна РАН
и
МГТУ имени Н.Э. Баумана
по функциональному языку Рефал
С докладами выступят сотрудники ИПС и преподаватели и студенты МГТУ. Совещание посвящено языку программирования Рефал и метавычислениям над ним.
Мероприятие впервые пройдёт в смешанном формате! Посетить его можно будет очно, приехав в МГТУ, либо дистанционно, подключившись к вебинару.
Адрес: ул. 2-я Бауманская, дом 5 (главный корпус). Время с 11:55 до 16:05, аудитория 330аю.
Ссылка для дистанционного участия: https://webinar6.bmstu.ru/b/avk-79s-jq1-ex4. Вебинар работает прямо из браузера, дополнительное ПО ставить не нужно. Регистрироваться не нужно — переходите по ссылке, вводите ник и участвуете.
Рядом с аудиторией есть столовая и кафетерий, где можно перекусить во время перерывов.
Программа мероприятия (аннотации в конце письма):
11:55–12:00 — открытие
Первая сессия, председатель Антонина Непейвода
12:00–13:00 — Андрей Немытых «Об одном равномерном свойстве суперкомпилятора SCP4»
13:00–13:05 — перерыв
13:05–14:00 — Александр Коновалов «Чистый рекурсивный спуск на Рефале-5»
14:00–14:20 — обед
Вторая сессия, председатель Александр Коновалов
14:20–15:05 — Антонина Непейвода «Обобщение при уточнении понятия закрытой переменной»
15:05–15:10 — перерыв
15:10–15:50 — Дмитрий Сырбу «Типизация функций подмножества языка РЕФАЛ»
15:50–16:00 — обсуждение
16:00–16:05 — закрытие
Аннотации докладов
1. Андрей Немытых «Об одном равномерном свойстве суперкомпилятора SCP4»
(построение специализированных версий алгоритма Матиясевича посредством специализации наивного поиска образца в строке)
В 1988 году Futamura и Nogi опубликовали результаты нескольких экспериментов по специализации программной модели наивного поиска образца в строке по конкретным образцам. Структура остаточных программ, автоматически построенных методом обобщённых частичных вычислений (generalized partial computation), совпадала со структурой специализированных версий алгоритма Матиясевича, по недоразумению часто называемого алгоритмом Кнута-Морриса-Пратта. Таблица переходов по строке, которую строит первая стадия алгоритма Матиясевича, была автоматически вставлена в остаточные программы.
Результаты Futamur-ы и Nogi существенно опираются на использовании методом обобщённых частичных вычислений «отрицательной информации» о параметризованных конфигурациях специализируемой программной модели, которая была определена в терминах хвостовой рекурсии.
Позже подобные эксперименты повторялись многими авторами в разных контекстах для демонстрации возможностей разных модельных специализаторов.
В 1989 году R.S. Bird, J. Gibbons и G. Jones представили в терминах функционального языка высшего порядка ручной просчёт преобразования модели наивного в общем положении поиска образца в строке, где образец неизвестный — произвольный — параметризованный. Результатом их вычислений является алгоритм Матиясевича в общем положении. Метод преобразования основан на алгебраической технике и использует не автоматизированные трюки, включая отношения высшего порядка понижающие сложность вычисления в худшем случае преобразуемой программной модели.
В докладе будет рассказано о ключевых свойствах суперкомпилятора SCP4, которые позволяют ему преобразовать для любого фиксированного образца программную модель наивного поиска, определённую в терминах хвостовой рекурсии, к соответствующей, специализированной по этому образцу, версии алгоритма Матиясевича. Описанное здесь свойство суперкомпилятора SCP4 невозможно проверить посредством экспериментов, поскольку существует бесконечно много образцов. В докладе будут также сформулированы основные утверждения, из которых следует это равномерное по множеству образцов свойство суперкомпилятора SCP4.
2. Александр Коновалов «Чистый рекурсивный спуск на Рефале-5»
Рекурсивный спуск — хорошо известная методика написания парсеров вручную. Методика позволяет, имея LL(1)-грамматику в виде БНФ или РБНФ, написать регулярным образом заготовку кода синтаксического анализатора, которую затем можно наполнять семантическими действиями.
Проблема классического рекурсивного спуска в том, что он императивен. Он подразумевает наличие глобальной переменной CurrentToken, в которой хранится текущий токен, и функции с побочным эффектом NextToken, которая считывает новый токен и обновляет содержимое этой переменной.
В докладе будет рассказано, как перенести методику рекурсивного спуска на Рефал-5 без побочных эффектов (т.е. без изменяемых ящиков и без копилки). Т.е. каким образом, можно, имея грамматику в БНФ, регулярным образом написать заготовку парсера, которую затем можно будет наполнять семантическими действиями.
Прямое следование этой методике приводит к написанию неэффективного кода, который просится быть оптимизированным во время компиляции. Будет показано, что этот код можно будет оптимизировать при помощи суперкомпиляции.
3. Антонина Непейвода «Обобщение при уточнении понятия закрытой переменной»
Не все синтаксически открытые переменные в образцах действительно требуют неоднозначных подстановок. Наличие структурных скобок или отрицательных рестрикций в некоторых случаях позволяет рассматривать n-ку образцов вместо единственного образца, в связи с чем иногда значения всех переменных, входящих в такие n-ки, определяется однозначно.
Мы рассмотрим простое расширение понятия закрытой переменной, которое позволяет строить более точные обобщения конфигураций, содержащие несколько подряд идущих е-параметров, и приведём набросок доказательства нётеровости обобщаемых образцов относительно (нестрогого) включения их языков при условии, что все переменные в данных образцах являются обобщённо закрытыми.
4. Дмитрий Сырбу «Типизация функций для подмножества языка РЕФАЛ»
Введение в язык механизма типизации позволит проверять корректность, написанных программистом функций до этапа компиляции программы.
Верификация типов будет заключаться в сопоставлении фактических типов аргументов и возвращаемых значений с формальными, описанными в нотации типов. Нотация типов представляет регулярную грамматику, что позволяет выражать типы как регулярные выражения, а значит использовать для сопоставления эквивалентные конечные автоматы.
Данный доклад посвящён разработке представления типов функций языка РЕФАЛ и процедуры автоматической верификации типов.
До встречи!
Александр Коновалов