The notion of iteratively defined functions from and to heterogeneous term algebras is introduced as the solution of a finite set of equations of a special shape. Such a notion has remarkable consequences: (1) Choosing the second-order typed lambda- calculus (Lambsa for short) as a programming language enables one to represent algebra elements and iterative functions by automatic uniform synthesis paradigms, using neither conditional nor recursive constructs. (2) A completeness theorem for Lambda-terms with type of degree at most two and a companion corollary for Lambda-programs have been proved. (3) A new congruence relation for the last-mentioned Lambda-terms which is stronger than Lambda-convertibility is introduced and proved to have the meaning of a Lambda-program equivalence. Moreover, an extension of the paradigms to the synthesis of functions of higher complexity is considered and exemplified. All the concepts are explained and motivated by examples over integers, list- and tree-structures.
Automatic Synthesis of Typed Lambda-Programs on Term Algebras
BERARDUCCI, ALESSANDRO;
1985-01-01
Abstract
The notion of iteratively defined functions from and to heterogeneous term algebras is introduced as the solution of a finite set of equations of a special shape. Such a notion has remarkable consequences: (1) Choosing the second-order typed lambda- calculus (Lambsa for short) as a programming language enables one to represent algebra elements and iterative functions by automatic uniform synthesis paradigms, using neither conditional nor recursive constructs. (2) A completeness theorem for Lambda-terms with type of degree at most two and a companion corollary for Lambda-programs have been proved. (3) A new congruence relation for the last-mentioned Lambda-terms which is stronger than Lambda-convertibility is introduced and proved to have the meaning of a Lambda-program equivalence. Moreover, an extension of the paradigms to the synthesis of functions of higher complexity is considered and exemplified. All the concepts are explained and motivated by examples over integers, list- and tree-structures.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
