Light Functional Interpretation

We give a Natural Deduction formulation of an adaptation of G¨odel’s functional (Dialectica) interpretation to the extraction of (more) efficient programs from (classical) proofs. We adapt Jørgensen’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 G¨odel’s Dialectica interpretation with its adaptation to the extraction of bounds due to Kohlenbach into a light monotone functional interpretation.

• Type: Conference
• Year: 2005
• Where: CSL
• Authors: Mircea-Dan Hernest
• Keywords: CSL 2005, Extracted Terms, Natural Deduction, Natural Deduction Formulation