Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.2); Tue, 24 Nov 1992 10:40:09 +0000 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA08664; Tue, 24 Nov 92 02:11:45 -0800 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Precedence: bulk Received: from ben.uknet.ac.uk by ted.cs.uidaho.edu (16.6/1.34) id AA08659; Tue, 24 Nov 92 02:11:33 -0800 Received: from eros.uknet.ac.uk by ben.uknet.ac.uk via UKIP with SMTP (PP) id ; Tue, 24 Nov 1992 10:08:37 +0000 Received: from eccles.dsbc.icl.co.uk by eros.uknet.ac.uk with UUCP id <1436-0@eros.uknet.ac.uk>; Tue, 24 Nov 1992 10:08:20 +0000 Received: on eccles.dsbc.icl.co.uk over UUCP id AA01304; Tue, 24 Nov 92 10:05:44 GMT Received: from wilfrid by iclbra.oasis.icl.co.uk (4.14/) id AA02463; Tue, 24 Nov 92 10:07:02 gmt From: Rob Arthan Date: Tue, 24 Nov 92 09:57:16 GMT Message-Id: <9211240957.6804.20@win.icl.co.uk> To: toal@edu.ucla.cs Subject: Re: list theorems with destructors Cc: info-hol@edu.uidaho.cs.ted Ray Toal asks which of the following are theorems of HOL: > > "~?n. n = HD[]" > > "~?s. s = TL[]" > > "!n s1 s2. (n = HD s2) /\ (s1 = TL s2) ==> (s2 = CONS n s1)" > > "!s1 s2. (s1 = TL s2) ==> ~NULL s2" > Answer: none of them. Counterexamples are: HD[] = HD[] TL[] = TL[] HD[] = HD[] /\ TL[] = TL[] but ~[] = CONS (HD[]) (TL[]) TL[] = TL[] but NULL[] As Ray points out, HOL functions are total. This is occasionally counterintuitive in that one expects "undefined" things like "TL[]" to be a little bit special; however, it has tremendous advantages in terms of logical simplicity. The "right" intuition to have about something like "TL[]" is that it is some list or other, but you just doesn't know what list it is. So, for example, while you don't know exactly what "HD[]" and "TL[]" denote, you do know that the empty list can't be obtained by applying "CONS" to them. Rob Arthan. (rda@win.icl.co.uk) ICL, Eskdale Rd. Winnersh, Wokingham Berks. RG11 5TT