边界线性头部减少和通过骨架的可见交互
Bounding linear head reduction and visible interaction through skeletons
摘要：
在本文中，我们研究了高阶程序设计语言的执行复杂性。我们的研究有两个方面：一方面给出了Hyland-Ong博弈语义中有界P-可见策略之间相互作用长度的上界。这一结果涵盖了程序设计语言的模型，可以访问非确定性，状态或控制运算符等计算效果，但其语义制定导致了与语法的松散联系。另一方面，我们给出了我们的语义研究的句法对应：一个非初等上限的长度的线性头减少序列（一个低层次的概念减少，接近实际实施的减少高阶程序的抽象机器）的简单类型的的类元项。在这两种情况下，我们的上限证明是最佳的匹配下界。这两个结果，虽然不同的范围，证明使用相同的方法：我们介绍了一个简单的减少有限树的自然数，在此称为互动骨架。我们研究这种减少，并给出其复杂性的上限。然后，我们应用这项研究，给出两个模拟结果：一个语义的测量进展博弈论的相互作用，通过互动骨架，和一个语法建立一个对应关系的线性头减少条款满足当地条件称为局部范围和减少互动骨架。这个结果，然后推广到任意条款的局部scopization变换。
英文摘要：
In this paper, we study the complexity of execution in higher-order programming languages. Our study has two facets: on the one hand we give an upper bound to the length of interactions between bounded P-visible strategies in Hyland-Ong game semantics. This result covers models of programming languages with access to computational effects like non-determinism, state or control operators, but its semantic formulation causes a loose connection to syntax. On the other hand we give a syntactic counterpart of our semantic study: a non-elementary upper bound to the length of the linear head reduction sequence (a low-level notion of reduction, close to the actual implementation of the reduction of higher-order programs by abstract machines) of simply-typed lambda-terms. In both cases our upper bounds are proved optimal by giving matching lower bounds. These two results, although different in scope, are proved using the same method: we introduce a simple reduction on finite trees of natural numbers, hereby called interaction skeletons. We study this reduction and give upper bounds to its complexity. We then apply this study by giving two simulation results: a semantic one measuring progress in game-theoretic interaction via interaction skeletons, and a syntactic one establishing a correspondence between linear head reduction of terms satisfying a locality condition called local scope and the reduction of interaction skeletons. This result is then generalized to arbitrary terms by a local scopization transformation.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
