DRAKON.SU

Текущее время: Понедельник, 19 Февраль, 2018 18:48

Часовой пояс: UTC + 3 часа




Начать новую тему Ответить на тему  [ Сообщений: 7 ] 
Автор Сообщение
 Заголовок сообщения: Логика веры
СообщениеДобавлено: Пятница, 08 Сентябрь, 2017 15:54 

Зарегистрирован: Вторник, 22 Сентябрь, 2015 20:43
Сообщения: 71
    Логика веры

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

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

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


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Логика веры
СообщениеДобавлено: Пятница, 08 Сентябрь, 2017 17:21 

Зарегистрирован: Пятница, 13 Март, 2009 16:36
Сообщения: 205
Откуда: Казань
По поводу веры мне в принципе сказать нечего. Я не специалист в этой теме.
Как мне показалось, она немного перекликается с темой, что такое доказательство.
Есть известная задача с 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), на котором возможно доказывать корректность программ для всех случаев, отпадает необходимость в тестировании и отладке, которые проверяют только ничтожно малую часть всех возможных вариантов".


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Логика веры
СообщениеДобавлено: Суббота, 09 Сентябрь, 2017 15:10 

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

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

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

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

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

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


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Логика веры
СообщениеДобавлено: Понедельник, 11 Сентябрь, 2017 12:29 

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

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

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


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Логика веры
СообщениеДобавлено: Понедельник, 18 Сентябрь, 2017 02:32 

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

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


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Логика веры
СообщениеДобавлено: Понедельник, 18 Сентябрь, 2017 08:54 

Зарегистрирован: Пятница, 13 Март, 2009 16:36
Сообщения: 205
Откуда: Казань
Guarded command language описан в книге Дейкстры "Дисциплина программирования", которая есть на русском языке. То как gcl можно применить к оптимизации программ описано в диссертации Bradis 1995, ETH. Как можно применить к верификации параллельных программ описано в книге авторов Apt и др, которая была издана в 1992 и переиздана в 2003, но они на английском.


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Логика веры
СообщениеДобавлено: Воскресенье, 24 Декабрь, 2017 22:48 
Аватара пользователя

Зарегистрирован: Пятница, 10 Март, 2017 08:05
Сообщения: 45
Коллеги, имеет ли тема "Логика веры" какое-либо отношение к разделу "Космическое программирование"? Вопрос про интуицию и веру, скорее всего, важный. Но расположить его, видимо, нужно в другом разделе форума.


Вернуться к началу
 Профиль  
 
Показать сообщения за:  Поле сортировки  
Начать новую тему Ответить на тему  [ Сообщений: 7 ] 

Часовой пояс: UTC + 3 часа


Кто сейчас на конференции

Сейчас этот форум просматривают: нет зарегистрированных пользователей и гости: 1


Вы не можете начинать темы
Вы не можете отвечать на сообщения
Вы не можете редактировать свои сообщения
Вы не можете удалять свои сообщения
Вы не можете добавлять вложения

Найти:
Вся информация, размещаемая участниками на конференции (тексты сообщений, вложения и пр.) © 2008-2017, участники конференции «DRAKON.SU», если специально не оговорено иное.
Администрация не несет ответственности за мнения, стиль и достоверность высказываний участников, равно как и за безопасность материалов, предоставляемых участниками во вложениях.
Powered by phpBB® Forum Software © phpBB Group
Русская поддержка phpBB