2014 dxdy logo

Научный форум dxdy

Математика, Физика, Computer Science, Machine Learning, LaTeX, Механика и Техника, Химия,
Биология и Медицина, Экономика и Финансовая Математика, Гуманитарные науки




Начать новую тему Ответить на тему
 
 Правильная работа программ
Сообщение07.02.2019, 04:00 


06/04/18
220
Предположим, я использую в своей программе алгоритм, истинность которого доказана методом математической индукции. Почему этот алгоритм даёт правильный результат? С математической точки зрения алгоритм является верным, поскольку может быть доказан по индукции. Но почему должна правильно работать программа, которая его использует?

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

Доказать можно вообще всё, что угодно. Имеется бесконечное число всевозможных аксиоматик, в каждой из которых можно доказать что-то, что опровергается в другой. Но у программы есть ровно два варианта поведения: либо работа программы приводит к ожидаемому результату, либо — нет.

Я перестал понимать, как связана математическая доказуемость с работоспособностью, и связана ли вообще. Впрочем, я и раньше этого не понимал, просто как-то не задумывался на эту тему.

 Профиль  
                  
 
 Re: Правильная работа программ
Сообщение07.02.2019, 08:00 


08/12/17
130
Так вы определитесь сначала, что для вас означает, что программа работает "правильно", иными словами, как вы интерпретирует результаты ее работы. Ибо при одной интерпретации результата одна и та же программа будет работать правильно, а при другой - нет. Вот тут то у вас и встанет все на свои места.

 Профиль  
                  
 
 Re: Правильная работа программ
Сообщение07.02.2019, 08:08 
Заслуженный участник


20/08/14
5502
Россия, Москва
Qlin в сообщении #1374586 писал(а):
Предположим, я использую в своей программе алгоритм, истинность которого доказана методом математической индукции. Почему этот алгоритм даёт правильный результат? С математической точки зрения алгоритм является верным, поскольку может быть доказан по индукции. Но почему должна правильно работать программа, которая его использует?
Может быть потому что Вы пока не наткнулись на задачу, которая не реализуема машиной Тьюринга (см. Полнота по Тьюрингу)? Т.е. не вышли за рамки класса тьюринг-полных алгоритмов, которые все базируются на одной аксиоматике? Или потому что ваши алгоритмы уже автоматом привязаны к некоей аксиоматике, точно реализуемой машиной Тьюринга и соответственно программой на тьюринг-полном языке программирования? Собственно даже само понятие Алгоритм у Вас может быть ограничено лишь реализуемыми алгоритмами ...

Qlin в сообщении #1374586 писал(а):
Но у программы есть ровно два варианта поведения: либо работа программы приводит к ожидаемому результату, либо — нет.
Ну это не совсем верно, есть и третий вариант: бесконечное ожидание. Т.е. программа не выдаёт ни ожидаемый результат, ни его отрицание за конечное время. См.: Алгоритмическая разрешимость, Алгоритмически неразрешимая задача, Проблема остановки, Константа Хайтина.

 Профиль  
                  
 
 Re: Правильная работа программ
Сообщение07.02.2019, 11:33 
Заслуженный участник


26/05/14
677
Мне в решении этих вопросов помогла книга Дэвида Гриса "Наука программирования". Для каждого оператора языка программирования определяется его точная семантика в терминах предусловий и постусловий (речь об императивном языке). Получается аксиоматика, привязанная к конкретному языку. На основании аксиом доказываются теоремы для процедур. Также на языке пред- и постусловий. В конце концов вы доказываете теорему для всей программы: если входные данные отвечают таким-то предусловиям, то выходные отвечают таким-то постусловиям.
Полная цепочка: постановка задачи, перевод задачи на язык пред- и постусловий, написание программы, доказательство теоремы.

Есть более формальная и фундаментальная книга Эдсгера Дейкстры "Дисциплина программирования".
Обе книги довольно старые, но основы с тех пор не поменялись. После прочтения вы по-новому взгляните на языки программирования.

 Профиль  
                  
 
 Re: Правильная работа программ
Сообщение15.02.2019, 20:42 


16/02/15
81
Qlin в сообщении #1374586 писал(а):
Я перестал понимать, как связана математическая доказуемость с работоспособностью, и связана ли вообще.

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

Смысл задаётся ограничениями, а программа просто оперирует в рамках ограничений, а программист доказывает, что в рамках общих и для его теории и для программы ограничений результат будет именно ожидаемым.

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

Модераторы: Karan, PAV, Toucan, maxal, Супермодераторы



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

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


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

Найти:
Powered by phpBB © 2000, 2002, 2005, 2007 phpBB Group