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 16:55:27 +0000 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA25903; Wed, 13 Jan 93 08:36:37 -0800 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Precedence: bulk Received: from tuminfo2.informatik.tu-muenchen.de by ted.cs.uidaho.edu (16.6/1.34) id AA25848; Wed, 13 Jan 93 08:35:30 -0800 Received: from sunbroy14.informatik.tu-muenchen.de ([131.159.0.114]) by tuminfo2.informatik.tu-muenchen.de with SMTP id <58000>; Wed, 13 Jan 1993 17:34:16 +0100 Received: by sunbroy14.informatik.tu-muenchen.de id <8121>; Wed, 13 Jan 1993 17:34:06 +0100 From: Konrad Slind To: info-hol@edu.uidaho.cs.ted Subject: parsing, term construction, etc. Message-Id: <93Jan13.173406met.8121@sunbroy14.informatik.tu-muenchen.de> Date: Wed, 13 Jan 1993 17:33:55 +0100 Just to finish beating this subject to death .... Victor writes > Well, yes and no. >> In `\x.x+1` the two occurrences of "x" must have the same type >> because they are in the same scope. > This statement is false (in the strict sence). If you replace the "must" > with a "should" then I agree with you. > You can create a term `\x:bool.(x:num)+1` using constructors. To me this > term does not have much use, but is similar to the terms Ching Tsun was > using when he ran into the renaming problem. I haven't been clear; I was talking about parsing heuristics, where the question is how to give types to variables; there is a choice. Of course, there are no choices for the system to make about types in mk_const, mk_var, mk_comb, and mk_abs. Using the constructor functions, one has total control over types; however these functions ensure that only well-typed terms are built. Antiquotation can also give this degree of control. Here's an example. $ hol90.4 HHH LL HHH LL HHH LL HHH LL HHH OOOO LL HHHHHHH OO OO LL HHHHHHH OO OO LLL HHH OOOO LLLL HHH LL LL HHH LL LL HHH LL LL HHH LL LL90.4 Created on Mon Jan 11 23:24:56 MET 1993 using: Standard ML of New Jersey, Version 0.92, November 18, 1992 The library "HOL" is loaded. - --`(f:num -> bool) ^(--`f:num`--)`-- val it = (--`f f`--) : term - Victor's example and this one show why not all well-typed terms, when prettyprinted, are reparsable to themselves. Konrad.