More feasible programs from (non-constructive) proofs by the Light (Monotone) Dialectica interpretation.
Mircea‐Dan Hernest · 2006
This thesis presents a new optimization of Godel's Dialectica interpretation for the extraction of more efficient exact realizers from (classical) arithmetical and even analytical proofs. The light variant of Dialectica also combines and even more smoothly with Kohlenbach's monotone optimization of Godel's functional interpretation for the extraction of more efficient majorants and bounds from (classical)monotonic proofs. Light Dialectica is obtained by adapting Berger's uniform or non-computational quantifiers. Moreover, its presentation is given in Natural Deduction style, as an improvement of Jorgensen's recent adaptation of pure Godel's Dialectica. A number of concrete examples are treated on the computer by means of the novel technique. The machine comparison with the more established program-synthesis technique of refined A-translation shows a very good performance of Light Dialectica, which is outperformed only in the case of Dickson's Lemma. Also the theory of synthesis of feasible, computable programs is developed for the new extraction technique. Two pre-existent frameworks due to Cook-Urquhart-Ferreira and respectively Kohlenbach are crossbreeded for this purpose into a poly-time bounded Analysis. The theoretical result is promising, yet practical examples are to be found for the difference with the pure Kohlenbach's polynomially bounded Analysis.