Project topics and materials
Get Complete Project Material File(s) Now! »
The light (monotone)functional interpretation
By LD-interpretation (a short for “Light Dialectica Interpretation”) we call below our adaptation of G¨odel’s functional “Dialectica” interpretation [45] to the extraction of (more) efficient programs from (classical) proofs. The LD-interpretation is a recursive syntactic translation from proofs in WeZ∃,nc+
(or in WeZnc,c+, modulo the Kuroda double-negation translation) to proofs in WeZ∃ or even WeZ, such that the positive occurrences of ∃ and the negative occurrences of ∀ in the proof’s conclusion formula get effectively realized by terms in G¨odel’s T. These realizing terms are also called the programs extracted by the LD-interpretation and (if only the extracted programs are wanted) the translation process is also referred to as program-extraction. The translated proof is also called the verifying proof since it verifies the fact that the extracted programs truly realize the existential side of the LD-interpretation (LD-translation) of the conclusion formula of the proof at input. G¨odel’s Dialectica interpretation (abbreviated D-interpretation) is relatively (far) more complicated when it has to face (computationally relevant1) contraction, which in Natural Deduction amounts to discharging more than one copy of an assumption formula in an Implication Introduction→+. Kohlenbach introduces in [68] an elegant method for simplifying the treatment of contraction when the goal is to extract Howard majorizing functionals for the Dialectica realizers. He named “monotone functional interpretation” this variant of the D-interpretation which we here abbreviate by MD-interpretation. The MD-interpretation has been used with great success over the last years for producing proofs to important new theorems in numerical functional analysis ([81] and [63] contain comprehensive surveys of such to-day applications of MD-interpretation to concrete mathematical proofs from the literature – for direct references see, e.g., [68, 62, 64, 66, 67, 75, 76, 78, 79, 80, 82, 41, 77]). Such theorems are completely new in the sense that they were not established previously via the usual mathematical means from inside the theory (despite attempts). However, whenever the extraction of exact realizers is concerned, the MD-interpretation does not necessarily bring efficient answers. A different kind of optimization of G¨odel’s D-interpretation appears to be necessary. We here propose the LD-interpretation as a refinement of G¨odel’s technique which allows for the extraction of more efficient exact realizers. Moreover, the same refinement equally applies to the extraction of more efficient majorants and bounds via what might be called the light monotone (or light bounded, following [33] rather than [68]) functional interpretation (abbreviated LMD- interpretation).
The light G¨odel Dialectica interpretation
The light functional (or “Light Dialectica”) interpretation/translation (on short “LD-interpretation” or “LD-translation”) subsumes the following unique assignment of formulas. To each instance2 of the formula A(a) (with a all the free variables of A) one associates a unique (α-isomorphism comprised) formula AD(a) ≡ ∃x ∀y AD(x; y; a) with AD not necessarily quantifier-free3 and x, y unique tuples of fresh variables of finite type (such that {x, y, a} are all free variables of AD). The types of x, y depend only on the types of the regularly bound variables of A and on the logical structure of A.
Extensions of the L(M)D-interpretation to extractions from fully classical proofs
The problem of full AxSTAB is that it has no (direct) realizer under (light) Dialectica interpretation. Preprocessing double negation translations will be necessary to interpret fully classical systems. There is a large choice in the literature of so-called negative or double-negation translations, initially introduced by G¨odel [44], Gentzen, Kolmogorov, Glivenko. However, they all have the common feature that the image of a formula is intuitionistically equivalent to a negative formula. This immediately implies the elimination of Stability in 84 The light (monotone) functional Dialectica interpretation the translated proof. Thus, the translation of formulas A induces a translation from classical proofs of A to intuitionistic proofs of the image of A. Kuroda’s N-translation (abbreviated “the KN-translation”) appears as a natural choice in the context of Dialectica interpretations because of its ability to uniformly handle blocks of universal quantifiers (see, e.g., [57, 63, 81]). We will also use the G¨odel-Gentzen negative translation (abbreviated “the GN-translation”, for important historical references see [123] and [90]) which simply replaces ∃ by ∃cl (and also ∃ by ∃cl in our ncm-setting). The usual double negation of every atomic formula would here be redundant because our systems enjoy quantifier-free stability, see Lemma 1.36. Hence the GN- translation appears to be structurally much simpler than the KN-translation and therefore appears to be most suitable in a Natural Deduction context (see [111] as an example, also for an important optimization relative to the program extraction by the BBS refined A-translation). Also the strong ∃ (and similarly ∃ in our ncm-setting) disappears from the translated system which therefore seems to be simpler than the KN-translated system (which conserves the strong existentials).
Table of contents :
Introduction
Outline of the following sections
1 Arithmetical systems for G¨odel functionals
1.1 Languages, types, terms and formulas
1.2 Logical axioms and rules and Boolean axioms
1.2.1 Stability, Case Distinction, Decidability and Disjunction Introduction/Elimination
1.3 Weakly extensional Intuitionistic Arithmetics WeZ, WeZ∃, WeZnc and WeZ∃,nc
1.3.1 The “no-undischarged-assumptions” Induction Rule
1.3.2 The rules of Equality for all simple types
1.3.3 Equality axioms induced by the Conversion Relation →֒ 40
1.3.4 The definition of systems WeZ, WeZ∃, WeZnc and WeZ∃,nc
1.3.5 Equivalence between three formulations of Induction
1.4 Immediate extension of systems WeZnc and WeZ∃,nc
1.5 The monotonic intuitionistic Arithmetics WeZ∃ m and WeZ∃,nc+
1.6 The classical (monotonic) Arithmetics WeZnc,c+ and WeZ∃,nc,c+ m
Discussion
2 The light (monotone) functional Dialectica interpretation
2.1 The light G¨odel functional “Dialectica” interpretation
2.2 The light monotone functional “Dialectica” interpretation
2.3 Extensions of the light (monotone) Dialectica interpretation to extractions from fully classical proofs
2.4 Light Monotone Dialectica extractions from classical analytical proofs by elimination-of-extensionality and ε-arithmetization
3 Feasible systems of Arithmetic and Analysis
3.1 A poly-time Arithmetic/Analysis due to Oliva, Cook-Urquhart and Ferrreira
3.2 A polynomial bounded Arithmetic/Analysis due to Kohlenbach
3.2.1 Elimination of the non-standard analytical axiom F−
3.2.2 Verification in the full set-theoretic type structure
3.3 Our proposal for a feasible Arithmetic/Analysis system
4 Comparison with other techniques for extraction of exact realizers from non-intuitionistic proofs
4.1 The BBS refined A-translation
4.1.1 Theoretical comparison with the BBS technique
4.2 Berger’s hsh example
4.2.1 MinLog source code for Berger’s hsh example
4.3 The (semi-)classical Fibonacci proof
4.3.1 Motivation for treatment of Fibonacci in MinLog
4.3.2 The semi-classical Fibonacci proof in MinLog
4.3.3 The light functional “Dialectica” interpretation
4.3.4 A comparison of the three extraction techniques
4.4 Conclusions and future work
4.5 The integer square root example
5 Synthesis of moduli of uniform continuity by the LMD-interpretation in the proof-system MinLog
5.1 The minimal arithmetic HeExtEq proof in the computer-system MinLog
5.2 The MinLog machine majorant extraction
5.3 Machine results for the HeExtEq case-study
Conclusions
Bibliography
