开放逻辑关系的通用性：连续性、自动微分和一个包含定理
On the Versatility of Open Logical Relations: Continuity, Automatic Differentiation, and a Containment Theorem
摘要：
逻辑关系是程序设计语言理论中最强大的技术之一，并已被广泛用于证明各种高阶演算的性质。然而，也有一些属性不能通过逻辑关系立即证明，例如程序的连续性和可微性在高阶语言中扩展了实值函数。非正式地说，这个问题源于这样一个事实，即这些属性自然地表达在非基类型的项上（或者等价地，在基类型的开放项上），并且对于基情况（即，对于基类型的封闭项）没有明显的好定义。为了克服这个问题，我们研究了一个广义的概念的逻辑关系，称为\emph{open logical relation}，并证明它可以卓有成效地应用在几个上下文中，其中感兴趣的属性是关于一阶类型的表达式。我们的设置是一个简单类型的$λ$-演算丰富的实数和实值的一阶函数从一个给定的集合，如连续或可微函数之一。我们首先证明了一个包含定理，说明对于任何这样的一个集合的功能，包括投影功能和关闭下的功能组合，任何良好的一阶类型的长期表示属于该集合的功能。然后，我们通过开放的逻辑关系的正确性的核心最近发表的算法向前自动微分。最后，我们定义了一个基于精化的类型系统的局部连续性在我们的演算与条件的扩展，并证明了可靠的类型系统使用开放的逻辑关系。
英文摘要：
Logical relations are one of the most powerful techniques in the theory of programming languages, and have been used extensively for proving properties of a variety of higher-order calculi. However, there are properties that cannot be immediately proved by means of logical relations, for instance program continuity and differentiability in higher-order languages extended with real-valued functions. Informally, the problem stems from the fact that these properties are naturally expressed on terms of non-ground type (or, equivalently, on open terms of base type), and there is no apparent good definition for a base case (i.e. for closed terms of ground types). To overcome this issue, we study a generalization of the concept of a logical relation, called \emph{open logical relation}, and prove that it can be fruitfully applied in several contexts in which the property of interest is about expressions of first-order type. Our setting is a simply-typed $λ$-calculus enriched with real numbers and real-valued first-order functions from a given set, such as the one of continuous or differentiable functions. We first prove a containment theorem stating that for any such a collection of functions including projection functions and closed under function composition, any well-typed term of first-order type denotes a function belonging to that collection. Then, we show by way of open logical relations the correctness of the core of a recently published algorithm for forward automatic differentiation. Finally, we define a refinement-based type system for local continuity in an extension of our calculus with conditionals, and prove the soundness of the type system using open logical relations.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
