Files in this item
Files  Description  Format 

application/pdf 9210949.pdf (3MB)  (no description provided) 
Description
Title:  Polynomialtime MartinLof type theory 
Author(s):  Pe, Joseph Lim 
Doctoral Committee Chair(s):  Henson, C. Ward 
Department / Program:  Mathematics 
Discipline:  Mathematics 
Degree Granting Institution:  University of Illinois at UrbanaChampaign 
Degree:  Ph.D. 
Genre:  Dissertation 
Subject(s):  Mathematics
Computer Science 
Abstract:  Fragments of extensional MartinLof type theory without universes, $ML\sb0,$ are introduced that conservatively extend S. A. Cook and A. Urquhart's $IPV\sp\omega.$ A model for these restricted theories is obtained by interpretation in Feferman's theory APP of operators, a natural model of which is the class of partial recursive functions. In conclusion, an example in group theory is considered. $IPV\sp\omega$ is a higherorder arithmetic that conservatively extends Cook's equational system PV. PV formalizes the notion of feasibly (i.e., polynomialtime verifiably) constructive proof. $IPV\sp\omega$ in turn captures a basic notion of polynomialtime computability for functionals of finite (linear) type as well. However, while $IPV\sp\omega$ formalizes feasibly constructive firstorder number theory, it does not naturally apply to higher mathematics, e.g., in general, it lacks the relation of equality among objects of the same type. This motivates the study of extensions of $IPV\sp\omega$ in more expressive formalisms. $ML\sb0$ is a predicative intuitionistic type theory based on the propositionsastypes paradigm which identifies a proposition with the set of its proofs. The fragments of $ML\sb0$ obtained extend the above notions for the polymorphic MartinLof type structure and exhibit functionals encoding proofs of theorems. Because of their richness, they are wellsuited for the development of feasibly constructive mathematics, particularly in the synthesis of feasible algorithms from proofs. 
Issue Date:  1991 
Type:  Text 
Language:  English 
URI:  http://hdl.handle.net/2142/21156 
Rights Information:  Copyright 1991 Pe, Joseph Lim 
Date Available in IDEALS:  20110507 
Identifier in Online Catalog:  AAI9210949 
OCLC Identifier:  (UMI)AAI9210949 
This item appears in the following Collection(s)

Graduate Dissertations and Theses at Illinois
Graduate Theses and Dissertations at Illinois 
Dissertations and Theses  Mathematics