@@ -0,0 +1,477 @@
; Quick miniKanren-like code
;
; written at the meeting of a Functional Programming Group
; (Toukyou/Shibuya, Apr 29, 2006), as a quick illustration of logic
; programming. The code is really quite trivial and unsophisticated:
; it was written without any preparation whatsoever. The present file
; adds comments and makes minor adjustments.
;
; $Id: sokuza-kanren.scm,v 1.1 2006/05/10 23:12:41 oleg Exp oleg $
; Point 1: `functions' that can have more (or less) than one result
;
; As known from logic, a binary relation xRy (where x \in X, y \in Y)
; can be represented by a _function_ X -> PowerSet{Y}. As usual in
; computer science, we interpret the set PowerSet{Y} as a multi-set
; (realized as a regular scheme list). Compare with SQL, which likewise
; uses multisets and sequences were sets are properly called for.
; Also compare with Wadler's `representing failure as a list of successes.'
;
; Thus, we represent a 'relation' (aka `non-deterministic function')
; as a regular scheme function that returns a list of possible results.
; Here, we use a regular list rather than a lazy list, just to be quick.
; First, we define two primitive non-deterministic functions;
; one of them yields no result whatsoever for any argument; the other
; merely returns its argument as the sole result.
(define (fail x ) '())
(define (succeed x ) (list x))
; We build more complex non-deterministic functions by combining
; the existing ones with the help of the following two combinators.
; (disj f1 f2) returns all the results of f1 and all the results of f2.
; (disj f1 f2) returns no results only if neither f1 nor f2 returned
; any. In that sense, it is analogous to the logical disjunction.
(define (disj f1 f2 )
(lambda (x )
(append (f1 x) (f2 x))))
; (conj f1 f2) looks like a `functional composition' of f2 and f1.
; Only (f1 x) may return several results, so we have to apply f2 to
; each of them.
; Obviously (conj fail f) and (conj f fail) are both equivalent to fail:
; they return no results, ever. It that sense, conj is analogous to the
; logical conjunction.
(define (conj f1 f2 )
(lambda (x )
(apply append (map f2 (f1 x)))))
; Examples
(define (cout . args )
(for-each display args))
(define nl #\newline)
(cout " test1"
((disj
(disj fail succeed)
(conj
(disj (lambda (x ) (succeed (+ x 1 )))
(lambda (x ) (succeed (+ x 10 ))))
(disj succeed succeed)))
100 )
nl)
; => (100 101 101 110 110)
; Point 2: (Prolog-like) Logic variables
;
; One may think of regular variables as `certain knowledge': they give
; names to definite values. A logic variable then stands for
; `improvable ignorance'. An unbound logic variable represents no
; knowledge at all; in other words, it represents the result of a
; measurement _before_ we have done the measurement. A logic variable
; may be associated with a definite value, like 10. That means
; definite knowledge. A logic variable may be associated with a
; semi-definite value, like (list X) where X is an unbound
; variable. We know something about the original variable: it is
; associated with the list of one element. We can't say though what
; that element is. A logic variable can be associated with another,
; unbound logic variable. In that case, we still don't know what
; precisely the original variable stands for. However, we can say that it
; represents the same thing as the other variable. So, our
; uncertainty is reduced.
; We chose to represent logic variables as vectors:
(define (var name ) (vector name))
(define var? vector?)
; We implement associations of logic variables and their values
; (aka, _substitutions_) as associative lists of (variable . value)
; pairs.
; One may say that a substitution represents our current knowledge
; of the world.
(define empty-subst '())
(define (ext-s var value s ) (cons (cons var value) s))
; Find the value associated with var in substitution s.
; Return var itself if it is unbound.
; In miniKanren, this function is called 'walk'
(define (lookup var s )
(cond
((not (var? var)) var)
((assq var s) => (lambda (b ) (lookup (cdr b) s)))
(else var)))
; There are actually two ways of implementing substitutions as
; associative list.
; If the variable x is associated with y and y is associated with 1,
; we could represent this knowledge as
; ((x . 1) (y . 1))
; It is easy to lookup the value associated with the variable then,
; via a simple assq. OTH, if we have the substitution ((x . y))
; and we wish to add the association of y to 1, we have
; to make rearrangements so to produce ((x . 1) (y . 1)).
; OTH, we can just record the associations as we learn them, without
; modifying the previous ones. If originally we knew ((x . y))
; and later we learned that y is associated with 1, we can simply
; prepend the latter association, obtaining ((y . 1) (x . y)).
; So, adding new knowledge becomes fast. The lookup procedure becomes
; more complex though, as we have to chase the chains of variables.
; To obtain the value associated with x in the latter substitution, we
; first lookup x, obtain y (another logic variable), then lookup y
; finally obtaining 1.
; We prefer the latter, incremental way of representing knowledge:
; it is easier to backtrack if we later find out our
; knowledge leads to a contradiction.
; Unification is the process of improving knowledge: or, the process
; of measurement. That measurement may uncover a contradiction though
; (things are not what we thought them to be). To be precise, the
; unification is the statement that two terms are the same. For
; example, unification of 1 and 1 is successful -- 1 is indeed the
; same as 1. That doesn't add however to our knowledge of the world. If
; the logic variable X is associated with 1 in the current
; substitution, the unification of X with 2 yields a contradiction
; (the new measurement is not consistent with the previous
; measurements/hypotheses). Unification of an unbound logic variable
; X and 1 improves our knowledge: the `measurement' found that X is
; actually 1. We record that fact in the new substitution.
; return the new substitution, or #f on contradiction.
(define (unify t1 t2 s )
(let ((t1 (lookup t1 s)) ; find out what t1 actually is given our knowledge s
(t2 (lookup t2 s))); find out what t2 actually is given our knowledge s
(cond
((eq? t1 t2) s) ; t1 and t2 are the same; no new knowledge
((var? t1) ; t1 is an unbound variable
(ext-s t1 t2 s))
((var? t2) ; t2 is an unbound variable
(ext-s t2 t1 s))
((and (pair? t1) (pair? t2)) ; if t1 is a pair, so must be t2
(let ((s (unify (car t1) (car t2) s)))
(and s (unify (cdr t1) (cdr t2) s))))
((equal? t1 t2) s) ; t1 and t2 are really the same values
(else #f ))))
; define a bunch of logic variables, for convenience
(define vx (var 'x ))
(define vy (var 'y ))
(define vz (var 'z ))
(define vq (var 'q ))
(cout " test-u1"
(unify vx vy empty-subst)
nl)
; => ((#(x) . #(y)))
(cout " test-u2"
(unify vx 1 (unify vx vy empty-subst))
nl)
; => ((#(y) . 1) (#(x) . #(y)))
(cout " test-u3"
(lookup vy (unify vx 1 (unify vx vy empty-subst)))
nl)
; => 1
; when two variables are associated with each other,
; improving our knowledge about one of them improves the knowledge of the
; other
(cout " test-u4"
(unify (cons vx vy) (cons vy 1 ) empty-subst)
nl)
; => ((#(y) . 1) (#(x) . #(y)))
; exactly the same substitution as in test-u2
; Part 3: Logic system
;
; Now we can combine non-deterministic functions (Part 1) and
; the representation of knowledge (Part 2) into a logic system.
; We introduce a 'goal' -- a non-deterministic function that takes
; a substitution and produces 0, 1 or more other substitutions (new
; knowledge). In case the goal produces 0 substitutions, we say that the
; goal failed. We will call any result produced by the goal an 'outcome'.
; The functions 'succeed' and 'fail' defined earlier are obviously
; goals. The latter is the failing goal. OTH, 'succeed' is the
; trivial successful goal, a tautology that doesn't improve our
; knowledge of the world. We can now add another primitive goal, the
; result of a `measurement'. The quantum-mechanical connotations of
; `the measurement' must be obvious by now.
(define (== t1 t2)
(lambda (s )
(cond
((unify t1 t2 s) => succeed)
(else (fail s)))))
; We also need a way to 'run' a goal,
; to see what knowledge we can obtain starting from sheer ignorance
(define (run g ) (g empty-subst))
; We can build more complex goals using lambda-abstractions and previously
; defined combinators, conj and disj.
; For example, we can define the function `choice' such that
; (choice t1 a-list) is a goal that succeeds if t1 is an element of a-list.
(define (choice var lst )
(if (null? lst) fail
(disj
(== var (car lst))
(choice var (cdr lst)))))
(cout " test choice 1"
(run (choice 2 ' (1 2 3 )))
nl)
; => (()) success
(cout " test choice 2"
(run (choice 10 ' (1 2 3 )))
nl)
; => ()
; empty list of outcomes: 10 is not a member of '(1 2 3)
(cout " test choice 3"
(run (choice vx ' (1 2 3 )))
nl)
; => (((#(x) . 1)) ((#(x) . 2)) ((#(x) . 3)))
; three outcomes
; The name `choice' should evoke The Axiom of Choice...
; Now we can write a very primitive program: find an element that is
; common in two lists:
(define (common-el l1 l2 )
(conj
(choice vx l1)
(choice vx l2)))
(cout " common-el-1"
(run (common-el ' (1 2 3 ) ' (3 4 5 )))
nl)
; => (((#(x) . 3)))
(cout " common-el-2"
(run (common-el ' (1 2 3 ) ' (3 4 1 7 )))
nl)
; => (((#(x) . 1)) ((#(x) . 3)))
; two elements are in common
(cout " common-el-3"
(run (common-el ' (11 2 3 ) ' (13 4 1 7 )))
nl)
; => ()
; nothing in common
; Let us do something a bit more complex
(define (conso a b l ) (== (cons a b) l))
; (conso a b l) is a goal that succeeds if in the current state
; of the world, (cons a b) is the same as l.
; That may, at first, sound like the meaning of cons. However, the
; declarative formulation is more powerful, because a, b, or l might
; be logic variables.
;
; By running the goal which includes logic variables we are
; essentially asking the question what the state of the world should
; be so that (cons a b) could be the same as l.
(cout " conso-1"
(run (conso 1 ' (2 3 ) vx))
nl)
; => (((#(x) 1 2 3))) === (((#(x) . (1 2 3))))
(cout " conso-2"
(run (conso vx vy (list 1 2 3 )))
nl)
; => (((#(y) 2 3) (#(x) . 1)))
; That looks now like 'cons' in reverse. The answer means that
; if we replace vx with 1 and vy with (2 3), then (cons vx vy)
; will be the same as '(1 2 3)
; Terminology: (conso vx vy '(1 2 3)) is a goal (or, to be more precise,
; an expression that evaluates to a goal). By itself, 'conso'
; is a parameterized goal (or, abstraction over a goal):
; conso === (lambda (x y z) (conso x y z))
; We will call such an abstraction 'relation'.
; Let us attempt a more complex relation: appendo
; That is, (appendo l1 l2 l3) holds if the list l3 is the
; concatenation of lists l1 and l2.
; The first attempt:
(define (apppendo l1 l2 l3 )
(disj
(conj (== l1 '() ) (== l2 l3)) ; [] ++ l == l
(let ((h (var 'h )) (t (var 't )) ; (h:t) ++ l == h : (t ++ l)
(l3p (var 'l3p )))
(conj
(conso h t l1)
(conj
(conso h l3p l3)
(apppendo t l2 l3p))))))
; If we run the following, we get into the infinite loop.
; (cout "t1"
; (run (apppendo '(1) '(2) vq))
; nl)
; It is instructive to analyze why. The reason is that
; (apppendo t l2 l3p) is a function application in Scheme,
; and so the (call-by-value) evaluator tries to find its value first,
; before invoking (conso h t l1). But evaluating (apppendo t l2 l3p)
; will again require the evaluation of (apppendo t1 l21 l3p1), etc.
; So, we have to introduce eta-expansion. Now, the recursive
; call to apppendo gets evaluated only when conj applies
; (lambda (s) ((apppendo t l2 l3p) s)) to each result of (conso h l3p l3).
; If the latter yields '() (no results), then appendo will not be
; invoked. Compare that with the situation above, where appendo would
; have been invoked anyway.
(define (apppendo l1 l2 l3 )
(disj ; In Haskell notation:
(conj (== l1 '() ) (== l2 l3)) ; [] ++ l == l
(let ((h (var 'h )) (t (var 't )) ; (h:t) ++ l == h : (t ++ l)
(l3p (var 'l3p )))
(conj
(conso h t l1)
(lambda (s )
((conj
(conso h l3p l3)
(lambda (s )
((apppendo t l2 l3p) s))) s))))))
(cout " t1"
(run (apppendo ' (1 ) ' (2 ) vq))
nl)
; => (((#(l3p) 2) (#(q) #(h) . #(l3p)) (#(t)) (#(h) . 1)))
; That all appears to work, but the result is kind of ugly;
; and all the eta-expansion spoils the code.
; To hide the eta-expansion (that is, (lambda (s) ...) forms),
; we have to introduce a bit of syntactic sugar:
(define-syntax conj*
(syntax-rules ()
((conj*) succeed)
((conj* g) g)
((conj* g gs ...)
(conj g (lambda (s ) ((conj* gs ...) s))))))
; Incidentally, for disj* we can use a regular function
; (because we represent all the values yielded by a non-deterministic
; function as a regular list rather than a lazy list). All branches
; of disj will be evaluated anyway, in our present model.
(define (disj* . gs )
(if (null? gs) fail
(disj (car gs) (apply disj* (cdr gs)))))
; And so we can re-define appendo as follows. It does look
; quite declarative, as the statement of two equations that
; define what list concatenation is.
(define (apppendo l1 l2 l3 )
(disj ; In Haskell notation:
(conj* (== l1 '() ) (== l2 l3)) ; [] ++ l == l
(let ((h (var 'h )) (t (var 't )) ; (h:t) ++ l == h : (t ++ l)
(l3p (var 'l3p )))
(conj*
(conso h t l1)
(conso h l3p l3)
(apppendo t l2 l3p)))))
; We also would like to make the result yielded by run more
; pleasant to look at.
; First of all, let us assume that the variable vq (if bound),
; holds the answer to our inquiry. Thus, our new run will try to
; find the value associated with vq in the final substitution.
; However, the found value may itself contain logic variables.
; We would like to replace them, too, with their associated values,
; if any, so the returned value will be more informative.
; We define a more diligent version of lookup, which replaces
; variables with their values even if those variables occur deep
; inside a term.
(define (lookup* var s )
(let ((v (lookup var s)))
(cond
((var? v) v) ; if lookup returned var, it is unbound
((pair? v)
(cons (lookup* (car v) s)
(lookup* (cdr v) s)))
(else v))))
; We can now redefine run as
(define (run g )
(map (lambda (s ) (lookup* vq s)) (g empty-subst)))
; and we can re-run the test
(cout " t1"
(run (apppendo ' (1 ) ' (2 ) vq))
nl)
; => ((1 2))
(cout " t2"
(run (apppendo ' (1 ) ' (2 ) ' (1 )))
nl)
; => ()
; That is, concatenation of '(1) and '(2) is not the same as '(1)
(cout " t3"
(run (apppendo ' (1 2 3 ) vq ' (1 2 3 4 5 )))
nl)
; => ((4 5))
(cout " t4"
(run (apppendo vq ' (4 5 ) ' (1 2 3 4 5 )))
nl)
; => ((1 2 3))
(cout " t5"
(run (apppendo vq vx ' (1 2 3 4 5 )))
nl)
; => (() (1) (1 2) (1 2 3) (1 2 3 4) (1 2 3 4 5))
; All prefixes of '(1 2 3 4 5)
(cout " t6"
(run (apppendo vx vq ' (1 2 3 4 5 )))
nl)
; => ((1 2 3 4 5) (2 3 4 5) (3 4 5) (4 5) (5) ())
; All suffixes of '(1 2 3 4 5)
(cout " t7"
(run (let ((x (var 'x )) (y (var 'y )))
(conj* (apppendo x y ' (1 2 3 4 5 ))
(== vq (list x y)))))
nl)
; => ((() (1 2 3 4 5)) ((1) (2 3 4 5)) ((1 2) (3 4 5))
; ((1 2 3) (4 5)) ((1 2 3 4) (5)) ((1 2 3 4 5) ()))
; All the ways to split (1 2 3 4 5) into two complementary parts
; For more detail, please see `The Reasoned Schemer'
Pet3ris created this gist