GAME, alternating reachability
Lax535992.Game · concepts/Lax535992/Game.lean · lax-535992
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Definition
An instance is an and-or graph: a directed graph of positions with moves between them, some positions marked as universal, the others being existential, some marked as starting positions and some as won outright. The winning positions are the least set such that a position won outright is winning, an existential position with a move to a winning position is winning, and a universal position that has a move and all of whose moves lead to winning positions is winning. The instance is a yes-instance of GAME when some starting position is winning; GAME is the decision problem of the structures isomorphic to such an instance. It is reachability in an alternating graph.
Concept map
Lean source view on GitHub
| 1 | import Mathlib.ModelTheory.Semantics |
| 2 | import Lax904597.Problems |
| 3 | import Lax485149.Problems |
| 4 | |
| 5 | /-! |
| 6 | --- |
| 7 | title: GAME, alternating reachability |
| 8 | type: definition |
| 9 | --- |
| 10 | An instance is an and-or graph: a directed graph of positions with moves |
| 11 | between them, some positions marked as universal, the others being |
| 12 | existential, some marked as starting positions and some as won outright. |
| 13 | The winning positions are the least set such that a position won outright |
| 14 | is winning, an existential position with a move to a winning position is |
| 15 | winning, and a universal position that has a move and all of whose moves |
| 16 | lead to winning positions is winning. The instance is a yes-instance of GAME |
| 17 | when some starting position is winning; GAME is the decision problem of the |
| 18 | structures isomorphic to such an instance. It is reachability in an |
| 19 | alternating graph. |
| 20 | -/ |
| 21 | |
| 22 | namespace Lax535992.Game |
| 23 | |
| 24 | open Lax904597.Problems Lax485149.Problems |
| 25 | |
| 26 | open FirstOrder |
| 27 | |
| 28 | open FirstOrder.Language |
| 29 | |
| 30 | /-- The relation symbols of the language. -/ |
| 31 | inductive andOrGraphRel : ℕ → Type where |
| 32 | /-- `move a b`: the player to move at `a` may move to `b`. -/ |
| 33 | | move : andOrGraphRel 2 |
| 34 | /-- `univ a`: the node `a` belongs to the universal player. -/ |
| 35 | | univ : andOrGraphRel 1 |
| 36 | /-- `start a`: the node `a` is a marked starting position. -/ |
| 37 | | start : andOrGraphRel 1 |
| 38 | /-- `won a`: the node `a` wins outright. -/ |
| 39 | | won : andOrGraphRel 1 |
| 40 | deriving DecidableEq |
| 41 | |
| 42 | /-- The relational vocabulary of AND/OR graphs: a move relation, a mark for the |
| 43 | nodes of the universal player, a mark for the starting positions and a mark for |
| 44 | the positions that win outright. -/ |
| 45 | def andOrGraph : FirstOrder.Language := |
| 46 | ⟨fun _ => Empty, andOrGraphRel⟩ |
| 47 | |
| 48 | instance instIsRelationalAndOrGraph : FirstOrder.Language.IsRelational andOrGraph := fun _ => |
| 49 | (inferInstance : IsEmpty Empty) |
| 50 | |
| 51 | /-- `move a b`: the player to move at `a` may move to `b`. -/ |
| 52 | abbrev agMove : andOrGraph.Relations 2 := |
| 53 | .move |
| 54 | |
| 55 | /-- `univ a`: the node `a` belongs to the universal player. -/ |
| 56 | abbrev agUniv : andOrGraph.Relations 1 := |
| 57 | .univ |
| 58 | |
| 59 | /-- `start a`: the node `a` is a marked starting position. -/ |
| 60 | abbrev agStart : andOrGraph.Relations 1 := |
| 61 | .start |
| 62 | |
| 63 | /-- `won a`: the node `a` wins outright. -/ |
| 64 | abbrev agWon : andOrGraph.Relations 1 := |
| 65 | .won |
| 66 | |
| 67 | open FirstOrder |
| 68 | |
| 69 | open Language Structure |
| 70 | |
| 71 | section Defs |
| 72 | |
| 73 | variable {A : Type} [andOrGraph.Structure A] |
| 74 | |
| 75 | /-- `move a b`: the player to move at `a` may move to `b`. -/ |
| 76 | def AGMove {A : Type} [andOrGraph.Structure A] (a0 : A) (a1 : A) : Prop := |
| 77 | FirstOrder.Language.Structure.RelMap agMove ![a0, a1] |
| 78 | |
| 79 | /-- `univ a`: the node `a` belongs to the universal player. -/ |
| 80 | def AGUniv {A : Type} [andOrGraph.Structure A] (a0 : A) : Prop := |
| 81 | FirstOrder.Language.Structure.RelMap agUniv ![a0] |
| 82 | |
| 83 | /-- `start a`: the node `a` is a marked starting position. -/ |
| 84 | def AGStart {A : Type} [andOrGraph.Structure A] (a0 : A) : Prop := |
| 85 | FirstOrder.Language.Structure.RelMap agStart ![a0] |
| 86 | |
| 87 | /-- `won a`: the node `a` wins outright. -/ |
| 88 | def AGWon {A : Type} [andOrGraph.Structure A] (a0 : A) : Prop := |
| 89 | FirstOrder.Language.Structure.RelMap agWon ![a0] |
| 90 | |
| 91 | variable (A) in |
| 92 | /-- **The winning positions of an AND/OR graph**, as a least fixed point: a |
| 93 | position that wins outright, an existential position with a winning successor, |
| 94 | or a universal position that has a successor and all of whose successors |
| 95 | win. -/ |
| 96 | inductive WinsOn : A → Prop |
| 97 | /-- A position that wins outright. -/ |
| 98 | | won {a : A} : AGWon a → WinsOn a |
| 99 | /-- An existential position with a winning successor. -/ |
| 100 | | ex {a b : A} : ¬AGUniv a → AGMove a b → WinsOn b → WinsOn a |
| 101 | /-- A universal position with a successor, all of whose successors win. -/ |
| 102 | | all {a : A} : AGUniv a → (∃ b, AGMove a b) → (∀ b, AGMove a b → WinsOn b) → WinsOn a |
| 103 | |
| 104 | variable (A) in |
| 105 | /-- Some marked starting position is winning. -/ |
| 106 | def GameWon : Prop := ∃ s : A, AGStart s ∧ WinsOn A s |
| 107 | |
| 108 | end Defs |
| 109 | |
| 110 | /-- GAME, alternating reachability: does the existential player win from some |
| 111 | starting position? -/ |
| 112 | def GAME : DecisionProblem andOrGraph := DecisionProblem.ofPred fun A _ => GameWon A |
| 113 | |
| 114 | end Lax535992.Game |
| 115 |
Builds on
Used by
Lax535992.CircuitValueInvarianceLax535992.CircuitValuePTIMECompleteLax535992.DeterministicMachineInvarianceLax535992.DeterministicMachinePTIMECompleteLax535992.GameInvarianceLax535992.GamePTIMECompleteLax535992.HornIsLeastFixedPointLax535992.HornSatInvarianceLax535992.HornSatPTIMECompleteLax535992.ImmermanVardiLax535992.InflationaryIsLeastFixedPointLax535992.LeastFixedPointComplementLax535992.NLSubsetPTIMELax535992.PTIMEClosureLax535992.PTIMEEqCoPTIMELax535992.PTIMESubsetNP
From Mathlib
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments