Denotational Semantics As a Foundation for Cost Recurrence Extraction for Functional Languages

A standard informal method for analyzing the asymptotic complexity of aprogram is to extract a recurrence that describes its cost in terms of the sizeof its input, and then to compute a closed-form upper bound on that recurrence.We give a formal account of that method for functional programs in ahigher-order language with let-polymorphism. The method consists of two phases.In the first phase, a monadic translation is performed to extract acost-annotated version of the original program. In the second phase, theextracted program is interpreted in a model. The key feature of this secondphase is that different models describe different notions of size. This playsout in several ways. For example, when analyzing functions that take argumentsof inductive types, different notions of size may be appropriate depending onthe analysis. When analyzing polymorphic functions, our approach shows that onecan formally describe the notion of size of an argument in terms of the datathat is common to the notions of size for each type instance of the domaintype. We give several examples of different models that formally justifyvarious informal cost analyses to show the applicability of our approach.