Skip to main content


eCommons@Cornell

eCommons@Cornell >
College of Engineering >
Computer Science >
Computer Science Technical Reports >

Please use this identifier to cite or link to this item: http://hdl.handle.net/1813/6991
Title: Extracting Constructive Content from Classical Proofs
Authors: Murthy, Chetan R.
Keywords: computer science
technical report
Issue Date: Aug-1990
Publisher: Cornell University
Citation: http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR90-1151
Abstract: This 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.
URI: http://hdl.handle.net/1813/6991
Appears in Collections:Computer Science Technical Reports

Files in This Item:

File Description SizeFormat
90-1151.pdf16.67 MBAdobe PDFView/Open
90-1151.ps3.08 MBPostscriptView/Open

Refworks Export

Items in eCommons are protected by copyright, with all rights reserved, unless otherwise indicated.

 

© 2014 Cornell University Library Contact Us