Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Tue, 22 Jun 1993 16:33:02 +0100 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA04433; Tue, 22 Jun 93 08:20:38 -0700 Sender: info-hol-request@ted.cs.uidaho.edu Errors-To: info-hol-request@ted.cs.uidaho.edu Precedence: bulk Received: from tuminfo2.informatik.tu-muenchen.de by ted.cs.uidaho.edu (16.6/1.34) id AA04428; Tue, 22 Jun 93 08:20:30 -0700 Received: from sunbroy14.informatik.tu-muenchen.de ([131.159.0.114]) by tuminfo2.informatik.tu-muenchen.de with SMTP id <57654>; Tue, 22 Jun 1993 17:20:31 +0200 Received: by sunbroy14.informatik.tu-muenchen.de id <8082>; Tue, 22 Jun 1993 17:20:13 +0200 From: Konrad Slind To: info-hol@ted.cs.uidaho.edu Subject: SML and Classic ML Message-Id: <93Jun22.172013met_dst.8082@sunbroy14.informatik.tu-muenchen.de> Date: Tue, 22 Jun 1993 17:20:01 +0200 Paul Loewenstein writes: > I would love to see more encouragement to make the switch, possibly > by a policy of introducing significant new features and proof procedures > to HOL90 first. Some proof procedures depend on having arrays (in AC unification, arrays are used for solving linear homogeneous diophantine equations; using lists or search trees would make things unbearably slow in my judgement, although I haven't tested it). Since Classic ML doesn't have arrays, the implementation of AC unification in hol88 would require dropping down into lisp. This is not acceptable, for now the implementation of the algorithm is in 2 languages and it becomes a maintenance nightmare. Further, in hol88, any algorithms that depend on hashing would need to be partly implemented in Lisp. Konrad.