Delivery-Date: 
Sender: info-hol-request@leopard.cs.byu.edu
Errors-To: info-hol-request@leopard.cs.byu.edu
Precedence: bulk
From: David Shepherd <des@inmos.co.uk>
Message-Id: <1410.9311241046@frogland.inmos.co.uk>
Subject: Re: Need "an undefined value", but not what you think.
To: shaw@cs.ucdavis.edu (Rob Shaw)
Date: Wed, 24 Nov 1993 10:46:00 +0000 (GMT)
Cc: info-hol@cs.uidaho.edu (info-hol mailing list)
In-Reply-To: <9311240707.AA20685@mahogany.cs.ucdavis.edu> from "Rob Shaw" at Nov 23, 93 11:07:07 pm
Content-Type: text
Content-Length: 3699

Rob Shaw has said:
> 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. For instance,
> 
>  does 23/0 = 22/0 ?
> 
> In certain circles the answer is arguably "maybe", in the sense
> that you shouldn't be able to prove or disprove the above equality.
> My concern is with elements "beyond" the end of a list, such as 
> 
>  (EL 9 [1;2;3])
> 
> It turns out this is provably equal to (EL 10 [0;1;2;3]), as the
> theorem
> 
>  ! lst i e. (EL i lst) = (EL (SUC i) (CONS e list))
> 
> has a one-line proof. Why is (EL 9 [1;2;3]) equal to some term 
> other than itself? It is not as undefined as I would like! Is 
> it somehow equal to (EL 9 [2;3;4]) or to (EL 8 [1;2;3])? I want
> to eventually work with a version of lists such that indexing 
> beyond the end of one is "an undefined value" in the way that
> 12/0 is "an undefined value". But I can't just define myEL to be 
> something like
> 
> myEL i l = (i in bounds) => (EL i l) | UNDEF
> 
> because UNDEF = UNDEF, which is not what I want. Is there any way
> for me to define lists such that (EL 9 [1;2;3]) can be proved
> neither equal nor unequal to any term that is not (EL 9 [1;2;3]) ??

This used to be a problem in general as in HOL you had to give
a "total" definition for any function. Back in the days pre-Hol88
things like DIV and MOD were, I seem to recall, defined in terms of
"@" expressions so that then I expect |- 23 DIV 0 = 22 DIV 0 
as each side would be (@ n. F).

This was a problem (especially I think to the ICL people who were
trying to embed Z semantics into HOL where the idea of an undefined
value has different semantics from (@ x. F)) and various work rounds
were used, such as the idea of a "parameterised" unknown so that you
used different instances in different places. However, this was not
pleasant.

The solution was to introduce the "loose specification" mechanism into
HOL whereby you prove the existence of a term to satisfy a definition
and the you define a constant satisfying the definition. In this way
you can leave undefined in the definition the things that you want to
leave undefined -- i.e. you do not define them to be undefined, you
just make no statement about them so that then nothing can be inferred
from them.

The problem with EL probably stems from the fact that no-one has
updated that definition to use loose definition (perhaps due to a fear
that someone *does* use the fact that out of range EL's return the same
value?) - however, DIV and MOD now have a new loose specification based
on the normal definition of the division.

For EL what needs to be done is instead of (in HOL90 syntax) the
definition:

val EL = new_recursive_definition
      {name = "EL",
       fixity = Prefix,
       rec_axiom = num_Axiom,
       def = --`(!l. EL 0 l = (HD l:'a)) /\
                (!l:'a list. !n. EL (SUC n) l = EL n (TL l))`--};

First a proof that

`? EL. (!x l. EL 0 (CONS x l) = x) /\
       (!x l n . EL (SUC n) (CONS x l) = EL n l)`

then using new_specification on this.

From this you will find that

|- EL 9 [1,2,3] = EL 6 []

and  

|- EL 8 [1,2,3] = EL 5 []

But you can neither prove or disprove 

--`EL 9 [1,2,3] = EL 8 [1,2,3]`--

which is perhaps what you mean by "undefined".

N.b. similar redefinitions, perhaps, ought to be done to HD and TL so
that their application to [] is unspecified?

--------------------------------------------------------------------------
david shepherd: des@inmos.co.uk                     tel: 0454-616616 x 625
                inmos ltd, 1000 aztec west, almondsbury, bristol, bs12 4sq
		"you might think that   ---   I couldn't possibly comment"