Branching execution symmetry in Jeopardy by available implicit arguments analysis

When the inverse of an algorithm is well-defined – that is, when its output can be deterministically transformed into the input pro- ducing it – we say that the algorithm is invertible. While one can describe an invertible algorithm using a general-purpose programming language, it is generally not possible to guarantee that its inverse is well-defined without additional argument. Reversible languages enforce determinis- tic inverse interpretation at the cost of expressibility, by restricting the building blocks from which an algorithm may be constructed. Jeopardy is a functional programming language designed for writing in- vertible algorithms without the syntactic restrictions of reversible pro- gramming. In particular, Jeopardy allows the limited use of locally non- invertible operations, provided that they are used in a way that can be statically determined to be globally invertible. However, guaranteeing invertibility in Jeopardy is not obvious. One of the central problems in guaranteeing invertibility is that of de- ciding whether a program is symmetric in the face of branching control flow. In this paper, we show how Jeopardy can solve this problem, us- ing a program analysis called available implicit arguments analysis, to approximate branching symmetries.