Edinburgh Research Archive >
Informatics, School of >
Informatics thesis and dissertation collection >
Please use this identifier to cite or link to this item:
|Title: ||Type Systems For Polynomial-time Computation|
|Authors: ||Hofmann, Martin|
|Issue Date: ||Feb-1999|
|Publisher: ||Vom Fachbereich Mathematik der Technischen Universitat Darmstadt|
|Abstract: ||This thesis introduces and studies a typed lambda calculus with higher-order primitive recursion over inductive datatypes which has the property that all definable number-theoretic functions are polynomial time computable. This is achieved by imposing type-theoretic restrictions on the way results of recursive calls can be used.
The main technical result is the proof of the characteristic property of this system. It proceeds by exhibiting a category-theoretic model in which all morphisms are polynomial time computable by construction.
The second more subtle goal of the thesis is to illustrate the usefulness of this semantic technique as a means for guiding the development of syntactic systems, in particular typed lambda calculi, and to study their meta-theoretic properties.
Minor results are a type checking algorithm for the developed typed lambda calculus and the construction of combinatory algebras consisting of polynomial time algorithms in the style of the first Kleene algebra.|
|Keywords: ||typed lambda calculi|
polynomial time algorithms
|Appears in Collections:||Informatics thesis and dissertation collection|
Items in ERA are protected by copyright, with all rights reserved, unless otherwise indicated.