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