Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Wed, 12 May 1993 13:23:09 +0100 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA14155; Wed, 12 May 93 05:12:59 -0700 Sender: info-hol-request@ted.cs.uidaho.edu Errors-To: info-hol-request@ted.cs.uidaho.edu Precedence: bulk Received: from animal.cs.chalmers.se by ted.cs.uidaho.edu (16.6/1.34) id AA14150; Wed, 12 May 93 05:12:54 -0700 Message-Id: <9305121212.AA03058@animal.cs.chalmers.se> Received: from zoot.cs.chalmers.se by animal.cs.chalmers.se (5.60+IDA/3.14+gl) id AA03058; Wed, 12 May 93 14:12:54 +0200 Received: by muppet77.cs.chalmers.se (5.60+IDA/3.14+gl) id AA00315; Wed, 12 May 93 12:45:51 +0200 To: toal@cs.ucla.edu (Ray J. Toal) Cc: info-hol@ted.cs.uidaho.edu Subject: Re: define_type again In-Reply-To: Your message of "Tue, 11 May 1993 18:14:32 PDT." <9305120114.AA12655@hana.cs.ucla.edu> Date: Wed, 12 May 1993 12:45:47 +0200 From: Andrew Gordon Ray writes: > I was wondering if anyone has ever done something like this: > > type store = Val num | Proc (store -> store) Elsa Gunter has a paper on this problem in the proceedings of HUG92 at Leuven, called "Why we can't have SML style datatype declarations in HOL". In the paper, she considers a grammar that is essentially an extension of yours, but her argument still applies. She gives a set theoretic argument that no set could satisfy the grammar, if -> is the full function space and the constructors are 1-1, and a second argument that an axiomatisation of such a grammar in the style of the define_type tool would be an inconsistent extension of HOL. Domain theory---which uses only continuous functions---is the classical solution to this problem, and LCF the classical computer formulation. I don't know whether Paulson's Cambridge LCF is still available, but I do know there is an implementation of LCF for Isabelle, and that there is ongoing work on implementing domain theory in several implementations of HOL. Andy.