A formula has the syntax shown in figure 1(a). If a formula has the particular syntax given in figure 1(b) we say that the formula is in Normal Form (NF).
Figure 1. Formular syntax, Figure 1(a) The general syntax of a formula
Figure 1. Formular syntax, Figure 1(b) The syntax of a NF formula
A formula is converted to NF according to the rewriting rules given below, where F represents a formula, S stands for a non empty sequence of formulae, and s and s' denote possibly empty sequences of formulae. Applying a rewriting rule q→r on a formula F means to substitute by r a part of F that matches the pattern q, as shown in figure 2. The conversion terminates when no rewriting rule can be applied. The conversion terminates for any formula, and the result is unique regardless which rules are applied on which parts of the formula and in which order.
- (+F)→F
- (*F)→F
- (+s(+S)s')→(+sSs')
- (*s(*S)s')→(*sSs')
- (*s(+FS)s')→(+(*sFs')(*s(+S)s'))
Figure 2. Converting a formula to NF
Let NF(F) be the normal form of the formula F. The problem is to write a term generator that for a given formula F and a number k outputs the next k terms from NF(F) in the order in which they appear in NF(F). If the terms are exhausted, the generator continues from the first term of NF(F). For example, consider F=(+(*(+(*ab)(+a))b)), and NF(F)=(+(*abb)(*ab)) as in figure 2. Generating the first term from NF(F) yields (*abb). Generating two more terms produces (*ab), (*abb). Notice that if NF(F) contains similar terms, as in the last example in figure 3, these terms are considered distinct.
Write a term generator that reads sets of data from the standard input.