Правило канонического сокращения

Всякое правильно построенное и корректное стековое выражение, не содержащее функций-запросов item и empty, имеет эквивалентную каноническую форму, которая не содержит функции remove (т.е. состоит только из функций put и new>). Эта каноническая форма получается путем применения аксиомы стека A2 всегда, пока это возможно.

Таким образом, мы завершили доказательство достаточной полноты, но только для выражений, не содержащих функции-запросы, и, следовательно, только свойства S1 (проверка корректности выражения). Для завершения доказательства нужно рассмотреть выражения, включающие функции-запросы, и обсудить задачу S2 (нахождение значений для выражений-запросов). Это означает, что нам нужно некоторое правило для определения корректности и значения всякого правильно построенного выражения вида f(s), где s - это правильно построенное выражение, а f - это либо item, либо empty.

Это правило и доказательство его корректности также используют индукцию по уровню вложенности. Пусть n - это уровень вложенности s. Если n=0, то s может быть только new, поскольку остальные функции требуют аргументов и, следовательно, содержат хоть одну пару скобок. Тогда для обеих функций-запросов ситуация ясна:

[x]. empty (new) корректно и имеет значение истина (true) (по аксиоме A3);

[x]. item (new) некорректно, так как предусловие item требует выполнения not empty (s).

Индукционный шаг: предположим, что s имеет уровень вложенности n не менее 1. Если у какого-либо подвыражения u выражения s внешняя функция есть item или empty, то уровень вложенности u не превосходит n-1, что по предположению индукции позволяет определить корректность u и, если u корректно, получить его значение, применяя аксиомы. Выполнив замены всех таких подвыражений, получим для s эквивалентную форму, в которую входят только функции put, remove и new.

Далее используем идею введенной выше канонической формы, чтобы избавиться от всех вхождений remove, так что результирующая форма для s будет включать только функции put и new. Случай, когда s это просто new уже был рассмотрен, остался случай, когда s имеет вид put(s', x). В этом случае для двух рассматриваемых выражений имеем:

[x]. empty (s) корректно и по аксиоме A3 значение этого выражения есть ложь (false);

[x]. item (s) корректно, так как предусловие not empty (s) для item выполнено; из аксиомы A1 следует, что значение этого выражения равно x.

Это завершает доказательство достаточной полноты, так как мы показали справедливость множества правил - правила корректного веса и правила канонического сокращения, позволяющего нам выяснять корректность заданного стекового выражения, а для корректного выражения-запроса - определять его значение в терминах значений типов BOOLEAN и G.