		Search-engine friendly clone of the ACL2 documentation.

Tailrec

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

Introduction

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 tailrec design notes, which use this notation, provide the mathematical concepts and template proofs upon which this transformation is based. These notes should be read alongside this reference documentation, which refers to them in some places.

The community book kestrel/apt/tailrec-examples.lisp contains some commented examples of use of tailrec.

General Form

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

Inputs

old

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 of tailrec is t, old must be guard-verified.
In the tailrec design notes, old is denoted by f.
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) or ntest<x1,...,xn> (in form 2) does not call old. This term computes the exit test of the recursion (in form 1) or its negation (in form 2). If old has form 2, let test<x1,...,xn> be: either (i) the negation of ntest<x1,...,xn>, i.e. (not ntest<x1,...,xn>), if ntest<x1,...,xn> is not a call of not; or (ii) the argument of ntest<x1,...,xn> if ntest<x1,...,xn> is a call of not, i.e. if ntest<x1,...,xn> is (not test<x1,...,xn>). Thus, in the rest of this documentation, we can assume that old has form 1 without loss of generality. In the tailrec design notes, test<x1,...,xn> is denoted by a(\overline{x}).
The term base<x1,...,xn> does not call old. This term computes the base value of the recursion. In the tailrec design notes, base<x1,...,xn> is denoted by b(\overline{x}). If the :variant input of tailrec is :monoid or :monoid-alt (see below), the term base<x1,...,xn> must be ground, i.e. actually not contain any of the xi 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 to old, namely (old update-x1<x1,...,xn> ... update-xn<x1,...,xn>), where each update-xi<x1,...,xn> is a term that does not call old. In the tailrec design notes, update-xi<x1,...,xn> is denoted by d_i(\overline{x}). Let combine<nonrec<x1,...,xn>,r> be the result of replacing (old update-x1<x1,...,xn> ... update-xn<x1,...,xn>) with a fresh variable r.
The term combine<nonrec<x1,...,xn>,r> is not just r (otherwise old would already be tail-recursive).
The term combine<nonrec<x1,...,xn>,r> is not a call of if.
All the occurrences of x1, ..., xn in combine<nonrec<x1,...,xn>,r> are within a subterm nonrec<x1,...,xn> where r does not occur. This means that if combine<q,r> is the result of replacing all the occurrences of nonrec<x1,...,xn> with a fresh variable q, then no xi occurs in combine<q,r>. The term combine<q,r> represents a binary operator that combines nonrec<x1,...,xn> (which does not involve the recursive call to old) with the result of the recursive call to old. The constraints just given may be satisfied by multiple subterms nonrec<x1,...,xn> of combine<nonrec<x1,...,xn>,r>: the exact nonrec<x1,...,xn> is determined via the procedure described in Section `Decomposition of the Recursive Branch' below. In the tailrec design notes, nonrec<x1,...,xn> is denoted by c(\overline{x}), and (lambda (q r) combine<q,r>) is denoted by *.

:variant — default :monoid

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 the tailrec 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 the tailrec 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 the tailrec 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 the tailrec 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 notes show 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.

:domain — default :auto

Denotes the domain (i.e. predicate) domain over which the combination operator combine<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 stobjs. This function must return a single (i.e. non-mv result. If the function(s) generated by tailrec 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 from old.
A unary closed lambda expression that only references logic-mode functions. This lambda expression must have no input or output stobjs. This lambda expression must return a single (i.e. non-mv result. If the function(s) generated by tailrec 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 of mbes or via ec-call. As an abbreviation, the name mac of a macro stands for the lambda expression (lambda (z1 z2 ...) (mac z1 z2 ...)), where z1, z2, ... are the required parameters of mac; that is, a macro name abbreviates its eta-expansion (considering only the macro's required parameters). This lambda expression must not reference old.
: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 by D.

:new-name — default :auto

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 the name of this function.

:new-enable — default :auto

Determines whether new is enabled.
It must be one of the following:
t, to enable it.
nil, to disable it.
:auto, to enable it iff old is enabled.

:accumulator — default :auto

Determines the name of the accumulator argument of new:
:auto, to use the fresh variable r 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.

:wrapper — default nil

Determines whether the wrapper function is generated.
It must be one of the following:
t, to generate it.
nil, to not generate it.

:wrapper-name — default :auto

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 is t.
In the rest of this documentation page, let wrapper be the name of this function.

:wrapper-enable — default from table

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 is t.

:old-to-new-name — default from table

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 and new. A keyword :kwd specifies the theorem name oldkwdnew, in the same package as new.
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.

:old-to-new-enable — default from table

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 be nil. At most one of these two inputs may be t at any time.

:new-to-old-name — default from table

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 and old. A keyword :kwd specifies the theorem name newkwdold, in the same package as new.
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.

:new-to-old-enable — default from table

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 be nil. At most one of these two inputs may be t at any time.

:old-to-wrapper-name — default from table

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 and wrapper. A keyword :kwd specifies the theorem name oldkwdwrapper, in the same package as wrapper.
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 is t.
In the rest of this documentation page, let old-to-wrapper be the name of this theorem (if it is generated).

:old-to-wrapper-enable — default from table

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 is t.
If this input is t, the :wrapper-to-old-enable input must be nil. At most one of these two inputs may be t at any time.

:wrapper-to-old-name — default from table

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 and old. A keyword :kwd specifies the theorem name wrapperkwdold, in the same package as wrapper.
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 is t.
In the rest of this documentation page, let wrapper-to-old be the name of this theorem (if it is generated).

:wrapper-to-old-enable — default from table

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 is t.
If this input is t, the :old-to-wrapper-enable input must be nil. At most one of these two inputs may be t at any time.

:verify-guards — default :auto

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 function old are verified.

:hints — default nil

Hints to prove the applicability conditions.
It must be one of the following:
A keyword-value list (appcond1 hints1 appcond2 hints2 ...), where each appcondk is a keyword that identifies one of the applicability conditions listed in the `Applicability Conditions' section and each hintsk is a list of hints of the kind that may appear just after :hints in a defthm. The hints hintsk are used to prove applicability condition appcondk. The appcond1, appcond2, ... keywords must be all distinct. An appcondk 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 a defthm. In this case, these same hints are used to prove every applicability condition,.

:print — default :result

Specifies what is printed on the screen (see 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 of tailrec. This is the default value of the :print input.
:info, to print, besides any error output and the results, also some additional information about the internal operations of tailrec.
: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, unless :print is nil.

:show-only — default nil

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 if :print is nil (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 :print is :result or :info or :all; no ACL2 output is printed for the event expansion even if :print is :all (because the event expansion is not submitted). If the call of tailrec is redundant (as defined in the `Redundancy' section), the event expansion generated by the existing call is printed.

Decomposition of the Recursive Branch

Replace every occurrence of the recursive call (old update-x1<x1,...,xn> ... update-xn<x1,...,xn>) in the recursive branch combine<nonrec<x1,...,xn>, (old update-x1<x1,...,xn> ... update-xn<x1,...,xn>)> of old with a fresh variable r, obtaining combine<nonrec<x1,...,xn>,r>.

Try to find the maximal and leftmost subterm nr of combine<nonrec<x1,...,xn>,r> such that r does not occur in nr and such that all the occurrences of x1, ..., xn in combine<nonrec<x1,...,xn>,r> occur within occurrences of nr in combine<nonrec<x1,...,xn>,r>. The latter constraint is equivalent to saying that after replacing all the occurrences of nr in combine<nonrec<x1,...,xn>,r> with a fresh variable q, the resulting term will have only r and q as free variables.

If such a term nr exists, that term is nonrec<x1,...,xn>, and combine<q,r> is the result of replacing every occurrence of nonrec<x1,...,xn> in combine<nonrec<x1,...,xn>,r> with q.

If such a term nr does not exist, decomposition fails.

In the tailrec design notes, the section `Decomposition of the Old Function' describes a more general decomposition process, which has multiple solutions in general. The current implementation follows the procedure detailed in the paragraphs above.

Automatic Inference of a Domain

Consider the following conditions:

The :variant input of tailrec is :monoid or :monoid-alt.
The term combine<q,r> (described above) has the form (op q r) or (op r q), where op is a named function, with formals y1 and y2.
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), where dom is a named function.

If all the above coditions hold, the inferred domain is dom. Otherwise, the inferred domain is (lambda (x) t), i.e. the domain consisting of all values.

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.

Applicability Conditions

In order for tailrec to apply, in addition to the requirements on the inputs stated in the `Inputs' section, the following applicability conditions must be proved. The proofs are attempted when tailrec is called, using the hints optionally supplied as the :hints input described in the `Inputs' section.

:domain-of-base

The base computation always returns values in the domain:
(implies test<x1,...,xn>
         (domain base<x1,...,xn>))
This corresponds to \mathit{Db} in the tailrec design notes.
This applicability condition is present if and only if the :variant input of tailrec is :monoid or :monoid-alt or :assoc.

:domain-of-nonrec

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 the tailrec design notes.
This applicability condition is present if and only if the :variant input of tailrec is :monoid or :assoc.

:domain-of-combine

The domain is closed under the combination operator:
(implies (and (domain u)
              (domain v))
         (domain combine<u,v>))
This corresponds to D* in the tailrec design notes.
This applicability condition is present if and only if the :variant input of tailrec is :monoid or :assoc or :assoc-alt.

:domain-of-combine-uncond

The combination operator unconditionally returns values in the domain:
(domain combine<u,v>)
This corresponds to D*' in the tailrec design notes.
This applicability condition is present if and only if the :variant input of tailrec is :monoid-alt.

:combine-associativity

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 the tailrec design notes.
This applicability condition is present if and only if the :variant input of tailrec is :monoid or :assoc.

:combine-associativity-uncond

The combination operator is unconditionally associative:
(equal combine<u,combine<v,w>>
       combine<combine<u,v>,w>)
This corresponds to \mathit{ASC}' in the tailrec design notes.
This applicability condition is present if and only if the :variant input of tailrec is :monoid-alt or :assoc-alt.

:combine-left-identity

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 the tailrec design notes.
This applicability condition is present if and only if the :variant input of tailrec is :monoid or :monoid-alt.

:combine-right-identity

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 the tailrec design notes.
This applicability condition is present if and only if the :variant input of tailrec is :monoid or :monoid-alt.

:domain-guard

The domain is well-defined (according to its guard) on every value:
domain-guard<z>
where domain-guard<z> is the guard term of domain if domain is a function name, while it is the guard obligation of domain if domain is a lambda expression.
This corresponds to \mathit{GD} in the tailrec 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 of tailrec)..

:combine-guard

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 of combine<q,r>.
This corresponds to G* in the tailrec 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 of tailrec)..

:domain-of-base-when-guard

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 of old.
This corresponds to \mathit{GDb} in the tailrec 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 of tailrec) and the :variant input of tailrec is :assoc-alt.

:domain-of-nonrec-when-guard

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 of old.
This corresponds to \mathit{GDc} in the tailrec 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 of tailrec) and the :variant input of tailrec is :monoid-alt or :assoc-alt.

When present, :combine-left-identity and :combine-right-identity, together with either :combine-associativity or :combine-associativity-uncond (one of them is always present), and together with either :domain-of-combine or :domain-of-combine-uncond (one of them is always present), mean that the domain has the algebraic structure of a monoid, with the combination operator as the binary operator and with the base value of the recursion as identity. When :combine-left-identity and :combine-right-identity are absent, the domain has the algebraic structure of a semigroup.

Generated Events

new

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 as old.
The guard is (and old-guard<x1,...,xn> (domain a)), where old-guard<x1,...,xn> is the guard term of old.
In the tailrec design notes, new is denoted by f'.

wrapper

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 is t.
In the tailrec design notes, wrapper is denoted by \tilde{f}.

old-to-new

Theorem that rewrites old in terms of new:

;; 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 by f\!f'.

new-to-old

Theorem that rewrites new in terms of old:

;; 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 by f'\!f.

old-to-wrapper

Theorem that rewrites old in terms of wrapper:
(defthm old-to-wrapper
  (equal (old x1 ... xn)
         (wrapper x1 ... xn)))
This is generated only if the :wrapper input is t.
In the tailrec design notes, old-to-wrapper is denoted by f\!\tilde{f}.

wrapper-to-old

Theorem that rewrites wrapper in terms of old:
(defthm wrapper-to-old
  (equal (wrapper x1 ... xn)
         (old x1 ... xn)))
This is generated only if the :wrapper input is t.
In the tailrec design notes, old-to-wrapper is denoted by \tilde{f}\!f.

A theory invariant is also generated to prevent old-to-new and new-to-old from being enabled at the same time.

A theory invariant is also generated to prevent old-to-wrapper and wrapper-to-old from being enabled at the same time.

Redundancy

A call of tailrec is redundant if and only if it is identical to a previous successful call of tailrec whose :show-only input is not t, except that the two calls may differ in their :print and :show-only inputs. These inputs do not affect the generated events, and thus they are ignored for the purpose of redundancy.

A call of tailrec whose :show-only input is t does not generate any event. Thus, no successive call may be redundant with such a call.

Subtopics

Tailrec-implementation: Implementation of tailrec.