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)