時相論理言語 Temporal Prolog の一実現について

初出: 2011/MAY/05
たけおか (竹岡尚三)

0.時相論理言語 Temporal Prologの一実現について

Temporal Prologは、桜川貴司氏が考案した時相論理型言語である。
竹岡は、Temporal Prologを、 通常のPrologと同じ効率で実行できる実行系を実現した。
本文書は、その実現について、述べている。

1.時相論理言語 Temporal Prolog

時相論理や時制論理というものは、基本的に、論理の中に様相として、時間を 取り込んだものであろう。
例えば、時制を扱うのに、□, ◇, ○, until などの記号を導入する。(表1)

Temporal Prologは、桜川貴司氏が考案した、時相論理型言語で、
時制を扱うのに、□,■,◆,●,atnext,since,after,forなどの記号を使用して表す。
Temporal Prologの扱う時間は離散的で、「一つ前の時刻の過去」の事実などを参照したりする。(表2)

時相論理そのものや、Temporal Prologの理論的な面について語るのは、 本文書の範囲では無い。
詳しくは、 桜川貴司氏の文書などを読んでいただきたい

なお、この文中では、pure Prologの実行(レゾリューション)を「リダクション」とか「評価」と書く。


表1. よくある時制の様相記号
a⇒○b ある時刻にaが成り立つと、次の時刻にbが成り立つ
a⇒□b ある時刻にaが成り立つと、その後ずっとbが成り立つ
a⇒◇b ある時刻にaが成り立つと、次の後いつかはbが成り立つ
a⇒ b until c ある時刻にaが成り立つと、次の後cが成り立つまでは、bが成り立つ


表2. Temporal Prologの様相記号
C(condition)
●c 前の時刻にcが成り立った(前の時刻が無い場合は false)
■c 現在までずっとcが成り立っている
◆c 現在までにcが成り立ったことがある
c since d 最も最近にdが成り立って以来、その時刻も含めて現在までcは常に成り立っている
c after d 最も最近にdが成り立って以後、その時刻も含めて現在までにcが成り立ったことがある
c for n 現在も含めて過去n回連続してcが成り立った

R(result)
r until a aが成り立つ直前の時刻までrが成り立つ
r atnext a aが初めて成り立つ時、r も成り立つ
□r 未来永劫r が成り立つ

2. Temporal Prologの性質

桜川氏の論文では、時制に関するすべての様相は、「一つ前の過去(●で表す)」 に変換できる。
Temporal Prologの処理系は、実行前に、時間に関するすべての様相を、 「一つ前(●)」に変換する。
したがって、実行系は「一つ前」に関する論理だけを扱えれば十分である。

一般的に信じられている、時相論理言語の処理系についての、否定的な話は、

というものである。
しかし、Temporal Prologにおいては、そういうことは起きない。

時相論理言語の全般については言及しかねるが、
桜川の Temporal Prologに関しては、 前述のとおり、すべての様相が、一つ前の過去の参照に変換できる。

つまり、Temporal Prologプログラムは、

のは、自明である。

1986年頃、私は、独自にこの結論を得た。 そして、当時、これについて、私は桜川氏と議論をし、 私は、一つのみの過去しか記憶しない処理系を作って、正しく動かした。

3. Temporal Prologの竹岡による実現

私は、効率の良い処理系を作ることを念頭に検討を行い、

  1. 過去は一つ前しか記憶しない
  2. 不要な評価を行わない
ことを実現する処理系を設計し、実現した。

a.の過去については、前述のとおりである。


b.については、それまでの多くの一般的な時相論理言語の処理系の実現では、 無駄な評価が行われていたのである。

多くの時相論理言語で行われていたのは、 ある時刻において、存在する節をすべてリダクションし、 それによって得られた事実を、 その時刻の事実として、 その時刻のデータベースにすべて記憶(アサート)する、ということである。
純Prologは、副作用の無い、たちのいい言語なので、 どの節をどういう順序でリダクション(評価)しても問題はない。
そして、それらの節のうち、真になったものは、 その節中のバインドされた変数を そのインスタンシエイトされた値に書き換えて、 過去データベースにアサートされるだろう。
しかし、これは、未来永劫、 絶対に参照されることのない節(事実)を作るためにも、 無駄なリダクションを行っているのである。
実用プログラムの多くの部分は、いわゆるサブルーチンであり、 それは、必要が無い(呼出しが無い)時は、リダクションしなくてよい。
ところが、多くの時相論理言語の実現では、それらのサブルーチンも 常にリダクションすることが多かった。それはすなわち、無駄な実行である。
これは、お話にならない欠点である。

私は、無駄な計算を行わないために、要求駆動の考えを取り入れようと考えた。
要求駆動を実現する観点から 桜川の論文を読むと、それは次のような素晴らしいことを教えてくれる。

現在のPrologの実行は、未来(すなわち次の時間)から、参照される事柄だけを、 作っておけばいい。
すなわち、未来から参照されない事柄は、作り出す必要がない。
つまり、簡単かつ具体的にいうと、

この時間に関する依存関係に基づき、必要な節だけを評価し、 まったく不要な節を評価しない実装は、 Temporal Prologを実用的に動かすことにとって重要である。

●と関係の無い節、すなわち時間に関する依存関係が無い節は、いわゆるサブルーチンであり、それは、時間依存関係のある節から呼び出される。

以上の、要求駆動に基づく考えは、非常に有効である。
また、依存関係の抽出も、ボディ部に●のついた項が出現することを静的に一回調べるだけなので、 極めて単純である。
これによって、そもそもたちの良かったTemporal Prologを、通常のPrologと同等の効率で実行することができるようになった。


4. Temporal Prologのプログラミング

Temporal Prologでは、一時刻の中では、無限ループを書いたり、長い有限なループを書いたりしない。
これは、一般的な時相論理言語の実現の多くがそうであろう。

理論的には、無限ループがあっても、矛盾にはならないであろう。
しかし、シングル・スレッド環境で実行される通常のプログラミング言語として考えた場合は、
現在の時刻の全評価が終わらないと次の時刻に進めないので、 現在の時刻で終了しない無限ループを回るのは、非常に都合が悪い。

桜川氏は、Temporal Prologを、実行可能な仕様記述言語という面と、 並列論理型言語という面の2つを言っている。
可能性としては、実行系が(コンカレントにでも)、マルチ・スレッドを実現すれば、 また、無限ループも許せるであろう。
しかし、私の本実現は、シングル・スレッド環境でのシングル・スレッド実行として 設計、実装した。

というわけで、ループは時間方向に繰り返しを書く。
10回の繰り返しは、各時刻で1回の処理を行い、10時刻ですべて終わるように書く。
時相論理言語なのだから、意味的にそう書くべきだし、プログラマもその方が楽しいであろう。


5. 本Temporal Prologについて

別文書のマニュアルで詳述。


以上


たけおかの Prologページ 目次

たけおかの Lispページ 目次
たけおか(竹岡尚三)のホームページ