Sun Sep 13 14:48:35 CEST 2009

How the query system works (SICP)

In [1] the stream-of-frames implementation is used to implement the
query system.

  In general, the query evaluator uses the following method to apply a
  rule when trying to establish a query pattern in a frame that
  specifies bindings for some of the pattern variables:

    * Unify the query with the conclusion of the rule to form, if
      successful, an extension of the original frame.

    * Relative to the extended frame, evaluate the query formed by the
      body of the rule.

  Notice how similar this is to the method for applying a procedure in
  the eval/apply evaluator for Lisp:

    * Bind the procedure's parameters to its arguments to form a frame
      that extends the original procedure environment.

    * Relative to the extended environment, evaluate the expression
      formed by the body of the procedure.

In my implementation, the stream-of-frames is the result of
`solutions', which can then be fed back into `amb' recursively.

It seems that the real problem is `alpha conversion' : to map
variables in a query to variables in a head/body combo.  A simple way
to do this is to represent the rules's parameters using functions
(higher order abstract syntax) HOAS[2]:

  ``In the domain of logical frameworks, the term higher-order
    abstract syntax is usually used to refer to a specific
    representation that uses the binders of the meta-language to
    encode the binding structure of the object language.''

However, in order to avoid explicit renaming and piggy-back on
Scheme's lexical variables, some deconstruction is necessary at
compile time.  It seems this needs to do the work twice.

Use explicit renaming then? (as in SICP).

Alternatively, we can give up the direct representation as lists and
only use the abstract one where the unification control flow is
expanded.  Maybe that's a better way: you don't need `eval' or any
direct interpreter as long as you have lambda and hygienic macros.  In
this case it looks like a store needs to be a run-time entitiy, but
the unification match is compile-time.

But, let's do renaming first.  A working implementation is worth more
it seems..  This is the core of [3]:

(define (unify-rule store pattern rule)
  (let* ((rule (map rename-variables rule))
         (store (add-free-variables store (rule-head rule))))
        ((store (unify store pattern (rule-head rule))))
        ((bpat (rule-body rule)))
      (unify-pattern store bpat))))

(define (unify-pattern store pattern)
  (unify-rule store pattern (choice/enum (rules-db))))

(define (solve pattern)
      (add-free-variables (empty) pattern)

So indeed, it is quite straightforward.

Rules can be partly staged + renames can be avoided, by piggy-backing
on a directed pattern matching binding form.  Currently I have this
implemented as a clause translator: the head match produces either a
fail, or a body where the rule's variables are substituted by the
corresponding sites in the input pattern.  Instead of constructing a
list, this could also just construct a recursive query invocation.

[1] http://mitpress.mit.edu/sicp/full-text/sicp/book/node94.html
[2] http://en.wikipedia.org/wiki/Higher-order_abstract_syntax
[3] http://zwizwa.be/darcs/staapl/staapl/machine/prolog.ss