University of Illinois Urbana-Champaign

Polynomial-time Martin-Lof type theory

Pe, Joseph Lim

This item is only available for download by members of the University of Illinois community. Students, faculty, and staff at the U of I may log in with your NetID and password to view the item. If you are trying to access an Illinois-restricted dissertation or thesis, you can request a copy through your library's Inter-Library Loan office or purchase a copy directly from ProQuest.

Permalink

https://hdl.handle.net/2142/21156

Description

Title
Polynomial-time Martin-Lof type theory
Author(s)
Pe, Joseph Lim
Issue Date
1991
Doctoral Committee Chair(s)
Henson, C. Ward
Department of Study
Mathematics
Discipline
Mathematics
Degree Granting Institution
University of Illinois at Urbana-Champaign
Degree Name
Ph.D.
Degree Level
Dissertation
Keyword(s)
  • Mathematics
  • Computer Science
Language
eng
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.
Type of Resource
text
Permalink
http://hdl.handle.net/2142/21156
Copyright and License Information
Copyright 1991 Pe, Joseph Lim

Owning Collections

Graduate Dissertations and Theses at Illinois PRIMARY
Graduate Theses and Dissertations at Illinois
Dissertations and Theses - Mathematics