Return-Path: Delivery-Date: Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Thu, 14 Oct 1993 10:52:27 +0100 Received: by leopard.cs.byu.edu (1.37.109.4/16.2) id AA07787; Thu, 14 Oct 93 03:38:32 -0600 Sender: info-hol-request@leopard.cs.byu.edu Errors-To: info-hol-request@leopard.cs.byu.edu Precedence: bulk Received: from dworshak.cs.uidaho.edu by leopard.cs.byu.edu with SMTP (1.37.109.4/16.2) id AA07783; Thu, 14 Oct 93 03:38:31 -0600 Received: from ganymede.inmos.co.uk by dworshak.cs.uidaho.edu with SMTP (1.37.109.4/16.2) id AA15792; Thu, 14 Oct 93 02:38:20 -0700 Received: from frogland.inmos.co.uk by ganymede.inmos.co.uk; Thu, 14 Oct 93 10:35:48 BST From: David Shepherd Message-Id: <26351.9310140934@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 10:34:55 +0100 (BST) In-Reply-To: <9310140407.AA13727@maui.cs.ucla.edu> from "chou@CS.UCLA.EDU" at Oct 13, 93 09:07:35 pm X-Mailer: ELM [version 2.4 PL20] Content-Type: text Content-Length: 1570 chou@CS.UCLA.EDU has said: > > I am verifying some distributed programs and need to deal with > big pairs (around 10 components). I found that HOL can be very > inefficient when processing big pairs, as the following session > shows. The conversion PUSH_IN_CONV pushes the first of sequence > of existential quantifiers all the way in: you call 10 big! .... try it with 30 or 40! Seriously, large tuples is something I had big problems with. The problem is that `? (a,b). P` is actually `$? (UNCURRY \a b. P)` So in your example where P is ?z. Q and you want to swap the exist binders around it is no longer just a matter of swapping two constructs but you have to pull one ? through an UNCURRY-ed term which takes much more effort. Basically, the HOL parser and pretty printer isolate the user from a large amount of underlying term structure so that terms thato on the outside look quite simple can be very complex! I felt that the only way of dealing with tuples efficiently would be to put tuples into the core logic and allow lambda abstraction on them. The problem then is that you probably need a whole family of primitive type operators ('a)tuple1, ('a,'b)tuple2, ('a,'b,'c)tuple3 I think that Veritas has uses tuples as a primitive concept. -------------------------------------------------------------------------- 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