Delivery-Date: 
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
Date: Mon, 2 Nov 92 20:52:17 -0800
From: austel@edu.ucla.cs (Vernon Austel)
Message-Id: <9211030452.AA26944@maui.cs.ucla.edu>
To: info-hol@edu.uidaho.cs.ted
Subject: mutually recursive types in HOL


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?

Section 10.5.5 of the HOL DESCRIPTION describes ``type specification''.  
This apparently generalizes type definition in way analogous
to how new_specification generalizes constant definition.

Has this been implemented?  If not, does anyone plan to?
Would someone please spell out in black and white what new
kinds of types this facility would allow us to define?

I have spent several weeks developing a mechanism to define recursive
functions on nonrecursive data types.  While doing so I noticed
strong similarities to the way trees are implemented in mk_tree.ml.
I still don't fully understand what I'm doing, and I am not quite
sure that it will work yet, but I think that in addition to doing what
I originally intended it to do, the mechanism I'm developing
will allow more general types (such as mutually recursive types)
to be defined, among other things.  This would not be a toy;
it would be quite practical.

Although I greatly enjoy working on this, I do not want to invest 
more time in it if the problem has already been solved satisfactorily,
or if a superior solution to the problem will be appearing shortly.

Thanks,
Vernon Austel
austel@cs.ucla.edu