Recursive Function Definition over Coinductive Types

  • John Matthews
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1690)


Using the notions of unique fixed point, converging equivalence relation, and contracting function, we generalize the technique of well-founded recursion. We are able to define functions in the Isabelle theorem prover that recursively call themselves an infinite number of times. In particular, we can easily define recursive functions that operate over coinductively-defined types, such as in finite lists. Previously in Isabelle such functions could only be defined corecursively, or had to operate over types containing “extra” bottom-elements. We conclude the paper by showing that the functions for filtering and flattening in finite lists have simple recursive definitions.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [1]
    Buskes, G., and van Rooij, A. Topological Spaces: from distance to neighborhood. UTM Series. Springer, New York, 1997.CrossRefzbMATHGoogle Scholar
  2. [2]
    Devillers, M., Griffioen, D., AND MüLLER, O. Possibly in finite sequences in theorem provers: A comparative study. In Theorem Proving in Higher Order Logics: 10th International Conference, TPHOLs’ 97 (Murray Hill, NJ, Aug. 1997), vol. 1275 of LNCS, Springer-Verlag, pp. 89–104.CrossRefGoogle Scholar
  3. [3]
    Gordon, M. J. C., and Melham, t. F. Introduction to HOL: A theorem proving environment for higher order logic. Cambridge University Press, 1993.Google Scholar
  4. [4]
    Gunter, C. A. Semantics of Programming Languages: Structures and Techniques. Foundations of Computing Science. The MIT Press, 1992.Google Scholar
  5. [5]
    Matthews, J., and Launchbury, J. Elementary microarchitecture algebra. To appear in CAV99, International Conference on Computer Aided Verification, July 1999.Google Scholar
  6. [6]
    Matthews, J., Launchbury, J., and Cook, B. Specifying microprocessors in Hawk. In IEEE International Conference on Computer Languages (Chicago, Illinois, May 1998), pp. 90–101.Google Scholar
  7. [7]
    Miner, P. Hardware Verification Using Coinductive Assertions. PhD thesis, Indiana University, 1998.Google Scholar
  8. [8]
    Müller, O., Nipkow, T., V. Oheimb, D., and Slotosch, O. HOLCF = HOL + LCF. To appear in Journal of Functional Programming, 1999.Google Scholar
  9. [9]
    Paulson, L. Isabelle: A Generic Theorem Prover. Springer-Verlag, 1994.Google Scholar
  10. [10]
    Paulson, L. C. Mechanizing coinduction and corecursion in higher-order logic. Journal of Logic and Computation 7,2 (Apr. 1997), 175–204.MathSciNetCrossRefzbMATHGoogle Scholar
  11. [11]
    Rudin, W. Principles of Mathematical Analysis, 3 ed. McGraw-Hill, 1976.Google Scholar
  12. [12]
    Rushby, J., and Stringer-calvert, D. W. J. A less elementary tutorial for the PVS specification and verification system. Tech. Rep. SRI-CSL-95-10, SRI International, Menlo Park, CA, June 1995. Revised, July 1996.Google Scholar
  13. [13]
    Slind, K. Function definition in higher order logic. In Ninth international Conference on Theorem Proving in Higher Order Logics TPHOL (Turku, Finland, Aug. 1996), J. Von Wright, J. Grundy, and J. Harrison, Eds., vol. 1125 of Lecture Notes in Computer Science, Springer Verlag, pp. 381–398.CrossRefGoogle Scholar
  14. [14]
    Slind, K. Derivation and use of induction schemes in higher-order logic. Lecture Notes in Computer Science 1275 (1997), 275–290.MathSciNetCrossRefGoogle Scholar
  15. [15]
    Tennent, R. D. Semantics of Programming Languages. Prentice Hall, New York, 1991.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1999

Authors and Affiliations

  • John Matthews
    • 1
  1. 1.Oregon Graduate InstitutePortland ORUSA

Personalised recommendations