Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
From: David Shepherd <des@inmos.co.uk>
Message-Id: <3893.9405110930@frogland.inmos.co.uk>
Subject: Re: Lists in HOL
To: shaw@cs.ucdavis.edu (Rob Shaw)
Date: Wed, 11 May 1994 10:30:48 +0100 (BST)
Cc: info-hol@cs.uidaho.edu
In-Reply-To: <9405102243.AA11792@ice.cs.ucdavis.edu> from "Rob Shaw" at May 10, 94 03:43:32 pm
Content-Type: text
Content-Length: 2743

Rob Shaw has said:
> Within HOL, is the following term provably false?
> 
> ? (i:num) . 17 = EL i []
> 
> My understanding is that, with the given axiomatization of lists, you
> can't say anything about, say, element twelve of the empty list (other
> than it is the same as element 13 of [1]). 

Your understanding is, I think, correct.

for a given i, then

	EL i [] = HD(TL( ... TL[]) ...))

where there are i TL's

the only info we have about HD and TL are

	HD(CONS h t) = h
	TL(CONS h t) = t

both are left unspecified when applied to [].

Hence, it is quite possible (i.e. we cannot prove that is isn't the case)
that 

	HD [] = 17
	TL [] = []

In which case 

	!i. 17 = EL i []

Having "loose specifications" which are "partial" - i.e. only specify
over the intended domain - adds some safety to proofs in that, as you
have discovered, you can't infer things from outside the domain of the
functions definition.

Without loose specifications you have to "totalize" such functions and
give an explicit value - however you can use the "@" binder to help.

E.g.
	TL l = @ t. ? h. l = CONS h t

would be a total definition of TL. In this case 

	TL [] = @ t. F

so again you can't infer much from it (although now you could prove
that it was equal to anything else that reduced to @ t. F)

A good example of a totalised functions are PRE and SUB

	(!m. PRE m = ((m = 0) => 0 | @n. m = SUC n))

	(!m. 0 - m = 0) /\
	(! m n. SUC m - n = ((m < n) => 0 | (SUC (m - n)))

Which have "anomalies" such as

	PRE 0 = 0
	3 - 5 = 0

The result is that there is a danger that someone uses "-" thinking
it is the usual additive inverse and proves, for example, that

	|- f x - g y = 0

and intuituively interprets this as being

	|- f x = g y

while in reality it is actually

	|- f x <= g y

They could have been loosely specified by

	PRE(SUC n) = n

	(!m. m - 0 = m) /\
	(!m n. m - (SUC n) = PRE(m - n))

Then the "anomalies" disappear as things like PRE 0 and 3 -5 cannot be
reasoned about. However, I suspect that when loose specifications came
in that it was thought that too much arithmetic theoruy already existed
using the total definitions to permit a change (note that changes were
made for division and lists etc)

Of course, you can do it all "properly" by having partial functions
where things like PRE 0 are specificied as being undefined ... however,
it seems that experience from Lambda has shown market resistance to the
use of  partial functions!

--------------------------------------------------------------------------
david shepherd: des@inmos.co.uk                     tel: 0454-616616 x 625
                inmos ltd, 1000 aztec west, almondsbury, bristol, bs12 4sq
		"I  am  not  a  nut      ---      I  am  a  human  being."