一句话:通过并发博弈与策略统一函数式与交互式计算,并表明多种函数式/逻辑方法是其全子范畴。
论文连接函数式与交互式两大范式:前者以输入到输出为基础,后者在运行中响应环境。交互的组合理论需处理系统/环境二分;并发博弈与策略通过 Player 与 Opponent 移动的分布式区分细致刻画它,函数式方法则借助输入/输出更巧妙地应对。作者展示如何把函数提升为策略、把函数依赖转为因果依赖,并复用函数式技术。关键结果是:稳定域理论、非确定性数据流、交互几何、dialectica 解释、lenses/optics 及其依赖容器扩展等,都自然构成并发博弈的全子范畴;概率、量子与实数计算等丰富化也可特化到函数式情形。
The article bridges between two major paradigms in computation, the functional, at basis computation from input to output, and the interactive, where computation reacts to its environment while underway. Central to any compositional theory of interaction is the dichotomy between a system and its environment. Concurrent games and strategies address the dichotomy in fine detail, very locally, in a distributed fashion, through distinctions between Player moves (events of the system) and Opponent moves (those of the environment). A functional approach has to handle the dichotomy more ingeniously, via its blunter distinction between input and output. This has led to a variety of functional approaches, specialised to particular interactive demands. Through concurrent games we can see what separates and connects the differing paradigms, and show how:•to lift functions to strategies; how to turn functional dependency to causal dependency and so exploit functional techniques.•several approaches of functional programming and logic arise naturally as full subcategories of concurrent games, including stable domain theory; nondeterministic dataflow; geometry of interaction; the dialectica interpretation; lenses and optics, and their extensions to containers in dependent lenses and optics.•the enrichments of strategies (e.g. to probabilistic, quantum or real-number computation) specialise to the functional cases.