Automatic Complexity Analysis Revisited
by Ralph Benzinger
In this talk, I'll present my recent work on automatic complexity
analysis of functional programs, in particular those synthesized by
Nuprl. After defining a simple abstract cost model based on the
current call-by-name evaluator, I introduce the notion of symbolic
evaluation of open terms and show how we can use this concept to
reason about primitive recursive programs with first-order
functions, lazy lists, and a subclass of higher-order functions.
In the second part of the talk, I'll present my ACAp System for automatic worst-case time complexity analysis of primitive recursive programs. Some selected examples highlight the use of the system and show the different behavior of call-by-name and call-by-value reduction. I'll conclude my presentation with the popular `But why IS it linear?' prize question.