Abstract
We propose a new approach to programming by example, in which a program is synthesized from examples by higher-order unification in a type theory with a recursion operator. The approach, when applied to the problem of proof generalization, makes it possible to synthesize a general proof from a concrete example proof and establish a method of proving by example. Cases in which a program and a proof are simultaneously synthesized are also considered. In order to represent proofs as terms and generalize proof terms by higher-order unification, we extend Logical Framework to a system with product and equality.
Preview
Unable to display preview. Download preview PDF.
References
Angluin, D., Smith, C. H.: Inductive inference: Theory and methods, Computing Surveys, Vol.15, No.3 (1983), pp.237–269.
Biermann, A.: The inference of regular LISP programs from examples, IEEE Transactions on Systems, Man, and Cybernetics, Vol.8, No.8 (1978), pp.585–600.
DeJong G. F., Mooney, R.: Explanation-based learning: An alternative view, Machine Learning, Vol.1, No.2 (1986), pp.145–176.
Castaing, J., Kodratoff, Y., Degano P.: Theorem proving by the study of example proof traces or theorem proving by a correct theorem statement, Automatic Program Construction Techniques (Biermann, A. W., Guiho, G., Kodratoff, Y. eds.), 1984, pp.421–431.
Cohen, W. W.: Generalizing numbers and learning from multiple examples in explanation based learning, Proceedings of the Fifth International Conference on Machine Learning, 1988, pp.256–269.
Coquand, T., Huet, G.: The calculus of constructions, Information and Computation, Vol.76, No.3/4 (1988), pp.95–120.
Dietzen, S. R., Pfenning, F.: Higher-order and modal logic as a framework for explanation-based generalization, ERGO-89-076, School of Computer Science, Carnegie Mellon University, 1989.
Donat, M. R., Wallen, L. A.: Learning and applying generalized solutions, 9th International Conference on Automated Deduction, LNCS310 (1988), pp.41–60.
Elliott, C. M.: Higher-order unification with dependent function types, Rewriting Techniques and Applications (Dershowitz, N. ed.), LNCS355 (1989), pp.121–136.
Fay, M.: First-order unification in an equational theory, 4th Workshop on Automated Deduction, Austin, Texas, 1979, pp.161–167.
Gordon, M. J., Milner, A. J., Wadsworth, C. P.: Edinburgh LCF: A Mechanised Logic of Computation, LNCS78, Springer-Verlag, 1979.
Hagiya, M.: Generalization from partial parametrization in higher-order type theory, Theoretical Computer Science, Vol.63 (1989), pp.113–139.
Harper, R., Honsell, F., Plotkin, G.: A framework for defining logics, Symposium on Logic in Computer Science, 1987, pp.194–204.
Hayashi, S., Nakano, H.: PX: A computational logic, MIT Press, 1989.
Howard, W. A.: The formulae-as-types notion of construction, To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, (Hindley, J. R., Seldin, J. P. eds.), Academic Press (1980), pp.479–490.
Huet, G. P.: A unification algorithm for typed λ-calculus, Theoretical Computer Science, Vol.1 (1975), pp.27–57.
Huet, G., Lang, B.: Proving and applying program transformations expressed with second-order patterns, Acta Informatica, Vol.11 (1978), pp.31–55.
Hullot, J.-M.: Canonical forms and unification, 5th Conference on Automated Deduction, LNCS87 (1980), pp. 318–334.
Jouannaud, J.-P., Kodratoff, Y.: Characterization of a class of functions synthesized from examples by a Summers like method using the Boyer-Moore-Wegbreit matching technique, Proceedings of IJCAI 79, 1979, pp.440–447.
Kedar-Cabelli, S., McCarty, T.: Explanation-based generalization as resolution theorem proving, Proceedings of the Fourth International Workshop on Machine Learning, 1987, pp.383–389.
Kodratoff, Y.: A class of functions synthesized from a finite number of examples and a LISP program scheme, International Journal of Computer and Information Science, Vol.8, Nol.7 (1979), pp.489–521.
Krawchuk, B. J., Witten, I. H.: Problem solvers that learn, Proceedings of the Third Europe Working Session on Learning (Sleeman, D. ed.), 1988, pp.93–106.
Martin-Löf, P.: Constructive mathematics and computer programming, Sixth International Congress in Logic, Methodology and Philosophy of Science, 1982, pp.153–175
Mitchell, T. M., Keller, R., Kedar-Cabelli, S.: Explanation-based generalization: A unifying view, Machine Learning, Vol.1, No.1 (1986), pp.47–80.
Myers, B. A.: Visual programming, programming by example, and program visualization: A taxonomy, Proceedings of the ACM CHI'86 Conference on Human Factors in Computing Systems, 1986, pp.59–66.
Nadathur, G., Miller, D.: An overview of λPROLOG, Proceedings of the Fifth International Conference and Symposium on Logic Programming, 1988, pp.810–827.
Nix, R.: Editing by example, Proceedings of the 11th ACM Symposium on Principles of Programming Languages, 1984, pp.186–195.
Paulson, L. C.: Natural deduction as higher-order resolution, Journal of Logic Programming, Vol.3 (1986), pp.237–258.
Pfenning, F.: Elf: A language for logic definition and verified metaprogramming, Symposium on Logic in Computer Science, 1989, pp.313–322.
Shapiro, E. Y.: Algorithmic program diagnosis, Proceedings of the 9th ACM Symposium on Principles of Programming Languages, 1982, pp.299–308.
Shavlik, J. W., DeJong, G. F.: An explanation-based approach to generalizing number, Proceedings of IJCAI 87, 1987, pp.236–238.
Smith, D. R.: The synthesis of LISP programs from examples: A survey, Automatic Program Construction Techniques (Biermann, A. W., Guiho, G., Kodratoff, Y. eds.), 1984, pp.307–324.
Snyder, W., Gallier, J.: Higher-order unification revisited: Complete sets of transformations, Journal of Symbolic Computation, Vol.8, Nos 1&2 (1989), pp.101–140.
Summers, P.D.: A methodology for LISP program construction from examples, JACM, Vol.24, No.1 (1977), pp.161–175.
Waldinger, R.: Achieving several goals simultaneously, Machine Intelligence, Vol.8 (1977), pp.94–136.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1990 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Hagiya, M. (1990). Programming by example and proving by example using higher-order unification. In: Stickel, M.E. (eds) 10th International Conference on Automated Deduction. CADE 1990. Lecture Notes in Computer Science, vol 449. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-52885-7_116
Download citation
DOI: https://doi.org/10.1007/3-540-52885-7_116
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-52885-2
Online ISBN: 978-3-540-47171-4
eBook Packages: Springer Book Archive