[Hol-info] recspace

[Mike Gordon]

Anyone know what recspace is (see question below)? I've not come
across it before.

Mike


---------- Forwarded message ----------
Date: Fri, Jun 20, 2008 at 2:05 PM
To: Mike Gordon <***@cl.cam.ac.uk>


Hi Mike,

Could I ask another quick question? I'm trying to find out what the
type `a recspace means in HOL (still looking at the list
theory)... I've tried searching through the 'description' and
'reference' manuals but haven't found an account. Is there separate
library documentation that I should be searching through? Thanks!

[John Harrison]

Hi Mike,

| Anyone know what recspace is (see question below)? I've not come
| across it before.

This type is used internally in HOL Light's type definition package.
Roughly, ":(A)recspace" is a type large enough to hold any finitely
branching recursive type built up from starting types that can be
injected into ":A". All types defined by "define_type" are carved
out of a type of the form, at least in HOL Light. It's defined in
the HOL Light source file "ind-types.ml". I believe the HOL4 type
definition package uses, or at least used, the same code:

src/datatype/ind_typeScript.sml
src/datatype/ind_types.sml

John.

[Michael Norrish]

Post by Mike Gordon
Anyone know what recspace is (see question below)? I've not come
across it before.

Recspace is the type used by the datatype package to support the
creation of algebraic types. It's basically a type of trees. Users
shouldn't rely on it at all, which is why it's not documented. (In
other words, the implementation of the datatype package might change,
and that type might disappear.)

If you are after types of trees, there are a couple in the distribution
that won't be lost (though they're minimal and need extending): inftree,
a type of potentially infinitely branching algebraic tree; and lbtree, a
type of "lazy" (i.e., co-algebraic) binary trees.

Michael.