Refinement of Classical Proofs for Program Extraction [Elektronische Ressource] / Diana Ratiu. Betreuer: Helmut Schwichtenberg

Diana Ratiu

Sujets

• Informatik
• Mathematics

Informations

• Publié par: ludwig-maximilians-universitat_munchen
• Publié le: 01 janvier 2011
• Nombre de lectures: 32
• Langue: English
• Poids de l'ouvrage: 1 Mo

Extrait

Fakult at fur Mathematik, Informatik und Statistik
Ludwig{Maximilians{Universit at
Munc hen
Mathematische Logik
Prof. Dr. Helmut Schwichtenberg
Re nement of Classical Proofs
for Program Extraction
Diana RatiuRe nement of Classical Proofs
for Program Extraction
Diana Ratiu
Dissertation
an der Fakult at fur Mathematik, Informatik und Statistik
Ludwig{Maximilians{Universit at
Munc hen
vorgelegt von
Diana Ratiu
April 2011
Diana Ratiu
Refinement of Classical Proofs for Program ExtractionDissertation an der Fakult at fur Mathematik, Informatik und Statistik
der Ludwig-Maximilians-Universit at Munc hen
1. Berichterstatter: Prof. Dr. Helmut Schwichtenberg
2. Berich Prof. Dr. Wilfried Buchholz
1. Prufer: Prof. Dr. Otto Forster
2. Prufer: Prof. Dr. Gun ther Kraus
Ersatzprufer: Prof. Dr. Martin Schottenloher
Externer Gutachter: Prof. Dr. Hajime Ishihara
Datum der Einreichung: 4. April 2011
Tag der mundlic hen Prufun g: 16. August 2011ivv
To my familyviAcknowledgments
"Should every one of those who have given
of themselves to us take their share back,
we could not possibly know what would be left of us;
therefore, we owe them all our gratitude." (Teo l P~ ar~ aian)
My gratitude goes to Prof. Helmut Schwichtenberg who has given me
the opportunity to be a PhD Student in the Mathlogaps Project. I have
learned from him a lot, in terms of Logics and in terms of research: his
rigor has taught me how proper mathematics is done. I am grateful that he
has encouraged me to visit other research groups and gave me the unique
opportunity to meet leading researchers in Munich.
I am honored to have Prof. Hajime Ishihara as a second reviewer of my
thesis. I would like to thank him in particular for his patience in clarifying
my questions during our long discussions both in Japan and in Munich.
During my PhD study, I bene ted from the high-quality lectures of Prof.
Wilfried Buchholz. His talks in our group meetings were mind-provoking
and his precision motivating. I am thankful to him for accepting to be my
internal reviewer.
The Mathlogaps project has given me the chance to visit various research
groups and get valuable advice and a critical view of my work. Among
those which have contributed, I am grateful in particular to Ulrich Berger
and Monika Seisenberger for the illuminating discussions during my visit in
Swansea, to Roy Dyckho for inviting me to visit his research group in St.
Andrews and raising issues that shed a new light on my research, to Paulo
Oliva for sharing his perspective regarding proof interpretation; to Bruno
Buchberger for challenging me with questions on the importance of classical
proofs, during his Gr obner Bases Semester in Linz.
In Munich I had the opportunity to be part of a competitive and open
environment: I have exchanged ideas and worked together with many people.
First of all, I would like to thank Stefan Schimanski for taking the time to
viiviii
read my blackboard notes on the intriguing parts of my work. On many
occasions he cleverly asked me questions; his insight has helped me clarify
many aspects regarding my research.
The underground seminar has been a valuable experience and I am
grateful to my colleagues for their wonderful talks and challenging ques-
tions: Basil Karadice, Freiric Baral, Luca Chiarabini, Dominik Schlenker
and Stefan Schimanski. Klaus Thiel was motivational with his perseverance
in tackling new theorems in Minlog.
I am also thankful to those who have their share in some of the chapters
of this thesis. Our long sessions with Trifon Trifonov on the example of the
In nite Pigeonhole Principle has clari ed many of the otherwise cumber-
some aspects of the associated program. The expertise of Josef Berger on
constructive mathematics has been helpful in investigating the strength of
Dickson’s Lemma and has opened the way to future research. I spend long
afternoons debating on the bene ts and limitations of the double-negation
translation with Christian Urban.
Special thanks to Daniel Ratiu, Stefan Schimanski, Bogomil Kovachev,
Kenji Miyamoto, Roy McCasland and Martin Ochoa for putting aside their
own research to review my thesis and provide me with valuable feedback.
I grew to become what I am today professionally thanks to my mathe-
matics teachers Saveta Coste and Ruxanda Georgescu. Later, my BSc Thesis
supervisors Prof. Viorel Negru and Prof. Tudor Jebelean have given me the
rst impulse towards research. My Master’s Thesis supervisor Prof. Dana
Petcu has been a role model, guiding me through my rst research years
and inspiring me with her energy, motivation and willingness to explore new
ideas.
Last but not least, I dedicate this work to our little one, Stefan, to my
husband Daniel and my parents. I thank in particular my husband for his
support and for being an inspiration with his hard-work and perseverance.
I am most grateful to my parents - their love and care for me have guided
me throughout all my life. I owe them what I am today.Abstract
The A-Translation enables us to unravel the computational information in
classical proofs, by rst transforming them into constructive ones, however
at the cost of introducing redundancies in the extracted code. This is due
to the fact that all negations inserted during translation are replaced by the
computationally relevant form of the goal.
In this thesis we are concerned with eliminating such redundancies, in or-
der to obtain better extracted programs. For this, we propose two methods:
a controlled and minimal insertion of negations, such that a re