Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.4); Wed, 13 Jan 1993 22:07:33 +0000 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA26553; Wed, 13 Jan 93 13:27:15 -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 AA26543; Wed, 13 Jan 93 13:27:04 -0800 Received: from LocalHost.cs.ucla.edu by maui.cs.ucla.edu (Sendmail 5.61d+YP/3.21) id AA25696; Wed, 13 Jan 93 13:26:27 -0800 Message-Id: <9301132126.AA25696@maui.cs.ucla.edu> To: Victor "A." Carreno Subject: Re: BETA_CONV Cc: info-hol@edu.uidaho.cs.ted (INFO-HOL mailing list) Date: Wed, 13 Jan 93 13:26:23 PST From: chou@edu.ucla.cs Dear Victor, Suppose t[i] is a term in which i occurs free. Then it is certainly reasonable to assume that the bndvar of \i.t[i] refers to the same i when the term is being parsed; otherwise it would be a real pain to write any term, as you pointed out. However, if i does not occur free in t, there seems to be no good argument as to which bound occurence of i in t the bndvar of \i.t should be identified with. Consider, for instance, "\i. (\i.i)(\i.i+1)" Should the first i be of type num or num->num? As it turned out, HOL88 parser assigns it type num->num, but there seems to be no good argument for it. In fact, I just find out that "\i:num. (\i.i)(\i.i+1)" does NOT parse! - Ching Tsun