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

#### 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.
##### Scheda breve Scheda completa Scheda completa (DC)
1985
Berarducci, Alessandro; Bohm, C.
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: `https://hdl.handle.net/11568/7450`
##### Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

• ND
• 170
• 117