Delivery-Date: 
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
Message-Id: <9303050010.AA14499@algron.cs.cornell.edu>
To: info-hol@edu.uidaho.cs.ted
Subject: extracting code in type theory
Date: Thu, 04 Mar 93 19:10:16 -0500
From: Paul Jackson <jackson@edu.cornell.cs>


Here's the Nuprl angle on extracting code from classical proofs, and
also a brief comment on Paul Loewenstein's remark about using a
`constructive' type theory for reasoning about hardware. 

In work done here at Cornell in using Nuprl for hardware, we have
found that Nuprl's constructivity poses few problems. Most instances
of the excluded middle of interest turn out to be constructively true,
and also there are ways of genuinely working classically. (I'll come
to these shortly). In doing hardware work, we define a type of
Booleans, quite distinct from the type of propositions. The Boolean
type has all the properties one would expect of it.  One uses it for
the values of digital signals and the propositional type for logical
relations characterizing circuit behaviour.  For more information on
current hardware work in Nuprl, see an article by Miriam Leeser in
"Mechanized Reasoning and Hardware Design", edited by Hoare and
Gordon, Prentice Hall, 1992, or a tutorial article which I wrote for
the 92 Theorem Provers in Circuit Design conference.

One can reason classically in Nuprl, and further can extract programs
from classical proofs.  There are several ways of doing this:

1.As Sree Rajan mentioned, Chet Murthy recently wrote a PhD thesis on
this topic.  You can read a summary of some of his arguments in a
LICS 91 paper of his.  Basically what he did was show that one can translate
classical proofs of certain class (pi-0-2 sentences, sentences of form
All x:S Exists y:T.P(x,y) where P(x,y) contains no further
quantifiers) into constructive proofs, and hence can get an extract.
Or, one can extract directly from these classical proofs, using a
non-local control operator (related to the call-cc, call-with-
current-continuation operator, used in continuation-passing-style
semantics and in compilers for functional languages) as the extract of
applications of the double-negation elimination rule.  (Which is
equivalent to the excluded middle.)

2.Doug Howe (also in a LICS 91 paper) has shown how to construct a
consistent model of Martin-Loef type theory in which the type 

  P:Ui -> (P | (P->Void))

corresponding via propositions-as-types to the excluded-middle 
proposition 

  All P:Propi. P or not(P)

is inhabited and hence the excluded-middle is true.  The extract of
this proposition in Doug's model is an oracle for deciding the truth
of any proposition at universe level i.  This oracle can easily be
used to construct a Hilbert choice (epsilon) operator.  Similar models
exist for Nuprl's type theory which is closely related to Martin-Loef's.

Working in type-theory using the propositions-as-types encoding of
logic, and with this model as the intended model, one should be able
to complete any classical proof. In general, the extract of any proof
will contain oracles and will not be executable. In the event that a
proof, and all the proofs that it depends on are constructive, the
extract will be executable.  Note that many instances of the law of
the excluded-middle are constructively true, and one can design an
excluded-middle tactic that always first attempts a constructive
proof before resorting to using the excluded-middle axiom. 
The constructive instances are exactly those for which the
proposition P is decidable. (I myself am currently experimenting with
such a tactic in work I'm doing on constructive and classical abstract
algebra in Nuprl).

The typing of propositions in this classical model isn't quite as
simple as in HOL. There isn't a single type of propositions. Instead
there is a cumulative hierarchy of propositional universes Prop1,
Prop2, ...., Propi, ...  equivalent to the type universes U1, U2, ...,
Ui,... .  If a proposition quantifies over all propositions at level
at most i, then it is at level i+1. This hierarchy is reminiscent of
the level hierarchy in Bertrand Russell's Type Theory. 

Recently we have introduced a mechanism for universe level
polymorphism into the Nuprl system, and with this we find that having
a hierarchy of propositional universes rather than a single type of
propositions type causes few problems.


  - Paul.