On the expressivity of elementary linear logic: Characterizing Ptime and an exponential time hierarchy

摘要

Elementary linear logic is a simple variant of linear logic due to Girard and which characterizes in the proofs-as-programs approach the class of elementary functions, that is to say functions computable in time bounded by a tower of exponentials of fixed height. Other systems like light and soft linear logics have then been defined to characterize in a similar way the more interesting complexity class of polynomial time functions, but at the price of either a more complicated syntax or of more sophisticated encodings. These logical systems can serve as the basis of type systems for λ-calculus ensuring polynomial time complexity bounds on well-typed terms. This paper aims at reviving interest in elementary linear logic by showing that, despite its simplicity, it can capture smaller complexity classes than that of elementary functions. For that we carry a detailed analysis of its normalization procedure, and study the complexity of functions represented by a given type. We then show that by considering a slight variant of this system, with type fixpoints and free weakening (elementary affine logic with fixpoints) we can characterize the complexity of functions of type !W -° !~(k+2)B, where W and B are respectively types for binary words and booleans. The key point is a sharper study of the normalization bounds. We characterize in this way the class P of polynomial time predicates, and more generally the hierarchy of classes k-EXP, for k ≥ 0, where k-EXP is the union of DTIME(2_k~(n~i)). for i ≥ 1.