I present a formal connection between algebraic effects and game semantics, two important lines of work in programming languages semantics with applications in compositional software verification. Specifically, the algebraic signature enumerating the possible side-effects of a computation can be read as a game, and strategies for this game constitute the free algebra for the signature in a category of complete partial orders (cpos). Hence, strategies provide a convenient model of computations with uninterpreted side-effects. In particular, the operational flavor of game semantics carries over to the algebraic context, in the form of the coincidence between the initial algebras and the terminal coalgebras of cpo endofunctors. Conversely, the algebraic point of view sheds new light on the strategy constructions underlying game semantics. Strategy models can be reformulated as ideal completions of partial strategy trees (free dcpos on the term algebra). Extending the framework to multi-sorted signatures would make this construction available for a large class of games.
翻译:我展示了代数效应和游戏语义学之间的正式联系,这是在编程语言语义和合成软件验证应用中的两种重要工作线。具体地说,计算可能的副作用的代数符号可以被解读为一种游戏,而这种游戏的战略构成在完全部分订单(cpos)类别中签名的免费代数。因此,战略提供了一种方便的计算模型,具有未经解释的副作用。特别是,游戏语义学的实用调味可以传到代数环境,其形式是初始代数与超离子体终端燃煤数的巧合。相反,代数观点为游戏语义学基础的战略构造提供了新的亮点。战略模型可以重新拟订为部分战略树的理想完成(在代数术语中不使用代数)。将框架扩展为多种排序的签名,将为大型游戏提供这种构造。