Как вы назовете утверждение P , которое никогда не было формально доказано, но все наблюдения подтверждают его?
Этот вопрос исходит из этого сценария: некоторые люди используют программное обеспечение для работы. Они часто используют определенную функцию. Когда эта функция была разработана, разработчики опасались, что могут возникнуть некоторые ошибки. Однако эти ошибки никогда не возникают, и рабочие используют его годами. Конечно, эта функция работает правильно, потому что никогда не подводила. Однако ни один разработчик не нашел времени, чтобы понять, как это сделать.
В этом примере P — это утверждение « эта функция не содержит ошибок ».
Частично это зависит от предметной области, в которую попадает утверждение, и от того, насколько оно было подтверждено фактами (например, просто еще не опровергнутым или тщательно проверенным и подтвержденным). Создание комментариев:
Вы могли бы назвать это предположением , если оно относится к математике или логике, или если оно еще не было хорошо подтверждено.
В науке это назвали бы гипотезой .
Более общим термином была бы [эпистемическая] возможность . Обратите внимание, что это эпистемическое, потому что мы говорим о доказательствах и способах, которыми мы можем узнать, что что-то истинно; модальность не очень актуальна.
Отредактировано после вопроса:
Ваш пример интересен, потому что он не совсем соответствует предложенным терминам. Я бы сказал, что это более общий случай индуктивного утверждения («Это всегда работало в прошлом, поэтому оно будет работать и дальше»). Вывод о том, что он продолжит работать, можно назвать индукцией . Это соответствует образцу обращения к дедуцируемому заключению как к дедукции .
Сократ мудр, а Сократ человек. Мой вывод состоит в том, что некоторые люди мудры.
Каждый раз, когда я ронял яблоко на поверхность земли, оно падало вниз. Мое предположение состоит в том, что так будет и в будущем.
Я признаю, что это немного необычное использование, но я думаю, что оно лучше всего подходит для вашей ситуации.
Поскольку ваш вопрос относился к программному обеспечению, вот ответ, связанный с программным обеспечением: программное обеспечение, которое используется в производстве в течение многих лет и еще не дало сбоев, называется либо надежным , либо зрелым .
Это не делает никаких предположений о его фактической правильности. Оба термина говорят только о том, что до сих пор они работали в реальных условиях, а не о том, что их правильность доказана при любых обстоятельствах.
Конечно, эта функциональность правильная, потому что она никогда не подводила.
Это неверный вывод. То, что он еще не потерпел неудачу, не означает, что этого не произойдет в будущем. Мы не можем быть уверены.
Есть способы доказать, что определенные параметры сохраняются при определенных условиях, и это делается строго в критическом программном обеспечении. Ожидается, что некоторые части программного обеспечения, такие как ОС VxWorks, будут иметь только один BSOD каждые 30 лет.
Для конкретной ситуации с программным обеспечением, которую вы описываете, взгляните на Hoare Logic, как обсуждалось, например, в https://en.wikipedia.org/wiki/Hoare_logic .
В этой модели корректность вашей программы определяется набором троек Хоара в форме {P}C{Q} , где {P} = предусловия/ввод, C = ваша_программа, {Q} = постусловия/вывод. Учитывая ввод, удовлетворяющий любому из предписанных предварительных условий, если вывод вашей программы удовлетворяет соответствующим постусловиям, то он «правильный».
В качестве простого примера предположим, что C =program_to_add_two_numbers. Тогда одна тройка Хоара может быть {P}C{Q} , где {P} =both_numbers_to_be_added_are_нечетно, а {Q} =sum_is_even. Очевидно, что одна тройка Хоара сама по себе не устанавливает правильность C. Но подходящая коллекция троек Хоара обычно помогает. («Обычно» означает всякий раз, когда существует набор троек Хоара, который однозначно, в смысле «если и только если», определяет функцию : ввод -> вывод, которую необходимо вычислить.)
И вы можете проверить некоторые из ссылок «См. также» в нижней части этой статьи в Википедии, чтобы узнать о нескольких других моделях корректности программ. Как вы можете себе представить, компьютерная наука посвятила этому предмету множество тщательных исследований.
edit: Спасибо, @JamesKingsbery Что касается вашего замечания «термин для этой концепции», да, я должен был прямо упомянуть, что вы можете найти в Google термин «корректность программы» для получения большого количества дополнительной информации.
Насколько я понимаю стандартное использование, формально доказуемое предложение является теоремой, поэтому «P является теоремой» говорит, что P истинно и что утверждение, что P истинно, подтверждается дедуктивным доказательством. Гипотеза выдвигается как верная, но без формального обоснования, будь то дедуктивного или индуктивного. Эмпирические утверждения никогда не доказуемы формально, поэтому их обоснования бывают либо индуктивными, либо абдуктивными. Это верно даже для «законов»; например, Закон Ома нельзя доказать формально. Лучшее, что мы можем сделать, это провести множество экспериментов, заметить, что оно никогда не нарушается, и сделать вывод (индуктивно? абдуктивно?), что это должно быть правдой. Тогда мы называем это теорией (о мире природы).
Я думаю, что ваш вариант использования принципиально отличается. Обычно мы не называем программы теоремами, хотя могли бы, если бы доказали их правильность. Скорее мы бы назвали их «сертифицированными» или тому подобное. Программа, корректность которой формально не доказана, но которая никогда не подводила, на самом деле не похожа на эмпирическую теорию, потому что она не является естественным артефактом. В отличие от эмпирического утверждения, в принципе можно было бы доказать, что такая программа верна или неверна.
Я бы предложил опираться на инженерию, а не на логику, и назвать такие программы надежными . Это имеет то преимущество, что устраняет понятие истины, которое является философским вопросом, не имеющим отношения к технике. У него также есть хорошее формальное статистическое определение, которым я не буду вас утомлять, и оно связано с такими понятиями, как надежность, поскольку обоснование заявлений о надежности будет включать дисперсию: если ваш код работает в течение 10 лет без ошибок, но всегда с один и тот же вход, то он может быть надежным для этого входа, но вы понятия не имеете, насколько он надежен, т.е. надежен ли он в различных условиях.
Их называют утверждениями, принимаемыми «на веру», «на доверие» или «с оговорками». Примером тому является утверждение - хорошие люди попадают в рай. Достоверность этого заявления больше зависит от правдоподобия (доверия) к человеку, делающему его, чем от самого заявления.
В частности, в отношении программ/функций это совершенно другое дело. Программа создается человеком (-ами), поэтому будет ли программа работать «всегда» во «всех возможных» условиях, зависит от того, насколько тщательно программист предусмотрел все такие возможные ошибки и насколько тщательно отдел тестирования выполнил свою работу. . Очевидно, что чем тщательнее были проведены эти мероприятия, тем меньше вероятность того, что программа провалится. Однако высокая вероятность «человеческих ошибок» не позволяет гарантировать , что та или иная программа (или функция) всегда будет работать при любых условиях! Следовательно, утверждению «эта функция не содержит ошибок» должно предшествовать выражение «пока что,this...", чтобы сделать его "разумным" утверждением (утверждением, имеющим смысл).
Утверждение, которое принимается за истину, но никогда не было доказано? В математике вы бы назвали это «неверно принятым за истину».
Даже в разработке программного обеспечения, где стандарты будут ниже, никто в здравом уме никогда не назовет какое-либо программное обеспечение «безошибочным». Вы можете услышать, что в программном обеспечении нет известных ошибок или дефектов.
Мауро АЛЛЕГРАНСА
Спросите о Монике
Элиран
Эра
пользователь20153
Альберто
пользователь20153
пользователь20153