Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: list
To: Einar-A.Snekkenes@ffi.no
Cc: info-hol@leopard.cs.byu.edu, tfm@dcs.gla.ac.uk
Subject: Re: Why "Extension by type specification" ?
In-Reply-To: Your message of "Fri, 07 Apr 1995 13:56:12 +0200." <"1278 95/04/07 13:56*/G=Einar-A/S=Snekkenes/O=ffi/PRMD=uninett/ADMD= /C=no/"@MHS>
Date: Wed, 12 Apr 1995 17:19:49 +0100
From: Tom Melham <tfm@dcs.gla.ac.uk>
Message-ID: <"swan.cl.cam.:270360:950412172647"@cl.cam.ac.uk>


In a recent message, Einer Snekkenes asked an interesting question
about type specifications:

> I've had a look at "Introduction to HOL" by M.J.C. Gordon
> and T.F. Melham. In chapter 16 they present two ways
> of extending a theory with a new type:
> 
>   1. Extension by type definition.
>   2. Extension by type specification.
> 
> (1) is a special case of (2).
> For $\Gamma=\{\}$ it seems like (2) can be obtained from (1) by applying
> MP and INST_TYPE (see below).
> I cannot see how (2) provides a significantly a more 
> abstract way of defining new types. 
> 
> What is it I'm missing?

The difference between type specification and type definitions
does not lie in what you *can* infer from each of them -- Einar
quite correctly points out that you can implement (2) from
(1) -- but in what you *can't* infer.

Here's a little example that explains the difference.  Suppose we
wish to define a type, :two say, about which we know only that it
has *at least* two distinct elements. Note that we specifically do
not want to know (i.e. be able to prove something about) exactly
how many elements the type has.

Using type specification, we would proceed as follows.  First, to
make the discussion a bit more readable, abbreviate

     type1 ~ P:type2->bool

to stand for

     ?f:type1->type2. Type_Definition P f

Now do this:

  1) prove 

        |- (:* ~ \x:bool.T) ==> ?a:*. ?b:*. ~(a = b)         [thm 1]

  2) introduce type :two using a type specification

        |- ?a:two. ?b:two. ~(a = b)                          [thm 2]

We now have a type :two, about which *all* we know is that theorem
2 holds.  Note that we *cannot* infer that :two is in bijection
with :bool, and hence that is "really" has exactly two elements.
We have no idea how exactly many elements :two has.

Now, following Einar's scheme for faking type specification using
type definitions, we would proceed as follows

  1) as before, prove 

        |- (:* ~ \x:bool.T) ==> ?a:*. ?b:*. ~(a = b)         [thm 3]

  2) using the type definition rule, introduce :two by

        |- :two ~ \x:bool.T                                  [thm 4]

  3) by type instantiation and modus ponens, we get 

        |- ?a:two. ?b:two. ~(a = b)                          [thm 5]


Sure enough, theorem 5 is the same as theorem 2.  But wait!  Our
theory in the second derivation will also contain the type
definition, i.e. theorem 4.  And from this we *will* be able to
prove that :two has exactly two elements.  We have thus failed to
enforce an abstraction away from the representation.

I hope this makes matters a bit clearer.

Tom