DRAKON.SU

Логика веры

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

Описание концепции логики веры в моей короткой статье.

Данная тема поставляет необходимый контекст для последующего обсуждения злободневного вопроса.
Почему структурное программирование превратилось в религию?
Кое-что по поводу структурного программирования было высказано раньше.
Есть другие вопросы, связанные с верой и затрагивающие данный раздел форума.

По поводу веры мне в принципе сказать нечего. Я не специалист в этой теме.
Как мне показалось, она немного перекликается с темой, что такое доказательство.
Есть известная задача с 62 клетками (как шахматная доска 8 на 8, где две угловые клетки убраны), которые нужно замостить с помощью домино 2 на 1. Можно очень долго думать над этой задачей и пытаться замостить, но если раскрасить доску, в черные и белые клетки, как шахматную доску и подсчитать сколько черных клеток, а сколько белых, то становится ясно, что невозможно замостить, так как количество черных и белых клеток не совпадает, а одна кастяшка домино всегда перекрывает одну черную и одну белую клетку. Когда разумному человеку это объясняется, он понимает это доказательство. В принципе можно составить математическую модель данной задачи и более строго показать, но все равно, любое математическое доказательство требует определенной интуиции, определенной веры, если хотите.

По поводу структурного программирования. Ваше описание не полное:

Дейкстра в одной из своих статей жаловался, что


Опишу вам мое понимание текстов Дейкстры о структурном программировании.
"Сложность программ высока, а интелеллектуальные способности человека ограничены" --->
"Необходимо декомпозировать задачу на подзадачи, решать подзадачи, убеждаться (доказывать), что подзадача решена верно, если все подзадачи решены верно, то и вся задача будет решена верна (стандартная методика "разделяй и влавствуй", а также стандартная методика решения задач в математике)" --->
"При решении задач или подзадач может потребоваться цикл (так как цикл является воплощением математического метода индукция в программировании), необходимо уметь доказывать корректность программ с циклами" --->
"Для того, чтобы доказывать корректность циклов необходим инвариант цикла и может потребоваться определенный счетчик цикла" --->
"Goto позволяет создавать неявные циклы в программе и для того, чтобы доказывать такие программы, с каждым таким неявным циклом необходимо связать свой инвариант и свой счетчик (об это как раз написано в статье Goto considered harmful)" --->
"Чтобы не мучиться, определяя все неявные циклы в программе, лучше избегать использования оператора Goto, достаточно обычного цикла (к тому же, это доказано Бёмом и Якопини)" --->
"То что мы избегаем goto, не означает, что не нужно разделять задачу на подзадачи и доказывать корректность решения каждой подзадачи" --->
"Когда Дейкстра решал, на каком же языке программирования, попроще донести свои мысли о решении задач в программировании до читателей, он выбирал из существующих языков программирования, но они его не удовлетворили" --->
"Он решил спроектировать свой язык программирования, который называют guarded command language" --->
"В процессе проектирования языка программирования, на котором будет проще доказывать программы, он сделал несколько открытий" --->
"То, что недетерминированность упрощает решение задачи, хотя большинство языков программирования строго детерминированные" --->
"Недетерминированность также позволяет довольно легко анализировать параллельные процессы, которые протекают в реальном мире, и которые сложно моделируются на существующих языках программирования" --->
"При наличии языка программирования (guarded command language), на котором возможно доказывать корректность программ для всех случаев, отпадает необходимость в тестировании и отладке, которые проверяют только ничтожно малую часть всех возможных вариантов".

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

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

Многие пытались реализовать стиль программирования Дейкстры в реальном производственном программировании.
Не получилось. Де факто. Никто не заявлял об успехе.
Данный метод декомпозиции программ был еще до Дейкстры.
Говорить, что цикл -- некий аналог математической индукции, не правильно. Это не так.

Вы знаете людей, которые писали инварианты циклов?
А я знаю. Их можно по пальцам пересчитать.
Инварианты не для простых программистов.


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

По мне так метод Дейкстры и метод Хоара - это практически одно и то же (хотя можно рассматривать как разный взгляд на одно и то же явление, например, в физике электрон иногда рассматривают как частцу, а иногда как волну).
И лично я не вижу, особых различий между двумя методами.
Единственное у Дейкстры пишется wp(...), а у Хоара {...}
Какие есть существенные различия между методом Дейкстры и методом Хоара?


Сейчас язык Дейкстры входит в арсенал инструментов информатики. С помощью этого языка описывают оптимизации программ, а также верификацию параллельных программ (Krzysztof R. Apt, Frank S. de Boer, Ernst-Rudiger Olderog "Verification of Sequential and Concurrent Programs"). Возможно, еще где-то используют.

Если я правильно понимаю, идея была в том, что перед действием записывается разрешающее его условие?
Можно ли получить ссылку на работу Дейкстры (желательно в русском переводе), где описан это язык? Заранее спасибо.
Нечто подобное, насколько я помню - вот только запамятовал ссылку, увы! - было у Тьюринга в его проекте ЭВМ Ace.
На самом деле подобный подход жив вполне, например, в архитектуре ARM с ее условным исполнением команд процессора.

Guarded command language описан в книге Дейкстры "Дисциплина программирования", которая есть на русском языке. То как gcl можно применить к оптимизации программ описано в диссертации Bradis 1995, ETH. Как можно применить к верификации параллельных программ описано в книге авторов Apt и др, которая была издана в 1992 и переиздана в 2003, но они на английском.

Коллеги, имеет ли тема "Логика веры" какое-либо отношение к разделу "Космическое программирование"? Вопрос про интуицию и веру, скорее всего, важный. Но расположить его, видимо, нужно в другом разделе форума.