SHF: SMALL: NONSTANDARD COMPUTATIONAL MODELS OF LINEAR LOGIC

标题：SHF：Small：非标准线性逻辑计算模型目前正在开发的许多有趣的软件依赖于数学基础，这些基础可以最好地用线性代数(例如大规模矩阵或图形数据)和统计学(例如机器学习算法或“大数据”分析)来表示。目前的编程语言并不特别适合处理这类数据，因此几乎没有提供内置支持来帮助科学家和软件开发人员。相反，在线性代数和统计学的背景下，已经发展了许多强大的数学技术，但这些技术还不适用于编程语言语义中的问题。这一研究项目寻求建立一个理论基础，将编程语言中看似完全不同的主题与这些数学领域联系起来。这项工作所采取的技术方法是开发“非标准”的线性逻辑模型，这是一种用于理解程序语义的可表达的低级框架。智力上的优点是在良好但不同的数学领域之间开发新的联系，将证明理论和程序语义与向量空间和概率度量类别中的表示联系起来。这项工作的更广泛影响通过其潜在的长期应用得到最好的理解，这些应用包括：用于处理数字数据的编程语言构造与支持高阶函数和抽象数据类型的平滑集成；基于数值方法的证据搜索的新技术；以及用于表达机器学习或概率算法的更好的编程语言。

TItle: SHF: Small: Nonstandard Computational Models of Linear LogicMuch of the interesting software being developed today relies on mathematical underpinnings that can best be expressed in terms of linear algebra (e.g. large scale matrices or graph data) and statistics (e.g. machine learning algorithms or "big data" analysis). Current programming languages aren't especially suited to working with such kinds of data, and so provide little built-in support to help scientists and software developers. Conversely, many powerful mathematical techniques have been developed in the contexts of linear algebra and statistics, but those techniques have not been applicable to problems in programming language semantics. This research project seeks to develop a theoretical foundation that connects the seemingly disparate topics of programming languages and these mathematical domains.The technical approach taken in this work is to develop "nonstandard" models of linear logic, which is an expressive and low-level framework for understanding program semantics. The intellectual merits are found in developing novel connections between well-established, but distinct, mathematical domains, connecting proof theory and program semantics to representations in vector spaces and categories of probability measures. The broader impacts of this work are best understood through its potential long-term applications, which include: smooth integration of programming language constructs for working with numerical data (like Matlab) with support for higher-order functions and abstract datatypes; new techniques for proof search based on numerical methods; and, better programming languages for expressing machine learning or probabilistic algorithm.