On the Constructive Content of Proofs

Abstract

This thesis aims at exploring the scopes and limits of techniques for extracting programs from proofs. We focus on constructive theories of inductive definitions and classical systems allowing choice principles. Special emphasis is put on optimizations that allow for the extraction of realistic programs. Our main field of application is infinitary combinatorics. Higman's Lemma, having an elegant non-constructive proof due to Nash-Williams, constitutes an interesting case for the problem of discovering the constructive content behind a classical proof. We give two distinct solutions to this problem. First, we present a proof of Higman's Lemma for an arbitrary alphabet in a theory of inductive definitions. This proof may be considered as a constructive counterpart to Nash-Williams' minimal-bad-sequence proof. Secondly, using a refined $A$-translation method, we directly transform the classical proof into a constructive one and extract a program. The crucial point in the latter is that we do not need to avoid the axiom of classical dependent choice but directly assign a realizer to its translation. A generalization of Higman's Lemma is Kruskal's Theorem. We present a constructive proof of Kruskal's Theorem that is completely formalized in a theory of inductive definitions. As a practical part, we show that these methods can be carried out in an interactive theorem prover. Both approaches to Higman's Lemma have been implemented in Minlog.

Abstract

Ziel der vorliegenden Arbeit ist es, die Reichweiten und Grenzen von Techniken zur Extraktion von Programmen aus Beweisen zu erforschen. Wir konzentrieren uns dabei auf konstruktive Theorien Induktiver Definitionen und klassische Systeme mit Auswahlprinzipien. Besonderes Gewicht liegt auf Optimierungen, die zur Extraktion von realisischen Programmen f"uhren. Unser Hauptanwendungsgebiet ist die unendliche Kombinatorik. Higmans Lemma, ein Satz mit einem eleganten klassischen, auf Nash-Williams zur"uckgehenden Beweis, ist ein interessantes Fallbeispiel f"ur die Suche nach dem konstruktiven Gehalt in einem klassischen Beweis. Wir zeigen zwei unterschiedliche L"osungen zu dieser Problemstellung auf. Zun"achst pr"asentieren wir einen induktiven Beweis von Higmans Lemma f"ur ein beliebiges Alphabet, der als konstruktives Pendant zum klassischen Beweis angesehen werden kann. Als zweiten Ansatz verwandeln wir mit Hilfe der verfeinerten $A$-"Ubersetzungs-methode den klassischen Beweis in einen konstruktiven und extrahieren ein Programm. Der entscheidende Punkt ist hierbei, dass wir einen direkten Realisierer f"ur das "ubersetzte Auswahlaxiom verwenden. Die Verallgemeinerung von Higmans Lemma f"uhrt zu Kruskals Satz. Wir geben einen konstruktiven Beweis von Kruskals Theorem, der vollst"andig auf den Induktiven Definitionen basiert. Der praktische Teil der Arbeit befasst sich mit der Ausf"uhrbarkeit dieser Methoden und Beweise in dem Beweissystem Minlog.

• Item Type: Thesis (Dissertation, LMU Munich)
• Keywords: Program extraction from constructive and classical proofs, Higman's Lemma, Kruskal's Theorem
• Dewey Decimal Classification: 600 Natural sciences and mathematics; 600 Natural sciences and mathematics > 510 Mathematics
• Faculties: Faculty of Mathematics, Computer Science and Statistics
• Language: English
• Date Accepted: 10. July 2003
• Persistent Identifier (URN): urn:nbn:de:bvb:19-16190
• Signature of the printed copy: 0001/UMC 13494