A Naïve Time Analysis and its Theory of Cost Equivalence

Research Council (The DART project) Techniques for reasoning about extensional properties of functional programs are well-understood, but methods for analysing the underlying intensional, or operational proper-ties have been much neglected. This paper begins with the development of a simple but useful calculus for time analysis of non-strict functional programs with lazy lists. One limitation of this basic calculus is that the ordinary equational reasoning on func-tional 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 evalu-ation 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 basic calculus) and provides useful proof techniques for establishing cost-equivalence laws. It is shown that basic evaluation time can be derived by demonstrating a certain for