Abstract Machines for Logic Programs

# Abstract machines for logic programs Source: [https://chrisistyping.bearblog.dev/abstract-machines-for-logic-programs/](https://chrisistyping.bearblog.dev/abstract-machines-for-logic-programs/) *06 Apr, 2026* \[Based on conversations with[Rob Simmons](https://typesafety.net/rob/about/)\. 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 states of the machine are- `k \>\> q`\(evaluate query`q`on stack`k`\), or - `k << a`\(return answer`a`to stack`k`\)\. - Stacks`k`are lists of frames representing "next steps of computation"\. The only frame we need for this machine is`s \_`, which tells us to add one\. - To start the machine, configure state`\[\] \>\> plus N M`\(where`\[\]`is the empty stack\), wait until it enters configuration`\[\] << P`, and read off`P`as the result\. 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](https://doi.org/10.1093%2Fcomjnl%2F6.4.308)\(though we're not fussed about the \-ECD parts here; I inherit the stacks\-only presentation most directly from[Harper](https://www.cs.cmu.edu/~rwh/pfpl.html)\)\. Stacks can also be seen as first\-order representations of*continuations*, a connection Reynolds describes in the OG[definitional interpreters paper](https://homepages.inf.ed.ac.uk/wadler/papers/papers-we-love/reynolds-definitional-interpreters-1998.pdf)\. 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](https://www.lix.polytechnique.fr/~dale/papers/mscs92.pdf)\. In 2004, Mads Sid Ager identified a fragment of logic programs for which this process could be automated:[From natural semantics to abstract machines](https://scispace.com/pdf/from-natural-semantics-to-abstract-machines-4kgcst64qr.pdf)\. I learned about this work via[Simmons and Zerny \(2013\)](https://dl.acm.org/doi/10.1145/2505879.2505899), who coin the term*logical*correspondence by analogy with Reynolds'*functional*correspondence, and extend prior results to[substructural operational semantics](https://www.cs.cmu.edu/~fp/papers/lics09.pdf)\. 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\.