Delivery-Date: 
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
Message-Id: <9303072138.AA12406@ted.cs.uidaho.edu>
Date: Sun, 7 Mar 93 16:38:26 EST
From: corella@com.ibm.watson
To: info-hol@edu.uidaho.cs.ted
Subject: Analysis and hardware verification

Miriam Leeser says:

> 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.

"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.

Francisco Corella