Type-set
How type information is encoded in ACL2
See type-reasoning for basic background on type reasoning in
ACL2.
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 (ens state) (w state) nil nil nil) will
return the type-set of term with respect to the current world and the
top-level enabled structure. For example,
(type-set '(integerp x) nil nil nil (ens state) (w state) nil nil 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-negative-integer*
denotes the set containing all of the negative integers.
*TS-ZERO* ;;; {0}
*TS-ONE* ;;; {1}
*TS-INTEGER>1* ;;; integers greater than 1
*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* ;;; nil-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 two's-complement bitwise `not' 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 7. The type-set
containing just *ts-nil* is thus represented by 128. If a term has
type-set 128 then the term is always equal to nil. The type-set
containing everything but *ts-nil* is the bitwise `not' of 128,
which is -129. If a term has type-set -129, 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 value
*ts-zero* 0 1
*ts-one* 1 2
*ts-integer>1* 2 4
*ts-nil* 7 128
*ts-t* 8 256
*ts-non-t-non-nil-symbol* 9 512
Thus, the type-set s is represented by (+ 1 2 4 128 256 512) =
903. The complement of s, i.e., the set of all objects other than
the natural numbers and the symbols, is -904. We can get ACL2 to provide
such information as follows.
ACL2 !>(decode-type-set 903)
(TS-UNION *TS-SYMBOL* *TS-NON-NEGATIVE-INTEGER*)
ACL2 !>(decode-type-set -904)
(TS-COMPLEMENT (TS-UNION *TS-SYMBOL* *TS-NON-NEGATIVE-INTEGER*))
ACL2 !>
Subtopics
- Type-alist
- An ACL2 representation of contextual knowledge
