# Tail-recursive-p

Check if a singly recursive function is tail-recursive.

- Signature
(tail-recursive-p fn wrld) → yes/no

- Arguments
`fn` — Guard (and (symbolp fn) (= 1 (len (irecursivep fn wrld)))).
`wrld` — Guard (plist-worldp wrld).
- Returns
`yes/no` — Type (booleanp 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 fn
(in which case it is a tail-recursive call),
and when the called function is not fn
(in which case it is not a recursive call).

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.

### Definitions and Theorems

**Function: **tail-recursive-p-aux

(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: **booleanp-of-tail-recursive-p-aux

(defthm booleanp-of-tail-recursive-p-aux
(b* ((yes/no (tail-recursive-p-aux fn term)))
(booleanp yes/no))
:rule-classes :rewrite)

**Function: **tail-recursive-p

(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: **booleanp-of-tail-recursive-p

(defthm booleanp-of-tail-recursive-p
(b* ((yes/no (tail-recursive-p fn wrld)))
(booleanp yes/no))
:rule-classes :rewrite)