Thumbnail
Access Restriction
Subscribed

Author Waldinger, Richard J. ♦ Manna, Zohar
Source ACM Digital Library
Content type Text
Publisher Association for Computing Machinery (ACM)
File Format PDF
Language English
Subject Keyword Automatic program synthesis ♦ Mathematical induction principle ♦ Theorem proving ♦ Problem solving ♦ Artificial intelligence ♦ Answer extraction
Abstract An elementary outline of the theorem-proving approach to automatic program synthesis is given, without dwelling on technical details. The method is illustrated by the automatic construction of both recursive and iterative programs operating on natural numbers, lists, and trees.In order to construct a program satisfying certain specifications, a theorem induced by those specifications is proved, and the desired program is extracted from the proof. The same technique is applied to transform recursively defined functions into iterative programs, frequently with a major gain in efficiency.It is emphasized that in order to construct a program with loops or with recursion, the principle of mathematical induction must be applied. The relation between the version of the induction rule used and the form of the program constructed is explored in some detail.
Description Affiliation: Stanford Univ., CA (Manna, Zohar) || Stanford Research Institute, Menlo Park, CA (Waldinger, Richard J.)
Age Range 18 to 22 years ♦ above 22 year
Educational Use Research
Education Level UG and PG
Learning Resource Type Article
Publisher Date 2005-08-01
Publisher Place New York
Journal Communications of the ACM (CACM)
Volume Number 14
Issue Number 3
Page Count 15
Starting Page 151
Ending Page 165


Open content in new tab

   Open content in new tab
Source: ACM Digital Library