A program inverter for a functional language with equality and constructors

Abstract. We present a method for automatic program inversion in a first-order functional programming language. We formalize the transfor-mation and illustrate it with several examples including the automatic derivation of a program for run-length decoding from a program for run-length encoding. This derivation is not possible with other automatic program inversion methods. One of our key observations is that the du-plication of values and testing of their equality are two sides of the same coin in program inversion. This leads us to the design of a new self-inverse primitive function that considerably simplifies the automatic inversion of programs.