Sign up to save your podcasts
Or
Share On the Constructive Content of Proofs
Share to email
Share to Facebook
Share to X
Share to email
Share to Facebook
Share to X
Or
On the Constructive Content of Proofs
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.
View all episodes
By Ludwig-Maximilians-Universität München
5
11 ratings
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.
More shows like Fakultät für Mathematik, Informatik und Statistik - Digitale Hochschulschriften der LMU - Teil 01/02
View all
Medizinische Fakultät - Digitale Hochschulschriften der LMU - Teil 06/19
0 Listeners
LMU Kapitalgesellschaftsrecht
0 Listeners
LMU Grundkurs Strafrecht I (L-Z) WS 2014/15
0 Listeners
MCMP – Metaphysics and Philosophy of Language
2 Listeners
Hegel lectures by Robert Brandom, LMU Munich
6 Listeners
John Lennox - Hat die Wissenschaft Gott begraben?
4 Listeners
LMU Rechtsphilosophie
0 Listeners
MCMP – Philosophy of Mathematics
2 Listeners
LMU Wiederholung und Vertiefung zum Schuldrecht - Lehrstuhl für Bürgerliches Recht
0 Listeners
Epistemology and Philosophy of Science: Prof. Dr. Stephan Hartmann – HD
1 Listeners