Alternating acceptance in bounded space is in EXPTIME

The third layer, and the theorem: DescriptiveComplexity.ATMAcceptSpace is a DescriptiveComplexity.SOGameSpec, so it is in EXPTIME (DescriptiveComplexity.atmAcceptSpace_mem_EXPTIME) – EXPTIME's first natural problem, and one that needs no succinctness argument.

The correspondence is a bisimulation between two inductive predicates of the same shape: DescriptiveComplexity.SOGameSpec.Wins on assignments of the configuration block and DescriptiveComplexity.ATMData.AltWin on configurations. It needs exactly two lemmas beyond the four realization ones – a move lands on a configuration and a start is a configuration – so junk assignments, which the block has plenty of, are never reached and never have to be reasoned about.

Where the promises go: DescriptiveComplexity.ExpDefinable compares P A with Q (X.Map A), and DescriptiveComplexity.TMData.WellFormed and DescriptiveComplexity.ATMData.BlocksSplit are conditions on A alone, so they ride on the start sentence – a game with no starting state is lost, which is what a failed promise should mean.

noncomputable def DescriptiveComplexity.ATMSpace.atmSpec : SOGameSpec (FirstOrder.Language.turingAlt 2)

The alternating machine, as a second-order game: its states are the assignments of the configuration block, its moves are the machine's steps, the universal player owns the states marked by the second block, an accepting state wins outright, and the starting states are the initial configurations of a well-formed machine whose marks split.

Equations

• One or more equations did not get rendered due to their size.

The bisimulation

theorem DescriptiveComplexity.atmAcceptSpace_soGameDefinable : SOGameDefinable ATMAcceptSpace

Alternating acceptance in bounded space is a second-order game.

theorem DescriptiveComplexity.atmAcceptSpace_mem_EXPTIME : EXPTIME.Mem ATMAcceptSpace

Alternating acceptance in bounded space is in EXPTIME (APSPACE ⊆ EXPTIME, half of Chandra–Kozen–Stockmeyer 1981): the game on the configuration graph is DescriptiveComplexity.GAME read over the expansion whose points are the configurations, and GAME is in DescriptiveComplexity.PTIME.

This is EXPTIME's first natural problem, and it needs no succinctness argument: the expansion is applied after the problem, which is the composition that exists. The other half – the Chandra–Kozen–Stockmeyer simulation – is DescriptiveComplexity.atmAcceptSpace_EXPTIME_hard, whence DescriptiveComplexity.atmAcceptSpace_EXPTIME_complete.