A compositional approach to game-theoretic economic modelling

博弈论是对不确定条件下战略互动和决策的数学研究。它可以说是微观经济学的核心工具，也被广泛应用于进化生物学、网络安全和军事战略等应用领域。可组合性是软件科学最基本的思想之一，它的原则是系统的行为应该根据其组件的行为是可理解的。可组合性允许以模块化方式设计、实施、分析和测试大型复杂系统，并允许在不同环境中重复使用模块。没有这一点，现代软件工程将是不可能的。然而，游戏模型不是组合式的，通常必须整体生产，而不是通过组合标准组件来生产。因此，博弈论建模是一个缓慢的过程，因为要建模的领域中的小变化可能会导致模型中所需的大变化。特别是，这意味着博弈论模型目前不太适合软件实现。这个项目涉及一种新的博弈论方法，它是组合的，因此承诺在目前不可能的规模上为经济学家和其他博弈论用户提供软件支持。具体地说，应该能够以一种允许重用现有工作的方式来指定、模拟、解决和更一般地推理游戏。例如，一个典型的经济系统有一个层次结构，从代理人到家庭，再到市场，再到经济，应该可以直接使用较低级别的现有模型来逐步建立每个级别的模型。这种方法背后的数学技术和概念主要来自证明论(数理逻辑的一部分)和编程语言理论(理论计算机科学的一部分)。幸运的是，用户不需要学习这个复杂的(对他们来说)陌生的理论，因为它也可以将数学隐藏在一种被称为串图的直观图形语言后面，最近由于在量子信息论、语言学和抽象代数中的应用，这种语言得到了广泛的研究。这意味着博弈论软件可以是图形和直观的，但仍然具有强大的理论基础。本项目的目的是开发这些经济应用所需的数学理论，以利用该领域理论和应用之间的密切关系，同时使用一个实例(基于智能电网的建模)来提供对组合的实际好处的持续测试。本项目的大部分理论部分将涉及使用博弈论中的各种已知概念来扩展选择函数理论，例如重复博弈、不完全信息和不同的解决方案概念，这些概念可以在任何关于博弈论的标准文本中找到。这将在很大程度上包括将现有理论推广到新框架。

Game theory is the mathematical study of strategic interaction and decision-making under uncertainty. It is arguably the central tool of microeconomics, and is also widely used in evolutionary biology, cybersecurity and military strategy, among other application areas. Compositionality, one of the most fundamental ideas of software science, is the principle that the behaviour of a system should be understandable in terms of the behaviour of its components. Compositionality allows large, complex systems to be designed, implemented, analysed and tested in a modular way, and allows modules to be reused in different contexts. Without this, modern software engineering would be impossible.Game models, however, are not compositional, and generally must be produced in their entirety rather than by combining standard components. As a result, game-theoretic modelling is a slow process, as small variations in the domain to be modelled can lead to large changes needed in the model. In particular this means that game-theoretic models are currently not well-suited to software implementation.This project concerns a new approach to game theory which is compositional, and therefore promises the possibility of software support for economists and other users of game theory on a scale that is currently impossible. Specifically, it should be possible to specify, simulate, solve and more generally reason about games in a way that allows the reuse of existing work. For example a typical economic system has a hierarchical structure, from agents to households to markets to economies, and it should be possible to gradually build models of each level in a way that directly uses existing models of the lower levels.The mathematical techniques and concepts underlying this approach mostly come from proof theory (part of mathematical logic) and the theory of programming languages (part of theoretical computer science). Fortunately there is no need for users to learn this sophisticated and (to them) unfamiliar theory, because it is also possible to hide the mathematics behind an intuitive graphical language known as string diagrams, which have been widely studied recently due to applications in quantum information theory, linguistics and abstract algebra. This means that game theoretic software can be graphical and intuitive, but still have a strong theoretical underpinning.The purpose of this project is to develop the mathematical theory needed for these economic applications, in a way that exploits the close relationship between theory and applications in this area, while using a worked example (based on modelling of smart energy grids) to provide a continual test of the practical benefits of compositionality.A large part of the theoretical part of this project will involve extending the theory of selection functions with various known concepts in game theory, such as repeated games, imperfect information and different solution concepts, which can be found in any standard text on game theory. This will largely consist of generalising existing theory to the new framework.