Automatic synthesis of typed \(\Lambda\)-programs on term algebras (Q1079357)

A data system is a finitary term algebra with ''parametric'' and/or ''proper'' carrier sets (data structures). Iterative functions are generalizations of primitive recursive functions to arbitrary data systems. An automatic method for representing data structures, elements of data structures, basic operations on data structures and, finally, iterative functions, in second-order typed lambda-calculus (\(\Lambda)\) is proposed. A completeness theorem for \(\Lambda\)-terms (with degree at most two) is proved and a new congruence relation ''\(\simeq ''\) between \(\Lambda\)-programs is defined (such that \(\simeq\) extends \(\Lambda\)- convertibility). For short, this is an elegant automatic synthesis method, and at the same time a system of notation for data structures and a frame for proving equivalence of programs without using structural induction on input. Open problems and possible generalizations are discussed and many examples are provided.