FAQ

What is a reversible semantics for Erlang?

A regular semantics declares what you have to do when you want to evaluate a particular statement.
In a reversible semantics, you declare how to "unevaluate" statements in addition (i.e., the program can run forward or backward).

For instance, if you find a let X = Y in Z expression, the associated rule of the semantics would say something like:

1. Evaluate Y with your environment.
2. Evaluate Z with your environment updated with [X -> Y].

However, in a reversible semantics, we also declare how the program can run in the backward direction. For instance, in the previous example, we can "unevaluate" the resulting expression by going back to the let X = Y in Z expression.

So basically, you have written an interpreter for Erlang, right?

Yes, but this interpreter can evaluate programs both directions (forward and backward).

What is this weird code that you show in the Code tab?

The reversible semantics are defined for a subset of the Core Erlang language. Core Erlang is a much simpler language than Erlang, and it is used as an intermediate language when compiling Erlang code. Here you can find a brief introduction to Core Erlang. Hence, this interpreter is actually a Core Erlang interpreter.

Then, why am I able to provide Erlang terms as input arguments?

We convert Erlang terms to Core Erlang terms before starting the evaluation.

I do not know how to interpret the states shown in the State tab

We recommend you to read the LOPSTR paper before trying to do that. The implemented semantics is an improved version of the semantics in that paper (submitted for publication).