turnstile travelogue

Abstract machines for logic programs

[Based on conversations with Rob Simmons. Reader prerequisites: comfortable with inference rules, peano notation, state machines.]

The following inference rules, it can be argued, define addition: whenever plus N M P holds, the numbers N and M sum to P.

----------------- pz
   plus 0 N N

   plus N M P
-------------------- ps
 plus (s N) M (s P)

With these rules, here's a derivation that 2 + 2 = 4:

----------------- pz
   plus 0 2 2
--------------- ps
   plus 1 2 3
--------------- ps
   plus 2 2 4

Inference rule sets aren't inherently programs, they are just definitions of relations. To use our definition of addition to calculate, we have to think of what we're doing as searching for a number X such that plus N M X holds, given N and M as inputs. The purpose of logic programming is to let us "run" a set of inference rules (perhaps together with a query) as a program. What mental model can we use to think about how a logic program runs, step by step?

Stack machines.

Here is a program, specified as a state machine, that evaluates queries of the form plus N M _, where N and M are known (in logic programming lingo, they are ground, which means they contain no logic variables that need solving-for):

k >> plus 0 N _     |----> k << N
k >> plus (s N) M _ |----> k; s _ >> plus N M _
k; s _ << N         |----> k << s N

Notation:

The syntax I used is meant to suggest the relational notation used in the inference rules, and to hint at the possibility that a logic programming language might use this kind of machine as an internal representation into which inference rules might be compiled.

Example run on plus 1 2 _:

       . >> plus 1 2 _
|----> .; s _ >> plus 0 2 _
|----> .; s _ << 2
|----> . << 3

Modes.

To produce this machine, we had to make one critical choice: which positions in the relation are inputs vs. outputs? This is called a mode assignment for a relation. In the previous example, we picked the first two positions as inputs and the last one as an output (assigned mode i/i/o). However, there are other modes we could pick for the plus relation, and they correspond to different abstract machines.

Here is a stack machine that instead implements subtraction, based on the mode assignment i/o/i. (You might have heard people claim that logic programs can be "run backwards"; this is one thing that can mean.)

k >> plus 0 _ P         |---->  k << P
k >> plus (s N) _ (s P) |---->  k; _ >> plus N _ P
k; _ << P               |---->  k << P

(We actually don't need a stack at all here, but we include it for uniformity.)

Example chain of steps:

        . >> plus 3 _ 4 
|---->  .; _ >> plus 2 _ 3
|---->  .; _ ; _ >> plus 1 _ 2
|---->  .; _ ; _ ; _ >> plus 0 _ 1
|---->  .; _ ; _ ; _ << 1
|---->4 . << 1

Note that this abstract machine can get stuck:

        . >> plus 3 _ 2 
|---->  .; _ >> plus 2 _ 1
|---->  .; _ ; _ >> plus 1 _ 0
|--/->

This corresponds to the fact that natural number subtraction is a partial function. When we write things as relations, one thing this frees us from is worrying about partiality and nondeterminism. But once we get interested in running a relation as a program, those concerns will arise. But, so far, we are just turning moded relations into state transitions for an abstract machine, which is perhaps a wee bit more "operational", but it's still a relation, just between states and successors to states (at mode i/o). Eventually we'll want to think of this state machine as a function in a total language, which means thinking about types, but let's hold off a little longer.

There's one more mode we could imagine running plus at: o/o/i. In other words, give me all the pairs of numbers N,M that sum to P.

Here's the stack machine.

k >> plus _ _ N     |---->  k << 0,N
k >> plus _ _ (s P) |---->  k; s _, _ >>  plus _ _ P
k; s _, _ << N , M  |---->  k << s N , M

This machine is nondeterministic. Here is one run for input . >> plus _ _ 3:

. >> plus _ _ 3
. << 0 , 3

And another:

. >> plus _ _ 3
. ; s _ , _ >> plus _ _ 2
. ; s _ , _ ; s _ , _ >> plus _ _ 1
. ; s _ , _ ; s _ , _ << 0 , 1
. ; s _ , _ << 1 , 1
. << 2 , 1

Exercise for reader and/or me in a later post:

Add an example for rules with multiple premises.

What are we doing?

This transformation is a pretty standard thing to do if you're in the business of specifying and implementing programming languages: we're taking what's variously known as a big-step or natural semantics and converting it into an abstract machine, a la Landin's SECD (though we're not fussed about the -ECD parts here; I inherit the stacks-only presentation most directly from Harper). Stacks can also be seen as first-order representations of continuations, a connection Reynolds describes in the OG definitional interpreters paper. Definitional interpreters can be seen as the most direct recursive interpretation of the inference rules we gave initially, but they don't give us the ability to express the full generality of relations, including partiality and nondeterminism, which incidentally are also things -- alongside exceptions, effect handlers, concurrency, and other useful programming idioms -- that one might want to implement for a programming language. Abstract machines are one tool for doing this. Reynold's process for carrying out these transformations on definitional interpreters represented as recursive functions is known as the functional correspondence.

In 1992, Hannan and Miller described how to carry out these transformations by hand over arbitrary logic programs in such a way that its correctness could be formally verified: From operational semantics to abstract machines. In 2004, Mads Sid Ager identified a fragment of logic programs for which this process could be automated: From natural semantics to abstract machines. I learned about this work via Simmons and Zerny (2013), who coin the term logical correspondence by analogy with Reynolds' functional correspondence, and extend prior results to substructural operational semantics.

From what I currently understand of the literature, the observation that this can be done (and, with some appropriate qualifiers, automated) has mostly been framed in terms of operational semantics for programming languages as the driving application. But the scope of "relations defined as collections of inference rules" is much larger than that, especially when you consider the advanced uptake of dependently-typed languages in which these definitions take the form of indexed inductive definitions. I've recently been curious about the abstract machines implied by this process for other kinds of programs.