An algorithm describes a sequence of steps that transform a problem into its solution. Furthermore, when the inverted sequence is well-defined, we say that the algorithm is invertible. 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. However, guaranteeing invertibility is not obvious. Thus, we furthermore outline three approaches that can give a partial static guarantee.

本文介绍了一种名为Jeopardy的函数式编程语言，它可以在不实施局部可逆的限制下保证程序可逆性，并且通过一系列方法来解决保证可逆性的通常困难问题，其中一个方法是隐含可用参数分析。

Jeopardy: 可逆的函数式编程语言