著者

沢村 一

出版者

一般社団法人情報処理学会

雑誌

情報処理学会論文誌 (ISSN:18827764)

巻号頁・発行日

vol.22, no.3, pp.216-224, 1981-05-15

---

R.Montagueは自然言語(英語)に現れるさまざまな種類の内包的な語法を一つの形式的体系の中に取り入れるために一種の高階の様相論理である内包論理を展開した.この内包論理はまた言語としてのプログラミング言語に現れる内包性の問題をも解決することができる.これまで様相論理に含まれるが概念とプログラムについて議論するさいに起る概念との間には意味論的および統語論的な両方の観点から密接な対応が存在するという理由で様相論理がプログラムの論証に対して適用されてきたが この能力のゆえに内包論理の一般的枠組はプログラムの論理を考えるさいに様相論理よりもより十分な表現能力を提供している.本文ではプログラミング言語の内包性にのみ注目して最初に 内包性の問題を解くために必要な言語要素を付加された内包論理について述べ 次にこの論理を基礎として Hoare論理の関数的変形となっている内包的Hoare論理(IHL)を形式化する.内包的Hoare論理は単にHoare論理の表現力に富んだ別形としてだけではなく これまで提案されてきたいろいろな算法論理とさらにはプログラミング言語と自然言語の双方に対する統一的な論理体系の可能な一つの形体であると考えられる.