Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
From: tfm@dcs.gla.ac.uk
Message-Id: <9406160929.AA18543@switha.dcs.gla.ac.uk>
To: rahard@ee.umanitoba.ca
Cc: info-hol@leopard.cs.byu.edu
Subject: Re: hardware and higher-order logic
In-Reply-To: Your message of "Thu, 16 Jun 94 00:52:06 CDT." <9406160552.AA06636@ic16.ee.umanitoba.ca>
Date: Thu, 16 Jun 94 10:29:54 +0100


> One of my Profs (a true believer of first-order logic)
> asked me "why the need for higher-order logic in hardware design ?
> Isn't first order logic good enough ? Is it necessary ?"
> 
> I am going to give him a copy of Gordon's paper
> "Why higher-order logic is a good formalism for specifying
> and verifying hardware".
> Are there other papers/ftp-able documents that I should give
> to him ? Any examples ?

I think Jeff Joyce also wrote a paper on this subject.  I haven't got
the exact reference to hand, but you might contact him (joyce@cs.ubc.ca)
to ask. I also allude to the issue in my book on hardware verification
using higher order logic.

I think the case for higher-order logic is good, by the way, but also 
easy to exaggerate.

It's not that some things are technically possible *only if* your
logic's higher-order, it's just that some of the details become (IMHO)
cleaner.  For example, in higher-order logic you can model signals using
variables ranging over functions, for example

   clock : num -> bool

and express correctness by an object-langage implication. However, in
first-order logic you can just use function *constants* and express
corectness using [the creaking machinery of:-)] theory interpretation.

By the way, there's a common misconception that just because you're
working in higher order logic, *everything* becomes a lot harder.
First-order logic is just a sublanguage of higher-order logic - with
pretty much the same rules and syntax. And quite often one finds oneself
essentially in this first-order subworld - where the first-order proofs
are no harder than usual.

Tom