开放图与计算推理
Open Graphs and Computational Reasoning
摘要：
我们提出了一种形式的代数推理的计算对象表示为图形。边描述了由顶点表示的基元操作之间的数据流。这些图有一个由半边（画出的边有一个不连接的端）组成的界面，并通过沿着这些半边连接图来享受丰富的组成原则。特别地，这允许在图之间指定等式和重写规则。特定的计算模型然后可以被编码为这样的规则的公理集。进一步的规则可以图形化地导出，并且重写可以用于模拟计算系统的动态，例如在输入上评估程序。可以以这种方式形式化的模型的例子包括传统的电子电路以及最近的量子信息分类帐户。
英文摘要：
We present a form of algebraic reasoning for computational objects which are expressed as graphs. Edges describe the flow of data between primitive operations which are represented by vertices. These graphs have an interface made of half-edges (edges which are drawn with an unconnected end) and enjoy rich compositional principles by connecting graphs along these half-edges. In particular, this allows equations and rewrite rules to be specified between graphs. Particular computational models can then be encoded as an axiomatic set of such rules. Further rules can be derived graphically and rewriting can be used to simulate the dynamics of a computational system, e.g. evaluating a program on an input. Examples of models which can be formalised in this way include traditional electronic circuits as well as recent categorical accounts of quantum information.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
