Delivery-Date: 
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
Message-Id: <199304021841.AA04771@panther.cs.uidaho.edu>
To: info-hol@edu.uidaho.cs.ted
Subject: Constructive Analysis and Hardware verification
Date: Fri, 02 Apr 93 10:41:33 -0800
From: Phil Windley <windley@edu.uidaho.cs.panther>


Miriam Leeser sent this to info-hol-request a while back and I just thought
everyone had seen it.  You haven't.  I apologize for not paying closer
attention to my mail.

------- Forwarded Message

From: mel@ultrastar.EE.CORNELL.EDU (Miriam Leeser)
Subject: Constructive Analysis and Hardware verification


Francisco Corella writes

  >"Analysis" does come up in hardware verification.  The ordering on
  >Time (the set of time instants) is isomorphic to the ordering of the
  >real numbers, and thus time is a continuum.  So if you want to verify
  >asynchronous circuits and "do things right", instead of using
  >induction, you must use the greatest lower bound property (every
  >non-empty subset bounded below has a greatest lower bound) and reason
  >by contradiction.  (See chapter 4, section 3 of Cambridge T.R. 232.)

  >As for finite representations of real numbers:  To verify whether an
  >operation on real numbers is implemented correctly, you presumably
  >want to prove that the computed result is is an adequate approximation
  >of the exact result.  For that you need a theory of the real numbers
  >implying what the exact result is.

I agree with most of what Francisco says.  Analysis does come up in
hardware verification, and in general, you want to prove that a
computed result of a real computation is an adequate approximation of
the exact result.

You can do this with constructive reals.  A constructive real is a
computable, convergent sequence of rationals such that we can
construct approximations arbitrarily close to the limit of the
sequence.  Two reals are equal if their difference can be made
arbitrarily close to zero.

Most hardware proofs done are inherently constructive, especially those done
with mechanical theorem provers.  Essentially, if you reason about a
number mechanically you must construct the representation of that
number.  The representation need not be limited by the architecture of
the machine; you can represent a real as a procedure which returns the
next rational in the sequence.

You CAN use proof by contradiction in constructive proofs.  However,
you must first prove that the predicate you wish to prove is
decidable, i.e. P \/ ~ P = true.

A good reference on this topic is:
   Bishop and Bridges, "Constructive Analysis",  Springer Verlag, 1985.

Note:  Chapter 1 of this book is titled "A Constructivist Manifesto."

Miriam Leeser  ( a born-again constructivist ?)
mel@ee.cornell.edu


------- End of Forwarded Message