On The Ambiguity Problem of Backus Systems

ABSTRACT

Backus [1] has developed an elegant method of defining well-formed formulas for computer languages such as ALGOL. It consists of (our notation is slightly different from that of Backus): A finite alphabet: a1, a2, …, at; Predicates: P1, P2, …, P@@@@; Productions, either of the form (a) aj ∈ Pi; or of the form (b) Pi2Pi1 … Pit → Pj. A word is a finite sequence of letters from the alphabet. Then IIIa states that certain words (containing only one letter) belong initially to some of the predicates, and IIIb states that if words W1, W2, …, Wt belong to the predicates Pi1, Pi2, …, Pit respectively, then the concatenation W1W2 … Wt belongs to Pj. We call this a Backus system. A simple example of such a system is: Alphabet: a, b; Predicates: P, Q, R; Productions: a ∈ P, b ∈ Q, PQ → R, QP → R; RR → R, PRQ → R, QRP → R. Then P and Q contain only the words a and b, respectively, while R contains all words which have the same number of a's and b's. In the above example, abab belongs to R and can be produced in two ways. Namely, as ab ∈ R and RR → R, abab ∈ R; also as ba ∈ R and PRQ → R, abab ∈ R. We call a Backus system ambiguous if one of its predicates contains a word which can be produced in more than one way. As, in practice, the meaning of a word is determined by the way it is produced, an ambiguous Backus System must be avoided. As the following example illustrates, ALGOL 60 [3] is ambiguous: if B ∧ C then for I: = 1 step 1 until N do if D ∨ E then A[I] : = 0 else K : = K + 1; K : = K - 1 In fact, both for I := 1 step 1 until N do if D ∨ E then A[I] := 0 and for I := 1 step 1 until N do if D ∨ E then A[I] := 0 else K := K + 1 are valid for statements of ALGOL 60. Combining the first with if B ∧ C then … else K = K + 1; or the second with if B ∧ C then … gives rise to the above example, and these two methods of construction correspond to the two possible meanings of the example. D. Dahm and H. Trotter, in a private communication, have raised the question: “Does there exist an algorithm to determine whether a Backus system is ambiguous?” We call this the ambiguity problem. The purpose of this paper is to show that no such algorithm exist, i.e., that the ambiguity problem is unsolvable.We first define a normal system. It consists of: A finite alphabet: a1, a2, …, at; A finite collection of ordered pairs: (g1, g1), (g2, g2), …, (gr, gr), where the gi and gi are words. An axiom A which is some fixed word. If U and V are words, we say U → V if U is of the form gP and V is of the form Pg where (g,g) is one of the ordered pairs. We also write, in this case, giP → Pgi. Also, if U1, U2, …, Un are words with Ui → Ui+1, 1 ≦ i ≦ n-1, then U1 → Un, and we say Un is derived from U1. The words which may be derived from the axiom A are called theorems. A normal system is called undecidable if there does not exist an algorithm for determining whether a word is a theorem of the system. It is implicit in [2, sec. 6.5] that there exists an undecidable normal system, which we denote by NS, with the property that in each ordered pair (g, g), the words g and g have no common letters. LEMMA. If U and V are words of NS, then U → V, if and only if there exists indices j1, j2, …, jm such that Ugj1gj2 … gjm = gj1gj2 … gjmV. PROOF. Suppose the equality holds. As gj1 and gj1 have no common letters, U is of the form gj1R1 ; let U1 = R1gj1. Then we have U → U1 and U1gj2 … gjm = gj2gj3 … gjmV. Proceeding inductively, we obtain a sequence of words, U, U1, U2, …, Um = V with U → U1 → … → Um ; hence U → V. Conversely, if U → V, then there exist words U0, U1, …, Um with U0 = U and Um = V, and indices j1, j2, …, jm such that Ui-1gji = gjiUi, 1 ≦ i ≦ m. Then U0gj1 = gj1 U1 or U0gj1gj2 = gj1U1gj2 = gj1gj2U2. By induction the proof is complete. THEOREM. The ambiguity problem is unsolvable. PROOF. We describe certain predicates and Backus systems; to save space we omit the formal definitions. It is easy to construct predicates and systems with the required properties. We use as alphabet the alphabet a1, a2, …, at of NS and in addition the letters b1, b2, …, br, one for each ordered pair (gi, gi) of NS. If A is the axiom of NS, form the predicate P which contains all words of the form bjmbjm-1 … bj1Agj1gj2 … gjm; if W is any word on the alphabet a1, a2, …, ar, let Qw be the predicate containing all words of the form bjmbjm-1 … bj1gj1gj2 … gjmW. It is possible to construct the predicates P and Qw so that there is no ambiguity in their definition, and we assume that this is done. Then form the Backus system Bw which contains the predicates P, Qw, and Sw, where Sw is defined by P → Sw and Qw → Sw. Now, in order for Bw to be ambiguous, Bw must contain a predicate which contains a word which comes about in two ways. The predicates P and Qw, and all predicates used in their definition, do not have this property. Thus Bw is ambiguous if and only if Sw contains a word which comes about in two ways. From the definition of Sw, it is clear that Bw is ambiguous if and only if P and Qw have a word in common. Observing the form of the words in P and Qw we see that Bw is ambiguous if and only if there exists indices j1, j2, …, jm such that bjm … bj1Agj1 … gjm = bjm … bj1gj1 … gjmW. By the lemma, this is true if and only if A → W. Thus if the ambiguity problem for Backus systems were solvable, then the decision problem for NS would be solvable, which is not the case. Hence the ambiguity problem is unsolvable.

REFERENCES

• 1: BACKUS, J.W. ACM-GAMM Conference ICIP, June 1959.
• 2: DAvis, MXR~IN. Computability and unsolvability. New York, 1958.
• 3: Peter Naur , J. W. Backus , F. L. Bauer , J. Green , C. Katz , J. McCarthy , A. J. Perlis , H. Rutishauser , K. Samelson , B. Vauquois , J. H. Wegstein , A. van Wijngaarden , M. Woodger, Report on the algorithmic language ALGOL 60, Communications of the ACM, v.3 n.5, p.299-314, May 1960 [doi>10.1145/367236.367262]

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.3 Formal Languages
          Subjects: Algebraic language theory

Additional Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Computability theory

General Terms:
Languages, Performance, Theory, Verification