Delivery-Date: 
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
Date: Tue, 3 Nov 92 16:24:26 EST
From: symdchon@au.edu.anu.mehta (donald syme )
Message-Id: <9211030524.AA24359@mehta>
To: info-hol@edu.uidaho.cs.ted
Subject: Re: mutually recursive types in HOL
Cc: symdchon@mehta.

Vernon Austel writes:

> 
> In the contrib directory in our distribution of HOL (version 2.0)
> there is a package for defining mutually recursive types.  
> 
> Does this packages work?  
> If so, why is it not part of the standard system?
> What exactly determines whether such a package ``works'',
> i.e. what is accepted as a specification?
>

No doubt others will reply to this also, but anyway...
I have been spending a good deal of my time this year working
with mutually recursive types in HOL.  My summary would be as follows:
   - The package in the contrib directory for HOL2.0 does NOT work,
either under HOL 1.11 when it was originally added (it returns the
wrong theorem I think), nor under HOL2.0, for it uses out-of-date
constructs.

   - Claudio Russo at Edinburgh has implemented a mutually recursive types
package in HOL90.  This works - I have used it this year.  I made
my definitions under HOL90 and then asserted the resulting theorems as
axioms in HOL88.  Given there would be no chance of introducing logical
inconsistency this seems ok.  I have also ported important parts of Claudio's
code such as new_mut_rec_definition to HOL88 2.0 and would be prepared
to make this generally available if people want to use the same method.
It works well - I defined the syntax for Standard ML in HOL, though it took
about 2 hours to run the code and the primitive recursion theorem was
about 200 lines long.

   - The main problems I have been having since results from the need to include
unstructured types such as finite sets, finite maps etc. in the type
structures developed.  This is similar to the problem Tom Melham sent
a solution to some time ago:

   DATA = INT | CHAR | RECORD (DATA)list

though somewhat harder, for instance:

   DATA = INT | CHAR | RECORD (DATA)finite_set

It would seem difficult to find a systematic way of doing this without
resorting to somewhat heavier type theory.


All in all my suggestion would be to either move to HOL90 and use the 
Claudio's package, or do what I did to get a version working under HOL88.
Failing all that just make up the existence & induction theorems yourself.
They follow a VERY standard pattern once you've got a few examples
to work from - I can provide these for you if you like.  This may prove
to be the quickest way and would probably help
heaps in coming to an understanding of exactly what the theorems are
and are not saying.


Hope this has helped.
Cheers,
Donald Syme,
Honours Student,
Australian National University.
> 
> Thanks,
> Vernon Austel
> austel@cs.ucla.edu
> 
> 
>