Programming with variable functions

ABSTRACT

What is a good method to specify and derive imperative programs? This paper argues that a new form of functional programming fits the bill: where variable functions can be updated at specified points in their domain.Traditional algebraic specification and functional programming are a powerful pair of tools for specifying and implementing domains of discourse and operations on them. Recent work on evolving algebras has introduced the function update in algebraic specifications, and has applied it with good success in the modelling of reactive systems. We show that similar concepts allow one to derive efficient programs in a systematic way from functional specifications. The final outcome of such a derivation can be made as efficient as a traditional imperative program with pointers, but can still be reasoned about at a high level.Variable functions can also play an important role in the structuring of large systems. They can subsume object-oriented programming languages, without incurring the latter's problems with pointer aliasing and modularity.

REFERENCES

• AP94: P. Achten and R. Plasmeijer. Towards distributed interactive programs in the functional programming language Clean. In J. Glauert, editor, Proceedings of the 6th International Workshop on the Implementation of Funtional Languages, pages 28.1- 28.16. University of East Anglia, Norwich, UK, 1994.
• Bak92: Henry G. Baker, Lively linear Lisp: “look ma, no garbage!”, ACM SIGPLAN Notices, v.27 n.8, p.89-98, Aug. 1992 [doi>10.1145/142137.142162]
• BBD+96: Christoph Beierle , Egon Börger , Igor Durdanovic , Uwe Glässer , Elvinia Riccobene, Refining Abstract Machine Specifications of the Steam Boiler Control to Well Documented Executable Code, Formal Methods for Industrial Applications, Specifying and Programming the Steam Boiler Control (the book grow out of a Dagstuhl Seminar, June 1995)., p.52-78, January 1996
• Bij89: A. Bijlsma, Calculating with pointers, Science of Computer Programming, v.12 n.3, p.191-205, Sept. 1989 [doi>10.1016/0167-6423(89)90002-6]
• BR94: Egon D. BSrger and Dean Rosenzweig. A mathematical definition of full Prolog. Science of Computer Programming, 1994.
• BS94: Egon Börger , Rosario F. Salamone, CLAM specification for provably correct compilation of CLP( R ) programs, Specification and validation methods, Oxford University Press, Inc., New York, NY, 1995
• Bur72: R.M. Burstall. Some techniques for proving correctness of programs which alter data structures. In B. Meltzer and D. Michie, editors, Machine Intelligence 7, pages 23-50. Edinburgh University Press, 1972.
• Bur82: Warren Burton. An efficient functional implementation of FIFO queues. Information Processing Letters, 14:205-206, 1982.
• CF91: Erik Crank , Matthias Felleisen, Parameter-passing and the lambda calculus, Proceedings of the 18th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.233-244, January 21-23, 1991, Orlando, Florida, United States [doi>10.1145/99583.99616]
• CH97: Chih-Ping Chen , Paul Hudak, Rolling your own mutable ADT—a connection between linear types and monads, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.54-66, January 15-17, 1997, Paris, France [doi>10.1145/263699.263708]
• Dij76: Edsger Wybe Dijkstra, A Discipline of Programming, Prentice Hall PTR, Upper Saddle River, NJ, 1997
• GH93: Yuri Gurevich , James K. Huggins, The Semantics of the C Programming Language, Selected Papers from the Workshop on Computer Science Logic, p.274-308, September 28-October 02, 1992
• GHJV94: Erich Gamma , Richard Helm , Ralph Johnson , John Vlissides, Design patterns: elements of reusable object-oriented software, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1995
• Gir87: Jean-Yves Girard, Linear logic, Theoretical Computer Science, v.50 n.1, p.1-102, Jan. 30, 1987 [doi>10.1016/0304-3975(87)90045-4]
• Gur95: Yuri Gurevich, Evolving algebras 1993: Lipari guide, Specification and validation methods, Oxford University Press, Inc., New York, NY, 1995
• Har79: David Harel, First-Order Dynamic Logic, Springer-Verlag New York, Inc., Secaucus, NJ, 1979
• HJ89: C. A. R. Hoare , C. B. Jones, Essays in computing science, Prentice-Hall, Inc., Upper Saddle River, NJ, 1989
• HM81: Robert Hood and Robert Melville. Real-time queue operations in pure Lisp. Information Processing Letters, 13:50-53, 1981.
• Hoa71: C. A. R. Hoare, Proof of a program: FIND, Communications of the ACM, v.14 n.1, p.39-45, Jan. 1971 [doi>10.1145/362452.362489]
• Hoa72: C.A.R. Hoare. Proof of correctness of data representations. Acta lnformatica, 1'271- 281. 1972.
• Hoa73: C. A. R. Hoare, Hints on programming language design., Stanford University, Stanford, CA, 1973
• Hö193: Urs Hölzle, Integrating Independently-Developed Components in Object-Oriented Languages, Proceedings of the 7th European Conference on Object-Oriented Programming, p.36-56, July 26-30, 1993
• HPW92: Paul Hudak, Simon Peyton Jones, and Philip Wadler. Report on the programming language Haskell' a non-strict, purely functional language, version 1.2. Technical Report YALEU/DCS/RR-777, Yale University Department of Computer Science, March 1992.
• Hug85: John Hughes, Lazy memo-functions, Proc. of a conference on Functional programming languages and computer architecture, p.129-146, January 1985, Nancy, France
• HW73: C.A.R. Hoare and Niklaus Wirth. An axiomatic definition of the programming language Pascal. Acta Informatica, 2'335-355, 1973.
• KH98: Ralph Keller , Urs Hölzle, Binary Component Adaptation, Proceedings of the 12th European Conference on Object-Oriented Programming, p.307-329, July 20-24, 1998
• LM92: Patrick Lincoln and John Mitchelk Operational aspects of linear lambda calculus. In Seventh Annual IEEE Symposium on Logic in Computer Science, Santa Cruz, California, pages 235-246, Los Alamitos. California, June 1992. IEEE Computer Society Press.
• Mas88: I. A. Mason, Verification of programs that destructively manipulate data, Science of Computer Programming, v.10 n.2, p.177-210, April 1988 [doi>10.1016/0167-6423(88)90026-3]
• Mog89: E. Moggi, Computational lambda-calculus and monads, Proceedings of the Fourth Annual Symposium on Logic in computer science, p.14-23, June 1989, Pacific Grove, California, United States
• Mog91: Eugenio Moggi, Notions of computation and monads, Information and Computation, v.93 n.1, p.55-92, July 1991 [doi>10.1016/0890-5401(91)90052-4]
• Möl93: Bernhard Möller, Towards pointer algebra, Science of Computer Programming, v.21 n.1, p.57-90, Aug. 1993 [doi>10.1016/0167-6423(93)90008-D]
• Möl97: Bernhard Möller, Calculating with pointer structures, Proceedings of the IFIP TC 2 WG 2.1 international workshop on Algorithmic languages and calculi, p.24-48, January 1997, Alsace, France
• MOTW95: J. Maraist , M. Odersky , D. N. Turner , P. Wadler, Call-by-name call-by-value, call-by-need and the linear lambda calculus, Theoretical Computer Science, v.228 n.1-2, p.175-210, Oct. 1999 [doi>10.1016/S0304-3975(98)00358-2]
• MPW92: Robin Milner , Joachim Parrow , David Walker, A calculus of mobile processes, II, Information and Computation, v.100 n.1, p.41-77, Sept. 1992 [doi>10.1016/0890-5401(92)90009-5]
• MT91: Ian Mason and Carolyn Talcott. Equivalence in functional languages with side effects. Journal of Functional Programming, 1(3):287-327, July 1991.
• Ode92: Martin Odersky, Observers for linear types, Symposium proceedings on 4th European symposium on programming, p.390-407, January 1992, Rennes, France
• Oka97: Chris Okasaki, Catenable double-ended queues, Proceedings of the second ACM SIGPLAN international conference on Functional programming, p.66-74, June 09-11, 1997, Amsterdam, The Netherlands
• ORH93: Martin Odersky , Dan Rabin , Paul Hudak, Call by name, assignment, and the lambda calculus, Proceedings of the 20th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.43-56, March 1993, Charleston, South Carolina, United States [doi>10.1145/158511.158521]
• Rey79: John C. Reynolds, Reasoning about arrays, Communications of the ACM, v.22 n.5, p.290-299, May 1979 [doi>10.1145/359104.359110]
• SBL+91: Robert E. Strom , David F. Bacon , Arthur P. Goldberg , Andy Lowry , Daniel M. Yellin , Shaula Alexander Yemini, Hermes: a language for distributed computing, Prentice-Hall, Inc., Upper Saddle River, NJ, 1991
• SDDS86: J. T. Schwartz , R. B. Dewar , E. Schonberg , E. Dubinsky, Programming with sets; an introduction to SETL, Springer-Verlag New York, Inc., New York, NY, 1986
• SF93: Amr Sabry and John Field. Reasoning about explicit and implicit representations of state. In SIPL '93 A CM SIGPLAN Workshop on State in Programming Languages, Copenhagen, Denmark, pages 17-30, June 1993. Yale University Research Report YALEU/DCS/RR-968.
• Wad90a: Philip Wadler, Comprehending monads, Proceedings of the 1990 ACM conference on LISP and functional programming, p.61-78, June 27-29, 1990, Nice, France [doi>10.1145/91556.91592]
• Wad90b: Philip Wadler. Linear types can change the world! In M. Broy and C. Jones, editors, IFIP TC 2 Working Conference on Programming Concepts and Methods, Sea of Galilee, Israel, pages 347-359. North Holland, April 1990.
• Wad92: Philip Wadler, The essence of functional programming, Proceedings of the 19th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.1-14, January 19-22, 1992, Albuquerque, New Mexico, United States [doi>10.1145/143165.143169]
• WH66: Niklaus Wirth , C. A. R. Hoare, A contribution to the development of ALGOL, Communications of the ACM, v.9 n.6, p.413-432, June 1966 [doi>10.1145/365696.365702]

INDEX TERMS

Primary Classification:
  D. Software
  D.1 PROGRAMMING TECHNIQUES

Additional Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.2 Semantics of Programming Languages
          Subjects: Operational semantics

  G. Mathematics of Computing
  G.2 DISCRETE MATHEMATICS
  G.3 PROBABILITY AND STATISTICS
      Subjects: Queueing theory
  G.4 MATHEMATICAL SOFTWARE
      Subjects: Algorithm design and analysis

General Terms:
Algorithms, Design, Languages, Performance, Theory