Program inversion algorithms for higher-order programs

Question

The term program inversion has multiple shades of meaning, but probably got started with J. McCarthy's 1956 work The Inversion of Functions Defined by Turing Machines in the context of AI. By now many connections between program inversion and other fields have been discovered, e.g. reversible programming (physical and logical), partial evaluation, verification, bidirectional programming, logic programming, and machine learning.

What is program inversion? In first approximation it's something like this: Given a program $P : A \rightarrow B$ taking arguments of type $A$ and returning results of type $B$, produce a program $P^{-1}$ that is "somehow" the inverse of $P$. I'm deliberately being vague here, since the concept can be (and is) clarified in various ways: e.g. is $P$ required to be injective? Should $P^{-1}(b)$ return all or just some $a$ such that $P(a) = b$?

There are generic ways of inverting a program, e.g. using diagonalisation as already pointed out by McCarthy, or using partial evaluation, but they tend not to be efficient. Also most work on program inversion I'm familiar with does not seem to deal with full higher-order programming languages (i.e. $\lambda$-calculi).

Reference request. What is the state-of-the-art in explicit algorithms for program inversion of $\lambda$-calculi (with no restriction on higher-orderness)?

Answer 1

There hasn't been a huge amount of work in this space, but what work there is, is pretty interesting.

1. Torben Mogensen has worked on this problem. Here are two papers of his.

   The first paper gives an algorithm for first-order functional programs, and the second extends it to higher-order. The precise characterization of when this algorithm will succeed is left to future work.

   • Semi-inversion of Guarded Equations
   • Semi-Inversion of Functional Parameters

2. Tetsuo Yokoyama, Holger Bock Axelsen, and Robert Glück.

   This describes the RFun programming language, which inverts first-order functional programs, but enforces injectivity and backwards determinism constraints which ensure that backwards evaluation is as fast as forwards. (They have written a number of other papers on this subject, which I have had trouble getting hold of.)

   • Towards a Reversible Functional Language.

3. Stefan Bohne and Baltasar Trancón Widemann.

   This is a really neat paper! It observes that (a) you can construct a category where the morphisms are functions paired with their inverse (for whatever particular notion of inverse you are using), and (b) this category has dagger compact structure. This means you can write a program with a slightly funky linear type discipline, and then read off the forwards and backwards interpretations from the semantics.

   They give a functional language with a fairly wild syntax: nigh-arbitrary expressions can be used as patterns, and reversibility makes it sensible.

   • An Approach for Generalized Reversible Functional Programming

4. Francesco Tiezzia, Nobuko Yoshida

   I haven't read this one, but only just discovered it when Googling for the other papers. Given the authors and the subject, I suspect this is right up your alley!

   • Reversible session-based pi-calculus