Вычислимая логика

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

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

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

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

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

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

Язык

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

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

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

Семантика

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

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

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

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

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

Параллельный оператор импликации → («пимпликация») определяется формулой A → B = ¬ A ∨ B . Интуитивный смысл этой операции заключается сведении B к A , т.е. решении A до тех пор, пока противник решает B. в

Параллельные кванторы ∧ («палл») и ∨ («пексисты») могут быть определены как ∧ 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 , и выигрывает ∃ xA ( 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∧... Последовательные («srecurrence») и переключаемые («trecurrence») виды повторений могут быть определены аналогичным образом.

Операторы коркуррентности можно определить как бесконечные дизъюнкции. Ветвящееся повторение («brecurrence») ⫰ , которое является самым сильным видом повторения, не имеет соответствующего союза. ⫰ A — игра, которая начинается и продолжается 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 тогда и только тогда, когда она имеет теоретическое доказательство. Таким образом, такую ​​теорию можно использовать для поиска не только алгоритмических решений, но и эффективных решений по запросу, например решений, которые работают в полиномиальном времени или логарифмическом пространстве . Следует отметить, что все кларифметические теории имеют одни и те же логические постулаты, и только их нелогические постулаты различаются в зависимости от целевого класса сложности. Их примечательная отличительная черта от других подходов с аналогичными устремлениями (таких как ограниченная арифметика ) состоит в том, что они расширяют, а не ослабляют ПА, сохраняя полную дедуктивную силу и удобство последних.

См. также

• Семантика игры
• Интерактивные вычисления
• Логика
• Логика для вычислимости

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

• Домашняя страница вычислимой логики Всесторонний обзор предмета.
• Георгий Джапаридзе
• Семантика игры или линейная логика?
• Курс лекций по вычислимой логике
• О семантике абстрактных ресурсов и вычислительной логике Видеолекция Н. Верещагина.
• Обзор вычислимой логики (PDF). Загружаемый эквивалент домашней страницы, указанной выше.