Computer Science – Logic in Computer Science
Scientific paper
2011-01-28
EPTCS 47, 2011, pp. 73-84
Computer Science
Logic in Computer Science
In Proceedings CL&C 2010, arXiv:1101.5200
Scientific paper
10.4204/EPTCS.47.8
Goedel's functional "Dialectica" interpretation can be used to extract functional programs from non-constructive proofs in arithmetic by employing two sorts of higher-order witnessing terms: positive realisers and negative counterexamples. In the original interpretation decidability of atoms is required to compute the correct counterexample from a set of candidates. When combined with recursion, this choice needs to be made for every step in the extracted program, however, in some special cases the decision on negative witnesses can be calculated only once. We present a variant of the interpretation in which the time complexity of extracted programs can be improved by marking the chosen witness and thus avoiding recomputation. The achieved effect is similar to using an abortive control operator to interpret computational content of non-constructive principles.
No associations
LandOfFree
Dialectica Interpretation with Marked Counterexamples 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 Dialectica Interpretation with Marked Counterexamples, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Dialectica Interpretation with Marked Counterexamples will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-551464