		Search-engine friendly clone of the ACL2 documentation.

Std/stobjs

Stobj-updater-independence

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.

Proposed Approach

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.

Example 1

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

Example 2

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.

Subtopics

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.