Unification of program expressions with recursive bindings
Manfred Schmidt-Schauß, David Sabel · 2016
This paper presents an algorithm for unification of meta-expressions of higher-order lambda calculi with recursive bindings. The meta-language uses higher-order abstract syntax. Besides usual unification variables for expressions and term variables, there are context-variables for generalized shapes of contexts, environment variables for sets of bindings, and (flexible) chain-variables as they, for instance, occur in formal descriptions of the operational semantics of lazy functional programming languages with shared environments. To exclude solutions with unintended scoping, the algorithm takes advantage of so-called non-capture constraints. The expressiveness of the meta-language comprises reduction contexts to support reasoning on program evaluation under reduction strategies. The non-deterministic unification algorithm runs in polynomial time provided certain restrictions on the number of occurrences of unification variables hold. The deterministic version of the algorithm will output a finite and concise set of representatives of all solutions. Results on an implementation of the algorithm are presented. The experiments focus on computing critical pairs of equations from program calculi modeling lazy functional languages which support the reasoning on the correctness of program transformations.