Light Dialectica Program Extraction from a Classical Fibonacci Proof
Mircea‐Dan Hernest · Electronic Notes in Theoretical Computer Science · 2007
We demonstrate program extraction by the Light Dialectica Interpretation ( LDI ) on a minimal logic proof of the classical existence of Fibonacci numbers. This semi-classical proof is available in MinLog 's library of examples. The term of Gödel's T extracted by the LDI is, after strong normalization, exactly the usual recursive algorithm which defines the Fibonacci numbers (in pairs). This outcome of the Light Dialectica meta-algorithm is much better than the T -program extracted by means of the pure Gödel Dialectica Interpretation. It is also strictly less complex than the result obtained by means of the refined A -translation technique of Berger, Buchholz and Schwichtenberg on an artificially distorted variant of the input proof, but otherwise it is identical with the term yielded by Berger's Kripke-style refined A -translation. Although syntactically different, it also has the same computational complexity as the original program yielded by the refined A -translation from the undistorted input classical Fibonacci proof.