Induction Principles for Context-Free Languages

Abstract

In proving assertions about programs, it is necessary to use induction principles in one form or another. Recursion induction was introduced by McCarthy [4] for the purpose of proving assertions about functions, in particular, functions defined by recursive conditional expressions. Structural induction was introduced by Burstall [1] for proving assertions about structures, such as lists and trees. The induction principles which we shall introduce here are useful for proving assertions about context-free languages and their semantic attributes, as this term is used by Knuth [3]. We shall introduce these principles informally and use them to prove the equivalence of two syntactic definitions of an unsigned integer, the equivalence of Knuth’s two examples of synthesized and inherited attributes, and the validity of Hoare’s first axiom (also known as the “back substitution rule”) for a large class of programming languages.