[Haskell-cafe] point-free simplification algoritm.

[Nuno Pinto]

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/