346 views

Skip to first unread message

Jun 22, 2016, 10:22:35 PM6/22/16

to Clojure

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

*
*

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 prover*s where you run backwards from the result.

Can somebody explain this ?

*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 `

I am not even sure what he meant exactly.

Thinking on it, i could only relate this to

Can somebody explain this ?

Jun 22, 2016, 10:46:53 PM6/22/16

to Clojure Group

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

b.ghose at gmail.com

Jun 23, 2016, 3:18:33 AM6/23/16

to clo...@googlegroups.com

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.

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.

Jun 23, 2016, 11:36:55 AM6/23/16

to clo...@googlegroups.com

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

Jun 27, 2016, 3:06:52 PM6/27/16

to Clojure

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.

One usecase of a "relational" lisp interpretter

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

Jun 28, 2016, 12:27:40 AM6/28/16

to Clojure

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

Reply all

Reply to author

Forward

0 new messages

Search

Clear search

Close search

Google apps

Main menu