Корректность — математическое понятие¶

Корректность — свойство логического или математического выражения (терма, формулы, доказательства, алгоритма), заключающееся в том, что оно построено согласно правилам синтаксиса и семантики соответствующего формального языка, то есть имеет осмысленную интерпретацию и допустимо в рамках принятой системы обозначений. Понятие противопоставляется некорректности: некорректным считается выражение, содержащее синтаксические ошибки, ссылки на необъявленные символы, нарушение правил построения формул или лишенное смысла в выбранной модели.

¶Синтаксическая и семантическая корректность

В математической логике различают два уровня корректности.

Синтаксическая корректность означает, что выражение построено по правилам грамматики формального языка: правильно расставлены скобки, использованы только объявленные символы, операторы применены к допустимым типам аргументов. Например, формула «(P ∧ Q → R)» синтаксически некорректна, если в языке не предусмотрены соответствующие скобки или порядок операций неоднозначен.

Семантическая корректность означает, что выражение имеет истинностное значение (или значение в некоторой модели) при любых допустимых интерпретациях примитивов. Формула, которая истинна в любой модели, называется логически истинной (в общем случае — валидной). Синтаксически корректная формула может быть семантически некорректной, если она не имеет смысла, например содержит обращение к несуществующему объекту.

¶Корректность в доказательствах

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

Понятие корректности тесно связано с понятием непротиворечивости формальной теории: теория считается непротиворечивой, если в ней не может быть выведено одновременно некоторое утверждение и его отрицание. Если теория противоречива, то из неё с помощью корректных рассуждений выводится что угодно (принцип «ex falso quodlibet»), и понятие корректности вывода теряет содержательный смысл.

¶Корректность алгоритмов

В теории вычислимости и программировании корректность алгоритма — это свойство алгоритма (программы) решать поставленную задачу согласно её формальному описанию. Различают:

• частную корректность (partial correctness): если алгоритм завершается, то результат соответствует спецификации;
• полную корректность (total correctness): алгоритм не только даёт правильный результат, но и гарантированно завершается за конечное время.

Проблема доказательства корректности программ была поставлена в 1960-е годы. Ричард Хоар предложил в 1969 году так называемую логику Хоара — формальную систему, в которой корректность программы выражается в виде тройки «{P} S {Q}», где P — предусловие, S — программа, Q — постусловие. Доказательство корректности состоит в обосновании того, что если предусловие P истинно до выполнения S, то после завершения S постусловие Q будет истинно.

¶Корректность в теории категорий и типах

В теории типов и особенно в интуиционистской математике корректность выражения определяется его типизированностью: выражение корректно, если его тип согласован с контекстом использования. В системах типа Curry–Howard корректность доказательства отождествляется с типизированностью программы, что позволяет переносить понятие корректности из логики в вычисления и обратно.

¶Критерий Гёделя

К. Гёдель в 1931 году доказал, что для достаточно богатых непротиворечивых формальных систем (содержащих арифметику натуральных чисел) невозможно внутри самой системы доказать её собственную непротиворечивость. Это ограничение касается и вопросов корректности: полный внутренний критерий корректности всех доказательств, выводимых в системе, в самой системе построить нельзя. Для практики это означает, что проверка корректности доказательства может требовать выхода за рамки исходной формальной системы.

¶Применение

Понятие корректности применяется в математической логике, теории доказательств, формальной верификации программ, теории баз данных (проверка корректности запросов), лингвистике (корректность построения высказываний естественного языка), юриспруденции (корректность нормативных актов с точки зрения иерархии законов). В теории баз данных под корректностью отношения понимается его согласованность с ограничениями целостности (primary key, foreign key, доменные ограничения).

¶Источники

• Кляйнрок Л. «Введение в теорию вычислимости»
• Хоар Т. «An Axiomatic Basis for Computer Programming» (1969)
• Клейни С. «Математическая логика»
• Дворецкий А. А., Суслов Е. И. «Дискретная математика»
• Мендельсон Э. «Введение в математическую логику»