Folding of finite program terms to recursive program schemes

摘要

We present an approach to inductive synthesis of functional programs based on the detection of recurrence relations. A given term is considered as the κth unfolding of an unknown recursive program. If a recurrence relations call be identified in the term, it can be folded into a recursive program which (a) can reproduce the term and (b) generalizes over it. Our approach goes beyond Summers' classical approach in several aspects: It is language independent and works for terms belonging to an arbitrary term algebra; it allows induction of sets of recursive equations which are in some arbitrary calls' relation; induced equations can be dependent on more than one input parameters and we can detect interdependencies of variable substitutions in recursive calls; the given input terms can represent incomplete unfolding of an hypothetical recursive program.