…す。つまり、シーケントの証明は2次元の多圏において解釈されます。証明図の変形を考えれば、それは3次元の射（3セル）となり、3次元の多圏が登場します。というわけで、シーケント証明系の圏論的解釈には、複圏／多圏／高次圏が現れます。カリー／ハワード対応により、プログラムと論理は対応するはずですから、プログラムの意味論や解釈にも複圏／多圏／高次圏が現れるのは避けがたいでしょう。避けられないなら、プログラムの解析に複圏／多圏／高次圏をどう使うかを正面から考えるのが得策でしょう、たぶん。

…コマンド： カリー／ハワード対応」に書いたので参照して下さい。シーケントは次の形をしています。 A1, ..., An ⇒ X1, ..., Xm 最初から圏C上の意味論を考えることにします。Ai（i = 1, ..., n）、Xj（j = 1, ..., m）は、論理なら命題変数や論理式ですが、ここでは、圏Cの対象だと考えます。圏Cの対象をカンマで区切って並べたものをΓ、Δなどのギリシャ大文字で表します。対象の並びにも圏Cの対象としての意味を与えます。シーケントの左辺に出現…

…つは、一種のカリー／ハワード対応を利用したいからです。カリー／ハワード対応とは、論理とプログラムの対応のことです。“連言と含意を持つ論理”と“型付きラムダ計算”の対応が有名ですね。僕がこれから話題にするのは、“古典論理（風）のシーケント計算”と“コマンド言語によるプログラム”の対応です。コマンド言語とは、「コマンド」と呼ばれる処理の基本単位があり、コマンド達をパイプで結合してプログラムを作るスタイルのスクリプト言語です。具体例は、我々（檜山とKuwataさん）が開発しているC…

…ムダ計算（のカリー／ハワード対応）はできるので、捨てたもんでもないです。含意命題 A⊃B が ¬B×C という形では書けません。なにしろ「¬」がないので。しかし、もっと簡単な公式 A⊃B ≡ A×B が成立します。あるいは、¬A ≡ A なのだ、と思ってもかまいません。連言（AND）と選言（OR）が一致してしまい、さらに含意までも一致してしまったわけです。超コンパクト論理と言っていいかもしれません。否定を持たないコンパクト論理＝“超コンパクト論理” の構文論や証明論は述べませ…

…と、次のメリットがあるように思います。 評価方式が正しいことを形式的に証明できる（あくまで原理的なハナシですが）。 推論図と証明図を使って型推論が出来るかもしれない（確証はありません）。 それと、評価シーケントの証明図と実際の評価手続きとの対応関係が、LKとNKとの関係に似てる気がします。ある種のカリー／ハワード対応があるんじゃないのかなぁ？ あったら面白いですね。もちろん、表示的意味論がダメとか嫌いとかでは全然ないので、デカルト半環圏ベースの表示的意味論も並行的に使います！

…もみなせます。つまり、おおざっぱに言えば： デカルト閉圏であるならば、型構成子Tと総称関数fにより自己関手Fを表現できるのです。 *1:一般的には、そのようなことが保証できない、ということです。 *2:最近書いた「デカルト閉圏を計算するスタックマシン、シーケント計算、カリー／ハワード対応」とは少し記法が違います。[A, B] は B←A と同じ意味です。 *3:普遍対象（万能対象）と呼ばれる特別な対象Uがあれば、C全体を（したがって|C|も当然）C(U, U)に埋め込めます。

…す。 (f :: A, B⇒C) ≡ (Λ(f) :: A ⇒ C←B; Apply :: C←B, B ⇒ C) シーケント計算を少しでもご存知の方は、実行過程を描いた図がシーケント計算の証明図と似ていると感じたでしょう。はい、そうです。カリー／ハワード対応です。多圏における絵算を使えば、これらの事がより鮮明に直感的に説明できます。絵算を少しでもご存知の方は試してみてください。 *1:以前から説明に使っていた方法は、大きなラムダ式（関数）と小さなラムダ式（関数データ）です。

…す。ここでもカリー／ハワード対応が成立しています -- ある種のコンパクト論理と平面ラムダ計算とテンパリー／リーブ圏の関係は、アブラムスキーの次の論説（以前の圏論勉強会テキスト）で解説されています。 "Temperley-Lieb Algebra: From Knot Theory to Logic and Computation via Quantum Mechanics"（http://web.comlab.ox.ac.uk/oucl/work/samson.abrams…

…は何なのか カリー／ハワード対応 例外処理のコードパターン 例外コンバーターをパラメータとする例外処理 どこかで見たような推論規則 それにしても不思議だ とても重要な注意土曜の晩に、口汚く差別用語を使ってまで強調したことがあります。それは、圏の射を、プログラミング言語の関数や手続きだと思い込むのはやめてくれ、ということです。集合と写像の圏をモデルに使う場合でも、写像によりモデル化されるものが「プログラミング言語の関数や手続き」ってことではありません。プログラム全体のなかで、任…

「カリー／ハワード（Curry-Howard）のお絵描きを楽しもう」にて： シリーズ3回全体を総括しなきゃ、とか思っている間に4月になってしまいました。「次はどうしようか？」とかもいずれ書くつもりです セミナー前後の事務的処理がどうも苦手で、けっこうそれが負担で苦痛だったりするんですが、、、、4月もやります！ なんとなく、そこはかとなく予告していたようにモナドシリーズの第1回。全体はたぶん3回。モナド以外のネタも考えたのですが、次の事情でやっぱりモナドにしました； ラムダ計算…

…)だから、「カリー／ハワード（Curry-Howard）対応をうんと一般化するとどうなるか」みたいなネタで。以前紹介したことがあるバエズ＆ステイのロゼッタストーン論文がarXivに入っていました。 題名: Physics, Topology, Logic and Computation: A Rosetta Stone 著者: John C. Baez, Mike Stay URL: http://arxiv.org/abs/0903.0340 ページ数: 73 この論文の最…

※ この記事はエイプリルフールとは無関係ですよ。3月19日にやったセミナー、それとシリーズ3回全体を総括しなきゃ、とか思っている間に4月になってしまいました。「次はどうしようか？」とかもいずれ書くつもりですが、今日は、superstring04さんが、Kuwataさんとは別な雰囲気のまとめを書いてくれたので、それに応答します。 http://d.hatena.ne.jp/superstring04/20090328/1238211198 superstring04さん曰く： …

…バリ、これがカリー／ハワード対応だ 最後に はじめにKuwataさんに刺激され、僕もこの長いエントリーを書きました。Kuwataさんのレポートと、当エントリーにより、「技術者／プログラマのためのラムダ計算、論理、圏」セミナー第3回の雰囲気と内容を、かなりの程度伝えることができるだろうと思います。 スライド資料は http://www.chimaira.org/archive/slide20090319.pptx ← クリックするとファイルがダウンロードされます。 参加者のみな…

…回)の紹介：カリー／ハワード対応」をご参照ください。今回から（今回だけ）参加でも、内容の2/3は自己完結的ですから大丈夫です。 申し込みページ（とそのバックエンド）をErlang+YAWSで作ろうかということだったのですが、なんか間に合いそうにありませんな。手作業で受け付けかな、やっぱり。 というような事情で、申し込み受け付け開始が遅くなってしまいました。ゴメンナサイ。受け付け作業は手作業にします（間に合わないからしょうがないや）。次のページから申し込み、または hiyama…

…たる動機は、カリー／ハワード対応を紹介したかったことです。カリー／ハワード対応は、命題論理と型付きラムダ計算のあいだに対応関係があり、その対応により「命題論理とラムダ計算は事実上同じものだとみなせる」ことを主張します。カリー／ハワード対応というと、なにか小難しくて近付きがたいような印象がありますが、ラムダ計算を“お絵描きで行う”手法（pictorial calculation）を使えば、とても簡単に説明できてしまいます。失礼なのを承知で言ってしまえば、「こんな当たり前のことが…

…全体の目標はカリー／ハワード対応です。24日は、ベータ変換の絵が描けるようになればそれでヨシだと思っています。さて、すごく悩んでいたことがあります； それは絵を「下から上に描く」か「上から下に描く」かです。最初の段階では「下から上」のほうが分かりやすいと思います。が、先ほど、「上から下にしよう！」と決心しました。理由のひとつは、僕自身が最近「上から下へのオダンゴ図」を描いているからです。次の図は、バエズ（John C. Baez）のテキストから抜いたものです。バエズは「上から…

…話題、目標はカリー・ハワード対応の簡単な事例を理解することですね。デカルト閉圏を使ったモデル論は、ほんのサワリくらい。ラムダ計算に関して言うと、以前書いた次のエントリーをベースにします。 JavaScriptで学ぶ・プログラマのためのラムダ計算 絵を描いて学ぶ・プログラマのためのラムダ計算 プログラミング言語の教養や基礎知識としてラムダ計算を知りたい方、上記のエントリーを読んで、なんか分かったような気もするが、いまいち腑に落ちないなー、という感じの人がターゲットです。ただし、…

…ルト閉圏上でカリー／ハワード対応を作ると、ゲンツェンNJとラムダ計算の対応が付く。コンパクト閉圏や自立圏で同じような手続きが遂行できれば、量子的NJと量子的ラムダ計算に関するカリー／ハワード対応が作れるはずだ。その計算体系は、ミクロな現実世界で実際に起きている計算現象の定式化に使えるのかもしれない。アブラムスキー一派は、そのへんを（も）ねらっているのだろうか？[追記]「EPRペア」という言葉もあるみたいね。ベル状態と同義？ 別物？[/追記] *1:スターは、対象に対してだけ定…

…る、ってのがカリー／ハワード対応。今、説明はしないけど*1。さて、それにしても、先の等式はいったいどこから来るのか。まー、天下りに仮定してもいいのだけど、「どこから？」と問うなら、それは「(-×A)と[A, -]の随伴性」以外の理由は考えられない。「(-×A)と[A, -]の随伴性」を真面目に調べれば、カリー化（関数抽象）と適用評価の関係は出てくるはず。実際のところ、Λ-1:C([A, B], [A, B])→C(A×B, B) という随伴を与える同型が自然変換（の成分）であ…

… A Term calculus for Intuitionistic Linear Logic →http://research.microsoft.com/~nick/tlca93.ps 三位一体を確認する方針としては； 対称モノイド閉圏の上で解釈できる論理計算（自然演繹、またはシーケント）とラムダ計算を定義する、その論理が閉圏をモデルと考えて“完全”であることを示す、論理と（型付き）ラムダのあいだはカリー／ハワード対応で結び付ける、と、そんな感じでしょうかね。[/追記]

…ようなもの（カリー・ハワード対応）ってことですね。さてそれでは、我々にとって一番お馴染みで一番基本的な古典論理はどんな圏と対応しているのでしょうか？ ストラスバーガーによれば、なんと、古典論理（ブール論理）に対応する圏が一筋縄では定義できないそうです。古典論理の証明を、標準的な形にして整理する部分が難しい、と。そこで、"What is a proof?"なる問＜とい＞がシリアスになるわけです。… が、これ以上は僕の手に余るので、原論文や関連文献をあたってみてください。お後がよ…