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 cod

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.