[Haskell-cafe] Logic programming using lazy evaluation

[Chris Kuklewicz]

Henning Thielemann wrote:
> I suspect that someone has already done this: A Haskell library which
> solves a system of simple equations, where it is only necessary to derive
> a value from an equation where all but one variables are determined. Say
> 
> 1+2=x      -- add 1 2 x
> y*z=20     -- times y z 20
> x+y=5      -- add x y 5
> 
> should be solved as
> 
> x=3
> y=2
> z=10
> 
> Of course, it is easy to do this for a finite number of variables and
> equations by assigning integer identifiers to the variables, then scanning
> the equations repeatedly until all determinable variables are determined.
> 
> However, imagine I have an infinite number of equations and an infinite
> number of variables, say
> 
> 1=x0        -- equal 1 x0
> 2*x0=x1     -- times 2 x0 x1
> 2*x1=x2     -- times 2 x1 x2
> 2*x2=x3     -- times 2 x2 x3
> ...
> 
> Accessing variable values by integer identifiers means that the garbage
> collector cannot free values that are no longer needed.

That will always be true for potentially non-finite lists of equations.

> 
> Thus I thought about how to solve the equations by lazy evaluation. Maybe
> it is possible to ty the knot this way
> 
> let (_,_,x0)  = add 1 2 x
>     (y0,z0,_) = times y z 20
>     (x1,y1,_) = add x y 5
>     x = alternatives [x0,x1]
>     y = alternatives [y0,y1]
>     z = alternatives [z0]
> in  (solve x, solve y, solve z)

> 
> Independent from the question of how to implement 'alternatives' and
> 'solve' I wonder if there is a less cumbersome way to do this kind of
> logic programming in Haskell.
> _______________________________________________


For an infinite number of equations you have to generate them as data at run
time.  Your notation above only works for a finite set of equations known at
compile time.

So you have a stream of equations, and each equation depends on some subset of
the variables seen so far and may also introduce new variables for the first time.

As equations are read it will become possible to solve for variables, so there
is an evolving environment of solved variables as you read the equation stream.

You can never free up the old variables since you cannot prove that future
equations will not use them.

You can forget old equations once all their variables have been assigned.

In general the combinatorial trick is: after reading a new equation to then find
a subset of n equations with n still unassigned variables.  Then run a solver on
these n equations & variables.  Once all such subsets have been solved you
proceed to the next new equation.  Then one of the n equations will have to be
the freshly read equation.  Your "only 1 undetermined variable" means that n is
restricted to only be 1, which greatly simplified finding an equation to solve.
 After any variable is solved the whole list of unsolved equations is revisited.

After each step the environment of variables and equations will be updated, and
if solving a set of equations found no solution then the whole set is
inconsistent and you can abort.  If solving a set of equations gives multiple
answers (x*x==4) then you could have parallel sets of variable assignments, or a
heuristic to pick only one member of that set of sets.  If a solved variables
causes other equations to fail then that set of values is inconsistent.

I can now see this as a straightforward State-like monad, where the state holds
the current environment of solved variables and unsolved equations.