Barliman's synthesis is based on the "relational interpreter" approach described in this 2012 Scheme Workshop paper: William E. Byrd, Eric Holk, and Daniel P.

Barliman's synthesis is based on the "relational interpreter" approach described in this 2012 Scheme Workshop paper: William E. Byrd, Eric Holk, and Daniel P. Friedman. miniKanren, Live and Untagged: Quine Generation via Relational Interpreters (Programming Pearl). Proceedings of the 2012 Workshop on Scheme and Functional Programming, Copenhagen, Denmark, 2012. http://webyrd.net/quines/quines.pdf http://webyrd.net/quines/quines.pdf https://github.com/webyrd/2012-scheme-workshop-quines-paper-code https://github.com/webyrd/2012-scheme-workshop-quines-paper-... The basic idea is to write an interpreter as a relation in a constraint logic programming language (miniKanren, in this case). Since the interpreter is a relation, there is no real distinction between "input" arguments and "output" values. More generally, arguments to the relational interpreter can be partially-instantiated terms that contain logic variables representing unknown subexpressions. Since the interpreter for "miniScheme" is fully relational, running the interpreter "forwards" to generate a value from a given expressions, or running the interpreter "backwards" to generate an expression that evaluates to a given value, are essentially the same operation. The only difference is where the logic variables are placed in the query to the relational interpreter. But the approach is more general than just running the interpreter forward or backward. Logic variables can be used in both the expression to be evaluated, and in the expected value. This is how we can generate quines (expressions that evaluate to themselves) in miniKanren directly from the mathematical definition of a quine, for example. The query (run N (q) (evalo q q)) will produce N quines, including a quine that is alpha-equivalent to the canonical Scheme quine ((lambda (x) (list x (list (quote quote) x))) (quote (lambda (x) (list x (list (quote quote) x))))) This example shows some of the generality of the relational interpreter approach---program inversion applied to a Scheme interpreter would not be able to generate quines. The search is done over all possible terms in "miniScheme," a Turing-complete subset of Scheme that supports higher-order variadic functions, recursion, lists and pairs, lexical scoping/shadowing, etc., and that has been extended with pattern-matching. Does that help?