Application of computer science ideas to the presentation of mathematical theorems and proofs

ABSTRACT

Based on the analogy between mathematical proofs and computer programs this paper illustrates how it is possible to apply methodologies from computer science, used in the development and presentation of computer programs, for the presentation of mathematical theorems and proofs. The following three methodologies are discussed: stepwise refinement, abstraction, and program verification.

REFERENCES

• 1: Harold Abelson , Gerald J. Sussman, Structure and Interpretation of Computer Programs, MIT Press, Cambridge, MA, 1996
• 2: Avital, S. M. (1973). The 'Let us define a function' syndrome. International Journal of Mathematics Education in Science and Technology4, pp. 143--147.
• 3: Richard A. De Millo , Richard J. Lipton , Alan J. Perlis, Social processes and proofs of theorems and programs, Communications of the ACM, v.22 n.5, p.271-280, May 1979 [doi>10.1145/359104.359106]
• 4: Dijkstra, E. W. (1972). Notes on structured programming. In Dahl, O. J., Hoare, C. A. R. and Dijkstra, E. W. (eds.). Structured Programming, Academic Press, New-York.
• 5: Dijkstra, E.W. (1986). On a cultural gap. The Mathematical Intelligencer8(1), pp. 48--52.
• 6: Dijkstra, E.W. (1989). A somewhat open letter to Uri Leron -- EWD1049. Unpublished personal correspondence.
• 7: Gray, R. (1991). Computer Programs and Mathematical Proofs. The Mathematical Intelligencer13(4), pp. 45--48.
• 8: David Gries, The Science of Programming, Springer-Verlag New York, Inc., Secaucus, NJ, 1987
• 9: Halmos, P. R. (1973). How to write mathematics. In Steenrod, N. E., Halmos, P. R., Schiffer, M. M. and Dieudonne, J. A. How to Write Mathematics?, American Mathematical Society.
• 10: Hoare, C. A. R. (1986). Mathematics of programming. Byte, August, pp. 115--124, 148--150.
• 11: Honsberger, R. (1985). Mathematical Games III. The Mathematical Association of America.
• 12: Knuth, D. E. (1974). Computer science and its relation to mathematics. The American Mathematical Monthly, 81 (April), pp. 323--343.
• 13: Lakatos, I. (1976). Proofs and Refutations. Cambridge: Cambridge University Press.
• 14: Leron, U. (1983). Structuring mathematical proofs. American Mathematical Monthly, 90(3), pp. 174--185.
• 15: Leron, U. (1985). Heuristic presentations: The role of structuring. For the Learning of Mathematics5(3), pp. 7--13.
• 16: P. Martin-Löf, Constructive mathematics and computer programming, Proc. of a discussion meeting of the Royal Society of London on Mathematical logic and programming languages, p.167-184, June 1985, London, United Kingdom
• 17: Mizler, D. (1968). Calculus, Ha'omanim Press, Jerusalem. (Hebrew).
• 18: Steenrod, N. E. (1973). How to write mathematics. In Steenrod, N. E., Halmos, P. R., Schiffer, M. M. and Dieudonne, J. A. How to Write Mathematics?, American Mathematical Society.
• 19: Wells, C. (1995). Communicating mathematics: Useful ideas from computer science. The American Mathematical Monthly102(5), pp. 397--408.
• 20: Niklaus Wirth, Program development by stepwise refinement, Communications of the ACM, v.14 n.4, p.221-227, April 1971 [doi>10.1145/362575.362577]