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

Preview |
PDF
Schimanski_Stefan.pdf 4MB |

**DOI**: 10.5282/edoc.9910

### 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 (non-trivial) compositional embedding of LFPL. The pull-out trick of LAL is identified as a technique to type certain non-size-increasing 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: | Theses (Dissertation, LMU Munich) |
---|---|

Keywords: | polynomial time, lambda calculus, programming language |

Subjects: | 500 Natural sciences and mathematics > 510 Mathematics 500 Natural sciences and mathematics |

Faculties: | Faculty of Mathematics, Computer Science and Statistics |

Language: | English |

Date of oral examination: | 23. February 2009 |

1. Referee: | Schwichtenberg, Helmut |

MD5 Checksum of the PDF-file: | b48cfa09f777e526733dc9cf691ac7bb |

Signature of the printed copy: | 0001/UMC 17726 |

ID Code: | 9910 |

Deposited On: | 20. Apr 2009 09:15 |

Last Modified: | 24. Oct 2020 06:18 |