Семантика игры

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

История [ править ]

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

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

Классическая логика [ править ]

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

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

В более общем смысле семантика игры может применяться к логике предикатов ; новые правила позволяют удалить доминирующий квантификатор его «владельцем» (верификатор для квантификаторов существования и фальсификатор для универсальных квантификаторов ) и заменять его связанную переменную во всех случаях на объект по выбору владельца, взятый из области квантификации . Обратите внимание, что один контрпример фальсифицирует универсально определенное количественное утверждение, а одного примера достаточно, чтобы проверить экзистенциально количественно определенное утверждение. Если исходить из выбранной аксиомы , теоретико-игровая семантика классической логики первого порядка согласуется с обычныммодельная (тарская) семантика . Для классической логики первого порядка выигрышная стратегия верификатора, по сути, состоит в нахождении адекватных сколемовских функций и свидетелей . Например, если S обозначает, то справедливо выполнимое утверждение для S равно . Функция Сколема f (если она существует) фактически кодирует выигрышную стратегию для Проверяющего S , возвращая свидетельство экзистенциальной подформулы для каждого выбора x, который может сделать Фальсификатор. ^[1]${\ Displaystyle \ forall х \ существует у \, \ фи (х, у)}$${\ Displaystyle \ существует f \ forall x \, \ phi (x, f (x))}$

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

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

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

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

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

Квантификаторы [ править ]

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

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

Логика вычислимости [ править ]

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

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

См. Также [ править ]

• Логика вычислимости
• Логика зависимости
• Игра Эренфойхта – Фраиссе
• Дружественная к независимости логика
• Интерактивные вычисления
• Интуиционистская логика
• Ludics

Ссылки [ править ]

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

Библиография [ править ]

Книги [ править ]

• Т. Ахо и А.В. Pietarinen (ред.) Правда и игры. Очерки в честь Габриэля Санду . 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 .
• С. Рахман, З. МакКонахи, А. Клев, Н. Клербау: Имманентное рассуждение или равенство в действии. Plaidoyer для уровня 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 ) 

Статьи [ править ]

• С. Абрамский и Р. Jagadeesan, Игры и полная полнота для мультипликативной линейной логики . Журнал символической логики 59 (1994): 543-574.
• А. Бласс, Семантика игры для линейной логики . Анналы чистой и прикладной логики 56 (1992): 151-166.
• Д. Р. Гика, Приложения семантики игр: от анализа программ к синтезу оборудования . 2009 24-й ежегодный симпозиум IEEE по логике в компьютерных науках: 17-26. ISBN 978-0-7695-3746-7 . 
• Джапаридзе Г. Введение в логику вычислимости . Анналы чистой и прикладной логики 123 (2003): 1-99.
• Г. Джапаридзе, По началу была игровая семантика . В Ондрей Майер, Ахти-Вейкко Пиетаринен и Теро Туленхеймо (редакторы), Игры: объединяющая логика, язык и философия . Спрингер (2009).
• Krabbe, ECW, 2001. « Основы диалога: восстановленная логика диалога [название было напечатано с опечаткой как« ... пересмотренное »],« Приложение к Трудам Аристотелевского общества 75 : 33-49.
• Х. Никау (1994). «Наследственно последовательные функционалы». В А. Нероде; Ю.В. Матиясевич (ред.). Proc. Symp. Логические основы информатики: логика в Санкт-Петербурге . Конспект лекций по информатике. 813 . Springer-Verlag . С. 253–264. DOI : 10.1007 / 3-540-58140-5_25 .
• де Кейро, Р. (1988). «Теоретическое доказательство программирования и роль правил редукции» . Диалектика . 42 (4): 265–282. DOI : 10.1111 / j.1746-8361.1988.tb00919.x .
• де Кейро, Р. (1991). «Смысл как грамматика плюс последствия» . Диалектика . 45 (1): 83–86. DOI : 10.1111 / j.1746-8361.1991.tb00979.x .
• де Кейро, Р. (1994). «Нормализация и языковые игры» . Диалектика . 48 (2): 83–123. DOI : 10.1111 / j.1746-8361.1994.tb00107.x .
• де Кейро, Р. (2001). «Значение, функция, цель, полезность, последствия - взаимосвязанные понятия» . Логический журнал IGPL . 9 (5): 693–734. DOI : 10.1093 / jigpal / 9.5.693 .
• де Кейруш, Р. (2008). «О правилах редукции, значении как использовании и теоретико-доказательной семантике» . Studia Logica . 90 (2): 211–247. DOI : 10.1007 / s11225-008-9150-5 . S2CID  11321602 .
• С. Рахман и Л. Кейфф, О том , как быть диалогистом . В книге Дэниела Вандеркена (редактор), « Логическая мысль и действие» , Springer (2005), 359-408. ISBN 1-4020-2616-1 . 
• С. Рахман и Т. Туленхеймо, От игр к диалогам и обратно: на пути к общей структуре действительности . В Ондрей Майер, Ахти-Вейкко Пиетаринен и Теро Туленхеймо (редакторы), Игры: объединяющая логика, язык и философия . Спрингер (2009).
• Йохан ван Бентем (2003). «Логика и теория игр: близкие встречи третьего рода». В GE Mints; Рейнхард Маскенс (ред.). Игры, логика и конструктивные наборы . Публикации CSLI. ISBN 978-1-57586-449-5.

Внешние ссылки [ править ]

• Домашняя страница Computability Logic
• GALOP: Мастерская по играм для логики и языков программирования
• Семантика игр или линейная логика?
• Томас Пьеха. «Диалогическая логика» . Интернет-энциклопедия философии .
• Статья Уилфрида Ходжеса «Логика и игры» в Стэнфордской энциклопедии философии
• Запись Лорана Кейффа "Dialogical Logic" в Стэнфордской энциклопедии философии