Collected Size Semantics for Functional Programs over Polymorphic Nested Lists -- Full version: 28 pages
Olha Shkaravska, M.C.J.D. van Eekelen, Alejandro Tamalet · Radboud Repository (Radboud University) · 2009
A b stra ct.Size analysis is an important prerequisite for heap consump tion analysis.This paper is a part of ongoing work about typing support for checking output-on-input size dependencies for function definitions in a strict functional language.A significant restriction for our earlier re sults is that inner data structures (e.g. in a list of lists) all must have the same size.Here, we make a big step forwards by overcoming this lim itation via the introduction of higher-order size annotations such that variate sizes of inner data structures can be expressed. In tro d u ctio nBound on the resource consupmtion of programs can be used, and are often needed, to ensure correctness and security properties, in particular in devices with scarce resources as mobile phones and sm art cards.B oth the memory and the tim e consumption of a program often depend on the sizes of input and interm ediate data.Here, we consider size analysis of strict functional programs over polymorphic lists.A size dependency of a program is a size fu n c tio n th at maps the size of inputs onto the sizes of the corresponding output.For instance, the typical size dependency for a program append, th a t appends two lists of length n and m, is the function append(n, m) = n + m.This paper is devoted to collecting size dependencies using m ultivalued size functions.Multivalued size functions can be defined by conditional multiplechoice rewriting rules [13].These multivalued size functions are used to annotate types.They make it possible to express th a t there can be more than one possible output size (like e.g. in the case of inserting an element to a list if it is not there already: the result will either have the same size or it will be one element larger).Consider e.g. the program insert : (a x a ^ Bool) x a x Ln (a) ^ L;nsf, rt(n)(a) th at inserts an element z of the type a in a list l, if this list does not contain an element z!, such th a t the relation g(z, z') holds: insert(g, z, l) = match l with | Nil ^ Cons(z, Nil) | Cons(hd, tl) ^ if g(z, hd) then l else Cons(hd, insert(g,z, tl)) * This work is part of the AHA project [16] which is sponsored by the Netherlands Organisation for Scientific Research (NWO) under grant nr.612.063.511.