Абстрактные типы данных (АТД)



         

Доказательство достаточной полноты - часть 4


Это доказывает утверждение индукции в случае 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).

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

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

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

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

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

  • empty (new) корректно и имеет значение истина (true) (по аксиоме A3);
  • item (new) некорректно, так как предусловие item требует выполнения not empty (s) .
  • Индукционный шаг: предположим, что s имеет уровень вложенности n не менее 1.


    Содержание  Назад  Вперед