10
$\begingroup$

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)?

$\endgroup$
5
+125
$\begingroup$

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.

  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.)

  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.

  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!

$\endgroup$
  • $\begingroup$ Thanks. (2, 3, 4) do not do program inversion, but design programming languages where programs are reversible/invertible by definition. This is a closely related, but different problem. In fact I'm not totally clear about how these problems relate. I had not seen semi-inversion before maybe it already solves the problem since inversion seems to be an edge case of semi-inversion? BTW Mogensen's second paper only goes up to 2nd-order. $\endgroup$ – Martin Berger Nov 13 '17 at 21:51
  • $\begingroup$ @MartinBerger: I guess the relationship depends on what you want to use program inversion for! I got interested in the problem because I was looking at type inference (if you have type-level functions, it is useful to be able to invert those functions to figure out quantifier instantiations), and so restricting the language wasn't a showstopper for me. What are you trying to do? $\endgroup$ – Neel Krishnaswami Nov 17 '17 at 10:25
  • $\begingroup$ Right now I'm interested in the general, abstract problem. My interest in program inversion comes from program verification. And I could not find anywhere that simply takes a lambda term (from PCF say or STLC) and inverts it. Is it because I'm not looking in the right place? $\endgroup$ – Martin Berger Nov 17 '17 at 12:30

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.