SYSTEMATIC SYNTHESIS OF -TERMS
Pieter Koopman, Rinus Plasmeijer · 2007
In this paper we show how to generate terms in the λ-calculus that match a given number of function argument result pairs. It appears that the number of λ-terms is too large to find terms reasonably fast based on the grammar of λ-calculus alone. By adding knowledge such as the desired number of arguments it is possible to synthesize λ-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.