Regarding your query about "undefined terms":
>> I'd like to hear
>> what is done in actual systems.
Here is a brief account of what is done in Nqthm (sometimes called the
"Boyer-Moore" prover) and in ACL2 (its successor).
In both Nqthm and ACL2, we take Harrison's approach [1]: ``Resolutely give
each partial function a convenient value on points outside its domain.'' Users
have found this approach to be really helpful in cutting down on the number of
cases and the number of lemmas required, and only rarely has there seemed to be
an issue about *which* convenient value to take, in the sense that Trybulec
mentioned:
>> What is more important, quite often it is not clear which value is
>> convenient.
>> One can put
>> 0" = 0, to get (-x)" = -x", or
>> 0" = 1, to get x/y = 0 implies x = 0 or
>> 0" = +\infty (the most reasonable if system allows for infinite values).
At one point, however, we considered moving more towards Harrison's approach
[2] in ACL2: ``Give each partial function some arbitrary value outside its
domain.'' This turned out to greatly complicate the proof burdens on users.
In particular, one of our colleagues who uses ACL2 daily has commented that the
reversion of ACL2 to an Nqthm-like approach (i.e., [1]) has greatly helped him
in his work.
Below is a simple example that illustrates the potential advantage of [1]
(assignment of convenient values) over [2] (use of arbitrary, undefined values)
in our context. This example is sufficiently simple that one could reasonably
argue that other approaches would solve it more simply, for example Harrison's
[3], using types. However, our goal here is simply to illustrate advantages of
[1] over [2].
Consider the following problem. Define a function that sums a list of natural
numbers, and then prove the following theorem: the sum of the result of
appending two lists together is the same as adding the sums of each list. In
ACL2 (in fact, in Common Lisp) one can define the sum of a list of natural
numbers as follows. Note: informally speaking, the "(declare ... :guard ...)"
expression below specifies that only those x that are lists of natural numbers
are "in the domain" of the function SUMLIST.
[Here and subsequently, semicolons (;) indicate comments to the end-of-line.]
(defun sumlist (x)
(declare (xargs :guard (nat-listp x))) ; x "should" be a list of naturals
(if (endp x) ; same as (atom x), but probably more efficient
0
(+ (car x)
(sumlist (cdr x)))))
Now the theorem we want to prove may be stated as follows. Note that it has no
hypotheses, even though we might only "intend" it to hold in the case that x
and y are lists of natural numbers. However, ACL2 uses rewriting heavily, and
the elimination of hypotheses in rewrite rules such as the following is helpful
in subsequent proofs.
(defthm sumlist-append ; name of theorem
(equal (sumlist (append x y)) ; left side of rewrite rule
(+ (sumlist x) (sumlist y)))) ; right side of rewrite rule
ACL2 has no trouble proving this theorem automatically, without any apparent
consideration of cases arising from adding non-numbers (which by the way are
treated as 0 for that purpose, i.e., 0 is the conveniently chosen value for
points outside the "domain" of +). However, in a previous version of ACL2 we
used approach [2], and the proof required the following lemmas.
(defthm sumlist-rationalp
;; If x is a list of naturals, then its sum is a rational number.
(implies (nat-listp x)
(rationalp (sumlist x)))
:rule-classes :type-prescription)
(defthm nat-listp-implies-true-listp
;; If x is a list of naturals, then it is a null-terminated list.
(implies (nat-listp x)
(true-listp x))
:rule-classes :forward-chaining)
(defthm nat-listp-append
;; If x and y are lists of naturals, then their concatenation is too.
(implies (and (nat-listp x)
(nat-listp y))
(nat-listp (append x y)))
:rule-classes :type-prescription)
The discovery of these lemmas required, unfortunately, some expertise in using
the system. Note also the obscure "rule-classes". We'll spare you the details
(but can send individuals a more extensive write-up upon request.) Moreover,
the final theorem *requires* hypotheses:
(defthm sumlist-append
(implies (and (nat-listp x)
(nat-listp y))
(equal (sumlist (append x y))
(+ (sumlist x) (sumlist y)))))
This kind of complicatation was sufficiently common to cause us to make major
changes in the ACL2 logic and implementation, the result being a system that
bears considerably more resemblance to its predecessor, Nqthm, than had been
the case.
Matt Kaufmann
J Moore