Delivery-Date: 
Sender: hol2000-request@lal.cs.byu.edu
Errors-To: hol2000-request@lal.cs.byu.edu
Precedence: bulk
From: David Shepherd <des@inmos.co.uk>
Message-Id: <24175.9405251145@frogland.inmos.co.uk>
Subject: Re: Basic changes
To: Richard.Boulton@cl.cam.ac.uk (Richard Boulton)
Date: Wed, 25 May 1994 12:45:24 +0100 (BST)
Cc: hol2000@leopard.cs.byu.edu
In-Reply-To: <"swan.cl.cam.:061420:940525091240"@cl.cam.ac.uk> from "Richard Boulton" at May 25, 94 10:12:19 am
Content-Type: text
Content-Length: 2899

Richard Boulton has said:
> Konrad Slind writes:
> 
> > IMHO, there could be some interesting changes made:
> >    .
> >    .
> >     - term: a more detailed (and hence more efficient) lambda-calculus, 
> >       perhaps with pairing or records "built-in"; 
> 
> Currently there are only two kinds of branch node in the trees that represent
> terms: COMB (combinations, i.e., function applications) and ABS
> (lambda abstractions). As Konrad says, having other constructs as basic (when
> currently they are represented in terms of COMB and ABS) can make some things
> more efficient, and easier. However, there is a price: programs operating over
> terms become more complex because all the new cases have to be dealt with.
> In my opinion, one of the beauties of the HOL logic is the simplicity of just
> having COMB and ABS, and it is not something that should be given up lightly.
> Having said that, there is a strong case for making abstractions over tuples
> built-in. In fact, is there any reason why such a construct can't subsume the
> existing ABS, it being taken as the special case in which the tuple has one
> component?

Given that in HOL90 abstraction uses de Bruijn indexing, I think that it
shouldn't be too difficult - the indexes just expand to a "level" and
an item in that level.

Of course, the next item on the agenda is do you just want to support

	--`\ (x,y,z). P x y z`--

in the object language or do you want to support general tuples like

	--`\ (x,(y,z),(((a,b),c),d` . <etc>`--

... I think that the former satisfies most needs with the latter still
being handled by the current UNCURRY methods.

BETA_CONV probably becomes slightly, but not greatly, different as I
would assume that it would only apply when the argument to the
application is of the same direct "form" as the abstracted tuple. I.e.

	BETA_CONV(--`(\ (x,y) . x+y)(1,2)`--)
	= |- (\ (x,y) . x+y)(1,2) = 1+2

but

	BETA_CONV(--`(\ (x,y) . x+y)z`--)

would result in an error (a derived rule could do the splitting of z
into (FST z,SND z)). This is (partly) motivated by the issue of where
tuples/pairs come in the logic ... I think do do this cleanly then the
definition of pairing has to move to the status of an axiom as the
extended BETA_CONV cannot be "properly" defined until pairing  is.
Note, this does not bring in pairs as an object language construct but
via an axiomatic definition of the pairing operator.

Note that this could introduce a need for new cases in proof functions
as BETA_CONV would not always succede in patterns where it always used
to (i.e. lambda abstraction applied to an argument).

--------------------------------------------------------------------------
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."