Toward automatic program synthesis

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.

REFERENCES

• 1: Ashcroft, E. A. Mathematical logic applied to the semantics of computer programs. Ph.D. Thesis, 1970, Imperial College, London.
• 2: Brice, C., and Derksen, J. A heuristically guided equality rule in a resolution theorem prover. Tech. Note 45, Stanford Res. Inst., Artificial Intelligence Group, Menlo Park, Calif.
• 3: Burstall, R. M. Proving properties of programs by structural induction. Comp. J. 12, 1 (1969), 41---48.
• 4: ----. Formal description of program structure and semantics in first-order logic. In Machine Intelligence 5, Meltzer and Michie, Eds., Edinburgh U. Press, Edinburgh, 1970, pp. 79-98.
• 5: Floyd, R. W. Assigning meaning to programs. In Proc. Symposia in Applied Mathematics, Vol. 19, American Mathematical Society, 1967, pp. 19-32.
• 6: Green, C. Application of theorem proving to problem solving. Proc. International Joint Conf. on Artificial Intelligence, Washington, D.C., 1969.
• 7: Claude Cordell Green, The application of theorem proving to question-answering systems, 1969
• 8: C. Cordell Green , Bertram Raphael, The use of theorem-proving techniques in question-answering systems, Proceedings of the 1968 23rd ACM national conference, p.169-181, August 27-29, 1968 [doi>10.1145/800186.810578]
• 9: Hayes, P. J. A machine-oriented formulation of the extended functional calculus. Memo 62, Stanford Artificial Intelligence Proj., Stanford U., Stanford, Calif., 1969. Also appeared as Metamathematics Unit Report, U. of Edinburgh, Scotland.
• 10: James Cornelius King, A program verifier, 1970
• 11: James C. King , Robert W. Floyd, An interpretation oriented theorem prover over integers, Proceedings of the second annual ACM symposium on Theory of computing, p.169-179, May 04-06, 1970, Northampton, Massachusetts, United States [doi>10.1145/800161.805162]
• 12: Luckham, D., and Nilsson, N. J. Extracting information from resolution proof trees. Tech. Note 32, Stanford Res. Inst., Artificial Intelligence Group, Menlo Park, Calif., 1970.
• 13: Manna, Z. The correctness of programs. J. Computer and System Sciences 3, 2, (1969), 119-127.
• 14: ----, and McCarthy, J. Properties of programs and partial function logic. In Machine Intelligence 5, Meltzer and Michie, Eds., Edinburgh U. Press, Edinburgh, 1970, pp. 79-98.
• 15: Zohar Manna , Amir Pnueli, Formalization of Properties of Functional Programs, Journal of the ACM (JACM), v.17 n.3, p.555-569, July 1970 [doi>10.1145/321592.321606]
• 16: McCarthy, J. Towards a mathematical science of computation. Proc. iviP Cong. 1962, North-Holland Pub. Co., Amsterdam.
• 17: ----. A Basis for a Mathematical Theory of Computation. In Computer Programming and Formal Systems, Braffort and Hirshberg, Eds., North Holland Pub. Co., Amsterdam, 1963.
• 18: ----. Predicate calculus with "undefined" as a truth-value. Memo 1, Stanford Artificial Intelligence Proj. Stanford U., 1963.
• 19: Elliott Mendelson, Introduction to mathematical logic (3rd ed.), Wadsworth Publ. Co., Belmont, CA, 1987
• 20: Morris, J. B. E-resolution: extension of resolution to include the equality relation. Proc. International Joint Conf. on Artificial Intelligence, Washington, D. C., 1969.
• 21: Park, D. Fixpoint induction and proofs of program properties. In Machine Intelligence 5. Meltzer and Michie, Eds., Edinburgh U. Press, Edinburgh, pp. 59-78.
• 22: Michael S. Paterson , Carl E. Hewitt, Comparative Schematology, Massachusetts Institute of Technology, Cambridge, MA, 1970
• 23: J. A. Robinson, A Machine-Oriented Logic Based on the Resolution Principle, Journal of the ACM (JACM), v.12 n.1, p.23-41, Jan. 1965 [doi>10.1145/321250.321253]
• 24: Scott, D. A type-theoretical alternative to CUCH, ISWlM, OWHY. Unpublished memo, 1969.
• 25: Herbert A. Simon, Experiments with a Heuristic Compiler, Journal of the ACM (JACM), v.10 n.4, p.493-506, Oct. 1963 [doi>10.1145/321186.321192]
• 26: James R. Slagle, Experiments with a deductive question-answering program, Communications of the ACM, v.8 n.12, p.792-798, Dec. 1965 [doi>10.1145/365691.365960]
• 27: H. R. Strong, Jr., Translating recursion equations into flow charts, Proceedings of the second annual ACM symposium on Theory of computing, p.184-197, May 04-06, 1970, Northampton, Massachusetts, United States [doi>10.1145/800161.805164]
• 28: Waldinger, R. J. Constructing programs automatically using theorem proving. Ph.D. Thesis, 1969, Carnegie-Mellon U., Pittsburgh, Pa.
• 29: ----, and Lee, R. C. T. PROW: a step toward automatic program writing. Proc. International Joint Conf. on Artificial Intelligence, Washington, D.C., 1969.

INDEX TERMS

Keywords:
answer extraction, artificial intelligence, automatic program synthesis, mathematical induction principle, problem solving, theorem proving