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
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)
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 nth/update-nth, assoc/acons, or
g/s. If the data structure in question doesn't have such a single
accessor/updater, it is easy (though perhaps tedious) to define them.
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 access-3rd of those two stobjs is equal:
(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 old is
free, which would greatly limit is usefulness. We use a bind-free
hypothesis to strategically bind old to a good candidate; see below.
The following theorem states that for any element other than number 4,
update-4th of an object preserves that element:
(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 k elements of
field 2 of two objects are equal, the non-primitive accessor sum-range-of-field2 of the two
objects is preserved:
(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 clear-field2-from only
affects elements k and above of field 2:
(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 range-equal and the
bind-free strategy below, these two rules are sufficient to prove:
(implies (<= (nfix j) (nfix k))
(equal (sum-range-of-field2 j (clear-field2-from k x))
(sum-range-of-field2 j x)))
Free Variable Binding Strategy
Accessor theorems of the form above contain a free variable old. Our
approaches use two strategies to bind this variable:
- When trying to prove another such accessor rule, we bind old to
old whenever new is bound to new (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 the prev-stobj-binding utility to bind old to
one of the actuals of that function call, depending on the formals and
stobjs-out of the function in question. For example, suppose foo takes
formals (x val st$) and has stobjs-out (nil st$). That is,
it (perhaps) modifies st$ and returns it as its second value. Then if
new is bound to (mv-nth 1 (foo k q bar)), we will find (nth 1
stobjs-out) = st$, find that st$ is the 3rd formal, and thus bind the
third actual, bar, to old.
- Check that a range of entries from two lists are equal.
- Prove an updater independence theorem, as discussed in stobj-updater-independence.