Schimanski, Stefan (2009): Polynomial Time Calculi. Dissertation, LMU München: Faculty of Mathematics, Computer Science and Statistics 

PDF
Schimanski_Stefan.pdf 4Mb 
Abstract
This dissertation deals with type systems which guarantee polynomial time complexity of typed programs. Such algorithms are commonly regarded as being feasible for practical applications, because their runtime grows reasonably fast for bigger inputs. The implicit complexity community has proposed several type systems for polynomial time in the recent years, each with strong, but different structural restrictions on the permissible algorithms which are necessary to control complexity. Comparisons between the various approaches are hard and this has led to a landscape of islands in the literature of expressible algorithms in each calculus, without many known links between them. This work chooses Light Affine Logic (LAL) and Hofmann's LFPL, both linearly typed, and studies the connections between them. It is shown that the light iteration in LAL, the fixed point variant of LAL, is expressive enough to allow a (nontrivial) compositional embedding of LFPL. The pullout trick of LAL is identified as a technique to type certain nonsizeincreasing algorithms in such a way that they can be iterated. The System T sibling of LAL is developed which seamlessly integrates this technique as a central feature of the iteration scheme and which is proved again correct and complete for polynomial time. Because iterations of the same level cannot be nested, is further generalised to , which surprisingly can express the impredicative iteration of LFPL and the light iteration of at the same time. Therefore, it subsumes both systems in one, while still being polynomial time normalisable. Hence, this result gives the first bridge between these two islands of implicit computational complexity.
Item Type:  Thesis (Dissertation, LMU Munich) 

Keywords:  polynomial time, lambda calculus, programming language 
Subjects:  600 Natural sciences and mathematics > 510 Mathematics 600 Natural sciences and mathematics 
Faculties:  Faculty of Mathematics, Computer Science and Statistics 
Language:  English 
Date Accepted:  23. February 2009 
1. Referee:  Schwichtenberg, Helmut 
Persistent Identifier (URN):  urn:nbn:de:bvb:1999100 
MD5 Checksum of the PDFfile:  b48cfa09f777e526733dc9cf691ac7bb 
Signature of the printed copy:  0001/UMC 17726 
ID Code:  9910 
Deposited On:  20. Apr 2009 09:15 
Last Modified:  16. Oct 2012 08:26 