Skip to main content
SpringerLink
Log in

Programming by example and proving by example using higher-order unification

  • Conference paper
  • First Online:
10th International Conference on Automated Deduction (CADE 1990)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 449))

Included in the following conference series:

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.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Angluin, D., Smith, C. H.: Inductive inference: Theory and methods, Computing Surveys, Vol.15, No.3 (1983), pp.237–269.

    Google Scholar 

  2. 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.

    Google Scholar 

  3. DeJong G. F., Mooney, R.: Explanation-based learning: An alternative view, Machine Learning, Vol.1, No.2 (1986), pp.145–176.

    Google Scholar 

  4. 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.

    Google Scholar 

  5. 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.

    Google Scholar 

  6. Coquand, T., Huet, G.: The calculus of constructions, Information and Computation, Vol.76, No.3/4 (1988), pp.95–120.

    Google Scholar 

  7. 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.

    Google Scholar 

  8. Donat, M. R., Wallen, L. A.: Learning and applying generalized solutions, 9th International Conference on Automated Deduction, LNCS310 (1988), pp.41–60.

    Google Scholar 

  9. Elliott, C. M.: Higher-order unification with dependent function types, Rewriting Techniques and Applications (Dershowitz, N. ed.), LNCS355 (1989), pp.121–136.

    Google Scholar 

  10. Fay, M.: First-order unification in an equational theory, 4th Workshop on Automated Deduction, Austin, Texas, 1979, pp.161–167.

    Google Scholar 

  11. Gordon, M. J., Milner, A. J., Wadsworth, C. P.: Edinburgh LCF: A Mechanised Logic of Computation, LNCS78, Springer-Verlag, 1979.

    Google Scholar 

  12. Hagiya, M.: Generalization from partial parametrization in higher-order type theory, Theoretical Computer Science, Vol.63 (1989), pp.113–139.

    Google Scholar 

  13. Harper, R., Honsell, F., Plotkin, G.: A framework for defining logics, Symposium on Logic in Computer Science, 1987, pp.194–204.

    Google Scholar 

  14. Hayashi, S., Nakano, H.: PX: A computational logic, MIT Press, 1989.

    Google Scholar 

  15. 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.

    Google Scholar 

  16. Huet, G. P.: A unification algorithm for typed λ-calculus, Theoretical Computer Science, Vol.1 (1975), pp.27–57.

    Google Scholar 

  17. Huet, G., Lang, B.: Proving and applying program transformations expressed with second-order patterns, Acta Informatica, Vol.11 (1978), pp.31–55.

    Google Scholar 

  18. Hullot, J.-M.: Canonical forms and unification, 5th Conference on Automated Deduction, LNCS87 (1980), pp. 318–334.

    Google Scholar 

  19. 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.

    Google Scholar 

  20. 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.

    Google Scholar 

  21. 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.

    Google Scholar 

  22. 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.

    Google Scholar 

  23. Martin-Löf, P.: Constructive mathematics and computer programming, Sixth International Congress in Logic, Methodology and Philosophy of Science, 1982, pp.153–175

    Google Scholar 

  24. Mitchell, T. M., Keller, R., Kedar-Cabelli, S.: Explanation-based generalization: A unifying view, Machine Learning, Vol.1, No.1 (1986), pp.47–80.

    Google Scholar 

  25. 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.

    Google Scholar 

  26. Nadathur, G., Miller, D.: An overview of λPROLOG, Proceedings of the Fifth International Conference and Symposium on Logic Programming, 1988, pp.810–827.

    Google Scholar 

  27. Nix, R.: Editing by example, Proceedings of the 11th ACM Symposium on Principles of Programming Languages, 1984, pp.186–195.

    Google Scholar 

  28. Paulson, L. C.: Natural deduction as higher-order resolution, Journal of Logic Programming, Vol.3 (1986), pp.237–258.

    Google Scholar 

  29. Pfenning, F.: Elf: A language for logic definition and verified metaprogramming, Symposium on Logic in Computer Science, 1989, pp.313–322.

    Google Scholar 

  30. Shapiro, E. Y.: Algorithmic program diagnosis, Proceedings of the 9th ACM Symposium on Principles of Programming Languages, 1982, pp.299–308.

    Google Scholar 

  31. Shavlik, J. W., DeJong, G. F.: An explanation-based approach to generalizing number, Proceedings of IJCAI 87, 1987, pp.236–238.

    Google Scholar 

  32. 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.

    Google Scholar 

  33. 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.

    Google Scholar 

  34. Summers, P.D.: A methodology for LISP program construction from examples, JACM, Vol.24, No.1 (1977), pp.161–175.

    Google Scholar 

  35. Waldinger, R.: Achieving several goals simultaneously, Machine Intelligence, Vol.8 (1977), pp.94–136.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Research Institute for Mathematical Sciences, Kyoto University, 606, Kitashirakawa Sakyo Kyoto, Japan

    Masami Hagiya

Authors
  1. Masami Hagiya
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Mark E. Stickel

Rights and permissions

Reprints 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

Publish with us

Policies and ethics

Search

Navigation