On Tue, 27 Feb 2007, Ulf Norell wrote:

On 2/27/07, 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

You might want to check out the following paper:

http://www.cs.chalmers.se/~koen/pubs/entry-haskell00-typedlp.html

Thanks for the link! It reminds me, that my problem differs from usual logic programming. I'm not interested in multiple solutions, I expect only one. If a variable is underdetermined, it shall be evaluated to "undefined". If a variable is overdetermined, that is different rules lead to different values for that variable, one of these values shall be returned. Checking for consistency per variable would require processing the whole (possibly infinite) list of rules. Instead one could check consistency per rule. That is, the solver should return a list of Bools which indicate which rules could be satisfied. In this setting it should be possible to solve the equations lazily. In contrast to the paper I assume that I can neither use Int variable identifiers nor STRefs because they would prevent the garbage collector from freeing unreferenced variable substitutions.

On Tue, 27 Feb 2007, Chris Kuklewicz wrote:

...

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.

Here is some implementation that creates and solves infinitely many equations - of course, it cannot check if found variable substitutions satisfy all equations. However this implementation still blows up the heap, because every variable needs one more iteration of the solution algorithm. {- | We want to solve 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 @ However different from usual logic programming, I'm not interested in multiple solutions, I expect only one. If a variable is underdetermined, e.g. if the only rule containing @x@ is @add x x 3@, it shall be evaluated to "undefined". If a variable is overdetermined, that is different rules lead to different values for that variable, one of these values shall be returned. Checking for consistency per variable would require processing the whole (possibly infinite) list of rules. Instead one could check consistency per rule. That is, the solver should return a list of Bools which indicates which rules could be satisfied. In this setting it is possible to solve the equations lazily. We use a naive algorithm, but the crux is that we implement it lazily. In each step we scan all equations and determine the values for variables which can be determined immediately. We repeat this infinitely often. Consider the system @ x+y=3 y*z=6 z=3 @ then we get the following iteration results for @(x,y,z)@: @ [(Nothing, Nothing, Nothing), (Nothing, Nothing, Just 3), (Nothing, Just 2, Just 3), (Just 1, Just 2, Just 3), (Just 1, Just 2, Just 3), ... @ However, since we organize the iteration per variable, we obtain @ x = [Nothing, Nothing, Nothing, Just 1, ... y = [Nothing, Nothing, Just 2, ... z = [Nothing, Just 3, ... @ Features: * free choice of types of values and static type checking * free choice of rules * lazy evaluation of solutions, thus infinitely many variables and rules are possible (although slow) -} module UniqueLogic where import Control.Monad (liftM, liftM2, msum, mplus) import Data.Maybe (catMaybes) import Data.List (transpose) {- * Basic routines -} newtype Variable a = Variable {listFromVariable :: [Maybe a]} deriving Show constant :: a -> Variable a constant = Variable . repeat . Just rule2 :: (b -> a) -> (a -> b) -> Variable a -> Variable b -> (Variable a, Variable b) rule2 getA getB (Variable as) (Variable bs) = (Variable $ map (liftM getA) bs, Variable $ map (liftM getB) as) -- rule3 :: ((a,b,c) -> (a,b,c)) -> rule3 :: (b -> c -> a) -> (c -> a -> b) -> (a -> b -> c) -> Variable a -> Variable b -> Variable c -> (Variable a, Variable b, Variable c) rule3 getA getB getC (Variable as) (Variable bs) (Variable cs) = (Variable $ zipWith (liftM2 getA) bs cs, Variable $ zipWith (liftM2 getB) cs as, Variable $ zipWith (liftM2 getC) as bs) {- | The following routine works only for finite lists, that is for a finite number of variable usages (e.g. finite number of equations. -} alternatives :: [Variable a] -> Variable a alternatives = Variable . scanl mplus Nothing . map msum . transpose . map listFromVariable -- Variable . (Nothing:) . map msum . transpose . map listFromVariable {- | Computing the value of a variable means finding the first time where the variable could be determined. -} solve :: Variable a -> a solve (Variable a) = head $ catMaybes a {- * Example rule generators -} equal :: (Num a) => Variable a -> Variable a -> (Variable a, Variable a) equal = rule2 id id -- | @a+b=c@ add :: (Num a) => Variable a -> Variable a -> Variable a -> (Variable a, Variable a, Variable a) add = rule3 subtract (-) (+) -- | @a*b=c@ times :: (Fractional a) => Variable a -> Variable a -> Variable a -> (Variable a, Variable a, Variable a) times = rule3 (flip (/)) (/) (*) {- * Example equation system -} {- | @ x=1 y=2 z=3 x+y=3 y*z=6 z=3 @ -} example :: (Double,Double,Double) example = let (x0,y0,_) = add x y (constant 3) (y1,z0,_) = times y z (constant 6) (z1,_) = equal z (constant 3) (x1,y2,_) = add x y (constant 3) -- duplicate rule x = alternatives [x0,x1] y = alternatives [y0,y1,y2] z = alternatives [z0,z1] in (solve x, solve y, solve z) {- | A variant of 'zipWith' which does not check for the end of lists and thus can generate infinite lists in a tied knot. -} zipWithInf :: (a -> b -> c) -> [a] -> [b] -> [c] zipWithInf f = let recurse ~(x:xs) ~(y:ys) = f x y : recurse xs ys in recurse {- | An infinite equation system. @ x0 = 0 x0+1 = x1 x1+1 = x2 x2+1 = x3 x3+1 = x4 ... @ In principle, infinitely many equations can be posed, but the solution slows down. That is, for computing @n@ variables you need about @n^2@ operations. Since per variable the number of iterations grows linearly we have a prefix of n @Nothing@s for the n-th variable. That is the space increases for later variables. -} exampleInf :: [Integer] exampleInf = let (x00,_) = equal (head xs) (constant 0) (_,xi0s,xi1s) = unzip3 $ zipWithInf (add (constant 1)) xs (tail xs) xs = zipWithInf (\xi0 xi1 -> alternatives [xi0,xi1]) xi0s (x00:xi1s) in map solve xs