Time analysis, cost equivalence and program refinement

  • David Sands
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 560)


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.


Operational Semantic Program Transformation Functional Language Semantic Rule Primitive Function 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [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
  2. [Abr90]
    S. Abramsky. The lazy lambda calculus. In D. Turner, editor, Research Topics in Functional Programming. Addison Wesley, 1990.Google Scholar
  3. [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
  4. [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
  5. [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
  6. [BHA86]
    G.L. Burn, C.L. Hankin, and S. Abramsky. The theory and practice of strictness analysis for higher order functions. Science of Computer Programming, 7:249–278, 1986.CrossRefGoogle Scholar
  7. [Bje89]
    B. Bjerner. Time Complexity of Programs in Type Theory. PhD thesis, Chalmers University of Technology, 1989.Google Scholar
  8. [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
  9. [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
  10. [GKP89]
    R. L. Graham, D. E. Knuth, and O. Patashnik. Concrete Mathematics. Addison-Wesley, 1989.Google Scholar
  11. [HC88]
    T. Hickey and J. Cohen. Automating program analysis. J. ACM, 35:185–220, January 1988.CrossRefGoogle Scholar
  12. [How89]
    D. J. Howe. Equality in lazy computation systems. In Fourth annual symposium on Logic In Computer Science. IEEE, 1989.Google Scholar
  13. [LeM88]
    D. LeMétayer. An automatic complexity evaluator. ACM ToPLaS, 10(2):248–266, April 1988.CrossRefGoogle Scholar
  14. [Mil83]
    R. Milner. Calculi for synchrony and asynchrony. Theoretical Computer Science, 25:267–310, 1983.CrossRefGoogle Scholar
  15. [MT91]
    I. Mason and C. Talcott. Equivalence in functional languages with effects. Journal of Functional Programming, 1(3):287–327, July 1991.Google Scholar
  16. [Par80]
    D. Park. Concurrency and automata on infinite sequences. In 5th GI conference on Theoretical Computer Science. LNCS 104, Springer Verlag, 1980.Google Scholar
  17. [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
  18. [Ros89]
    M. Rosendahl. Automatic complexity analysis. In Functional Programming Languages and computer architecture, conference proceedings. ACM press, 1989.Google Scholar
  19. [San88]
    D. Sands. Complexity analysis for a higher order language. Technical Report DOC 88/14, Imperial College, October 1988.Google Scholar
  20. [San90a]
    D. Sands. Calculi for Time Analysis of Functional Programs. PhD thesis, Imperial College, September 1990.Google Scholar
  21. [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
  22. [San91a]
    D. Sands. Time analysis, cost equivalence and program refinement. Technical report, Imperial College, 1991.Google Scholar
  23. [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
  24. [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
  25. [Tar55]
    A. Tarski. A lattice-theoretical fixpoint theorem and its applications. Pacific Journal of Math., 5, 1955.Google Scholar
  26. [Wad88]
    P. Wadler. Strictness analysis aids time analysis. In 15th ACM Symposium on Principals of Programming Languages, January 1988.Google Scholar
  27. [Weg75]
    B. Wegbreit. Mechanical program analysis. C.ACM, 18:528–539, September 1975.CrossRefGoogle Scholar
  28. [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

Copyright information

© Springer-Verlag Berlin Heidelberg 1991

Authors and Affiliations

  • David Sands
    • 1
  1. 1.Department of ComputingImperial CollegeLondon

Personalised recommendations