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.
On 23 June 2016 at 03:46, Baishampayan Ghose <b.gh...@gmail.com> wrote:
> 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
>
> On Thu, Jun 23, 2016 at 7:52 AM, Ashish Negi <thisismyidash...@gmail.com>
> wrote:
>>
>> 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 ?
>>
>> --
>> You received this message because you are subscribed to the Google
>> Groups "Clojure" group.
>> To post to this group, send email to clojure@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+unsubscr...@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+unsubscr...@googlegroups.com.
>> For more options, visit https://groups.google.com/d/optout.
>
>
>
>
> --
> Baishampayan Ghose
> b.ghose at gmail.com
>
> --
> You received this message because you are subscribed to the Google
> Groups "Clojure" group.
> To post to this group, send email to clojure@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+unsubscr...@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+unsubscr...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.
--
You received this message because you are subscribed to the Google
Groups "Clojure" group.
To post to this group, send email to clojure@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+unsubscr...@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+unsubscr...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.
