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: <26903.9310141433@frogland.inmos.co.uk>
Subject: Re: Inefficiency when processing big pairs
To: info-hol@cs.uidaho.edu (info-hol mailing list)
Date: Thu, 14 Oct 1993 15:33:44 +0100 (BST)
In-Reply-To: <"swan.cl.cam.:276960:931014131057"@cl.cam.ac.uk> from "John Harrison" at Oct 14, 93 02:08:29 pm
Content-Type: text
Content-Length: 3042

John Harrison has said:
> On the subject of a more efficient implementation of pairs, the following may
> be worth thinking about. Observe that:
> 
>   (\x. s[x]) = @f. !x. f x = s[x]
> 
> This has a natural extension to pairs:
> 
>   (\(x,y,z). s[x,y,z]) = @f. !x y z. f (x,y,z) = s[x,y,z]
> 
> So how about *defining* paired abstraction this way rather than the current
> prettyprinting? It also extends to more general varstructs, which may not be
> exhaustive, e.g.
> 
>   (\(CONS h t). s[h,t]) = @f. !h t. f (CONS h t) = s[h,t]
> 
> I haven't thought it through carefully, but the varstruct which you are
> (intuitively) abstracting over is actually *there* in the basic term, so it
> might well be more efficient for operations. Anyone have any thoughts on 
> this?

Interesting idea (especially when it suddenly dawned on me that by
s[x,y,z] you weren't apply the fuction s to a list of 3 elements :-)
However, consider the original conversion to prove

--`? (x,y,z). ? a. P[a,x,y,z] = ?a. ? (x,y,z). P[a,x,y,z]`--

Under this scheme this is

--`$? (@f. ! x y z. f(x,y,z) = $? (@f'. ! a. f' a = P[a,x,y,z])) =
   $? (@f'. ! a. f; a = $? (@f. ! x y z. f(x,y,z) = P[a,x,y,z]))`--

which looks to be a bit tricky to me!

Thinking a bit more about it I think, certainly in HOL90, it
would be possible to do something along the lines of the way
Veritas handles things.

The key is the fact that hol90 uses Be Bruijm style indexing
of bound variables. This is simply extend so that instead
of indexing a level of abstraction you index a level + a tuple element
in that level.

i.e.

	--`\ (a,b). \c. a+c = b`--

would be encoded as

	Abs [a,b] (Abs c (Bv(1,0) + Bv(0,0) = Bv(1,1))

(N.b. [a,b] is a list in the SML representation *NOT* in the object
language)

Effectively the term language encodes the unpaired version of
the term

	--`\ ab. \c. (FST ab) + c = (SND ab)`--

and so none of the UNCURRY-ing stuff is needed.

The only downside of this is (apart from having to rewrite all the
bound variable code!) that you may have to make the type operator
"pair" a primitive? Though, actually, it could still be derived
so long as the code you use to derive it doesn't try to do
a tupled abstraction.

Returning to the example we start with the term

--`$? (ABS [x,y,z] ($? (ABS [a] (P[Bv(0,0),Bv(1,0),Bv(1,1),Bv(1,2)]))))`--

This would be simply converted with SWAP_EXISTS_CONV and the
bound variable code would (I hope) cope with the renamings to produce

--`$? (ABS [a] ($? (ABS [x,y,z] (P[Bv(1,0),Bv(0,0),Bv(0,1),Bv(0,2)]))))`--

What does anyone thing of this ... or more to the point, anyone (i.e.
Konrad!) know if this is implementable?

Note, that it is an upward compatible extension - old style abstraction
is a subset of this.

--------------------------------------------------------------------------
david shepherd: des@inmos.co.uk                     tel: 0454-616616 x 625
                inmos ltd, 1000 aztec west, almondsbury, bristol, bs12 4sq
                Latest football score: Real Madrid:1, Surreal Madrid:lemon