Назовем вычислительной последовательностью [4] для дерева вывода t в AG последовательность вида:
cs = (n1, A1)(n2, A2)(n2, A2) ... (nr, Ar);
где
Таким образом при входе "вниз" в поддерево вычисляются некоторые наследуемые атрибуты корня поддерева, при возврате из поддерева вычисляются некоторые синтезируемые атрибуты корня поддерева.
Назовем незацикленную атрибутную грамматику корректной, если для всякого еe атрибутированного дерева существует вычислительная последовательность.
Теорема B.4. Незацикленная атрибутная грамматика корректна тогда и только тогда, когда для каждого правила p : X0
X1 ... Xnp если aI(Xi), i[1, np], то имеется в точности одно семантическое правило, сопоставленное p и определяющее значение a(Xi), и если aS(X0), то имеется в точности одно семантическое правило, сопоставленное p и определяющее значение a(X0).Теорема B.5. Сложность проверки незацикленной атрибутной грамматики на корректность линейна по размеру атрибутной грамматики.
Пусть t - дерево вывода и n - его внутренняя вершина. Рассмотрим вычислительную последовательность для t вида cs = cs1<n, B1>cs2<n, B2>cs3, где n входит в cs1 чeтное число раз, и не входит в cs2. Последовательность cs2 обходит поддерево с корнем n. Будем говорить, что <n, B1>cs2<n, B2> определяет визит в поддерево с корнем n и что вершина n в результате этого визита посещается один раз. Таким образом, если n входит в cs 2h раз, то n посещается h раз.