2008-08-31 [長年日記]
λ. あろは先生を問い詰める会 (ET Seminar)
あろは先生を問い詰める会というイベントに参加。
これはなんと、あろはさんが7時間ぶっ続けで発表し、問い詰める気満々の聴衆からすごい勢いでツッコミと質問が入るという恐ろしいイベントだった。 ツッコミまくってたお前が言うなという気もするけど。 特に、あまり本質的でない質問や、勘違いした質問を結構してしまって、そこはちょっと反省。 そんな過酷な環境にもかかわらず、長時間にわたって忍耐強く続けてくださったあろはさんには感謝するとともに賛辞を送りたい。
こないだの論文とあわせて、ETの目指すものと現状について大体理解できた気がする。
以下はとりあえず自分がした質問を中心に簡単に、感想や聞きそびれてしまったことなども含めてメモ。
命令型の理論とか仕様とか
ホワット・ア・ワンダフル・ワールド ET Q&Aでは「仕様 (what) の概念無し」、今回のスライドでも「そもそも理論が無い (あるけど，後付け （現場の要請ドリブン）)」と書いてあった。
そこで、「命令型言語でもホーア論理とかで仕様書けるし、最近JMLとか少し流行ってるよ」と聞いたら、ここで仕様と呼んでいるものは解きたい問題を記述したもので、関数の性質とかを記述したものではないとのこと。仕様をそう定義すれば確かにそうなんだけど、うーん……。
あと、他の方から「JMLとかは仕様ではなくアサーションでは」というコメントがあった。私の理解では「アサーション」は満たすべき性質の一部を記述したもので、「仕様」は満たすべき性質の全てを記述しつくしたもの。JMLはそのどちらも記述可能。
それから、命令型言語における仕様からの合成という話では、refinement calculus みたいな古典的な話もあるので、その辺りも少し質問してみたけど、仕様の概念が違うこともあって、あまり比較対象にはされていないような感じだった。
notは無理筋?
「notの定義例」のスライドでは後で書く否定の種類の方面の話に気をとられていたけど、落ち着いて考えると、ET 版の not が Prolog 版 not の問題を解決しているのか良く分からない。 というのも、結局PrologのSLD導出アルゴリズムの手続き的性質に依存していたのが、Dルールの手続き的性質に依存するようになっただけで、今回のセミナーではあまり触れられていなかったDルールの理論的扱いがわからないと何が変わったのか分からないので。
また、リファレンスマニュアルのnotの項の「(not *s)」の説明で「notは副作用を起こします。*s中の変数が実行中に変更されると、共有するnotの外側の変数も変更されます。この変更は、結果の真偽によりません」とあるけど、これはPrologの問題よりも遥かに凶悪なような気がする。 あろはさんも「条件部の結果が本体にひきずるのは問題」「実装で解決できるかも」というようなことを言っていた。
否定の種類
「notの定義例」というスライドのところで質問したが、利点として<URL:http://assam.cims.hokudai.ac.jp/et/indexj.html>に「否定を含む問題を正しく扱える」とあったのが気になっている。 Prolog でも negation as failure については問題なく扱える*1ので、これは negation as failure ではない通常の否定(classical negation とか strong negation と呼ばれる)を扱えるといっているのだろうか。
あろはさんによると、最近、DL(Description Logics) を扱う関係で ET で真の否定を扱える理論(?)が出来たとか。 論理プログラミングの文脈だと、通常の否定を扱うためには解集合プログラミング(answer set programming, ASP)のような枠組みが必要になってくるが、これは理論的にはともかく実装技術としては問題領域を限定した技術だと思う。 広い問題領域を対象としたETに対して実装されるとしたらどのような形になるのか興味深いところ。
構成的プログラミング
前日の LL Future での Lightning Talk 「超未来言語Gallina」で「仕様を効率的に実行可能な形に等価変換していくことを実現したのがGallina(Coq)」だと断言したyoshihiro503さんと、「Coq等はルールのように分解可能性のある(単体で正当性が議論できる)コンポーネントの集合で構成されているわけでない」というあろはさんとのバトルをちょっと期待してたんだけど、特にそんなことはなかった。
それはそうと、効率に関しては確かにちょっと問題はあるのかもと思うこともある。 というのも、Coqで書ける*2のは停止性が検査機によって自動的に判定出来る関数だけで、停止性が自動判定出来ない関数定義は書けないため、効率的だけど停止性が自動判定出来ない関数を書けずに問題になる場合が本当に無いのか自信がないため。Coqで“無限オブ無限”を書いたときにもちょっと思ったんだけどね。
palpal問題
ETの論文でよく出てくるpalindromeの例がpalpal問題と呼ばれてるのね。どうでもいいが、最近やっている英語版の逆転裁判で Detective Gumshoe (糸鋸刑事) が pal という呼びかけを頻繁に使っているので、それを連想してしまって、少しツボだった。
肝になる5番目のルール rv(*x, *y), rv(*x, *z) ⇒ {=(*y, *z)}, rv(*x, *y). にみんなの質問が集中していて、その結構な部分が「証明できる」が指すことについてだった気がする。
結局、このルールを自動導出出来るようになったのが最近というのは良いのだけど、「本当に厳密に D に対して ET ルールであることが証明可能になったのは，つい最近」というのが機械による自動証明だけを指しているのか、人間による証明についても不可能だったのかがよく分からなかった。
プライオリティ
これは私の勘違いでした。済みません。
(後で書く)
特殊化システムと書き換え系
「書き換え系としては多重集合の書き換え系(+情報変数)と思ってよいのか?」と聞いたら、その通りとのこと。多重集合の書き換え系なら線形論理の証明探索を書いたりするのに便利かもと思った。
それから、情報付き変数を使って特殊化システムを拡張可能とのこと。
書き換え系という意味では、Maudeの代数的仕様記述+書き換え論理という枠組みとの比較なんかも質問してみたかったが、これは質問しそびれてしまった。
圏論による定式化?
仕様空間とプログラム空間の理論は、channel theory とか chu space とか institution とか良くあるやつに似ているので、良くあるような感じで定式化してやれば良いのではないかと。 それで何か嬉しい結果が出てくるかはわからないけど。
あろはさんの研究とか
スライドにはあまり書いていないけど、私の理解では「命令型言語のプログラムの空間からETプログラム(Dルール)の空間への埋め込みを定義して、その逆変換としてDルールから命令型言語へのコンパイルを定式化」というのを一つのアプローチとして考えていたようだだった。
ただ、プログラムの埋め込みは仕様を何らかの意味で保たなくてはならないはず*3で、その部分があまり考えられていない気がして、その辺りを質問してみた。
そして、その議論からどうもDルールで副作用のあるアトム(?)の扱いが仕様上どう扱われているのかが気になりだして、それも聞いてみた。unification が substitution を生成するのと同じ扱いで、副作用については世界の枝分かれみたいな感じで扱われるとか。 ただ、一方でDルールにはNルールと違って正当性の概念がない(?)とか、どうもあまり理論的には扱われていないようでもあった。
ネタとかどうでも良い点とか
- S式版の記法で使われているasはassertの略でprolog-kr由来
- 『仕様からの合成』と要約してしまうとLyeeと同じになってしまってアレ
- 闇世界仮説。
- 高階質問状
- 「すごいパーツをいれれば僕はすごくなるよ」
他の方の感想など
- 埒を明ける日々: ET Seminar
- LLFuture と、等価変換セミナーに行ってきた - にわとり小屋でのプログラミング日記
- 等価変換理論集中セミナー2008（at 溜池某所） - ヤドカリデンキ商会（第一倉庫）
- 2008-09-03 - 兼雑記
- とりあえず俺はProlog知らなすぎだ - soutaroにっき
- <URL:http://morihyphen.hp.infoseek.co.jp/log2/200808.html#083118>
- <URL:http://page.freett.com/shelarcy/log/2008/diary_08.html#haduki312008>
- 8月31日は問い詰める会 - YasuyukiMiuraの日記
