Extracting Cost Recurrences From Sequential and Parallel Functional Programs

Complexity analysis aims to predict the resources, most often time and space, which a program requires. We build on previous work by Danner et al. [2013] and Danner et al. [2015], which formalizes the extraction of recurrences for evaluation cost from higher order functional programs. Source language programs are translated into a complexity language. The translation of a program is a pair of a cost, a bound on the cost of evaluating the program to a value, and a potential, the cost of future use of the value. We use the formalization to analyze the time complexity of higher order functional programs. We also demonstrate the exibility of the method by extending it to parallel cost semantics. In parallel cost semantics, costs are cost graphs, which express dependencies between subcomputations in the program. We prove by logical relations that the extracted recurrences are an upper bound on the evaluation cost of the original program. We also give examples of the analysis of higher order functional programs under the parallel evaluation semantics. We also prove the recurrence for the potential of a program does not depend on the cost of the program.