Return-Path: Delivery-Date: Received: from bescot.cl.cam.ac.uk (user exim (mailer)) by swan.cl.cam.ac.uk with SMTP (PP-6.5) to cl; Wed, 20 Dec 1995 15:22:28 +0000 Received: from leopard.cs.byu.edu [128.187.2.182] by bescot.cl.cam.ac.uk with esmtp (Exim 0.25 #7) id E0tSQL5-00005W-00; Wed, 20 Dec 1995 15:21:56 +0000 Received: by leopard.cs.byu.edu (1.37.109.15/16.2) id AA173041881; Wed, 20 Dec 1995 08:04:41 -0700 Sender: info-hol-request@lal.cs.byu.edu Errors-To: info-hol-request@lal.cs.byu.edu Precedence: list Received: from relay.xlink.net by leopard.cs.byu.edu with SMTP (1.37.109.15/16.2) id AA173001804; Wed, 20 Dec 1995 08:03:24 -0700 Received: from gate.fzi.de by relay.xlink.net id <20907-0@relay.xlink.net>; Wed, 20 Dec 1995 16:02:15 +0000 Received: from ACID0.fzi.de by gate.fzi.de with SMTP (PP) id <22307-0@gate.fzi.de>; Wed, 20 Dec 1995 16:02:04 +0100 Received: from fzi.de by acid0.fzi.de with SMTP (PP) id <16120-0@acid0.fzi.de>; Wed, 20 Dec 1995 16:01:56 +0100 X-Mailer: exmh version 1.6 4/21/95 To: info-hol@leopard.cs.byu.edu X-Url: http://www.fzi.de/eisenbiegler.html Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii Date: Wed, 20 Dec 1995 16:01:47 +0100 From: Dirk Eisenbiegler Message-Id: <"acid0.fzi..122:20.11.95.15.02.00"@fzi.de> I have recently had efficiency problems when building large HOL terms. I figured out, that the very reason for this problem was the mk_abs function. Whenever it is applied, the program traverses the entire term in order to substitute free variables by bound variables. When building large terms with many nested lambda-abstractions, the time consumption increases in a quadratic manner. So I rebuild the HOL system adding two new functions to term.sml: lazy_mk_abs : lazy_mk_abs is equivalent to mk_abs except that the free variables in the body are not bound, i.e. remain free bind_free_vars : binds all free variables within the scope of some lambda abstraction over the same variable When building big terms, I used lazy_mk_abs rather than mk_abs and then finally applied bind_free_vars. This leads to a linear time consumption, since the term is traversed only once. Remark: bind_free_vars uses a hash-table Dirk