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/ |