[Haskell-cafe] Re: equations and patterns

Thanks all. I just found this list is very nice. Everybody are so friendly.

Regards,
Mingli

On 5/31/07, oleg@pobox.com  wrote:
>
>
> mingli yuan wrote:
> > Seems mathematic axioms and pattern matching are different things.
> > So how could I rewrite the equations to pattern matching? Which
> technique
> > should I learn?
>
> Haskell is more suitable for re-writing systems, which are based
> on oriented equations. The question of orientation is well-described,
> for example, in the book
>
>         Term Rewriting and All That
>         by Franz Baader, Tobias Nipkow
>         http://www4.in.tum.de/~nipkow/TRaAT/
>
> I should also point out Clean, where equations like associativity can
> be stated -- and even proven by Clean's built-in proof assistant.
>
> But something can be done in Haskell too. It is quite a general
> technique: free term algebra. It is explained in two excellent papers,
>
> John Hughes: The Design of a Pretty-printing Library
> http://citeseer.ist.psu.edu/hughes95design.html
>
> and
>
> Ralf Hinze: Deriving Backtracking Monad Transformers (ICFP2000)
> http://citeseer.ist.psu.edu/hinze00deriving.html
>
> The following Haskell98 code demonstrates the technique for your
> problem. Well, actually we take quite a similar problem: instead of
> lattices, we take rings -- or, to be precise, Num. They have two
> operations (+) and (*) which are too (usually taken to be)
> associative. This property is not stated in the Num class. Rather, it
> is described informally in comments. But we can deal with that property
> formally and directly.
>
> We introduce a free term algebra as follows
>
> > data FN = N Int | Add FN FN | Mul FN FN
> >         deriving (Eq,Show)
>
> and define an embedding of it in Haskell:
>
> > instance Num FN where
> >     fromInteger = N . fromInteger
> >     (+) = Add
> >     (*) = Mul
>
> So, we can write
>
> > test1 :: FN
> > test1  = (1 + 2) * 3 * 4 + 5
>
> and see the result
>         Add (Mul (Mul (Add (N 1) (N 2)) (N 3)) (N 4)) (N 5)
>
> Well, this doesn't actually do anything. It is a free term algebra
> after all. We need to give it a meaning, that is, define an
> observation function, or an interpreter
>
> > -- Interpreter (the observation function): big-step semantics
> > interp :: FN -> Int
> > interp (N x) = x
> > interp (Add x y) = interp x + interp y
> > interp (Mul x y) = interp x * interp y
>
> Now, evaluating "interp test1" gives 41.
>
> One may question the wisdom of this round-about way of adding and
> multiplying integers. Indeed, first we `compile' an arithmetic
> expression to the `byte-code'. Next, we wrote a byte-code interpreter,
> 'interp'. The benefit is that we can insert a `byte-code optimizer'
> before the interpretation. And here we may associate to the right
>
> > mul_right :: FN -> Maybe FN
> > mul_right (Mul (Mul a b) c) = Just (Mul a (Mul b c))
> > mul_right x = congruence mul_right x
>
> > test3 = closure mul_right test1
>
>   *FreeNum> test3
>   Add (Mul (Add (N 1) (N 2)) (Mul (N 3) (N 4))) (N 5)
>
> or to the left, distribute multiplication over addition
>
> > mul_add_distr (Mul a (Add b c)) = Just (Add (Mul a b) (Mul a c))
> > mul_add_distr (Mul (Add b c) a) = Just (Add (Mul b a) (Mul c a))
> > mul_add_distr x = congruence mul_add_distr x
>
> > test4 = closure mul_add_distr test1
>   *FreeNum> test4
>   Add (Add (Mul (Mul (N 1) (N 3)) (N 4)) (Mul (Mul (N 2) (N 3)) (N 4))) (N
> 5)
>
> or combine arbitrary number of steps
>
> > test5 = closure (compose mul_add_distr mul_right) test1
>
> *FreeNum> test5
> Add (Add (Mul (N 1) (Mul (N 3) (N 4))) (Mul (N 2) (Mul (N 3) (N 4)))) (N
> 5)
>
>
> Here's the complete code
>
> -- Haskell98!
>
> -- Free Term algebra for Nums
>
> module FreeNum where
>
> -- we'll use Ints as the base for simplicity
> data FN = N Int | Add FN FN | Mul FN FN
>           deriving (Eq,Show)
>
> instance Num FN where
>     fromInteger = N . fromInteger
>     (+) = Add
>     (*) = Mul
>
> test1 :: FN
> test1  = (1 + 2) * 3 * 4 + 5
>
> -- Interpreter (the observation function): big-step semantics
> interp :: FN -> Int
> interp (N x) = x
> interp (Add x y) = interp x + interp y
> interp (Mul x y) = interp x * interp y
>
> test2 = interp test1
>
> -- optimizer
>
> -- the driver: it applies an optimization step. If it succeeded, it
> applies
> -- again. Otherwise, we are finished.
> -- In other words, compute the transitive closure of the optimization step
>
> closure step term = maybe term (closure step) (step term)
>
>
> congruence step (N _) = Nothing
> congruence step (Add x y) = choose Add (x,step x) (y,step y)
> congruence step (Mul x y) = choose Mul (x,step x) (y,step y)
>
> -- Here's the benefit of laziness: we don't actually do step y
> -- if step x succeeded
> choose fn (_,Just x) (y,_)        = Just $ fn x y
> choose fn (x,Nothing) (_,Just y)  = Just $ fn x y
> choose fn (_,Nothing) (_,Nothing) = Nothing
>
>
> -- One step: associate Mul to the right
> -- (a `Mul` b) `Mul` c  ==> a `Mul` (b `Mul` c)
> -- or: (Mul (Mul a b) c) ==> (Mul a (Mul b c))
>
> mul_right :: FN -> Maybe FN
> mul_right (Mul (Mul a b) c) = Just (Mul a (Mul b c))
> mul_right x = congruence mul_right x
>
> -- do the opposite
> mul_left :: FN -> Maybe FN
> mul_left (Mul a (Mul b c)) = Just (Mul (Mul a b) c)
> mul_left x = congruence mul_left x
>
> test3 = closure mul_right test1
>
> -- Let us distribute multiplication over addition
> --  a * (b+c) => a*b + a*c
> -- (b+c) * a  => b*a + c*a
> mul_add_distr (Mul a (Add b c)) = Just (Add (Mul a b) (Mul a c))
> mul_add_distr (Mul (Add b c) a) = Just (Add (Mul b a) (Mul c a))
> mul_add_distr x = congruence mul_add_distr x
>
> test4 = closure mul_add_distr test1
>
> -- combine steps (it is mplus)
>
> compose step1 step2 x = maybe (step2 x) Just (step1 x)
>
> test5 = closure (compose mul_add_distr mul_right) test1
>
>
>