Systematic Synthesis of Lambda-Terms
In this paper we show how to generate terms in the lambda-calculus that match a given number of function argument result pairs. It appears that the number of lambda-terms is too large to find terms reasonably fast based on the grammar of lambda-calculus alone. By adding knowledge such as the desired number of arguments it is possible to synthesize lambda-terms effectively for some interesting examples. This yields surprising terms that are unlikely to be found by a human.
An interesting subproblem is the determination of suitability of candidate terms based on equivalence of terms. We used an approximation of equivalence by a finite number of reduction steps. This implies that the test for equivalence can also yield the value undefined. Fortunately the test system used is able to handle undefined test results.