Logic and Computation
CS 2800 Fall 2019

Khoury College of Computer Sciences
Northeastern University
ACL2s reference

ACL2s reference

Types

Name
Recognizer
Description
all allp the ACL2s universe
atom atom atomic data: numbers, strings, ...
symbol symbolp symbols
boolean booleanp t or nil
bool booleanp only works with definec
rational rationalp rational numbers (we assume that all numbers are rationals, which is not technically true in ACL2s)
integer integerp integers
int integerp only works with definec
nat natp natural numbers (int >= 0)
pos posp positive integers (int > 0)
cons consp conses, constructed with cons
true-list tlp, true-listp true lists (nil terminated cons)
tl tlp, true-listp only works in definec
list listp conses or nil

Function signatures

Name
Contract
Description
if All x All x All -> All if test then else
equal All x All -> Bool checks if args are equal
implies All x All -> Bool implication
iff All x All -> Bool if and only if (Boolean equality)
xor All x All -> Bool xor (Boolean disequality)
binary-+ Rational x Rational -> Rational addition
binary-* Rational x Rational -> Rational multiplication
< Rational x Rational -> Bool less than
unary-- Rational -> Rational unary -
unary-/ Rational \ {0} -> Rational unary /
expt (Rational X Integer) \ {(0, i) : i < 0} exponentiation
numerator Rational -> Integer numerator
denominator Rational -> Pos denominator
mod Rational x Rational \ {0} -> Rational modular arithmetic
ceiling Rational x Rational \ {0} -> Integer ceiling of quotient
floor Rational x Rational \ {0} -> Integer floor of quotient
evenp Integer -> Bool is the number even?
oddp Integer -> Bool is the number odd?
cons All x All -> All create a cons
car List -> All car of a list
cdr List -> All cdr of a list
head Cons-> All car of a cons (not builtin, see lecture notes)
tail Cons -> All cdr of a cons (not builtin, see lecture notes)
endp List -> Bool is list empty?
aapp TL x TL -> TL concatenate two lists (not builtin, see lecture notes)
binary-append TL x All -> All concatenation
rev ALL -> TL reverse
rrev TL -> TL reverse a list (not builtin, see lecture notes)
len ALL -> Nat length of anything
llen TL -> Nat length of a true list (not builtin, see lecture notes)
in ALL x TL -> Bool (in a X) checks if a is in X (not builtin, see lecture notes)
del ALL x TL -> TL (del a X) deletes first occurrence of a from X (not builtin, see lecture notes)

Macros

Name
Description
and arbitrary # of args, expands to ifs
or arbitrary # of args, expands to ifs
cond expand into ifs
+ arbitrary # of args, expands to binary-+
* arbitrary # of args, expands to binary-*
- 1 (unary--) or 2 (subtraction) args
/ 1 (unary-/) or 2 (division) args
<= less than or equal, expands into <
> greater than, expands into <
>= greater than or equal, expands into <
first synonym for car
rest synonym for cdr
caar (car (car ...))
cadr (car (cdr ...))
c****r Can have up to 4 a's d's and expands into nested car/cdr's
second synonym for cadr
third synonym for caddr, up to tenth supported
list create a truelist of 0 or more arguments, expands into cons
app append 0 or more lists, expands into binary-append