Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: list
To: Rob Arthan <rda@win.icl.co.uk>
Cc: info-hol@leopard.cs.byu.edu, leonard@ricks.enet.dec.com, tfm@dcs.gla.ac.uk
Subject: Re: Synonymous types
In-Reply-To: Your message of "Fri, 29 Sep 1995 14:20:38 -0000." <9509291320.13300.0@win.icl.co.uk>
Date: Sat, 30 Sep 1995 17:46:15 +0100
From: Tom Melham <tfm@dcs.gla.ac.uk>
Message-ID: <"swan.cl.cam.:138110:950930171829"@cl.cam.ac.uk>

>> Has it ever occurred to you to try to merge two implementations of the same
>> type, by proving that they're equivalent?
> 
> One problem is that, as the elements of an HOL type have no internal
> structure in their own right, about the only general definition
> of equivalence you can apply is to say that two types are equivalent iff they
> have the same number of elements. This doesn't help much when what you
> want to do is exploit theorems about operations on one type to get
> theorems about operations on another one. To be useful, the notion of
> equivalence must depend on the structure imposed by the operations
> which characterise the type (e.g., CONS and NIL for lists), and
> there's no completely general way of defining such a notion, as far as
> I know.

Of course for the simple class of "initial algrebras", i.e. the types
definable using the various automatic packages in HOL, there is a
characterization in terms of homomorphisms w.r.t their constructors.  This
immediately gives a natural definition of equivalence.  But Tim was
probably thinking of some more general cases...

Tom