In functional languages, functions are usually constructed by structural recursion where the result is composed of the results of the same function on smaller parts of the input. This method makes the structure of the function clear, and also substantiate that the recursion is finite. Unfortunately, natural solutions to some problems can't be implemented with structural recursion. These problems include syntactic unification, which occurs, for example, in logic programming and type analysis. Most unification algorithms use non-structural recursion, so they require a separate careful proof of termination. We will study the approach to the implementation of unification algorithm as а structurally recursive program that uses the expressiveness of languages with dependent types.
Supplementary materials: Conor McBride. First-order unification by structural recursion. Journal of Functional Programming, 2003.
Presenter: Dmitri Rozplokhas
Date: April 9, 2018
Venue: room 3248, Faculty of Mathematics and Mechanics, Saint Petersburg State University, Stary Peterhof, Universitetski pr., 28