# [Haskell-cafe] point-free simplification algoritm.

Nuno Pinto nuno at hotmail.co.uk
Tue Jan 31 14:54:37 EST 2006

```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/

```