Теорема Бёма-Якопини

Question

Согласно теореме Бёма-Якопини, алгоритм может быть написан с использованием только трех утверждений:

• последовательность
• выбор
• итерация

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

Но когда я прошу объяснения, никто не может предоставить доказательства теоремы.

Лично я не думаю, что теорема неверна, но я думаю, что ее применимость в реальном мире не всегда лучший выбор.

Итак, я провел небольшой поиск, и это мои сомнения:

1. Доказана теорема об индукции в структуре блок-схемы, но действительно ли она применима в компьютерной программе?
   Согласно википедии "Бем и Якопини не были действительно практичны в качестве алгоритма преобразования программы, и, таким образом, открыли дверь для дополнительных исследований в этом направлении".

2. Следствие теоремы доказывает, что каждое "goto" может быть переведено в отбор или итерацию по индукции, но как насчет эффективности? Я не могу найти никаких доказательств того, что каждый алгоритм может быть переписан с сохранением той же производительности.

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

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

Образец:

n = 0;
while (n < 1000 || (cond1 && cond2) || (cond3 && cond4) || (cond5 && cond6)) 
{  
   n++;  
   //The rest of code  
}   

Может быть переписан как:

for (n = 0; n < 1000; n++)
{
   if (cond1 && cond2) break;
   elseif (cond2 && cond3) break;
   elseif (cond4 && cond5) break;
   elseif (cond6 && cond7) break;
   //The rest of code
}

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

5. Я нашел эту интересную статью: https://www.cs.cornell.edu/~kozen/papers/bohmjacopini.pdf Я думаю, это доказывает, что настоящая программа не должна принуждаться следовать теореме Яопини.
   Вы разделяете те же выводы?

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

Answer 1

Доказана теорема об индукции в структуре блок-схемы, но действительно ли она применима в компьютерной программе? Согласно википедии "Бем и Якопини не были действительно практичны в качестве алгоритма преобразования программы, и, таким образом, открыли дверь для дополнительных исследований в этом направлении".

Операции и структура, которые они дают, могут быть легко продемонстрированы способными воспроизводить функцию машины Тьюринга. Как таковая, это эквивалентная по Тьюрингу система вычислений. Согласно тезису Черча-Тьюринга, это, как полагают, столько вычислений, сколько мы можем сделать: goto не добавил бы ничего, что уже невозможно.

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

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

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

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

Answer 2

Согласно теореме Бёма-Якопини, алгоритм может быть написан с использованием только трех утверждений:

• последовательность
• выбор
• итерация

Язык While имеет следующие конструкции:

1. Назначение, V := E
2. Пустая программа, skip
3. Последовательность, S1;S2
4. Выбор, if B then S1 [elsif Si] else Sn fi, а также
5. Итерация. while B do S od

Вы пропустили назначение и skip, который является нейтральным элементом, как 0 в арифметике. Есть и другие структуры, которые я пропустил. Они имеют отношение к процедурной абстракции, которая называет последовательности операторов, то есть функции и процедуры. Но я не хочу расширять это сейчас.

Я нашел эту интересную статью: https://www.cs.cornell.edu/~kozen/papers/bohmjacopini.pdf Я думаю, это доказывает, что настоящая программа не должна принуждаться к следованию теореме Якопини. Вы разделяете те же выводы?

Козен - очень хороший автор, он строг и ясен.

Козен показал ограничение исчисления высказываний при доказательстве теоремы Бёма-Якопини. В оригинальной статье использовалось исчисление предикатов. Он дает правильное доказательство теоремы, используя методы, недоступные в 1960-х годах. Проблема возникает из-за того, что в преобразовании используются переменные, то, что не может быть обработано в исчислении высказываний. Существует другое преобразование, которое использует цикл с разрывами вместо While язык. Вся эта дискуссия о GOTO теперь хорошо понято. Статья интересна тем, что является примером того, как использовать новые методы в старой хорошо известной проблеме.

Вы можете использовать теорему Бёма-Якопини, потому что она производит эквивалентную программу.

Лично я не думаю, что теорема неверна, но я думаю, что ее применимость в реальном мире не всегда лучший выбор.

Этот результат поддерживает структурированное программирование. Но вы не должны использовать его, потому что вы не должны использовать диаграммы потоков данных для разработки программ. Вы не должны даже использовать While псевдокод для разработки программ.

Лучше всего использовать язык абстрактных спецификаций, который более адекватен для представления проблемы, которую вы хотите решить. Докажите свое решение, а затем напишите документ, который можно преобразовать в код вашего языка программирования. Это идея грамотного программирования. Объясните точно, что вы знаете о предметной области проблемы, укажите, как вы представляете свою проблему на языке абстрактных спецификаций, и систематически преобразуйте ее в язык программирования. Все объяснения должны выполняться на естественном языке и в математических формулах, а фрагменты кода должны быть отделимыми для создания программного кода. Для этого вы можете использовать такие программы, как CWeb и LaTeX.

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

Answer 3

https://stackru.com/images/0af6ad2f54d3ee d32b38f4cf9e729a4022d2aeb6.png

Любая программа, которая выглядит как Тип 1 /2 /3, может быть преобразована в

https://stackru.com/images/c76a2c42caa299487aee d67d03da5e d59e8d2831.png

Answer 4

Лично я считаю, что теорема создана не для того, чтобы писать лучший код,

Ну, этого никогда не было. Теорема не создавалась (теоремы просто так не создавались). Теорема была найдена как модель вычислений, как способ продемонстрировать, что оператор GOTO не является абсолютной необходимостью для кодирования алгоритма.

Нам необходимо понять контекст, в котором теорема была впервые предложена. В то время программисты использовали GOTO довольно жестоко и бессистемно, твердо веря, что операторы GOTO необходимы.

Теорема показывает, что это не так. Теперь теорема не означает, что программа, структурированная с ее помощью, неизбежно лучше (поскольку есть случаи, когда отклонение от предложенной структуры является лучшим/более элегантным/эффективным путем).

В то время эта теорема послужила гвоздем в гроб аргумента о том, что операторы GOTO необходимы для создания сложных программ (а это не так).

Самое большое преимущество теоремы в том, что она предложила новый (и в общем случае лучший) способ формулировать, анализировать и систематизировать алгоритмы.

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

В общем случае это правда, и не по какой-либо субъективной причине. Теорема является основой для структурного программирования, и в целом она оказалась намного лучше, чем ее предшественники.

Повторюсь, вся суть теоремы в том, что ДЛЯ ОБЩЕГО СЛУЧАЯ

1. вам не нужно полагаться на GOTO для последовательной логики
2. последовательная логика может быть единообразно описана этим методом
3. результирующая кодификация последовательной логики может быть формально проанализирована (попробуйте это с супом GOTO).

Именно так следует рассматривать теорему, объективно говоря.