The universal resolving algorithm and its correctness: inverse computation in a functional language

We present an algorithm for inverse computation in a first-order functional language based on the notion of a perfect process tree. The Universal Resolving Algorithm introduced in this paper is sound and complete, and computes each solution for which the given program terminates, in finite time. The algorithm has been implemented for TSG, a typed dialect of S-Graph, and shows some remarkable results for the inverse computation of functional programs such as a pattern matcher and an interpreter for imperative programs.