ocr-030720214909.djvu: eKnigu

Home / lib / 0pre-Library / 2003-07_unsorted /

ocr-030720214909.djvu

Size 2.0Mb
Date Nov 30, 2003

Suppose r P outermost-reduces to t P,
and that r P = --(s) (since r is a proposition, r P is automatically outermost
double-negated...
Arith is guaranteed to succeed, since this resulting sequent has all the same
decidable hypotheses, and the same conclusion, as the original sequent...
Chapter 8
The Implementation of Proof
Translations in Nuprl
In this chapter we will discuss our experiences in implementing the double-negation
and A-translations in Nuprl...
Since
the translated subgods may be in a different order from the original subgoals, or
fewer in number, we must also compare each translated subgod against each of the
original subgods in turn until a match is found, at which point we can recurse...
The Actual Proof Translation Experiment
We implemented the entire translation system in Cambridge ML, the Nuprl met-
alanguage, and used it to (almost automatically) translate the classical proof of
Higman's Lemma into a constructive proof...
We will define the logic Heyting Arithmetic (HA) in complete detail, starting
with the programming language, a subset of Nuprl, its evaluation rules, the
lOO
Double-Negation, Compilation, and Continuations
forms of propositions in the logic, and finally the rules of the logic...
Plotkin defined a similar
SECD machine which captured exactly the operational semantics of the call-by-
name lambda-calculus...
T = Int, one could apply the CPS-translated program to the
empty continuation, A x.x, and recover the same value that the original program
evaluated to...
Thus, our work provides for programming language theorists and designers the
beginnings of a rational and correct basis for typing and reasoning about explicit
continuations...
Moreover, the translated program (the witness extracted from the trans-
lated proof) mimicks the evaluation semantics of the original program, and they
are semantically equivalent...
Extending to Classical Logic
To make the above logic classical, we must add one rule, that of double-negation
elimination...
Another fact to note at this point is the similarity between the sequence of
proofs we generated above, and the sequence of proofs that we generated in the
GSdel/Friedman translation; there, we took a classical proof of 95, generated a
constructive proof of 95, and from that generated a constructive proof of 95...
However, we must make some allowances for the
peculiarities of primitive recursive function definitions in order to avoid being caught
up in insignificant details...
r, though, is supplied with a continuation which computes the value of r,
binds it to m, and returns the pair (n, m)...
Likewise,
when we introduce primitive-recursive function symbols, we will treat primitive
recursive applications as values...
,Terma)
(where F is a primitive recursire function symbol)
S(Terml) (S is the successor function)
0
Dom _-- Int
Vat -- x, y, z, ...
Existential Quantification
There are just two rules for existential types: introduction and elimination...
Unfortunately, we find that we must make other changes to the logic in order
to preserve total correctness...
On the one hand, it is our wish to "guess"
a classical axiom which, when translated, yields the known CPS-translated axiom,
which drives us to make the above changes...
A top-level continuation of type 05 is
Definition 9.9.6 (Top-Level Continuation) A top-level continuation of type 05
is a term r4 of type T, = K;(05) = (05* 05), such that for any value V of type 05,
Vr, V (Vr,, the CPS-translation of V, apphed to the proper top-level continu-
ation, computes to V)...