Skip to main content
SpringerLink
Log in

From programming-by-example to proving-by-example

  • Invited Paper
  • Conference paper
  • First Online:
Theoretical Aspects of Computer Software (TACS 1991)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 526))

Included in the following conference series:

Abstract

In the machine learning community, it is widely recognized that there are two fundamentally different approaches to learning: inductive learning and deductive learning. This paper formalizes both of the approaches to learning under a uniform framework of type theory and investigates the use of higher-order unification to solve learning problems in both.

I first introduce the simply typed λ-calculus with inductive definitions and give a unification procedure for the calculus. I then formalize a problem of programming-by-example (i.e., inductive learning) as a system of equations in the calculus and reformulate existing methods for programming-by-example as restricted versions of the unification procedure.

It is a new attempt to formalize a problem of proving-by-example (i.e., deductive learning) as an equation in a typed λ-calculus. For that purpose, I extend LF with inductive definitions and consider a unification procedure for it.

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.

    Article  Google Scholar 

  2. Barendregt, H.: Introduction to generalized type systems, Theoretical Computer Science — Proceedings of the Third Italian Conference, World Scientific, 1989, pp.1–37.

    Google Scholar 

  3. Dybjer, P.: An inversion principle for Martin-Löf's type theory, Proceedings of the Workshop on Programming Logic, PMG-R54, University of Göteborg and Chalmers University of Technology, 1989, pp.177–188.

    Google Scholar 

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

    Google Scholar 

  5. Elliott, C. M.: Some extensions and applications of higher-order unification, Ph.D Thesis, School of Computer Science, Carnegie Mellon University, 1990.

    Google Scholar 

  6. Ellman, T.: Explanation-based learning: A survey of programs and perspectives, ACM Computing Surveys, Vol.21, No.2 (1989), pp.163–221.

    Google Scholar 

  7. Hagiya, M.: Programming by example and proving by example using higher-order unification, 10th International Conference on Automated Deduction, LNAI449 (1990), pp.588–602.

    Google Scholar 

  8. Hagiya, M.: Synthesis of rewrite programs by higher-order and semantic unification, Proceedings of the First International Workshop on Algorithmic Learning Theory (1990), pp.396–410. Also in New Generation Computing, Vol.8, No.4 (1991), pp.403–420.

    Google Scholar 

  9. Hagiya, M.: On reduction and projection in type theory with inductive definitions, in preparation.

    Google Scholar 

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

    Google Scholar 

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

    Article  Google Scholar 

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

    Article  Google Scholar 

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

  14. Ling, X.: Inventing theoretical terms in inductive learning of functions — search and constructive methods, Methodologies for Intelligent Systems (Ras, Z. W. ed.), Vol.4 (1989), pp.332–341.

    Google Scholar 

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

    Google Scholar 

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

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

    Google Scholar 

  18. Van Harmelen, F., Bundy, A.: Explanation-based generalization = partial evaluation, Artificial Intelligence, Vol.36 (1988), pp.401–412.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. RIMS, Kyoto University, 606-01, Kyoto, Japan

    Masami Hagiya

Authors
  1. Masami Hagiya
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Takayasu Ito Albert R. Meyer

Rights and permissions

Reprints and permissions

Copyright information

© 1991 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Hagiya, M. (1991). From programming-by-example to proving-by-example. In: Ito, T., Meyer, A.R. (eds) Theoretical Aspects of Computer Software. TACS 1991. Lecture Notes in Computer Science, vol 526. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-54415-1_56

Download citation

  • DOI: https://doi.org/10.1007/3-540-54415-1_56

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-54415-9

  • Online ISBN: 978-3-540-47617-7

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation