論理プログラミングつぶやき

某高校生のつり
http://pc11.2ch.net/test/read.cgi/mysv/1102662133/
で私がつられた箇所:

  • 34: この環境だと、エージェントを送り込んだり(受け入れたり)、それを自由に移動させたりできるように思いますが、
  • 51: 並列実行は可能ですか。
    1) 複数サーバにたいするOR並列
    2) Prologを拡張してのAND並列
  • 60: プログラム言語は最終的にはMLとPrologの一騎打ちになるとお考えですか。
  • 118: ...日本のprolog屋がC/C++なんて書けるはずもないか。無意味な論文積み上げて、博士や大学教員になる事しか考えてないからな。
  • 133: 何故にErlangが出てきたかという話をしておきます。
  • 135: Wijaという環境上に構築されるオーバーレイGHCというものがあります。例の未踏ソフトの一つなのですが、PrologGHCの違いはありますが、やりたいことはたいへん似ているようです。


これにつられて、たくさんTwitterでつぶやいた。

    • -
  • Prologは完全性がない、という意味で十分な論理型言語ではない。第一階述語論理をプログラミング言語として解釈させるというKowalskiの論文(提唱)を正しく実装できなかったのが原因。
  • けれど、後から考えるとKowalskiの論文の方にも落ち度がある。それは、SLD演繹がそのまま実装できると思った点。具体的には数学の世界の集合とプログラミングの世界のリストがごっちゃになっている。
  • とはいえ、ユニフィケーションという強力な計算機構は不完全なPrologに夢を与えた。Prologはその後、第5世代プロジェクトの中心言語となり、並列処理機構の拡張がなされ、GHCという新たな言語を生み出す。
  • 一方、ユニフィケーションと並列処理に注目し、演繹処理でいう完全性を排除したのがErlangである。Erlangは、こうなると論理型とはいえない。関数型のラップを施した。
  • Erlangは、じゃ関数型か?それは違う。ユニフィケーションを計算機構に使っている以上、論理型である。Prologは完全性がなくても論理型と称されていることを考えると、論理型と言ってもあながちウソではない。
  • GHCErlangは計算モデルの似通った言語である。元来ユニフィケーションはcallerとcalleeの両方の変数に束縛の変化を与える。GHCはこれをそのまま適用しているが、Erlangはcallerにおける変化を制限している。ここが違う。
  • Erlangはなぜこうしたか?それは、ユニフィケーションが強力すぎて普通のプログラマの手に負えないと判断したからだと思う。
  • Prologは実用性の乏しい言語だと評される一方で、Lispより遙かに強力で実用性があるという意見もある。これはどちらも正しいと思う。
  • Prologが過去の失敗作として、未だに葬り去られてないのは、この点、つまりユニフィケーションの可能性にある。
  • 論理型言語としてもまだ確立していないし、並列分散機構もまだ確立していない。これに終止符を打った第5世代プロジェクトだけを見てはいけない。
  • プログラミング言語への嗜好が最近になって手続き型から関数型に移ってきたように思う。Lisp復権は、Paul Grahamの影響が大きいように思う。実際にWebシステムで大成功した。また、LLにおける関数型フレーバー(高階関数、closure)も影響している。
  • 論理型はいつ来るだろうか?これはさすがに見えないが、並列分散の世界では可能性がありそう。その良い例がErlangである。人は知らずに論理型を勉強していることになる。
  • 関数型の並列性は、ラムダ計算のチャーチ・ロッサー性にしかないと自分は考えている。これに対して論理型の並列性はほぼ無限に近い。Prologで言えば、AND/OR並列のOR並列部分であるが、SLD演繹の枠をはずすともっと出る。
  • SLD演繹の枠をはずすというのは、計算順序を変更するということで、昔、「部分計算」と呼ばれる研究でも取り上げられたテーマである。これが論理型では容易にできる。
  • 考えてみれば、λ言語をプログラミング言語として適用するという研究は、1960年代にあった。論理型言語の方では、ユニフィケーションがアルゴリズムとして完全であることが証明されたのは、1965年である。Lispは1962年。とにかく大昔だ。
  • コンピュータの進歩は著しいと言われるがそれは表層で、実際にはとてもゆっくりと研究が進んでいる。論理型言語についてはまだまだやることがたくさん残っているし、さっきの「部分計算」も過去の研究としてしまうのはおしい。