Исследовательская группа

Лаборатория языковых инструментов

Структурно-рекурсивная реализация алгоритма синтаксической унификации

April 9

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

Материалы к докладу: Conor McBride. First-order unification by structural recursion. Journal of Functional Programming, 2003.

Докладчик: Дмитрий Розплохас