Логика вычислимости - Computability logic

Не путать с Вычислительная логика.

Логика вычислимости (CoL) представляет собой исследовательскую программу и математическую основу для преобразования логики в систематическую формальную теорию вычислимость, в отличие от классическая логика что является формальной теорией истины. Он был представлен и назван так Георгий Джапаридзе в 2003 г.[1]

В классической логике формулы представляют собой истинные / ложные утверждения. В CoL формулы представляют вычислительные проблемы. В классической логике действительность формулы зависит только от ее формы, а не от ее значения. В CoL валидность означает всегда вычислимость. В более общем плане классическая логика говорит нам, когда истинность данного утверждения всегда следует из истинности данного набора других утверждений. Точно так же CoL сообщает нам, когда вычислимость данной проблемы А всегда следует из вычислимости других заданных задач B1, ..., Bп. Более того, он обеспечивает единообразный способ построения решения (алгоритм ) для такого А из любых известных решений B1, ..., Bп.

CoL формулирует вычислительные проблемы в их самом общем виде: интерактивный смысл. CoL определяет вычислительная проблема как игра машины против своего окружения. Такая проблема вычислимый если есть машина, которая побеждает в игре против любого возможного поведения окружающей среды. Такой игровой автомат обобщает Тезис Черча-Тьюринга на интерактивный уровень. Классическое понятие истины оказывается особым случаем вычислимости с нулевой степенью интерактивности. Это делает классическую логику особым фрагментом CoL. Таким образом, CoL является консервативное расширение классической логики. Логика вычислимости более выразительна, конструктивна и вычислительно значима, чем классическая логика. Помимо классической логики, независимая (IF) логика и некоторые правильные расширения линейная логика и интуиционистская логика также оказываются естественными фрагментами CoL.[2][3] Следовательно, значимые концепции «интуиционистской истины», «истины линейной логики» и «истины IF-логики» могут быть получены из семантики CoL.

CoL систематически отвечает на фундаментальный вопрос о том, что и как можно вычислить; таким образом, CoL имеет множество приложений, таких как конструктивные прикладные теории, системы баз знаний, системы планирования и действий. Из них пока широко исследованы только приложения в конструктивных прикладных теориях: построена серия теорий чисел на основе CoL, называемых «кларифметикой».[4][5] как значимые с точки зрения вычислений и сложности альтернативы основанной на классической логике Арифметика Пеано и его вариации, такие как системы ограниченная арифметика.

Традиционные системы доказательства, такие как естественный вычет и последовательное исчисление недостаточны для аксиоматизации нетривиальных фрагментов CoL. Это потребовало разработки альтернативных, более общих и гибких методов доказательства, таких как круговой исчисление.[6][7]

Язык

Операторы логики вычислимости: имена, символы и чтения

Полный язык CoL расширяет язык классической логики первого порядка. Его логический словарь имеет несколько видов союзов, дизъюнкций, кванторов, импликаций, отрицаний и так называемых операторов повторения. Этот сборник включает все связки и кванторы классической логики. В языке также есть два вида нелогических атомов: элементарный и Общее. Элементарные атомы, которые представляют собой не что иное, как атомы классической логики, представляют собой элементарные проблемы, то есть игры без ходов, которые автоматически выигрываются машиной при истинном значении и проигрывают при ложном. С другой стороны, общие атомы можно интерпретировать как любые игры, элементарные или неэлементарные. Как семантически, так и синтаксически классическая логика есть не что иное, как фрагмент CoL, полученный путем запрета общих атомов на ее языке и запрета всех операторов, кроме ¬, ∧, ∨, →, ∀, ∃.

Джапаридзе неоднократно указывал, что язык CoL является открытым и может подвергаться дальнейшим расширениям. Из-за выразительности этого языка достижения в CoL, такие как построение аксиоматизаций или построение прикладных теорий на основе CoL, обычно ограничивались тем или иным надлежащим фрагментом языка.

Семантика

Игры, лежащие в основе семантики CoL, называются статические игры. В таких играх нет порядка хода; игрок всегда может двигаться, пока другие игроки «думают». Однако статические игры никогда не наказывают игрока за слишком долгое «размышление» (откладывание собственных ходов), поэтому такие игры никогда не становятся соревнованиями на скорость. Все элементарные игры автоматически статичны, так же как и игры могут быть интерпретациями общих атомов.

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

Под логическими операторами CoL понимаются операции над играми. Здесь мы неофициально рассматриваем некоторые из этих операций. Для простоты мы предполагаем, что предметом обсуждения всегда является множество всех натуральных чисел: {0,1,2, ...}.

Операция ¬ из отрицание («не») меняет роли двух игроков, превращая ходы и победы машины в ходы и победы среды, и наоборот. Например, если Шахматы это игра в шахматы (но с исключенной ничьей) с точки зрения белого игрока, то ¬Шахматы это та же игра с точки зрения черного игрока.

В параллельное соединение ∧ ("панд") и параллельная дизъюнкция ∨ («пор») объединяют игры параллельно. Пробежка А∧B или А∨B это одновременная игра в двух союзов. Машина выигрывает А∧B если он выиграет их обоих. Машина выигрывает А∨B если выиграет хотя бы один из них. Например, Шахматы∨¬Шахматы это игра на двух досках, на одной белой и черной, и в которой задача автомата - выиграть хотя бы на одной доске. Такую игру можно легко выиграть независимо от того, кто противник, копируя его ходы с одной доски на другую.

В параллельное следствие оператор → («пимпликация») определяется как А→B = ¬А∨B. Интуитивный смысл этой операции таков: сокращение B к А, т.е. решение А пока противник решает B.

В параллельные кванторы ∧ («приелась») и ∨ («пексисты») могут быть определены как ∧xA(Икс) = А(0)∧А(1)∧А(2) ∧ ... и ∨xA(Икс) = А(0)∨А(1)∨А(2) ∨ .... Таким образом, это одновременные игры А(0),А(1),А(2), ..., каждый на отдельной доске. Машина выигрывает ∧xA(Икс) (соотв. ∨xA(Икс)), если он выиграет все (или некоторые) из этих игр.

В слепые кванторы ∀ («болтун») и ∃ («блексисты»), с другой стороны, создают одноплатные игры. Пробежка ∀xA(Икс) или ∃xA(Икс) - это один запуск А. Машина выигрывает ∀xA(Икс) (соответственно ∃xA(Икс)) если такой пробег - выигранный пробег А(Икс) для всех (соответственно хотя бы одного) возможных значений Икс.

Все описанные до сих пор операторы ведут себя точно так же, как их классические аналоги, когда они применяются к элементарным (безходным) играм, и подтверждают те же принципы. Вот почему CoL использует те же символы для этих операторов, что и классическая логика. Однако, когда такие операторы применяются к неэлементарным играм, их поведение перестает быть классическим. Так, например, если п является элементарным атомом и п общий атом, п→п∧п действительно пока п→п∧п не является. Принцип исключенного среднего п∨¬пОднако остается в силе. Тот же принцип недействителен для всех трех видов дизъюнкции (выбор, последовательный и переключаемый).

В дизъюнкция выбора ⊔ («хор») игр А и B, написано А⊔B, это игра, в которой для победы машина должна выбрать один из двух дизъюнктов, а затем выиграть в выбранном компоненте. В последовательная дизъюнкция ("сор") АᐁB начинается как А; он также заканчивается как А если машина не делает "переключение", в этом случае А прерывается, игра перезапускается и продолжается B. в переключение дизъюнкции ("тор") А⩛B, машина может переключаться между А и B любое конечное количество раз. У каждого оператора дизъюнкции есть двойная конъюнкция, полученная путем перестановки ролей двух игроков. Соответствующие кванторы могут быть дополнительно определены как бесконечные конъюнкции или дизъюнкции так же, как в случае параллельных кванторов. Каждая дизъюнкция сортировки также вызывает соответствующую операцию импликации так же, как это было в случае параллельной импликации →. Например, значение выбора («шимпликация») А⊐B определяется как ¬А⊔B.

В параллельное повторение ("предвестник") А можно определить как бесконечное параллельное соединение А∧A∧A∧ ... Последовательный ("повторяемость") и переключаемый ("повторение") виды повторений могут быть определены аналогично.

В сердцевина операторы можно определить как бесконечные дизъюнкции. Повторение ветвления ("краткость") ⫰, который является наиболее сильным типом повторения, не имеет соответствующей конъюнкции. ⫰А это игра, которая начинается и продолжается как А. Однако в любое время среде разрешается совершить «репликационный» ход, который создает две копии текущей на тот момент позиции А, таким образом разделяя игру на две параллельные нити с общим прошлым, но, возможно, с разными будущими событиями. Таким же образом среда может в дальнейшем реплицировать любую позицию любого потока, тем самым создавая все больше и больше потоков А. Эти потоки воспроизводятся параллельно, и машина должна выиграть А во всех темах, чтобы стать победителем в ⫰А. Ветвление сердечника ("повторение") ⫯ определяется симметрично заменой «машина» и «среда».

Каждый вид повторения далее порождает соответствующую слабую версию импликации и слабую версию отрицания. Первый считается римпликация, а последний опровержение. В разветвление римпликации ("бимпликация") А⟜B не что иное, как ⫰А→B, а разветвленное опровержение ("брефутация") А является А⟜⊥, где ⊥ - всегда проигрышная элементарная игра. Точно так же и со всеми остальными импликациями и опровержениями.

Как инструмент описания проблемы

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

Позволять ж быть унарной функцией. Проблема вычислений ж будет записано как ⊓Икс⊔у (у=ж(Икс)). Согласно семантике CoL, это игра, в которой первый ход («ввод») осуществляется средой, которая должна выбрать значение м для Икс. Интуитивно это равносильно тому, чтобы попросить машину сказать значение ж(м). Игра продолжается как ⊔у (у=ж(м)). Теперь ожидается, что машина сделает ход («выход»), который должен выбирать значение п для у. Это означает, что п это ценность ж(м). Игра теперь сведена к элементарному п=ж(м), который выигрывает машина тогда и только тогда, когда п действительно ценность ж(м).

Позволять п быть унарным предикатом. потом ⊓Икс(п(Икс)⊔¬п(Икс)) выражает проблему решение п, ⊓Икс(п(Икс)&ᐁ¬п(Икс)) выражает проблему полурешение п, и ⊓Икс(п(Икс)⩛¬п(Икс)) проблема рекурсивно аппроксимирующий п.

Позволять п и q быть двумя унарными предикатами. потом ⊓Икс(п(Икс)⊔¬п(Икс))⟜⊓Икс(q(Икс)⊔¬q(Икс)) выражает проблему Редукция по Тьюрингу q к п (в том смысле, что q сводится ли Тьюринг к п тогда и только тогда, когда интерактивная задача ⊓Икс(п(Икс)⊔¬п(Икс))⟜⊓Икс(q(Икс)⊔¬q(Икс)) вычислимо). ⊓Икс(п(Икс)⊔¬п(Икс))→⊓Икс(q(Икс)⊔¬q(Икс)) делает то же самое, но для более сильной версии редукции Тьюринга, где оракул для п можно запросить только один раз. ⊓Икс⊔у(q(Икс)↔п(у)) делает то же самое для проблемы много-одно сокращение q к п. С помощью более сложных выражений можно охватить все виды безымянных, но потенциально значимых отношений и операций над вычислительными задачами, такими как, например, «уменьшение по Тьюрингу проблемы полурешения. р к проблеме сокращения многих единиц q к п". Налагая ограничения по времени или пространству на работу машины, можно получить теоретико-сложные аналоги таких отношений и операций.

Как инструмент решения проблем

Известные дедуктивные системы для различных фрагментов CoL обладают тем свойством, что решение (алгоритм) может быть автоматически извлечено из доказательства проблемы в системе. Это свойство далее наследуется всеми прикладными теориями, основанными на этих системах. Итак, чтобы найти решение данной проблемы, достаточно выразить его на языке CoL, а затем найти доказательство этого выражения. Другой способ взглянуть на это явление - придумать формулу г CoL как спецификация программы (цель). Тогда доказательство г это - точнее, переводится - программа, соответствующая этой спецификации. Нет необходимости проверять соответствие спецификации, потому что само доказательство фактически является такой проверкой.

Примерами прикладных теорий на основе CoL являются так называемые кларифметика. Это теории чисел, основанные на CoL в том же смысле, в каком арифметика Пеано PA основана на классической логике. Такая система обычно является консервативным продолжением PA. Обычно он включает все Аксиомы Пеано, и добавляет к ним одну или две аксиомы экстра-Пеано, такие как ⊓Икс⊔у(у=Икс'), выражающие вычислимость функции-последователя. Обычно в нем также есть одно или два нелогических правила вывода, таких как конструктивные версии индукции или понимания. Посредством рутинных изменений таких правил можно получить надежные и законченные системы, характеризующие тот или иной интерактивный класс вычислительной сложности. C. Это в том смысле, что проблема принадлежит C тогда и только тогда, когда у него есть доказательство в теории. Таким образом, такую ​​теорию можно использовать для поиска не только алгоритмических решений, но и эффективных по запросу, таких как решения, которые выполняются за полиномиальное время или в логарифмическом пространстве. Следует отметить, что все кларифметические теории разделяют одни и те же логические постулаты, и только их нелогические постулаты меняются в зависимости от целевого класса сложности. Их заметная отличительная черта от других подходов с похожими устремлениями (например, ограниченная арифметика ) заключается в том, что они расширяют, а не ослабляют PA, сохраняя при этом полную дедуктивную силу и удобство последнего.

Смотрите также

использованная литература

  1. ^ Г. Джапаридзе, Введение в логику вычислимости. Анналы чистой и прикладной логики 123 (2003), страницы 1–99. Дои:10.1016 / S0168-0072 (03) 00023-X
  2. ^ Г. Джапаридзе, Вначале была семантика игры?. Игры: объединяющая логику, язык и философию. О. Майер, А.-В. Пьетаринен и Т. Туленхеймо, ред. Springer 2009, стр. 249–350. Дои:10.1007/978-1-4020-9374-6_11 Предварительная публикация
  3. ^ Г. Джапаридзе, Интуиционистский фрагмент логики вычислимости на пропозициональном уровне. Анналы чистой и прикладной логики 147 (2007), страницы 187–227. Дои:10.1016 / j.apal.2007.05.001
  4. ^ Г. Джапаридзе, Введение в кларифметику I. Информация и вычисления 209 (2011), стр. 1312–1354. Дои:10.1016 / j.ic.2011.07.002 Предварительная публикация
  5. ^ Г. Джапаридзе, Создайте свою собственную кларифметику I: Настройка и полнота. Логические методы - информатика 12 (2016), выпуск 3, статья 8, стр. 1–59.
  6. ^ Г. Джапаридзе, Введение в круговое исчисление и семантику абстрактных ресурсов. Журнал логики и вычислений 16 (2006), страницы 489–532. Дои:10.1093 / logcom / exl005 Предварительная публикация
  7. ^ Г. Джапаридзе, Укрощение повторений в логике вычислимости с помощью кругового исчисления, часть I. Архив математической логики 52 (2013), стр. 173–212. Дои:10.1007 / s00153-012-0313-8 Предварительная публикация

внешние ссылки