Coalgebras, Modal Logic, Stone Duality

点击翻译按钮获取中文摘要

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.