JetBrains Research — наука, меняющая мир

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

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

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

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

09.04.2018, 17:15.

Место: ауд. 3248, мат-мех. факультет СПбГУ, Старый Петергоф, Университетский пр-т, д. 28