Studies in many-valued logics, partial traces, and computability

多值逻辑、部分迹和可计算性研究

• 批准号: RGPIN-2018-06867
• 负责人: Scott, Philip
• 金额: $ 1.68万
• 依托单位: University of Ottawa
• 依托单位国家: 加拿大
• 项目类别: Discovery Grants Program - Individual
• 财政年份: 2020
• 资助国家: 加拿大
• 起止时间: 2020-01-01 至 2021-12-31
• 项目状态: 已结题
• 来源: https://www.nserc-crsng.gc.ca/ase-oro/Details-Detailles_eng.asp?id=714509
• 关键词: Studies; many; valued; logics; partial

My research program for many years has been in theoretical computer science and its mathematical and logical foundations. My work involves analyzing the mathematical models and the many formal logics related to modern programming language theory. We include such notions as higher-order logics, resource sensitive linear logics, as well as the algebraic and topological structure of proofs and networks of proofs. This leads to my current studies in the dynamics of proofs-as-programs, models of feedback, and the logical foundations of quantum computing and quantum measurement theory. A central tool in our work is category theory and categorical logic. In this research proposal, I continue to extend my previous work in three interlocking themes. Theme 1 involves many-valued logics and their algebras, called MV algebras. These fascinating logics were developed by logicians during the 1920's. In the last 30 years, MV algebras were shown to have remarkable connections to several current research areas of mathematics, as well as to computer science and physics. In the 1990s, mathematical physicists working in quantum measurement and quantum probability theories developed algebras of quantum effects. Surprisingly, these effect algebras turn out to include MV algebras. My work (with colleagues in Edinburgh) develops a general representation and classification (or “coordinatization”) program for MV and Effect algebras, using certain semigroups arising from operator algebras. My students and I will continue the coordinatization program to classify MV algebras using semigroups common to both physics and theoretical computer science, with applications to such areas as: infinite automata, probabilistic logics, and programming language semantics. Theme 2 studies partial feedback, including recursion and fixed-points in programming language theory. My students and I developed a general theory of partially traced categories (for analyzing feedback in linear logic proof theory), with many mathematical models. We continue to look for new models motivated by quantum information theory (e.g. in certain C*-algebras). Future directions include analysis of metric space models in the foundations of analog computing, studying feedback with delay, and analysis of MV-algebras with fixed-point operators (in Theme 1). Theme 3 is a long-term project. It studies new foundations of computability theory: Turing categories (by R. Cockett and P. Hofstra). A key feature will be using formal methods (in Coq) to formalize the relevant proofs. This is part of formalized mathematics. Theories studied will include computable functions from resource bounded logics, higher-order computation, and models arising from combinatory algebras in linear logic. Practical projects will include studies in formal security.

多年来，我的研究计划一直在理论计算机科学及其数学和逻辑基础中。我的工作涉及分析与现代编程语言理论相关的数学模型和许多正式逻辑。我们包括高阶逻辑，资源敏感线性逻辑以及证明和证明网络的代数和拓扑结构等注释。这导致了我目前在证明动力学的研究，反馈模型以及量子计算和量子测量理论的逻辑基础上的研究。我们工作中的一个核心工具是类别理论和分类逻辑。 在这项研究建议中，我继续将以前的工作扩展到三个互锁主题。主题1涉及多元价值逻辑及其代数，称为MV代数。这些引人入胜的逻辑是由逻辑学家在1920年代开发的。在过去的30年中，显示MV代数与当前数学的几个研究领域以及计算机科学和物理学有着显着的联系。在1990年代，从事量子测量和量子概率理论的数学物理学家产生了量子效应的代数。令人惊讶的是，这些代数结果包括MV代数。我的工作（在爱丁堡与同事）使用操作员代数引起的某些半群为MV和效应代数开发了一般代表和分类（或“协调”）计划。我和我的学生将继续使用两种物理学共同的半群来进行协调计划，以对MV代数进行分类 和理论计算机科学，并在以下领域进行了应用：无限自动机，概率逻辑和编程语言语义。主题2研究部分反馈，包括编程语言理论中的递归和固定点。我和我的学生通过许多数学模型制定了部分追踪类别的一般理论（用于线性逻辑证明理论中的反馈）。我们继续寻找以量子信息理论（例如在某些C*-代数中）动机的新模型。未来的方向包括对模拟计算基础中的度量空间模型的分析，延迟研究反馈以及用定点操作员对MV-Elgebras进行分析（主题1）。主题3是一个长期项目。它研究了计算理论的新基础：图灵类别（作者：R。Cockett和P. Hofstra）。关键功能将使用正式方法（In COQ）正式化相关的证据。这是形式化数学的一部分。研究的理论将包括来自资源有限逻辑，高阶计算的可计算功能，以及由线性逻辑中的组合代数引起的模型。实用项目将包括对正式安全的研究。