Check if a singly recursive function is tail-recursive.
(tail-recursive-p fn wrld) → yes/no
A singly recursive function is tail-recursive if each of its recursive calls are the last action taken by the function on that execution path. We recursively examine the body of the function to see whether that is the case.
Variables and quoted constants cannot contain recursive calls and thus pass the check. Calls of if are non-strict, and thus they are treated specially: they pass the check if their `then' and `else' branches individually pass the check (since just one of these branches is executed each time) and their test has no recursive calls (because after the test a branch has to be evaluated, so evaluating the test is never the function's last action).
Calls of other named functions pass the check
if the arguments do not contain recursive calls.
This applies both when the called function is
Calls of lambda expressions pass the check if the arguments do not contain recursive calls and the body of the lambda expression passes the check. The body of the lambda expression is the last thing to be evaluated in the call.
Function:
(defun tail-recursive-p-aux (fn term) (declare (xargs :guard (and (symbolp fn) (pseudo-termp term)))) (let ((__function__ 'tail-recursive-p-aux)) (declare (ignorable __function__)) (b* (((when (variablep term)) t) ((when (fquotep term)) t) ((when (eq (ffn-symb term) 'if)) (and (not (ffnnamep fn (fargn term 1))) (tail-recursive-p-aux fn (fargn term 2)) (tail-recursive-p-aux fn (fargn term 3)))) ((when (ffnnamep-lst fn (fargs term))) nil) ((when (symbolp (ffn-symb term))) t)) (tail-recursive-p-aux fn (lambda-body (ffn-symb term))))))
Theorem:
(defthm booleanp-of-tail-recursive-p-aux (b* ((yes/no (tail-recursive-p-aux fn term))) (booleanp yes/no)) :rule-classes :rewrite)
Function:
(defun tail-recursive-p (fn wrld) (declare (xargs :guard (and (plist-worldp wrld) (and (symbolp fn) (= 1 (len (irecursivep fn wrld))))))) (let ((__function__ 'tail-recursive-p)) (declare (ignorable __function__)) (tail-recursive-p-aux fn (ubody+ fn wrld))))
Theorem:
(defthm booleanp-of-tail-recursive-p (b* ((yes/no (tail-recursive-p fn wrld))) (booleanp yes/no)) :rule-classes :rewrite)