Skip to main content
SpringerLink
Log in

Induce-statements and induce-expressions: Constructs for inductive programming

  • Conference paper
  • First Online:
Foundations of Software Technology and Theoretical Computer Science (FSTTCS 1993)

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

Abstract

A for-loop is somewhat similar to an inductive argument. Just as the truth of a proposition P(n+1) depends on the truth of P(n), the correctness of iteration n+1 of a for-loop depends on iteration n having been completed correctly.

This paper presents the induce-construct, a new programming construct based on the form of inductive arguments. It is more expressive than the for-loop yet less expressive than the while-loop. Like the for-loop, it is always terminating. Unlike the for-loop, it allows the convenient and concise expression of many algorithms. The for-loop traverses a set of consecutive natural numbers, the induce-construct generalizes to other data types.

The induce-construct is presented in two forms, one for imperative languages and one for functional languages. The expressive power of languages in which this is the only recursion construct is greater than primitive recursion, namely it is the multiply recursive functions in the first order case and the set of functions expressible in Gödel's system T in the general case.

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. Val Breazu-Tannen and Albert R. Meyer. Computable values can be classical. In Fourteenth ACM Symposium on Principles of Programming Languages, pages 238–243, 1987.

    Google Scholar 

  2. R.M. Burstall. Proving properties of programs by structural induction. The Computer Journal, 12:41–48, 1969.

    Google Scholar 

  3. R.M. Burstall. Inductively defined functions. In Mathematical Foundations of Software Development, pages 92–96. Number 185 in Lecture Notes in Computer Science, Springer Verlag, 1985.

    Google Scholar 

  4. R.M. Burstall. Inductively defined functions in functional programming languages. Journal of Computer and System Sciences, 34:409–421, 1987.

    Google Scholar 

  5. Robin Cockett and Tom Fukushima. About CHARITY. Unpublished draft, 1992.

    Google Scholar 

  6. Jean-Yves Girard. Proof Theory and Logical Complexity, Vol. 1. Number 1 in Studies in Proof Theory. Bibliopolis, 1987.

    Google Scholar 

  7. Eric C.R. Hehner. A practical theory of programming. Science of Computer Programming, 14:133–158, 1990.

    Google Scholar 

  8. Eric C.R. Hehner. A Practical Theory of Programming. Springer-Verlag, 1993.

    Google Scholar 

  9. C.A.R. Hoare. Recursive data types. International Journal of Computer and Information Science, 4:105–132, 1975.

    Google Scholar 

  10. Richard C. Holt, Philip A. Matthews, J. Allan Rosselet, and James R. Cordy. The Turing Programming Language: Design and Definition. Prentice Hall, 1988.

    Google Scholar 

  11. Andrew Malton. Functional Interpretation of Programming Methods. PhD thesis, University of Toronto, 1990.

    Google Scholar 

  12. Robert Mandl. On “PowerLoop” constructs in programming languages. SIGPLAN Notices, 25(4):73–82, 1990.

    Google Scholar 

  13. John McCarthy. Recursive functions of symbolic expressions and their computation by machine, part 1. Communications of the ACM, 3(4):184–195, 1963.

    Google Scholar 

  14. Lambert Meertens. Paramorphisms. Formal Aspects of Computing, 4(5):413–424, 1992.

    Google Scholar 

  15. Bengt Nordström, Kent Petersson, and Jan Smith. Programming in Martin-Löf's Type Theory. Clarendon Press, 1990.

    Google Scholar 

  16. Theodore S. Norvell and Eric C.R. Hehner. Logical specifications for functional programs. In R.S. Bird, C.C. Morgan, and J.C.P. Woodcock, editors, Mathematics of Program Construction, number 669 in LNCS, pages 269–290. Springer Verlag, 1993.

    Google Scholar 

  17. Rósa Péter. Konstruktion nichtrekursiver Funktionen. Mathematishe Annalen, 111:42–60, 1935.

    Google Scholar 

  18. Rósa Péter. Recursive Functions. Academic Press, 1967.

    Google Scholar 

  19. H. E. Rose. Subrecursion: Functions and Hierarchies. Number 9 in Oxford Logic Guides. Clarendon Press, 1984.

    Google Scholar 

  20. Philip Wadler. Theorems for free! In The Fourth International Conference on Functional Programming Languages and Computer Architecture. ACM Press, 1989.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, University of Toronto, Canada

    Theodore S. Norvell

Authors
  1. Theodore S. Norvell
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Rudrapatna K. Shyamasundar

Rights and permissions

Reprints and permissions

Copyright information

© 1993 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Norvell, T.S. (1993). Induce-statements and induce-expressions: Constructs for inductive programming. In: Shyamasundar, R.K. (eds) Foundations of Software Technology and Theoretical Computer Science. FSTTCS 1993. Lecture Notes in Computer Science, vol 761. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-57529-4_62

Download citation

  • DOI: https://doi.org/10.1007/3-540-57529-4_62

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-57529-0

  • Online ISBN: 978-3-540-48211-6

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation