Аксиомы стека

Для всех x: G, s: STACK [G]

[x]. (A3) empty (new)

[x]. (A4) not empty (put (s, x))

При уровне вложенности 0 (без скобок) выражение e должно совпадать с new, поэтому его вес равен 0 и оно корректно, так как у new нет никаких предусловий. Аксиома A3 утверждает, что empty (new) истинно. Это обеспечивает базис индукции как для правила корректного веса, так и для правила нулевого веса.

Индукционный шаг: предположим, что оба правила выполняются для всех выражений с уровнем вложенности не более n. Нужно доказать, что тогда они выполняются и для любого выражения e с уровнем вложенности n+1. Поскольку наши выражения сейчас не содержат функций-запросов, то e должно иметь один из следующих двух видов:

E1 · e = put (s, x)

E2 · e = remove (s)

где x имеет тип G, а уровень вложенности у s равен n. Пусть ws - это вес s.

В случае E1, поскольку put - всюду определенная функция, e корректно тогда и только тогда, когда s корректно, т. е. (по предположению индукции) тогда и только тогда, когда s и все его подвыражения имеют неотрицательные веса. Но это эквивалентно тому, что e и все его подвыражения имеют неотрицательные веса, что и доказывает правило корректного веса в этом случае. Кроме того, e имеет положительный вес ws+1, и (по аксиоме A4) является непустым, что доказывает правило нулевого веса.

В случае E2 выражение e корректно тогда и только тогда, когда выполняются два следующих условия:

EB1 _ s и все его подвыражения являются корректными.

EB2 _ not empty (s) (это предусловие для функции remove).

По предположению индукции условие EB2 означает, что вес s ws положителен или, что эквивалентно, вес e, равный ws - 1, является неотрицательным. Следовательно, e удовлетворяет Правилу корректного веса. Чтобы доказать, что оно также удовлетворяет правилу нулевого веса, нужно показать, что e пусто тогда и только тогда, когда его вес равен 0. Так как вес s положителен, то s должно содержать по крайней мере одно вхождение put, которое также входит и в e. Рассмотрим самое внешнее вхождение put в e, это вхождение находится непосредственно внутри remove (так как remove находится на самом внешнем уровне у e). Это означает, что у e имеется подвыражение (быть может, совпадающее с самим e) вида

remove (put (stack_expression, g_expression)),

которое по аксиоме A2 можно сократить просто до stack_expression. После выполнения этой замены вес e уменьшится на 2, и получившееся выражение, имеющее то же значение, что и e, удовлетворяет по предположению индукции правилу нулевого веса. Это доказывает утверждение индукции в случае E2.

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

put (remove (remove (put (put (remove (put (put (new, x1), x2)), x3), x4))), x5)

имеет то же значение, что и каноническая форма:

put (put (new, x1), x5).

Давайте дадим этому механизму имя и приведем его определение: