TY - GEN

T1 - Branching execution symmetry in Jeopardy by available implicit arguments analysis

AU - Tilsted Kristensen, Joachim

AU - Kaarsgaard, Robin

AU - Thomsen, Michael Kirkedal

N1 - Conference code: 35

PY - 2023

Y1 - 2023

N2 - 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.

AB - 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.

M3 - Conference article

VL - 2022

SP - 1

EP - 14

JO - NIKT: Norsk IKT-konferanse for forskning og utdanning

JF - NIKT: Norsk IKT-konferanse for forskning og utdanning

SN - 1892-0713

IS - 1

T2 - Norwegian ICT Conference for Research and Education

Y2 - 27 November 2022 through 30 November 2022

ER -