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

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

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

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

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

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

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

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

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

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

В языке 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.

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

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

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

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

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

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

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

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

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

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

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

Вот как следует рассматривать теорему объективно.