Recursive Function Definition over Coinductive Types
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.
- 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
- Gunter, C. A. Semantics of Programming Languages: Structures and Techniques. Foundations of Computing Science. The MIT Press, 1992.Google Scholar
- Matthews, J., and Launchbury, J. Elementary microarchitecture algebra. To appear in CAV99, International Conference on Computer Aided Verification, July 1999.Google Scholar
- 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
- Miner, P. Hardware Verification Using Coinductive Assertions. PhD thesis, Indiana University, 1998.Google Scholar
- Müller, O., Nipkow, T., V. Oheimb, D., and Slotosch, O. HOLCF = HOL + LCF. To appear in Journal of Functional Programming, 1999.Google Scholar
- Paulson, L. Isabelle: A Generic Theorem Prover. Springer-Verlag, 1994.Google Scholar
- Rudin, W. Principles of Mathematical Analysis, 3 ed. McGraw-Hill, 1976.Google Scholar
- 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
- 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
- Tennent, R. D. Semantics of Programming Languages. Prentice Hall, New York, 1991.Google Scholar