ACL2 is an Untyped Language
ACL2 is an Untyped Language
The example
ACL2 !>(app '(a b c) 27)
(A B C . 27)
illustrates the fact that ACL2's logic is untyped (click here for a brief discussion of the typed versus untyped
nature of the logic).
The definition of app makes no restriction of the arguments to lists.
The definition says that if the first argument satisfies endp
then return the second argument. In this example, when app has recursed
three times down the cdr of its first argument, '(a b c), it reaches
the final nil, which satisfies endp, and so 27 is returned. It is
naturally consed into the emerging list as the function returns from
successive recursive calls (since cons does not require its arguments to
be lists, either). The result is an ``improper'' list, (a b c . 27).
You can think of (app x y) as building a binary tree by replacing the
right-most tip of the tree x with the tree y.
