Skip to Main content Skip to Navigation
Theses

More feasible programs from (non-constructive) proofs by the Light (Monotone) Dialectica interpretation.

Abstract : This thesis presents a new optimization of Gödel'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 Gödel'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 Jørgensen's recent adaptation of pure Gödel'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, poly-time 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".
Document type :
Theses
Complete list of metadatas

Cited literature [108 references]  Display  Hide  Download

https://pastel.archives-ouvertes.fr/pastel-00002286
Contributor : Ecole Polytechnique <>
Submitted on : Wednesday, July 28, 2010 - 4:25:39 PM
Last modification on : Wednesday, March 27, 2019 - 4:41:26 PM
Long-term archiving on: : Tuesday, October 23, 2012 - 11:35:17 AM

Identifiers

  • HAL Id : pastel-00002286, version 1

Collections

Citation

Mircea Dan Hernest. More feasible programs from (non-constructive) proofs by the Light (Monotone) Dialectica interpretation.. Computer Science [cs]. Ecole Polytechnique X, 2006. English. ⟨pastel-00002286⟩

Share

Metrics

Record views

379

Files downloads

472