Towards a reversible functional language

TY - GEN

T1 - Towards a reversible functional language

AU - Yokoyama, Tetsuo

AU - Axelsen, Holger Bock

AU - Glück, Robert

N1 - Conference code: 3

PY - 2012

Y1 - 2012

N2 - We identify concepts of reversibility for a functional language by means of a set of semantic rules with specific properties. These properties include injectivity along with local backward determinism, an important operational property for an efficient reversible language. We define a concise reversible first-order functional language in which access to the backward semantics is provided to the programmer by inverse function calls. Reversibility guarantees that in this language a backward run (inverse interpretation) is as fast as the corresponding forward run itself. By adopting a symmetric first-match policy for case expressions, we can write overlapping patterns in case branches, as is customary in ordinary functional languages, and also in leaf expressions, unlike existing inverse interpreter methods, which enables concise programs. In patterns, the use of a duplication/equality operator also simplifies inverse computation and program inversion. We discuss the advantages of a reversible functional language using example programs, including run-length encoding. Program inversion is seen to be as lightweight as for imperative reversible languages and realized by recursive descent. Finally, we show that the proposed language is r-Turing complete.

AB - We identify concepts of reversibility for a functional language by means of a set of semantic rules with specific properties. These properties include injectivity along with local backward determinism, an important operational property for an efficient reversible language. We define a concise reversible first-order functional language in which access to the backward semantics is provided to the programmer by inverse function calls. Reversibility guarantees that in this language a backward run (inverse interpretation) is as fast as the corresponding forward run itself. By adopting a symmetric first-match policy for case expressions, we can write overlapping patterns in case branches, as is customary in ordinary functional languages, and also in leaf expressions, unlike existing inverse interpreter methods, which enables concise programs. In patterns, the use of a duplication/equality operator also simplifies inverse computation and program inversion. We discuss the advantages of a reversible functional language using example programs, including run-length encoding. Program inversion is seen to be as lightweight as for imperative reversible languages and realized by recursive descent. Finally, we show that the proposed language is r-Turing complete.

U2 - 10.1007/978-3-642-29517-1_2

DO - 10.1007/978-3-642-29517-1_2

M3 - Article in proceedings

SN - 978-3-642-29516-4

T3 - Lecture notes in computer science

SP - 14

EP - 29

BT - Reversible Computation

A2 - De Vos, Alexis

A2 - Wille, Robert

PB - Springer

T2 - 3rd International Workshop on Reversible Computation

Y2 - 4 July 2011 through 5 July 2011

ER -