Семантика игры - Game semantics

Семантика
Вычисление
Типы
Теория
Анализ
Приложения

Семантика игры ( немецкий : dialogische Logik , переводится как диалогическая логика ) - это подход к формальной семантике, который основывает концепции истины или валидности на теоретико-игровых концепциях, таких как существование выигрышной стратегии для игрока, чем-то напоминающей диалоги Сократа или средневековая теория обязательств .

История

В конце 1950-х Пол Лоренцен первым ввел игровую семантику для логики , и ее развил Куно Лоренц . Почти одновременно с Лоренценом Яакко Хинтикка разработал теоретико-модельный подход, известный в литературе как GTS (теоретико-игровая семантика). С тех пор в логике изучается ряд различных семантик игр.

Шахид Рахман (Лилль) и его сотрудники развили диалогическую логику в общую основу для изучения логических и философских вопросов, связанных с логическим плюрализмом. Начиная с 1994 г. это вызвало своего рода возрождение с долгосрочными последствиями. Этот новый философский импульс претерпел параллельное обновление в областях теоретической информатики , вычислительной лингвистики , искусственного интеллекта и формальной семантики языков программирования , например, работы Йохана ван Бентема и его сотрудников в Амстердаме, которые тщательно изучили взаимосвязь между логикой. и игры, и Ханно Никау, который решил проблему полной абстракции в языках программирования с помощью игр. Новые результаты в линейных логиках от Жан-Ив Жирар в интерфейсах между математической теорией игр и логикой с одной стороны , и теорией аргументации и логикой, с другой стороны , в результате работы многих других, в том числе С. Абрамского , Й. ван Бентемого, А Бласс , Д. Габбей , М. Хайленд , В. Ходжес , Р. Джагадисан, Г. Джапаридзе , Э. Краббе, Л. Онг, Х. Праккен, Г. Санду, Д. Уолтон и Дж. Вудс, которые разместили семантика игры в центре новой концепции логики, в которой логика понимается как динамический инструмент вывода. Существовала также альтернативная точка зрения на теорию доказательств и теорию значения, отстаивающую, что парадигма Витгенштейна «значение как использование», понимаемая в контексте теории доказательств, где так называемые правила редукции (демонстрирующие влияние правил исключения на результат правила введения) следует рассматривать как подходящие для формализации объяснения (непосредственных) последствий, которые можно извлечь из предложения, тем самым показывая функцию / цель / полезность его главной связки в исчислении языка ( de Queiroz (1988) , де Кейруш (1991) , де Кейрос (1994) , де Кейруш (2001) , де Кейрос (2008) )

Классическая логика

Самым простым приложением семантики игры является логика высказываний . Каждая формула этого языка интерпретируется как игра между двумя игроками, известная как «Проверяющий» и «Фальсификатор». Проверяющему дается «владение» всеми дизъюнкциями в формуле, а фальсификатору также дается право собственности на все конъюнкции . Каждый ход игры заключается в том, чтобы позволить владельцу доминирующего соединительного элемента выбрать одну из его ветвей; затем игра будет продолжена в этой подформуле, и любой игрок, контролирующий ее доминирующую связку, сделает следующий ход. Игра заканчивается, когда два игрока сделали такое примитивное предложение; на этом этапе Проверяющий считается победителем, если результирующее предложение истинно, а Фальсификатор считается победителем, если оно ложно. Исходная формула будет считаться верной именно тогда, когда у Проверяющего есть выигрышная стратегия , а она будет ложной, когда у Фальсификатора есть выигрышная стратегия.

Если формула содержит отрицания или импликации, можно использовать другие, более сложные методы. Например, отрицание должно быть истинным, если отрицание ложно, поэтому оно должно иметь эффект смены ролей двух игроков.

В более общем смысле семантика игры может применяться к логике предикатов ; новые правила позволяют удалить доминирующий квантификатор его «владельцем» (верификатор для квантификаторов существования и фальсификатор для универсальных квантификаторов ) и заменять его связанную переменную во всех случаях на объект по выбору владельца, взятый из области квантификации . Обратите внимание, что один контрпример фальсифицирует универсально определенное количественное утверждение, а одного примера достаточно, чтобы проверить экзистенциально количественно определенное утверждение. Предполагая , что аксиому выбора , игра-теоретической семантика для классической логики первого порядка совпадает с обычной модельной (Тарской) семантикой . Для классической логики первого порядка выигрышная стратегия верификатора, по сути, состоит в нахождении адекватных сколемовских функций и свидетелей . Например, если S обозначает, то справедливо выполнимое утверждение для S равно . Функция Сколема f (если она существует) фактически кодирует выигрышную стратегию для Проверяющего S , возвращая свидетельство экзистенциальной подформулы для каждого выбора x, который может сделать Фальсификатор.

Приведенное выше определение было впервые сформулировано Яакко Хинтиккой как часть его интерпретации GTS. Первоначальная версия игровой семантики для классической (и интуиционистской) логики, разработанная Полом Лоренценом и Куно Лоренцем, была определена не в терминах моделей, а в терминах выигрышных стратегий над формальными диалогами (П. Лоренцен, К. Лоренц 1978, С. Рахман и Л. Кейфф 2005). Шахид Рахман и Теро Туленхеймо разработали алгоритм для преобразования выигрышных в GTS стратегий классической логики в диалогические выигрышные стратегии и наоборот.

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

Интуиционистская логика, денотационная семантика, линейная логика, логический плюрализм

Основная мотивация для Лоренсена и Куно Лоренца была найти теоретико-игровую (их термин был диалогическим , на немецком языке Dialogische Logik  [ де ] ) семантики для интуиционистской логики . Андреас Бласс первым указал на связь между семантикой игры и линейной логикой . Эта линия получила дальнейшее развитие Samson Абрамского , Radhakrishnan Jagadeesan , Pasquale Malacaria и независимо друг от друга Мартин Хайленд и Люк Онг , который сделал особый акцент на композиционности, т.е. определение стратегий индуктивно по синтаксису. Используя семантику игры, упомянутые выше авторы решили давнюю проблему определения полностью абстрактной модели для языка программирования PCF . Следовательно, семантика игр привела к полностью абстрактным семантическим моделям для множества языков программирования и к новым семантически-направленным методам проверки программного обеспечения с помощью проверки модели программного обеспечения .

Шахид Рахман  [ фр ] и Хельге Рюкерт расширили диалогический подход на изучение нескольких неклассических логик, таких как модальная логика , логика релевантности , свободная логика и связная логика . Недавно Рахман с соавторами развили диалогический подход в общую структуру, направленную на обсуждение логического плюрализма.

Квантификаторы

Основополагающие соображения семантики игр были больше подчеркнуты Яакко Хинтиккой и Габриэлем Санду, особенно для логики, ориентированной на независимость (логика IF, в последнее время логика, ориентированная на информацию ), логики с кванторами ветвления . Считалось, что принцип композиционности не подходит для этих логик, так что определение истины Тарского не могло обеспечить подходящую семантику. Чтобы обойти эту проблему, кванторам было придано теоретико-игровое значение. В частности, подход такой же, как и в классической логике высказываний, за исключением того, что игроки не всегда имеют точную информацию о предыдущих ходах другого игрока. Уилфрид Ходжес предложил композиционную семантику и доказал, что она эквивалентна семантике игр для IF-логик.

Совсем недавно Шахид Рахман  [ фр ] и команда диалогической логики в Лилле реализовали зависимости и независимости в рамках диалогической структуры посредством диалогического подхода к интуиционистской теории типов, называемого имманентным рассуждением .

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

Джапаридзе «ы Вычислимость логика игра-семантический подход к логике в крайнем смысле, рассматривая игры в качестве мишеней , которые будут обслуживаться с помощью логики , а не в качестве технических средств или основополагающих для изучения или обоснования логики. Его исходная философская точка зрения состоит в том, что логика предназначена быть универсальным, универсальным интеллектуальным инструментом для `` навигации по реальному миру '' и, как таковая, ее следует истолковывать семантически, а не синтаксически, потому что именно семантика служит мостом между реальный мир и бессмысленные формальные системы (синтаксис). Таким образом, синтаксис вторичен и интересен только в той мере, в какой он обслуживает базовую семантику. С этой точки зрения, Джапаридзе неоднократно критиковал часто следует практику регулирования семантики некоторых уже существующих целевых синтаксические конструкции, с Lorenzen подходом «s к интуиционистской логике быть примером. Затем эта линия мысли утверждает, что семантика, в свою очередь, должна быть семантикой игры, потому что игры «предлагают наиболее полные, последовательные, естественные, адекватные и удобные математические модели для самой сути всех« навигационных »действий агентов. : их взаимодействие с окружающим миром ». Соответственно, парадигма построения логики, принятая логикой вычислимости, состоит в том, чтобы идентифицировать наиболее естественные и базовые операции в играх, рассматривать эти операторы как логические операции, а затем искать надежные и полные аксиоматизации наборов семантически валидных формул. На этом пути появилось множество знакомых или незнакомых логических операторов открытого языка логики вычислимости с несколькими видами отрицаний, союзов, дизъюнкций, импликаций, квантификаторов и модальностей.

В игры играют между двумя агентами: машиной и ее средой, где от машины требуется следовать только эффективным стратегиям. Таким образом, игры рассматриваются как интерактивные вычислительные задачи, а выигрышные стратегии машины - как решения этих проблем. Было установлено, что логика вычислимости устойчива по отношению к разумным вариациям сложности разрешенных стратегий, которые могут быть уменьшены до логарифмического пространства и полиномиального времени (одно не подразумевает другого в интерактивных вычислениях), не влияя на логику. Все это объясняет название «логика вычислимости» и определяет применимость в различных областях информатики. Классическая логика , независимая логика и некоторые расширения линейной и интуиционистской логики оказываются особыми фрагментами логики вычислимости, получаемыми просто путем запрета определенных групп операторов или атомов.

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

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

Список используемой литературы

Книги

  • Т. Ахо и А.В. Пьетаринен (ред.) Правда и игры. Очерки в честь Габриэля Санду . Societas Philosophica Fennica (2006). ISBN  951-9264-57-4 .
  • Дж. Ван Бентем, Г. Хайнцманн, М. Ребуши и Х. Виссер (ред.) Эпоха альтернативной логики . Спрингер (2006). ISBN  978-1-4020-5011-4 .
  • Р. Инхетвин: Логик . Eine dialog-orientierte Einführung. , Лейпциг 2003 ISBN  3-937219-02-1
  • Л. Кейфф Le Pluralisme Dialogique . Диссертация Université de Lille 3 (2007).
  • К. Лоренц, П. Лоренцен: Dialogische Logik , Дармштадт 1978 г.
  • П. Лоренцен: Lehrbuch der konstruktiven Wissenschaftstheorie , Штутгарт 2000 ISBN  3-476-01784-2
  • О. Майер, А.-В. Пьетаринен и Т. Туленхеймо (редакторы). Игры: объединяющая логику, язык и философию . Спрингер (2009).
  • С. Рахман, Über Dialogue protologische Kategorien und andere Seltenheiten . Франкфурт 1993 ISBN  3-631-46583-1
  • С. Рахман и Х. Рюкерт (редакторы), Новые перспективы в диалогической логике . Synthese 127 (2001) ISSN  0039-7857 .
  • С. Рахман и Н. Клербау: Связывание игр и теории конструктивного типа: диалогические стратегии, CTT-демонстрации и аксиома выбора. Трусы Springer (2015). https://www.springer.com/gp/book/9783319190624 .
  • С. Рахман, З. МакКонахи, А. Клев, Н. Клербау: Имманентное рассуждение или равенство в действии. Плайдойер для уровня Play . Спрингер (2018). https://www.springer.com/gp/book/9783319911489 .
  • Дж. Редмонд и М. Фонтейн, Как играть в диалоги. Введение в диалоговую логику. Лондон, College Publications (Col. Dialogues and the Games of Logic. A Philosophical Perspective N ° 1). ( ISBN  978-1-84890-046-2 )

Статьи

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