Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: list
From: Rob Arthan <rda@win.icl.co.uk>
Date: Fri, 29 Sep 95 14:20:38 BST
Message-Id: <9509291320.13300.0@win.icl.co.uk>
To: info-hol@leopard.cs.byu.edu, leonard@ricks.enet.dec.com
Subject: Re: Synonymous types

Tim Leonard asks:
 
> 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.

>I was thinking the other day about
> how unfortunate it is that one must choose between alternative implementations
> of things like integers, when each implementation's supporting library has
> advantages, and the two types are actually describing the same objects.

I had a closely related problem constructing the linear arithmentic
proof procedure for Z in ProofPower. This works by using the proof
procedure for ProofPower-HOL integers. In this case, the two types are
the same but the operations are different: very approximately, in HOL,
addition, multiplication etc. are represented as HOL functions in the
usual way, while the Z operations are represented sets of pairs. The
definitions of the operations are quite independent, but, not
unsurprisingly, give the same underlying mathematical structure.  To
relate the two, you prove theorems showing (roughly) that the identity
function on the type preserves the additive and multiplicative
structure, and then use these in conversions to translate Z formulae
into equivalent HOL ones and back again. This works, but it is heavily
dependent on the fact that I am working with two different treatments
of the same well understood thing, namely the integers (OK, it would
work more or less for an arbitrary ring).

>I
> wondered if it would be possible to prove that the two types were the same, and
> thereafter be able to treat them as synonyms.  I couldn't see how to make that
> work, but the next best thing, automated conversion between the two, seems
> workable and potentially useful. 
> 
> Given two types defined by specification, and proofs that the two specs are
> equivalent, it seems to me it should be possible to automatically derive
> mapping theorems for rewriting theorems about objects of one type into theorems
> about objects of the other, and it should be easy to wrap shells around derived
> rules (and theorem-tactics, etc.) from one theory to create equivalent rules
> for the other theory.  (All this is assuming the two theories avoid name
> conflicts, which I recognize is a bad assumption, but that seems an
> uninteresting issue.) 
> 
> Since I didn't know that anyone else has already thought about it, I thought
> I'd bring it up.  Do you see a way of making two existing types synonyms?  If
> not, do you think mechanisms for converting between equivalent types would be
> useful?
> 

I suspect the hard part is coming up with an implementable, useful and
adequately general formulation of what it means for the two specs to be
equivalent.  I dare say you would have to look at a number of realistic
examples to invent something worthwhile. Are there many useful examples
which you could reasonably expect to handle automatically?

Rob Arthan (rda@win.icl.co.uk)