3 ms·

Does this have anything to do with modal logic?

gylterud 1y ago
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.html https://hakon.gylterud.net/programming/applicative-logic.htm... [1]: https://github.com/typeterrorist/applicative-logic/blob/modal-logic/src/Control/Applicative/Logic/Modal.hs https://github.com/typeterrorist/applicative-logic/blob/moda... – this is a branch with the modal logic operators defined.
- gylterud 1y ago
  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

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.html https://hakon.gylterud.net/programming/applicative-logic.htm... [1]: https://github.com/typeterrorist/applicative-logic/blob/modal-logic/src/Control/Applicative/Logic/Modal.hs https://github.com/typeterrorist/applicative-logic/blob/moda... – this is a branch with the modal logic operators defined.

gylterud 1y ago
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