Fri Sep 11 12:37:47 CEST 2009


Looks like I really need Prolog, and more general, some kind of
theorem prover / constraint system.  It will probably pay to build one
and have an idea of the tradeoffs.

Let's finish what I have now.  In the previous attack, mapping rule
inference to lambda abstractions doesn't work, because it requires
_unification_ which is a symmetric binding construct, while pattern
matching and construction is asymmetric.

So, given a rule

    P(X) & Q(X,Y) -> R(Y)

this can be used in a query for R(Y) as follows:

     - the query R(Y) leads to a store with one unbound variable Y.
     - extend the vocabulary with the variable X
     - find a stream of solutions for Q(X,Y)
     - filter it with P(X)