Proof Methods for Corecursive Programs

• Autorzy: Gibbons J. , Hutton G.
• Języki publikacji: EN

Abstrakty

EN

Recursion is a well-known and powerful programming technique, with a wide variety of applications. The dual technique of corecursion is less well-known, but is increasingly proving to be just as useful. This article is a tutorial on the four main methods for proving properties of corecursive programs: fixpoint induction, the approximation (or take) lemma, coinduction, and fusion.

Słowa kluczowe

EN

recursion theory; symbolic; mathematical logic; computer programming; approximation theory; recursive programming

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2005
• Tom: Vol. 66, nr 4
• Strony: 353--366
• Opis fizyczny: Bibliogr. 40 poz.

Twórcy

autor

Gibbons J.

• Oxford University Computing Laboratory, UK

autor

Hutton G.

• School of Computer Science and IT University of Nottingham, UK

Bibliografia

• [1] Aczel, P.: Non-Well-Founded Sets, Number 14 in CSLI Lecture Notes, Stanford: CSLI Publications, 1988.
• [2] de Bakker, J.: Mathematical Theory of Program Correctness, Prentice-Hall, 1980.
• [3] Bartels, F.: Generalised Coinduction, Mathematical Structures in Computer Science, 13, 2003, 321–348.
• [4] Barwise, J., Moss, L.: Vicious Circles: On the Mathematics of Non-Wellfounded Phenomena, Number 60 in CSLI Lecture Notes, Stanford: CSLI Publications, 1996.
• [5] Bird, R.: Introduction to Functional Programming using Haskell (second edition), Prentice Hall, 1998.
• [6] Bird, R., de Moor, O.: Algebra of Programming, Prentice Hall, 1997.
• [7] Bird, R., Wadler, P.: An Introduction to Functional Programming, Prentice Hall, 1988.
• [8] Burge,W.: Recursive Programming Techniques, Addison-Wesley, 1975.
• [9] Coquand, T.: Infinite Objects in Type Theory, in: Types for Proofs and Programs (H. Barendregt, T. Nipkow, Eds.), vol. 806 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, 1994, 62–78.
• [10] Danielsson, N., Jansson, P.: Chasing Bottoms: A Case Study in Program Verification in the Presence of Partial and Infinite Values, in: Proceedings of the 7th International Conference on Mathematics of Program Construction, vol. 3125 of Lecture Notes in Computer Science, Springer, Stirling, Scotland, July 2004.
• [11] Davey, B., Priestley, H.: Introduction to Lattices and Order, Cambridge University Press, 1990.
• [12] Fokkinga, M. M., Meijer, E.: Program Calculation Properties of Continuous Algebras, Technical Report CS–R9104, CWI, Amsterdam, January 1991, Available online at http://www.home.cs.utwente.nl/~fokkinga/#detail_0000003528.
• [13] Ghani, N., Luth, C., de Marchi, F., Power, J.: Algebras, Coalgebras,Monads and Comonads, in: Proceedings of the 4th International Workshop on Coalgebraic Methods in Computer Science, number 44.1 in Electronic Notes in Theoretical Computer Science, Elsevier Science, April 2001.
• [14] Ghani, N., Uustalu, T., Vene, V.: Build, Augment, Destroy. Universally, Proceedings of Programming Languages and Systems: Second Asian Symposium, LNCS 3302, Springer Verlag, 2004.
• [15] Gibbons, J.: Calculating Functional Programs, in: Algebraic and Coalgebraic Methods in the Mathematics of Program Construction, vol. 2297 of Lecture Notes in Computer Science, Springer-Verlag, January 2002, 148–203.
• [16] Gibbons, J., Hutton, G., Altenkirch, T.: When is a Function a Fold or an Unfold?, in: Proceedings of the 4th International Workshop on Coalgebraic Methods in Computer Science, number 44.1 in Electronic Notes in Theoretical Computer Science, Elsevier Science, April 2001.
• [17] Gibbons, J., Jones, G.: The Under-Appreciated Unfold, in: Proceedings of the Third ACM SIGPLAN International Conference on Functional Programming, Baltimore, Maryland, September 1998, 273–279.
• [18] Gordon, A.: A Tutorial on Co-induction and Functional Programming, in: Proceedings of the 1994 Glasgow Workshop on Functional Programming, SpringerWorkshops in Computing, 1995, 78–95.
• [19] Gordon, A.: Bisimilarity as a Theory of Functional Programming, BRICS Notes Series NS-95-3, Aarhus University, 1995.
• [20] Gumm, H. P., Ed.: Proceedings of the Sixth International Workshop on Coalgebraic Methods in Computer Science, Elsevier Science, 2003, Electronic Notes in Theoretical Computer Science Volume 82.1.
• [21] Hutton, G., Gibbons, J.: The Generic Approximation Lemma, Information Processing Letters, 79(4), August 2001, 197–201.
• [22] Jacobs, B., Rutten, J.: A Tutorial on (Co)Algebras and (Co)Induction, Bulletin of the European Association for Theoretical Computer Science, 62, 1997, 222–259.
• [23] Johann, P.: Short Cut Fusion is Correct, Journal of Functional Programming, 13(4), 2003, 797–814.
• [24] Lassen, S.: Relational Reasoning About Contexts, in: Higher Order Operational Techniques in Semantics (A. Gordon, A. Pitts, Eds.), Cambridge University Press, 1998, 91–135.
• [25] Malcolm, G.: Algebraic Data Types and Program Transformation, Science of Computer Programming, 14(2-3), September 1990, 255–280.
• [26] Manna, Z., Ness, S., Vuillemin, J.: Inductive Methods for Proving Properties of Programs, Communications of the ACM, 16(8), August 1973, 491–502.
• [27] Moss, L., Ed.: Proceedings of the Fifth International Workshop on Coalgebraic Methods in Computer Science, Elsevier Science, 2002, Electronic Notes in Theoretical Computer Science Volume 65.1.
• [28] Moss, L., Danner, N.: On the Foundations of Corecursion, Logic Journal of the Interest Group in Pure and Applied Logics, 5(2), 1997, 231–257.
• [29] Park, D.: Fixpoint Induction and Proofs of Program Properties, Machine Intelligence, 5, 1969, 59–78.
• [30] Paulson, L.: Mechanizing Coinduction and Corecursion in Higher-Order Logic, Journal of Logic and Computation, 7, 1997, 175–204.
• [31] Pavlovic, D.: Guarded Induction on Final Coalgebras, in: Coalgebraic Methods in Computer Science (B. Jacobs, L. Moss, H. Reichel, J. Rutten, Eds.), number 11 in Electronic Notes in Theoretical Computer Science, Elsevier, 2000.
• [32] Peyton Jones, S.: Haskell 98 Language and Libraries: The Revised Report, Cambridge University Press, 2003.
• [33] Pitts, A. M.: Parametric Polymorphism and Operational Equivalence, Mathematical Structures in Computer Science, 10, 2000, 321–359.
• [34] Reynolds, J. C.: Theories of Programming Languages, Cambridge University Press, 1998.
• [35] Sands, D.: Computing with Contexts: A Simple Approach, in: Second Workshop on Higher-Order Operational Techniques in Semantics (HOOTS II) (A. D. Gordon, A. M. Pitts, C. L. Talcott, Eds.), vol. 10 of Electronic Notes in Theoretical Computer Science, Elsevier Science Publishers B.V., 1998.
• [36] Sands, D.: ImprovementTheory and Its Applications, in: Higher Order Operational Techniques in Semantics (A. Gordon, A. Pitts, Eds.), Cambridge University Press, 1998, 275–306.
• [37] Sangiorgi, D.: On the Bisimulation Proof Method, Mathematical Structures in Computer Science, 8, 1998, 447–479.
• [38] Schmidt, D. A.: Denotational Semantics: A Methodology for Language Development, Allyn and Bacon, Inc., 1986.
• [39] Smyth, M. B., Plotkin, G. D.: The Category-Theoretic Solution of Recursive Domain Equations, SIAM Journal on Computing, 11(4), November 1982, 761–783.
• [40] Turner, D. A.: Elementary Strong Functional Programming, in: Proceedings of the First International Symposium on Functional Programming Languages in Education, vol. 1022 of Lecture Notes in Computer Science, Springer-Verlag, 1995, 1–13.