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:
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