|
コバヤシ サトシ
KOBAYASHI SATOSHI
小林 聡 所属 京都産業大学 情報理工学部 情報理工学科 職種 教授 |
|
| 言語種別 | 英語 |
| 発行・発表の年月 | 1997/03/30 |
| 形態種別 | その他 |
| 標題 | Monad as modality |
| 執筆形態 | その他 |
| 掲載誌名 | Theoretical Computer Science |
| 出版社・発行元 | Elsevier |
| 巻・号・頁 | 175(1),pp.29-74 |
| 著者・共著者 | Satoshi Kobayashi |
| 概要 | 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 Curry-Howard 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. |
| DOI | 10.1016/S0304-3975(96)00169-7 |
| ISSN | 0304-3975 |