Delivery-Date: 
Sender: info-hol-request@leopard.cs.byu.edu
Errors-To: info-hol-request@leopard.cs.byu.edu
Precedence: bulk
Date: Wed, 24 Nov 93 10:49:59 -0500
From: guttman@linus.mitre.org
Message-Id: <9311241549.AA01777@nausicaa.mitre.org>
To: shaw@cs.ucdavis.edu (Rob Shaw)
Cc: info-hol@cs.uidaho.edu
In-Reply-To: shaw@cs.ucdavis.edu's message of 24 Nov 1993 07:30:59 GMT
Subject: Need "an undefined value", but not what you think.

> I may eventually need to denote "an undefined value" in HOL, in 
> such a way that it isn't even reflexive. This is not as strange
> as it sounds. 

You might alternatively consider using a different proof system such as Imps,
in which partial are handled directly.  That is, 23/0 is simply undefined.  An
*atomic* formula with an undefined immediate subterm is *false*, so that 23/0 =
22/0 is false.  (No "maybe" about it, though.)  The logic above the level of
atomic formulas is perfectly classical.  

The Imps simplifier uses algorithms that exploit a lot of information about the
domain and range of fns (for instance, which fns have been proved total) to
relieve the user of the bulk of tedious definedness reasoning.

Imps is available for ftp (along with a number of papers) from
harvard.math.edu:/imps

I'd be happy to give you more info if you're interested.  

	Josh