Automatic synthesis of typed Λ-programs on term algebras☆

摘要: Abstract The notion of iteratively defined functions from and to heterogeneous term algebras is introduced as the solution a finite set equations special shape. Such has remarkable consequences: (1) Choosing second-order typed lamdda-calculus (Λ for short) programming language enables one represent algebra elements iterative by automatic uniform synthesis paradigms, using neither conditional nor recursive constructs. (2) A completeness theorem Λ-terms with type degree at most two companion corollary Λ-programs have been proved. (3) new congruence relation last-mentioned which stronger than Λ-convertibility proved meaning Λ-program equivalence. Moreover, an extension paradigms higher complexity considered exemplified. All concepts are explained motivated examples over integers, list- tree-structures.