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

Все ссылки в этой статье принадлежат исключительно одному автору, Г. Джапаридзе. Соответствующее обсуждение можно найти на странице обсуждения . Пожалуйста, помогите улучшить эту статью, добавив ссылки на дополнительные источники . Найти источники:  "Computability logic" – новости  · газеты  · книги  · ученый  · JSTOR ( май 2020 г. )

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

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

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

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

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

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

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

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

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

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

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

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

Оператор параллельной импликации → («pimplication») определяется как 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 ), если она выигрывает некоторые.

С другой стороны, слепые квантификаторы ∀ («blall») и ∃ («blexists») генерируют однодосочные игры. Серия ∀ 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 остается действительным. Тот же принцип недействителен для всех трех других видов дизъюнкции (выбор, последовательный и переключение).

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

Параллельное повторение («предтеча») A можно определить как бесконечную параллельную конъюнкцию A ∧A∧A∧... Последовательное («srecurrence») и переключающееся («trecurrence») виды повторений можно определить аналогичным образом.

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

Каждый вид повторения далее индуцирует соответствующую слабую версию импликации и слабую версию отрицания. Первая называется rimplication , а вторая — опровержением . Разветвленная rimplication («brimplication») A ⟜ B есть не что иное, как ⫰ A → B , а разветвленное опровержение («brefutation») A есть A ⟜ ⊥, где ⊥ — всегда проигранная элементарная игра. Аналогично для всех других видов rimplication и опровержения.

Язык 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, сохраняя полную дедуктивную силу и удобство последнего.

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

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