Extraktion von Programmen aus klassischen Beweisen -Extraction of programs from classical proofs

• Applicant: Professor Dr. Helmut Schwichtenberg
• Subject Area: Theoretical Computer Science
• Term: from 2009 to 2011
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 108789012

• Final Report Year: 2015

Final Report Abstract

Mathematical proofs often contain – at least implicitly – an algorithm to solve the problem posed by the proven proposition. This – in a less direct sense – even applies to non-constructive (“classical”) proofs. The two main methods to obtain such computational content are Gödel’s Dialectica (or functional) interpretation from 1958 and the (refined) Dragalin-Friedman A-translation. The goal of the project was to study the extraction of computational content from classical proofs, and in particular compare and further develop the two methods above. The main results of the research done within the project can be described as follows. (1) We found and developed a decoration algorithm for proofs, which helps substantially to fine tune the computational content of classical proofs. (2) By a detailed analysis of the inner workings of the Gödel interpretation we have described many optimizations, which make it more suitable for program extraction from classical proofs. (3) There is an interesting example (Dickson’s lemma) where a direct analysis of the classical proof (using the finite pigeonhole principle) leads to constructive proof with an easy-to-see computational content. (4) We have found a quadratic algorithm to transform a classical proof (given as a proof in minimal logic using stability axioms) into a constructive proof (by eliminating the stability axioms). It turned out that the Gödel-interpretation and the (refined) A-translation are much closer related than expected. In fact, the latter can be seen as a special case of the former, with suitably decorated logical connectives.

Publications

• Dialectica interpretation with fine computational control. In Proc. 5th Conference on Computability in Europe, volume 5635 of LNCS, pages 467–477. Springer Verlag, Berlin, Heidelberg, New York, 2009
  T. Trifonov
  
• Exploring the computational content of the Infinite Pigeonhole Principle. In Journal of Logic and Computation, 20(2):11–22, 2010
  D. Ratiu and T. Trifonov
  
• Proofs and Computations, Perspectives in Logic. Assoc. Symb. Logic and Cambridge University Press, 2012
  H. Schwichtenberg and S. Wainer
  
• Minimal from classical proofs. In Annals of Pure and Applied Logic, 164:740–748, 2013
  H. Schwichtenberg and C. Senjak