Refinement of Classical Proofs for Program Extraction

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.