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

<ol>
<li><p>Torben Mogensen has worked on this problem. Here are two papers of his. </p>

<p>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.</p>

<ul>
<li><a href="https://link.springer.com/chapter/10.1007/11561347_14" rel="noreferrer"><em>Semi-inversion of Guarded Equations</em></a></li>
<li><a href="https://dl.acm.org/citation.cfm?id=1328413" rel="noreferrer"><em>Semi-Inversion of Functional Parameters</em></a></li>
</ul></li>
<li><p>Tetsuo Yokoyama, Holger Bock Axelsen, and Robert Glück. </p>

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

<ul>
<li><a href="https://link.springer.com/chapter/10.1007/978-3-642-29517-1_2" rel="noreferrer"><em>Towards a Reversible Functional Language.</em></a></li>
</ul></li>
<li><p>Stefan Bohne and Baltasar Trancón Widemann.</p>

<p>This is a really neat paper! It observes that (a) you can construct a category where the morphisms are functions <em>paired with</em> 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. </p>

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

<ul>
<li><a href="http://www.complang.tuwien.ac.at/kps2015/proceedings/KPS_2015_submission_15.pdf" rel="noreferrer"><em>An Approach for Generalized Reversible Functional Programming</em></a></li>
</ul></li>
<li><p>Francesco Tiezzia, Nobuko Yoshida </p>

<p>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!</p>

<ul>
<li><a href="http://www.sciencedirect.com/science/article/pii/S2352220815000346" rel="noreferrer"><em>Reversible session-based pi-calculus</em></a></li>
</ul></li>
</ol>

CC BY-SA 3.0
2017-11-13T21:51:12.817Z
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.
Martin Berger
CC BY-SA 3.0
2017-11-17T10:25:43.083Z
@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?
Neel Krishnaswami
CC BY-SA 3.0
2017-11-17T12:30:25.647Z
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?
Martin Berger
CC BY-SA 3.0
2017-11-13T15:44:10.197Z
2017-11-13T15:44:10.197Z
Neel Krishnaswami
<p>The term <strong>program inversion</strong>
has multiple shades of  meaning, but probably got started with
J. McCarthy's 1956 work <em><a href="http://jmc.stanford.edu/articles/inversion.html" rel="noreferrer">The Inversion of Functions Defined by Turing Machines</a></em> 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.</p>

<p>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$?</p>

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

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

<reference-request><lambda-calculus><typed-lambda-calculus><reversible-computing>
Program inversion algorithms for higher-order programs
Martin Berger
# Program inversion algorithms for higher-order programs

(Asked by: username_0 on 2017-11-10)

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](http://jmc.stanford.edu/articles/inversion.html)* 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)?

**Tags:** reference-request, lambda-calculus, typed-lambda-calculus, reversible-computing

---

## 1 answers

### Answer by username_1 on 2017-11-13. Score: 5

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*](https://link.springer.com/chapter/10.1007/11561347_14)
   * [*Semi-Inversion of Functional Parameters*](https://dl.acm.org/citation.cfm?id=1328413)
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.*](https://link.springer.com/chapter/10.1007/978-3-642-29517-1_2)
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*](http://www.complang.tuwien.ac.at/kps2015/proceedings/KPS_2015_submission_15.pdf)
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*](http://www.sciencedirect.com/science/article/pii/S2352220815000346)

> **Comments:**
> **username_0**: 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.  
> **username_1**: @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?  
> **username_0**: 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?  

---

