		Search-engine friendly clone of the ACL2 documentation.

Varp

Representation of a Boolean variable.

Signature
(varp x) → bool
Returns: bool — Type (booleanp bool).

A variable is now represented as just a natural number, and the abstract data type wrapper described below is no longer used (we found it too hard to reason about). We're preserving the documentation below for reference, but it's no longer true.

Think of a VARIABLE as an abstract data type that represents a Boolean variable. A variable has an index that can be used to distinguish it from other variables. The interface for working with variables is simply:

(varp x) → bool: Recognize valid identifiers.
(make-var index) → id: Construct an identifier with the given given a natural number index.
(var->index id) → index: Get the index from an identifier.

In the implementation, variables are nothing more than natural numbers. That is, varp is just natp, while make-var and var->index are logically just nfix and in the execution are the identity.

Why, then, bother with a variable type at all? We use (for efficiency) integer encodings of related data types like variables and literals. Treating these as separate types helps us avoid confusing them for one another when we write programs.

A very nice presentation of this idea is found in Type Kata: Distinguishing different data with the same underlying representation, a blog post by Edward Z. Yang.

Definitions and Theorems

Function: varp

(defun varp (x)
  (declare (xargs :guard t))
  (let ((__function__ 'varp))
    (declare (ignorable __function__))
    (natp x)))

Theorem: booleanp-of-varp

(defthm booleanp-of-varp
  (b* ((bool (varp x))) (booleanp bool))
  :rule-classes :tau-system)

Theorem: varp-compound-recognizer

(defthm varp-compound-recognizer
  (equal (varp x) (natp x))
  :rule-classes :compound-recognizer)

Subtopics

Varp-reasoning: Basic rules for reasoning about identifiers.