檜山正幸のキマイラ飼育記 このページをアンテナに追加 RSSフィード Twitter

キマイラ・サイトは http://www.chimaira.org/です。
トラックバック/コメントは日付を気にせずにどうぞ。
連絡は hiyama{at}chimaira{dot}org へ。
蒸し返し歓迎!
このブログの更新は、Twitterアカウント @m_hiyama で通知されます。
Follow @m_hiyama
ところで、アーカイブってけっこう便利ですよ。

2015-12-08 (火)

ハイコンテキストな定数・記号の解釈

| 12:19 | ハイコンテキストな定数・記号の解釈を含むブックマーク

演算子オーバーロードに関する記事「コンピュータは「掛け算は足し算とする」を理解できるか」に対して、id:kmizushimaさんとid:matarilloさんが、それぞれScala、F#で対応するサンプルを書いてくださいました。ありがとうございます。

Scala、F#でも、C++と同じことができるのが分かります。

でもね、まだ不満があるんですよ。

ソースコード内で 1 + 1 と書けば、さすがにこれは2になります。数値をmin-plus半環の要素だと思って書いても、コンパイラは心のなかまでは察してくれません。

ここが不満。1 + 1 と書いたら答が1になって欲しい。いや、もちろん「心のなかまで察してくれ」とは言いません。ヒントは与えますが、それが 1_mp + 1 のような接尾辞ってのはどうもなー、ということです。

我々人間がコミュニケーションしている状況では会話のコンテキストがあります。min-plus半環を話題にしている“トロピカルなコンテキスト”では、ホワイトボードに 1 + 1 と書けば、定数リテラル1はmin-plus要素と解釈されるはずです。

C++でも名前空間の宣言があります。using namespace std; とすれば、スコープを明示するstd::接頭辞を省略できます。つまり、名前の解釈が変わるわけです。であるなら、記号やリテラルの解釈も変わっていいじゃないか、と思うわけです。例えば、using context tropical; とかすると、定数リテラル1の解釈が1_mpとなる、とか。

Coqにはnotationとinterpretation scopeというメカニズムがあり、Open Scope tropical_scope のようにして記号の解釈を変えられます。しかし、厳密な型付けの都合から、同じ名前を同時に(同一文脈で)異なる型に割り当てることはできません。Coq型クラスのラベル名(フィールド名)を局所化できないという酷い話もあって、結局、名前の増加を防げません。

僕が名前(記号やリテラルも含む)のオーバーロードに拘るのは、名前の増加に耐えられないからです。

Coqで半環:アンバンドル方式の例として」より:

名前の増加にはシンドイ思いをしたので、人間が使うシステムではいかにして名前の個数を減らせるかはとても重要な課題だと思っています。共通の性質・構造を持つモノを同じ名前で呼べることは、ものすごい節約・効率化・汎用化につながります。

文脈依存の多義語は、ときに混乱をもたらす弊害もありますが、有限少数の語彙を効果的に使ってジェネリックな記述や推論を可能にするというベラボーなメリットがあります。だから、コンピュータとのコミュニケーションにも文脈依存だが適切にコントロールされた多義語を使いたいのです。

shiroshiro 2015/12/08 16:26 言語によっては数値リテラルの基数を文脈で変えられるものがありますから、型を文脈で指定できても確かに良さそうにも思えます。

しかし!我々はUnicode時代に生きているので、𝟙+𝟙 とか 𝟭+𝟭 とか ?+? とか書く手があるかもしれません。

shiroshiro 2015/12/08 16:27 ああ、コメント内のUnicode文字が残念なことになってしまった…

m-hiyamam-hiyama 2015/12/08 19:21 shiroさん、
> ああ、コメント内のUnicode文字が残念なことになってしまった…
𝟙 は、MATHEMATICAL DOUBLE-STRUCK DIGIT ONE' (U+1D7D9) で、
𝟭 は、MATHEMATICAL SANS-SERIF BOLD DIGIT ONE' (U+1D7ED) ですね。
?+? は何だったんだろう?

> 型を文脈で指定できても確かに良さそうにも思えます。
今の技術なら、トークナイザー/パーザーを動的に変えるのは難しくはないでしょう。
一部分を局所的に見たとき、意味不明だったり誤解を招いたりという問題はありますが、どんなコミュニケーション形態でもそれはあることなので、致し方ないと思います。
Unicode文字利用に関して言えば、関数抽象が「λ」で書けたり、論理式が「∧」「∨」「¬」で書けるのは、とても気持ちいいです(Coqがサポートしている)。