Polarized logics, geometry of proofs, and semantics of computation

极化逻辑、证明几何和计算语义

• 批准号: 8544-2006
• 负责人: Scott, Philip
• 金额: $ 2.48万
• 依托单位: University of Ottawa
• 依托单位国家: 加拿大
• 项目类别: Discovery Grants Program - Individual
• 财政年份: 2007
• 资助国家: 加拿大
• 起止时间: 2007-01-01 至 2008-12-31
• 项目状态: 已结题
• 来源: https://www.nserc-crsng.gc.ca/ase-oro/Details-Detailles_eng.asp?id=363010
• 关键词: Polarized; logics; geometry; proofs; semantics

Linear logic and proof nets, introduced by Girard in 1987, gave rise to new ways of thinking about computation and the geometry of proofs. For example normalization of proofs (which corresponds to evaluation of functional programs) can be modelled in terms of travelling along paths in the nets (graphs) representing proofs. These travels are governed by algebraic laws on operators associated to edges of proof nets. This led to  dynamical semantics of proofs in terms of functional analysis, to a new semantics of algorithms and to dynamical invariants for normalization.   This is Girard's Geometry of Interaction (GoI).    In this work, we shall examine the program of Geometry of Interaction as well as so-called Polarized fragments of linear logic, trying to find models for dynamics of information flow and connections with complexity theory and the theory of quantum programming languages.

线性逻辑和证明网，由吉拉德在1987年提出，引起了新的思维方式的计算和几何证明。例如，证明的标准化（对应于函数程序的评估）可以按照表示证明的网络（图）中的沿着路径行进来建模。这些行程由与证明网的边缘相关联的算子的代数定律支配。这导致了动态语义的证明功能分析方面，一个新的语义的算法和动态不变量的规范化。 这是吉拉德的相互作用几何学。 在这项工作中，我们将研究相互作用几何的程序以及所谓的线性逻辑的极化片段，试图找到信息流的动力学模型以及与复杂性理论和量子编程语言理论的联系。