Логика для вычислимости
Логики для вычислимости — это формулировки логики, которыезахватить некоторый аспект вычислимости как основное понятие. Обычно это предполагает сочетаниеспециальных логических связок , а также семантики , которая объясняет, как логику следует интерпретировать вычислительным способом.
Вероятно, первой формальной трактовкой логики вычислимости является интерпретация реализуемости Стивена Клини в 1945 году, который дал интерпретацию интуиционистской теории чисел в терминах вычислений машины Тьюринга . Его мотивацией было уточнить интерпретацию интуиционизма Хейтинга-Брауэра-Колмогорова (БГК) , согласно которой доказательства математических утверждений следует рассматривать как конструктивные процедуры.
С появлением многих других видов логики, таких как модальная логика и линейная логика , а также новых семантических моделей, таких как семантика игр , логика вычислимости была сформулирована в нескольких контекстах. Здесь мы упомянем два.
Модальная логика для вычислимости
[ редактировать ]Оригинальная интерпретация реализуемости Клини привлекла большое внимание тех, кто изучает связи между вычислимостью и логикой. Он был расширен до полной высшего порядка интуиционистской логики Мартином Хайландом в 1982 году, который построил эффективный топос . В 2002 году Стив Аводи , Ларс Биркедал и Дана Скотт сформулировали модальную логику вычислимости , которая расширила обычную интерпретацию реализуемости двумя модальными операторами, выражающими понятие «вычислимо истинности».
Вычислительная логика Джапаридзе
[ редактировать ]«Вычислимая логика» — это имя собственное, относящееся к исследовательской программе, инициированной Георгием Джапаридзе в 2003 году. Ее целью является переработка логики на основе теоретико-игровой семантики. Такая семантика рассматривает игры как формальные эквиваленты интерактивных вычислительных задач, а их «истину» — как существование алгоритмических выигрышных стратегий. См. Логику вычислимости.
См. также
[ редактировать ]Ссылки
[ редактировать ]- СК Клини. Об интерпретации интуиционистской теории чисел . Журнал символической логики , 10:109–124, 1945.
- JME Хайланд. Эффектный топос . В книге А. С. Трульстра и Д. ван Далена , редакторов, Симпозиум, посвященный столетию Л. Дж. Брауэра, страницы 165–216. Издательство Северной Голландии, 1982.
- С. Аводи, Л. Биркедал и Д.С. Скотт. Топосы локальной реализуемости и модальная логика вычислимости . Математические структуры в информатике, 12(3):319-334, 2002.
- Г. Джапаридзе, Введение в вычислимую логику . Анналы чистой и прикладной логики 123 (2003), страницы 1–99.