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.

多年来，我的研究项目一直是理论计算机科学及其数学和逻辑基础。我的工作涉及分析数学模型和与现代编程语言理论相关的许多形式逻辑，其中包括高阶逻辑、资源敏感等概念。线性逻辑，以及证明和证明网络的代数和拓扑结构，这导致了我目前对程序证明动力学、反馈模型以及量子计算和量子测量理论的逻辑基础的研究。一个核心工具我们的工作是范畴论和范畴逻辑。 在这个研究计划中，我继续在三个相互关联的主题中扩展我之前的工作，涉及多值逻辑及其代数，称为 MV 代数。这些令人着迷的逻辑是逻辑学家在过去 30 年间发展起来的。代数被证明与当前的几个数学研究领域以及 20 世纪 90 年代的计算机科学和物理学有着显着的联系。量子测量和量子概率理论发展了量子效应的代数，令人惊讶的是，这些效应代数竟然包括了 MV 代数。我的工作（与爱丁堡的同事）开发了 MV 和效应代数的通用表示和分类（或“协调”）程序。 ，使用由算子代数产生的某些半群，我和我的学生将继续协调程序，使用两个物理学共有的半群对 MV 代数进行分类。 主题 2 研究部分反馈，包括编程语言理论中的递归和定点。追踪类别（用于分析线性逻辑证明理论中的反馈），我们继续寻找由量子信息理论驱动的新模型（例如在某些 C* 代数中）。未来的方向包括度量空间的分析。模拟计算基础中的模型、研究延迟反馈以及定点算子的 MV 代数分析（主题 3 是一个长期项目）它研究可计算性理论的新基础：图灵范畴（。作者：R. Cockett 和 P. Hofstra）。有界逻辑、高阶计算以及线性逻辑中组合代数产生的模型将包括形式安全性的研究。