FAQ

What is causal consistency?

Causal consistency implies that, when evaluating a program backward, an action can only be undone provided that its consequences (if any) have been undone beforehand.

For example, say that you want to undo the spawning of a process p, and p has sent a message m to some other process. Here, all the actions that p has done (sequential actions within the p, and also the sending of m) are a consequence of spawning p. Thus, you must undo all these actions before undoing the spawning p in order to keep causal consistency. Otherwise, you can end up in a system state that was not reachable from the initial state.

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.

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.