Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.4); Tue, 12 Jan 1993 14:51:28 +0000 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA22476; Tue, 12 Jan 93 06:41:00 -0800 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Precedence: bulk Received: from swan.cl.cam.ac.uk by ted.cs.uidaho.edu (16.6/1.34) id AA22470; Tue, 12 Jan 93 06:40:48 -0800 Received: from auk.cl.cam.ac.uk (user jrh (rfc931)) by swan.cl.cam.ac.uk with SMTP (PP-6.4) to cl; Tue, 12 Jan 1993 14:39:21 +0000 To: KIKUCHI Yutaka Cc: info-hol@edu.uidaho.cs.ted Subject: Re: APPLY function on HOL In-Reply-To: Your message of Tue, 12 Jan 93 22:57:54 +0200. <9301121357.AA05118@jevex.cs.titech.ac.jp> Date: Tue, 12 Jan 93 14:39:09 +0000 From: John Harrison Message-Id: <"swan.cl.ca.767:12.01.93.14.39.45"@cl.cam.ac.uk> Hi, You write: > 1. > I want to define a function that takes two arguments, > the first one is an arbitrary type function, > the second one is an argument for the first. > For example, we can use APPLY function in LISP for the perpose. > (apply #'+ '(1 2 3)) => 6 The type system of HOL won't let you define such functions with quite the abandon of LISP. However the function ITLIST ("iterate on list") defined as follows may do what you want: let ITLIST = new_list_rec_definition(`ITLIST`, "(ITLIST (f:*->**->**) [] x = x) /\ (ITLIST f (CONS hd tl) x = f hd (ITLIST f tl x))");; This is a precise counterpart of the ML function |itlist|, which would probably be defined in a very similar way (though I think it's actually coded in LISP for speed). This is a "classic" combinator in functional programming languages, though it's now more common to see it called something like "fold". All sorts of list operations can be defined in terms of it, with a little ingenuity. A real-life example in the HOL system is: let GENL = itlist GEN;; An example of |itlist| similar to the one you suggest is: #itlist (curry $+) [1; 2] 3;; 6 : int (You wouldn't need |curry| at the HOL level: $+ is already curried there.) Perhaps closer to what you had in mind is the associated function |end_itlist| #end_itlist (curry $+) [1; 2; 3];; 6 : int A counterpart in HOL could certainly be defined, but it would be convenient to use the functions in the |more_list| library for taking lists apart from the `wrong' end. > 2. > "node [node [node []];node[]]";; > causes an error as the following > skipping: ] ; node [ ] ] " ;; parse failed > in HOL ver.2.01, although it is acceptable in HOL ver.2.00. > > "node [node [];node [node []]]";; > makes no error in the both versions. > > Is it a bug of HOL2.01 or something wrong with me? The former I think! Someone else will have to answer this in detail, but my guess is that it's a side-effect of fixing the following bug in 2.0, which works in 2.01: #"[1 = 2]";; bad list separator skipping: 1 = 2 ] " ;; parse failed John.