Post 1: Datalog, Chain-Forward Computation, and Relational Algebra
Our setting is logic programming, a field which attempts to design programming languages whose semantics have a close relationship to formal logic. The reason we might want to do this is that it suits our application domain more precisely than an implementation in a traditional programming language. Thus, using a logic programming language allows us to write more obviously-correct code, and perhaps even code that can be extracted cleanly from a certified implementation. Alternatively, if we did it ourselves, we’d have to do what our compiler (interpreter, …) would do anyway, so there’s no sense in doing it manually. Unfortunately, when we see a powerful tool, we are tempted to use it for everything: if our application is not ultimately-suited to the operationalization strategy of the logic programming engine we’re using, we simply obfuscate the issue in a veneer of formalism and end up with leaky abstractions. This is, I speculate, why logic programming languages have never caught on broadly for general-purpose programming. In this blog, I will detail the various trade-offs and implementation paradigms for modern logic programming engines, starting from Datalog and with a focus on program analysis.
The history of logic programming is rich, and I will not attempt to recount it all. Here I will focus on more restricted, application-specific languages, especially Datalog and its derivatives. The specific features of these languages, and the particulars of their implementation, often dovetail with a “right place, right time” effect. For example, Datalog backed by BDDs was a significant step forward in terms of production program analyses. More modern implementations eschew BDDs for more explicit representations, but it remains the case that engineers and computer scientists are on the lookout for logic-programming-based approaches to hard problems, especially those which deal intrinsically in the enumeration of large state spaces.
