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.

  • $\begingroup$ Isn't that equation trivially solveable with $f=id$ and $h=g$? $\endgroup$ Aug 7, 2019 at 4:49
  • $\begingroup$ Sure. That will be one of the solutions. I am looking to generate all functions $f$ and $h$ for a given $g$ satisfying the equation. $\endgroup$ Aug 7, 2019 at 16:38


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.