Return-Path: Return-Path: Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.0) id <04170-0@swan.cl.cam.ac.uk>; Thu, 13 Feb 1992 15:43:59 +0000 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA02555; Thu, 13 Feb 92 07:34:33 -0800 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Received: from swan.cl.cam.ac.uk by ted.cs.uidaho.edu (16.6/1.34) id AA02551; Thu, 13 Feb 92 07:34:23 -0800 Received: from guillemot.cl.cam.ac.uk by swan.cl.cam.ac.uk with SMTP (PP-6.0) to cl id <03998-0@swan.cl.cam.ac.uk>; Thu, 13 Feb 1992 15:36:22 +0000 To: shb@com.oracorp.sparta Cc: info-hol@edu.uidaho.cs.ted Subject: Re: Huge expressions In-Reply-To: Your message of Thu, 13 Feb 92 09:50:12 -0500. <9202131450.AA08108@sparta.oracorp.com> Date: Thu, 13 Feb 92 15:36:16 +0000 From: Tom.Melham@uk.ac.cam.cl Message-Id: <"swan.cl.ca.002:13.01.92.15.36.26"@cl.cam.ac.uk> > My guess is that the main HOL strategy for dealing with huge > subexpressions is not letting them arise in the first place, limiting > rewriting to keep things manageable. I would say that this is an excellent stategy. Perhaps you can use let-terms to eliminate multiple occurences of the same subexpression. Version 1.12 has good support, in the form of let_CONV, for this notation. I should also mention that David Shepherd at INMOS also works with very large expressions. He occasionally finds deeply-buried inefficiencies in the LISP code that make the system very slow for such expressions. Fortunately, he sends us optimizations to fix these problems. I just installed one in, version 2.01, this week... Tom