![]() Главная страница Случайная страница КАТЕГОРИИ: АвтомобилиАстрономияБиологияГеографияДом и садДругие языкиДругоеИнформатикаИсторияКультураЛитератураЛогикаМатематикаМедицинаМеталлургияМеханикаОбразованиеОхрана трудаПедагогикаПолитикаПравоПсихологияРелигияРиторикаСоциологияСпортСтроительствоТехнологияТуризмФизикаФилософияФинансыХимияЧерчениеЭкологияЭкономикаЭлектроника |
Аксиомы стека
Для всех 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).
Давайте дадим этому механизму имя и приведем его определение:
|