Hernest, Mircea Dan (2006) More feasible programs from (non-constructive) proofs by the Light (Monotone) Dialectica interpretation. PhD thesis LIX, EP - LIX Laboratoire d'Informatique de l'X, EP/X p.264.

Alternative Locations: http://www.imprimerie.polytechnique.fr/Theses/Files/Hernest.pdf

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".

Table of content

\contentsline {chapter}{Introduction}{10}{chapter*.10}
\contentsline {section}{Outline of the following sections}{12}{section*.11}
\contentsline {chapter}{\numberline {1}Arithmetical systems for {\unhbox \voidb@x \hbox {G\"odel}} functionals}{16}{chapter.1}
\contentsline {section}{\numberline {1.1}Languages, types, terms and formulas}{18}{section.1.1}
\contentsline {subsubsection}{Positive and negative occurrences of quantifiers $\forall \hspace {0.5pt},\hspace {0.5pt}\exists \hspace {0.5pt},\hspace {0.5pt}\overline {\forall }\hspace {0.5pt},\hspace {0.5pt}\overline {\exists }$ in formulas}{22}{section*.12}
\contentsline {section}{\numberline {1.2}Logical axioms and rules and Boolean axioms}{24}{section.1.2}
\contentsline {subsection}{\numberline {1.2.1}Stability, Case Distinction, Decidability and\\ Disjunction Introduction/Elimination}{29}{subsection.1.2.1}
\contentsline {section}{\numberline {1.3}Weakly extensional Intuitionistic Arithmetics\\ $\mathtt {WeZ}$, $\mathtt {WeZ^{\exists }}$, $\mathtt {WeZ^{nc}}$ and $\mathtt {WeZ^{\exists ,nc}}$}{37}{section.1.3}
\contentsline {subsection}{\numberline {1.3.1}The ''no-undischarged-assumptions'' Induction Rule}{37}{subsection.1.3.1}
\contentsline {subsection}{\numberline {1.3.2}The rules of Equality for all simple types}{38}{subsection.1.3.2}
\contentsline {subsection}{\numberline {1.3.3}Equality axioms induced by the Conversion Relation $\DOTSB \lhook \joinrel \rightarrow $}{40}{subsection.1.3.3}
\contentsline {subsection}{\numberline {1.3.4}The definition of systems $\mathtt {WeZ}$, $\mathtt {WeZ^{\exists }}$, $\mathtt {WeZ^{nc}}$ and $\mathtt {WeZ^{\exists ,nc}}$}{40}{subsection.1.3.4}
\contentsline {subsubsection}{Lemmas of $\mathtt {WeZ_0}$ which necessarily require the Rewrite Relation $\DOTSB \lhook \joinrel \rightarrow $}{41}{section*.13}
\contentsline {subsection}{\numberline {1.3.5}Equivalence between three formulations of Induction}{42}{subsection.1.3.5}
\contentsline {section}{\numberline {1.4}Immediate extension of systems $\mathtt {WeZ^{nc}}$ and $\mathtt {WeZ^{\exists ,nc}}$}{44}{section.1.4}
\contentsline {section}{\numberline {1.5}The monotonic intuitionistic Arithmetics $\mathtt {WeZ^{\exists }_{m}}$ and $\mathtt {WeZ^{\exists ,nc+}_{m}}$}{47}{section.1.5}
\contentsline {section}{\numberline {1.6}The classical (monotonic) Arithmetics $\mathtt {WeZ^{nc,c+}}$ and $\mathtt {WeZ^{\exists ,nc,c+}_{m}}$}{54}{section.1.6}
\contentsline {section}{Discussion}{56}{section*.14}
\contentsline {chapter}{\numberline {2}The \emph {light} (monotone) functional \emph {Dialectica} interpretation}{58}{chapter.2}
\contentsline {section}{\numberline {2.1}The light \emph {\unhbox \voidb@x \hbox {G\"odel}} functional {''}\textnormal {Dialectica}{''} interpretation}{60}{section.2.1}
\contentsline {section}{\numberline {2.2}The light \emph {monotone} functional {''}\textnormal {Dialectica}{''} interpretation}{76}{section.2.2}
\contentsline {section}{\numberline {2.3}Extensions of the light (monotone) Dialectica interpretation to\\extractions from fully classical proofs}{83}{section.2.3}
\contentsline {section}{\numberline {2.4}Light Monotone Dialectica extractions from classical analytical proofs by elimination-of-extensionality and $\varepsilon $-arithmetization}{93}{section.2.4}
\contentsline {section}{Discussion}{99}{section*.15}
\contentsline {chapter}{\numberline {3}Feasible systems of Arithmetic and Analysis}{102}{chapter.3}
\contentsline {section}{\numberline {3.1}A poly-time Arithmetic/Analysis due to Oliva, Cook-Urquhart and Ferrreira}{104}{section.3.1}
\contentsline {section}{\numberline {3.2}A polynomial bounded Arithmetic/Analysis due to Kohlenbach}{110}{section.3.2}
\contentsline {subsection}{\numberline {3.2.1}\tmspace -\thinmuskip {.1667em}\tmspace -\thinmuskip {.1667em}\tmspace -\thinmuskip {.1667em}\tmspace -\thinmuskip {.1667em}\unhbox \voidb@x \hbox {Elimination of the non-standard analytical axiom $\mathtt {F^{-}}$}}{116}{subsection.3.2.1}
\contentsline {subsection}{\numberline {3.2.2}\tmspace -\thinmuskip {.1667em}\tmspace -\thinmuskip {.1667em}\tmspace -\thinmuskip {.1667em}\unhbox \voidb@x \hbox {Verification in the full set-theoretic type structure}}{117}{subsection.3.2.2}
\contentsline {section}{\numberline {3.3}Our proposal for a feasible Arithmetic/Analysis system}{121}{section.3.3}
\contentsline {section}{Discussion}{124}{section*.16}
\contentsline {chapter}{\numberline {4}Comparison with other techniques for extraction of exact\\ realizers from non-intuitionistic proofs. Case Studies}{126}{chapter.4}
\contentsline {section}{\numberline {4.1}The {\texttt {BBS}} refined {$\mathtt {A}$-translation}}{127}{section.4.1}
\contentsline {subsection}{\numberline {4.1.1}Theoretical comparison with the {\texttt {BBS}} technique}{129}{subsection.4.1.1}
\contentsline {section}{\numberline {4.2}Berger's \emph {hsh} example}{129}{section.4.2}
\contentsline {subsection}{\numberline {4.2.1}{\texttt {MinLog}} source code for Berger's \emph {hsh} example}{130}{subsection.4.2.1}
\contentsline {section}{\numberline {4.3}The (semi-)classical Fibonacci proof}{134}{section.4.3}
\contentsline {subsection}{\numberline {4.3.1}Motivation for treatment of Fibonacci in {\texttt {MinLog}}}{134}{subsection.4.3.1}
\contentsline {subsection}{\numberline {4.3.2}The semi-classical Fibonacci proof in {\texttt {MinLog}}}{136}{subsection.4.3.2}
\contentsline {subsection}{\numberline {4.3.3}The light functional ''Dialectica'' interpretation}{137}{subsection.4.3.3}
\contentsline {subsection}{\numberline {4.3.4}A comparison of the three extraction techniques}{138}{subsection.4.3.4}
\contentsline {section}{\numberline {4.4}Conclusions and future work}{143}{section.4.4}
\contentsline {section}{\numberline {4.5}The integer square root example}{143}{section.4.5}
\contentsline {section}{Discussion}{147}{section*.17}
\contentsline {chapter}{\numberline {5}Synthesis of moduli of uniform continuity by the\\ {\texttt {LMD}-interpretation} in the proof-system {\texttt {MinLog}}}{148}{chapter.5}
\contentsline {section}{\numberline {5.1}The minimal arithmetic {\texttt {HeExtEq}} proof in the\\ computer-system {\texttt {MinLog}}}{150}{section.5.1}
\contentsline {section}{\numberline {5.2}The {\texttt {MinLog}} machine majorant extraction}{152}{section.5.2}
\contentsline {section}{\numberline {5.3}Machine results for the {\texttt {HeExtEq}} case-study}{153}{section.5.3}
\contentsline {section}{Discussion}{154}{section*.18}
\contentsline {chapter}{Conclusions}{158}{chapter*.22}
\contentsline {chapter}{Bibliography}{160}{section*.24}
\contentsline {chapter}{Index of Chapters 1 and 2}{172}{section*.25}
\contentsline {chapter}{\numberline {A}A complexity analysis of functional interpretations}{178}{appendix.A}
\contentsline {subsection}{\numberline {A.0.1}Outline of the main results}{182}{subsection.A.0.1}
\contentsline {subsection}{\numberline {A.0.2}Notational conventions}{185}{subsection.A.0.2}
\contentsline {section}{\numberline {A.1}The weak base system $\mathtt {EIL^{\omega }}$}{186}{section.A.1}
\contentsline {subsection}{\numberline {A.1.1}The type structure $\mathtt {FT}$}{188}{subsection.A.1.1}
\contentsline {subsection}{\numberline {A.1.2}Intuitionistic Equality Logic over $\mathtt {FT}$ ($\mathtt {IEL^{\omega }}$)}{188}{subsection.A.1.2}
\contentsline {subsection}{\numberline {A.1.3}Extended Intuitionistic Equality Logic over $\mathtt {FT}$ ($\mathtt {EIL^{\omega }}$)}{193}{subsection.A.1.3}
\contentsline {section}{\numberline {A.2}A quantitative analysis of functional interpretation}{197}{section.A.2}
\contentsline {subsection}{\numberline {A.2.1}Axiom extensions of $\mathtt {EIL^{\omega }}$.\\The system $\mathtt {EIL_+^{\omega }}\tmspace -\thinmuskip {.1667em}+\tmspace -\thinmuskip {.1667em}\mathtt {AC}\tmspace -\thinmuskip {.1667em}+\tmspace -\thinmuskip {.1667em}\mathtt {IP_\forall }\tmspace -\thinmuskip {.1667em}+\tmspace -\thinmuskip {.1667em}\mathtt {MK}$}{200}{subsection.A.2.1}
\contentsline {subsection}{\numberline {A.2.2}The treatment of $\tmspace +\thickmuskip {.2777em}\mathtt {EIL^{\omega }}$ rules}{201}{subsection.A.2.2}
\contentsline {subsection}{\numberline {A.2.3}Bounds for realizing terms for\\$\mathtt {EIL_+^{\omega }}\tmspace -\thinmuskip {.1667em}+\tmspace -\thinmuskip {.1667em}\mathtt {AC}\tmspace -\thinmuskip {.1667em}+\tmspace -\thinmuskip {.1667em}\mathtt {IP_\forall }\tmspace -\thinmuskip {.1667em}+\tmspace -\thinmuskip {.1667em}\mathtt {MK}$ axioms}{205}{subsection.A.2.3}
\contentsline {subsection}{\numberline {A.2.4}Better bounds on the size of extracted terms}{218}{subsection.A.2.4}
\contentsline {subsection}{\numberline {A.2.5}Space and time complexity of the\\term extraction algorithm}{222}{subsection.A.2.5}
\contentsline {section}{\numberline {A.3}Immediate extensions of the quantitative analysis}{223}{section.A.3}
\contentsline {subsection}{\numberline {A.3.1}Treatment of classical $\mathtt {EIL^{\omega }}$. The system $\mathtt {ECL_+^{\omega }}\tmspace -\thinmuskip {.1667em}+\tmspace -\thinmuskip {.1667em}\mathtt {AC_0}$}{223}{subsection.A.3.1}
\contentsline {subsection}{\numberline {A.3.2}A quantitative analysis of the\\monotone functional interpretation}{227}{subsection.A.3.2}
\contentsline {section}{\numberline {A.4}Extensions to Arithmetic and fragments of Analysis}{232}{section.A.4}
\contentsline {subsection}{\numberline {A.4.1}Treatment of Primitive Recursive Arithmetic $\mathtt {PRA^{\omega }}$}{232}{subsection.A.4.1}
\contentsline {subsection}{\numberline {A.4.2}Extension to the analytical system $\mathtt {PRA^{\omega }}\tmspace -\thinmuskip {.1667em}+\tmspace -\thinmuskip {.1667em}\mathtt {AC_0}\tmspace -\thinmuskip {.1667em}+\tmspace -\thinmuskip {.1667em}\mathtt {WKL}$.}{234}{subsection.A.4.2}
\contentsline {subsection}{\numberline {A.4.3}The case of Peano Arithmetic $\mathtt {PA^{\omega }}$ and $\mathtt {PA^{\omega }}\tmspace -\thinmuskip {.1667em}+\tmspace -\thinmuskip {.1667em}\mathtt {AC_0}\tmspace -\thinmuskip {.1667em}+\tmspace -\thinmuskip {.1667em}\mathtt {WKL}$}{237}{subsection.A.4.3}
\contentsline {section}{Index of Notations}{239}{section*.26}

Statistiques de consultation

Repository Staff Only: edit this item