Barliman: Prototype of a smart text editor

Re:Barliman: Prototype of a smart text editor by YeGoblynQueenne on Saturday July 30, 2016 @04:50PM (#12194647)

It would have been nice to see some more information on the way this works. I'm not clear exactly what is being searched- some set of built-in functions that are combined in the hopes of finding one that makes tests pass? A space of function components?

It's cool but I'd like to know what it does exactly. Maybe the explanation is spread around examples, but skimming through them I couldn't find it.

[ Parent | on HN ]

Re:Barliman: Prototype of a smart text editor by will_byrd on Monday August 01, 2016 @02:37AM (#12200564)

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

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?

[ Parent | on HN ]