Реализуемость - Realizability
В математической логике , реализуемость представляет собой совокупность методов в теории доказательств , используемых для изучения конструктивных доказательств и извлечения дополнительной информации из них. Формулы формальной теории «реализуются» объектами, известными как «реализаторы», таким образом, что знание реализатора дает знание об истинности формулы. Есть много вариантов реализации; какой именно класс формул изучается и какие объекты являются реализаторами, различаются от одной вариации к другой.
Реализуемость можно рассматривать как формализацию интерпретации интуиционистской логики BHK ; в реализуемости понятие «доказательства» (которое остается неопределенным в интерпретации BHK) заменяется формальным понятием «реализатор». Большинство вариантов реализуемости начинаются с теоремы о том, что любое утверждение, которое можно доказать в изучаемой формальной системе, реализуемо. Реализатор, однако, обычно дает больше информации о формуле, чем непосредственно формальное доказательство.
Помимо понимания интуиционистской доказуемости, реализуемость может быть применена для доказательства свойств дизъюнкции и существования для интуиционистских теорий и для извлечения программ из доказательств, как в добыче доказательств . Это также связано с теорией топосов через реализуемость топосов .
Пример: реализуемость по цифрам
В первоначальной версии реализуемости Клини натуральные числа используются в качестве реализаторов формул в арифметике Гейтинга . Следующие пункты используются для определения отношения « n реализует A » между натуральными числами n и формулами A на языке арифметики Гейтинга. Требуется несколько обозначений: во-первых, упорядоченная пара ( n , m ) обрабатывается как одно число с использованием фиксированной эффективной функции спаривания ; во- вторых, для каждого натурального числа п , ф п является вычислимая функция с индексом п .
- Число n реализует атомарную формулу s = t тогда и только тогда, когда s = t истинно. Таким образом, каждое число реализует истинное уравнение, и никакое число не реализует ложное уравнение.
- Пара ( п , м ) реализует формулу ∧ B тогда и только тогда , когда п реализует А и м реализует B . Таким образом, реализатор конъюнкции - это пара реализаторов конъюнктов.
- Пара ( n , m ) реализует формулу A ∨ B тогда и только тогда, когда выполняется следующее: n равно 0 или 1; и если n равно 0, то m реализует A ; и если п равно 1 , то м реализует B . Таким образом, реализатор для дизъюнкции явно выбирает один из дизъюнктов (с n ) и предоставляет для него реализатор (с m ).
- Ряд п реализует формулу → B , если и только если для каждого м , реализующего А , ф п ( м ) реализует B . Таким образом, реализатор для импликации - это вычислимая функция, которая принимает реализатор для гипотезы и производит реализатор для заключения.
- Пара ( n , m ) реализует формулу (∃ x ) A ( x ) тогда и только тогда, когда m является реализатором для A ( n ). Таким образом, реализатор для экзистенциальной формулы производит явное свидетельство для квантора вместе с реализатором для формулы, экземпляр которой создан с этим свидетелем.
- Число n реализует формулу (∀ x ) A ( x ) тогда и только тогда, когда для всех m определено φ n ( m ) и реализует A ( m ). Таким образом, реализатор для универсального оператора - это вычислимая функция, которая производит для каждого m реализатор для формулы, экземпляр которой создается с помощью m .
С этим определением получается следующая теорема:
- Пусть A будет предложением арифметики Гейтинга (HA). Если HA доказывает А , то есть п такое , что п реализует A .
С другой стороны, есть формулы, которые реализованы, но не могут быть доказаны в HA - факт, впервые установленный Роузом.
Дальнейший анализ метода может быть использован для доказательства того, что HA обладает « свойствами дизъюнкции и существования »:
- Если HA доказывает предложение (∃ x ) A ( x ), то существует n такое, что HA доказывает A ( n )
- Если HA доказывает предложение ∨ B , то HA доказывает или HA доказывает , B .
Более поздние разработки
Крайзель представил модифицированную реализуемость , которая использует типизированное лямбда-исчисление в качестве языка реализаторов. Модифицированная реализуемость - это один из способов показать, что принцип Маркова не выводится из интуиционистской логики. Напротив, он позволяет конструктивно обосновать принцип независимости помещения:
- .
Относительная реализуемость - это интуиционистский анализ рекурсивных или рекурсивно перечислимых элементов структур данных, которые не обязательно вычислимы, таких как вычислимые операции над всеми действительными числами, когда действительные числа могут быть только аппроксимированы в цифровых компьютерных системах.
Приложения
Реализуемость - один из методов, используемых в добыче доказательств для извлечения конкретных «программ» из, казалось бы, неконструктивных математических доказательств. Извлечение программ с использованием реализуемости реализовано в некоторых помощниках проверки, таких как Coq .
Смотрите также
Ноты
Ссылки
- Биркедал, Ларс; Яап ван Остен (2000). Относительная и модифицированная относительная реализуемость .
- Крайзель Г. (1959). «Интерпретация анализа с помощью конструктивных функционалов конечных типов», в: Конструктивность в математике, под редакцией А. Хейтинга, Северная Голландия, стр. 101–128.
- Клини, SC (1945). «Об интерпретации интуиционистской теории чисел». Журнал символической логики . 10 (4): 109–124. DOI : 10.2307 / 2269016 . JSTOR 2269016 .
- Клини, SC (1973). «Реализуемость: ретроспективный обзор» от Матиаса, ARD; Хартли Роджерс (1973). Кембридж Летняя школа в математической логики: провел в Кембридже / Англия, август 1-21, 1971 . Берлин: Springer. ISBN 3-540-05569-X.С. 95–112.
- ван Остен, Яап (2000). Реализуемость: исторический очерк .
- Роза, GF (1953). «Исчисление высказываний и реализуемость» . Труды Американского математического общества . 75 (1): 1–19. DOI : 10.2307 / 1990776 . JSTOR 1990776 .
внешние ссылки
- Реализуемость Сборник ссылок на последние статьи по реализуемости и смежным темам.