APT tail recursion transformation: turn a recursive function that is not tail-recursive into an equivalent tail-recursive function.

Under certain conditions, the computations performed by a recursive function that is not tail-recursive can be re-arranged so that they can be performed by a tail-recursive function whose arguments do not grow in the same way as the call stack of the original function. A tail-recursive function can be compiled into an imperative loop that does not run out of space due to the call stack growth.

The

The file

(tailrec old :variant ; default :monoid :domain ; default :auto :new-name ; default :auto :new-enable ; default :auto :accumulator ; default :auto :wrapper ; default nil :wrapper-name ; default :auto :wrapper-enable ; default from table :old-to-new-name ; default from table :old-to-new-enable ; default from table :new-to-old-name ; default from table :new-to-old-enable ; default from table :old-to-wrapper-name ; default from table :old-to-wrapper-enable ; default from table :wrapper-to-old-name ; default from table :wrapper-to-old-enable ; default from table :verify-guards ; default :auto :hints ; default nil :print ; default :result :show-only ; default nil )

Denotes the target function to transform.

It must be the name of a function, or a

numbered name with a wildcard index that resolves to the name of a function. In the rest of this documentation page, for expository convenience, it is assumed that old is the name of the denoted function.

old must be in logic mode, be defined, return a non-multiple value, have no input or output stobjs, be singly (not mutually) recursive, and not have a :? measure. If the:verify-guards input oftailrec ist ,old must be guard-verified.In the

tailrec design notes,old is denoted byf .With the body in

translated form, and after expanding all lambda expressions (i.e. lets), the function must have one of the forms;; form 1: (defun old (x1 ... xn) (if test<x1,...,xn> base<x1,...,xn> combine<nonrec<x1,...,xn>, (old update-x1<x1,...,xn> ... update-xn<x1,...,xn>)>)) ;; form 2: (defun old (x1 ... xn) (if ntest<x1,...,xn> combine<nonrec<x1,...,xn>, (old update-x1<x1,...,xn> ... update-xn<x1,...,xn>)> base<x1,...,xn>))where:

- The term
test<x1,...,xn> (in form 1) orntest<x1,...,xn> (in form 2) does not callold . This term computes the exit test of the recursion (in form 1) or its negation (in form 2). Ifold has form 2, lettest<x1,...,xn> be: either (i) the negation ofntest<x1,...,xn> , i.e.(not ntest<x1,...,xn>) ifntest<x1,...,xn> is not a call ofnot; or (ii) the argument ofntest<x1,...,xn> ifntest<x1,...,xn> is a call ofnot, i.e.ntest<x1,...,xn> is(not test<x1,...,xn>) . Thus, in the rest of this documentation, we can assume thatold has form 1 without loss of generality. In thetailrec design notes,test<x1,...,xn> is denoted bya(\overline{x}) .- The term
base<x1,...,xn> does not callold . This term computes the base value of the recursion. In thetailrec design notes,base<x1,...,xn> is denoted byb(\overline{x}) . If the:variant input oftailrec is:monoid or:monoid-alt (see below), the termbase<x1,...,xn> must be ground, i.e. actually not contain any of thexi variables. The section `Special case: Ground Base Value' of the design notes shows that this restriction (which may be lifted eventually) avoids the need to generate and use the function\beta . (When the:variant input is:assoc or:assoc-alt , no\beta needs to be generated anyway, and thus the restriction does not apply.)- The term
combine<nonrec<x1,...,xn>, (old update-x1<x1,...,xn> ... update-xn<x1,...,xn>)> contains one or more identical calls toold , namely(old update-x1<x1,...,xn> ... update-xn<x1,...,xn>) , where eachupdate-xi<x1,...,xn> is a term that does not callold . In thetailrec design notes,update-xi<x1,...,xn> is denoted byd_i(\overline{x}) . Letcombine<nonrec<x1,...,xn>,r> be the result of replacing(old update-x1<x1,...,xn> ... update-xn<x1,...,xn>) with a fresh variabler .- The term
combine<nonrec<x1,...,xn>,r> is not justr (otherwiseold would already be tail-recursive).- The term
combine<nonrec<x1,...,xn>,r> is not a call ofif.- All the occurrences of
x1 , ...,xn incombine<nonrec<x1,...,xn>,r> are within a subtermnonrec<x1,...,xn> wherer does not occur. This means that ifcombine<q,r> is the result of replacing all the occurrences ofnonrec<x1,...,xn> with a fresh variableq , then noxi occurs incombine<q,r> . The termcombine<q,r> represents a binary operator that combinesnonrec<x1,...,xn> (which does not involve the recursive call toold ) with the result of the recursive call toold . The constraints just given may be satisfied by multiple subtermsnonrec<x1,...,xn> ofcombine<nonrec<x1,...,xn>,r> : the exactnonrec<x1,...,xn> is determined via the procedure described in Section `Decomposition of the Recursive Branch' below. In thetailrec design notes,nonrec<x1,...,xn> is denoted byc(\overline{x}) , and(lambda (q r) combine<q,r>) is denoted by* .

Indicates the variant of the transformation to use:

:monoid , for the monoidal variant, where the applicability conditions below imply the algebraic structure of a monoid (i.e. associativity and identity) for the combination operator. In thetailrec design notes, this variant is described in the sections `Associative Binary Operator with Left and Right Identity' and `Restriction of Operator Properties to a Domain'.:monoid-alt , for the alternative monoidal variant, where the applicability conditions below also imply the algebraic structure of a monoid (i.e. associativity and identity) for the combination operator. In thetailrec design notes, this variant is described in the section `Extension of Operator Associativity and Closure outside the Domain'.:assoc , for the associative variant, where the applicability conditions below imply the algebraic structure of a semigroup (i.e. associativity only) for the combination operator. In thetailrec design notes, this variant is described in the sections `Associative Binary Operator' and `Restriction of Operator Properties to a Domain'.:assoc-alt , for the alternative associative variant, where the applicability conditions below also imply the algebraic structure of a semigroup (i.e. associativity only) for the combination operator. In thetailrec design notes, this variant is described in the section `Associative-Only Variant,Extended outside the Domain'.The associative variants of the transformation is more widely applicable, but the monoidal variants yield simpler new functions. The applicability conditions for the alternative monoidal variant are neither stronger nor weaker than the ones for the monoidal variant, so these two variants apply to different cases. Similarly, the applicability conditions for the alternative associative variant are neither stronger nor weaker than the ones for the associative variant, so these two variants apply to different cases.

While the

tailrec design notesshow how to handle variants in which, besides associativity, only either left or right identity holds, the current implementation does not handle them independently. They are either both absent (in the:assoc and:assoc-alt variants) or both present (in the:monoid and:monoid-alt variants). Support for their independent handling may be added eventually.

Denotes the domain (i.e. predicate)

domain over which the combination operatorcombine<q,r> must satisfy some of the applicability conditions below.It must be one of the following:

- The name of a unary logic-mode function. This function must have no input or output ACL2::stobjs. This function must return a single (i.e. non-
mv) result. If the function(s) generated bytailrec is/are guard-verified (which is determined by the:verify-guards input; see below), then this function must be guard-verified. This function must be distinct fromold .- A unary closed lambda expression that only references logic-mode functions. This lambda expression must have no input or output ACL2::stobjs. This lambda expression must return a single (i.e. non-
mv) result. If the function(s) generated bytailrec is/are guard-verified (which is determined by the:verify-guards input; see below), then the body of this lambda expression must only call guard-verified functions, except possibly in the:logic subterms ofmbes or viaec-call. As an abbreviation, the namemac of a macro stands for the lambda expression(lambda (z1 z2 ...) (mac z1 z2 ...)) , wherez1 ,z2 , ... are the required parameters ofmac ; that is, a macro name abbreviates its eta-expansion (considering only the macro's required parameters). This lambda expression must not referenceold .:auto , to automatically infer a domain as described in Section `Automatic Inference of a Domain' below.In the rest of this documentation page, let

domain be this function or lambda expression.In the

tailrec design notes,domain is denoted byD .

Determines the name of the generated new function.

It must be one of the following:

:auto , to generate the name automatically as described in function-name-generation.- Any other symbol, to use as the name of the function.
In the rest of this documentation page, let

new be this function.

Determines whether

new is enabled.It must be one of the following:

t , to enable it.nil , to disable it.:auto , to enable it iffold is enabled.

Determines the name of the accumulator argument of

new :

:auto , to use the fresh variabler described above.- Any other symbol that is a valid formal parameter name and that is distinct from
x1 , ...,xn .In the rest of this documentation page, let

a be this variable.

Determines whether the wrapper function is generated.

It must be one of the following:

t , to generate it.nil , to not generate it.

Determines the name of the generated wrapper function.

It must be one of the following:

:auto , to generate the name automatically as described in function-name-generation.- Any other symbol, to use as the name of the function.
This input may be present only if the

:wrapper input ist .In the rest of this documentation page, let

wrapper be this function.

Determines whether the wrapper function is enabled.

It must be one of the following:

t , to enable it.nil , to disable it.- Absent, to use the value from the APT defaults table, which is set via
set-default-input-wrapper-enable.This input may be present only if the

:wrapper input ist .

Determines the name of the theorem that rewrites the old function in terms of the new function.

It must be one of the following:

- A keyword, to use as separator between the names of
old andnew . A keyword:kwd specifies the theorem nameoldkwdnew , in the same package asnew .- Any other symbol, to use as the name of the theorem.
- Absent, to use the value from the APT defaults table, which is set via
set-default-input-old-to-new-name.In the rest of this documentation page, let

old-to-new be the name of this theorem.

Determines whether the

old-to-new theorem is enabled.It must be one of the following:

t , to enable the theorem.nil , to disable the theorem.- Absent, to use the value from the APT defaults table, which is set via
set-default-input-old-to-new-enable.If this input is

t , the:new-to-old-enable input must benil . At most one of these two inputs may bet at any time.

Determines the name of the theorem that rewrites the new function in terms of the old function.

It must be one of the following:

- A keyword, to use as separator between the names of
new andold . A keyword:kwd specifies the theorem namenewkwdold , in the same package asnew .- Any other symbol, to use as the name of the theorem.
- Absent, to use the value from the APT defaults table, which is set via
set-default-input-new-to-old-name.In the rest of this documentation page, let

new-to-old be the name of this theorem.

Determines whether the

new-to-old theorem is enabled.It must be one of the following:

t , to enable the theorem.nil , to disable the theorem.- Absent, to use the value from the APT defaults table, which is set via
set-default-input-new-to-old-enable.If this input is

t , the:old-to-new-enable input must benil . At most one of these two inputs may bet at any time.

Determines the name of the theorem that rewrites the old function in terms of the wrapper function.

It must be one of the following:

- A keyword, to use as separator between the names of
old andwrapper . A keyword:kwd specifies the theorem nameoldkwdwrapper , in the same package aswrapper .- Any other symbol, to use as the name of the theorem.
- Absent, to use the value from the APT defaults table, which is set via
set-default-input-old-to-wrapper-name.This input may be present only if the

:wrapper input ist .In the rest of this documentation page, let

old-to-wrapper be the name of this theorem (if it is generated).

Determines whether the

old-to-wrapper theorem is enabled.It must be one of the following:

t , to enable the theorem.nil , to disable the theorem.- Absent, to use the value from the APT defaults table, which is set via
set-default-input-old-to-wrapper-enable.This input may be present only if the

:wrapper input ist .If this input is

t , the:wrapper-to-old-enable input must benil . At most one of these two inputs may bet at any time.

Determines the name of the theorem that rewrites the wrapper function in terms of the old function.

It must be one of the following:

- A keyword, to use as separator between the names of
wrapper andold . A keyword:kwd specifies the theorem namewrapperkwdold , in the same package aswrapper .- Any other symbol, to use as the name of the theorem.
- Absent, to use the value from the APT defaults table, which is set via
set-default-input-wrapper-to-old-name.This input may be present only if the

:wrapper input ist .In the rest of this documentation page, let

wrapper-to-old be the name of this theorem (if it is generated).

Determines whether the

wrapper-to-old theorem is enabled.It must be one of the following:

t , to enable the theorem.nil , to disable the theorem.- Absent, to use the value from the APT defaults table, which is set via
set-default-input-wrapper-to-old-enable.This input may be present only if the

:wrapper input ist .If this input is

t , the:old-to-wrapper-enable input must benil . At most one of these two inputs may bet at any time.

Determines whether the guards of the generated functions are verified or not.

It must be one of the following:

t , to verify the guards.nil , to not verify guards.:auto , to verify the guards if and only if the guards of the target functionold are verified.

Hints to prove the applicability conditions.

It must be one of the following:

- A keyword-value list
(appcond1 hints1 appcond2 hints2 ...) , where eachappcondk is a keyword that identifies one of the applicability conditions listed in the `Applicability Conditions' section and eachhintsk is a list of hints of the kind that may appear just after:hints in adefthm. The hintshintsk are used to prove applicability conditionappcondk . Theappcond1 ,appcond2 , ... keywords must be all distinct. Anappcondk keyword is allowed only if the corresponding applicability condition is present, as specified in the `Applicability Conditions' section.- A list of hints of the kind that may appear just after
:hints in adefthm. In this case, these same hints are used to prove every applicability condition,.

Specifies what is printed on the screen (see ACL2::event-macro-screen-printing).

It must be one of the following:

nil , to print nothing (not even error output).:error , to print only error output (if any).:result , to print, besides any error output, also the results oftailrec . This is the default value of the:info , to print, besides any error output and the results, also some additional information about the internal operations oftailrec .:all , to print, besides any error output, the results, and the additional information, also ACL2's output in response to all the submitted events.If the call of

tailrec is redundant, an indication to that effect is printed on the screen, unlessnil .

Determines whether the event expansion of

tailrec is submitted to ACL2 or just printed on the screen:

nil , to submit it.t , to just print it. In this case: the event expansion is printed even ifnil (because the user has explicitly asked to show the event expansion); the resulting events are not re-printed separately (other than their appearance in the printed event expansion) even if:result or:info or:all ; no ACL2 output is printed for the event expansion even if:all (because the event expansion is not submitted). If the call oftailrec is redundant (as defined in the `Redundancy' section), the event expansion generated by the existing call is printed.

Replace every occurrence of the recursive call

Try to find the maximal and leftmost subterm

If such a term

If such a term

In the

Consider the following conditions:

- The
:variant input oftailrec is:monoid or:monoid-alt . - The term
combine<q,r> (described above) has the form(op q r) or(op r q) , whereop is a named function, with formalsy1 andy2 . - The guard term of
op has one of the forms (i)(and (dom y1) (dom y2)) , (ii)(and (dom y2) (dom y1)) , (iii)(dom y1) , and (iv)(dom y2) , wheredom is a named function.

If all the above coditions hold, the inferred domain is

This domain inference is a heuristic. It has no impact on soundness, since the user could supply any domain anyhow. Inferring a tigther domain than the one consisting of all values may be helpful to prove left and right identity, which may not hold over all values (e.g. left and right identity of addition). On the other hand, associativity may hold over all values (e.g. associativity of addition), particularly when the combination operator fixes its arguments. Given that using a tighter domain than all values involves additional applicability conditions below, it seems most useful to attempt to infer a tighter domain only for the monoidal variants, and use the domain of all values for the associative variants.

In order for

The base computation always returns values in the domain:

(implies test<x1,...,xn> (domain base<x1,...,xn>))This corresponds to

\mathit{Db} in thetailrec design notes.This applicability condition is present if and only if the

:variant input oftailrec is:monoid or:monoid-alt or:assoc .

The non-recursive operand of the combination operator always returns values in the domain, when the exit test of the recursion fails:

(implies (not test<x1,...,xn>) (domain nonrec<x1,...,xn>))This corresponds to

\mathit{Dc} in thetailrec design notes.This applicability condition is present if and only if the

:variant input oftailrec is:monoid or:assoc .

The domain is closed under the combination operator:

(implies (and (domain u) (domain v)) (domain combine<u,v>))This corresponds to

D* in thetailrec design notes.This applicability condition is present if and only if the

:variant input oftailrec is:monoid or:assoc or:assoc-alt .

The combination operator unconditionally returns values in the domain:

(domain combine<u,v>)This corresponds to

D*' in thetailrec design notes.This applicability condition is present if and only if the

:variant input oftailrec is:monoid-alt .

The combination operator is associative over the domain:

(implies (and (domain u) (domain v) (domain w)) (equal combine<u,combine<v,w>> combine<combine<u,v>,w>))This corresponds to

\mathit{ASC} in thetailrec design notes.This applicability condition is present if and only if the

:variant input oftailrec is:monoid or:assoc .

The combination operator is unconditionally associative:

(equal combine<u,combine<v,w>> combine<combine<u,v>,w>)This corresponds to

\mathit{ASC}' in thetailrec design notes.This applicability condition is present if and only if the

:variant input oftailrec is:monoid-alt or:assoc-alt .

The base value of the recursion is left identity of the combination operator:

(implies (and test<x1,...,xn> (domain u)) (equal combine<base<x1...,xn>,u> u))This corresponds to

\mathit{LI} in thetailrec design notes.This applicability condition is present if and only if the

:variant input oftailrec is:monoid or:monoid-alt .

The base value of the recursion is right identity of the combination operator:

(implies (and test<x1,...,xn> (domain u)) (equal combine<u,base<x1...,xn>> u))This corresponds to

\mathit{RI} in thetailrec design notes.This applicability condition is present if and only if the

:variant input oftailrec is:monoid or:monoid-alt .

The domain is well-defined (according to its guard) on every value:

domain-guard<z>where

domain-guard<z> is the guard term ofdomain ifdomain is a function name, while it is the guard obligation ofdomain ifdomain is a lambda expression.This corresponds to

\mathit{GD} in thetailrec design notes.This applicability condition is present if and only if the function(s) generated by

tailrec is/are guard-verified (which is determined by the:verify-guards input oftailrec )..

The combination operator is well-defined (according to its guard) on every value in the domain:

(implies (and (domain q) (domain r)) combine-guard<q,r>)where

combine-guard<q,r> is the guard obligation ofcombine<q,r> .This corresponds to

G* in thetailrec design notes.This applicability condition is present if and only if the function(s) generated by

tailrec is/are guard-verified (which is determined by the:verify-guards input oftailrec )..

The base computation returns values in the domain, when the exit test of the recursion succeeds, and under the guard of

old :(implies (and old-guard<x1,...,xn> test<x1,...,xn>) (domain base<x1,...,xn>))where

old-guard<x1,...,xn> is the guard term ofold .This corresponds to

\mathit{GDb} in thetailrec design notes.This applicability condition is present if and only if the function(s) generated by

tailrec is/are guard-verified (which is determined by the:verify-guards input oftailrec ) and the:variant input oftailrec is:assoc-alt .

The non-recursive operand of the combination operator returns values in the domain, when the exit test of the recursion fails, and under the guard of

old :(implies (and old-guard<x1,...,xn> (not test<x1,...,xn>)) (domain nonrec<x1,...,xn>))where

old-guard<x1,...,xn> is the guard term ofold .This corresponds to

\mathit{GDc} in thetailrec design notes.This applicability condition is present if and only if the function(s) generated by

tailrec is/are guard-verified (which is determined by the:verify-guards input oftailrec ) and the:variant input oftailrec is:monoid-alt or:assoc-alt .

When present,

Tail-recursive equivalent of

old :;; when the :variant input of tailrec is :monoid or :monoid-alt: (defun new (x1 ... xn a) (if test<x1,...,xn> a (new update-x1<x1,...,xn> ... update-xn<x1,...,xn> combine<a,nonrec<x1,...,xn>>))) ;; when the :variant input of tailrec is :assoc or :assoc-alt: (defun new (x1 ... xn a) (if test<x1,...,xn> combine<a,base<x1,...,xn>> (new update-x1<x1,...,xn> ... update-xn<x1,...,xn> combine<a,nonrec<x1,...,xn>>)))The measure term and well-founded relation of

new are the same asold .The guard is

(and old-guard<x1,...,xn> (domain a)) , whereold-guard<x1,...,xn> is the guard term ofold .In the

tailrec design notes,new is denoted byf' .

Non-recursive wrapper of

new :;; when the :variant input of tailrec is :monoid or :monoid-alt: (defun wrapper (x1 ... xn) (new x1 ... xn base<x1,...,xn>)) ;; when the :variant input tailrec is :assoc or :assoc-alt: (defun wrapper (x1 ... xn) (if test<x1,...,xn> base<x1,...,xn> (new update-x1<x1,...,xn> ... update-xn<x1,...,xn> nonrec<x1,...,xn>)))The guard is the same as

old .This is generated only if the

:wrapper input ist .In the

tailrec design notes,new is denoted by\tilde{f} .

Theorem that rewrites

old in terms ofnew :;; when the :variant input of tailrec is :monoid or :monoid-alt: (defthm old-to-new (equal (old x1 ... xn) (new x1 ... xn base<x1,...,xn>))) ;; when the :variant input of tailrec is :assoc or :assoc-alt: (defthm old-to-new (equal (old x1 ... xn) (if test<x1,...,xn> base<x1,...,xn> (new update-x1<x1,...,xn> ... update-xn<x1,...,xn> nonrec<x1,...,xn>))))In the

tailrec design notes,old-to-new is denoted byf\!f' .

Theorem that rewrites

new in terms ofold :;; when the :variant input of tailrec is ;; :monoid or :monoid-alt or :assoc: (defthm new-to-old (implies (domain a) (equal (new x1 ... xn a) combine<a,(old x1 ... xn)>))) ;; when the :variant input of tailrec is :assoc-alt: (defthm new-to-old (equal (new x1 ... xn a) combine<a,(old x1 ... xn)>))In the

tailrec design notes,new-to-old is denoted byf'\!f .

Theorem that rewrites

old in terms ofwrapper :(defthm old-to-wrapper (equal (old x1 ... xn) (wrapper x1 ... xn)))This is generated only if the

:wrapper input ist .In the

tailrec design notes,old-to-wrapper is denoted byf\!\tilde{f} .

Theorem that rewrites

wrapper in terms ofold :(defthm wrapper-to-old (equal (wrapper x1 ... xn) (old x1 ... xn)))This is generated only if the

:wrapper input ist .In the

tailrec design notes,old-to-wrapper is denoted by\tilde{f}\!f .

A theory invariant is also generated to prevent

A theory invariant is also generated to prevent

A call of

A call of

- Tailrec-implementation
- Implementation of
`tailrec`.