Re: [Haskell-cafe] Logic programming using lazy evaluation
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,
Re: [Haskell-cafe] Logic programming using lazy evaluation
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. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Logic programming using lazy evaluation
On 2/27/07, Henning Thielemann [EMAIL PROTECTED] 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 / Ulf ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Logic programming using lazy evaluation
On Tue, 27 Feb 2007, Ulf Norell wrote: On 2/27/07, Henning Thielemann [EMAIL PROTECTED] 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. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Logic programming using lazy evaluation
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. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
