Игра Эренфойхта — Фраиса (Nijg |jyuskw]mg — Sjgnvg)

Перейти к навигации Перейти к поиску

Игры Эренфойхта — Фраиса (иногда челночные игры англ. back-and-forth games) — это техника определения, являются ли две структуры[англ.] элементарно эквивалентными[англ.]. Основное приложение игр Эренфойхта — Фраиса — доказательство невозможности выразить определённые свойства в логике первого порядка. Более того, игры Эренфойхта — Фраиса дают полную методологию для доказательства невозможности выразить свойства в логике первого порядка. В такой роли эти игры особенно важны в теории конечных моделей[англ.] и её приложениях в информатике (особенно в компьютерной верификации[англ.] и теории баз данных[англ.]), поскольку игры Эренфойхта — Фраиса являются одной из немногочисленных техник в теории моделей, которые остаются верными в контексте конечных моделей. Другие широко используемые техники для доказательства невозможности выразить свойства, такие как теорема о компактности, не работает для конечных моделей.

Игры, подобные игре Эренфойхта — Фраиса, могут быть также определены для других логик, таких как логик фиксированной точки[англ.][1] и фишечные игры для логик с конечным числом переменных. Расширения достаточно мощны, чтобы описать определимость в экзистенциальной логике второго порядка.

Основная идея

[править | править код]

Основная идея игры заключается в том, что мы имеем две структуры и два игрока (определены ниже). Один из игроков хочет показать, что эти две структуры отличны, в то время как другой игрок хочет показать, что они элементарно эквивалентны[англ.] (удовлетворяют тем же предложения первого порядка). Игра ведётся поочерёдно по раундам. Раунд протекает следующим образом: Сначала первый игрок Новатор[2] выбирает любой элемент из одной из структур, а другой игрок выбирает элемент из другой структуры. Целью второго игрока всегда является выбор элемента, который «похож» на элемент, выбранный Новатором. Второй игрок (Консерватор) выигрывает, если существует изоморфизм между выбранными элементами в двух различных структурах.

Игра завершается за фиксированное число шагов () (ординал, но обычно конечное число или ).

Определение

[править | править код]

Предположим, что нам даны две структуры and с одинаковыми множеством отношений символов и дано фиксированное натуральное число n. Мы можем тогда определить игру Эренфойхта — Фраиса как игру между двумя игроками, Новатором и Консерватором, следующим образом:

  1. Первый игрок, Новатор, выбирает либо члена структуры , или члена структуры .
  2. Если Новатор выбирает члена структуры , Консерватор выбирает члена структуры . В противном случае Консерватор выбирает члена структуры .
  3. Новатор выбирает либо члена структуры или члена структуры .
  4. Консерватор выбирает элемент или в модели, из которой Новатор не выбирал.
  5. Новатор и Консерватор продолжают выбирать члены из структур и ещё на шагах.
  6. Под конец игры мы выбрали различные элементы структуры и структуры . Мы поэтому имеем две структуры на множестве , одна получена из структуры отображением в , а другая получена из отражением в . Консерватор выигрывает, если эти структуры одинаковы. Новатор выигрывает, если они не одинаковы.

Для любого n мы определяем отношение , если Консерватор выигрывает в игре с n ходами . Это все отношения эквивалентности на классе структур с заданными символами отношений. Пересечение всех этих отношений снова является отношением эквивалентности .

Легко доказать, что если Консерватор выигрывает игру для всех n, то есть , то и элементарно эквивалентны. Если множество отношений символов конечно, обратное тоже верно.

Челночный метод[англ.] (или метод подбора), использованный в игре Эренфойхта — Фраиса для проверки элементарной эквивалентности предложил Роланд Фрейсе[англ.] в своей диссертации[3][4]. Метод сформулировал в виде игры Анджей Эренфойхт[англ.][5]. Названия Spoiler и Duplicator дал Joel Spencer[6]. Также используются названия Eloise и Abelard (и обозначаются часто и ) по именам Элоиза и Абеляр, по схеме именований, предложенной Вильфридом Ходжисом[англ.] в его книге Теория моделей.

Литература для дальнейшего чтения

[править | править код]

Глава 1 книги Пуазы по теории моделей[7] содержат введение в игру Эренфойхта — Фраиса. Главы 6, 7 и 13 книги Розенштейна о линейных порядках[8] также содержит введение в игру. Простые примеры игры Эренфойхта — Фраиса есть в одной из колонок MathTrek Иварса Петерсона[9].

Введение в игру Эренфойхта — Фраиса и некоторые простые примеры этой игры можно найти в книге Верещагина и Шеня[10].

Слайды Фокион Колайтиса[11] и глава книги Нейла Иммермана[12] об играх Эренфойхта — Фраиса обсуждают приложения в информатике, методологической теореме для доказательства невыразимости и некоторые простые доказательства невыразимости с помощью этой методологии.

Примечания

[править | править код]
  1. Bosse, 1993, с. 100–114.
  2. Используется терминология из книги Верещагина и Шеня (Верещагин, Шень 2008). В английском варианте Новатор=Spoiler, Консерватор=Duplicator. В книге игра называется игрой Эренфойхта и приведено несколько примеров простых игр для понимания идеи.
  3. Fraïssé, 1950, с. 1022-1024.
  4. Fraïssé, 1954, с. 35-182.
  5. Ehrenfeucht, 1961, с. 129-141.
  6. Stanford Encyclopedia of Philosophy, entry on Logic and Games. Дата обращения: 1 апреля 2019. Архивировано 2 декабря 2020 года.
  7. Poizat, 2000.
  8. Rosenstein, 1982.
  9. Пример игры Эренфойхта — Фраиса. Дата обращения: 1 апреля 2019. Архивировано 1 апреля 2019 года.
  10. Верещагин, Шень, 2008.
  11. Course on combinatorial games in теории конечных моделей by Phokion Kolaitis
  12. Immerman, 1999, с. Chapter 6.

Литература

[править | править код]
  • Верещагин Н. К., Шень А. Лекции по математической логике и теории алгоритмов. Часть 2. Языки исчисления.. — Москва, 2008. — С. 143. — ISBN 978-5-94057-322-7.
  • Uwe Bosse. An Ehrenfeucht–Fraïssé game for fixpoint logic and stratified fixpoint logic // Computer Science Logic: 6th Workshop, CSL'92, San Miniato, Italy, September 28 - October 2, 1992. Selected Papers / Egon Börger. — Springer-Verlag, 1993. — Т. 702. — С. 100–114. — (Lecture Notes in Computer Science). — ISBN 3-540-56992-8.
  • Roland Fraïssé. Sur une nouvelle classification des systèmes de relations // Comptes Rendus. — 1950. — Вып. 230.
  • Roland Fraïssé. Sur quelques classifications des systèmes de relations. — Paris, 1953. — (thesis). Опубликовано в
    • Roland Fraïssé. Publications Scientifiques de l'Université d'Alger. — 1954. — (series A).
  • Ehrenfeucht A. {{{заглавие}}} // Fundamenta Mathematicae. — 1961. — Вып. 49.
  • Bruno Poizat. A Course in Model Theory / tr. Moses Klein. — New York: Springer-Verlag, 2000.
  • Joseph G. Rosenstein. Linear Orderings. — New York: Academic Press, 1982.
  • Neil Immerman. chapter 6 // Descriptive complexity. — Springer, 1999. — ISBN 978-0-387-98600-5.
  • Erich Grädel, Phokion G. Kolaitis, Leonid Libkin, Marx Maarten, Joel Spencer, Moshe Y. Vardi, Yde Venema, Scott Weinstein. Finite model theory and its applications. — Berlin: Springer-Verlag, 2007. — (Texts in Theoretical Computer Science. An EATCS Series). — ISBN 978-3-540-00428-8.