Well-formed-lambda-objectp
Predicate for recognizing well-formed LAMBDA objects
Example: value
(well-formed-lambda-objectp T
'(lambda (x) (binary-+ '1 x))
(w state))
(well-formed-lambda-objectp NIL
'(lambda (x) (+ 1 x))
(w state))
(well-formed-lambda-objectp T
'(lambda (x)
(declare (type (satisfies natp) x)
(xargs :guard (natp x)
:split-types t))
(binary-+ '1 x))
(w state))
(well-formed-lambda-objectp NIL
'(lambda (x)
(declare (type (satisfies natp) x))
(binary-+ '1 x))
(w state))
General Form:
(well-formed-lambda-objectp obj wrld)
Well-formed-lambda-objectp is a :program mode function that
checks the well-formedness of an arbitrary ACL2 object being used as a
LAMBDA object by apply$.
Before we tell you what ``well-formedness'' means in this context we
collect some random related facts that we consider more important than its
precise meaning!
Lambda$ terms always translate to quoted well-formed LAMBDA
objects unless translate signals an explanatory error. Don't try to type
well-formed LAMBDA objects as explicitly quoted constants. Use lambda$!
Only well-formed LAMBDA objects can be compiled. Use lambda$.
But the compiled code is not necessarily always run when a well-formed
LAMBDA object is apply$d! The object must additionally be guard
verified and its guards must be satisfied by the arguments supplied by
apply$. Well-formedness does not do guard verification.
The definitional axiom for apply$ knows nothing about
well-formedness. It checks that the purported LAMBDA object satisfies
tamep-lambdap, which is a simpler :logic mode concept. If you
are writing a definition or theorem about an arbitrary object to be used as a
LAMBDA object by apply$, and want to restrict it to the kind of
objects handled as LAMBDA objects by apply$, use the predicate
tamep-lambdap to characterize the object. (Since
well-formed-lambda-objectp is in :program mode and requires
access to the world, using it in a :logic mode context would involve a
lot of work!)
Well-formedness implies tameness. So if you write your LAMBDA
objects with lambda$ apply$ will be able to handle them. But
apply$ can handle more objects than the Common Lisp compiler can. Some
tame LAMBDA objects can be applied faster than others. The fast ones
are recognized by well-formed-lambda-objectp -- but also have to be
guard verified and guard checked. Applications of ill-formed but tame
LAMBDA objects are evaluable, but the evaluation is done more slowly.
See the performance comparison in print-cl-cache.
We compare well-formedness to tameness at the end of this topic.
You can't call this predicate on a lambda$ term, as by
(well-formed-lambda-objectp (lambda$ (x) x) (w state))
because lambda$ can only be called in slots of ilk :FN.
Furthermore, there's no point! Lambda$ terms always translate to
well-formed LAMBDA objects unless an explanatory error is signaled by
translation.
If you want to see the translation of a lambda$ term, e.g., to
copy the text and modify it to produce some similar LAMBDA object,
use :translam. We sometimes do this to explore by example the
restrictions on well-formedness.
If you have a LAMBDA object, e.g., one printed by print-cl-cache, that you suspect is ill-formed, this function won't tell you
why it is ill-formed! It will just tell you whether it's ill-formed.
If you want to know why, translate the quoted LAMBDA object with
:translam, which generates sometimes verbose error messages.
The global setting of set-ignore-ok has no effect on well-formedness
of LAMBDA objects. IGNORE and IGNORABLE declarations inside the
LAMBDA are effective.
ACL2 !>(set-ignore-ok t)
T
ACL2 !>(well-formed-lambda-objectp
'(LAMBDA (X Y)
(DECLARE (XARGS :GUARD (NATP X) :SPLIT-TYPES T))
(BINARY-+ '1 X))
(w state))
NIL
ACL2 !>(well-formed-lambda-objectp
'(LAMBDA (X Y)
(DECLARE (XARGS :GUARD (NATP X) :SPLIT-TYPES T)
(IGNORE Y))
(BINARY-+ '1 X))
(w state))
T
There should be very few occasions on which you need to know what this
predicate checks!
That said, here are the rules enforced.
An object is a well-formed LAMBDA object iff it has one of the
following two forms:
(LAMBDA vars tbody) ; ``simple'' LAMBDA object
(LAMBDA vars tdcl tbody) ; ``declared'' LAMBDA object
where
- vars is a list of distinct legal variable names
- tdcl, if present, is a DECLARE form containing, at most,
TYPE, IGNORE, IGNORABLE, and XARGS keys. The user of
lambda$ may provide multiple DECLARE forms but when
translated they are combined into one as shown here.
- If an XARGS key is present it has exactly this form (XARGS
:GUARD tguard :SPLIT-TYPES T), where tguard is a fully
translated logic mode term involving only the formal variables,
vars. Note that the user of lambda$ may supply
:SPLIT-TYPES NIL and may do so before or after the :GUARD,
and the guard term need not be in translated form, but the resulting
LAMBDA object has the form described here.
- The :GUARD specified in XARGS must include as a conjunct
every TYPE expression generated by any TYPE specs. E.g.,
(INTEGERP x) must be a conjunct of tguard if (TYPE INTEGER
... x ...) is declared. That is consistent with the :SPLIT-TYPES
T setting and means the guard does not need to be extended any
further with the TYPES. The point of this restriction is to
guarantee that the guard implies the types declared to the compiler. But
this is a purely syntactic check and so may at times require entering
silly-looking guards. For example, (declare (type rational x) (xargs
:guard (integerp x) :split-types t)) is ruled ill-formed because
(rationalp x) is not a conjunct of the guard, even though it is
logically implied by the guard. So you'd have to use (declare (type
rational x) (xargs :guard (if (integerp x) (rationalp x)
'nil) :split-types t)). Note also that the guard is a fully translated
conjunction, i.e., an IF, not an AND! Order of the conjuncts
does not matter.
Note: The guard need not be tame (or even fully badged) because guards
are irrelevant to the axioms of apply$. But guards must be in
:logic mode from the outset because we may have to prove guard
obligations on-the-fly in evaluation (we do not want to try to convert
functions used in the guard from from :program to :logic mode
while doing an evaluation of an apply$).
- tbody is a fully translated, tame term, involving no free
variables and respecting the declared IGNORE and IGNORABLE
declarations.
Furthermore, in the case of a lambda object generated by lambda$,
tbody is a ``tagged'' version of the translation of the body used in
the lambda$ expression. Tagging involves use of a special form
generated by tag-translated-lambda$-body and recognized by
lambda$-bodyp. This form contains the untranslated lambda$
expression as well as the translation of its body. For example,
(lambda$ (x) (+ 1 x)) translates to the tagged lambda object
'(LAMBDA (X) (RETURN-LAST 'PROGN 'orig-form tbody)), where
orig-form is (LAMBDA$ (X) (+ 1 X)) and tbody is
(BINARY-+ '1 X).
It may be helpful to use :translam to inspect examples of
the translations of lambda$ expressions.
The Differences Between Well-Formed and Merely Tame Lambda Objects
Roughly put, tame LAMBDA objects have to have one of the two basic
shapes described above (simple or declared), the listed formals merely have
to be symbols -- not necessarily variable symbols and not necessarily
distinct. The declaration, if present, is completely irrelevant and the body
merely has to be a tame expression -- not necessarily closed with respect to
the formals or respecting IGNORE or IGNORABLE declarations. The
meaning assigned to such an object when applied to some arguments is just the
result delivered by ev$ under an alist formed by pairing the formals --
including non-variables and any duplicates -- with the actuals. If a free
variable is encountered, ev$ gives it the value NIL courtesy of
assoc.
This behavior is implemented by compiled Common Lisp only when
well-formedness, guard verification, and guard checking approve of the object
and its application.
