Systems such as λ2 have special built-in axioms for particular functions that greatly aid their synthesis search (for example, the axiom that map g . map f == map (g . f)). It may be possible to encode these rules as special "introduction forms" for these functions so that examples can be refined according to these axioms, speeding up the synthesis procedure for functions that rely on these general-purpose combinators by taking work done by raw term enumeration (which is just "guessing") and giving it to type-and-example-directed refinement.
Systems such as λ2 have special built-in axioms for particular functions that greatly aid their synthesis search (for example, the axiom that
map g . map f == map (g . f)). It may be possible to encode these rules as special "introduction forms" for these functions so that examples can be refined according to these axioms, speeding up the synthesis procedure for functions that rely on these general-purpose combinators by taking work done by raw term enumeration (which is just "guessing") and giving it to type-and-example-directed refinement.