Automatic synthesis of typed \(\Lambda\)-programs on term algebras
type: Item
instance of: scholarly article
title: Automatic synthesis of typed \(\Lambda\)-programs on term algebras
zbMATH Open document ID: 0597.68017
DOI: 10.1016/0304-3975(85)90135-5
author: Alessandro Berarducci
author: Corrado Böhm
published in: Theoretical Computer Science
publication date: 1985-01-01T00:00:00Z
review text: 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.
Mathematics Subject Classification ID: 68N01
Mathematics Subject Classification ID: 03B40
Mathematics Subject Classification ID: 03D20
Mathematics Subject Classification ID: 08B20
zbMATH DE Number: 3963173
zbMATH Keywords: automatic synthesis of programs
zbMATH Keywords: data system
zbMATH Keywords: finitary term algebra
zbMATH Keywords: data structures
zbMATH Keywords: Iterative functions
zbMATH Keywords: primitive recursive functions
zbMATH Keywords: second- order typed lambda-calculus
zbMATH Keywords: completeness theorem
zbMATH Keywords: equivalence of programs
reviewed by: Cristian Masalagiu
MaRDI profile type: Publication
full work available at URL: 0304-3975(85)90135-5
OpenAlex ID: W1513579486
cites work: Programs as proofs: A synopsis
cites work: The Expressiveness of Simple and Second-Order Type Structures
cites work: ÜBER EINE BISHER NOCH NICHT BENÜTZTE ERWEITERUNG DES FINITEN STANDPUNKTES
cites work: Q4068054
cites work: Q4172911
description: scientific article; zbMATH DE number 3963173