		Search-engine friendly clone of the ACL2 documentation.

Kestrel-utilities

Sublis-expr+

Replace terms by variables, even inside lambda bodies

WARNING: This utility takes an alist that maps terms to variables. In that sense it is more restrictive than the corresponding utility that is built into ACL2, sublis-expr. This restriction to variables could probably be lifted with a little effort (but was acceptable for its initial purpose).

General Form:
(sublis-expr+ alist term)

where alist is an alist that maps terms to variables and term is a (translated) term. The value is a term that results from replacing occurrences of terms in the domain of alist by the corresponding variables. Notably, this replacement can take place in bodies of lambdas, with attention to avoiding so-called variable capture (as discused further below).

Consider the following example, which for readability is expressed in terms of untranslated terms.

alist:
(((nth '0 (binary-append a b)) . x)
 ((nth '1 (binary-append a b)) . y))

term (untranslated):
(let ((u (cons (nth 0 (append a b))
               (nth 1 (append a b)))))
  (cons (nth 0 (append a b)) u))

result (untranslated):
(let ((u (cons x y)))
  (cons x u))

Note that substitution occurred even inside the body of the input let expression, which corresponds to the body of the input lambda expression below. Here is an actual call, with translated terms, that corresponds to the description above.

ACL2 !>(sublis-expr+ '(((nth '0 (binary-append a b)) . x)
                       ((nth '1 (binary-append a b)) . y))
                     '((lambda (u b a)
                         (cons (nth '0 (binary-append a b)) u))
                       (cons (nth '0 (binary-append a b))
                             (nth '1 (binary-append a b)))
                       b a))
((LAMBDA (U B A) (CONS X U))
 (CONS X Y)
 B A)
ACL2 !>

Remark. Notice that a simpler term that is equivalent to the one above is as follows.

((LAMBDA (U) (CONS X U))
 (CONS X Y))

Indeed, they both untranslate to: (let ((u (cons x y))) (cons x u)). An enhancement to consider would be to drop formals that are bound to themselves, like A and B in the example above. End of Remark.

Finally, we note that variable capture is avoided, as illustrated by the following example. Consider the (untranslated) input (let ((u (cons x y))) (cons x u)), and suppose that we try to replace x with a ``global'' value of u. Then it would be an error to replace x by u in the body of the let, (cons x u), because the new occurrence of u would reference (be ``captured by'') the bound variable u, not the ``global'' value of u. Let's see what actually happens.

ACL2 !>(sublis-expr+ '((x . u))
                      '((lambda (u x) (cons x u)) (cons x y) x))
((LAMBDA (U X) (CONS X U)) (CONS U Y) U)
ACL2 !>(untranslate ; input
        '((lambda (u x) (cons x u)) (cons x y) x)
        nil (w state))
(LET ((U (CONS X Y))) (CONS X U))
ACL2 !>(untranslate ; result
        '((LAMBDA (U X) (CONS X U)) (CONS U Y) U)
        nil (w state))
(LET ((U (CONS U Y)) (X U)) (CONS X U))
ACL2 !>

It would also be an error to replace u by x in that same body of the let, (cons x u), because that new occurrence of u would reference the bound variable u, not the ``global'' value of u. The input term is returned unchanged in this case.

ACL2 !>(sublis-expr+ '((u . x))
                     '((lambda (u x) (cons x u)) (cons x y) x))
((LAMBDA (U X) (CONS X U)) (CONS X Y) X)
ACL2 !>(untranslate ; new result
        '((LAMBDA (U X) (CONS X U)) (CONS X Y) X)
        nil (w state))
(LET ((U (CONS X Y))) (CONS X U))
ACL2 !>

It would also have been correct to rename the bound variable, to produce the result ((LAMBDA (U1 X) (CONS X U1)) (CONS X Y) X), which untranslates to (let ((u1 (cons x y))) (cons x u1)). Perhaps a future enhancement of this utility will do such renaming.