Войти
Семантика игры (немецкий : dialogische Logik, переводится как диалогическая логика ) - это подход к формальной семантике, который основывает концепции истины или достоверности на теоретико-игровых концепциях, таких как существование выигрышная стратегия для игрока, чем-то напоминающая сократические диалоги или средневековую теорию обязательств.
В конце 1950-х годов Пол Лоренцен был первым, кто ввел игровую семантику для логики, и ее развил Куно Лоренц. Почти одновременно с Лоренценом Яакко Хинтикка разработал теоретико-модельный подход, известный в литературе как GTS (теоретико-игровая семантика). С тех пор в логике изучается ряд различных семантик игр.
Шахид Рахман (Лилль) и его сотрудники развили диалогическую логику в общую основу для изучения логических и философских вопросов, связанных с логическим плюрализмом. Начиная с 1994 года это вызвало своего рода возрождение с долгосрочными последствиями. Этот новый философский импульс претерпел параллельное обновление в областях теоретической информатики, вычислительной лингвистики, искусственного интеллекта и формальной семантики языков программирования., например, работа Йохана ван Бентема и его сотрудников в Амстердаме, которые тщательно изучили интерфейс между логикой и играми, и Ханно Никау, который рассмотрел проблему полной абстракции в программировании. языки с помощью игр. Новые результаты в линейной логике от Жана-Ива Жирара в интерфейсах между математической теорией игр и логикой с одной стороны и теорией аргументации и логика же привела к работам многих других, в том числе С. Абрамский, Я. ван Бентем, А. Бласс, Д. Габбай, М. Хайленд, У. Ходжес, Р. Джагадисан, Г. Джапаридзе, Э. Краббе, Л. Онг, Х. Праккен, Г. Санду, Д. Уолтон и Дж. Вудс, которые поместили семантику игр в центр новой концепции логики, в которой логика понимается как динамический инструмент вывода.
Простейшее применение семантики игры - логика высказываний. Каждая формула этого языка интерпретируется как игра между двумя игроками, известная как «Проверяющий» и «Фальсификатор». Верификатору дается «право собственности» на все дизъюнкции в формуле, а фальсификатору также дается право владения всеми конъюнкциями. Каждый ход игры заключается в том, чтобы позволить владельцу доминирующего соединительного элемента выбрать одну из его ветвей; затем игра будет продолжена в этой подформуле, и любой игрок, контролирующий ее доминирующую связку, сделает следующий ход. Игра заканчивается, когда два игрока сделали такое примитивное предложение; на этом этапе Проверяющий считается победителем, если результирующее предложение истинно, а Фальсификатор считается победителем, если оно ложно. Исходная формула будет считаться истинной именно тогда, когда Проверяющий имеет выигрышную стратегию , в то время как она будет ложной, когда Фальсификатор имеет выигрышную стратегию.
Если формула содержит отрицания или импликации, можно использовать другие, более сложные методы. Например, отрицание должно быть истинным, если отрицание ложно, поэтому оно должно иметь эффект смены ролей двух игроков.
В более общем смысле семантика игры может применяться к логике предиката ; новые правила позволяют удалить доминирующий квантификатор его "владельцем" (верификатор для экзистенциальных кванторов и фальсификатор для универсальных кванторов ) и его связанная переменная заменяется во всех случаях объектом по выбору владельца, взятым из области количественной оценки. Обратите внимание, что один контрпример фальсифицирует универсально определенное количественное утверждение, а одного примера достаточно, чтобы проверить экзистенциально количественно определенное. Принимая аксиому выбора , теоретико-игровая семантика для классической логики первого порядка согласуется с обычной семантикой, основанной на моделях (тарскианской). Для классической логики первого порядка выигрышная стратегия верификатора по существу состоит в нахождении адекватных функций Сколема и свидетелей. Например, если S обозначает 
Приведенное выше определение было первым сформулирован Яакко Хинтиккой как часть его интерпретации GTS. Первоначальная версия игровой семантики для классической (и интуиционистской) логики, разработанная Полом Лоренценом и Куно Лоренцем, была определена не в терминах моделей, а в терминах выигрышных стратегий над формальными диалогами (П. Лоренцен, К. Лоренц 1978, С. Рахман и Л. Кейфф 2005). Шахид Рахман и Теро Туленхеймо разработали алгоритм для преобразования выигрышных GTS стратегий классической логики в диалогические выигрышные стратегии и наоборот.
Для наиболее распространенных логик, включая приведенные выше, игры, которые возникают из них, имеют точную информацию, то есть два игрока всегда знают значения истинности каждый примитив и знает обо всех предыдущих ходах в игре. Однако с появлением игровой семантики были предложены логики, такие как независимая логика Хинтикки и Санду, с естественной семантикой в терминах игр с несовершенной информацией.
Первичной мотивацией для Лоренцена и Куно Лоренца было найти теоретико-игровую концепцию (их термин был диалогическим, в немецком [de ]) семантика для интуиционистской логики. Андреас Бласс первым указал на связь между семантикой игры и линейной логикой. Эта линия была далее развита Самсоном Абрамски и независимо Мартином Хайландом и, которые уделяли особое внимание композиционности, то есть определению стратегий индуктивно на синтаксисе. Используя семантику игры, упомянутые выше авторы решили давнюю проблему определения полностью абстрактной модели для языка программирования PCF. Следовательно, семантика игр привела к полностью абстрактным семантическим моделям для множества языков программирования, а также к новым семантически-направленным методам верификации программного обеспечения с помощью программ проверка моделей.
[fr ], а Хельге Рюкерт расширил диалогические подход к изучению нескольких неклассических логик, таких как модальная логика, логика релевантности, свободная логика и связная логика. Недавно Рахман и его сотрудники развили диалогический подход в общую структуру, направленную на обсуждение логического плюрализма.
Основополагающие аспекты семантики игры были больше подчеркнуты Яакко Хинтиккой и Габриэлем Санду, особенно для независимой логики (IF logic, в последнее время дружественная к информации логика), логика с кванторами ветвления. Считалось, что принцип композиционности не работает для этих логик, поэтому тарскианское определение истины не могло обеспечить подходящую семантику. Чтобы обойти эту проблему, кванторам было придано теоретико-игровое значение. В частности, подход такой же, как и в классической логике высказываний, за исключением того, что игроки не всегда имеют точную информацию о предыдущих ходах другого игрока. Уилфрид Ходжес предложил композиционную семантику и доказал, что она эквивалентна игровой семантике для IF-логик.
Совсем недавно [fr ] и команда диалогической логики в Лилле реализовали зависимости и независимости в рамках диалогической структуры посредством диалогического подхода к интуиционистской теории типов, названной имманентное рассуждение.
логика вычислимости Джапаридзе - это игровой семантический подход к логике в крайнем смысле, рассматривающий игры как цели, которые должны обслуживаться логикой а не как техническое или основное средство изучения или обоснования логики. Его исходный философский пункт состоит в том, что логика предназначена быть универсальным, универсальным интеллектуальным инструментом для `` навигации в реальном мире '' и, как таковая, ее следует истолковывать семантически, а не синтаксически, потому что именно семантика служит мостом между реальный мир и бессмысленные формальные системы (синтаксис). Таким образом, синтаксис вторичен и интересен только в той мере, в какой он обслуживает базовую семантику. С этой точки зрения Джапаридзе неоднократно критиковал часто применяемую практику подгонки семантики к некоторым уже существующим целевым синтаксическим конструкциям, примером чего может служить подход Лоренцена к интуиционистской логике. Затем эта линия мысли утверждает, что семантика, в свою очередь, должна быть семантикой игры, поскольку игры «предлагают наиболее полные, последовательные, естественные, адекватные и удобные математические модели для самой сути всех« навигационных »действий агентов. : их взаимодействие с окружающим миром ». Соответственно, парадигма построения логики, принятая в логике вычислимости, заключается в том, чтобы идентифицировать наиболее естественные и базовые операции в играх, рассматривать эти операторы как логические операции, а затем искать надежные и полные аксиоматизации наборов семантически валидных формул. На этом пути появилось множество знакомых или незнакомых логических операторов открытого языка логики вычислимости с несколькими видами отрицаний, союзов, дизъюнкций, импликаций, квантификаторов и модальностей.
В игры играют между двумя агентами: машиной и ее средой, где от машины требуется следовать только эффективным стратегиям. Таким образом, игры рассматриваются как интерактивные вычислительные задачи, а выигрышные стратегии машины - как решения этих проблем. Было установлено, что логика вычислимости устойчива по отношению к разумным вариациям сложности разрешенных стратегий, которые могут быть уменьшены до логарифмического пространства и полиномиального времени (одно не подразумевает другого в интерактивных вычислениях), не влияя на логику. Все это объясняет название «логика вычислимости» и определяет применимость в различных областях информатики. Классическая логика, независимая логика и некоторые расширения линейной и интуиционистской логики оказываются особыми фрагментами логики вычислимости, полученной просто запретив определенные группы операторов или атомов.
