npinsker on The Anti-Pattern Game

Does this have anything to do with modal logic?

Yes, but the connection is not clear from what I wrote. I keep intending to make a little post about the connection, but I want it to highlight some Haskell code I wrote, but I haven't polished it yet. I want to make an update to it, using my applicative logic library[0][1].

The short version: By representing the game coalgebraically, one can use modal logic to solve it (find a winning strategy for player 1) by brute force.

The old code looks like:

    -- Modal operators
    e = modal any' (Coalg possible)
    a = modal all' (Coalg possible)

    -- Test for winning strategy within a limited number of moves.
    winning :: Integer -> Player -> State -> Bool
    winning 0 _ _ = False
    winning n p s = wonAlready || e (a (winning (n-1) p)) s where
           wonAlready = (winner s == Just p)

We can translate this into more standard modal logic: Letting ◇ be "There is a move a player could make", and □ be any move a player makes. We define the existence of a winnning strategy for player 1 inductively:

    S(0) = ⊥
    S(n+1) = W(p₁) ∨ ◇ □ S(n)

Intuitively, you have a winning strategy if you won already, or if there is a move you make, such that whatever move the opponent makes you, you still have a winning strategy.

[0]: https://hakon.gylterud.net/programming/applicative-logic.htm...

[1]: https://github.com/typeterrorist/applicative-logic/blob/moda... – this is a branch with the modal logic operators defined.

gylterudOP1y

The above just test for existence, but a slight modification, based on the same logical expression, gets us to a winning strategy:

     -- Game data
     data Player = P1 | P2
            deriving (Eq, Show)

     data Color = Red | Blue
            deriving (Eq, Show)

     data State = S [Color]
            deriving (Eq, Show)

     data Strategy = Won
                   | Force Color Strategy
                   | Choice (Color -> Strategy)



    -- Modal operators
    e' = modal sany' (Coalg possible')
    a' = modal sall' (Coalg possible')

     -- Test for winning strategy within a limited number of moves.
     winning' :: Integer -> Player -> State -> Maybe Strategy
     winning' 0 _ _ = Nothing
     winning' n p s = wonAlready <|> (e' (a' (winning' (n-1) p)) s) where
            wonAlready = if (winner s == Just p) then Just Won else Nothing

Comments