Automatic synthesis of typed \(\Lambda\)-programs on term algebras (Q1079357): Difference between revisions
From MaRDI portal
Set OpenAlex properties. |
ReferenceBot (talk | contribs) Changed an Item |
||
Property / cites work | |||
Property / cites work: Programs as proofs: A synopsis / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: The Expressiveness of Simple and Second-Order Type Structures / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: ÜBER EINE BISHER NOCH NICHT BENÜTZTE ERWEITERUNG DES FINITEN STANDPUNKTES / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q4068054 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q4172911 / rank | |||
Normal rank |
Latest revision as of 15:16, 17 June 2024
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | Automatic synthesis of typed \(\Lambda\)-programs on term algebras |
scientific article |
Statements
Automatic synthesis of typed \(\Lambda\)-programs on term algebras (English)
0 references
1985
0 references
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.
0 references
automatic synthesis of programs
0 references
data system
0 references
finitary term algebra
0 references
data structures
0 references
Iterative functions
0 references
primitive recursive functions
0 references
second- order typed lambda-calculus
0 references
completeness theorem
0 references
equivalence of programs
0 references