[Haskell-cafe] Logic programming using lazy evaluation

[Henning Thielemann]

On Tue, 27 Feb 2007, Chris Kuklewicz wrote:

> 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.

Since the program, which generates the equations is finite, it may well be
possible to see - even for the garbage collector - that some variables are
no longer used.

> 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.

For me it is ok to consider x*x==4 as unsolveable, if there is no other
equation where x can be derived from.