Abstract
We recapitulate Friedman's conservative extension result of (suitable) classical over constructive systems for Π 02 sentences, viewing it in two lights: as a translation of programs from an almost-functional language (with C) back to its functional core, and as a translation of a constructive logic for a functional language to a classical logic for an almost-functional language. We investigate the computational properties of the translation and of classical proofs and characterize the classical proofs which give constructions in concrete, computational terms, rather than logical terms. We characterize different versions of Friedman's translation as translating slightly different almost-functional languages to a functional language, thus giving a general method for arriving at a sound reduction semantics for an almost-functional language with a mixture of eager and lazy constructors and destructors, as well as integers, pairs, unions, etc. Finally, we describe how to use classical reasoning in a disciplined manner in giving classical (yet constructivizable) proofs of sentences of greater complexity than Π 02 . This direction offers the possibility of applying classical reasoning to more general programming problems.
Supported in part by an NSF graduate fellowship and NSF grant CCR-8616552 and ONR grant N00014-88-K-0409
Preview
Unable to display preview. Download preview PDF.
References
H. P. Barendregt. The Lambda Calculus: Its Syntax and Semantics, volume 103 of Studies in Logic and the Foundations of Mathematics. North-Holland, Amsterdam, revised edition, 1984.
W. Clinger and J. Rees. The revised3 report on the algorithmic language scheme. SIGPLAN Notices, 21(12):37–79, 1986.
R. Constable. The semantics of evidence. Technical Report TR 85-684, Cornell University, Department of Computer Science, Ithaca, New York, May 1985.
D. A. V. Dalen and A. S. Troelstra. Constructivism in Mathematics. North-Holland, 1989.
O. Danvy and A. Filinski. Abstracting control. In Proceedings of the 1990 ACM Conference on Lisp and Functional Programming, pages 151–160, 1990.
M. Felleisen. The Calculi of λ v — CS conversion: A Syntactic Theory of Control and State in Imperative Higher-Order Programming Languages. PhD thesis, Indiana University, 1987.
M. Felleisen and D. Friedman. Control operators, the SECD machine and the λ-calculus. In Formal Description of Programming Concepts III, pages 131–141. North-Holland, 1986.
M. Felleisen, D. Friedman, E.Kohlbecker, and B. Duba. Reasoning with continuations. In Proceedings of the First Annual Symposium on Logic in Computer Science, pages 131–141, 1986.
M. J. Fischer. Lambda-calculus schemata. In Proceedings of the ACM Conference on Proving Assertions about Programs, volume 7 of Sigplan Notices, pages 104–109, 1972.
H. Friedman. Classically and intuitionistically provably recursive functions. In Scott, D. S. and Muller, G. H., editor, Higher Set Theory, volume 699 of Lecture Notes in Mathematics, pages 21–28. Springer-Verlag, 1978.
T. G. Griffin. A formulae-as-types notion of control. In Conference Record of the Seventeenth Annual ACM Symposium on Principles of Programming Languages, 1990.
A. N. Kolmogorov. On the principle of the excluded middle. In J. van Heijenoort, editor, From Frege to Gödel: A Source Book in Mathematical Logic, 1879–1931, pages 414–437. Harvard University Press, Cambridge, Massachusetts, 1967.
C. Murthy. An evaluation semantics for classical proofs. In Proceedings of the Fifth Annual Symposium on Logic in Computer Science, 1991.
G. Plotkin. Call-by-name, call-by-value, and the λ-calculus. Theoretical Computer Science, pages 125–159, 1975.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1992 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Murthy, C.R. (1992). Classical proofs as programs: How, what and why. In: Myers, J.P., O'Donnell, M.J. (eds) Constructivity in Computer Science. Constructivity in CS 1991. Lecture Notes in Computer Science, vol 613. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0021084
Download citation
DOI: https://doi.org/10.1007/BFb0021084
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-55631-2
Online ISBN: 978-3-540-47265-0
eBook Packages: Springer Book Archive