Major Section: MISCELLANEOUS

To help you experiment with type-sets we briefly note the following utility functions.

`(type-set-quote x)`

will return the type-set of the object `x`

. For
example, `(type-set-quote "test")`

is `2048`

and
`(type-set-quote '(a b c))`

is `512`

.

`(type-set 'term nil nil nil nil (ens state) (w state) nil)`

will
return the type-set of `term`

. For example,

(type-set '(integerp x) nil nil nil nil (ens state) (w state) nil)will return (mv 192 nil). 192, otherwise known as

`*ts-boolean*`

,
is the type-set containing `t`

and `nil`

. The second result may
be ignored in these experiments. `Term`

must be in the
`translated`

, internal form shown by `:`

`trans`

. See trans
and see term.
`(type-set-implied-by-term 'x nil 'term (ens state)(w state) nil)`

will return the type-set deduced for the variable symbol `x`

assuming
the `translated`

term, `term`

, true. The second result may be ignored
in these experiments. For example,

(type-set-implied-by-term 'v nil '(integerp v) (ens state) (w state) nil)returns

`11`

.
`(convert-type-set-to-term 'x ts (ens state) (w state) nil)`

will
return a term whose truth is equivalent to the assertion that the
term `x`

has type-set `ts`

. The second result may be ignored in these
experiments. For example

(convert-type-set-to-term 'v 523 (ens state) (w state) nil)returns a term expressing the claim that

`v`

is either an integer
or a non-`nil`

true-list. `523`

is the `logical-or`

of `11`

(which
denotes the integers) with `512`

(which denotes the non-`nil`

true-lists).
The ``actual primitive types'' of ACL2 are listed in
`*actual-primitive-types*`

, whose elements are shown below. Each
actual primitive type denotes a set -- sometimes finite and
sometimes not -- of ACL2 objects and these sets are pairwise
disjoint. For example, `*ts-zero*`

denotes the set containing 0 while
`*ts-positive-integer*`

denotes the set containing all of the positive
integers.

*TS-ZERO* ;;; {0} *TS-POSITIVE-INTEGER* ;;; positive integers *TS-POSITIVE-RATIO* ;;; positive non-integer rationals *TS-NEGATIVE-INTEGER* ;;; negative integers *TS-NEGATIVE-RATIO* ;;; negative non-integer rationals *TS-COMPLEX-RATIONAL* ;;; complex rationals *TS-NIL* ;;; {nil} *TS-T* ;;; {t} *TS-NON-T-NON-NIL-SYMBOL* ;;; symbols other than nil, t *TS-PROPER-CONS* ;;; null-terminated non-empty lists *TS-IMPROPER-CONS* ;;; conses that are not proper *TS-STRING* ;;; strings *TS-CHARACTER* ;;; characters

The actual primitive types were chosen by us to make theorem proving
convenient. Thus, for example, the actual primitive type `*ts-nil*`

contains just `nil`

so that we can encode the hypothesis ```x`

is `nil`

''
by saying ```x`

has type `*ts-nil*`

'' and the hypothesis ```x`

is
non-`nil`

'' by saying ```x`

has type complement of `*ts-nil*`

.'' We
similarly devote a primitive type to `t`

, `*ts-t*`

, and to a third type,
`*ts-non-t-non-nil-symbol*`

, to contain all the other ACL2 symbols.

Let `*ts-other*`

denote the set of all Common Lisp objects other than
those in the actual primitive types. Thus, `*ts-other*`

includes such
things as floating point numbers and CLTL array objects. The actual
primitive types together with `*ts-other*`

constitute what we call
`*universe*`

. Note that `*universe*`

is a finite set containing one
more object than there are actual primitive types; that is, here we
are using `*universe*`

to mean the finite set of primitive types, not
the infinite set of all objects in all of those primitive types.
`*Universe*`

is a partitioning of the set of all Common Lisp objects:
every object belongs to exactly one of the sets in `*universe*`

.

Abstractly, a ``type-set'' is a subset of `*universe*`

. To say that a
term, `x`

, ``has type-set `ts`

'' means that under all possible
assignments to the variables in `x`

, the value of `x`

is a member of
some member of `ts`

. Thus, `(cons x y)`

has type-set
`{*ts-proper-cons* *ts-improper-cons*}`

. A term can have more than
one type-set. For example, `(cons x y)`

also has the type-set
`{*ts-proper-cons* *ts-improper-cons* *ts-nil*}`

. Extraneous types
can be added to a type-set without invalidating the claim that a
term ``has'' that type-set. Generally we are interested in the
smallest type-set a term has, but because the entire theorem-proving
problem for ACL2 can be encoded as a type-set question, namely,
``Does `p`

have type-set complement of `*ts-nil*`

?,'' finding the
smallest type-set for a term is an undecidable problem. When we
speak informally of ``the'' type-set we generally mean ``the
type-set found by our heuristics'' or ``the type-set assumed in the
current context.''

Note that if a type-set, `ts`

, does not contain `*ts-other*`

as an
element then it is just a subset of the actual primitive types. If
it does contain `*ts-other*`

it can be obtained by subtracting from
`*universe*`

the complement of `ts`

. Thus, every type-set can be
written as a (possibly complemented) subset of the actual primitive
types.

By assigning a unique bit position to each actual primitive type we
can encode every subset, `s`

, of the actual primitive types by the
nonnegative integer whose ith bit is on precisely if `s`

contains the
ith actual primitive type. The type-sets written as the complement
of `s`

are encoded as the `twos-complement`

of the encoding of `s`

. Those
type-sets are thus negative integers. The bit positions assigned to
the actual primitive types are enumerated from `0`

in the same order
as the types are listed in `*actual-primitive-types*`

. At the
concrete level, a type-set is an integer between `*min-type-set*`

and
`*max-type-set*`

, inclusive.

For example, `*ts-nil*`

has bit position `6`

. The type-set containing
just `*ts-nil*`

is thus represented by `64`

. If a term has type-set `64`

then the term is always equal to `nil`

. The type-set containing
everything but `*ts-nil*`

is the twos-complement of `64`

, which is `-65`

.
If a term has type-set `-65`

, it is never equal to `nil`

. By ``always''
and ``never'' we mean under all, or under no, assignments to the
variables, respectively.

Here is a more complicated example. Let `s`

be the type-set
containing all of the symbols and the natural numbers. The relevant
actual primitive types, their bit positions and their encodings are:

actual primitive type bit valueThus, the type-set*ts-zero* 0 1 *ts-positive-integer* 1 2 *ts-nil* 6 64 *ts-t* 7 128 *ts-non-t-non-nil-symbol* 8 256

`s`

is represented by `(+ 1 2 64 128 256)`

= `451`

.
The complement of `s`

, i.e., the set of all objects other than the
natural numbers and the symbols, is `-452`

.