Evaluating Recursive Sets
Many computations (e.g., program analyses) are best expressed as recursively defined sets. For example, the set of paths in a graph can be defined recursively as follows:
- If there is an edge from A to B, then there is a path from A to B.
- If there is an edge from A to B and a path from B to C, then there is a path from A to C.
This set can be computed by applying these two rules iteratively. At each step of the iteration, knowing how the state changed in the last iteration can help speed up the program compared to a naïve approach. This is essentially a form of incrementalization. For example, for efficiently computing paths in a graph, you need to know which paths were found in the last iteration.
Recursive set computations are often expressed in a logic programming language like Datalog. In this seminar topic, you will look at Datafun, a functional language inspired by Datalog. Datafun makes use of seminaïve evaluation, which is an incremental approach for computing recursive sets.
You will look at:
- What makes Datafun different from other functional languages,
- How seminaïve evaluation provides a speed-up,
- How Datafun's approach compares to Datalog, and
- What the limits and drawbacks are.
You will also write a small program that either
- Uses Datafun or Datalog (see Soufflé and Ascent) to implement a use case like graphs or program analysis, or
- Implements the core of seminaïve evaluation.