These criticisms are somewhat mitigated by three observations.
Having said all that, we now critique the 14 September, 1973, version of PLTP. The definitive sources for that version of the code is provided in Listing-F and Listing-H. However, because those are hard-to-search OCR pdf files, we have transcribed the contents of those listings into a simple text file henceforth referred to as listings-f-and-h. We assume you can use your favorite text editor to search the listings and/or find the lines mentioned by number.
In PLTP's logical theory there were five primitives functions symbols,
COND, and there was one
(CONS NIL 0),
(CONS NIL 1), etc.
PLTP did not check the well-formedness of input terms and did not expand abbreviations away
before beginning the theorem proving process. Thus, for example, the code might encounter
(CONS NIL NIL),
(CONS 0 NIL), etc., all of which
are different concrete representations of the same logical term.
This convention of allowing multiple concrete representations of the same abstract term invites coding mistakes and several of the bugs below are due to this.
FUNCTION EVAL(line 128)
X = "CDR", where we say
THEN Y - 1;(line 170) we are trying to implement such transformations as the evaluation of
2, by replacing
(CDR y)by y-1 when y is a number. But we don't know that y is non-0. Thus, the definition of
-1, which is not actually a term. We should have considered the possibility that y is
0here and returned
NILrepresent the same term and we see, from the
An oddity (but not bug) in
EVAL is the code:
RETURN; STEPCNT + 1 -> STEPCNT; GOTO CONDRULES;
RETURNexits the function, the two lines after it are dead code.
FUNCTION ISREALLINK(line 424)
ISINTEGERto recognize numbers representing lists of
NILs. But everywhere else (nine times) we use the more general
ISNUMBERto recognize such terms. Note: There are ten occurrences of
ISNUMBERin the code, but the occurrence in
GENSYMis not concerned with a term.
It would have been nice to see the same idiom used throughout the code.
By the way, the name ``
ISREALLINK'' stems from the POP-2
convention of calling a cons-pair a link. In the parlance of ACL2,
this function is meant to recognize explicit values, variable-free
terms using only constructors (i.e.,
CONS here) and constants
FUNCTION ISNUMSKO(line 438) and All Its Callers
ISNUMSKOare suspect because they implement the assumption that ``numeric variables'' may only be instantiated with numerically valued terms, but the logical language is untyped.
ISNUMSKO recognizes POP-2 words beginning which a letter between
N. These are considered ``numeric'' variables. For example,
if the system is trying to prove
(p N) then it might do an induction
suitable for natural numbers:
(AND (p 0) (IMPLIES (p N) (p (ADD1 N)))).
This would be ok if one thought of oneself as proving
N) (p N)) which, indeed, we imagined.
However, because the language is untyped one can still imagine problems.
Suppose one defined the successor function,
(DEFINE (SUCC (N) (CONS NIL
N))) with the numeric formal parameter
SUCC would be considered always numerically valued and that
fact would be stored on the property list of
SUCC. It would
have been possible to then prove
(NUMBERP (SUCC (CONS T T)))
which is unfortunate since it evaluates to
This contradiction would not be possible if one prohibited function
definitions from having numeric formal parameters like
Indeed, no definition in the standard proveall or the JACM paper used numeric
formal parameters. Furthermore, PLTP never instantiated previously proved
theorems. So we believe that from a practical perspective, this bug never
But we consider the whole idea of numeric variables suspect without a proper type system!
FUNCTION ISCONS(line 446)
1(POP-2's true truthvalue) if the term is a
CONS, i.e., has
CONSas its top-level function symbol, and
0(false) otherwise. But this code treats all numbers as representing
0does not represent a
FUNCTION APPSUB1(line 480)
APPSUBis the function that that applies a substitution to a term and
APPSUB1does all the work. But this function does not just visit the subterms, it visits and possibly replaces the function symbols too.
This is not necessarily a problem and, indeed, problems can be avoided if (a) the set of symbols allowed as function symbols in the theory were disjoint from the set of symbols used as variables and (b) well-formedness were checked when new definitions and theorems are submitted. But PLTP does not make such checks.
Suppose the user defined a predicate named
X, and imagine that
some conjecture to be proved by induction involved both the
X and the variable
X. The base case is
formed by using
APPSUB to replace
NIL in the conjecture to be proved, and the induction
conclusion is formed by replacing
(CONS X1 X).
But if the conjecture were
(X X) this would create the
(AND (NIL NIL) (IMPLIES (X X) ((CONS X1 X) (CONS X1 X)))).
Fortunately, PLTP's provealls never introduced a function symbol whose name was ever used as a variable symbol. So this bug never manifested itself.
Furthermore, the induction mechanism
APPSUB's ability to replace function
FUNCTION PICKINDVARS uses
rename all occurrences of
CDR to new
symbols to avoid confusing
CDR-terms in the
input formula with
CDR-terms introduced by
FUNCTION TYPEEXP1(line 652)
TERM, and returns an expression in the variable
Xthat recognizes the output of the term. For example, if
(CONS 1 V)the returned expression is a term equivalent to
(AND X (EQUAL (CAR X) 1)). When
TERMis the call of some function, fn, for which no type function has been stored,
TYPEEXP1recursively computes the type expression for the body of fn, stores an appropriate type function with name fn
TYPE, and returns
There are two problems.
ELSEIF FUNSYM = "CONS" dealing with
CONS-expression is incorrect when it checks
NUMERIC(TERM) (line 665).
It should also check that
TERM is an explicit value, i.e.,
(ISREALLINK TERM). Otherwise,
TERM might be a term like
(CONS NIL (TIMES A B)) which is a numerically valued term
TYPEEXP1 generates the
definition of a type function whose formal parameter is
bug could result in a type function whose definition contains free variables,
B in the example just given.
The second problem is that
TYPEEXP1 does not check that the newly introduced
TYPE is a new function symbol. It will inadvertently
redefine that function (line 696) if the user has previously defined a function of that
name. An obvious correction is to enforce a pre-condition that no user
function name ends with
TYPE. None of the definitions in the
provealls violate this pre-condition.
FUNCTION GENSYM(line 779)
GENSYMis used to generate ``new'' variable symbols. It does so by taking an existing symbol (
TOPWORD) and tacking on an integer ``suffix,'' as when it transforms the root (
X1. For any given root symbol, the first suffix it uses in a given proof is
1, the next time in that proof it uses
The problem with this is that it assumes that the user did not included any
suffixed variables in the original conjecture. That is, the code is written
as though the only suffixed variables are those introduced
GENSYM. If the user submitted a conjecture containing the
GENSYM is called with root
X, it will generate
X1 but that would not be
a new variable.
No variable used in our provealls is suffixed. So this potential problem never manifested itself. The problem could be fixed by simply enforcing a pre-condition that no user-submitted term contained suffixed variables.
CDRmentioned in the above discussion of
APPSUB1is done by applying the substitution
RIDCARCDRwhose value is set by this assignment:
CONSPAIR("CAR","CARARG")::(CONSPAIR("CDR","CDRARG")::NIL) -> RIDCARCDR;
CDRARGare assumed to be function symbols of arity 1 that do not occur in any user formula. This is another implicit pre-condition that ought to be enforced:
CDRARGare never defined or used by user.
While no change was caused by this, the following is worth noting: in the EQUAL case of FUNCTION EVAL there is an odd sequence: because the RETURN rips control out. Thus, the last two statements above are dead code.