Solving Higher-Order Equations: From Logic To Programming
Christian Prehofer · 2012
Higher-order constructs provide the necessary level of abstraction for concise and natural formulations in many areas of computer science. We present constructive methods for higher-order equational reasoning with applications ranging from theorem proving to novel programming concepts. A major problem of higher-order programming is the undecidability of higher-order unification. In the first part, we develop several classes with decidable second-order unification. As the main result, we show that the unification of a linear higher-order pattern s with an arbitrary second-order term that shares no variables with s is decidable and finitely solvable. This is the unification needed for second-order functional-logic programming. The second main contribution is a framework for solving higher-order equational problems by narrowing. In the first-order case, narrowing is the underlying computation rule for the integration of logic programming and functional programming. We argue that there are...