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.
翻译:当反算法被明确界定时,也就是当其输出可以决定性地转化成生成它的输入时,我们说算法是不可逆的。虽然可以描述使用通用编程语言的不可逆算法,但一般不可能保证其反算法是完全定义的,而没有额外的论点。反省语言以表达为代价,以限制可构建算法的构件为代价,强制进行确定偏反解释。Jeopardy是一种功能性编程语言,设计该语言是为了写不可逆算法/emph{不考虑可逆编程的合成限制。特别是,Jeopardy允许有限地使用本地不可逆的操作,只要它们的使用方式是静态地确定为全球不可逆的。然而,在Jeopardy中保证不可逆解释性并不是显而易见的。保证不可逆性的中心问题之一是决定一个程序在分支控制流中是否具有对称性。在这个文件中,我们展示了Jeopardy可隐含的分支如何用程序分析来解决这个问题。