Online Otter-λ

Implicit and Explicit Typing

The no-nilpotents example

Let us begin the discussion of typing with an example. Consider the problem of proving that there are no nilpotent elements in an integral domain. To explain the problem: an integral domain is a ring R in which xy=0 implies x=0 or y=0, i.e. there are no zero divisors. A element c of R is called nilpotent if for some positive integer n, c raised to the n-th power (i.e., c multiplied by itself n times) is zero. Informally, one proves by induction on n that c to the n-th power, which we write pow(n,c), is not zero. The equation defining pow is pow(s(n),x) = x*pow(n,x). If c and pow(n,c) are both nonzero, then the integral domain axiom implies that pow(n+1,c) is also nonzero. It's a very simple proof, but it's interesting because it involves two types of objects, ring elements and natural numbers, and the proof involves a mix of the algebraic axioms and the number-theoretical axioms (mathematical induction). Since the proof is so simple, we can consider the issues raised by having two types of objects without being distracted by a complicated proof.

How are we to formalize this theorem in first order logic? The traditional way would be to have two unary predicates R(x) and N(x), whose meaning would be "x is a member of the ring R" and "x is a natural number", respectively. Then the ring axioms would be "relativized to R", which means that instead of saying x+0=0, we would say R(x) implies x+0 =0, or in clausal form, -R(x) | x+0 = 0. (The vertical bar means "or", and the minus sign means "not".) Similarly, the axiom of induction would be relativized to N. The axiom of induction is usually formulated using a symbol s for the successor function, or "next-integer" function. For example, s(4)= 5. The correct way to express the induction axiom in clausal form is explained here. In our case, the specific instance of induction we need for this proof can be expressed by the two (unrelativized) clauses

pow(o,x)!=0 | pow(g(x,n),x) = 0 | pow(n,x)=0.
pow(o,x)!=0 | pow(s(g(x,n)),x) != 0 | pow(n,x)=0.

To see that this corresonds to induction, think of g(x,n) as a constant (which x and n are not allowed to depend on). Then the middle literal of the first clause is pow(c,x) = 0. That's the induction hypothesis. The middle literal of the second clause is pow(s(c),x) != 0. That's the negated conclusion of the induction step. We've used 'o' instead of 0 for the natural number zero, which might not be the same as the ring element 0.

A traditional course in logic would teach you that to formalize this problem, you need to relativize all the axioms using R and N. Just to be explicit, the relativized versions of the induction axioms would be

-R(x) | -N(n) | pow(o,x)!=0 | pow(g(x,n),x) = 0 | pow(n,x)=0.
-R(x) | -N(n) | pow(o,x)!=0 | pow(s(g(x,n)),x) != 0 | pow(n,x)=0. -R(x) | -N(n) | N(g(n,x)).

-R(x) | -N(n) | R(pow(n,x)). -R(x) | -R(y) | R(x+y). -R(x) | -R(y) | R(x*y). -R(x) | x+0 = 0.

and so on for the other ring axioms.

Implicit Typing

Now here is the question: when formalizing this problem, do we need to relativize the induction axioms and the ring axioms using R(x) and N(x), or not? Experimentally, if we put the unrelativized axioms into Otter (Otter-λ is not needed, since we have explicitly given the prover the required instance of induction), we do find a proof. What does this proof actually prove? Certainly it shows that in any integral domain whose underlying set is the natural numbers, there are no nilpotents. And we can prove informally that any countable integral domain is isomorphic to one whose underlying set is the natural numbers. But this is not the theorem that we set out to prove, so it may appear that we must use R(x), N(x), and relativization to formalize this problem.

That is, however, not so. The method of ``implicit typing'' shows that under certain circumstances we can dispense with unary predicates such as R and N. One assigns a type to each predicate, function symbol, and constant symbol, telling what the sort of each argument is, and the sort of the value (in case of a function; predicates have Boolean value). Specifically each argument position of each function or predicate symbol is assigned a sort and the symbol is also assigned a `"value type" or "return type". For example, in this problem the ring operations + and * have the type of functions taking two R arguments and producing an R value, which we might express as

type(R,+(R,R)).

If we use N for the sort of natural numbers then we need to use a different symbol for addition on natural numbers, say type(N, plus(N,N)), and we need to use a different symbol for 0 in the ring and zero in N. The Skolem symbol g in the induction axiom has the type specification type(N,g(N,P)). The exponentiation function has the type specification

type(R,pow(N,R)).

Constants are considered as 0-ary function symbols, so they get assigned types, for example type(R,0) and type(N,o). We call a formula or term ``correctly typed'' if it is built up consistently with these type assignments. Note that variables are not typed; e.g. x + y is correctly typed no matter what variables x and y are. Types as we discuss them here are not quite the same as types in most programming languages, where variables are declared to have a certain type. Here, when a variable occurs in a formula, it inherits a type from the term in which it occurs, and if it occurs again in the same clause, it must have the same type at the other occcurence for the clause to be considered correctly typed. Once all the function symbols, constants, and predicate symbols have been assigned types, one can check (manually) whether the clauses supplied in an input file are correctly typed.

Then one observes that if the rules of inference preserve the typing, and if the axioms are correctly typed, and the prover finds a proof, then every step of the proof can be correctly typed. That means that it could be converted into a proof that used unary predicates for the sorts. Hence, if it assists the proof-finding process to omit these unary predicates, it is all right to do so. This technique was introduced long ago in [1], but McCune says it was already folklore at that time. It implies that the proof Otter finds using an input file without relativization actually is a valid proof of the theorem, rather than just of the special case where the ring elements are the natural numbers.

"Implicit typing" is the name of this technique, in which unary predicates whose function would be to establish typing are omitted. There are two ways to use implicit typing. First, we could just omit the unary predicates, let Otter (or Otter-λ) find a proof, and afterwards verify by hand (or by a computer program) that the proof is indeed well-typed. Second, we could verify that the axioms are well-typed, and prove that the inference rules used in the prover lead from correctly typed clauses to correctly typed clauses.

Let us explore this second alternative. Consider the inference rule of (binary) resolution.

Theorem. Suppose all function symbols and constants are assigned type specifications in such a way that all the axioms in a theory T are correctly typed. Then conclusions reached from T by binary resolution (using first-order unification) are also correctly typed.

Proof. Suppose that literal P(r) resolves with literal -P(t), where r and t are terms; then there is a substitution σ such that rσ = tσ, the unifying substitution. Here P stands for any atomic formula and t and r might stand for several terms if P has more than one argument position. Since P(r) and P(t) are correctly typed by hypothesis, r and t must have the same value type (if they are not variables). The result of the resolution will be a disjunction of literals Qσ | Sσ where Q and S are the remaining (unresolved) literals in the clauses that originally contained P(r) and -P(t), respectively. Now Q and S are correctly typed by hypothesis, so we just need to show that applying the substitution σ to a correctly typed term or literal will produce a correctly typed term or literal. This will be true by induction on the complexity of terms, provided that substitution σ assigns to each variable x in its domain, a term $q$ whose value type is the same as the value type of x in the clause in which x occurs. In first-order unification (but not in lambda-unification) variables get assigned a value in unification only when the variable occurs as an argument, either of a parent term or a parent literal. That is, a variable cannot occur in the position of a literal. Thus when we are unifying f(x,u) and f(q,v), x will get assigned to q, and the type of x and the value type of q must be the same since they are both in the first argument place of f. But have we ensured this in the no-nilpotents example? We have to be careful about the type specification of the equality symbol. If we specify type(bool, =(R,R)), then we cannot use the same equality symbol in the axioms for the natural numbers, for example s(x) != 0 and x=y|s(x)!=s(y). However, Otter treats any symbol beginning with EQ as an equality; = is a synonym for EQ, but one can also use, for example EQ2. Therefore, if we want to apply the theorem, we need to use two different equality symbols. Of course, we could just use = throughout and verify afterwards that the proof can be correctly typed, as = is never used in the same clause for equality between natural numbers and equality between ring elements. Otter has more inference rules than just binary resolution. Even in this example, the proof uses demodulation. The theorem above can be extended to included additional rules of inference:

Theorem. Suppose all function symbols and constants are assigned type specifications in such a way that all the axioms in a theory T are correctly typed. The type specifications of equality symbols must have the form type(bool, =(X,X)) for some type X. Then conclusions reached from T by binary resolution, hyperresolution, demodulation, and paramodulation (using first-order unification in applying these rules) are also correctly typed, provided demodulation and paramodulation are not applied to or from variables.

Remark. The theorem cannot be extended to apply to paramodulation from variables. An example is given below.

Proof. Conclusions reached by hyperresolution can also be reached by binary resolution, so that part of the theorem follows from the previous theorem. The results on paramodulation and demodulation follow from the fact that applying a substitution produced by unification preserves correct typings. The lemma that we need is that if p and r unify, then they have the same value type. If neither is a variable, this follows from the assumption that the axioms of T are correctly typed. (If one is a variable, this need not be the case.)

Suppose, for example, that r = s is to be used as a demodulator on term t. The demodulator is applied by unifying r with a certain subterm p of t. Let σ be the substitution that performs this unification, so pσ = rσ. Then p and r, since they unify, have the same value type, and hence p, pσ and rσ all have the same value type. The type specification of equality must have the form type(bool,=(X,X)) for some type X; so r and s have the same value type, so rσ and sσ have the same value type. Hence sσ and pσ also have the same value type, and hence the result of replacing p in t by sσ (the result of the demodulation) is a correctly typed term.

Example. This example will show that one cannot allow "overloading", or multiple type specifications for the same symbol, and still use implicit typing with guaranteed correctness. For example, suppose we want to use x+y both for natural numbers and for integers. Thinking of integers, we write the axiom

x + (-x) = 0.

and thinking of natural numbers we write

s(0) + x != 0.

where s(y) is the successor of y. Now resolving these two unit clauses, we find a contradiction upon taking x = s(0).

Example. This example, taken from Euclidean geometry, shows that the theorem cannot be extended to paramodulation from variables. In this example, EQpt stands for equality between points, EQline stands for equality between lines, I(a,b) stands for point a incident to line b, and p1(u) and p2(u) are two distinct points on line u. The types here are boolean, point, and line. Axioms (1) and (2) are correctly typed:

(1) EQpt(x,y) | I(x, line(x,y)).
(2) EQline(line(p1(u), p2(u)), u).

Paramodulating from the first clause of (1) into (2), we unify x with line(p1(u),p2(u)), and thus derive the incorrectly typed conclusion
(3) EQline(y,x) | I(x, line(x,y)).

Explicit Typing

The (proof of the) theorem above does not apply if lambda-unification is used instead of first order unification.

Otter-λ offers the user the possibility of explicitly listing the type specifications, in the form illustrated above. For example, one can put into the input file

list(types).
type(R,pow(N,R)).
type(R,0).
type(N,o).
type(N,s(N)).
type(R,+(R,R)).
end_of_list.

[1] Wick, C., and McCune, W., Automated reasoning about elementary point-set topology, J. Automated Reasoning 5(2) 239-255, 1989.