Yet Another Ranha このページをアンテナに追加 RSSフィード

2009-06-15

ギレンさんが

01:20 | ギレンさんがを含むブックマーク ギレンさんがのブックマークコメント

「諸君らの愛した表示的意味論(R5RS)は死んだ。なぜだ?」

と述べられた時、シャアさんはR6RSに鑑みて、ひいてはプログラミング言語意味論を思ってどう答えるのでしょうか?

教えてください。m(_ _)m

ここに至った流れ

藍ちゃんの「表示的意味論て要らない子なん?」ていう質問について考える

紆余曲折

領域理論から圏論へと接続したい どうすれば はっ!領域方程式はどうだろう。逆極限法とか!

領域方程式でググる http://lambda.bugyo.tk/hatena/r5rs.html つまり・・・説明になっとらん!

"Scott-Strachey Approach to Programming Language Theory"は読んでみたい

ところで、歴史的な流れで書くと、ストレイチー・スコットなんでは無いでしょうか。どうなんでしょうか?

ところで、改めてですけどSchemeはR5RSで表示的意味論なんて(すいません なんて とか書いちゃって)何故に使ってるんだろう

http://practical-scheme.net/wiliki/wiliki2.cgi?Scheme%3A%E8%A1%A8%E7%A4%BA%E7%9A%84%E6%84%8F%E5%91%B3%E8%AB%96

なんとR6RSでは操作的意味論か

http://cl-www.msi.co.jp/solutions/knowledge/lisp-world/articles/three-dogmas-of-scheme

うーむ・・・。表示的意味論のコンテキストだ、というのは分かる物の、操作的意味論はパクって取り込んじゃってるし

分からんから質問しよう。 <=> 今ココ

追記

なんとか考査と某アレで盛り上がってる期間で私はその所為で盛り下がっているので、一段落付いてからこれに関しては書きます。すいませんなんかコメント盛り上がってるのに言い出しっぺが何も書いてなくて・・・。

時間が取れないとちゃんと書けそうにないので、なのでまぁ一段落付いてからです。本当に申し訳ないです。

h_iwkh_iwk 2009/06/20 02:00 自分もわからない。ただ、表示的意味論と操作的意味論の折衷したものと説明されるSOS(Structural Operational Semantics)という意味論をR6RS採用せず、なぜ操作的意味論を採用したのか?という疑問がある。(ちなみに自分はSOSは全然わかっていないのでそもそも大間違いなのかもしれないけど、”折衷したもの説明される”と書いたけど、どこでその記述を見つけたのかも分からなくなってしまっているし。)

>領域理論から圏論へと接続したい どうすれば
これは自分も考えている。おそらく詰まっているところというのは、圏の射をどう考えればよいか?というところだと思う。原因としては関数概念の曖昧さ。
一般に述べられる”関数”という言葉には曖昧性がある。
んで、その曖昧性を排除してちゃんと形式化した関数(対の集合としての関数、もしくは関数合成から公理化してしまった関数。)というのが、ちょうどScott連続関数と一致する、ということになるようだ。(まだよくわかってない。)

まぁ参考までにコメント。別に返事はいらないです。

cafeliercafelier 2009/06/20 08:33 今「操作的意味論」と何も注釈無しで言ったらSOSのことを言う(…というと言い過ぎかもしれませんが、真っ先に想起されるものはそれ)ような気がします。もちろんR6RSの採用している意味論もそうなっています。

h_iwkh_iwk 2009/06/24 02:34 >>cafelierさん
その話、すごく興味あります。
正直言って、表示的意味論、操作的意味論ともによくわかっていないので伺ってもあまりピンとこないと思うので、うーん、なリアクションに成ってしまうと思うのですが、SOSって表示的、操作的意味論と比較した場合、どこに利点があるのでしょうか。

どういった問題意識からSOSが出てきたのかさっぱりわからないのです。
もしよろしければ、お教えください。

h_iwkh_iwk 2009/06/25 21:59 対象領域をU、解釈関数をIとしたとき、表示的意味論において<U,I>はテクニカルタームとして<<構造(structure)>>と呼びます(情報科学における論理p66など参照。)けれど、SOSはその表示的意味論的な構造(structure)を保持する操作的意味論ということでstructural operational semanticsということではありませんか?

スローガンで言えば、
表示的意味論:関数とはグラフである(関数の返り値が分かっているので構造は定義できる。)。
操作的意味論:関数とは変換操作である(関数の返り値はわからないので構造は定義できない。)。
ですが、SOSの場合、本当に折衷と考えて、
SOS:関数とは構造を定義できるような変換操作である。
というところですかね。
そう考えると、
http://www.ece.northwestern.edu/~robby/pubs/papers/scheme2005-mf.pdf
これがすっきり読める気がするんですよ。

cafeliercafelier 2009/06/26 00:05 SOSの"structural"は、そちらの意味の構造(structure)とは特に関係ありません。「プログラムのsyntax的な構造に関する帰納的な定義(structural induction)で定めた操作的意味論」が由来だったと記憶しています。

表示的意味論の解釈関数Iも普通は文法構造に関する構造帰納で定義するので、この点において、SOSと表示的意味論は似ています。逆に、違うのは、表示的意味論は構造帰納でプログラムを領域Uの元に対応づける(Program→I)のに対して、SOSでは構造帰納によってプログラムの変換操作(Program→Program)を定義することろです。言い方を変えると、表示的意味論はプログラムの"意味"を一発で与えるのですが、SOSは、"プログラムを1ステップ実行すること"の"意味"を与えます。プログラムの意味そのものの意味は"その1ステップを終わりまで繰り返すこと"的に解釈します。

"古い"操作的意味論も、プログラムの意味を一発で与えるのではなく、直接的には"プログラムを1ステップ実行すること"の意味を与えます。この意味でSOSは操作的意味論に含まれます。逆に違いとしては、SOSは構造帰納で1ステップの意味を定義しますが、"古い"操作的意味論では、(例えばSECDマシンのような、WAMのような、アセンブラのような)非常にプリミティブな命令の列へのプログラムのコンパイル方法を提示します。そのプリミティブな命令1個1個の"(ある種表示的な)意味"が、プログラムを1ステップ実行することの意味になります。

cafeliercafelier 2009/06/26 00:06 SOSに限らず操作的意味論の表示的意味論に対する強力な利点として、意味論を使って何かの性質を証明するときに「プログラムの実行ステップに関する帰納法」という技を使える、というポイントがあります。この技法が使えることでいくつかの証明が非常に簡単/可能になったりします。例えば「静的型がついたら型安全」という性質を示すのに、「静的型のつくプログラムの表示的意味が⊥(対象領域Uの最小限)ではない」のを言うかわりに「型がつくなら1ステップは実行を進められる&進めた先も型がつく」という、「1ステップだけ証明すればあとは帰納法さんがなんとかしてくれる!」作戦で行くのは楽です。あとそもそも、新しく言語を作ったときにSOSは比較的サクッとお手軽に定義できますが、適切な表示的意味論的構造(structure)を定義するのはそう簡単ではないですよね、というのも比較しての利点ですね。


"古い"操作的意味論と比較した場合は、プログラムの文法的構造に関する帰納的定義になっている、というのがSOSの利点になっています。そもそも意味論を使って証明したい「性質」って、プログラムの構造に沿って述べられることがほとんどです。さっきの例だと、静的型システムは「ifの条件部の型はbool、==の左右は同じ型、…」などなどプログラムの構造で定義されてます。間違っても、SECDやWAMにコンパイルした後のその抽象マシンの構造に関して定義されたりはしません。なので、"古い"操作的意味論での1ステップで帰納法を回そうとしても、扱いたい性質と定義されてるレイヤが違うので、議論がちぐはぐになってうまく回りません。そういうズレが起こりにくい、というのがSOSの"古い"操作的意味論に対する利点です。

cafeliercafelier 2009/06/26 00:07 まとめると、「1ステップ1ステップに話を分解して考えられるので簡単」「領域理論のような大変な道具立ても要らないので定義するのは簡単」という操作的意味論の利点は保ったまま、「プログラムの構造に関して帰納的に定義されているので、プログラムに関して述べたい証明したい諸々と話がマッチして綺麗」な表示的意味論の利点を合わせ持てるようにしたのがSOS、と考えてよいのではないかと思います。

h_iwkh_iwk 2009/06/26 00:57 おーーーー!丁寧にありがとうございます。ていうか、間違ってましたか。orz

とりあえず、自分の理解を述べてみます。
”古い”操作的意味論:とりあえず、あるマシン上でそのプログラムが動くならば、そのプログラムのプロセス1ステップ1ステップを節操無くそのプログラムの意味として対応させてしまう。例えば、x86アーキテクチャで動いているなら、いろいろ考えるのも面倒くさいしそのまんまx86の命令に対応させてしまう。(?)
SOS:プログラムのプロセス1ステップ1ステップに対応させてしまうところは同一であるが、マシンの形式仕様はあらかじめ定めておく。Prologであれば、Horn集合における論理の導出システムをそのプログラムが動く形式系と考えて意味を対応させる。(あれ、でもPrologは公理的意味論か。)

という感じに理解しました。この理解でどうでしょうか。

h_iwkh_iwk 2009/06/26 01:13 ただ、そうなると、操作的意味論ではUの特定の対象は指示できないということになるんですか?あくまでProgram->Programの射があるだけで、Program->Uという射は存在しないのですよね?

cafeliercafelier 2009/06/26 02:52 もう1段ずらした方がいいかもしれません。

"古い"操作的意味論でも、あらかじめ形式仕様を定めたマシンの命令に対応させます。(PrologだとWAMなどですね。さすがにx86の命令だと落とした先の形式的な意味が定かでないので、それをもって意味と言うのは微妙…という感覚です)
SOSでは…マシンと言えばマシンでしょうか、ただ、特に、""プログラムそのものの文法構造にそのまま従う形で定義された形式マシン""に対応させます。(なので、Prologだと、Horn集合(=Prologのプログラムそのまま)を使って定義された論理導出システムに落とすのは確かにSOS的です。)

# ついでに。ボトムアップ戦略で得られる項の集合がPrologプログラムの意味である、とするのは、表示的意味論的なやり方ですね。公理的意味論は、(私の感覚だと)副作用のある言語に対して考えるのが基本なので、PureなPrologに対してはあまり考えることがないかもしれません。

>操作的意味論ではUの特定の対象は指示できないということになるんですか?
はい、そうです。そもそもその"U"のような物を考えません。

# 強いて言えば「Program->Programの変換を繰り返していって止まった終点(or 終点での変数割り当て等)」という対象を指すのだ、と考えることはできなくもないです。が、その場合U=Programだったりして、表示的意味論の場合ほどは意味がないです。

cafeliercafelier 2009/06/26 02:55 (なので 0:05の投稿でアセンブラのような、と書いたのは勇み足でした。そこはナシで…(^^;)

h_iwkh_iwk 2009/06/26 23:49 一日考えてみました。

>""プログラムそのものの文法構造にそのまま従う形で定義された形式マシン""
これがキーなのですね。もう一度要約を試みてみれば、
SOSというのは、
”プログラムの理論的な取扱いが容易な形式マシン上における操作的意味論”
ということなのですね。核心的な部分については理解できた気がします。

>公理的意味論は、(私の感覚だと)副作用のある言語に対して考えるのが基本なので、PureなPrologに対してはあまり考えることがないかもしれません。

この部分についてはすいません。ちょっと勉強不足でよくわかりません。今度調べてみます。

># 強いて言えば「Program->Programの変換を繰り返していって止まった終点(or 終点での変数割り当て等)」という対象を指すのだ、と考えることはできなくもないです。が、その場合U=Programだったりして、表示的意味論の場合ほどは意味がないです。

これはかなり興味のある話です。λ計算における正規形(normal form)、または、マーチンレーフの言うところのカノニカルなものに対して対象を対応させようということですね。
実際確認していないので誤っている可能性があるのですが、『プログラム意味論』(横内寛文著 絶版)の中では、その終点を操作的意味論の意味とする、となっているらしいです。あくまで参考として一応。
c.f. http://www.geocities.jp/minao_kukita/files/kukita_ronso08.pdf

さらに、調べてみるとSOSのPlotkinがSOSの一種(?)のGSOSというものを用いて表示的意味論、操作的意味論の一致させるような研究をしていました。(読んでみたのですが今の私にはちょっと難しすぎました。)
http://citeseerx.ist.psu.edu/viewdoc/download;jsessionid=30C6020D417532E3B4AF5795A297907D?doi=10.1.1.47.730&rep=rep1&type=pdf

関係の無い話になりますが、個人的につながりがあるだろうと思っていた、表示的意味論、操作的意味論、SOS、圏論、Aczel等々がこの論文に全て出てきているんですよね。個人的にかなりの収穫です。

懇切丁寧に教えていただきありがとうございました!非常に参考になりました!

h_iwkh_iwk 2009/06/27 00:04 「誤っている」だとちょっと意図と違ってpdfの方に対して酷いですね。「勘違いしている」で。
横内本は持ってないんです。

h_iwkh_iwk 2009/06/27 11:51 なんというか、ranhaさんのブログなのに除け者感を出してしまいました。
ranhaさんにむけて自分の理解を述べると、そもそも意味論と言うのは、数学とか計算機理論の話と言うより、多分、言語哲学な話題なのです。

SOS,GSOSの話を抜けば、計算機の意味論として
表示的意味論 v.s. 操作的意味論
という対立軸を考えられます。でも、実は50年くらい前に哲学の世界でも類似したものがあって、
ラッセルの表示の理論 v.s ストローソンの指示の理論
「On Denoting」     「On Refering」
(*下に示したのは代表論文の名前)
という似たような対立軸の元で論争がなされたのです。

それで、どこかで記述を見つけたというわけではなく、あくまで自分の理解としてなのですが、表示的意味論はラッセルの理論を元ネタとしており、操作的意味論はストローソンの理論を元ネタにしていると考えると、話しが分かりやすくなります。

参考図書としては、ライカンの言語哲学あたりがいいかな。
http://www.amazon.co.jp/dp/4326101598

h_iwkh_iwk 2009/06/27 12:16 あと、もう毒を食うなら皿までで書いてしまう。

論理から数学を構成する新フレーゲ主義(新論理主義)としてはProgram -> Uの射が無くても数学的対象は指示できますね。と書いておく。