Lightweight Semiformal Time Complexity Analysis for Purely Functional Data StructuresLightweight Semiformal Time Complexity Analysis for Purely Functional Data Structures AbstractOkasaki and others have demonstrated how purely functional data structures that are efficient even in the presence of persistence can be constructed. To achieve good time bounds essential use is often made of laziness. The associated complexity analysis is frequently subtle, requiring careful attention to detail, and hence formalising it is valuable. This paper describes a simple library which can be used to make the analysis of a class of purely functional data structures and algorithms almost fully formal. The basic idea is to use the type system to annotate every function with the time required to compute its result. An annotated monad is used to combine time complexity annotations. The library has been used to analyse some existing data structures, for instance the deque operations of Hinze and Paterson's finger trees. ErratumIn the typing rule for fix (in Section 10) the term fix t should be replaced by fix (λx.t). Nils Anders DanielssonLast updated Mon May 13 12:27:47 UTC 2013. |