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

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

История

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

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

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

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

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

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

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

Формальные диалоги и игры GTS могут быть бесконечными и использовать правила окончания игры, а не позволять игрокам решать, когда прекратить игру. Достижение этого решения с помощью стандартных средств стратегических умозаключений ( повторное устранение доминирующих стратегий или IEDS) в GTS и формальных диалогах было бы эквивалентно решению проблемы остановки и превосходило бы мыслительные способности человеческих агентов. GTS позволяет избежать этого с помощью правила проверки формул на соответствие базовой модели; логические диалоги с правилом неповторения (аналог троекратного повторения в шахматах). Жено и Жако (2017) доказал, что игроки с сильно ограниченной рациональностью могут решить прекратить игру без СВУ.

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

Интуиционистская логика, денотационная семантика, линейная логика

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

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

Кванторы

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

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

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

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

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

См. также

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

Библиография

Книги

• Т. Ахо и А.В. Пиетаринен (ред.) Правда и игры. Очерки в честь Габриэля Санду . Феннические философские общества (2006). ISBN   951-9264-57-4 .
• Дж. ван Бентем, Г. Хайнцманн, М. Ребуски и Х. Виссер (ред.) Эпоха альтернативной логики . Спрингер (2006). ISBN   978-1-4020-5011-4 .
• Р. Инхетвен: Логика. Введение, ориентированное на диалог. , Лейпциг 2003 г. ISBN   3-937219-02-1
• Л. Кейфф Диалогический плюрализм . Диссертация Университета Лилля 3 (2007).
• К. Лоренц, П. Лоренцен: Диалогическая логика , Дармштадт, 1978 г.
• П. Лоренцен: Учебник конструктивной теории науки , Штутгарт, 2000 г. ISBN   3-476-01784-2
• О. Майер, А.-В. Пиетаринен и Т. Туленхеймо (редакторы). Игры: объединяем логику, язык и философию . Спрингер (2009).
• Рахман С. О диалоге протологических категорий и других редкостях . Франкфурт 1993 г. ISBN   3-631-46583-1
• С. Рахман и Х. Рюкерт (редакторы), Новые перспективы в диалогической логике . Синтез 127 (2001) ISSN   0039-7857 .
• С. Рахман и Н. Клербоут: Связывающие игры и конструктивная теория типов: диалогические стратегии, CTT-демонстрации и аксиома выбора . Спрингер-Брифы (2015). https://www.springer.com/gp/book/9783319190624 .
• С. Рахман, З. МакКонахи, А. Клев, Н. Клербоут: Имманентное рассуждение или равенство в действии. Пледойер для игрового уровня . Спрингер (2018). https://www.springer.com/gp/book/9783319911489 .
• Дж. Редмонд и М. Фонтейн, Как разыгрывать диалоги. Введение в диалогическую логику. Лондон, Публикации колледжа (Диалоги полковника и логические игры. Философская перспектива № 1). ( ISBN   978-1-84890-046-2 )

Статьи

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

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

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