Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.4); Thu, 7 Jan 1993 17:04:01 +0000 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA07965; Thu, 7 Jan 93 08:50:02 -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 AA07960; Thu, 7 Jan 93 08:49:54 -0800 Received: from LocalHost.cs.ucla.edu by maui.cs.ucla.edu (Sendmail 5.61d+YP/3.21) id AA12631; Thu, 7 Jan 93 00:21:06 -0800 Message-Id: <9301070821.AA12631@maui.cs.ucla.edu> To: info-hol@edu.uidaho.cs.ted (INFO-HOL mailing list) Subject: Unnecessary renaming by BETA_CONV Date: Thu, 07 Jan 93 00:20:59 PST From: chou@edu.ucla.cs Dear HOL gurus: Why does BETA_CONV perform the renaming shown below at all? #BETA_CONV "(\j. (\ i j. i > j)) i";; |- (\j i j. i > j)i = (\i' j. i' > j) #BETA_CONV "(\j. (\ i j. i > j)) j";; |- (\j i j. i > j)j = (\i j. i > j) #BETA_CONV "(\j. (\ i j. i > j)) x";; |- (\j i j. i > j)x = (\i j. i > j) #BETA_CONV "(\i j. (\i j. i > j)) i";; |- (\i j i j. i > j)i = (\j i j. i > j) #BETA_CONV "(\i j. (\i j. i > j)) j";; |- (\i j i j. i > j)j = (\j' i j. i > j) #BETA_CONV "(\i j. (\i j. i > j)) x";; |- (\i j i j. i > j)x = (\j i j'. i > j') One may ask why I'm concerned about this "feature", since no non-theorem is proved after all. But BETA_CONV is used at so many places and such a "feature" can cause unexpected behaviors in other proof procedures, one of which I encountered to my great annoyance. - Ching Tsun