Received: from scaup.cl.cam.ac.uk by Steve.CL.Cam.AC.UK with SMTP/TCP/IP over Ethernet id a003025; 27 Oct 88 3:23 BST Via: uk.ac.ucl.cs.nss; 27 Oct 88 2:20 GMT (UK.AC.Cam.Cl.scaup) Received: from clover.ucdavis.edu by NSS.Cs.Ucl.AC.UK via Satnet with SMTP id aa00844; 27 Oct 88 2:37 BST Received: from cheetah.ucdavis.edu by clover.ucdavis.edu (5.59/UCD.EECS.1.1) id AA16588; Wed, 26 Oct 88 18:39:01 PDT Received: by cheetah.ucdavis.edu (AIX 2.2/3.14) id AA03218; Wed, 26 Oct 88 18:46:42 PDT Message-Id: <8810270146.AA03218@cheetah.ucdavis.edu> Qotw: In any organization, there will always be one person who knows what is going on; eventually, this person will be fired. Pointers: (916) 752-7324/3168 To: info-hol@edu.ucdavis.clover Subject: type definitions Date: Wed, 26 Oct 88 18:46:41 -0800 From: Phil Windley Sender: windley Status: RO I'm trying to define a few new types in HOL. I defined a type stack without too much trouble. I now want to define a type called symtab for symbol tables. The problem is that the selectors on symbol tables are both recursive and paramterized (either one would present problems). For example, the selector "retrieve" looks like this: retrieve (addid symtab id attrlist) id' = (id = id') => attrlist | retrieve symtab id' where addid is one of the symbol table constructors. This is different than lists or stacks where the selectors are neither recursive nor parameterized (note that retrieve selects based on id'). Has anyone had experience defining these types like this? I'd be grateful for any pointers that I could get. P.S. The goal of all this is to duplicate in HOL the kind of verifications that are done in AFFIRM (ala Guttag, Horowitz, and Musser). --phil-- Phil Windley | windley@iris.ucdavis.edu Division of Computer Science | ucbvax!ucdavis!iris!windley College of Engineering | (916) 752-7324 (or 3168) University of California, Davis | Davis, CA 95616