このブログの更新は Twitterアカウント @m_hiyama で通知されます。
Follow @m_hiyama

メールでのご連絡は hiyama{at}chimaira{dot}org まで。

はじめてのメールはスパムと判定されることがあります。最初は、信頼されているドメインから差し障りのない文面を送っていただけると、スパムと判定されにくいと思います。

参照用 記事

感動か効率性か

随伴のニョロニョロ関係をTypeScriptで確認する」で話題にした2つのニョロニョロ関係式:

  1. εP(X) \circ P(ηX) = idP(X)
  2. E(εX) \circ ηE(X) = idE(X)

一番目だけをTypeScriptで書いてみました。TypeScriptプログラムで出来ることは、幾つかの個別事例を確認することだけで、等式の証明ではありません。手と紙を使えば等式の証明も出来るだろうとやってみると、二番目の等式が難しい。

「難しい」と言うより、計算の道具が揃ってない、というのが実状です。集合圏Setを仮定して、具体的な写像の計算をすればニョロニョロ関係式を示せますが、形式的な計算体系のなかでやろうとすると途方に暮れます。

基本的な事実が定式化できないとか、やたらに複雑になってしまう、って何かオカシイです。どうにも致し方ないケースもあるでしょうが、ニョロニョロの事例では、形式的な計算体系に不備があるとしか思えない。

ニョロニョロの計算では、ラムダ計算(ベータ変換やイータ変換による項の変形)と型の計算とシーケント計算を使います。意味論的な対象物はデカルト閉圏なのですが、計算手法はあっちこっちから寄せ集めてハイブリッドな計算をします。

そもそもこの状況がオカシイと思うのですよ。ラムダ計算と(型理論における)型の計算と(論理における)シーケント計算は、歴史的経緯としては別々に誕生し独自に発展したものでしょう。しかし現在では、カリー/ハワード対応により、同じものだと認識されています。

「同じもの」とは、同じ意味論的な対象物を指していて、表現としての構文が違うだけ、ということです。同じ意味論的な対象物とは、デカルト閉圏やその変形・拡張のことです。そうであるなら、同じ対象物に対する異なる構文を異なるままにしておく意義ってあるんでしょうか?

現状では、ラムダ計算とシーケント計算では、それぞれ別な記号法や用語法が使われていて、一緒に使おうとするとメチャクチャ使い勝手が悪いことになります。型理論型理論で、また別な世界を形成しています。

そろそろ、歴史的な経緯は無視して、記法・用語法・定式化を統合してもいいんではないでしょうか。計算論と型理論と論理を別々に勉強して、それでやっとカリー/ハワード対応ではあまりにも大変過ぎます! 歴史や伝統に拘らなければいくらでもショートカットはあるでしょうに。

最初にカリー/ハワード対応を知ったとき、「オオーッ」と感動します。それは、まったく別な分野でまったく別な形で定式化された2つのモノが実は同じだったという驚きからでしょう。カリー/ハワード対応が自明に見えてしまうような統合的な定式化をすれば、感動も驚きも味わうことはできなくなるでしょう。

感動が失われる -- いいんじゃないの、それで。はじめて発見された時は驚くべき事実でも、何世代か後には常識になってしまう、それが進歩なのだと思います。苦労して登った山頂からの景色は、その苦労のゆえに感動的かも知れません。しかし、単に景色を眺めたいならロープウェイだろうがヘリコプターだろうがかまわないでしょう。トレーニングを積んだ登山者しか登れないコースしか存在しないって状況は前近代的で良くないよ。