Computer Science – Logic in Computer Science
Scientific paper
2011-01-23
LMCS 7 (2:2) 2011
Computer Science
Logic in Computer Science
52 pages. Accepted in Logical Methods for Computer Science (LMCS), 2010
Scientific paper
10.2168/LMCS-7(2:2)2011
We show how to extract existential witnesses from classical proofs using Krivine's classical realizability---where classical proofs are interpreted as lambda-terms with the call/cc control operator. We first recall the basic framework of classical realizability (in classical second-order arithmetic) and show how to extend it with primitive numerals for faster computations. Then we show how to perform witness extraction in this framework, by discussing several techniques depending on the shape of the existential formula. In particular, we show that in the Sigma01-case, Krivine's witness extraction method reduces to Friedman's through a well-suited negative translation to intuitionistic second-order arithmetic. Finally we discuss the advantages of using call/cc rather than a negative translation, especially from the point of view of an implementation.
No associations
LandOfFree
Existential witness extraction in classical realizability and via a negative translation does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.
If you have personal experience with Existential witness extraction in classical realizability and via a negative translation, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Existential witness extraction in classical realizability and via a negative translation will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-587151