Jeopardy: An Invertible Functional Programming Language

TL;DR

Jeopardy is a functional programming language designed to ensure program invertibility without requiring local reversibility, allowing the use of uninvertible operations under static analysis guarantees.

Contribution

It introduces Jeopardy, a language that guarantees invertibility through static analysis, enabling more flexible programming compared to reversible languages.

Findings

Provides static analysis techniques for invertibility

Allows uninvertible and nondeterministic operations safely

Guarantees invertibility without local reversibility constraints

Abstract

Algorithms are ways of mapping problems to solutions. An algorithm is invertible precisely when this mapping is injective, such that the initial problem can be uniquely inferred from its solution. While invertible algorithms can be described in general-purpose languages, no guarantees are generally made by such languages as regards invertibility, so ensuring invertibility requires additional (and often non-trivial) proof. On the other hand, while reversible programming languages guarantee that their programs are invertible by restricting the permissible operations to those which are locally invertible, writing programs in the reversible style can be cumbersome, and may differ significantly from conventional implementations even when the implemented algorithm is, in fact, invertible. In this paper we introduce Jeopardy, a functional programming language that guarantees program invertibility without imposing local reversibility. In particular, Jeopardy allows the limited use of uninvertible -- and even nondeterministic! -- operations, provided that they are used in a way that can be statically determined to be invertible. To this end, we outline an \emph{implicitly available arguments analysis} and three further approaches that can give a partial static guarantee to the (generally difficult) problem of guaranteeing invertibility.