Startseite
Podcasts
Fakultät für Mathematik, Informatik und Statistik - Digitale Hochschulschriften der LMU - Teil 01/02 Podcast
On the Constructive Content of Proofs

On the Constructive Content of Proofs

Fakultät für Mathematik, Informatik und Statistik - Digitale Hochschulschriften der LMU - Teil 01/02 vor 23 Jahren

0:00

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.