Cette thèse présente une nouvelle optimisation de l'interprétation fonctionnelle (dite "Dialectica") de Gödel pour l'extraction de programmes plus efficaces à partir de preuves arithmétiques et même analytiques (classiques). La version dite "légère" de Dialectica se combine aussi et encore plus facilement avec l'optimisation dite "monotone" de Kohlenbach sur l'interprétation fonctionnelle de Gödel pour l'extraction de majorants et marges plus efficaces à partir de preuves monotones (classiques). La Dialectica légère est obtenue par l'adaptation des quantificateurs "uniformes" (sans signification computationnelle) de Berger. En plus, sa présentation est faite dans le style de la Déduction Naturelle, comme amélioration de l'adaptation récente de Jørgensen s! ur la Dialectica originelle de Gödel. Un bon nombre d'exemples concrèts sont traités sur l'ordinateur par la nouvelle technique d'extraction de programmes. La comparaison en machine avec la technique de synthèse de programmes appelée "A-traduction raffinée" de Berger, Buchholz et Schwichtenberg montre une très bonne performance de la Dialectica légère. Cette dernière n'est dépassée que dans le cas du Lemme de Dickson. Nous développons aussi la théorie de la synthèse de programmes efficaces, de complexité calculatoire polynômiale en temps, par la nouvelle Dialectica légère (monotone). Dans ce but nous métissons deux structures préexistantes de Cook-Urquhart-Ferreira et respectivement Kohlenbach pour obtenir une "Analyse bornée par des polynômes en temps". Ici, le résultat théorique est prometteur mais des exemple! s pratiques restent encore à trouver pour montrer la diff! ére nce de cette structure par rapport à l'"Analyse bornée par un polynôme" de Kohlenbach.
| Identifer | oai:union.ndltd.org:CCSD/oai:pastel.archives-ouvertes.fr:pastel-00002286 |
| Date | 14 December 2006 |
| Creators | Hernest, Mircea Dan |
| Publisher | Ecole Polytechnique X |
| Source Sets | CCSD theses-EN-ligne, France |
| Language | English |
| Detected Language | French |
| Type | PhD thesis |
Page generated in 0.1231 seconds