On the Constructive Content of Proofs,
Monika Seisenberger, PhD thesis 2003,
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.
@PhDthesis{Seisenberger03,
author = "Monika Seisenberger",
title = "On the computational content of proofs",
school = "Ludwigs-Maximilians-Universit{\"a}t M{\"u}nchen",
year = "2003"}