Refinement of Classical Proofs for Program Extraction

Ratiu, Diana (2011): Refinement of Classical Proofs for Program Extraction. Dissertation, LMU München: Fakultät für Mathematik, Informatik und Statistik

Abstract

The A-Translation enables us to unravel the computational information in classical proofs, by first 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 order to obtain better extracted programs. For this, we propose two methods: a controlled and minimal insertion of negations, such that a refinement of the A-Translation can be used and an algorithmic decoration of the proofs, in order to mark the computationally irrelevant components. By restricting the logic to be minimal, the Double Negation Translation is no longer necessary. On this fragment of minimal logic we apply the refined A-Translation, as proposed in (Berget et al., 2002). This method identifies further selected classes of formulas for which the negations do not need to be substituted by computationally relevant formulas. However, the refinement imposes restrictions which considerably narrow the applicability domain of the A-Translation. We address this issue by proposing a controlled insertion of double negations, with the benefit that some intuitionistically valid \Pi^0_2-formulas become provable in minimal logic and that certain formulas are transformed to match the requirements of the refined A-Translation. We present the outcome of applying the refined A-translation to a series of examples. Their purpose is two folded. On one hand, they serve as case studies for the role played by negations, by shedding a light on the restrictions imposed by the translation method. On the other hand, the extracted programs are characterized by a specific behaviour: they adhere to the continuation passing style and the recursion is in general in tail form. The second improvement concerns the detection of the computationally irrelevant subformulas, such that no terms are extracted from them. In order to achieve this, we assign decorations to the implication and universal quantifier. The algorithm that we propose is shown to be optimal, correct and terminating and is applied on the examples of factorial and list reversal.

Abstract

Die A-Übersetzung ermöglicht es, die rechnerische Information aus klassischen Beweisen einzuholen. Dennoch hat sie den Nachteil, dass die Programme, die man aus auf diese Weise transformierten Beweisen extrahiert, viele redundante Teile enthalten. Das liegt daran, dass die A-Übersetzung viele doppelte Negationen hinzufügt und alle diese Negationen durch die rechnerisch relevante Form der Ziel-Formel substituiert werden. In dieser Doktorarbeit werden Methoden dargestellt, um Teile der redundante Information in den extrahierten Programen zu entfernen. Einerseits wird das Einfügen der Negationen minimal gehalten und anderseits werden die nicht rechnerischen Teile als solche indentifiziert und ausgezeichnet. Wir bemerken zuerst, dass in der Minimallogik das Einfügen der doppelten Negationen nicht mehr nötig ist. Darüber hinaus, um das Ersetzen aller Negationen zu vermeiden, identifizieren (Berger et al., 2002) diejenigen, wo die Substitution nicht nötig ist. Diese verfeinerte A-Übersetzung hat aber den Nachteil, dass sie den Anwendungsbereich begrenzt. Um das zu beseitigen, wird in dieser Dissertation eine verfeinerte Doppel-Negation angewandt, die bestimmte Formeln so umsetzt, dass die verfeinerte A-Übersetzung darauf anwendbar ist. Als Zugabe kann diese Methode auch benutzt werden, um konstruktive Beweise mancher \Pi^0_2-Formeln in der Minimallogik durchzuführen. Dieses Verfahren wird durch Anwendung der verfeinerten A-Übersetzung auf eine Reihe von bedeutenden Fallstudien illustriert. Es werden das Lemma von Dickson, das unendliche Schubfachprinzip und das Erdös-Szekeres Theorem betrachtet. Dabei wird es festgestellt, dass ein Zusammenhang zu der Endrekursion und dem Rechnen mit Fortsezungen besteht. Ferner, um möglichst viel der überflüssigen Information zu entfernen, wird ein Dekorationsalgorithmus vorgelegt. Dadurch werden die rechnerisch irrelevanten Komponenten identifiziert und entsprechend annotiert, so dass sie während der Extraktion nicht berücksichtigt werden. Es wird gezeigt, dass das vorgeschlagene Dekorationsverfahren, das auf Beweisebene eingesetzt wird, optimal, korrekt und terminierend ist.

• Dokumententyp: Dissertationen (Dissertation, LMU München)
• Keywords: Program extraction, classical proofs, Refined A-Translation, Refined Double Negation, definite and goal formulas, L-critical predicate symbols, algorithmic proof decoration, Infinite Pigeonhole Principle, Dickson's Lemma, Minimum Principle, Finite Pigeonhole Principle, Erdös-Szekeres Theorem
• Themengebiete: 000 Allgemeines, Informatik, Informationswissenschaft > 004 Informatik ; 000 Allgemeines, Informatik, Informationswissenschaft
• Fakultäten: Fakultät für Mathematik, Informatik und Statistik
• Sprache der Hochschulschrift: Englisch
• Datum der mündlichen Prüfung: 16. August 2011
• 1. Bericht­erstatter:in: Schwichtenberg, Helmut