Via:  uk.ac.ucl.cs.nss; 16 Dec 88 20:24 GMT  (UK.AC.Cam.Cl.scaup)
Message-Id: <8812161805.AA13608@clover.ucdavis.edu>
Date: Fri, 16 Dec 88 10:01:50 PST
From: "Paul N. Loewenstein" <paul@edu.stanford.tina>
To: info-hol@edu.ucdavis.clover
Subject: Worries about existential definitions
Sender: paul <paul%edu.stanford.tina@edu.ucdavis.clover>
Status: R


I have been working with state machines, representing them as
relations between inputs and outputs, for example:

     |- ser_add i1 i2 out =
       ?s. (!t. out = sum (i1 t) (i2 t) (s t)) /\
           (s (SUC t) = carry (i1 t) (i2 t) (s t))
where
     |- sum x y z = x xor y xor z
and
     |- carry x y z = x /\ y /\ z

is a representation of a serial adder. This is an example of hardware
with only a partially defined behaviour, and as HOL stands it is not
possible to describe ser_add as a function from inputs to outputs
except via explicit use of @, which, since it represents some fixed
but undefined function, cannot be used to usefully represent a partial
function.

However, it can easily be proven that:

     |- ?f. ! i1 i2. ser_add i1 i2 (f i1 i2)

which, via the proposed existential definition mechanism allows us to
define a function Ser_Add, which satisfies the relation:

     ! i1 i2. ser_add i1 i2 (Ser_Add i1 i2)

without directly invoking @.

The semantics of this function are that of a serial adder with some
fixed but undetermined initial state, which is identical to the
semantics of defining it via @. It is therefore dangerous to
represent state machines in this way, since a design with multiple
Ser_Add's would have an over-defined initial state. We would have
to define a new constant for each instance. This is not terribly
useful either, because we cannot nest constant definition inside a
recursive definition.

So I am worried about whether the gain of being able to define
multiple constants with different "fixed but undefined or partially
defined" values are outweighed by the dangers of accidentally proving
theorems that are too weak by mis-using these constants. Maybe we
should use a logic which handles partial functions for this type
of work.

         Paul Loewenstein, National Semiconductor Corporation.

New mail address until end October 1989: paul@sierra.stanford.edu