Polynomial Time Calculi

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.