Nothing Special   »   [go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

Time analysis, cost equivalence and program refinement

  • Conference paper
  • First Online:
Foundations of Software Technology and Theoretical Computer Science (FSTTCS 1991)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 560))

Abstract

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.

This work was partially funded by ESPRIT BRA 3124, Semantique.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Similar content being viewed by others

References

  1. 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. S. Abramsky. The lazy lambda calculus. In D. Turner, editor, Research Topics in Functional Programming. Addison Wesley, 1990.

    Google Scholar 

  3. 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. 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. 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. 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.

    Article  Google Scholar 

  7. B. Bjerner. Time Complexity of Programs in Type Theory. PhD thesis, Chalmers University of Technology, 1989.

    Google Scholar 

  8. 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. 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. R. L. Graham, D. E. Knuth, and O. Patashnik. Concrete Mathematics. Addison-Wesley, 1989.

    Google Scholar 

  11. T. Hickey and J. Cohen. Automating program analysis. J. ACM, 35:185–220, January 1988.

    Article  Google Scholar 

  12. D. J. Howe. Equality in lazy computation systems. In Fourth annual symposium on Logic In Computer Science. IEEE, 1989.

    Google Scholar 

  13. D. LeMétayer. An automatic complexity evaluator. ACM ToPLaS, 10(2):248–266, April 1988.

    Article  Google Scholar 

  14. R. Milner. Calculi for synchrony and asynchrony. Theoretical Computer Science, 25:267–310, 1983.

    Article  Google Scholar 

  15. I. Mason and C. Talcott. Equivalence in functional languages with effects. Journal of Functional Programming, 1(3):287–327, July 1991.

    Google Scholar 

  16. D. Park. Concurrency and automata on infinite sequences. In 5th GI conference on Theoretical Computer Science. LNCS 104, Springer Verlag, 1980.

    Google Scholar 

  17. 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. M. Rosendahl. Automatic complexity analysis. In Functional Programming Languages and computer architecture, conference proceedings. ACM press, 1989.

    Google Scholar 

  19. D. Sands. Complexity analysis for a higher order language. Technical Report DOC 88/14, Imperial College, October 1988.

    Google Scholar 

  20. D. Sands. Calculi for Time Analysis of Functional Programs. PhD thesis, Imperial College, September 1990.

    Google Scholar 

  21. 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. D. Sands. Time analysis, cost equivalence and program refinement. Technical report, Imperial College, 1991.

    Google Scholar 

  23. 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. 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. A. Tarski. A lattice-theoretical fixpoint theorem and its applications. Pacific Journal of Math., 5, 1955.

    Google Scholar 

  26. P. Wadler. Strictness analysis aids time analysis. In 15th ACM Symposium on Principals of Programming Languages, January 1988.

    Google Scholar 

  27. B. Wegbreit. Mechanical program analysis. C.ACM, 18:528–539, September 1975.

    Article  Google Scholar 

  28. 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 

Download references

Author information

Authors and Affiliations

  1. Department of Computing, Imperial College, 180 Queens Gate, SW7 2BZ, London

    David Sands

Authors
  1. David Sands
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Somenath Biswas Kesav V. Nori

Rights and permissions

Reprints and permissions

Copyright information

© 1991 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Sands, D. (1991). Time analysis, cost equivalence and program refinement. In: Biswas, S., Nori, K.V. (eds) Foundations of Software Technology and Theoretical Computer Science. FSTTCS 1991. Lecture Notes in Computer Science, vol 560. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-54967-6_59

Download citation

  • DOI: https://doi.org/10.1007/3-540-54967-6_59

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-54967-3

  • Online ISBN: 978-3-540-46612-3

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation