I am fairly new at program synthesis and the use of SMT solvers for this purpose. Given a function g, I want to generate all the functions f and h such that the following holds:
f . g = h . f
Are there program synthesis tools and techniques that would allow me to search the program space for these functions?
I am assuming the search space is going to be extremely large for general programming languages like Haskell. How should one go about pruning the search space: would one have to drastically reduce the search space by defining a small language and performing the search over this language? It seems that the type constraints of the above equation would also help in pruning the search space. Any observations or pointer to tools, papers, or presentations would be appreciated.