		Search-engine friendly clone of the ACL2 documentation.

Apply$

Gratuitous-lambda-object-restrictions

Enforcement of logically unnecessary restrictions on :FN slots

When a form is submitted to the ACL2's read-eval-print loop the terms in it are translated (``macroexpanded'') into ACL2's internal form, in which abbreviations like (cadr x) are expanded away and constants are always quoted. See term for details of the internal form.

But translation also enforces a logically unnecessary restriction in argument positions of ilk :FN. If a quoted consp object whose car is the symbol LAMBDA occurs in a :FN slot, translate insists that the object satisfy well-formed-lambda-objectp. Well-formedness implies tameness, so any LAMBDA object that passes this translate-time test will have the ``expected behavior'' under apply$. If a quoted ill-formed ``LAMBDA-like'' object is passed into a :FN slot, an error is signaled.

This is logically unnecessary because, like all ACL2 functions, apply$ can be called on any objects. Indeed, ill-formed LAMBDA-like objects induce some kind of default behavior by apply$ and can, sometimes, deliver non-erroneous values.

But ground apply$ terms can be evaluated more quickly on well-formed LAMBDA objects than on ill-formed ones. See for example the discussion of performance in print-cl-cache. So this restriction is really motivated by a desire to encourage the exclusive use of well-formed LAMBDA objects.

Why would you want to call apply$ on ill-formed input? The answer is that you might be trying to explore the semantics of apply$ by example. Since this is a time-honored methodology, we have made it possible to circumvent the translate-time check if you insist on feeding an ill-formed object into a :FN slot. Soundness is not imperiled but execution may slow down.

Warning: Using an ill-formed LAMBDA object in a :FN slot in a defun will make it impossible to warrant the newly defined function because it will not pass the stringent tests necessary to analyze its ilks. See defwarrant. Basically these bypasses are intended primarily for top-level input to ACL2's read-eval-print loop.

There are two ways to bypass the check. Bypass 1 is to construct the object in place rather than supply a quoted constant. This can be as simple as consing a LAMBDA onto the rest of your ill-formed constant. This, of course, costs one cons at eval-time. Bypass 2 is to cons the ill-formed object together in a defconst and then use the defined constant symbol in the :FN slot. We illustrate these and other points below.

; Here we show the error that occurs if you use an ill-formed
; LAMBDA object in a :FN slot.

ACL2 !>(apply$ '(lambda (t) (cons t t)) '(a))

ACL2 Error in TOP-LEVEL: The second element of a well-formed
LAMBDA object or lambda$ term must be a true list of distinct
legal variable symbols and (T) is not.  See :DOC
gratuitous-lambda-object-restrictions for a workaround if you
really mean to have an ill-formed LAMBDA-like constant in your
code.  Note: this error occurred in the context
(APPLY$ '(LAMBDA (T) (CONS T T)) '(A)).

; Bypass 1:  Cons the ill-formed object together in place.

ACL2 !>(apply$ (cons 'lambda '((t) (cons t t))) '(a))
(A . A)

; Bypass 1 (more attractive but perhaps too subtle): Use
; backquote.  This looks prettier, indeed, it is almost
; unnoticeable!  But it does more eval-time consing.

ACL2 !>(apply$ `(lambda (t) (cons t t)) '(a))
(A . A)

; Bypass 2:  Use defconst first.  No runtime consing.

ACL2 !>(defconst *my-ill-formed-lambda*
          `(lambda (t) (cons t t)))
...output elided...

ACL2 !>(apply$ *my-ill-formed-lambda* '(a))
(A . A)

; You can, of course, use these bypasses when defining new
; functions.

ACL2 !>(defun foo (x) (apply$ *my-ill-formed-lambda* (list x)))
...successful defun output elided...

; You can then execute the new function, possibly slowly.

ACL2 !>(foo 'b)
(B . B)

; But you can't warrant the new function because defwarrant
; can't determine the ilks.

ACL2 !>(defwarrant foo)

ACL2 Error in DEFWARRANT: FOO will not be warranted because
a :FN slot in its body is occupied by a quoted cons object,
'(LAMBDA (T) (CONS T T)), that is not a well-formed,
fully-translated, closed ACL2 lambda object. ...

; Thus, you can't apply$ 'foo either.

ACL2 !>(apply$ 'foo '(c))

ACL2 Error in TOP-LEVEL: The value of APPLY$-USERFN is not
specified on FOO because FOO has not been warranted.

By the way, :FN slots are treated differently in another way by translate: lambda$ terms are only allowed in :FN slots. This restriction is necessary for ACL2's correct operation. Lambda$ expands differently in the logic than it does in the underlying Common Lisp. If lambda$ terms were allowed to occur anywhere, this difference could be detected by the difference between proved behavior and computed behavior and could be used to render ACL2 unsound.