С2С (математика)

В математике S2S — это монадическая теория второго порядка с двумя преемниками. Это одна из наиболее выразительных известных естественных разрешимых теорий, многие из которых можно интерпретировать в S2S. Ее разрешимость была доказана Рабиным в 1969 году.

Основные свойства

Объектами первого порядка S2S являются конечные двоичные строки. Объекты второго порядка представляют собой произвольные наборы (или унарные предикаты) конечных двоичных строк. S2S имеет функции s → s 0 и s → s 1 на строках, а также предикат s ∈ S (эквивалентно S ( s что строка s принадлежит множеству S. )), означающий ,

Некоторые свойства и соглашения:

• По умолчанию строчные буквы относятся к объектам первого порядка, а прописные — к объектам второго порядка.
• Включение наборов делает S2S вторым порядком, причем «монадический» указывает на отсутствие k -арных переменных-предикатов для k > 1.
• Объединение строк s и t обозначается st и обычно недоступно в S2S, даже s →0 s . Префиксное отношение между строками можно определить.
• Равенство является примитивным, или его можно определить как s = t ⇔ ∀ S ( S ( s ) ⇔ S ( t )) и S = ​​T ⇔ ∀ s ( S ( s ) ⇔ T ( s )).
• Вместо строк можно использовать (например) натуральные числа с n → 2 n +1 и n → 2 n +2, но без других операций.
• Набор всех двоичных строк обозначается {0,1} ^* , используя звезду Клини .
• Произвольные подмножества {0,1} ^* иногда отождествляются с деревьями, в частности, как дерево с меткой {0,1} {0,1} ^* ; {0,1} ^* образует полное бесконечное двоичное дерево.
• Что касается сложности формулы, префиксное отношение к строкам обычно рассматривается как отношение первого порядка. Без него не все формулы были бы эквивалентны ∆ ¹ ₂ формулы.
• Для свойств, выражаемых в S2S (рассмотрение набора всех двоичных строк в виде дерева), для каждого узла только O между левым поддеревом и правым поддеревом и остальными может передаваться (1) битов (см. сложность связи ).
• Для фиксированного k функция от строк до k (т.е. натуральных чисел ниже k ) может быть закодирована одним набором. Более того, s , t ⇒ s 01 t ′, где t ′ удваивает каждый символ t, является инъективным, и s ⇒ { s 01 t ′ : tε{0,1} ^* } является определяемым S2S. Напротив, по аргументу сложности связи, в S1S (ниже) пара наборов не может быть закодирована одним набором.

Ослабление S2S: Слабое S2S (WS2S) требует, чтобы все множества были конечными (обратите внимание, что конечность выражается в S2S с помощью леммы Кенига ). S1S можно получить, потребовав, чтобы «1» не появлялась в строках, а WS1S также требует конечности. Даже WS1S может интерпретировать арифметику Пресбургера с предикатом для степеней 2, поскольку множества можно использовать для представления неограниченных двоичных чисел с определяемым сложением.

Сложность решения

S2S разрешима, и каждая из S2S, S1S, WS2S, WS1S имеет неэлементарную сложность решения, соответствующую линейно растущему набору экспонент. Для нижней оценки достаточно рассмотреть Σ ¹ ₁ предложение WS1S. Один квантор второго порядка может использоваться для предложения арифметических (или других) вычислений, которые можно проверить с помощью кванторов первого порядка, если мы сможем проверить, какие числа равны. этого, если мы соответствующим образом закодируем числа 1.. m , мы можем закодировать число в двоичном представлении i ₁ i ₂ ... im _Для как i ₁ 1 i ₂ 2 ... im _m , которому предшествует охранник. Благодаря объединению тестирования средств защиты и повторному использованию имен переменных количество битов линейно зависит от количества экспонент. Что касается верхней границы, используя процедуру решения (ниже), предложения с k -кратным чередованием кванторов могут быть решены за время, соответствующее k + O (1)-кратному возведению в степень длины предложения (с равномерными константами).

Аксиоматизация

WS2S можно аксиоматизировать с помощью определенных основных свойств и индукционной схемы.

S2S можно частично аксиоматизировать следующим образом:
(1) ∃! s ∀ t ( t 0≠ s ∧ t 1≠ s ) (пустая строка, обозначается ε; ∃! s означает «существует уникальное s »)
(2) ∀ s , t ∀ i ∈ {0,1} ∀ j ∈ {0,1} ( si = tj ⇒ s = t ∧ i = j ) (использование i и j является сокращением; для i = j , 0 не равно 1)
(3) ∀ S ( S (ε) ∧ ∀ s ( S ( s ) ⇒ S ( s 0) ∧ S ( s 1))⇒ ∀ s S (s)) ( индукция )
(4) ∃ S ∀ s ( S ( s ) ⇔ φ( s )) ( S несвободен в φ)

(4) представляет собой схему понимания по формулам φ, которая всегда справедлива для логики второго порядка. Как обычно, если φ имеет непоказанные свободные переменные, мы берем универсальное замыкание аксиомы. Если равенство примитивно для предикатов, добавляется также экстенсиональность S = T ⇔ ∀ s ( S ( s ) ⇔ T ( s )). Поскольку у нас есть понимание, индукция может быть одним утверждением, а не схемой.

Аналогичная аксиоматизация S1S завершена. Однако по S2S полнота открыта (по состоянию на 2021 год). Хотя S1S имеет униформизацию, не существует определяемой S2S (даже допускающей параметры) функции выбора , которая при непустом множестве S возвращает элемент S , а схемы понимания обычно дополняются различными формами аксиом выбора . Однако (1)-(4) является полным, если расширить его схемой детерминированности для некоторых игр с четностью .

S2S также можно аксиоматизировать с помощью Π ¹ ₃ предложения (с использованием префиксного отношения к строкам в качестве примитива). Однако оно не является конечно аксиоматизируемым и не может быть аксиоматизировано с помощью Σ ¹ ₃ предложения, даже если добавить индукционную схему и конечное множество других предложений (это следует из ее связи с Π ¹ ₂ -СА ₀ ).

связанные с

Для каждого конечного k монадическая теория счетных графов второго порядка (MSO) с шириной дерева ≤ k (и соответствующее древесное разложение) интерпретируема в S2S (см. теорему Курселя ). Например, теория MSO деревьев (как графов) или последовательно-параллельных графов разрешима . Здесь (т.е. для ограниченной ширины дерева) мы также можем интерпретировать квантор конечности для набора вершин (или ребер), а также подсчитывать вершины (или ребра) в наборе по модулю фиксированного целого числа. Допуск несчетных графов не меняет теорию. Также, для сравнения, S1S может интерпретировать связные графы с ограниченной шириной пути .

Напротив, для каждого набора графов неограниченной древовидной ширины его экзистенциал (т. е. Σ ¹ ₁ ) Теория MSO неразрешима, если мы допускаем предикаты как на вершинах, так и на ребрах. Таким образом, в некотором смысле разрешимость S2S является наилучшей из возможных. Графы с неограниченной шириной дерева имеют большие миноры сетки, которые можно использовать для моделирования машины Тьюринга .

При сведении к S2S теория MSO счетных порядков разрешима, как и теория MSO счетных деревьев с их порядками Клини – Брауэра . Однако теория MSO ( $\mathbb {R}$, <) неразрешимо. Теория МСО ординалов <ω ₂ разрешима; разрешимость для ω ₂ не зависит от ZFC (в предположении Con(ZFC + слабо компактный кардинал )). Кроме того, ординал можно определить с использованием монадической логики второго порядка для ординалов тогда и только тогда, когда его можно получить из определимых регулярных кардиналов путем сложения и умножения порядковых номеров.

S2S полезен для разрешимости некоторых модальных логик, при этом семантика Крипке естественным образом приводит к деревьям.

S2S+U (или просто S1S+U) неразрешима, если U — неограниченный квантор — U X Φ( X ) тогда и только тогда, когда Φ( X ) выполняется для некоторого сколь угодно большого конечного X . Однако WS2S+U, даже при количественной оценке бесконечных путей, разрешима, даже с подформулами S2S, которые не содержат U.

Сложность формулы

Набор двоичных строк можно определить в S2S тогда и только тогда, когда он регулярен (т.е. образует регулярный язык ). В S1S (унарный) предикат на множествах (без параметров) определим тогда и только тогда, когда он является ω-регулярным языком . Для S2S, для формул, которые используют свои свободные переменные только в строках, не содержащих 1, выразительность такая же, как и для S1S.

Для любой формулы S2S φ( S ₁ ,..., S _k ), (с k свободными переменными) и конечного дерева двоичных строк T , φ( S ₁ ∩T,..., S _k ∩T) можно вычислить. во времени линейно по | Т | (см. теорему Курселя ), но, как отмечалось выше, накладные расходы могут быть итерированы экспоненциально по размеру формулы (точнее, время равно $O(|T|k)+2_{O(|\phi |)}^{2}$).

Для S1S каждая формула эквивалентна ∆ ¹ ₁ и логической комбинации Π ⁰ ₂ арифметические формулы. При этом каждая формула S1S эквивалентна принятию соответствующим ω-автоматом параметров формулы. Автомат может быть детерминированным автоматом четности: автомат четности имеет целочисленный приоритет для каждого состояния и принимает, если наивысший приоритет, наблюдаемый бесконечно часто, является нечетным (альтернативно, четным).

Для S2S с использованием древовидных автоматов (ниже) каждая формула эквивалентна Δ ¹ ₂ формула. Более того, каждая формула S2S эквивалентна формуле всего с четырьмя кванторами: ∃ S ∀ T ∃ s ∀ t ... (при условии, что наша формализация имеет как префиксное отношение, так и функции-преемники). Для S1S достаточно трех кванторов (∃ S ∀ s ∃ t ), а для WS2S и WS1S двух кванторов (∃ S ∀ t достаточно ); отношение префикса здесь не требуется для WS2S и WS1S.

Однако при наличии свободных переменных второго порядка не каждая формула S2S может быть выражена в арифметике второго порядка только через Π ¹ ₁ трансфинитная рекурсия (см. обратную математику ). RCA ₀ + (схема) {τ: τ — истинное предложение S2S} эквивалентно (схеме) {τ: τ — Π ¹ ₃ предложения доказуемы на Π ¹ ₂ -СА ₀ }. В рамках базовой теории схемы эквивалентны (схеме над k ) ∀ S ⊆ω ∃α ₁ <...<α _k L _{α 1} ( S ) ≺ _{Σ 1} ... ≺ _{Σ 1} L _{α k} (S) где L — конструируемая вселенная (см. также большой счетный ординал ). Из-за ограниченной индукции Π ¹ ₂ -CA ₀ не доказывает, что все верно (при стандартной процедуре принятия решения) Π ¹ ₃ утверждения S2S на самом деле верны, даже если каждое такое предложение доказуемо Π ¹ ₂ -СА ₀ .

Более того, для данных наборов двоичных строк S и T следующие эквивалентны:
(1) T является S2S определяемым из некоторого набора двоичных строк, вычислимых за полиномиальное время из S .
(2) T можно вычислить по множеству выигрышных позиций для некоторой игры, выигрыш которой представляет собой конечную булеву комбинацию Π ⁰ ₂ ( S ) комплекта.
(3) T может быть определен из S в арифметическом μ-исчислении (арифметические формулы + логика наименьшей фиксированной точки )
(4) T является наименьшей β-моделью (т. е. ω-моделью, теоретико-множественный аналог которой транзитивен ), содержащей S и удовлетворяющей всем Π ¹ ₃ последствия в Π ¹ ₂ -СА ₀ .

show

Эскиз доказательства:

See and, but briefly the proof runs as follows. (1)⇒(2) follows from the below decidability proof using tree automata. (2)⇒(1) follows by converting the game associated with a binary string s into a tree parity game with a fixed number of priorities and then merging these trees into a single tree (the binary trees can be merged here using s,t ⇒ s01t′ where t′ doubles every character of t). The below determinacy proof (in the decidability section) also leads to (2)⇒(3). Π¹₂-CA₀ proves Δ¹₂ monotonic induction, so (3)⇒(4).

For (3)⇒(2), define a game where player 1 attempts to show that the desired element s is inside the least fixed point. Player 1 gradually labels elements including s with rational numbers, intended to correspond to ordinal stages of the monotonic induction (any countable ordinal is embeddable into $\mathbb {Q}$). Player 2 plays elements with strictly descending labels (and he can pass) and wins iff the sequence is infinite or player 2 wins the last auxiliary game. In the auxiliary game, player 1 attempts to show that the last element picked by player 2 is a valid inductive step using elements with smaller labels. Now, if s is not in the least fixed-point, then the set of labels is ill-founded, or an inductive step is wrong, and (using monotonicity) this can be picked up by player 2. (If player 1 plays a smaller label outside the least fixed point, player 2 can use it (abandoning the auxiliary game), otherwise (using monotonicity) player 2 can use an auxiliary game strategy that assumes that the set of smaller labels in the original game will equal the least fixed point.)

For (4)⇒(3), we use monotonic induction to build an initial segment of the constructible hierarchy above a given real number r. This works as long as each ordinal α is identified by some appropriately expressible property of α so that we can encode α by a natural number and continue. Now, suppose that we built L_α(r) and the inductive step (which uses L_α(r) as a parameter) allows examining L_β(r). If a new Σ₁^(L(r),∈,r) fact appears between α and β, we can use it to label α and continue. Otherwise, we get the above Σ₁ elementary chains whose length corresponds to the nesting depth of the monotonic inductive definitions.

For the equivalence of RCA₀+S2S with {Π¹₃ φ: Π¹₂-CA₀⊢φ}, for each k the positional determinacy with k priorities is provable in Π¹₂-CA₀, while the rest (in terms of proving S2S sentences) can be done in a weak base theory. Conversely, RCA₀+S2S gives us a determinacy schema that gives existence of least fixed points (by a modification of the above (3)⇒(2) and even without requiring positionality; see the reference). In turn, their existence (using (4)⇒(3)) gives the desired Σ₁ elementary chains.

Модели S1S и S2S

Помимо стандартной модели (которая является уникальной моделью MSO для S1S и S2S), существуют другие модели для S1S и S2S, которые используют некоторые, а не все подмножества предметной области (см. семантику Хенкина ).

Для каждого S ⊆ω множества, рекурсивные в S, образуют элементарную подмодель стандартной модели S1S, и то же самое для любой непустой коллекции подмножеств ω, замкнутой относительно соединения по Тьюрингу и сводимости по Тьюрингу.

Это следует из относительной рекурсивности определяемых множеств S1S плюс униформизация:
- φ( s ) (как функция s ) может быть вычислена из параметров φ и значений φ( s ′ ) для конечного набора s ′ (с его размером, ограниченным количеством состояний в детерминированном автомате для φ).
- Свидетельство для ∃ S φ( S ) может быть получено путем выбора k и конечного фрагмента S ′ из S и многократного расширения S ′ так, чтобы наивысший приоритет во время каждого расширения был k и что расширение могло быть завершено до S удовлетворение φ без достижения приоритетов выше k (это разрешено только для начального S ′ ). Кроме того, используя лексикографически наименьший кратчайший выбор, существует формула S1S φ' такая, что φ'⇒φ и ∃ S φ( S ) ⇔∃! S φ'( S ) (т.е. униформизация; φ может иметь свободные переменные, которые не показаны; φ' зависит только от формулы φ).

Минимальная модель S2S состоит из всех обычных языков на двоичных строках. Это элементарная подмодель стандартной модели, поэтому, если определимый набор деревьев без параметров S2S непуст, то он включает в себя регулярное дерево. Регулярный язык также можно рассматривать как обычное полное бесконечное двоичное дерево с меткой {0,1} (идентифицируемое предикатами в строках). Помеченное дерево является регулярным, если его можно получить путем развертывания конечного ориентированного графа с помеченными вершинами и начальной вершиной; (направленный) цикл в графе, достижимый из начальной вершины, дает бесконечное дерево. При такой интерпретации и кодировании регулярных деревьев каждое истинное предложение S2S уже может быть доказуемо с помощью арифметики элементарных функций . Именно нерегулярные деревья могут потребовать непредикативного понимания для определения (ниже). Существуют нерегулярные (т.е. содержащие нерегулярные языки) модели S1S (и, предположительно, S2S) (как со стандартной частью первого порядка, так и без нее) с вычислимым отношением удовлетворения. Однако набор рекурсивных наборов строк не образует модель S2S из-за отсутствия понимания и определенности.

S2S

Доказательство разрешимости заключается в показе того, что каждая формула эквивалентна принятию недетерминированным древесным автоматом (см. древесный автомат и автомат с бесконечным деревом ). Автомат бесконечного дерева начинается с корня, движется вверх по дереву и принимает, если и только если каждая ветвь дерева принимает. Недетерминированный древовидный автомат принимает тогда и только тогда, когда игрок 1 имеет выигрышную стратегию, в которой игрок 1 выбирает разрешенную (для текущего состояния и входа) пару новых состояний ( p ₀ , p ₁ ), а игрок 2 выбирает ветвь с переходом к p _0, если выбрано 0, и p ₁ в противном случае. Для ко-недетерминированного автомата все выборы делает игрок 2, тогда как для детерминированного (p ₀ ,p ₁ ) фиксируется состоянием и вводом; а в игровом автомате два игрока играют в конечную игру, чтобы установить ветвь и состояние. Принятие ветки основано на состояниях, наблюдаемых в ветке бесконечно часто; автоматы четности здесь достаточно общие.

Для преобразования формул в автоматы базовый случай прост, а недетерминизм дает замыкание при наличии кванторов существования, поэтому нам нужно замыкание только при дополнении. Используя позиционную детерминированность игр на четность (именно здесь нам нужно непредикативное понимание), отсутствие выигрышной стратегии игрока 1 дает выигрышную стратегию игрока 2 S , с ко-недетерминированным древовидным автоматом, проверяющим ее правильность. Тогда автомат можно сделать детерминированным (при этом мы получаем экспоненциальное увеличение числа состояний), и, таким образом, существование S соответствует принятию недетерминированным автоматом.

Определенность: доказуемо, что в ZFC борелевские игры определяются и доказательство определенности для булевых комбинаций Π. ⁰ ₂ формулы (с произвольными вещественными параметрами) здесь также дают стратегию, которая зависит только от текущего состояния и позиции в дереве. Доказательство проводится индукцией по числу приоритетов. Предположим, что существует k приоритетов, причем наивысший приоритет равен k , и что k имеет правильную четность для игрока 2. Для каждой позиции (позиция в дереве + состояние) назначьте наименьший порядковый номер α (если есть), такой, что у игрока 1 есть выигрыш. стратегия, в которой все введенные (после одного или нескольких шагов) приоритетные k позиций (если таковые имеются) имеют метки <α. Игрок 1 может выиграть, если начальная позиция помечена: каждый раз, когда достигается состояние приоритета k , порядковый номер уменьшается, и, более того, между понижениями игрок 1 может использовать стратегию для приоритетов k -1. Игрок 2 может выиграть, если позиция не помечена: в силу определенности для приоритетов k -1 у игрока 2 есть стратегия, которая выигрывает или переходит в состояние немаркированного приоритета k , и в этом случае игрок 2 может снова использовать эту стратегию. Чтобы сделать стратегию позиционной (по индукции по k ), при игре во вспомогательную игру, если две выбранные позиционные стратегии приводят к одной и той же позиции, продолжить стратегию с меньшим α, или для того же α (или для игрока 2) с меньшим начальная позиция (поэтому мы можем менять стратегию конечное число раз).

Детерминизация автоматов. Для детерминизации коннедетерминированных древесных автоматов достаточно рассмотреть ω-автоматы, рассматривая выбор ветки как входные данные, определяя автомат и используя его для детерминированного древесного автомата. Обратите внимание, что это не работает для недетерминированных древовидных автоматов, поскольку детерминация перехода налево (т. е. s → s 0) может зависеть от содержимого правой ветви; в отличие от недетерминизма, детерминированные древесные автоматы не могут принимать даже точно непустые множества. Чтобы определить недетерминированный ω-автомат M (для ко-недетерминированного возьмем дополнение, отметив, что детерминированные автоматы четности закрыты относительно дополнений), мы можем использовать дерево Сафра , в котором каждый узел хранит набор возможных состояний M , и создание узла и удаление на основе достижения состояний с высоким приоритетом. Подробности см. или.

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

Теория деревьев. Для разрешимости логики MSO на деревьях (т. е. графах, которые являются деревьями), даже при наличии конечности и модульных кванторов счета для объектов первого порядка, мы можем встроить счетные деревья в полное двоичное дерево и использовать разрешимость S2S. Например, для узла s мы можем представить его дочерние элементы как s 1, s 01, s 001 и так далее. Для несчетных деревьев мы можем использовать теорему Шелаха-Ступа (ниже). Мы также можем добавить предикат для множества объектов первого порядка, имеющих мощность ω ₁ , и предикат для мощности ω ₂ и т. д. для бесконечных регулярных кардиналов. Графы ограниченной ширины дерева интерпретируются с помощью деревьев, и без предикатов над ребрами это также применимо к графам ограниченной ширины клики .

S2S с другими

Древовидные расширения монадических теорий: по теореме Шелаха-Ступа если монадическая реляционная модель M разрешима, то разрешима и ее древовидная модель. Например, (по модулю выбора формализации) S2S является древовидным аналогом {0,1}. В аналоге дерева объекты первого порядка представляют собой конечные последовательности элементов M , упорядоченных расширением, а M -отношение P _i отображается в Pi _' ( vd ₁ ,..., vd _k ) ⇔ P _i ( d ₁ ,..., d _k ) с Pi _' false в противном случае ( d _j ∈ M , а v представляет собой (возможно, пустую) последовательность элементов M ). Доказательство аналогично доказательству разрешимости S2S. На каждом шаге (недетерминированный) автомат получает на вход кортеж из M объектов (возможно, второго порядка), и формула M определяет, какие переходы состояний разрешены. Игрок 1 (как указано выше) выбирает отображение дочернего состояния, которое разрешено формулой (с учетом текущего состояния), а игрок 2 выбирает дочернего элемента (узла) для продолжения. Чтобы засвидетельствовать отклонение недетерминированным автоматом, для каждого (узел, состояние) выберите набор пар (дочерний, состояние) такой, чтобы для каждого выбора попадалась хотя бы одна из пар, и такой, чтобы все результирующие пути вели к отказу.

Объединение монадической теории с теорией первого порядка: теорема Фефермана – Вота расширяется/применяется следующим образом. Если M — модель MSO, а N — модель первого порядка, то M остается разрешимой относительно оракула (Theory( ) , Theory( N )) M даже если M дополняется всеми функциями M → N , где M отождествляется со своим первые объекты, и для каждого s ∈ M мы используем несвязную копию N с соответствующим изменением языка. Например, если N равно ( $\mathbb {R}$,0,+,⋅), мы можем сформулировать ∀(функция f ) ∀ s ∃ r ∈ N _s f ( s ) + _{N s} r = 0 _{N s} . Если M является S2S (или, в более общем смысле, древовидным аналогом некоторой монадической модели), автоматы теперь могут использовать N -формулы и тем самым преобразовывать f : M → N ^к в кортеж из M множеств. Дизъюнктность необходима, так как в противном случае для любого бесконечного N с равенством расширенное S2S или просто WS1S неразрешимо. Кроме того, для (возможно, неполной) теории T теория T ^М M -произведений T M разрешима относительно оракула (Theory( ) , T ), где модель T ^М использует произвольную непересекающуюся модель N _s из T для каждого s ∈ M (как указано выше, M является моделью MSO; Theory( N _s ) может зависеть от s ). Доказательство проводится индукцией по сложности формулы. Пусть v _s — список свободных N _s переменных, включая f ( s ), если функция f свободна. По индукции показывается, что v _s используется только через конечный набор N -формул с | в _с | свободные переменные. Таким образом, мы можем количественно оценить все возможные результаты, используя N (или T ), чтобы ответить на то, что возможно, и, учитывая список возможностей (или ограничений), сформулировать соответствующее предложение в M .

Кодирование в расширения S2S: каждый разрешимый предикат в строках может быть закодирован (с кодированием и декодированием с линейным временем) для разрешимости S2S (даже с указанными выше расширениями) вместе с закодированным предикатом. Доказательство: Учитывая недетерминированный бесконечный древесный автомат, мы можем разделить множество конечных двоичных помеченных деревьев (имеющих метки, над которыми может работать автомат) на конечное число классов так, что если полное бесконечное двоичное дерево может состоять из деревьев одного класса, прием зависит только от класса и начального состояния (т.е. состояния, в котором автомат входит в дерево). (Обратите внимание на грубое сходство с леммой о накачке .) Например (для автомата с четностью), присвойте деревьям один и тот же класс, если они имеют тот же предикат, что и заданное начальное_состояние и набор Q пар (состояние, наивысший_приоритет_достигнутый) возвращает ли игрок 1 ( т.е. недетерминизм) может одновременно заставить все ветви соответствовать элементам Q . Теперь для каждого k выберем конечное множество деревьев (подходящих для кодирования), принадлежащих одному классу для автоматов 1- k , с выбором класса, согласованным по k . Чтобы закодировать предикат, закодируйте несколько битов, используя k =1, затем еще биты, используя k =2, и так далее.

Ссылки

Дополнительная ссылка:
Вейер, Марк (2002). «Разрешимость S1S и S2S» . Автоматы, логика и бесконечные игры . Конспекты лекций по информатике. Том. 2500. Спрингер. стр. 207–230. дои : 10.1007/3-540-36387-4_12 . ISBN  978-3-540-00388-5 .