CONSTRAINT

restrictions on certain functions introduced in encapsulate events 
Major Section:  MISCELLANEOUS

Suppose that a given theorem, thm, is to be functionally instantiated using a given functional substitution, alist, as described in :DOC lemma-instance. (For an example, see functional-instantiation-example.) What is the set of proof obligations generated? It is the set of all terms, tm, such that (a) tm mentions some function symbol in the domain of alist, and (b) either (i) tm arises from the ``constraint'' on a function symbol ancestral in thm or in some defaxiom or (ii) tm is the body of a defaxiom. Here, a function symbol is ``ancestral'' in thm if either it occurs in thm, or it occurs in the definition of some function symbol that occurs in thm, and so on.

The remainder of this note explains what we mean by ``constraint'' in the words above.

In a certain sense, function symbols are introduced in essentially two ways. The most common way is to use defun (or when there is mutual recursion, mutual-recursion or defuns). There is also a mechanism for introducing ``witness functions''; see defchoose. The documentation for these events describes the axioms they introduce, which we will call here their ``definitional axioms.'' These definitional axioms are generally the constraints on the function symbols that these axioms introduce.

However, when a function symbol is introduced in the scope of an encapsulate event, its constraints may differ from the definitional axioms introduced for it. For example, suppose that a function's definition is local to the encapsulate; that is, suppose the function is introduced in the signature of the encapsulate. Then its constraints include, at the least, those non-local theorems and definitions in the encapsulate that mention the function symbol.

Actually, it will follow from the discussion below that if the signature is empty for an encapsulate, then the constraint on each of its new function symbols is exactly the definitional axiom introduced for it. Intuitively, we view such encapsulates just as we view include-book events. But the general case, where the signature is not empty, is more complicated.

In the discussion that follows we describe in detail exactly which constraints are associated with which function symbols that are introduced in the scope of an encapsulate event. In order to simplify the exposition we make two cuts at it. In the first cut we present an over-simplified explanation that nevertheless captures the main ideas. In the second cut we complete our explanation by explaining how we view certain events as being ``lifted'' out of the encapsulate, resulting in a possibly smaller encapsulate, which becomes the target of the algorithm described in the first cut.

At the end of this note we present an example showing why a more naive approach is unsound.

Finally, before we start our ``first cut,'' we note that constrained functions always have guards of T. This makes sense when one considers that a constrained function's ``guard'' only appears in the context of a local defun, which is skipped. Note also that any information you want ``exported'' outside an encapsulate event must be there as an explicit definition or theorem. For example, even if a function foo has output type (mv t t) in its signature, the system will not know (true-listp (foo x)) merely on account of this information. Thus, if you are using functions like foo (constrained mv functions) in a context where you are verifying guards, then you should probably provide a :type-prescription rule for the constrained function, for example, the :type-prescription rule (true-listp (foo x)).

First cut at constraint-assigning algorithm. Quite simply, the formulas introduced in the scope of an encapsulate are conjoined, and each function symbol introduced by the encapsulate is assigned that conjunction as its constraint.

Clearly this is a rather severe algorithm. Let us consider two possible optimizations in an informal manner before presenting our second cut.

Consider the (rather artificial) event below. The function before1 does not refer at all, even indirectly, to the locally-introduced function sig-fn, so it is unfortunate to saddle it with constraints about sig-fn. 

(encapsulate
 (((sig-fn *) => *))


 (defun before1 (x)
   (if (consp x)
       (before1 (cdr x))
     x))


 (local (defun sig-fn (x) (cons x x)))


 (defthm sig-fn-prop
   (consp (sig-fn x)))
 )
We would like to imagine moving the definition of before1 to just in front of this encapsulate, as follows. 
(defun before1 (x)
  (if (consp x)
      (before1 (cdr x))
    x))


(encapsulate
 (((sig-fn *) => *))


 (local (defun sig-fn (x) (cons x x)))


 (defthm sig-fn-prop
   (consp (sig-fn x)))
 )
Thus, we will only assign the constraint (consp (sig-fn x)), from the theorem sig-fn-prop, to the function sig-fn, not to the function before1.

More generally, suppose an event in an encapsulate event does not mention any function symbol in the signature of the encapsulate, nor any function symbol that mentions any such function symbol, and so on. (We might say that no function symbol from the signature is an ``ancestor'' of any function symbol occurring in the event.) Then we imagine moving the event, so that it appears in front of the encapsulate. We don't actually move it, but we pretend we do when it comes time to assign constraints. Thus, such definitions only introduce definitional axioms as the constraints on the function symbols being defined, and such theorems introduce no constraints.

Once this first optimization is performed, we have in mind a set of ``constrained functions.'' These are the functions introduced in the encapsulate that would remain after moving some of them out, as indicated above. Consider the collection of all formulas introduced by the encapsulate, except the definitional axioms, that mention these constrained functions. So for example, in the event below, no such formula mentions the function symbol after1. 

(encapsulate
 (((sig-fn *) => *))


 (local (defun sig-fn (x) (cons x x)))


 (defthm sig-fn-prop
   (consp (sig-fn x)))


 (defun after1 (x)
   (sig-fn x))
 )
We can see that there is really no harm in imagining that we move the definition of after1 out of the encapsulate, to just after the encapsulate.

Many subtle aspects of this rearrangement process have been omitted. For example, suppose the function fn uses sig-fn, the latter being a function in the signature of the encapsulation. Suppose a formula about fn is proved in the encapsulation. Then from the discussion above fn is among the constrained functions of the encapsulate: it cannot be moved before the encapsulate and it cannot be moved after the encapsulation. But why is fn constrained? The reason is that the theorem proved about fn may impose or express constraints on sig-fn. That is, the theorem proved about fn may depend upon properties of the witness used for sig-fn. Here is a simple example: 

(encapsulate
 (((sig-fn *) => *))


 (local (defun sig-fn (x) (declare (ignore x)) 0))


 (defun fn (lst)
   (if (endp lst)
       t
       (and (integerp (sig-fn (car lst)))
            (fn (cdr lst)))))


 (defthm fn-always-true
   (fn lst)))
In this example, there are no explicit theorems about sig-fn, i.e., no theorems about it explicitly. One might therefore conclude that it is completely unconstrained. But the witness we chose for it always returns an integer. The function fn uses sig-fn and we prove that fn always returns true. Of course, the proof of this theorem depends upon the properties of the witness for sig-fn, even though those properties were not explicitly ``called out'' in theorems proved about sig-fn. It would be unsound to move fn after the encapsulate. It would also be unsound to constrain sig-fn to satisfy just fn-always-true without including in the constraint the relation between sig-fn and fn. Hence both sig-fn and fn are constrained by this encapsulation and the constraint imposed on each is the same and states the relation between the two as characterized by the equation defining fn as well as the property that fn always returns true. Suppose, later, one proved a theorem about sig-fn and wished to functional instantiate it. Then one must also functionally instantiate fn, even if it is not involved in the theorem, because it is only through fn that sig-fn inherits its constrained properties.

This is a pathological example that illustrate a trap into which one may easily fall: rather than identify the key properties of the constrained function the user has foreshadowed its intended application and constrained those notions. Clearly, the user wishing to introduce the sig-fn above would be well-advised to use the following instead: 

(encapsulate
 (((sig-fn *) => *))
 (local (defun sig-fn (x) (declare (ignore x)) 0))
 (defthm integerp-sig-fn
   (integerp (sig-fn x))))

(defun fn (lst)
  (if (endp lst)
      t
    (and (integerp (sig-fn (car lst)))
         (fn (cdr lst)))))

(defthm fn-always-true
   (fn lst)))
Note that sig-fn is constrained merely to be an integer. It is the only constrained function. Now fn is introduced after the encapsulation, as a simple function that uses sig-fn. We prove that fn always returns true, but this fact does not constrain sig-fn. Future uses of sig-fn do not have to consider fn at all.

Sometimes it is necessary to introduce a function such as fn within the encapsulate merely to state the key properties of the undefined function sig-fn. But that is unusual and the user should understand that both functions are being constrained.

Another subtle aspect of encapsulation that has been brushed over so far has to do with exactly how functions defined within the encapsulation use the signature functions. For example, above we say ``Consider the collection of all formulas introduced by the encapsulate, except the definitional axioms, that mention these constrained functions.'' We seem to suggest that a definitional axiom which mentions a constrained function can be moved out of the encapsulation and considered part of the ``post-encapsulation'' extension of the logic, if the defined function is not used in any non-definitional formula proved in the encapsulation. For example, in the encapsulation above that constrained sig-fn and introduced fn within the encapsulation, fn was constrained because we proved the formula fn-always-true within the encapsulation. Had we not proved fn-always-true within the encapsulation, fn could have been moved after the encapsulation. But this suggests an unsound rule because whether such a function can be moved after the encapsulate depend on whether its admission used properties of the witnesses! In particular, we say a function is ``subversive'' if any of its governing tests or the actuals in any recursive call involve a function in which the signature functions are ancestral.

Another aspect we have not discussed is what happens to nested encapsulations when each introduces constrained functions. We say an encapsulate event is ``trivial'' if it introduces no constrained functions, i.e., if its signatures is nil. Trivial encapsulations are just a way to wrap up a collection of events into a single event.

From the foregoing discussion we see we are interested in exactly how we can ``rearrange'' the events in a non-trivial encapsulation -- moving some ``before'' the encapsulation and others ``after'' the encapsulation. We are also interested in which functions introduced by the encapsulation are ``constrained'' and what the ``constraints'' on each are. We may summarize the observations above as follows, after which we conclude with a more elaborate example.

Second cut at constraint-assigning algorithm. First, we focus only on non-trivial encapsulations that neither contain nor are contained in non-trivial encapsulations. (Nested non-trivial encapsulations are not rearranged at all: do not put anything in such a nest unless you mean for it to become part of the constraints generated.) Second, in what follows we only consider the non-local events of such an encapsulate, assuming that they satisfy the restriction of using no locally defined function symbols other than the signature functions. Given such an encapsulate event, move, to just in front of it and in the same order, all definitions and theorems for which none of the signature functions is ancestral. Now collect up all formulas (theorems) introduced in the encapsulate other than definitional axioms. Add to this set any of those definitional equations that is either subversive or defines a function used in a formula in the set. The conjunction of the resulting set of formulas is called the ``constraint'' and the set of all the signature functions of the encapsulate together with all function symbols defined in the encapsulate and mentioned in the constraint is called the ``constrained functions.'' Assign the constraint to each of the constrained functions. Move, to just after the encapsulate, the definitions of all function symbols defined in the encapsulate that have been omitted from the constraint.

Implementation note. In the implementation we do not actually move events, but we create constraints that pretend that we did.

Here is an example illustrating our constraint-assigning algorithm. It builds on the preceding examples. 

(encapsulate
 (((sig-fn *) => *))


 (defun before1 (x)
   (if (consp x)
       (before1 (cdr x))
     x))


 (local (defun sig-fn (x) (cons x x)))


 (defthm sig-fn-prop
   (consp (sig-fn x)))


 (defun during (x)
   (if (consp x)
       x
     (cons (car (sig-fn x))
           17)))


 (defun before2 (x)
   (before1 x))


 (defthm before2-prop
   (atom (before2 x)))


 (defthm during-prop
   (implies (and (atom x)
                 (before2 x))
            (equal (car (during x))
                   (car (sig-fn x)))))


 (defun after1 (x)
   (sig-fn x))


 (defchoose after2 (x) (u)
   (and (< u x) (during x)))
 )
Only the functions sig-fn and during receive extra constraints. The functions before1 and before2 are viewed as moving in front of the encapsulate, as is the theorem before2-prop. The functions after1 and after2 are viewed as being moved past the encapsulate. Notice that the formula (consp (during x)) is a conjunct of the constraint. It comes from the :type-prescription rule deduced during the definition of the function during. The implementation reports the following. 
(SIG-FN X) is axiomatized to return one result.


In addition, we export AFTER2, AFTER1, DURING-PROP, BEFORE2-PROP, BEFORE2,
DURING, SIG-FN-PROP and BEFORE1.


The following constraint is associated with both of the functions DURING
and SIG-FN:


(AND (EQUAL (DURING X)
            (IF (CONSP X)
                X (CONS (CAR (SIG-FN X)) 17)))
     (CONSP (DURING X))
     (CONSP (SIG-FN X))
     (IMPLIES (AND (ATOM X) (BEFORE2 X))
              (EQUAL (CAR (DURING X))
                     (CAR (SIG-FN X)))))

We conclude by asking (and to a certain extent, answering) the following question: Isn't there an approach to assigning constraints that avoids over-constraining more simply than our ``second cut'' above? Perhaps it seems that given an encapsulate, we should simply assign to each locally defined function the theorems exported about that function. If we adopted that simple approach the events below would be admissible.

(encapsulate
 (((foo *) => *))
 (local (defun foo (x) x))
 (defun bar (x)
   (foo x))
 (defthm bar-prop
   (equal (bar x) x)
   :rule-classes nil))


(defthm foo-id
  (equal (foo x) x)
  :hints (("Goal" :use bar-prop)))


; The following event is not admissible in ACL2.


(defthm ouch!
  nil
  :rule-classes nil
  :hints
  (("Goal" :use
    ((:functional-instance foo-id
                           (foo (lambda (x) (cons x x))))))))
Under the simple approach we have in mind, bar is constrained to satisfy both its definition and bar-prop because bar mentions a function declared in the signature list of the encapsulation. In fact, bar is so-constrained in the ACL2 semantics of encapsulation and the first two events above (the encapsulate and the consequence that foo must be the identity function) are actually admissible. But under the simple approach to assigning constraints, foo is unconstrained because no theorem about it is exported. Under that approach, ouch! is proveable because foo can be instantiated in foo-id to a function other than the identity function.

It's tempting to think we can fix this by including definitions, not just theorems, in constraints. But consider the following slightly more elaborate example. The problem is that we need to include as a constraint on foo not only the definition of bar, which mentions foo explicitly, but also abc, which has foo as an ancestor. 

(encapsulate
 (((foo *) => *))
 (local (defun foo (x) x))
 (local (defthm foo-prop
          (equal (foo x) x)))
 (defun bar (x)
   (foo x))
 (defun abc (x)
   (bar x))
 (defthm abc-prop
   (equal (abc x) x)
   :rule-classes nil))


(defthm foo-id
  (equal (foo x) x)
  :hints (("Goal" :use abc-prop)))


; The following event is not admissible in ACL2.


(defthm ouch!
  nil
  :rule-classes nil
  :hints
  (("Goal" :use
    ((:functional-instance foo-id
                           (foo (lambda (x) (cons x x)))
                           (bar (lambda (x) (cons x x))))))))