Light Functional Interpretation
| Autor: | Mircea-Dan Hernest |
|---|---|
| Rok vydání: | 2005 |
| Předmět: | |
| Zdroj: | Computer Science Logic ISBN: 9783540282310 CSL |
| DOI: | 10.1007/11538363_33 |
| Popis: | We give a Natural Deduction formulation of an adaptation of Godel's functional (Dialectica) interpretation to the extraction of (more) efficient programs from (classical) proofs. We adapt Jorgensen's formulation of pure Dialectica translation by eliminating his “Contraction Lemma” and allowing free variables in the extracted terms (which is more suitable in a Natural Deduction setting). We also adapt Berger's uniform existential and universal quantifiers to the Dialectica-extraction context. The use of such quantifiers without computational meaning permits the identification and isolation of contraction formulas which would otherwise be redundantly included in the pure-Dialectica extracted terms. In the end we sketch the possible combination of our refinement of Godel's Dialectica interpretation with its adaptation to the extraction of bounds due to Kohlenbach into a light monotone functional interpretation. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|