Return-Path: Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.0) id <03543-0@swan.cl.cam.ac.uk>; Thu, 23 Apr 1992 13:08:11 +0100 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA02257; Thu, 23 Apr 92 04:55:15 -0700 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Received: from swan.cl.cam.ac.uk by ted.cs.uidaho.edu (16.6/1.34) id AA02253; Thu, 23 Apr 92 04:55:08 -0700 Received: from guillemot.cl.cam.ac.uk by swan.cl.cam.ac.uk with SMTP (PP-6.0) to cl id <03232-0@swan.cl.cam.ac.uk>; Thu, 23 Apr 1992 12:54:55 +0100 To: btg@uk.ac.cam.cl Cc: windley@edu.uidaho.cs.panther, info-hol@edu.uidaho.cs.ted, Tom.Melham@uk.ac.cam.cl Subject: Re: mutual recursion In-Reply-To: Your message of Thu, 23 Apr 92 10:04:14 +0100. <"swan.cl.ca.513:23.03.92.09.04.22"@cl.cam.ac.uk> Date: Thu, 23 Apr 92 12:54:51 +0100 From: Tom Melham Message-Id: <"swan.cl.ca.242:23.03.92.11.55.08"@cl.cam.ac.uk> Regarding Brian's recent message: > 2. The form of theorem returned by the above grammar will look like: > > |- !f1 f2 f3 f4 f5 f6 f7. > ?! x1 x2. > ( x1 B1 = f1) /\ > > ... etc ... > > Defining an induction theorem from this would be a desirable > next step. > > ... etc ... > > I believe that this result is NOT obtainable however. The nested > unique existence quantifiers in the theorem characterizing the > datatypes suggest that we want to derive a uniqueness property > somwhat like the following example: > > (?! x y. P(x,y)) ==> > !x x' y y'. (P (x,y) /\ P(x',y')) ==> (x = x') /\ (y = y') > > ... etc. I am very surprised that "the form of the theorem returned" is that shown above. This is, as Brian rightly guessed, incorrect. Instead, it must assert simultaneously the unique existence of a PAIR of functions: |- !f1 f2 f3 f4 f5 f6 f7. ?! (x1,x2). (x1 B1 = f1) /\ ... etc Otherwise, the theorem does not correctly characterize the required recursive data type (= initial algebra). Note in general that, unlike ordinary existence, unique existence does not "commute" (to coin a term): |- ~ !P. ?!x y. P[x,y] = ?!y x. P[x,y] The technical report from Aarhus gets it right (I think---I haven't got it to hand), so I'm a bit surprised that the package returns the wrong theorem. By the way, anyone interested in mutual recursive data types may find this report useful. If there's sufficient interest, I could post a little example of how to do a quick-and-dirty mutual recursive data type definition "by hand"... Tom