Solving equations in an equational language

Abstract

The problem of solving equations is a key and challenging problem in many formalisms of integrating logic and functional programming, while narrowing is now a widely used mechanism for generating solutions. In this paper, we continue to investigate the problem of solving equations in O'Donnell's equational language. We define a restricted equality theory which we argue adequately captures the notion of first-order functional programming and permits an efficient implementation. In particular, we show that there exists a special class of narrowing derivations which generates complete and minimal sets of solutions.