Automatic Complexity Analysis

Researchers (from FMC and APS groups)

   Mário Florido, Hugo Simões, Pedro Vasconcelos
  (Joint work with Kevin Hammond, University of St. Andrews, U.K.)

• Cost analysis using type and effect systems
  We have previously described a type-and-effect system allowing the derivation of upper bounds on program costs. One problem that can arise with this and other similar analyses based on the standard Damas-Milner type system, is that of size aliasing, whereby a single polymorphic type variable may capture different cost properties but the same type. In extreme cases, this leads to complete loss of cost information. We then extended the framework  using rank-2 intersection types.  We show that such a system solves the size aliasing problem in many cases.
  
  Ongoing and future work:  We are currently in the process of extending the language with a fix-point operator for dealing with recursion, extending the type-and-effect system and completing the associated proofs.

• Cost analysis for lazy language
  Cost analysis has been undertaken in the context of a strict, purely functional language, producing cost information in the form of data structure sizes. Extending it to lazy evaluation is a difficult problem that would make possible the use of high declarative languages, such as Haskell, in  domains where obtaining good-quality information concerning runtime costs (whether space or time) is important, such as compiler or database optimization, parallel computing, and real-time systems.
  
  Ongoing and future work:  We are studying extensions of this work to a call-by-need semantics, based on extending a semantics for lazy evaluation with appropriate cost information; and secondly, we are investigating more realistic metrics in the form of stack and heap memory allocations, and in terms of concrete time costs. 

[Go back]