Show simple item record

dc.contributor.authorMurthy, Chetan R.en_US
dc.description.abstractThis thesis is concerned with the relationship between classical and constructive mathematics. It is well-known that in many constructive logics, we can interpret mathematical sentences as program specifications, and we can interpret a constructive proof of such a sentence as a program which meets this specification. It is also well-known that many classical logics do not have the property, as shown by Brouwer's counterexamples to some theorems of analysis. Kreisel and Friedman showed that for certain classes of sentences $(\Pi_{2}^{0})$, the classical theories conservatively extend their constructive counterparts, and furthermore give effective translations from classical proofs to constructive proofs. This thesis consists of two parts. In the first, we describe our implementation of Friedman's translation results, and their use in translating Higman's Lemma, a nontrivial theorem of combinatorics. To do this, we delineate a subtheory of a constructive type theory (Nuprl) for which Friedman's translation is guaranteed to succeed. We also extend the Nuprl type theory with impredicative $\Pi$-quantification, and use this to provide a classical proof of Higman's Lemma, which we go on to mechanically translate to a constructive proof. In the second part, we discuss connections that we have discovered between Friedman's translation and a standard compilation technique, continuation-passing-style (CPS) translation. We demonstrate that a classical proof of a $(\Pi_{2}^{0})$ sentence $\Phi$ is a program which meets the specification $\Phi$. We demonstrate that we can consistently give algorithmic content to the only constructively problematic rule of classical logic, the rule of double-negation elimination. This algorithmic content is the nonlocal control operator $C$ (a relative of call-with-current-continuation). Moreover, we show that Friedman's translation is exactly a CPS-translation on the classical "program" (with $C$), converting it into a pure functional program (without $C$). Our work provides a semantic account of Friedman's translation, in terms of its effect on programs, making the connections (and the differences) between classical and constructive systems clearer and more precise. Moreover, we provide the first steps towards integrating nonlocal control operators into a type-theoretic explanation of computation.en_US
dc.format.extent17069087 bytes
dc.format.extent3156418 bytes
dc.publisherCornell Universityen_US
dc.subjectcomputer scienceen_US
dc.subjecttechnical reporten_US
dc.titleExtracting Constructive Content from Classical Proofsen_US
dc.typetechnical reporten_US

Files in this item


This item appears in the following Collection(s)

Show simple item record