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.