Branching execution symmetry in Jeopardy by available implicit arguments analysis

TL;DR

This paper introduces a program analysis technique for the Jeopardy language that approximates branching symmetries to ensure invertibility of algorithms with branching control flow.

Contribution

It presents available implicit arguments analysis as a method to verify invertibility in Jeopardy, enabling more flexible invertible programming without strict syntactic restrictions.

Findings

Successfully approximates branching symmetries in Jeopardy programs

Enables verification of invertibility in algorithms with branching control flow

Improves the expressibility of invertible algorithms in a functional language

Abstract

When the inverse of an algorithm is well-defined -- that is, when its output can be deterministically transformed into the input producing 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 deterministic 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 invertible algorithms \emph{without} the syntactic restrictions of reversible programming. 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 deciding whether a program is symmetric in the face of branching control flow. In this paper, we show how Jeopardy can solve this problem, using a program analysis called available implicit arguments analysis, to approximate branching symmetries.