Tame
Definitions of the various notions of tameness
The adjective ``tame'' can be applied to four different kinds of
objects, LAMBDA objects, function symbols, expressions, and lists of
expressions. Formally, these notions are defined mutually recursively as the
macro tamep-lambdap and the :logic mode functions named
tamep-functionp, tamep, and suitably-tamep-listp,
respectively. We exhibit the formal definitions at the end of this
documentation.
Definitions
- tame LAMBDA object aka tamep-lambdap: An object is a
tame LAMBDA object if is of the form (LAMBDA vars body) or
(LAMBDA vars dcl body) where vars is a list of symbols and
body is a tame expression. Formally, an object x is a tame
LAMBDA object iff (tamep-lambdap x). Tamep-lambdap is
actually a macro.
- tame function aka tamep-functionp: An object is a tame
function iff it is either (a) a badged symbol and ilks is T, or (b)
a tame LAMBDA object (see above). Formally, an object x is a tame
function iff (tamep-functionp x).
- tame expression aka tamep: An object is a tame
expression iff it is a symbol, a quoted constant, the call of an badged
function symbol on the correct number of suitably tame expressions with
respect to the ilks of the function symbol, or the call of a tame LAMBDA
expression on the correct number of tame expressions. Formally, an object
x is a tame expression iff (tamep x). Note that tameness implies
every function symbol in the expression is badged but not necessarily
warranted.
- suitably tame with (respect to arity and ilks) aka
suitably-tamep-listp: A list of objects x is suitably tame
with respect to an arity n and a list of ilks iff x is a true
list of length n, and when an ilk is :FN the corresponding object
is a quoted tame function, when an ilk is :EXPR the object is a
quoted tame expression, and when an ilk is NIL the object is a
tame expression. Formally, an object x is suitably tame with respect to
n and ilks iff (suitably-tamep-listp n ilks x). Note in
particular our use of the word ``quoted'' above. We illustrate this in the
example below.
Note that the various notions of tameness make no mention of whether the
function symbols involved are in :program or :logic mode. The
function symbols must have badges but need not have warrants.
Intuitively, a tame expression can be built out of functions that are not
themselves tame, e.g., scions, by making sure that every :FN slot is
occupied by a quoted tame function. Put another way, if we were to trace the
calls of apply$ while evaluating a tame expression every branch
eventually bottoms out on a call of a primitive. This is illustrated
below.
Examples
We assume the following events have been processed.
(include-book "projects/apply/top" :dir :system)
(defun$ sq (x) (* x x))
(defun$ foldr (lst fn init)
(if (endp lst)
init
(apply$ fn
(list (car lst)
(foldr (cdr lst) fn init)))))
Sq and foldr above are defined as :logic mode functions and
are badged and warranted (note the use of defun$). But for our purposes
they could have been introduced by defun in :program mode and then
badged with two calls of defbadge.
As a result, we see the following badges:
symbol badge
CONS (APPLY$-BADGE 2 1 . T) ; . T means all args ordinary
SQ (APPLY$-BADGE 1 1 . T) ; . T means all args ordinary
FOLDR (APPLY$-BADGE 1 1 NIL :FN NIL)
Consider the following expression.
(foldr lst (lambda$ (x y) (foldr y 'cons (list (sq x)))) nil)
Forgetting about tameness for a moment, what does this term compute?
Study the definition of foldr if you're not familiar with it and work it
out! Answer: It collects, in reverse order, the squares of the elements of
lst. E.g., if lst is (1 2 3 4) the value of the foldr
expression above is (16 9 4 1).
But we are interested in whether it is tame. Tameness is a concept
applied to objects representing formal (fully translated) terms (or
components of terms in the case of ``tame functions,'' ``tame lambdas,''
etc.). Saying ``x is a tame expression'' is just a colloquial way of
saying ``(tamep x) = t. So we can evaluate this
term in the top-level ACL2 loop,
(tamep '(foldr lst (lambda$ (x y) (foldr y 'cons (list (sq x)))) nil))
and the result is nil because lambda$ is not a ``badged function
symbol.'' In fact, lambda$ is not a function symbol. It is a macro.
We're really interested in the formal translation of the foldr
expression. One way to understand the situation is that tamep does not
expand macros.
The translation of the above term is
(FOLDR LST
'(LAMBDA (X Y)
(DECLARE (IGNORABLE X Y))
(RETURN-LAST 'PROGN
'(LAMBDA$ (X Y)
(FOLDR Y 'CONS (LIST (SQ X))))
(FOLDR Y 'CONS (CONS (SQ X) 'NIL))))
'NIL)
The RETURN-LAST subterm is a marker that records the original
user-supplied lambda$ expression, which is needed during compilation and
execution in raw Lisp. But the value of that RETURN-LAST is the
expected FOLDR expression in its last argument. To simplify our
discussion of tameness let's determine whether the following equivalent term
is tame.
(FOLDR LST
'(LAMBDA (X Y)
(FOLDR Y
'CONS
(CONS (SQ X) 'NIL)))
'NIL)
The answer is yes, it is a tame expression. In particular
(tamep '(FOLDR LST
'(LAMBDA (X Y)
(FOLDR Y
'CONS
(CONS (SQ X) 'NIL)))
'NIL))
= T
By the way, tamep answers the same way on the quotation of the
actual translation of the foldr term.
We explain below how tamep computes this result. But before we dive
into details consider what this example illustrates. FOLDR is not a
tame function according to the definitions above. But it can be used in
the construction of tame expressions provided, mainly, that its second
argument is a quoted tame function. Indeed, the example illustrates that we
can even call FOLDR within the LAMBDA expression passed to another
FOLDR and still have a tame expression.
If we were to trace$ the functions tamep,
tamep-functionp, and suitably-tamep-listp, and then call tamep
on the FOLDR term above we would see a tree of calls of the various
tameness notions. Here are selected calls from that tree. All of the calls
return T. We discuss each of these calls below.
(tamep '(CONS (SQ X) 'NIL)) ; [1]
(suitably-tamep-listp 3 ; [2]
'(NIL :FN NIL)
'(Y 'CONS (CONS (SQ X) 'NIL)))
(tamep '(FOLDR Y 'CONS (CONS (SQ X) 'NIL))) ; [3]
(tamep-functionp '(LAMBDA (X Y) ; [4]
(FOLDR Y 'CONS (CONS (SQ X) 'NIL))))
(tamep '(FOLDR LST ; [5]
'(LAMBDA (X Y)
(FOLDR Y 'CONS (CONS (SQ X) 'NIL)))
'NIL))
[1]: The object here, (CONS (SQ X) 'NIL), is tame because both
CONS and SQ are tame functions and they are applied to the correct
number of tame expressions.
[2]: The list of objects here, (Y 'CONS (CONS (SQ X) 'NIL)) is a
suitably tame list of length 3 with ilks NIL, :FN, and
NIL because Y and 'NIL are both tame and 'CONS is a
quoted tame function, CONS.
[3]: The object here is tame because FOLDR is a badged function
of arity 3 and its actuals are suitably tame with respect to its arity and
ilks as shown by example [2].
[4]: The LAMBDA object here is a tame function because it is of
the form (LAMBDA vars body), where vars is the list of symbols
(X Y) and body is the tame object shown in example [4].
[5]: The object here, a call of FOLDR, is tame because there are
3 actuals, the first and third are tame expressions and the second is a
quoted tame function as shown in Example [4].
Logical Definitions
The various notions of tameness, tamep-functionp, tamep, and
suitably-tamep-listp, are defined mutually recursively as :logic
mode functions. The definition employs the macro tamep-lambdap, which
is used by tamep-functionp to handle the LAMBDA case.
Function: tamep-functionp
(defun tamep-functionp (fn)
(declare (xargs :guard t))
(if (symbolp fn)
(let ((bdg (badge fn)))
(and bdg
(eq (access apply$-badge bdg :ilks) t)))
(and (consp fn) (tamep-lambdap fn))))
Function: tamep
(defun tamep (x)
(declare (xargs :guard t))
(cond
((atom x) (symbolp x))
((eq (car x) 'quote)
(and (consp (cdr x)) (null (cddr x))))
((symbolp (car x))
(let ((bdg (badge (car x))))
(cond ((null bdg) nil)
((eq (access apply$-badge bdg :ilks) t)
(suitably-tamep-listp (access apply$-badge bdg :arity)
nil (cdr x)))
(t (suitably-tamep-listp (access apply$-badge bdg :arity)
(access apply$-badge bdg :ilks)
(cdr x))))))
((consp (car x))
(let ((fn (car x)))
(and (tamep-lambdap fn)
(suitably-tamep-listp (length (cadr fn))
nil (cdr x)))))
(t nil)))
Function: suitably-tamep-listp
(defun suitably-tamep-listp (n flags args)
(declare (xargs :guard (and (natp n) (true-listp flags))))
(cond ((zp n) (null args))
((atom args) nil)
(t (and (let ((arg (car args)))
(case (car flags)
(:fn (and (consp arg)
(eq (car arg) 'quote)
(consp (cdr arg))
(null (cddr arg))
(tamep-functionp (cadr arg))))
(:expr (and (consp arg)
(eq (car arg) 'quote)
(consp (cdr arg))
(null (cddr arg))
(tamep (cadr arg))))
(otherwise (tamep arg))))
(suitably-tamep-listp (- n 1)
(cdr flags)
(cdr args))))))
Macro: tamep-lambdap
(defmacro tamep-lambdap (fn)
(list 'let
(list (list 'fn fn))
'(and (lambda-object-shapep fn)
(symbol-listp (lambda-object-formals fn))
(tamep (lambda-object-body fn)))))
At the top-level of the ACL2 loop you can determine whether an object
satisfies one of these predicates by calling the appropriate formal notion on
the object. But because these functions are defined in terms of badge these notions of tameness are evaluable only in the evaluation
theory (where warrants are implicitly assumed). If you want to prove
that an object is tame, you may need warrant hypotheses. See guarantees-of-the-top-level-loop.
