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 09:02:25 +0000 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA22420; Tue, 12 Jan 93 00:35:56 -0800 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Precedence: bulk Received: from Maui.CS.UCLA.EDU by ted.cs.uidaho.edu (16.6/1.34) id AA22414; Tue, 12 Jan 93 00:35:50 -0800 Received: from LocalHost.cs.ucla.edu by maui.cs.ucla.edu (Sendmail 5.61d+YP/3.21) id AA10014; Tue, 12 Jan 93 00:34:54 -0800 Message-Id: <9301120834.AA10014@maui.cs.ucla.edu> To: Konrad Slind Subject: Re: BETA_CONV Cc: info-hol@edu.uidaho.cs.ted (INFO-HOL mailing list) Date: Tue, 12 Jan 93 00:34:53 PST From: chou@edu.ucla.cs Dear Konrad, Thanks for your comments. The HOL88 tests you suggested produced: #BETA_CONV "(\y (x:*) (x:*). T) 1" ;; |- (\y x x. T)1 = (\x x'. T) #BETA_CONV "(\x (y:*). T) (y:bool)" ;; |- (\x y. T)y = (\y. T) as you expected. However, #BETA_CONV "(\x (y:*). T) (y:*)" ;; |- (\x y. T)y = (\y'. T) Three more tests that may interest you are: #BETA_CONV "(\x (y:*). y) (y:*)" ;; |- (\x y. y)y = (\y'. y') #BETA_CONV "(\x (y:*). y) (y:bool)" ;; |- (\x y. y)y = (\y. y) #BETA_CONV "(\x y. x /\ (y > 0)) (y)" ;; |- (\x y. x /\ y > 0)y = (\y. y /\ y > 0) > No spurious renaming occurs in hol90, by the way. For example, none > of Ching Tsun's examples renamed in hol90. What is the time complexity of HOL90's BETA_CONV's renaming algorithm? O(n) or O(n^2), where n is the size of the term being renamed? > I am curious as to why Ching Tsun didn't need to add more type > information to get the terms to parse: sticky_types = true? Good point, I didn't notice this until you mention it. No, I did not use any sticky type. However, in "(\i j. (\i j. i > j))" HOL88 apparently assumes the first i and j are of type :num because the second i and j are. However, "(\i' j'. (\i j. i > j))" does not parse. Yet another peculiarity of HOL88. - Ching Tsun