IDEALS Home University of Illinois at Urbana-Champaign logo The Alma Mater The Main Quad

Polynomial-time Martin-Lof type theory

Show full item record

Bookmark or cite this item: http://hdl.handle.net/2142/21156

Files in this item

File Description Format
PDF 9210949.pdf (3MB) Restricted to U of Illinois (no description provided) PDF
Title: Polynomial-time Martin-Lof 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 Urbana-Champaign
Degree: Ph.D.
Genre: Dissertation
Subject(s): Mathematics Computer Science
Abstract: Fragments of extensional Martin-Lof 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 higher-order arithmetic that conservatively extends Cook's equational system PV. PV formalizes the notion of feasibly (i.e., polynomial-time verifiably) constructive proof. $IPV\sp\omega$ in turn captures a basic notion of polynomial-time computability for functionals of finite (linear) type as well. However, while $IPV\sp\omega$ formalizes feasibly constructive first-order 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 propositions-as-types paradigm which identifies a proposition with the set of its proofs. The fragments of $ML\sb0$ obtained extend the above notions for the polymorphic Martin-Lof type structure and exhibit functionals encoding proofs of theorems. Because of their richness, they are well-suited 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: 2011-05-07
Identifier in Online Catalog: AAI9210949
OCLC Identifier: (UMI)AAI9210949
 

This item appears in the following Collection(s)

Show full item record

Item Statistics

  • Total Downloads: 1
  • Downloads this Month: 0
  • Downloads Today: 0

Browse

My Account

Information

Access Key