Joy of Clojure : Backward running lisp ??

[Ashish Negi]

I am reading joy of clojure. In the "forward to second edition" William E Byrd and Daniel P Firedman says :

As with recursion, the art of defining little languages encourages—and rewards—wishful thinking. You might think to yourself, “If only I had a language for expressing the rules for legal passwords for my login system.” A more involved example—a story, really—started several years ago, when we thought to ourselves, “If only we had the right relational language, we could write a Lisp interpreter that runs backward.”[2] What does this mean?

An interpreter can be thought of as a function that maps an input expression, such as (+ 5 1), onto a value—in this case, 6. We wanted to write an interpreter in the style of a relational database, in which either the expression being interpreted or the value of that expression, or both, can be treated as unknown variables. We can run the interpreter forward using the query (interpret ‘(+ 5 1) x), which associates the query variable x with the value 6. Better yet, we can run the interpreter backward with the query (interpret x 6), which associates x with an infinite stream of expressions that evaluate to 6, including (+ 5 1) and ((lambda (n) (* n 2)) 3). (Brainteaser: determine the behavior of the query (interpret x x).)

Although the writer gave an example of `(interpret x 6)` i could not imagine the use case of `lisp interpreter running backwards` ?
I am not even sure what he meant exactly.

Thinking on it, i could only relate this to theorem provers where you run backwards from the result.
Can somebody explain this ?

[Baishampayan Ghose]

Running "backwards" here pertains to logic/relational programming in MiniKanren/core.logic style. Roughly here programs are expressed in terms of relations between the input and output. So given an input and an output query you'll run it forwards and by making the input itself a variable with a fixed output will generate a series of possible inputs, that'd be running it backwards. Useful for generating programs :-)

Here is an example: http://jvns.ca/blog/2013/11/20/day-31-logic-programming-pretty-music/

~BG

--
You received this message because you are subscribed to the Google
Groups "Clojure" group.
To post to this group, send email to clo...@googlegroups.com
Note that posts from new members are moderated - please be patient with your first post.
To unsubscribe from this group, send email to
clojure+u...@googlegroups.com
For more options, visit this group at
http://groups.google.com/group/clojure?hl=en
---
You received this message because you are subscribed to the Google Groups "Clojure" group.
To unsubscribe from this group and stop receiving emails from it, send an email to clojure+u...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

--

Baishampayan Ghose
b.ghose at gmail.com

[Gary Verhaegen]

In functional programming, you work with functions. Functions have a
well-defined list of inputs and a single output. So you can say of the
function cons, for example, that it takes as input a value and a list,
and yields as output a new list with the value prepended to the given
list; for example (cons 1 '(3 4)) would yield the value '(1 3 4).

In logic (sometimes called relational) programming, you work with
relations. A relation defines some link between multiple values. The
equivalent example to the above, usually denoted "conso" in the
Clojure world (and something like cons° in miniKanren, I think) would
be a relation of three values: (conso a b c). The more mathematical
interpretation would be "conso is true for any three values a, b, c
such that c is a list of at least one element, a is the first element
of c and b is a list of all elements of c except the first, in the
same order". In practical terms, a logic engine like miniKanren will
allow you to supply real values for some of the arguments and let the
others be free, and will return example values for which the relation
holds.

For example, (conso 1 '(3 4) c) would return something that says "c
must be '(3 4)". In this case, by analogy to the functional version,
we say we are running the relation "forward", i.e. in the same
direction as the function. But you can also ask a logic engine for
"(conso a b '(1 3 4))", and it will reply with something like "a
should be 1, b should be '(3 4)", and, again, by analogy with the
functional equivalent, we would say you are running the "function"
backwards. In terms of relational programming, in either case you're
just applying the relation, but most people who hear about relational
programming are more familiar with functions (or procedures) and will
relate to the notion that the "natural", i.e. "forward" way of running
conso is to supply the first two arguments and expect the engine to
supply values for the third, rather than the other way around.

Note that you could also ask a logic engine for "(conso 1 b '(1 3
4))", and it should respond with "b should be '(3 4)", which is
running it middleward, I guess. It's harder to relate to functions
when you have more than one "input", as logic programming would let
you specify any subset of them. Relations can also fail, such as if
you ask for "(conso 1 b '(3 4 5))"; in that case the logic engine,
depending on the robustness of its own implementation and the
definition of conso, would either enter an infinite loop trying to
find a value for which this holds or just respond with "there is no
value for b that makes this relation hold".

conso is a simple example in that it is bijective. If you instead
consider a concat function, such that (concat l1 l2), where l1 and l2
are lists, would yield a new list l3 with first all of the elements of
l1 then all of the elements of l2, then you can get a more interesting
equivalent relation ("concato"?).

Let's imagine you define (concato l1 l2 l3) to be true if l3 = (concat
l1 l2) (you cannot just state it like that to the logic engine). Then,
if you ask your logic engine about the relation (concato a b '(1 2
3)), it would respond with "Here are some possible values for a and b:
a = '(), b = '(1 2 3); a = '(1), b = '(2 3); a = '(1 2), b = '(3); a =
'(1 2 3), b = '()".

What Byrd and Friedman have been working on for some time now is the
(research) question of "can we write a relation that defines a Lisp
interpreter?", where a Lisp interpreter is thought of as the function
eval, essentially. So if (eval '(+ 1 2)) would yield 3, can you define
a relation evalo, within the constraints of their specific logic
engine ({mini,alpha}Kanren), that mimics that behaviour when run
"forward" (i.e. given the first argument as a value and the second one
as a free-floating logic variable) and also works "backwards" (i.e.
given the first argument as a free-floating variable and the second
one as a value).

So they would define (evalo a b) such that it is satisfied iff (eval
a) yields b (though again you cannot tell it that simply to your logic
engine, hence the research part); this means that for example (evalo
'(+ 1 2) 3) would be satisfied, (evalo '(+ 1 2) 4) would not be
satisfied, (evalo '(+ 1 2) a) would return something like "this can be
satisfied if a = 3" (forward), and (evalo a 3) (i.e. "backward with
respect to the equivalent function) would return something along the
lines of "There are a bunch of programs that can evaluate to 3. Here
are a few of them: '(+ 0 3), '(+ 1 2), '(+ 2 1), '(- 4 1), '((fn []
3)), ..."

Their last question is a bit tricky: what program, when evaluated,
yields itself? This is the notion of a quine, and quines are pretty
hard to generate for humans (apart from the simple self-evaluating
values, of course). An example quine in Clojure, which I just stole
from http://programming-puzzler.blogspot.co.uk/2012/11/clojure-makes-quines-way-too-easy.html,
would be:

((fn [x] (list x (list (quote quote) x))) (quote (fn [x] (list x (list
(quote quote) x)))))

I'm not sure it's the simplest possible quine, but you can probably
already see that this is far from trivial to generate by searching
through the space of all possible programs.

[Colin Yates]

Gary - that was great to read. Thanks ;-)

[Nathan Davis]

One common problem we deal with in programming goes like this:

I have certain inputs.  I desire a certain output.  What function (or combination of functions) will give me the desired output?

Since a relation makes no distinction between "inputs" and "outputs", relational programming is one way we can approach this problem.  All we need is a relation that relates a program, its input(s), and its output.  Then, by fixing the inputs and output, we can generate programs that produce the desired output.

We could use such a tool as an aid to guide us in writing programs.  I.e., we can basically write queries to find core functions (and combinations thereof) that produce the desired output.  But we can take this even further.  In general, we can write specifications for functions.  From this specification, we can generate programs that conform to the specification.

But we don't have to stop there.  Instead of specifying (either entirely or in part) the inputs and output, we can fix and leave free any components of the relation to any degree.  For example, we might (partially) specify a program and its output.  We can then generate inputs that result in the given output.

So, at least in theory, a relational lisp interpreter would give us (in many respects) the "ultimate" development tool.  If we leave everything free (i.e., no restrictions on the programs, its inputs, or the output), then we can generate every possible lisp program.  This isn't very useful per se.  But by partially specifying one or more components of the relation, we provide a priori knowledge to help guild the process.  Even if it is not enough to produce the desired result immediately, we might be able to gain further insight into the specific problem we are trying to solve.  From this, we can refine the specification.  We can iterate this process until we arrive at an acceptable solution.  This gives us a development process where human and machine "collaborate" to derive a program.

Unfortunately, the power of relational programming comes at a cost.  That cost is divergence (non-termination of the search algorithm).  It is extremely tricky to write relations in a way that guarantee (when there are a fininte number of solutions) that (a) all soutions will be found in a finite amout of time, and (b) if there are no (more) solutions, the search terminates in a finite amount of time.  This largely boils down to limiting the search space to a finite domain (while ensuring no valid results are excluded).  This seems simple, but is far from trivial in practice (see, for instance, the chapter on relational arithmetic in Byrd's thesis).

The possibility of infinite results sets presents its own problems, such as how to output such an infinite set.  core.logic uses Clojure's lazy seqs for this.  Minikanren's original implementation in Scheme requires limiting the number of results rendered from an inifinite result set.

Furthermore, whether the solution set is inifinite or finite, it can be difficult to separate "interesting" solutions from "mundane" solutions.  Minikanren's interleaving search can help with this (especially when the solution set is infinite), but is not a panacea.

In the case of generating programs, it would also be desirable that the generated programs are guaranteed to terminate.  However, is has been shown that there algorithm that is capable of determining (for all possible programs) if a given program always terminates for any input.  So it would appear that we must choose between the possibility of non-terminating programs and limiting the range of generated programs to those which (the generative system) can prove to be terminating.  Different situations may call for different choices.

Hopefully this helps highlight some of the (theoretical) use-cases of a relational lisp interpreter, as well as provide some insight into the difficulties in implementing such an interpreter.

 

On Wednesday, June 22, 2016 at 9:22:35 PM UTC-5, Ashish Negi wrote:

One usecase of a "relational" lisp interpretter

[Scott Nielsen]

One of the authors of the forward (William Byrd) gave a great presentation on miniKanren at lambda lounge utah a couple of years ago. Towards the end of the presentation we went through the exercise of actually creating a simple lisp interpreter that can run backwards. Luckily it was recorded and posted online. https://www.youtube.com/watch?v=zHov3fKYqBA