Generalization is Semantical

Claus-Peter Wirth FR Informatik, Saarland Univ.

                                 chris@ags.uni-sb.de

SEKI-Working-Paper SWP–2005–02

SEKI-Working-Paper ISSN 1860-5931 ^{UNIVERSITÄT DES SAARLANDES FACHRICHTUNG INFORMATIK D–66123 SAARBRÜCKEN GERMANY WWW: http://www.ags.uni-sb.de/}

This SEKI-Working-Paper was internally reviewed by: Erica Melis FR Informatik, Universität des Saarlandes, D–66123 Saarbrücken, Germany

E-mail: melis@activemath.org
WWW: http://www.activemath.org/~melis/

Editor of SEKI series: Claus-Peter Wirth FR Informatik, Universität des Saarlandes, D–66123 Saarbrücken, Germany

E-mail: cp@ags.uni-sb.de
WWW: http://www.ags.uni-sb.de/~cp/welcome.html

Generalization is Semantical

Claus-Peter Wirth FR Informatik, Saarland Univ.

                     chris@ags.uni-sb.de

April 14, 2005

Abstract

We want to list some examples that show that it is hopeless to achieve generalization of inductive theorems by syntactical means.

1 Specification Too Poor

The following example is from Kühler (2000), p.11.

Suppose we have the definitions

(double1) double(0)=0
(double2) double(s(x^{δ} ))=s(s(double(x^{δ} )))

and want to prove the clause

(double-irrefl) double(x^{δ} )≠x^{δ} , x^{δ} =0

This cannot be proved without the introduction of additional functions such as

(less1) less(0, s(y^{δ} ))=true
(less2) less(x^{δ} , 0)=false
(less3) less(s(x^{δ} ), s(y^{δ} ))=less(x^{δ} , y^{δ} )

to formulate lemmas such as

(less-s)  less(x^{δ} , s(x^{δ} ))=true
(less-trans) less(x^{δ} , z^{δ} )=true, less(x^{δ} , y^{δ} )≠true, less(y^{δ} , z^{δ} )≠true
(less-double) less(x^{δ} , double(x^{δ} ))=true, x^{δ} =0
(less-≠)  less(x^{δ} , y^{δ} )=false, x^{δ} ≠y^{δ}

Now (less-s) and (less-trans) are trivial by induction and prove (less-double) by induction, and this together with the inductively trivial (less-≠) deductively implies (double-irrefl).

It seems obvious that the generation of all these symbols, definitions, and lemmas cannot be reasonably hoped to be achieved by syntactic manipulations in any framework.

2 Properly Generalizing does Not Find a Proof

The example of this section is a rational reconstruction and elaboration of Section 5.2 of Busch (1993) within the superior formalism of Wirth (2004). We do not agree with the conclusion of Section 5.2 of Busch (1993):

“Although another induction proof has to be performed, the complexity of the induction compared to the original goal is reduced.”

To the contrary, we do not see a reduction in complexity because a direct induction proof of the open goals is still not possible. We see this as an example, where generalization helps to find a theorem but not a proof of it.

Suppose we have the definitions

(append1) append(nil, l2^{δ})=l2^{δ}
(append2) append(cons(x1^{δ} , l1^{δ}), l2^{δ})=cons(x1^{δ} , append(l1^{δ} , l2^{δ}))
(revtail1) revtail(nil, l2^{δ})=l2^{δ}
(revtail2) revtail(cons(x1^{δ} , l1^{δ}), l2^{δ})=revtail(l1^{δ} , cons(x1^{δ} , l2^{δ}))

and want to prove

(revtail-append1) revtail(append(l1^{δ} , l2^{δ}), nil)=append(revtail(l2^{δ} , nil), revtail(l1^{δ} , nil))

Although this is inductively valid, a simple proof fails because the induction hypothesis is too weak. Both straightforward generalizations

(revtail-append2) revtail(append(l1^{δ} , l2^{δ}), l3^{δ})=append(revtail(l2^{δ} , l3^{δ}), revtail(l1^{δ} , l3^{δ}))
(revtail-append3) revtail(append(l1^{δ} , l2^{δ}), l3^{δ})=append(revtail(l2^{δ} , l4^{δ}), revtail(l1^{δ} , l5^{δ}))

can easily be refuted, however. To generalize avoiding over-generalization, we should try to prove

(revtail-append4) revtail(append(l1^{δ} , l2^{δ}), l3^{γ}(l1^{δ} , l2^{δ} , l3^{δ} , l4^{δ} , l5^{δ}))=
append(revtail(l2^{δ} , l4^{γ}(l1^{δ} , l2^{δ} , l3^{δ} , l4^{δ} , l5^{δ})), revtail(l1^{δ} , l5^{γ}(l1^{δ} , l2^{δ} , l3^{δ} , l4^{δ} , l5^{δ})))

with variable-condition {l3^{γ}, l4^{γ}, l5^{γ}} × {l1^{δ} , l2^{δ} , l3^{δ} , l4^{δ} , l5^{δ} }. As induction over l1^{δ} is unflawed, let us start it. The case {l1^{δ} ↦ cons(x1^{δ} , l6^{δ})} adds {l1^{δ} } × {x1^{δ} , l6^{δ} } to our variable-condition and reduces to

(revtail-append4.2) revtail(append(l6^{δ} , l2^{δ}), cons(x1^{δ} , l3^{γ}(cons(x1^{δ} , l6^{δ}), l2^{δ} , l3^{δ} , l4^{δ} , l5^{δ})))=
append (\begin{matrix}revtail(l2^{δ} , l4^{γ}(cons(x1^{δ} , l6^{δ}), l2^{δ} , l3^{δ} , l4^{δ} , l5^{δ})) & , \\ revtail & ( & l6^{δ} & , & cons(x1^{δ} , l5^{γ}(cons(x1^{δ} , l6^{δ}), l2^{δ} , l3^{δ} , l4^{δ} , l5^{δ})) & ) \end{matrix})

Unifying the left hand side of this with the left-hand side of the induction hypothesis (revtail-append4) under the substitution {l1^{δ} ↦l6^{δ} } would require

cons(x1^{δ} , l3^{γ}(cons(x1^{δ} , l6^{δ}), l2^{δ} , l3^{δ} , l4^{δ} , l5^{δ}))=l3^{γ}(l6^{δ} , l2^{δ} , l3^{δ} , l4^{δ} , l5^{δ}),

which is hopeless. But with a substitution that replaces all unmatched free δ^{−}-variables with free γ-variables, say {l1^{δ} ↦l6^{δ} , l3^{δ} ↦l3′^{γ}, l4^{δ} ↦l4′^{γ}, l5^{δ} ↦l5′^{γ}}, this requirement becomes

cons(x1^{δ} , l3^{γ}(cons(x1^{δ} , l6^{δ}), l2^{δ} , l3^{δ} , l4^{δ} , l5^{δ}))=l3^{γ}(l6^{δ} , l2^{δ} , l3′^{γ}, l4′^{γ}, l5′^{γ}),

which, after substitution {l3^{γ} ↦ λl_{1}, l_{2}, l_{3}, l_{4}, l_{5}. l_{3}} and λβ-reduction, reads

cons(x1^{δ} , l3^{δ})=l3′^{γ},

which is solved by {l3′^{γ} ↦ cons(x1^{δ} , l3^{δ})}. After this the original clause reads

(revtail-append4) revtail(append(l1^{δ} , l2^{δ}), l3^{δ})=
append(revtail(l2^{δ} , l4^{γ}(l1^{δ} , l2^{δ} , l3^{δ} , l4^{δ} , l5^{δ})), revtail(l1^{δ} , l5^{γ}(l1^{δ} , l2^{δ} , l3^{δ} , l4^{δ} , l5^{δ})))

and the result of the induction hypothesis application is

(revtail-append4.2.1) append (\begin{matrix}revtail(l2^{δ} , l4^{γ}(l6^{δ} , l2^{δ} , cons(x1^{δ} , l3^{δ}), l4′^{γ}, l5′^{γ})) & , \\ revtail & ( & l6^{δ} & , & l5^{γ}(l6^{δ} , l2^{δ} , cons(x1^{δ} , l3^{δ}), l4′^{γ}, l5′^{γ}) & ) \end{matrix} )=
append (\begin{matrix}revtail(l2^{δ} , l4^{γ}(cons(x1^{δ} , l6^{δ}), l2^{δ} , l3^{δ} , l4^{δ} , l5^{δ})) & , \\ revtail & ( & l6^{δ} & , & cons(x1^{δ} , l5^{γ}(cons(x1^{δ} , l6^{δ}), l2^{δ} , l3^{δ} , l4^{δ} , l5^{δ})) & ) \end{matrix})

As there are many choices to close this goal by instantiation and λβ-reduction, let us have a look at the base case first. The case {l1^{δ} ↦ nil} reduces to

(revtail-append4.1) revtail(l2^{δ} , l3^{δ})=append(revtail(l2^{δ} , l4^{γ}(nil, l2^{δ} , l3^{δ} , l4^{δ} , l5^{δ})), l5^{γ}(nil, l2^{δ} , l3^{δ} , l4^{δ} , l5^{δ}))

Now induction on l2^{δ} is unflawed. The base case {l2^{δ} ↦ nil} reduces to

(revtail-append4.1.1) l3^{δ} =append(l4^{γ}(nil, nil, l3^{δ} , l4^{δ} , l5^{δ}), l5^{γ}(nil, nil, l3^{δ} , l4^{δ} , l5^{δ}))

Rewriting with (append1), this (unsafely) reduces to

(revtail-append4.1.1.1) l3^{δ} =l5^{γ}(nil, nil, l3^{δ} , l4^{δ} , l5^{δ})
(revtail-append4.1.1.2) l4^{γ}(nil, nil, l3^{δ} , l4^{δ} , l5^{δ})=nil

As the substitution {l5^{γ} ↦ λl_{1}, l_{2}, l_{3}, l_{4}, l_{5}. l3^{δ} } is blocked by our variable-condition, (revtail-append4.1.1.1) can only be closed by applying {l5^{γ} ↦ λl_{1}, l_{2}, l_{3}, l_{4}, l_{5}. l_{3}} and λβreduction. With this, (revtail-append4.2.1) can be (unsafely) reduced to

(revtail-append4.2.1.1) l4^{γ}(l6^{δ} , l2^{δ} , cons(x1^{δ} , l3^{δ}), l4′^{γ}, l5′^{γ})=l4^{γ}(cons(x1^{δ} , l6^{δ}), l2^{δ} , l3^{δ} , l4^{δ} , l5^{δ})

The case {l2^{δ} ↦ cons(x2^{δ} , l7^{δ})} of (revtail-append4.1) adds {l2^{δ} } × {x2^{δ} , l7^{δ} } to our variablecondition and reduces to

(revtail-append4.1.2) revtail(l7^{δ} , cons(x2^{δ} , l3^{δ}))=
append(revtail(l7^{δ} , cons(x2^{δ} , l4^{γ}(nil, cons(x2^{δ} , l2^{δ}), l3^{δ} , l4^{δ} , l5^{δ}))), l3^{δ})

The case {l7^{δ} ↦ nil} reduces to

(revtail-append4.1.2.1) cons(x2^{δ} , l3^{δ})=append(l4^{γ}(nil, cons(x2^{δ} , l2^{δ}), l3^{δ} , l4^{δ} , l5^{δ}), cons(x2^{δ} , l3^{δ}))

By (append1) this (unsafely) reduces to

(revtail-append4.1.2.1.1) l4^{γ}(nil, cons(x2^{δ} , l2^{δ}), l3^{δ} , l4^{δ} , l5^{δ})=nil

Now (revtail-append4.1.1.2) and (revtail-append4.1.2.1.1) can be solved by projection on the first component and the imitation of nil, i.e. {l4^{γ} ↦ λl_{1}, l_{2}, l_{3}, l_{4}, l_{5}. nil}. As only the latter closes (revtail-append4.2.1.1), we apply it globally. The top open goal then is

(revtail-append4.1) revtail(l2^{δ} , l3^{δ})=append(revtail(l2^{δ} , nil), l3^{δ})

But again there is no chance to prove this by an easy induction. Indeed, even with the additional lemma

(append-assoc) append(append(l1^{δ} , l2^{δ}), l3^{δ})=append(l1^{δ} , append(l2^{δ} , l3^{δ}))

Tobias Schmidt-Samoa was not able to prove (revtail-append4.1) with Nqthm, cf. Boyer & Moore (1988). The inductive theorem prover QuodLibet, cf. Avenhaus &al. (2003), which is stronger than the famous and excellent Nqthm in the generation of induction hypotheses, proves it automatically by induction on l2^{δ}. We have to apply (revtail-append4.1) as an induction hypothesis twice to

(revtail-append4.1.2) revtail(l7^{δ} , cons(x2^{δ} , l3^{δ}))=append(revtail(l7^{δ} , cons(x2^{δ} , nil)), l3^{δ})

namely once with {l2^{δ} ↦ l7^{δ} , l3^{δ} ↦ cons(x2^{δ} , l3^{δ})} and once with {l2^{δ} ↦ l7^{δ} , l3^{δ} ↦

cons(x2^{δ} , nil)}, both for rewriting. This results in

(revtail-append4.1.2.1) append(revtail(l7^{δ} , nil), cons(x2^{δ} , l3^{δ}))
=append(append(revtail(l7^{δ} , nil), cons(x2^{δ} , nil)), l3^{δ})

the right-hand side of which can be rewritten to the left-hand side by application of (append-assoc), (append1), and (append1).

All in all, although we have been able to synthesize a sound conjecture, namely

(revtail-append4) revtail(append(l1^{δ} , l2^{δ}), l3^{δ})=append(revtail(l2^{δ} , nil), revtail(l1^{δ} , l3^{δ}))

we did not know how to prove it. Although QuodLibet was finally able to prove (revtail-append4.1) with some additional lemma, neither I nor Nqthm were able to do it. In our opinion, this demonstrates that generalization by syntactic means is poor. Now what does a human expert do? First he sees

(revtail-append5) revtail(append(l1^{δ} , l2^{δ}), l3^{δ})=revtail(l2^{δ} , revtail(l1^{δ} , l3^{δ}))
(revtail-append6) revtail(l1^{δ} , append(l2^{δ} , l3^{δ}))=append(revtail(l1^{δ} , l2^{δ}), l3^{δ})

which are trivial by induction on l1^{δ} and (together with (append1)) prove (revtail-append4) and—a fortiori—(revtail-append1) by deductive rewriting, where (revtail-append6) has to be applied from right to left.

Note that the proof of (revtail-append5) (whose left-hand side is identical to the one of (revtail-append4)) is what let us instantiate l3^{γ} in the above proof attempt due to the erroneous assumption that (revtail-append4) should be proved by induction on l1^{δ}.

References

Jürgen Avenhaus, Ulrich Kühler, Tobias Schmidt-Samoa, Claus-Peter Wirth (2003). How to Prove Inductive Theorems? QuodLibet!. 19^{th} CADE 2003, LNAI 2741, pp. 328–333, Springer.

Robert S. Boyer, J S. Moore (1988). A Computational Logic Handbook. Academic Press.

Holger Busch (1993). Unification-Based Induction. In: Claesen & Gordon (1993), pp. 97– 116.

Luc J. M. Claesen, Michaël J. C. Gordon (eds.) (1993). Higher Order Logic Theorem Proving and its Applications. North-Holland (Elsevier).

Ulrich Kühler (2000). A Tactic-Based Inductive Theorem Prover for Data Types with Partial Operations. Ph.D. thesis, Infix, Sankt Augustin.

Claus-Peter Wirth (2004). Descente Infinie + Deduction. Logic J. of the IGPL 12,

   pp. 1–96, Oxford Univ. Press. http://www.ags.uni-sb.de/˜ cp/p/d/welcome.html
   (Sept.12,2003).