Systematic Synthesis of Lambda-Terms
Abstract
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.
Full text