Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.4) outside ac.uk; Wed, 10 Mar 1993 09:07:26 +0000 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA04869; Wed, 10 Mar 93 00:41:34 -0800 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Precedence: bulk Received: from relay.pipex.net by ted.cs.uidaho.edu (16.6/1.34) id AA04862; Wed, 10 Mar 93 00:40:58 -0800 X400-Received: by mta relay.pipex.net in /PRMD=pipex/ADMD=cwmail/C=GB/; Relayed; Wed, 10 Mar 1993 08:39:31 +0000 X400-Received: by /PRMD=icl/ADMD=gold 400/C=GB/; converted (ia5 text (2)); Relayed; Wed, 10 Mar 1993 08:36:36 +0000 Date: Wed, 10 Mar 1993 08:36:36 +0000 X400-Originator: R.B.Jones@uk.co.icl.wins.win0109 X400-Recipients: info-hol@edu.uidaho.cs.ted X400-Mts-Identifier: [/PRMD=icl/ADMD=gold 400/C=GB/;win0109 0000012600002381] Original-Encoded-Information-Types: undefined (0) X400-Content-Type: P2-1984 (2) Content-Identifier: 2381 From: R.B.Jones@uk.co.icl.wins.win0109 Message-Id: <"2381*/I=RB/S=Jones/OU=win0109/O=icl/PRMD=icl/ADMD=gold 400/C=GB/"@MHS> To: info-hol@edu.uidaho.cs.ted Subject: "overloading" in ProofPower-HOL I thought there were two approaches to overloading until Konrad described two, one of which had not occurred to me! ProofPower HOL has "aliases", which are one way of getting overloading just by playing with the parser and pretty-printer without changing the logic. There must be many variations on this purely syntactic approach to overloading. We do use the aliasing mechanisms to achieve overloading, and many such uses are entirely uncontroversial. If people want to make their specifications obscure they will succeed even if denied overloading. We also considered implementing overloading in the logic simply by allowing more liberal rules of conservative extension. This requires no changes to the term structure of HOL or to anything but the definitional mechanisms. All you need to do is arrive at some safe rules which admit a definition if none of the possible instances of the type at which the constants are defined has any overlap with instances previously defined (logically the constant is the name/type pair and there is no more reason to consider the constant "A:bool" the same as the constant "A:num" than there is to consider variables of distinct types the same). You then need some rules for dealing with amibiguities arising in parsing. We didn't do this because the extra benefits were small, and we wanted to stick to the same underlying logic as Cambridge HOL, even down to the rules for conservative extension. Konrad talks of actually changing the term structure, which would presumably make overloading with even fewer constraints logically sound, but only by tagging constants with more information, presumably not normally visible in the concrete syntax. This seems likely to maximise the problems arising from overloading. Roger Jones International Computers Limited R.B.Jones@win0109.wins.icl.co.uk