Войти
Логика вычислимости (CoL ) - это исследовательская программа и математическая основа для преобразования логики в систематическую формальная теория вычислимости, в отличие от классической логики, которая является формальной теорией истины. Он был введен и назван так Георгием Джапаридзе в 2003 году.
В классической логике формулы представляют собой истинные / ложные утверждения. В CoL формулы представляют вычислительные проблемы. В классической логике действительность формулы зависит только от ее формы, а не от ее значения. В CoL валидность означает всегда вычислимость. В более общем плане классическая логика говорит нам, когда истинность данного утверждения всегда следует из истинности данного набора других утверждений. Точно так же CoL сообщает нам, когда вычислимость данной проблемы A всегда следует из вычислимости других данных задач B 1,..., B n. Более того, он обеспечивает единообразный способ фактически построить решение (алгоритм ) для такого A из любых известных решений B 1,..., B n.
CoL формулирует вычислительные проблемы в их самом общем - интерактивном смысле. CoL определяет вычислительную проблему как игру машины против своего окружения. Такая проблема вычислима, если есть машина, которая выигрывает игру против любого возможного поведения окружающей среды. Такая игровая машина обобщает тезис Чёрча-Тьюринга на интерактивный уровень. Классическое понятие истины оказывается особым случаем вычислимости с нулевой степенью интерактивности. Это делает классическую логику особым фрагментом CoL. Таким образом, CoL - это консервативное расширение классической логики. Логика вычислимости более выразительна, конструктивна и вычислительно значима, чем классическая логика. Помимо классической логики, естественными фрагментами CoL также оказываются дружественная к независимости (IF) логика и определенные собственные расширения линейной логики и интуиционистской логики. Следовательно, значимые концепции «интуиционистской истины», «истины линейной логики» и «истины IF-логики» могут быть получены из семантики CoL.
CoL систематически отвечает на фундаментальный вопрос о том, что и как можно вычислить; таким образом, CoL имеет множество приложений, таких как конструктивные прикладные теории, системы баз знаний, системы планирования и действий. Из них только приложения в конструктивных прикладных теориях были широко изучены до сих пор: серия основанных на CoL теорий чисел, названных «кларифметикой», была построена как значимые с точки зрения вычислений и сложности альтернативы основанной на классической логике Арифметика Пеано и ее разновидности, такие как системы ограниченной арифметики.
Традиционные системы доказательства, такие как естественная дедукция и последовательное исчисление, недостаточны для аксиоматизации нетривиальных фрагментов CoL. Это потребовало разработки альтернативных, более общих и гибких методов доказательства, таких как круговое исчисление.
Операторы логики вычислимости: имена, символы и значения Полный язык CoL расширяет язык классических логика первого порядка. Его логический словарь имеет несколько видов союзов, дизъюнкций, кванторов, импликаций, отрицаний и так называемых операторов повторения. Этот сборник включает все связки и кванторы классической логики. В языке также есть два вида нелогических атомов: элементарные и общие. Элементарные атомы, которые представляют собой не что иное, как атомы классической логики, представляют собой элементарные проблемы, то есть игры без ходов, которые автоматически выигрываются машиной, если они истинны, и проигрывают, когда ложны. С другой стороны, общие атомы можно интерпретировать как любые игры, элементарные или неэлементарные. Как семантически, так и синтаксически классическая логика есть не что иное, как фрагмент CoL, полученный путем запрета общих атомов на ее языке и запрета всех операторов, кроме ¬, ∧, ∨, →, ∀, ∃.
Джапаридзе неоднократно указывал, что язык CoL является открытым и может подвергнуться дальнейшим расширениям. Из-за выразительности этого языка достижения в CoL, такие как построение аксиоматизаций или построение прикладных теорий на основе CoL, обычно ограничивались тем или иным надлежащим фрагментом языка.
Игры, лежащие в основе семантики CoL, называются статическими играми. В таких играх нет порядка хода; игрок всегда может двигаться, пока другие игроки «думают». Однако статические игры никогда не наказывают игрока за слишком долгое «размышление» (откладывание собственных ходов), поэтому такие игры никогда не становятся соревнованиями на скорость. Все элементарные игры автоматически статичны, так же как и игры могут быть интерпретациями общих атомов.
В статических играх участвуют два игрока: машина и окружающая среда. Машина может следовать только алгоритмическим стратегиям, при этом нет ограничений на поведение среды. Каждый забег (игра) выигрывается одним из этих игроков и проигрывается другим.
Под логическими операторами CoL понимаются операции над играми. Здесь мы неофициально рассматриваем некоторые из этих операций. Для простоты мы предполагаем, что предметом обсуждения всегда является множество всех натуральных чисел: {0,1,2,...}.
Операция отрицания («не») переключает роли двух игроков, превращая ходы и выигрыши машины в ходы и победы окружения, и наоборот. Например, если шахматы - это игра в шахматы (но с исключенной ничьей) с точки зрения белого игрока, то ¬Шахматы - это та же игра с точки зрения черного игрока.
Параллельная конъюнкция ∧ («pand») и параллельная дизъюнкция ∨ («por») объединяют игры параллельным образом. Прогон A∧B или A∨B - это одновременная игра в двух конъюнктах. Машина выигрывает A∧B, если выигрывает их обоих. Автомат выигрывает A∨B, если выигрывает хотя бы один из них. Например, Chess∨¬Chess - это игра на двух досках, на одной белой и черной, и в которой задача машины - выиграть хотя бы на одной доске. Такую игру можно легко выиграть независимо от того, кто противник, копируя его ходы с одной доски на другую.
Оператор параллельной импликации → («пимпликация») определяется как A → B = ¬A∨B. Интуитивный смысл этой операции сводится к уменьшению B до A, т. Е. Решение A до тех пор, пока противник решает B.
Параллельные кванторы ∧(«pall») и ∨(«pexists») можно определить следующим образом: ∧xA (x) = A (0) ∧A (1) ∧A (2) ∧... и ∨xA (x) = A (0) ∨A (1))A (2) ∨.... Таким образом, это одновременные игры A (0), A (1), A (2),..., каждая на отдельной доске. Машина выигрывает ∧xA (x) (соответственно ∨xA (x)), если она выигрывает все (или некоторые) из этих игр.
Слепые кванторы ∀ («болтовня») и ∃ («блексисты»), с другой стороны, генерируют одноплатные игры. Запуск ∀xA (x) или ∃xA (x) - это одиночный запуск A. Машина выигрывает ∀xA (x) (соответственно ∃xA (x)), если такой запуск является выигранным запуском A (x) для всех (соответственно хотя бы одного) возможных значений x.
Все описанные до сих пор операторы ведут себя точно так же, как их классические аналоги, когда они применяются к элементарным (безходным) играм, и подтверждают те же принципы. Вот почему CoL использует те же символы для этих операторов, что и классическая логика. Однако, когда такие операторы применяются к неэлементарным играм, их поведение перестает быть классическим. Так, например, если p - элементарный атом, а P - атом общего вида, p → p∧p допустимо, а P → P∧P - нет. Однако принцип исключенного среднего P∨¬P остается в силе. Тот же принцип недействителен для всех трех видов дизъюнкции (выбор, последовательный и переключаемый).
Выбор дизъюнкции ⊔ («хор») игр A и B, обозначаемый A⊔B, - это игра, в которой для победы машина должна выбрать одну из двух дизъюнктов и затем выиграть в выбранный компонент. Последовательная дизъюнкция («сор») A ᐁ B начинается как A; он также заканчивается как A, если машина не выполняет "переключение", и в этом случае A прекращается, и игра возобновляется и продолжается как B. В переключающейся дизъюнкции ("tor") A⩛B машина может переключаться между A и B любое конечное число раз. У каждого оператора дизъюнкции есть двойная конъюнкция, полученная путем перестановки ролей двух игроков. Соответствующие кванторы могут быть дополнительно определены как бесконечные конъюнкции или дизъюнкции так же, как в случае параллельных кванторов. Каждая дизъюнкция сортировки также вызывает соответствующую операцию импликации так же, как это было в случае параллельной импликации →. Например, импликация выбора («химпликация») A⊐B определяется как ¬A⊔B.
Параллельное повторение ("предвестие") A можно определить как бесконечное параллельное соединение A∧A∧A∧... Последовательный ("повторение") и переключающийся ("повторение") виды повторений можно определить аналогично.
Операторы corecurrence можно определить как бесконечные дизъюнкции. Ветвление повторения ("прерывание") ⫰, которое является наиболее сильным типом повторения, не имеет соответствующей конъюнкции. ⫰ A - это игра, которая начинается и продолжается как A. Однако в любое время среде разрешается сделать «репликативный» ход, который создает две копии текущей позиции A, таким образом разделение игры на две параллельные нити с общим прошлым, но, возможно, с разными будущими событиями. Таким же образом среда может дополнительно реплицировать любую позицию любого потока, создавая, таким образом, все больше и больше потоков A. Эти потоки воспроизводятся параллельно, и машина должна выиграть A во всех потоках, чтобы стать победителем в ⫰ А. Повторяемость («повторение») ⫯ определяется симметрично путем замены «машина» и «среда».
Каждый вид повторения далее порождает соответствующую слабую версию импликации и слабую версию отрицания. Первое называется повторением, а второе - опровержением. Ветвящееся римпликация («бримпликация») A ⟜ B есть не что иное, как ⫰ A → B, а ветвящее опровержение («брефутация») A - это A ⟜ ⊥, где ⊥ - всегда проигрышная элементарная игра. Точно так же и со всеми остальными импликациями и опровержениями.
Язык CoL предлагает систематический способ определения бесконечного множества вычислительных задач, с именами, установленными в литературе, или без них. Ниже приведены некоторые примеры.
Пусть f - унарная функция. Задача вычисления f будет записана как ⊓x⊔y (y = f (x)). Согласно семантике CoL, это игра, в которой первый ход («ввод») делается средой, которая должна выбрать значение m для x. Интуитивно это равносильно тому, чтобы попросить машину сообщить значение f (m). Игра продолжается как ⊔y (y = f (m)). Теперь ожидается, что машина сделает ход («выход»), который должен выбрать значение n для y. Это означает, что n - это значение f (m). Теперь игра сводится к элементарному n = f (m), который выигрывает машина тогда и только тогда, когда n действительно является значением f (m).
Пусть p - унарный предикат. Тогда ⊓x (p (x) ⊔¬p (x)) выражает проблему принятия решения p, ⊓x (p (x) ᐁ ¬ p ( x)) выражает проблему полурешения p, а ⊓x (p (x) ⩛¬p (x)) - проблему рекурсивной аппроксимации p.
Пусть p и q - два унарных предиката. Тогда ⊓x (p (x) ⊔¬p (x)) ⟜⊓x (q (x) ⊔¬q (x)) выражает проблему редукции по Тьюрингу q к p ( в том смысле, что q сводится по Тьюрингу к p тогда и только тогда, когда интерактивная задача ⊓x (p (x) ⊔¬p (x)) ⟜⊓x (q (x) ⊔¬q (x)) является вычислимый). ⊓x (p (x) ⊔¬p (x)) →⊓x (q (x) ⊔¬q (x)) делает то же самое, но для более сильной версии редукции Тьюринга, где оракул для p может быть запрашивается только один раз. ⊓x⊔y (q (x) ↔p (y)) делает то же самое для задачи многие-один, сокращая q до p. С помощью более сложных выражений можно охватить все виды безымянных, но потенциально значимых отношений и операций над вычислительными задачами, таких как, например, «Тьюринг, сводящий проблему полурешения r к проблеме уменьшения числа единиц q до p». Наложение ограничений по времени или пространству на работу машины, дополнительно приводит к теоретико-сложным аналогам таких отношений и операций.
Известные дедуктивные системы для различных фрагментов CoL обладают тем свойством, что решение (алгоритм) может быть автоматически извлечено из доказательства проблемы в системе. Это свойство далее наследуется всеми прикладными теориями, основанными на этих системах. Итак, чтобы найти решение данной проблемы, достаточно выразить его на языке CoL, а затем найти доказательство этого выражения. Другой способ взглянуть на это явление - представить формулу G CoL как спецификацию (цель) программы. Тогда доказательство G - точнее, переводится в - программу, соответствующую этой спецификации. Нет необходимости проверять соответствие спецификации, потому что само доказательство фактически является такой проверкой.
Примерами прикладных теорий, основанных на CoL, являются так называемая кларифметика. Это теории чисел, основанные на CoL в том же смысле, в каком арифметика Пеано PA основана на классической логике. Такая система обычно является консервативным продолжением PA. Обычно он включает все аксиомы Пеано и добавляет к ним одну или две дополнительные аксиомы Пеано, такие как ⊓x⊔y (y = x '), выражающие вычислимость функции-преемника. Обычно в нем также есть одно или два нелогических правила вывода, таких как конструктивные версии индукции или понимания. Посредством обычных изменений таких правил можно получить надежные и полные системы, характеризующие тот или иной интерактивный класс вычислительной сложности C. Это в том смысле, что проблема принадлежит C тогда и только тогда, когда у нее есть доказательство в теории. Таким образом, такую теорию можно использовать для поиска не только алгоритмических решений, но и эффективных по запросу, таких как решения, которые выполняются за полиномиальное время или в логарифмическом пространстве. Следует отметить, что все кларифметические теории разделяют одни и те же логические постулаты, и только их нелогические постулаты меняются в зависимости от целевого класса сложности. Их заметная отличительная черта от других подходов с аналогичными целями (таких как ограниченная арифметика ) заключается в том, что они расширяют, а не ослабляют PA, сохраняя полную дедуктивную силу и удобство последнего.
