The universal resolving algorithm: inverse computation in a functional language

Abstract. 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 (URA) introduced in this paper is sound and complete, and computes each solution, if it exists, in finite time. The algorithm has been implemented for TSG, a typed dialect of S-Graph, and shows some remarkable results for the inverse computa-tion of functional programs such as pattern matching and the inverse interpretation of While-programs.