Program extraction has been initiated in the field of constructive
mathematics, and it attracts interest not only from mathematicians but
also from computer scientists nowadays. From a mathematical viewpoint
its aim is to figure out computational meaning of proofs, while from a
computer-scientific viewpoint its aim is the study of a method to
obtain correct programs. Therefore, it is natural to have both
theoretical results and a practical computer system to develop
executable programs via program extraction.
In this Thesis we study the computational interpretation of
constructive proofs involving inductive and coinductive reasoning. We
interpret proofs by translating the computational content of proofs
into executable program code. This translation is the procedure we
call program extraction and it is given through Kreisel's modified
realizability. Here we study a proof-theoretic foundation for program
extraction, enriching the proof assistant system Minlog based on this
theoretical improvement. Once a proof of a formula is written in
Minlog, a program can be extracted from the proof by the system
itself, and the extracted program can be executed in Minlog.
Moreover, extracted programs are provably correct with respect to the
proven formula due to a soundness theorem which we prove. We practice
program extraction by elaborating some case studies from exact real
arithmetic within our formal theory. Although these case studies have
been studied elsewhere, here we offer a formalization of them in
Minlog, and also machine-extraction of the corresponding programs. / Die Methode der Programmextraktion hat ihren Ursprung im Bereich der
konstruktiven Mathematik, und stößt in letzter Zeit auf viel
Interesse nicht nur bei Mathematikern sondern auch bei Informatikern.
Vom Standpunkt der Mathematik ist ihr Ziel, aus Beweisen ihre
rechnerische Bedeutung abzulesen, während vom Standpunkt der
Informatik ihr Ziel die Untersuchung einer Methode ist, beweisbar
korrekte Programme zu erhalten. Es ist deshalb naheliegend, neben
theoretischen Ergebnissen auch ein praktisches Computersystem zur
Verfügung zu haben, mit dessen Hilfe durch Programmextraktion
lauffähige Programme entwickelt werden können.
In dieser Doktorarbeit wird eine rechnerische Interpretation
konstruktiver Beweise mit induktiven und koinduktiven Definitionen
angegeben und untersucht. Die Interpretation geschieht dadurch,
daß der rechnerische Gehalt von Beweisen in eine
Programmiersprache übersetzt wird. Diese übersetzung wird
Programmextraktion genannt; sie basiert auf Kreisels modifizierter
Realisierbarkeit. Wir untersuchen die beweistheoretischen Grundlagen
der Programmextraktion und erweitern den Beweisassistenten Minlog auf
der Basis der erhaltenen theoretischen Resultate. Wenn eine Formel in
Minlog formal bewiesen ist, läßt sich ein Programm aus dem
Beweis extrahieren, und dieses extrahierte Programm kann in Minlog
ausgeführt werden. Ferner sind extrahierte Programme beweisbar
korrekt bezüglich der entsprechenden Formel aufgrund eines
Korrektheitsatzes, den wir beweisen werden. Innerhalb unserer
formalen Theorie bearbeiten wir einige aus der Literatur bekannte
Fallstudien im Bereich der exakten reellen Arithmetik. Wir entwickeln
eine vollständige Formalisierung der entsprechenden Beweise und
diskutieren die in Minlog automatisch extrahierten Programme.
| Identifer | oai:union.ndltd.org:MUENCHEN/oai:edoc.ub.uni-muenchen.de:17777 |
| Date | 27 December 2013 |
| Creators | Miyamoto, Kenji |
| Publisher | Ludwig-Maximilians-Universität München |
| Source Sets | Digitale Hochschulschriften der LMU |
| Detected Language | English |
| Type | Dissertation, NonPeerReviewed |
| Format | application/pdf |
| Relation | http://edoc.ub.uni-muenchen.de/17777/ |
Page generated in 0.0013 seconds