Definitions of the various notions of tameness

The adjective ``tame'' can be applied to four different kinds of
objects,

**tame**akaLAMBDA objecttamep-lambdap : An object is a tameLAMBDA object if is of the form(LAMBDA vars body) or(LAMBDA vars dcl body) wherevars is a list of symbols andbody is a tame expression. Formally, an objectx is a tameLAMBDA object iff(tamep-lambdap x) .Tamep-lambdap is actually a macro.**tame function**akatamep-functionp : An object is a*tame function*iff it is either (a) a badged symbol and ilks isT , or (b) a tameLAMBDA object (see above). Formally, an objectx is a tame function iff(tamep-functionp x) .**tame expression**akatamep : 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 tameLAMBDA expression on the correct number of tame expressions. Formally, an objectx 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)**akasuitably-tamep-listp : A list of objectsx is*suitably tame*with respect to an arityn and a list ofilks iffx is a true list of lengthn , 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 isNIL the object is a tame expression. Formally, an objectx is suitably tame with respect ton andilks 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

Intuitively, a tame expression can be built out of functions that are not
themselves tame, e.g., scions, by making sure that every

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)))))

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

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 ``*x*

(tamep '(foldr lst (lambda$ (x y) (foldr y 'cons (list (sq x)))) nil))

and the result is

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

(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,

We explain below how *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

If we were to `trace$` the functions

(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))

*quoted* tame function,

*quoted* tame function as shown in Example

The various notions of tameness,

**Function: **

(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: **

(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: **

(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: **

(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 `warrant`s 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.