КаталогИндекс раздела


    

Вычисление в сравнении с программированием

Эдсгер В. Дейкстра

Computation versus program (EWD238)

Я буду использовать два простых примера, чтобы проиллюстрировать весьма фундаментальный опыт. Два вычисления, которые порождают одинаковый выход, являются эквивалентными в этом смысле и априори неэквивалентными любому другому.

В отношении между программой и вычислением мы видим, что программа разворачивается в пространстве текста, а вычисление разворачивается во времени. Для любой данной комбинации программы и вычисления, так называемое, установление последовательности описывает, как продвижение вычисления (как "движется" время) отображается на продвижение через программу (как "продвижение" по тексту).

Последнее является путями для сравнения программ; некоторые хотят делать это, чтобы сравнивать соответствующие вычисления. Основной опыт состоит в том, что невозможно (или бесполезно, или ужасно трудно, или непривлекательно, или что хотите) сравнивать вычисления путем сравнения соответствующих программ, когда на уровне сравнения установления последовательностей двух программ различаются.

Чуть более подробно: если мы можем разобрать два вычисления как последовательности действий, и мы можем отобразить две последовательности действий друг на друга, мы можем сравнивать их сравнением текстов программ, при условии, что тексты программ могут быть так же разобраны в инструкции, каждая из которых соответствует действию.

Позвольте мне привести два примера, абстрактный и конкретный. Абстрактный пример следующий. За исключение побочных эффектов булевских выражений и константы B2

    "while B1 do if B2 then S1
                      else S2"
эквивалентно
    "if B1 then while B1 do S1
          else while B1 do S2"

Первая конструкция является в основном одной из тех последовательностей, которые управляются выражением повторения, вторая является в основном одной из тех последовательностей, которые управляются условным выражением. Я могу установить эквивалентность результата вычислений, но я не могу рассматривать их как эквивалентные в любом другом полезном смысле.

Конкретный пример состоит в конструировании программы, генерирующей непустые последовательности из цифр 0, 1 и 2 без непустых поэлементно равных соседних последовательностей, генерировать их в алфавитном порядке до тех пор, пока длина последовательности не достигнет 100 (т.е до 100 цифр). (Начало списка последовательностей, который должен генерироваться такое:
    0
    01
    010
    0102
    01020
    01021
    010210
    010212    )

Программист может использовать знание того, что последовательность длиной 100, удовлетворяющая условиям, уже существует. Каждое решение (кроме первого) является расширением (на одну цифру) предыдущего решения, и алгоритм, следовательно, является явным алгоритмом с возвратами.

Мы ищем "хорошую" последовательность, мы предполагаем, что доступен некоторый примитив, исследующий, является ли пробная последовательность хорошей. Если она хорошая, пробная последовательность печатается и расширяется нулем, чтобы получить следующую пробную последовательность; если пробная последовательность не хорошая, мы выполняем на ней операцию "увеличение", чтобы получить следующую пробную последовательность, т.е., последние цифры = 2 удаляются, а затем последняя оставшаяся цифра увеличивается на 1. (Существование решения длиной 100 и наша остановка на нем будет видно из того, что удаление последних цифр = 2 никогда не приведет к пустой последовательности.)

Версия 1a использует тот факт, что единичный ноль является первым правильным решением.

Версия 1a:

    "Установить пробную последовательность в единичный ноль (и длину в 1)
     while длина < 101 do
        begin if хорошая then
           begin печатать пробную последовательность; расширить пробную последовательность нулем end
              else
           увеличить пробную последовательность
        end"

Версия 1b рассматривает пустую последовательность как виртуальное решение, не печатаемое:

Версия 1b:

    "Установить пробную последовательность пустой (и длину в 0)
     while длина < 100 do
        begin расширить пробную последовательность нулем
           while не хорошая do увеличить пробную последовательность
                  печатать пробную последовательность
        end

Одно заметное различие состоит в операторе, который должен повторяться. В Версии 1a (условной) печать решения предшествует генерации следующей попытки, в Версии 1b печать находится в конце повторяемого оператора. Это различие объясняет и различия в инициализации и проверке повторения. Но это незначительное различие, как показывает

Версия 1c:

    "Установить пробную последовательность в единичный ноль (и длину в 1)
     while длина < 101 do
        begin while не хорошая do увеличить пробную последовательность;
              печатать пробную последовательность;
              расширить пробную последовательность нулем 
        end"

Громадное различие состоит в том, что в Версии 1a два повторения сливаются в одно, тогда как Версия 1b может рассматриваться как детализация Версии 0b:

    "Установить пробную последовательность пустой (и длину в 0)
     while длина < 100 do
        begin преобразовать текущую последовательность в следующее решение
                  печатать пробную последовательность
        end

Версии 1a и 1b явно несовместимы. В этом состоял мой основной опыт.

Поразмыслив, я решил предложить вашему вниманию третий пример, представляющий граничный случай. Даны два массива X[1:N] и Y[1:N] и булевское "equal", сделать программу, которая придает "equal" смысл "два данных массива поэлементно равны". Пустые массива рассматриваются как равные.

Нельзя сравнить два массива одним действием, нужно проделывать это поэлементно; мы введем целое "j" и придадим "equal" следующий смысл "между первыми j парами элементов не найдено различий", и придем к следующему фрагменту программы:

Версия 1:

    j := 0; equal := true;
    while j < N do
       begin j:= j + 1; equal := equal and (X[j] = Y[j]) end

Задача выполнена: начальное состояние соответствует j = 0, оператор в выражении повторения реализует шаг индукции от j к j + 1 (до сих пор не было различий и нет новых различий) и ко времени, когда j = N, мы будем иметь желаемое значение.

Рассматривая это присваивание:

       "equal := equal and ..." 

мы можем прийти к заключению, что однажды сохраненное equal=false будет постоянным и, следовательно, последующее выполнение выражения повторения не имеет смысла. (Вспомните, что нас интересует только конечное значение "equal".) Это наблюдение дает в результате следующую программную секцию:

Версия 2:

    j := 0; equal := true;
    while j < N and equal  do
       begin j:= j + 1; equal := equal and (X[j] = Y[j]) end

Но теперь мы сделали программу таким способом, что повторяющийся оператор будет выполняться только при "equal = true" и в результате "equal and" может быть пропущено.

Версия 3:

    j := 0; equal := true;
    while j < N and equal  do
       begin j:= j + 1; equal := (X[j] = Y[j]) end

и это, по-видимому, будет наша последняя версия.

Вышеприведенное является формой "латания программы", которую я ненавижу. Например, заключение, приведшее к Версии 2, порождено чтением Версии 1; Версия 2 довольно смехотворна, она появляется только как промежуточный шаг между двумя другими версиями. Вопрос: как Версии 1 и 3 соотносятся друг с другом? Последовательности разные, хотя достаточно похожие, так что я могу отобразить их одну на другую.

Мы имеем N + 1 функций EQUAL[j] для 0 <= j <= N определенных на массивах и заданных, как:

    EQUAL[0] = true
    EQUAL[j] = EQUAL[j-1] and (X[j] = Y[j])

и в терминах этих функций запрашиваем выполнение присваивания

    equal := EQUAL[N].

Общий прототип Версии 1 и Версии 3 будет чем-то вроде:

    j := 0; equal := EQUAL[0];
    while "возможно equal <> EQUAL[N]" do
       begin j:= j + 1; "equal := EQUAL[j]" end 

Теперь это хитро и не слишком хорошо сформулировано. Каждый раз, когда выполняется проверка, отношение equal = EQUAL[j] будет сохранятся, поскольку общий прототип сделан таким способом. При каждой проверке, независимо от того equal = EQUAL[N] или нет, я включил слово "возможно" и поместил условие в кавычки на всякий случай, чтобы показать, что в любом случае мы гарантируем, что равенство сохраняется. Если мы отказываемся дать такую гарантию, ну, тогда "возможно" сохраняется неравенство.

Другой способ сказать, почему я поместил проверку в кавычки, - что я имел в виду, что я связываю истинность или ложность с булевским выражением, не устанавливая, какое это выражение.

Наш выбор проверки зависит от нашей лени, от того количества математического анализа, которое мы захотим потратить в определении функции EQUAL. Мы можем быть ленивыми и сказать так: ну, на момент проверки я знаю, что

    equal := EQUAL[j]
и я отказываюсь принимать решение, что
    equal := EQUAL[N]
прежде, чем будет
    j = N .

Это приведет к Версии 1.

Мы можем применить некоторый анализ к рекуррентному отношению и принять решение, что для каждого j

    EQUAL[j] = false предполагает  EQUAL[i] = false для всех  i>=j.

Класс ситуации, на которой мы теперь готовы гарантировать равенство "equal = EQUAL[N]", расширился до "j = N or equal = false", это ведет к Версии 3.

Теперь последует действительно хитрая вещь. Мы можем рассматривать "возможно equal = EQUAL[N]" как открытый примитив, который мы выберем позднее, но выбор, который мы делаем, определяет набор условий, при которых повторяющийся оператор должен выполняться. В Версии 1 единственное, что мы можем сделать, это

В Версии 3 вычисление EQUAL[j] ограничено случаем EQUAL[j-1] = true, так что требует другого взятого в кавычки действия "equal = EQUAL[j]", в зависимости от выбора проверки. В Версии 3 это может быть реализовано при помощи

    "equal := (X[j] = Y[j]) или if X[j] <> Y[j] then equal := false",

используя известный нам факт, что изначальное equal = true сохраняется.

Мой общий прототип является неудобным предком!


КаталогИндекс раздела