Induction is only valid for proving sentences about algebras that are definable with initial semantics. In our applications, the data algebra is usually defined this way, and so proofs by induction are valid for it. For example, the integers or naturals are often part of the data algebra, and lemmas about them are usually needed for all but the simplest proofs.

Initial specifications generally have more than one induction scheme; even the natural numbers have many different schemes. The most familiar one proves P(n) for all n by proving P(0) and then proving that P(n) implies P(s n). However, we could instead prove P(0) and P(s 0), and then prove that P(n) implies P(s s n). These two schemes correspond to different choices of generators: the first takes 0, s as generators, while the second takes 0, s0, ss. There are infinitely many such schemes.

A general definition of induction for (initial models of) a specification (,E) takes a little work: call a signature with equations G inductive for ( ,E) iff: (1) under the equations (E G) every ground ( )-term equals some -term; and (2) every ground -term equals some -term.

Now given an S-indexed family of predicates P on ground -terms, if (,G) is inductive for (,E), then we can prove P by the following induction scheme: show P(c) for each constant c in , and then show P(g(t1,...,tk)) for each g in , assuming P(ti) for each i and using (E G).

This gives the familiar induction schemes in the usual cases, noting that P is often defined to be true except on one particular sort.

To show soundness of this proof rule, we define an S-sorted set M of ground -terms by Ms= { t | Ps(t) }. Then P is true of all ground -terms if M is a -algebra.

[Prev] [Home] [BHome]
28 October 1996