Speculating about an actually satisfactory way of proving correctness of open games I think proof by induction won't cut it. I want to use the Joyal-Street Sledgehammer to turn open games into acyclic graphs via string diagrams. That should be easier to relate to extensive form
-
-
Good question. I didn't think about infinite games. I'd also like to get correctness for infinite games at the same time if possible, which means coinduction would be needed. But coinduction hurts my head, I'd need some serious help for that
Thanks. Twitter will use this to make your timeline better. UndoUndo
-
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.
Read my blog!