Theory and Pragmatics of Optimal Reduction: Logic, Linear Naming, and Programming Language Design

这项研究计划利用最优评估和线性逻辑的原理，研究命名和共享数据和计算线程的理论和语用。这些工具明确强调了过程调用协议中必不可少的复制和丢弃操作。该项目分析了优化求值算法、盒子管理的复杂性以及具有显式控制的语言的求值语用。研究议程中还包括内涵完全抽象定理，其中术语的含义包括关于如何共享计算的操作信息，以及使用上下文语义学作为流分析工具，其中所谓的“交互几何”可以提供有关过程如何访问其参数的信息。计划对高级别共享中出现的“重叠”现象进行进一步调查。最后一个部分寻求用线性逻辑对图归约的总线系统进行精细的解释，以期给出具有最佳评价特征的增量计算的新的范畴表示。

This research program investigates the theory and pragmatics of naming and sharing data and computation threads, using principles of optimal evaluation and linear logic. These tools explicitly highlight the operations of copying and discarding that are essential in procedure calling protocols.The project analyzes the algorithmics of optimal evaluation, the complexity of box management, and the evaluation pragmatics for languages with explicit control. Also included in the research agenda are intensional full abstraction theorems, where the meaning of a term includes operational information about how computations are shared, and the use of context semantics as a flow analysis tool, where the so-called "geometry of interaction" can give information about how procedures access their arguments. A further investigation of ``superposition'' phenomena that occur in high-level sharing is planned. The final component seeks a refined explanation of the bus system of graph reduction in terms of linear logic, in the hope of giving a new categorical rendition of the incremental computation that characterizes optimal evaluation.