DRAKON.SU
https://forum.drakon.su/

Логика веры
https://forum.drakon.su/viewtopic.php?f=140&t=6065
Страница 1 из 1

Автор:  Владимир Шелехов [ Пятница, 08 Сентябрь, 2017 15:54 ]
Заголовок сообщения:  Логика веры

    Логика веры

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

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

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

Автор:  Rifat [ Пятница, 08 Сентябрь, 2017 17:21 ]
Заголовок сообщения:  Re: Логика веры

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

По поводу структурного программирования. Ваше описание не полное:
Цитата:
Структурное программирование объявляет оператор goto опасным и предлагает использовать только правильные операторы: последовательный, условный и цикл while. Больше ничего в структурном программировании по сути нет. Все остальное -- пустые декларации и спекуляции.

Дейкстра в одной из своих статей жаловался, что
Цитата:
Apparently, IBM did not like the popularity of my text; it stole the term "Structured Programming" and under its auspices Harlan D. Mills trivialized the original concept to the abolishment of the goto statement.


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

Автор:  Владимир Шелехов [ Суббота, 09 Сентябрь, 2017 15:10 ]
Заголовок сообщения:  Re: Логика веры

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

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

Rifat писал(а):
По поводу структурного программирования. Ваше описание не полное:
Цитата:
Структурное программирование объявляет оператор goto опасным и предлагает использовать только правильные операторы: последовательный, условный и цикл while. Больше ничего в структурном программировании по сути нет. Все остальное -- пустые декларации и спекуляции.
Дейкстра в одной из своих статей жаловался, что программисты почему-то не понимают, что структурное программирование это не просто удаление goto. До конца своей жизни Дейкстра писал заметки с примерами правильного доказательного программирования небольших программ. А люди по своей серости почему-то не понимают.
Многие пытались реализовать стиль программирования Дейкстры в реальном производственном программировании.
Не получилось. Де факто. Никто не заявлял об успехе.
Rifat писал(а):
Опишу вам мое понимание текстов Дейкстры о структурном программировании.
"Сложность программ высока, а интелеллектуальные способности человека ограничены" --->
"Необходимо декомпозировать задачу на подзадачи, решать подзадачи, убеждаться (доказывать), что подзадача решена верно, если все подзадачи решены верно, то и вся задача будет решена верна (стандартная методика "разделяй и влавствуй", а также стандартная методика решения задач в математике)"
Данный метод декомпозиции программ был еще до Дейкстры.
Rifat писал(а):
"При решении задач или подзадач может потребоваться цикл (так как цикл является воплощением математического метода индукция в программировании), необходимо уметь доказывать корректность программ с циклами" --->
"Для того, чтобы доказывать корректность циклов необходим инвариант цикла и может потребоваться определенный счетчик цикла"
Говорить, что цикл -- некий аналог математической индукции, не правильно. Это не так.

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

Rifat писал(а):
"Дейкстра .... решил спроектировать свой язык программирования, который называют guarded command language" --->
"В процессе проектирования языка программирования, на котором будет проще доказывать программы, он сделал несколько открытий" --->
"То, что недетерминированность упрощает решение задачи, хотя большинство языков программирования строго детерминированные" --->
"Недетерминированность также позволяет довольно легко анализировать параллельные процессы, которые протекают в реальном мире, и которые сложно моделируются на существующих языках программирования" --->
"При наличии языка программирования (guarded command language), на котором возможно доказывать корректность программ для всех случаев, отпадает необходимость в тестировании и отладке, которые проверяют только ничтожно малую часть всех возможных вариантов".

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

Автор:  Rifat [ Понедельник, 11 Сентябрь, 2017 12:29 ]
Заголовок сообщения:  Re: Логика веры

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

Цитата:
Сейчас этот язык Дейкстры упоминается лишь в историческом контексте.
По большому счету в нем нет ничего нового и полезного.

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

Автор:  TAU [ Понедельник, 18 Сентябрь, 2017 02:32 ]
Заголовок сообщения:  Re: Логика веры

Цитата:
"Дейкстра .... решил спроектировать свой язык программирования, который называют guarded command language" ---> недетерминированность упрощает решение задачи, хотя большинство языков программирования строго детерминированные" ---> "Недетерминированность также позволяет довольно легко анализировать параллельные процессы, которые протекают в реальном мире, и которые сложно моделируются на существующих языках программирования" ---> "При наличии языка программирования (guarded command language), на котором возможно доказывать корректность программ для всех случаев, отпадает необходимость в тестировании и отладке, которые проверяют только ничтожно малую часть всех возможных вариантов"
Сейчас этот язык Дейкстры упоминается лишь в историческом контексте

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

Автор:  Rifat [ Понедельник, 18 Сентябрь, 2017 08:54 ]
Заголовок сообщения:  Re: Логика веры

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

Автор:  Василий Валевич [ Воскресенье, 24 Декабрь, 2017 22:48 ]
Заголовок сообщения:  Re: Логика веры

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

Страница 1 из 1 Часовой пояс: UTC + 3 часа
Powered by phpBB® Forum Software © phpBB Group
https://www.phpbb.com/