## PUT-ASSOC-EQUAL

modify an association list by associating a value with a key
Major Section:  PROGRAMMING

(Put-assoc-equal name val alist) returns an alist that is the same as the list alist, except that the first pair in alist with a car of name is replaced by (cons name val), if there is one. If there is no such pair, then (cons name val) is added at the end.

The guard of (put-assoc-equal name val alist) requires that alist is an alistp.

## RASSOC

look up value in association list, using eql as test
Major Section:  PROGRAMMING

(Rassoc x alist) is similar to (assoc x alist), the difference being that it looks for the first pair in the given alist whose cdr, rather than car, is eql to x. See assoc.

The guard of rassoc requires its second argument to be an alist, and in addition, that either its first argument is eqlablep or else all second components of pairs belonging to the second argument are eqlablep. See eqlablep.

Rassoc is a Common Lisp function. See any Common Lisp documentation for more information.

## RATIONAL-LISTP

recognizer for a true list of rational numbers
Major Section:  PROGRAMMING

The predicate rational-listp tests whether its argument is a true list of rational numbers.

## RATIONALP

recognizer for rational numbers (ratios and integers)
Major Section:  PROGRAMMING

(rationalp x) is true if and only if x is an rational number.

## REAL/RATIONALP

recognizer for rational numbers (including real number in ACL2(r))
Major Section:  PROGRAMMING

For most ACL2 users, this is a macro abbreviating rationalp. In ACL2(r) (see real), this macro abbreviates the predicate realp, which holds for real numbers as well (including rationals). Most ACL2 users can ignore this macro and use rationalp instead, but many books in the ACL2 distribution use real/rationalp so that these books will be suitable for ACL2(r) as well.

## REALFIX

coerce to a real number
Major Section:  PROGRAMMING

Realfix simply returns any real number argument unchanged, returning 0 on a non-real argument. Also see nfix, see ifix, see rfix, and see fix for analogous functions that coerce to a natural number, an integer, a rational, and a number, respectively.

Realfix has a guard of t.

## REALPART

real part of a complex number
Major Section:  PROGRAMMING

Completion Axiom:

(equal (realpart x)
(if (acl2-numberp x)
(realpart x)
0))

Guard for (realpart x):

(acl2-numberp x)

## REDEFINING-PROGRAMS

an explanation of why we restrict redefinitions
Major Section:  PROGRAMMING

ACL2 does not in general allow the redefinition of functions because logical inconsistency can result: previously stored theorems can be rendered invalid if the axioms defining the functions involved are changed. However, to permit prototyping of both :program and :logic mode systems, ACL2 permits redefinition if the user has accepted logical responsibility for the consequences by setting ld-redefinition-action to an appropriate non-nil value. The refusal of ACL2 to support the unrestricted redefinition of :program mode functions may appear somewhat capricious. After all, what are the logical consequences of changing a definition if no axioms are involved?

Three important points should be made before we discuss redefinition further.

The first is that ACL2 does support redefinition (of both :program and :logic functions) when ld-redefinition-action is non-nil.

The second is that a ``redefinition'' that does not change the mode, formals or body of a function is considered redundant and is permitted even when ld-redefinition-action is nil. We recognize and permit redundant definitions because it is not uncommon for two distinct books to share identical function definitions. When determining whether the body of a function is changed by a proposed redefinition, we actually compare the untranslated versions of the two bodies. See term. For example, redundancy is not recognized if the old body is (list a b) and the new body is (cons a (cons b nil)). We use the untranslated bodies because of the difficulty of translating the new body in the presence of the old syntactic information, given the possibility that the redefinition might attempt to change the signature of the function, i.e., the number of formals, the number of results, or the position of single-threaded objects in either.

The third important point is that a ``redefinition'' that preserves the formals and body but changes the mode from :program to :logic is permitted even when ld-redefinition-action is nil. That is what verify-termination does.

This note addresses the temptation to allow redefiniton of :program functions in situations other than the three described above. Therefore, suppose ld-redefinition-action is nil and consider the cases.

Case 1. Suppose the new definition attempts to change the formals or more generally the signature of the function. Accepting such a redefinition would render ill-formed other :program functions which call the redefined function. Subsequent attempts to evaluate those callers could arbitrarily damage the Common Lisp image. Thus, redefinition of :program functions under these circumstances requires the user's active approval, as would be sought with ld-redefinition-action '(:query . :overwrite).

Case 2. Suppose the new definition attempts to change the body (even though it preserves the signature). At one time we believed this was acceptable and ACL2 supported the quiet redefinition of :program mode functions in this circumstance. However, because such functions can be used in macros and redundancy checking is based on untranslated bodies, this turns out to be unsound! It is therefore now prohibited. We illustrate such an unsoundness below. Let foo-thm1.lisp be a book with the following contents.

(in-package "ACL2")
(defun p1 (x) (declare (xargs :mode :program)) (list 'if x 't 'nil))
(defmacro p (x) (p1 x))
(defun foo (x) (p x))
(defthm foo-thm1 (iff (foo x) x) :rule-classes nil)
Note that the macro form (p x) translates to (if x t nil). The :program function p1 is used to generate this translation. The function foo is defined so that (foo x) is (p x) and a theorem about foo is proved, namely, that (foo x) is true iff x is true.

Now let foo-thm2.lisp be a book with the following contents.

(in-package "ACL2")
(defun p1 (x) (declare (xargs :mode :program)) (list 'if x 'nil 't))
(defmacro p (x) (p1 x))
(defun foo (x) (p x))
(defthm foo-thm2 (iff (foo x) (not x)) :rule-classes nil)
In this book, the :program function p1 is defined so that (p x) means just the negation of what it meant in the first book, namely, (if x nil t). The function foo is defined identically -- more precisely, the untranslated body of foo is identical in the two books, but because of the difference between the two versions of the the :program function p1 the axioms defining the two foos are different. In the second book we prove the theorem that (foo x) is true iff x is nil.

Now consider what would happen if the signature-preserving redefinition of :program functions were permitted and these two books were included. When the second book is included the redefinition of p1 would be permitted since the signature is preserved and p1 is just a :program. But then when the redefinition of foo is processed it would be considered redundant and thus be permitted. The result would be a logic in which it was possible to prove that (foo x) is equivalent to both x and (not x). In particular, the following sequence leads to a proof of nil:

(include-book "foo-thm1")
(include-book "foo-thm2")
(thm nil :hints (("Goal" :use (foo-thm1 foo-thm2))))

It might be possible to loosen the restrictions on the redefinition of :program functions by allowing signature-preserving redefinition of :program functions not involved in macro definitions. Alternatively, we could implement definition redundancy checking based on the translated bodies of functions (though that is quite problematic). Barring those two changes, we believe it is necessary simply to impose the same restrictions on the redefinition of :program mode functions as we do on :logic mode functions.

## REM

remainder using truncate
Major Section:  PROGRAMMING

ACL2 !>(rem 14 3)
2
ACL2 !>(rem -14 3)
-2
ACL2 !>(rem 14 -3)
2
ACL2 !>(rem -14 -3)
-2
ACL2 !>(rem -15 -3)
0
ACL2 !>
(Rem i j) is that number k that (* j (truncate i j)) added to k equals i.

The guard for (rem i j) requires that i and j are rational (real, in ACL2(r)) numbers and j is non-zero.

Rem is a Common Lisp function. See any Common Lisp documentation for more information.

## REMOVE

remove all occurrences, testing using eql
Major Section:  PROGRAMMING

(remove x l) is l if x is not a member of l, else is the result of removing all occurrences of x from l.

The guard for (remove x l) requires l to be a true list and moreover, either x is eqlablep or all elements of l are eqlablep.

Remove is a Common Lisp function. See any Common Lisp documentation for more information. Note that we do not allow keyword arguments (such as test) in ACL2 functions, in particular, in remove.

## REMOVE-DUPLICATES

remove duplicates from a string or (using eql) a list
Major Section:  PROGRAMMING

Remove-duplicates returns the result of deleting duplicate elements from the beginning of the given string or true list, i.e., leaving the last element in place. For example,

(remove-duplicates '(1 2 3 2 4))
is equal to '(1 3 2 4).

The guard for Remove-duplicates requires that its argument is a string or a true-list of eqlablep objects. It uses the function eql to test for equality between elements of its argument.

Remove-duplicates is a Common Lisp function. See any Common Lisp documentation for more information. Note that we do not allow keyword arguments (such as test) in ACL2 functions, in particular, in remove-duplicates. But see remove-duplicates-equal, which is similar but uses the function equal to test for duplicate elements.

## REMOVE-DUPLICATES-EQUAL

remove duplicates from a list
Major Section:  PROGRAMMING

Remove-duplicates-equal is the same as remove-duplicates, except that its argument must be a true list (not a string), and equal is used to check membership rather than eql. See remove-duplicates.

The guard for Remove-duplicates-equal requires that its argument is a true list. Note that unlike remove-duplicates, it does not allow string arguments.

## REST

rest (cdr) of the list
Major Section:  PROGRAMMING

In the logic, rest is just a macro for cdr.

Rest is a Common Lisp function. See any Common Lisp documentation for more information.

## REVAPPEND

concatentate the reverse of one list to another
Major Section:  PROGRAMMING

(Revappend x y) concatenates the reverse of the list x to y, which is also typically a list.

The following theorem characterizes this English description.

(equal (revappend x y)
(append (reverse x) y))
Hint: This lemma follows immediately from the definition of reverse and the following lemma.
(defthm revappend-append
(equal (append (revappend x y) z)
(revappend x (append y z))))

The guard for (revappend x y) requires that x is a true list.

Revappend is defined in Common Lisp. See any Common Lisp documentation for more information.

## REVERSE

reverse a list or string
Major Section:  PROGRAMMING

(Reverse x) is the result of reversing the order of the elements of the list or string x.

The guard for reverse requires that its argument is a true list or a string.

Reverse is defined in Common Lisp. See any Common Lisp documentation for more information.

## RFIX

coerce to a rational number
Major Section:  PROGRAMMING

Rfix simply returns any rational number argument unchanged, returning 0 on a non-rational argument. Also see nfix, see ifix, see realfix, and see fix for analogous functions that coerce to a natural number, an integer, a real, and a number, respectively.

Rfix has a guard of t.

## ROUND

division returning an integer by rounding off
Major Section:  PROGRAMMING

Example Forms:
ACL2 !>(round 14 3)
5
ACL2 !>(round -14 3)
-5
ACL2 !>(round 14 -3)
-5
ACL2 !>(round -14 -3)
5
ACL2 !>(round 13 3)
4
ACL2 !>(round -13 3)
-4
ACL2 !>(round 13 -3)
-4
ACL2 !>(round -13 -3)
4
ACL2 !>(round -15 -3)
5
ACL2 !>(round 15 -2)
-8
(Round i j) is the result of taking the quotient of i and j and rounding off to the nearest integer. When the quotient is exactly halfway between consecutive integers, it rounds to the even one.

The guard for (round i j) requires that i and j are rational (real, in ACL2(r)) numbers and j is non-zero.

Round is a Common Lisp function. See any Common Lisp documentation for more information.

## SECOND

second member of the list
Major Section:  PROGRAMMING

See any Common Lisp documentation for details.

## SET-DIFFERENCE-EQUAL

elements of one list that are not elements of another
Major Section:  PROGRAMMING

(Set-difference-equal x y) equals a list whose members (see member-equal) contains the members of x that are not members of y. More precisely, the resulting list is the same as one gets by deleting the members of y from x, leaving the remaining elements in the same order as they had in x.

The guard for set-difference-equal requires both arguments to be true lists. Essentially, set-difference-equal has the same functionality as the Common Lisp function set-difference, except that it uses the equal function to test membership rather than eql. However, we do not include the function set-difference in ACL2, because the Common Lisp language does not specify the order of the elements in the list that it returns.

## SEVENTH

seventh member of the list
Major Section:  PROGRAMMING

See any Common Lisp documentation for details.

## SIGNUM

indicator for positive, negative, or zero
Major Section:  PROGRAMMING

(Signum x) is 0 if x is 0, -1 if x is negative, and is 1 otherwise.

The guard for signum requires its argument to be rational (real, in ACL2(r)) number.

Signum is a Common Lisp function. See any Common Lisp documentation for more information.

From ``Common Lisp the Language'' page 206, we see a definition of signum in terms of abs. As explained elsewhere (see abs), the guard for abs requires its argument to be a rational (real, in ACL2(r)) number; hence, we make the same restriction for signum.

## SIXTH

sixth member of the list
Major Section:  PROGRAMMING

See any Common Lisp documentation for details.

## STANDARD-CHAR-LISTP

recognizer for standard characters
Major Section:  PROGRAMMING

(standard-char-listp x) is true if and only if x is a null-terminated list all of whose members are standard characters. See standard-char-p.

Standard-char-listp has a guard of t.

## STANDARD-CHAR-P

recognizer for standard characters
Major Section:  PROGRAMMING

(Standard-char-p x) is true if and only if x is a ``standard'' character, i.e., a member of the list *standard-chars*. This list includes #Newline and #Space characters, as well as the usual punctuation and alphanumeric characters.

Standard-char-p has a guard requiring its argument to be a character.

Standard-char-p is a Common Lisp function. See any Common Lisp documentation for more information.

## STANDARD-CO

the character output channel to which ld prints
Major Section:  PROGRAMMING

Standard-co is an ld special (see ld). The accessor is (standard-co state) and the updater is (set-standard-co val state). Standard-co must be an open character output channel. It is to this channel that ld prints the prompt, the form to be evaluated, and the results. The event commands such as defun, defthm, etc., which print extensive commentary do not print to standard-co but rather to a different channel, proofs-co, so that you may redirect this commentary while still interacting via standard-co. See proofs-co.

``Standard-co'' stands for ``standard character output.'' The initial value of standard-co is the same as the value of *standard-co* (see *standard-co*).

## STANDARD-OI

the standard object input ``channel''
Major Section:  PROGRAMMING

Standard-oi is an ld special (see ld). The accessor is (standard-oi state) and the updater is (set-standard-oi val state). Standard-oi must be an open object input channel, a true list of objects, or a list of objects whose last cdr is an open object input channel. It is from this source that ld takes the input forms to process. When ld is called, if the value specified for standard-oi is a string or a list of objects whose last cdr is a string, then ld treats the string as a file name and opens an object input channel from that file. The channel opened by ld is closed by ld upon termination.

``Standard-oi'' stands for ``standard object input.'' The read-eval-print loop in ld reads the objects in standard-oi and treats them as forms to be evaluated. The initial value of standard-oi is the same as the value of *standard-oi* (see *standard-oi*).

## STRING

coerce to a string
Major Section:  PROGRAMMING

(String x) coerces x to a string. If x is already a string, then it is returned unchanged; if x is a symbol, then its symbol-name is returned; and if x is a character, the corresponding one-character string is returned.

The guard for string requires its argument to be a string, a symbol, or a character.

String is a Common Lisp function. See any Common Lisp documentation for more information.

## STRING-ALISTP

recognizer for association lists with strings as keys
Major Section:  PROGRAMMING

(String-alistp x) is true if and only if x is a list of pairs of the form (cons key val) where key is a string.

String-alistp has a guard of t.

## STRING-APPEND

concatenate two strings
Major Section:  PROGRAMMING

NOTE: It is probably more efficient to use the Common Lisp function concatenate in place of string-append. That is,

(string-append str1 str2)
is equal to
(concatenate 'string str1 str2).

At any rate, string-append takes two arguments, which are both strings (if the guard is to be met), and returns a string obtained concatenating together the characters in the first string followed by those in the second. See concatenate.

## STRING-DOWNCASE

in a given string, turn upper-case characters into lower-case
Major Section:  PROGRAMMING

For a string x, (string-downcase x) is the result of applying char-downcase to each character in x.

The guard for string-downcase requires its argument to be a string.

String-downcase is a Common Lisp function. See any Common Lisp documentation for more information.

## STRING-EQUAL

string equality without regard to case
Major Section:  PROGRAMMING

For strings str1 and str2, (string-equal str1 str2) is true if and only str1 and str2 are the same except perhaps for the cases of their characters.

The guard on string-equal requires that its arguments are strings.

String-equal is a Common Lisp function. See any Common Lisp documentation for more information.

## STRING-LISTP

recognizer for a true list of strings
Major Section:  PROGRAMMING

The predicate string-listp tests whether its argument is a true-listp of strings.

## STRING-UPCASE

in a given string, turn lower-case characters into upper-case
Major Section:  PROGRAMMING

For a string x, (string-upcase x) is the result of applying char-upcase to each character in x.

The guard for string-upcase requires its argument to be a string.

String-upcase is a Common Lisp function. See any Common Lisp documentation for more information.

## STRING<

less-than test for strings
Major Section:  PROGRAMMING

(String< str1 str2) is non-nil if and only if the string str1 precedes the string str2 lexicographically, where character inequalities are tested using char<. When non-nil, (string< str1 str2) is the first position (zero-based) at which the strings differ. Here are some examples.

ACL2 !>(string< "abcd" "abu")
2
ACL2 !>(string< "abcd" "Abu")
NIL
ACL2 !>(string< "abc" "abcde")
3
ACL2 !>(string< "abcde" "abc")
NIL

The guard for string< specifies that its arguments are strings.

String< is a Common Lisp function. See any Common Lisp documentation for more information.

## STRING<=

less-than-or-equal test for strings
Major Section:  PROGRAMMING

(String<= str1 str2) is non-nil if and only if the string str1 precedes the string str2 lexicographically or the strings are equal. When non-nil, (string<= str1 str2) is the first position (zero-based) at which the strings differ, if they differ, and otherwise is their common length. See string<.

The guard for string<= specifies that its arguments are strings.

String<= is a Common Lisp function. See any Common Lisp documentation for more information.

## STRING>

greater-than test for strings
Major Section:  PROGRAMMING

(String> str1 str2) is non-nil if and only if str2 precedes str1 lexicographically. When non-nil, (string> str1 str2) is the first position (zero-based) at which the strings differ. See string<.

String> is a Common Lisp function. See any Common Lisp documentation for more information.

## STRING>=

less-than-or-equal test for strings
Major Section:  PROGRAMMING

(String>= str1 str2) is non-nil if and only if the string str2 precedes the string str1 lexicographically or the strings are equal. When non-nil, (string>= str1 str2) is the first position (zero-based) at which the strings differ, if they differ, and otherwise is their common length. See string>.

The guard for string>= specifies that its arguments are strings.

String>= is a Common Lisp function. See any Common Lisp documentation for more information.

## STRINGP

recognizer for strings
Major Section:  PROGRAMMING

(stringp x) is true if and only if x is a string.

## STRIP-CARS

collect up all first components of pairs in a list
Major Section:  PROGRAMMING

(strip-cars x) is the list obtained by walking through the list x and collecting up all first components (cars). This function is implemented in a tail-recursive way, despite its logical definition.

(strip-cars x) has a guard of (alistp x).

## STRIP-CDRS

collect up all second components of pairs in a list
Major Section:  PROGRAMMING

(strip-cdrs x) has a guard of (alistp x), and returns the list obtained by walking through the list x and collecting up all second components (cdrs). This function is implemented in a tail-recursive way, despite its logical definition.

## SUBLIS

substitute an alist into a tree
Major Section:  PROGRAMMING

(Sublis alist tree) is obtained by replacing every leaf of tree with the result of looking that leaf up in the association list alist. However, a leaf is left unchanged if it is not found as a key in alist.

Leaves are lookup up using the function assoc. The guard for (sublis alist tree) requires (eqlable-alistp alist). This guard ensures that the guard for assoc will be met for each lookup generated by sublis.

Sublis is defined in Common Lisp. See any Common Lisp documentation for more information.

## SUBSEQ

subsequence of a string or list
Major Section:  PROGRAMMING

For any natural numbers start and end, where start <= end <= (length seq), (subseq seq start end) is the subsequence of seq from index start up to, but not including, index end. End may be nil, which which case it is treated as though it is (length seq), i.e., we obtain the subsequence of seq from index start all the way to the end.

The guard for (subseq seq start end) is that seq is a true list or a string, start and end are integers (except, end may be nil, in which case it is treated as (length seq) for ther rest of this discussion), and 0 <= start <= end <= (length seq).

Subseq is a Common Lisp function. See any Common Lisp documentation for more information. Note: In Common Lisp the third argument of subseq is optional, but in ACL2 it is required, though it may be nil as explained above.

## SUBSETP

test if every member of one list is a member of the other
Major Section:  PROGRAMMING

(Subsetp x y) is true if and only if every member of the list x is a member of the list y.

Membership is tested using the function member. Thus, the guard for subsetp requires that its arguments are true lists, and moreover, at least one satisfies eqlable-listp. This guard ensures that the guard for member will be met for each call generated by subsetp.

Subsetp is defined in Common Lisp. See any Common Lisp documentation for more information.

## SUBSETP-EQUAL

check if all members of one list are members of the other
Major Section:  PROGRAMMING

(Subsetp-equal x y) returns t if every member of x is a member of y, where membership is tested using member-equal.

The guard for subsetp-equal requires both arguments to be true lists. Subsetp-equal has the same functionality as the Common Lisp function subsetp, except that it uses the equal function to test membership rather than eql.

## SUBST

a single substitution into a tree
Major Section:  PROGRAMMING

(Subst new old tree) is obtained by substituting new for every occurence of old in the given tree.

Equality to old is determined using the function eql. The guard for (subst new old tree) requires (eqlablep old), which ensures that the guard for eql will be met for each comparison generated by subst.

Subst is defined in Common Lisp. See any Common Lisp documentation for more information.

## SUBSTITUTE

substitute into a string or a list, using eql as test
Major Section:  PROGRAMMING

(Substitute new old seq) is the result of replacing each occurrence of old in seq, which is a list or a string, with new.

The guard for substitute requires that either seq is a string, or else seq is a true-listp such that either all of its members are eqlablep or old is eqlablep.

Substitute is a Common Lisp function. See any Common Lisp documentation for more information. Since ACL2 functions cannot take keyword arguments (though macros can), the test used in substitute is eql.

## SYMBOL-<

less-than test for symbols
Major Section:  PROGRAMMING

(symbol-< x y) is non-nil if and only if either the symbol-name of the symbol x lexicographially precedes the symbol-name of the symbol y (in the sense of string<) or else the symbol-names are equal and the symbol-package-name of x lexicographically precedes that of y (in the same sense). So for example, (symbol-< 'abcd 'abce) and (symbol-< 'acl2::abcd 'foo::abce) are true.

The guard for symbol specifies that its arguments are symbols.

## SYMBOL-ALISTP

recognizer for association lists with symbols as keys
Major Section:  PROGRAMMING

(Symbol-alistp x) is true if and only if x is a list of pairs of the form (cons key val) where key is a symbolp.

## SYMBOL-LISTP

recognizer for a true list of symbols
Major Section:  PROGRAMMING

The predicate symbol-listp tests whether its argument is a true list of symbols.

## SYMBOL-NAME

the name of a symbol (a string)
Major Section:  PROGRAMMING

Completion Axiom:

(equal (symbol-name x)
(if (symbolp x)
(symbol-name x)
""))

Guard for (symbol-name x):

(symbolp x)

## SYMBOL-PACKAGE-NAME

the name of the package of a symbol (a string)
Major Section:  PROGRAMMING

Completion Axiom:

(equal (symbol-package-name x)
(if (symbolp x)
(symbol-package-name x)
""))

Guard for (symbol-package-name x):

(symbolp x)