Automatic parallelization of recursive functions using quantifier elimination

Although the recent popularity of parallel-computing environments has called for parallel programs, it is difficult for nonspecialists to develop those that are efficient. What is required are parallelization methods that can automatically generate efficient parallel programs from sequential ones. In this paper, we propose an automatic method of parallelization for recursive functions. The key is a quantifier-eliminationbased derivation of an operator that shrinks function closures representing partial computations. Once we obtain such an operator, we can split the input structure and perform computation on each part in parallel. Our method has several features: it does not require any human help, it guarantees computational efficiency of generated programs, and it deals with complicated recursive functions such as those that are nonlinear recursive, non-self recursive, and accumulative.