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 much more ingeniously, through 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 more clearly see what separates and connects the differing paradigms, and show how: * to lift functions to strategies; the "Scott order" intrinsic to concurrent games plays a key role in turning functional dependency to causal dependency. * several paradigms of functional programming and logic arise naturally as 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. * to transfer enrichments of strategies (such as to probabilistic, quantum or real-number computation) to functional cases.
翻译:本文在两个主要计算范式之间建立桥梁:一是功能性范式,其基础是从输入到输出的计算;二是交互性范式,其计算在运行过程中对其环境作出反应。任何组合交互理论的核心都是系统与其环境之间的二分法。并发博弈与策略通过区分玩家移动(系统事件)与对手移动(环境事件),以极其局部的分布式方式细致处理这种二分法。而函数式方法必须通过其较为粗糙的输入与输出区分,更为巧妙地处理这种二分法。这导致出现了多种专门适应特定交互需求的函数式方法。通过并发博弈,我们可以更清晰地看到两种范式的联系与区别,并展示:* 如何将函数提升为策略;并发博弈固有的"Scott序"在将函数依赖转化为因果依赖中起着关键作用。* 若干函数式编程与逻辑范式自然而然地作为并发博弈的子范畴出现,包括稳定域理论、非确定性数据流、交互几何、双重解释、透镜与光学器件,以及它们在依赖透镜与光学器件中对容器的扩展。* 如何将策略的丰富扩展(如概率计算、量子计算或实数计算)转移到函数式情形。