		Search-engine friendly clone of the ACL2 documentation.

Tau-system

Tau-intervalp

Boolean recognizer for tau intervals

General Form:
(tau-intervalp x)

An interval is a structure of the form: (dom (lo-rel . lo) . (hi-rel . hi)). Every tau contains an interval used to represent the domain and the upper and lower bounds of the objects recognized by the tau.

Restrictions on the components of an interval are as follows. For an interpretation of the meaning of the components, see in-tau-intervalp or make-tau-interval.

Dom (``domain'') must be one of four symbols: INTEGERP, RATIONALP, ACL2-NUMBERP, or NIL.

The two ``relations,'' lo-rel and hi-rel, must be Booleans.

Lo and hi must be either nil or explicit rational numbers. Lo must be no greater than hi (where nils represent negative or positive infinity for lo and hi respectively.

Finally, if the dom is INTEGERP, then both relations must nil and lo and hi must be integers when they are non-nil.

Recall that make-tau-interval constructs intervals. The intervals it constructs are well-formed only if the arguments to make-tau-interval satisfy the rules above; make-tau-interval does not coerce or adjust its arguments in any way. Thus, it can be (mis-)used to create non-intervals. Here are examples of tau-intervalp using make-tau-interval.

; integers: 0 <= x <= 10:
(tau-intervalp (make-tau-interval 'INTEGERP nil 0 nil 10))      = t

; integers: 0 <= x (i.e., the natural numbers):
(tau-intervalp (make-tau-interval 'INTEGERP nil 0 nil nil))     = t

; violations of domain rules:
(tau-intervalp (make-tau-interval 'INTEGERP t 0 t 10))          = nil
(tau-intervalp (make-tau-interval 'INTEGERP nil 0 nil 10/11))   = nil

; violation of rule that bounds must be rational if non-nil:
(tau-intervalp (make-tau-interval 'ACL2-NUMBERP t 0 t #c(3 5))) = nil

; violation of rule that lo <= hi:
(tau-intervalp (make-tau-interval 'ACL2-NUMBERP t 0 t -10))     = nil

; rationals: 0 < x <= 22/7:
(tau-intervalp (make-tau-interval 'RATIONALP t 0 nil 22/7))     = t

; numbers: -10 < x < 10:
(tau-intervalp (make-tau-interval 'ACL2-NUMBERP t -10 t 10))    = t

; any: -10 < x < 10:
(tau-intervalp (make-tau-interval nil t -10 t 10))              = t

: any:
(tau-intervalp (make-tau-interval nil nil nil nil nil))         = t

Note that the second-to-last interval, with domain nil contains all non-numbers as well as numbers strictly between -10 and 10. The reason is that the interval contains 0 and all non-numbers are coerced to 0 by the inequality functions.

Note that the last interval contains all ACL2 objects. It is called the ``universal interval.''