Time analysis, cost equivalence and program refinement
Techniques for reasoning about extensional properties of functional programs are wellunderstood, but methods for analysing the underlying intensional, or operational properties have been much neglected. This paper presents the development of a simple but practically useful calculus for time analysis of non-strict functional programs with lazy lists.
We begin by considering an operational semantics for a non-strict functional language. The semantic rules directly induce a set of equations which form a basis of a calculus for reasoning about time-cost. However, one limitation of this calculus is that the ordinary equational reasoning on functional programs is not valid. In order to buy back some of these equational properties we develop a non-standard operational equivalence relation called cost equivalence, by considering the number of computation steps as an “observable” component of the evaluation process. We define this relation by analogy with Park's definition of bisimulation in CCS. This formulation allows us to show that cost equivalence is a contextual congruence (and thus is substitutive with respect to the calculus) and provides a uniform method for establishing cost-equivalence laws.
The development of cost-equivalence suggests many other non-standard equivalence relations and preorders. In particular a notion of refinement arises naturally, in which one expression is considered to be a refinement of another (equivalent) expression when it is at least as efficient in any program context. Implications for a theory of program transformation are briefly considered.
KeywordsOperational Semantic Program Transformation Functional Language Semantic Rule Primitive Function
Unable to display preview. Download preview PDF.
- [AA91]Z. M. Ariola and Arvind. A syntactic approach to program transformation. In Proceedings of the symposium on Partial Evaluation and Semantics-Based Program Manipulation. ACM press, SIGPLAN notices, 26(9), September 1991.Google Scholar
- [Abr90]S. Abramsky. The lazy lambda calculus. In D. Turner, editor, Research Topics in Functional Programming. Addison Wesley, 1990.Google Scholar
- [AHU74]A.V. Aho, J.E. Hopcroft, and J.D. Ullman. The Design and Analysis of Computer Algorithms. The Addison-Wesley Series in Computer Science and Information Processing. Addison-Wesley Publishing Company, London, 1974.Google Scholar
- [Bar84]H.P. Barendregt. The Lambda Calculus, volume 103 of Studies in Logic and the Foundations of Mathematics. Elsevier Science Publishers B.V., 2nd edition, 1984.Google Scholar
- [BH89]B. Bjerner and S. Holmström. A compositional approach to time analysis of first order lazy functional programs. In Functional Programming Languages and Computer Architecture, conference proceedings. ACM press, 1989.Google Scholar
- [Bje89]B. Bjerner. Time Complexity of Programs in Type Theory. PhD thesis, Chalmers University of Technology, 1989.Google Scholar
- [Bur91]G. L. Burn. The evaluation transformer model of reduction and its correctness. In TAPSOFT '91 (also Imperial College report DOC 90/19), 1991.Google Scholar
- [BvEG+87]H.P. Barendregt, M.C.J.D. van Eekelen, J.R.W. Glauert, J.R. Kennaway, M.J. Plasmeijer, and M.R. Sleep. Term graph rewriting. In PARLE '87 volume II, number 259 in LNCS, pages 191–231. Springer Verlag, 1987.Google Scholar
- [GKP89]R. L. Graham, D. E. Knuth, and O. Patashnik. Concrete Mathematics. Addison-Wesley, 1989.Google Scholar
- [How89]D. J. Howe. Equality in lazy computation systems. In Fourth annual symposium on Logic In Computer Science. IEEE, 1989.Google Scholar
- [MT91]I. Mason and C. Talcott. Equivalence in functional languages with effects. Journal of Functional Programming, 1(3):287–327, July 1991.Google Scholar
- [Par80]D. Park. Concurrency and automata on infinite sequences. In 5th GI conference on Theoretical Computer Science. LNCS 104, Springer Verlag, 1980.Google Scholar
- [Pey87]S. L. Peyton Jones. The Implementation of Functional Programming Languages. Prentice-Hall International Series in Computer Science. Prentice-Hall International (UK) Ltd, London, 1987.Google Scholar
- [Ros89]M. Rosendahl. Automatic complexity analysis. In Functional Programming Languages and computer architecture, conference proceedings. ACM press, 1989.Google Scholar
- [San88]D. Sands. Complexity analysis for a higher order language. Technical Report DOC 88/14, Imperial College, October 1988.Google Scholar
- [San90a]D. Sands. Calculi for Time Analysis of Functional Programs. PhD thesis, Imperial College, September 1990.Google Scholar
- [San90b]D. Sands. Complexity analysis for a lazy higher-order language. In Proceedings of the Third European Symposium on Programming, number 432 in LNCS. Springer-Verlag, May 1990.Google Scholar
- [San91a]D. Sands. Time analysis, cost equivalence and program refinement. Technical report, Imperial College, 1991.Google Scholar
- [San91b]D. Sands. Towards semantic notions of program improvement. In Proceedings of the Fourth Glasgow Workshop on Functional Programming, Skye, 1991. To appear: Springer Workshop Series.Google Scholar
- [Tal85]C. L. Talcott. The Essence of Rum, A Theory of the intensional and extensional aspects of Lisp-type computation. PhD thesis, Stanford University, August 1985.Google Scholar
- [Tar55]A. Tarski. A lattice-theoretical fixpoint theorem and its applications. Pacific Journal of Math., 5, 1955.Google Scholar
- [Wad88]P. Wadler. Strictness analysis aids time analysis. In 15th ACM Symposium on Principals of Programming Languages, January 1988.Google Scholar
- [WH87]P. Wadler and R. J. M. Hughes. Projections for strictness analysis. In 1987 Conference on Functional Programming and Computer Architecture, Portland, Oregon, September 1987.Google Scholar