Since it's my first post, hi all! I have been reading this for some days but only now i decided to write something. I am researching a to build a computer assisted simplification algorithm used to simplify pointfree expression.. Example. If i give the program: fst . snd . id . id it will return: fst . snd. it wil also show all steps it made to reach that goal. to do this we must have the laws (such as f. id = f) that help us doing this defined. the program uses a datatype such as: data ExpTree v c = Var v | Term c [ExpTree] exp :: Exp Char PF exp = Term Comp [Term Comp [Term Fst [], Term Comp [Term Snd [], Term Id []]], Term Id []] I have previously defined the catamorphism, hylo and anamorphism for this data type, so recursion is insured. I have also implemented a generic calculador that, given a list of functions will try to aply them and returns the best simplification aswell as the steps made to reach it. I am now trying to implement such functions in a "decent" way, but i am however interested in the theory behind all this. I am looking for algorithms that will help me efficiently simplify the expression to the fullest. I am also interested in knowing what zygomorphisms and paramorphisms are? and how can u build a gcata?? (a cata for all datatypes). I head about "proof-by-exhaustion" and "four color theorem" beeing used to make mathematical proves such as this ones, but i have never seen any example of such and would like to see it, if possible, in haskell.. If anyone can help me find what im looking for, a decent mathematical proofing algoritm.. or just tell me what it is that im looking for :P. or even contribute with any ideas, it would be very much aprecciated. :) TY, and Hi all :D :) and have fun coding haskell :) _________________________________________________________________ Don't just search. Find. Check out the new MSN Search! http://search.msn.click-url.com/go/onm00200636ave/direct/01/