编程接口和基本拓扑
Programming interfaces and basic topology
摘要：
在编程中一次又一次出现的交互模式是“握手”，其中两个代理交换数据。交换被认为是提供服务。每一次交互都是由一个特定的代理发起的--客户端或天使--并由另一个代理结束--服务器或恶魔。我们提出了一个类别，其中的对象-称为交互结构的文件-作为描述的服务提供了这样的握手接口。态射--称为（通用）模拟--对提供一种这样的服务的组件进行建模，依赖于另一种服务。态射是相互作用结构的底层集合之间的关系。证明一个关系是一个模拟可以（原则上）作为一个可执行的程序，其规格是，它提供的服务所描述的域，给定的实现所描述的服务，其codomain。这一类别，然后示出符合子类别的“生成”的基本拓扑Sambin的术语，其中一个基本拓扑是由一个封闭运营商，其诱导的超格结构不需要分配;此外，这个运营商是归纳生成的基本覆盖关系。这种巧合为拓扑学家提供了非分配形式拓扑的自然例子来源。它提出了一些感兴趣的问题都正式拓扑和编程。然后在交互结构的上下文中解释使这样的基本拓扑成为真正的形式拓扑所需的额外结构。
英文摘要：
A pattern of interaction that arises again and again in programming is a "handshake", in which two agents exchange data. The exchange is thought of as provision of a service. Each interaction is initiated by a specific agent--the client or Angel--and concluded by the other--the server or Demon. We present a category in which the objects--called interaction structures in the paper--serve as descriptions of services provided across such handshaken interfaces. The morphisms--called (general) simulations--model components that provide one such service, relying on another. The morphisms are relations between the underlying sets of the interaction structures. The proof that a relation is a simulation can serve (in principle) as an executable program, whose specification is that it provides the service described by its domain, given an implementation of the service described by its codomain. This category is then shown to coincide with the subcategory of "generated" basic topologies in Sambin's terminology, where a basic topology is given by a closure operator whose induced sup-lattice structure need not be distributive; and moreover, this operator is inductively generated from a basic cover relation. This coincidence provides topologists with a natural source of examples for non-distributive formal topology. It raises a number of questions of interest both for formal topology and programming. The extra structure needed to make such a basic topology into a real formal topology is then interpreted in the context of interaction structures.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
