[Haskell-cafe] Logic programming using lazy evaluation

[Henning Thielemann]

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