Вопрос о связи суперкомпиляции и well-structured transition systems

4 views

Skip to first unread message

Shilov Nikolay

unread,

Mar 25, 2023, 2:07:00 AM3/25/23

to metacompu...@googlegroups.com

Мне недавно попалась свежая статья Branch-Well-Structured Transition Systems and Extensions (Benedikt Bollig, Alain Finkel, Amrita Suresh, [2211.15913v1] Branch-Well-Structured Transition Systems and Extensions (arxiv.org)), в которой, по-моему, описан вариант well-structured transitionsystem наиболее близкий к суперкомпиляции (так как все «происходит» вдоль одного пути в дереве вычислений, на котором встречается обобщение пройденной конфигурации).

Поэтому у меня возник вопрос: где-либо кто-либо явно писал связь между WSTS и суперкомпиляции?

Н.В. Шилов

Antonina Nepejvoda

unread,

Mar 25, 2023, 8:32:36 AM3/25/23

to Метавычисления и специализация программ

Здравствуйте!

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

Ещё в этой статье мне очень понравилось понятие branch-wqo (у нас тоже есть свой branch-wqo для обрыва ветвей - отношение Турчина). Большое спасибо, обязательно приму к сведению!