Delivery-Date: 
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
Date: Fri, 5 Mar 93 20:56:50 EST
From: mel@EDU.CORNELL.EE.ultrastar (Miriam Leeser)
Message-Id: <9303060156.AA10011@ultrastar.EE.CORNELL.EDU>
To: info-hol@edu.uidaho.cs.ted
Cc: mel@edu.uidaho.ee
Subject: Constructive logic, Nuprl and Hardware Verification


I just want to follow up on the discussion about extraction,
constructivity, and Nuprl.  I think there are three issues here.  The
first, extracting code from classical proofs, has been well covered by
earlier messages and by Chet Murthy's research.

The other two issues are hardware verification with constructive
logic, and using Nuprl for hardware verification.

Constructive logic is not conceptually difficult.  In terms of proof,
it means that I do not in general, have use of the law of the excluded
middle (P \/ ~P) and that I can not always prove things by
contradiction.  For predicates which are decidable (and most
encountered in hardware verification are), I can prove things by
contradiction.  Or, to paraphrase Dave Musser's message, most proofs
done (in HOL or otherwise) are inherently constructive.

The example Paul Loewenstein cited of a theorem that is classically
but not constructively true is Koenig's lemma.  

An informal statement of Koenig's lemma is:

   If there is no finite upper bound to the lengths of paths
   in a finitely branching tree, then there is at least one
   infinite path in the tree.

In general, this is not constructively true.  What is constructively
provable is a form of the contrapositive, i.e. if there are no
infinite paths in the tree, then there is a finite upper bound on the
lengths.  For most practical uses of Koenig's lemma, this
constructively true fact is all that is required.

There are two other classes of theorems which are classically but not
constructively true that come to mind.  
1) Things like analysis, which depend on non-constructive data
(the real numbers).  In this case, you can define constructive
real numbers and get results analogous to classical analysis.
In hardware, of course, we are dealing with finite representations
of real numbers already, so it's not a problem.

2) Things like the halting problem, which are more directly
dependent on decidability.  Classically, the statement
"There is a function f(n) such that f(n) = 1 if Turing
machine n halts on all inputs and f(n) = 0 if Turing
machine n does not halt on all inputs" is true, but of
course the function f is not computable so it doesn't
exist constructively.  Koenig's lemma is in this category
since, given there is no finite upper bound, one cannot
decide which path is infinite.  If one deals only with decidable
predicates, then this is not a problem either.

In our experience working in Nuprl 3, we can do most hardware proofs
exactly in the same style we would do them in HOL, if we want to.
However, we find it useful to have a dichotomy between propositions
and booleans.  We reason over propositions, and use booleans as types
of signals.  Propositions may be proven false, proven true, or
neither.

In the new version of Nuprl (Nuprl 4), you can easily use constructive
or classical logic.  In Nuprl 4, we can prove things classically with
the following advantages.  We have the dichotomy between propositions
and booleans that I mentioned above, and we also have dependent types.
See Keith Hanna's research [Hanna] for advantages in using dependent
types for hardware verification.  Keith Hanna's work uses dependent types
with classical logic.

In the HOL workshop last September, Mark Aagaard and I had a paper
discussing how to exploit Nuprl's type theory to support multiple
hardware implementations of the same specification.  This work could
be done in HOL.  We believe that this would essentially require
duplicating the support of dependent types in HOL.  

The main cost of the added complexity of Nuprl's richer type theory is
that type checking is formally undecidable.  In our experience, the
benefits of the richer type theory far outweigh the costs.  In
addition, in all cases I can think of, the type checking is decidable,
and in most of those cases, is handled automatically by Nuprl's
type-checking system.  Type checking may sometimes be slow; however,
this is usually noticeable only in rewriting with very large terms.

Miriam Leeser
Assistant Professor
Cornell School of Electrical Engineering
Ithaca, NY
mel@ee.cornell.edu

Note:  Thanks to Judith Underwood, Mark Aagaard, and Paul Jackson, all
of Cornell, for their contributions to this message.

[Hanna]

F. K. Hanna and N. Daeche, "Dependent types and formal synthesis" in
Hoare and Gordon, editors, Mechanized Reasoning and Hardware Design.
Prentice Hall International, 1992.