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$ – jmite Aug 7 '19 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$ – user5803465 Aug 7 '19 at 16:38

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.