Monad as Modality
Monad as Modality
复制标题
作为情态的单子
DOI：
10.1016/s0304-3975(96)00169-7
复制
发表时间：
1997
期刊：
影响因子：
--
通讯作者：
Satoshi Kobayashi
中科院分区：
文献类型：
--
作者：
Satoshi Kobayashi
1989年，Eugenio Moggi提出了一个基于强单子概念的程序语义范畴框架。他证明了各种计算都可以在他的框架中建模。另一方面，强单子不适合传统模态逻辑的范畴语义。根据这些观察，莫吉认为CurryHoward对应在模态逻辑中的程序和构造性证明之间不成立。然而，与他的观点相反，我们可以证明，在某种模态逻辑中的证明实际上被认为是程序。在本文中，首先我们将引入一个强单子的概念，它是强单子的推广。使用这个新概念，我们可以概括莫吉的语义--保持他的方程式逻辑的正确性和完整性。接下来，我们将证明，S4模态逻辑的一个建设性版本的一个健全的和完整的语义，强单子。最后，我们提出了一种方法来提取一个基于单子的命令式功能程序从模态逻辑的证明。有趣的是，这个方法也可以用强单子来理解。
In 1989, Eugenio Moggi proposed a categorical framework for program semantics based on the notion of a strong monad. He showed that various kinds of computation can be modeled in his framework. On the other hand, strong monads are not suited for the categorical semantics of traditional modal logics. According to these observations, Moggi thought that the CurryHoward correspondence would not hold between programs and constructive proofs in modal logics. However, contrary to his view, we can show that proofs in a certain kind of modal logics are actually considered as programs. In this paper, first we shall introduce the notion of an ℓ-strong monad which is a generalization of strong monads. Using this new notion, we can generalize Moggi's semantics-preserving soundness and completeness with respect to his equational logic. Next we shall show that ℓ-strong monads give a sound and complete semantics of a constructive version of S4 modal logic. Finally, we present a method to extract a monad-based imperative functional program from a proof in the modal logic. Interestingly, this method can also be understood in terms of ℓ-strong monads.