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; Fri, 17 Jun 1994 10:17:51 +0100 Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA26605; Fri, 17 Jun 1994 02:57:47 -0600 Sender: info-hol-request@lal.cs.byu.edu Errors-To: info-hol-request@lal.cs.byu.edu Precedence: bulk Received: from dworshak.cs.uidaho.edu by leopard.cs.byu.edu with SMTP (1.37.109.8/16.2) id AA26601; Fri, 17 Jun 1994 02:57:32 -0600 Received: from oberon.inmos.co.uk by dworshak.cs.uidaho.edu with SMTP (1.37.109.8/16.2) id AA23137; Fri, 17 Jun 1994 01:55:54 -0700 Received: from frogland.inmos.co.uk by oberon.inmos.co.uk; Fri, 17 Jun 1994 09:55:45 +0100 From: David Shepherd Message-Id: <1632.9406170853@frogland.inmos.co.uk> Subject: Re: how fast is hol90's function theorem? To: reetz@ira.uka.de (reetz) Date: Fri, 17 Jun 1994 09:53:19 +0100 (BST) Cc: info-hol@cs.uidaho.edu In-Reply-To: <"i80fs2.ira.938:17.05.94.08.12.36"@ira.uka.de> from "reetz" at Jun 17, 94 10:12:29 am X-Mailer: ELM [version 2.4 PL20] Content-Type: text Content-Length: 954 reetz has said: > I need a fast function to get a certain collection of alreay > stored theorems in HOL90.6. Normally, looking for a theorem > "bla" in theory "bli", one uses > > theorem "bli" "bla"; > > However, I would like to know how fast is it's implementation > to estimate whether it is worth to program my own data structure > to find things even faster. Assume there are n theorems in theory "bli", > how long taks theorem "bli" to look for a certain theorem "bla", > e.g. O(n), O(log n) ? ? how about looking in the source code ? A simple search shows that theorem uses grab_item which in turn uses assoc1. assoc1 is a linear search, hence it's O(n). -------------------------------------------------------------------------- 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."