Coalgebras, Modal Logic, Stone Duality

计算机编程的核心问题之一是编写正确的程序或使自己相信某些程序是正确的是非常困难的。解决这个问题的一个方法是运用逻辑。让我们先简单看一下逻辑。我们可以使用逻辑来(1)对世界做出陈述，(2)定义一个陈述在世界上什么时候成立或不成立，(3)使用推理规则从给定的陈述推导出新的陈述。“世界”可以指我们生活的世界，逻辑最初确实是用来推理日常问题的。在数学中，推理的世界是数学对象的世界。数学世界足够丰富，可以对不同的计算概念进行建模。因此，数学逻辑允许我们为不同的计算模型设计不同的逻辑。与此建议相关的逻辑被称为模态逻辑。这种努力的结果应该是使关于计算的推理完全精确，从而消除人类在对程序进行推理时容易犯的错误。在我的项目中，我将研究被称为转换系统的特定计算模型。过渡系统由状态和状态之间的关系组成。其思想是，每个状态代表计算的给定时刻，关系描述计算如何从一个状态进行到另一个状态。该项目旨在建立过渡系统的一般逻辑理论。它将建立逻辑和转换系统之间的关系，通过下面的弯路，允许我们使用某些被称为斯通对偶的数学理论。最近的发展建议使用协代数来表示过渡系统。余代数与代数有一种特殊的关系——称为对偶关系。就像在学校里解方程一样，代数可以用来表述推理原理。具体而言，本建议的目的如下。将适当的逻辑关联到任何类型的转换系统。演示如何将这些逻辑应用于关于程序的语句的验证。研究数学逻辑的某些概念和工具如何适用于余代数及其逻辑。iii .该项目将有助于将余代数理论作为20世纪90年代许多研究者发展起来的转移系统的一般理论。它也将对最近关于（模态）逻辑和余代数之间的联系的工作做出重要贡献。协代数和模态逻辑受到了数学和计算机科学不同领域研究者的关注，本研究将揭示它们之间的新联系。在更广泛的背景下，该项目一方面关注计算模型的基本关系，另一方面关注逻辑。协代数理论的发展为整合现有的见解和探索新的方向提供了可能性。

I.One of the central problems of programming computers is that it isvery difficult to write correct programs or to convince yourself ofthe correctness of some program. One way to tackle this problem is theuse of logic.Let us first take a brief look at logic. We can use logic to (1) make statements about the world, (2) define when a statement holds or does not hold in the world, (3) deduce new statements from given ones using rules of reasoning.`World' can mean the world we live in and logic was originally indeeddeveloped to reason about everyday problems. In mathematics, the worldone reasons about is the world of mathematical objects. Themathematical world is rich enough to model different notions ofcomputation. Mathematical logic thus allows us to devise differentlogics for different models of computation. The logics relevant forthis proposal are known as modal logics.The upshot of this effort should be to make reasoning aboutcomputations completely precise and thus to eliminate the errorshumans tend to make when reasoning about programs.II.In my project I will look at particular models of computation whichare called transition systems. Transition systems consist of statesand relations between states. The idea is that each state representsa given moment of the computation and the relations describe how thecomputation proceeds from on state to another.The project aims at a general theory of logics for transitionsystems. It will establish the relationship between logics andtransition systems via the following detour that allows us to use acertain mathematical theory known as Stone duality. Recent developments suggest using co-algebras to represent transitionsystems. Coalgebras are in a special relationship---calledduality---to algebras. In a similar way as known from solvingequations in school, algebra can be used to formulate reasoningprinciples.In particular, the aims of this proposal are the following. Toassociate to any type of transition system an appropriate logic. Toshow how these logics can be applied to the verification of statementsabout programs. To investigate how certain concepts and tools ofmathematical logic can be adapted to coalgebras and their logics.III.The project will contribute to the theory of coalgebras as a generaltheory of transition systems as developed in the 1990s by manyresearchers. It will also be an important contribution to the recentworks on the connections between (modal) logic andcoalgebras. Coalgebras and modal logic have received attention fromresearchers in different areas of mathematics and computer science andthis research will bring to light new connections them.In a wider context, the project concerns the fundamental relationshipunderlying models of computation on the one hand and logic on theother hand. The development of the theory of coalgebras opens up thepossibility of integrating existing insights and to explore newdirections.