Robert S. Boyer

J Strother Moore

August, 2017

These criticisms are somewhat mitigated by three observations.

- PLTP was always just a
research tool for us and never really intended to be used by others. We were
exploring the automation of induction and the almost-exclusive use of
rewriting as a theorem proving paradigm.
- The 14 September, 1973, version of the code was just a snapshot of an
ever-changing system. Some of the problems discussed here were subsequently fixed by
us, as can be seen by looking at, say, the source files from November, 1973
Listing-B,
Listing-C,
Listing-D, and
Listing-E.
- The POP-2/ICL 4130 system we were using was extraordinarily cramped and slow by today's standards and so it was necessary to take some short-cuts just to get PLTP to run.

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,
`CAR`

, `CDR`

, `CONS`

, `EQUAL`

,
and `COND`

, and there was one
constant, `NIL`

.

`T`

abbreviated ```
(CONS NIL
NIL)
```

.
`0`

abbreviated `NIL`

, `1`

abbreviated `(CONS NIL 0)`

,
`2`

abbreviated `(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
`T`

, `1`

, `(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 `(CDR 3)`

to `2`

,
by replacing `(CDR `*y*)

by `EVAL`

will evaluate `(CDR 0)`

to `-1`

,
which is not actually a term. We should have considered the possibility that `0`

here and returned
`NIL`

since `0`

and `NIL`

represent the same term and we see, from the `Y=NIL`

case,
that `(CDR NIL)`

is `NIL`

.
An oddity (but not bug) in `EVAL`

is the code:

```
RETURN;
STEPCNT + 1 -> STEPCNT;
GOTO CONDRULES;
```

Since the `RETURN`

exits the function, the two lines after it are dead code.
`FUNCTION ISREALLINK`

(line 424)`ISREALLINK`

we
use `ISINTEGER`

to recognize numbers representing lists of `NIL`

s.
But everywhere else (nine times) we use the more
general `ISNUMBER`

to recognize such terms. Note: There are ten
occurrences of `ISNUMBER`

in the code, but the occurrence
in `GENSYM`

is 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
(`NIL`

here).

`FUNCTION ISNUMSKO`

(line 438) and All Its Callers`ISNUMSKO`

are 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 `I`

and `N`

. These are considered ``numeric'' variables. For example,
if the system is trying to prove `(`

then it might do an induction
suitable for natural numbers:
*p* N)`(AND (`

.
This would be ok if one thought of oneself as proving *p* 0) (IMPLIES (*p* N) (*p* (ADD1 N))))```
(IMPLIES (NUMBERP
N) (
```

which, indeed, we imagined.
*p* N))

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 `N`

.
Then `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 `NIL`

!

This contradiction would not be possible if one prohibited function
definitions from having numeric formal parameters like `N`

.
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
manifested itself.

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 `CONS`

as its
top-level function symbol, and `0`

(false) otherwise. But this
code treats all numbers as representing `CONS`

es.
But `0`

does not represent a `CONS`

.
`FUNCTION APPSUB1`

(line 480)`APPSUB`

is the function that that applies a substitution to a term and
`APPSUB1`

does 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
function `X`

and the variable `X`

. The base case is
formed by using `APPSUB`

to replace `X`

by `NIL`

in the conjecture to be proved, and the induction
conclusion is formed by replacing `X`

by `(CONS X1 X)`

.
But if the conjecture were `(X X)`

this would create the
nonsensical non-formula:

```
(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
actually *exploits* `APPSUB`

's ability to replace function
symbols. The `FUNCTION PICKINDVARS`

uses `APPSUB`

to
rename all occurrences of `CAR`

and `CDR`

to new
symbols to avoid confusing `CAR`

- and `CDR`

-terms in the
input formula with `CAR`

- and `CDR`

-terms introduced by
evaluation.

`FUNCTION TYPEEXP1`

(line 652)`TERM`

, and returns an expression in
the variable `X`

that recognizes the output of the term. For
example, if `TERM`

is `(CONS 1 V)`

the returned
expression is a term equivalent to `(AND X (EQUAL (CAR X) 1))`

.
When `TERM`

is the call of some function, `TYPEEXP1`

recursively
computes the type expression for the body of `TYPE`

,
and returns `(`*fn*TYPE X)

.
There are two problems.

The case `ELSEIF FUNSYM = "CONS"`

dealing with `TERM`

being
a `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
beginning with `CONS`

. Since `TYPEEXP1`

generates the
definition of a type function whose formal parameter is `X`

, this
bug could result in a type function whose definition contains free variables,
e.g., `A`

and `B`

in the example just given.

The second problem is that `TYPEEXP1`

does not check that the newly introduced
*fn*`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)`GENSYM`

is 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 (`TOPWORD`

) symbol
`X`

to `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 `2`

, etc.
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
by `GENSYM`

. If the user submitted a conjecture containing the
variable symbol `X1`

and `GENSYM`

is called with root
symbol `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.

`RIDCARCDR`

(line 1864)`CAR`

and `CDR`

mentioned in the
above discussion of `APPSUB1`

is done by applying the
substitution `RIDCARCDR`

whose value is set by this assignment:
```
CONSPAIR("CAR","CARARG")::(CONSPAIR("CDR","CDRARG")::NIL)
-> RIDCARCDR;
```

So `CARARG`

and `CDRARG`

are 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: `CARARG`

and `CDRARG`

are 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.