Discussion of the accessor/updater independence or *frame problem*,
especially as it relates to the def-updater-independence-thm utility.

Note: This is related to what is known as the frame problem in philosophy/artificial intelligence/logic; for a broader discussion see this article.

When reasoning about structured data in ACL2, especially stobjs, one commonly needs to know that a given updater has no effect on a given accessor. During the development of any large program involving such a structured object, the number and complexity of accessor and updater functions tends to grow until the ad-hoc approach to the problem (proving each such theorem as it is needed) becomes unworkable.

In the ad hoc approach, a given data structure might require a number of theorems close to the product of the structure's accessor and updater count. For many programs this isn't so large that it is impossible to generate and prove all such theorems, but we propose a much more scalable approach here.

Broadly speaking, the approach requires the following two sorts of theorems:

The approach described here (and implemented by def-updater-independence-thm relies on indexed accesses and updates of the
structure. That is, there should be a single accessor and a single updater
function in terms of which all primitive accesses and updates can be logically
described, such as

The main idea is to prove two kinds of theorems that work together:

- For each accessor, a theorem stating sufficient conditions under which the accessor applied to two different structures produces equal results.
- For each updater, one or more theorems stating that the updater does not change certain fields or accessor applications.

The following theorem states that as long as element 3 of
two objects are equal, the

(implies (equal (nth 3 new) (nth 3 old)) (equal (access-3rd new) (access-3rd old)))

Note that if we interpret this as a rewrite rule, the variable

The following theorem states that for any element other than number 4,

(implies (not (equal (nfix n) 4)) (equal (nth n (update-4th val x)) (nth n x)))

These two rules can be used with the bind-free strategy below to prove:

(equal (access-3rd (update-4th val x)) (access-3rd x))

The following theorem states that as long as the first

(implies (range-equal 0 k (nth 2 new) (nth 2 old)) (equal (sum-range-of-field2 k new) (sum-range-of-field2 k old)))

The following theorem states that the non-primitive updater

(implies (< (nfix i) (nfix k)) (equal (nth i (nth 2 (clear-field2-from k x))) (nth i (nth 2 x))))

Given an appropriate reasoning strategy about

(implies (<= (nfix j) (nfix k)) (equal (sum-range-of-field2 j (clear-field2-from k x)) (sum-range-of-field2 j x)))

Accessor theorems of the form above contain a free variable

- When trying to prove another such accessor rule, we bind
old toold whenevernew is bound tonew (and do not apply the rule otherwise). This strategy is effective as long as all such accessor rules are phrased in terms of the same two variables. - In other contexts, we only apply the rule when
new is a function call. In that case, we use theprev-stobj-binding utility to bindold to one of the actuals of that function call, depending on the formals and stobjs-out of the function in question. For example, supposefoo takes formals(x val st$) and has stobjs-out(nil st$) . That is, it (perhaps) modifiesst$ and returns it as its second value. Then ifnew is bound to(mv-nth 1 (foo k q bar)) , we will find(nth 1 stobjs-out) = st$ , find thatst$ is the 3rd formal, and thus bind the third actual,bar , toold .

- Range-equal
- Check that a range of entries from two lists are equal.
- Def-updater-independence-thm
- Prove an updater independence theorem, as discussed in stobj-updater-independence.