Alternating machines in bounded space
Lax480241.AlternatingSpace · concepts/Lax480241/AlternatingSpace.lean · lax-480241
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Definition
An alternating Turing machine instance of the polynomial hierarchy accepts in bounded space when an initial configuration wins the game played on its configurations, without a bound on the number of steps; its states are split in two by the marks, one per player. Acceptance by alternating machines in bounded space, the problem defining APSPACE, holds of a well-formed instance whose states are so split and which accepts in bounded space.
Concept map
Lean source view on GitHub
| 1 | import Mathlib.Algebra.BigOperators.Finprod |
| 2 | import Mathlib.Data.Set.Finite.Lemmas |
| 3 | import Mathlib.Data.Fintype.EquivFin |
| 4 | import Mathlib.Data.Set.Card |
| 5 | import Mathlib.SetTheory.Cardinal.Finite |
| 6 | import Mathlib.Logic.Equiv.Prod |
| 7 | import Lax564036.AlternatingMachines |
| 8 | import Lax904597.Machines |
| 9 | import Lax485149.Problems |
| 10 | |
| 11 | /-! |
| 12 | --- |
| 13 | title: Alternating machines in bounded space |
| 14 | type: definition |
| 15 | --- |
| 16 | An alternating Turing machine instance of the polynomial hierarchy accepts |
| 17 | in bounded space when an initial configuration wins the game played on its |
| 18 | configurations, without a bound on the number of steps; its states are split |
| 19 | in two by the marks, one per player. Acceptance by alternating machines in |
| 20 | bounded space, the problem defining APSPACE, holds of a well-formed instance |
| 21 | whose states are so split and which accepts in bounded space. |
| 22 | -/ |
| 23 | |
| 24 | namespace Lax480241.AlternatingSpace |
| 25 | |
| 26 | open Lax564036.AlternatingMachines Lax904597.Machines |
| 27 | |
| 28 | namespace ATMData |
| 29 | |
| 30 | variable {A : Type} (M : ATMData A) |
| 31 | |
| 32 | /-- **Winning the alternating game**, with no bound on the length of a play: an |
| 33 | accepting state wins; an existential configuration wins when some successor |
| 34 | does; a universal one wins when it has a successor and every successor wins. |
| 35 | |
| 36 | Being a least fixed point, this makes an infinite play a loss for the |
| 37 | existential player – the standard convention, and the one the budgeted |
| 38 | `ATMData.AltAcc` already has. -/ |
| 39 | inductive AltWin (start : Bool) : Config A → Prop |
| 40 | /-- An accepting state wins outright. -/ |
| 41 | | acc {c : Config A} : M.Acc c.state → AltWin start c |
| 42 | /-- An existential configuration wins when some successor does. -/ |
| 43 | | ex {c c' : Config A} : ¬M.IsUniv start c.state → M.Step c c' → AltWin start c' → |
| 44 | AltWin start c |
| 45 | /-- A universal configuration wins when it has a successor and every |
| 46 | successor wins. -/ |
| 47 | | all {c : Config A} : M.IsUniv start c.state → (∃ c', M.Step c c') → |
| 48 | (∀ c', M.Step c c' → AltWin start c') → AltWin start c |
| 49 | |
| 50 | /-- **Acceptance in bounded space**: an initial configuration wins, the choice |
| 51 | of that configuration belonging to the player who moves first – exactly as in |
| 52 | `ATMData.AltAccepts`, and for the same reason. -/ |
| 53 | def AltAcceptsSpace (start : Bool) : Prop := |
| 54 | guardQ start (fun c₀ : Config A => M.IsInit c₀) (fun c₀ => ATMData.AltWin M start c₀) |
| 55 | |
| 56 | variable {M} |
| 57 | |
| 58 | variable (M) |
| 59 | |
| 60 | /-- **The marks split the states in two.** This is all the block discipline an |
| 61 | unbounded alternation needs: no state carries a mark above `1`, and every state |
| 62 | carries exactly one of the two. `ATMData.BlocksWellFormed` |
| 63 | is deliberately *not* required – its ordering clause is what bounds the number |
| 64 | of alternations. -/ |
| 65 | def BlocksSplit : Prop := |
| 66 | (∀ q, ∃ j, j < 2 ∧ M.Blk j q ∧ ∀ j', M.Blk j' q → j' = j) |
| 67 | |
| 68 | end ATMData |
| 69 | |
| 70 | open Lax904597.Problems Lax485149.Problems |
| 71 | |
| 72 | /-- **Alternating acceptance in bounded space**: the instance is a well-formed |
| 73 | alternating machine whose states the marks split in two, and it accepts in |
| 74 | bounded space. -/ |
| 75 | def ATMAcceptSpace : DecisionProblem (turingAlt 2) := |
| 76 | DecisionProblem.ofPred fun A _ => TMData.WellFormed (atmData 2 A).toTMData ∧ |
| 77 | ATMData.BlocksSplit (atmData 2 A) ∧ ATMData.AltAcceptsSpace (atmData 2 A) true |
| 78 | |
| 79 | end Lax480241.AlternatingSpace |
| 80 |
Used by
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments