[enum.ss tom@zwizwa.be**20090909082605 Ignore-this: 122f54db9d669d7c3926202acdeefd58 ] addfile ./staapl/machine/enum.ss hunk ./doc/staapl-ramblings.txt 52353 +Entry: Prolog and Pattern Matching +Date: Tue Sep 8 09:47:46 CEST 2009 + +Looks like I missed some important point about Prolog. In my head +it's simplified to `amb' + constraints in the form of horn clauses. +But then what? As a guide, let's take [1] and [2]. + +In [2], chapter 22 talks about `amb' (or `choose'). Relatively +straightforward. So what is `cut', explained in 22.5? Essentially, +eliminating part of a search tree. This is straightforward in +depth-first search, and requires marking of the resume stack. Then +22.6 talsk about breath-first search, implemented by replacing the +resume stack with a queue. + +Chapter 24 talks about prolog as ``rules as a means to construct a +tree of implications, which can then be searched using +non-determinism.'' Or prolog as a combination of pattern matching, +nondetermism and rules. A rule has the form + + if then . + +The basic idea is that if the body matches a fact, its head can be +added to the collection of facts. + +When asked for a fact, we can recursively sift through the facts and +heads of rules, essentially picking out rules and finding evidence. +The search ends when there is evidence found, or when all rules and +facts are exhausted. + +So, what about binding? Find all occurences of variables satisfying a +certain property. It looks like what is necessary to implement this +in Scheme is to map Scheme's binding mechanism to the rule binding. +In the following rule, + + (if (and (tree x) (summer)) then (green x)) + +which is the binding site, and which is the reference site for `x' ? + +It's not obvious, so maybe the answer is it depends on whether this is +interpreted as a constructor or a destructor, or both. Unification? +Indeed. [1][3]. + +One thing that confuses me is the 2 directions of information flow: to +see if a parameterized fact is true, one needs to run the rules +backwards, but for every value found, the value propagation runs the +other way. So it looks like control flow is going in one direction, +while data flow moves the opposite way! + +Let's try to organise the control flow first, and see how the data +flow can be incorporated in that solution. Given a set of rules, +construct functions that are indexed by proposition. + + ;; rule + (rule (and (tree x) (summer)) (green x)) + (rule #t (summer)) + (rule #t (tree pine)) + (rule #t (green algae)) + +Suppose `(green x)' nondeterministically binds x. How does this look +as in expression form? + +I'm stuck at expressing binding recursively. Let's try to make it +more difficult first + + (rule (and (tree x) (brown y)) (browntree x y)) + + +... + + +[1] http://mitpress.mit.edu/sicp/full-text/sicp/book/node92.html +[2] http://www.paulgraham.com/onlisptext.html +[3] http://en.wikipedia.org/wiki/Unification + + + +Entry: Resolution (Logic) +Date: Wed Sep 9 09:05:16 CEST 2009 + +Reading CTM[1] chapter 9 about relational + logic programming. + +The basic idea is that you want theorem proving: given a logic +sentence, the system needs to find a proof for it. On page 634 it +remarks: + +- theorem prover is limited (Goedel's [in]completeness theorems) +- algorithmic complexity: need a predictable operational semantics +- deduction should be constructive + +This is ensured by restricting the form of axioms so that an efficient +constructive theorem prover is possible. For Prolog these axioms are +Horn clauses, which allow an inference rule called resolution[2]. +Additionally, Prolog allows to add hints to map a logic program to a +more efficient operational semantics. + + +[1] http://www.info.ucl.ac.be/~pvr/book.html +[2] http://en.wikipedia.org/wiki/Resolution_%28logic%29 + + +Entry: Relational programming +Date: Wed Sep 9 09:29:28 CEST 2009 + + +( The theoretical framework of logic programming needs to sink in a +bit.. Let's focus on relational programming first: `choice' and +`fail'. ) + +I was wondering if it makes sense to allow infinite choice sequences. +Probably not, unless they appear at only one place in the tree. For +depth-first this should be on top, and for breath-first at the bottom. +Otherwise the infinite branching will prevent some children from ever +being reached. + +But, it does seem usefult to at least keep an algorithmic description +of choice points without having to resort to explicit lists. +Additionally, these choice points could be results from another search +problem, generated lazily.. + +So, what about reformulating choice as taking an enumerator by +default, instead of trying to shoe-horn procedural sequences back into +explicit lists. + +Design principles: + + - lazyness is good + + - enumerators (HOFs) are better than lazy lists (data structs) + + +So, `amb' takes a function. A choice point is then a continuation (a +hole) and an enumerator. The contination can be plugged into the +enumerator directly. + +(struct choice (k enum)) -> (enum k) + + +Now, does this compose? I.e. can the driver just execute the +enumerator and nest the backtracking that way? + +Hmm.. + + + + + hunk ./staapl/machine/amb-param.ss 19 - +(require "enum.ss") + hunk ./staapl/machine/amb-param.ss 40 -(define (amb . vals) ((current-amb) vals)) +(define (amb . vals) ((current-amb) (list->enum vals))) +(define (amb-enum enum) ((current-amb) enum)) hunk ./staapl/machine/amb-param.ss 47 -(define-struct choice (k values)) +(define-struct choice (k enum)) hunk ./staapl/machine/amb-param.ss 53 -(define (amb-for-each fn! prompt-thunk) +;; FIXME: implementing `cut' requires marking the stack of resume-points. + + + + +(define (amb-for-each fn! prompt-thunk [depth-first #t]) hunk ./staapl/machine/amb-param.ss 60 - ;; (printf "rps: ~a\n" resume-points) hunk ./staapl/machine/amb-param.ss 63 - ;; (printf "rv: ~a\n" rv) hunk ./staapl/machine/amb-param.ss 66 - ((struct choice (k vals)) - (next (for/fold ((rps rps)) ((v vals)) - (cons (lambda () (k v)) rps)))) + ((struct choice (k enum)) + (let ((vals (enum->list enum))) + (let ((thunks (map + (lambda (val) + (lambda () (k val))) + vals))) + (next + (if depth-first + (append thunks rps) + (append rps thunks)))))) hunk ./staapl/machine/amb-param.ss 85 - (shift/parameters (p ...) k (make-choice k vals)))) + (if (null? vals) + (fail) + (shift/parameters + (p ...) k + (make-choice k vals))))) hunk ./staapl/machine/amb-param.ss 97 + + hunk ./staapl/machine/enum.ss 1 +#lang scheme/base +(require scheme/base) +(require scheme/control) +(require srfi/45) +(require srfi/41) + +(provide (all-defined-out)) + +;; According to [1], enumerators are the superior traversal interface, +;; compared to generators or lazy lists. + +;; [1] http://lambda-the-ultimate.org/node/1224 +;; [2] http://srfi.schemers.org/srfi-41/srfi-41.html +;; [3] http://srfi.schemers.org/srfi-45/srfi-45.html + +;; The most general one is non-recursive left fold. + +(define (enum->stack enum) (enum cons '())) +(define (enum->list enum) (reverse (enum->stack enum))) +(define (list->enum lst) + (lambda (fn init) (foldl fn init lst))) + +(define (seq->enum seq) + (lambda (fn init) + (for/fold ((state init)) ((el seq)) (fn el state)))) + + +;; Converting an enumerator to a SRFI-45 stream. This needs to invert +;; control of the enumerator. + +(define (enum->stream enum) + (prompt + (enum (lambda (el _) (shift k (stream-cons el (k #f)))) #f) + stream-null)) hunk ./staapl/machine/prolog.ss 5 -(define (constrain bool) - (unless bool (fail))) hunk ./staapl/machine/prolog.ss 6 -(define x (make-parameter #f)) hunk ./staapl/machine/prolog.ss 7 -(amb-for-each - (lambda (x) (printf "sol: ~a\n" x)) - (lambda () - (amb-begin - (let ((a (amb 1 2)) - (b (amb 4 5))) - (constrain (= 6 (+ a b))) - (list a b))))) hunk ./staapl/machine/prolog.ss 8 + + +(define-struct rule (body head)) +(define (make-fact x) (make-rule #t x)) ;; Facts are rules without body. + +(define rules (make-parameter '())) +(define (rule! x) (rules (cons x (rules)))) + + +(define (query x) + (amb-for-each + (lambda (x) (printf "sol: ~a\n" x)) + (lambda () + (amb-begin + (x))))) + +(define-syntax rule-body + (syntax-rules (and or not) + ((_ (and b ...)) + (_ (or b ...)) + (_ (not b)) + (_ b + +(define-syntax-rule (rule body (name . params)) + (define-rule name + (lambda params + (rule-body body)))) + + + + +(rule (and (tree x) (summer)) (green x)) +(rule #t (summer)) +(rule #t (tree pine)) +(rule #t (green algae)) + +(define-syntax-rule (for-all binder fn) + + +(for-all (green x) (display x))