…る道具です。カリー／ハワード／ランベック対応の処方箋に従えば、カップル化可能圏から論理計算（シーケント計算／自然演繹）のシステムを得ることは出来ます。カップル化可能圏が半コンパクト構造（コンパクト閉構造を弱めたもの）とダガー構造を持つことから、幾分かは線形代数の計算とも似ています。この計算システム（仮称・カップリング計算）の計算を、日常論理の計算と解釈することが（ある程度は）可能だろうと思っています。カップル化可能圏／カップリング計算の目的は、ベイズ確率の計算とデータベースの…

…き（例えば、カリー／ハワード／ランベック対応）にも使えそうです。事例 1：モナドの結合律モナドを (A, μ, η)/C in Cat という形で表しましょう。モナドの素材〈ingredient | constituent〉は： C は圏 A は関手 A:C→C μ は自然変換 μ::A＊A⇒A:C→C （'＊'は図式順の結合記号） η は自然変換 η::IdC⇒A:C→C （IdCは恒等関手） モナドが満たすべき法則 -- 結合律、左単位律、右単位律のなかで、結合律だけを扱…

… 1/2： カリー／ハワード対応のために 型付きラムダ計算 構文論 再入門 2/2： カリー／ハワード対応のために 内容： 微分計算の構文 型システム 型判断と型推論 解釈不可能／困難な式の例 何がダメなのか どうすればいいのか 微分計算の構文この記事の目的は、ちゃんとした形式的体系を構成することではなくて、普通の微分計算の手順を明確化することです。なので、構文に関しては大雑把に記します*1。出てくる基本記号は： 特定の値を表す定数記号 ： 0, 1, -10.2, π（円周…

…*1:証明図と呼ばず推論図と呼ぶには事情があります。「証明」という言葉があまりにも曖昧なので、使用しないことにしました。自然演繹風の証明図を推論図、シーケント計算風の証明図はリーズニング図と呼びます。これで曖昧さは無くなりますが、世間の習慣とズレてしまうことが問題です。 *2:「相当する」は、カリー／ハワード対応により関係付けられることを意味します。 *3:推論／証明とは呼ばずリーズニングと呼ぶのは、先の注釈で説明した事情です。 *4:もう少し一般的な形にすることが多いかも。

…のでしょう。カリー／ハワード／ランベックの教義によれば、「圏論、論理、型理論／プログラム論」のあいだには対応関係（類似性）があるはずです。特徴述語論理をあいだにはさむことによって、カン拡張に対応する型理論／プログラム論的概念が見つかるかも知れません。限量子が関係するなら、依存型っぽいナニカかも知れません（よく知らんけど）。 *1:最近、僕がよくこのテの注意書きをするのは、国語辞書的な解釈に拘る人が、どうも相当数いるらしいと気付いたからです。「拡張してないのに、なんで『拡張』な…

…インの話題はカリー／ハワード対応でした。が、他の話もあって、「プログラムの停止性判定の不可能性」も入れていました。「プログラムの停止性判定の不可能性」は、主題ではなかったので急ぎ足でしたが一応の説明をした記憶があります。その当時の記録は： 「ラムダ計算、論理、圏」セミナー（第1回）の報告＋次回の告知 あっ、言い忘れていた：なんで停止性なのか？ 「プログラムの停止性判定の不可能性」は、「ゲーデルの不完全性定理」の仲間です。どちらも、メタレベルから分析することにより、ある種のアル…

…貼り合わせ カリー／ハワード対応の新しい仲間 独身男性にもコウノトリはモナドを運んでくるのか カン拡張っぽいアレコレ データベースとカン拡張と思い出 *1:[追記]もちろん、整理すればシッチャカメッチャカなんてことはありません。断片的な情報を脈絡なく収集すると、シッチャカメッチャカな印象を受けるであろう、ということです。[/追記] *2:カン拡張の定義が何種類かあります。そのことは、nLabエントリー https://ncatlab.org/nlab/show/Kan+ext…

…ルの作り方 カリー／ハワード対応への障壁 言い残したことなど次のような話題がまだ残っています。 トランスフォーマー 指標に対する様々な操作 相対指標、部分インスタンス、指標のパラメータ化 プロファイル推論／指標推論 データストアオブジェクト さらにオブジェクト指向 データベーススキーマ メイヤー流の契約モデル 名前構造と名前管理 表明付きの指標 高次の指標 このなかで最も重要なのはトランスフォーマー（Standard MLのfunctor相当）です。これ、ホントゥに重要なんで…

…ルト閉圏も、カリー／ハワード対応の観点からは重要です。なお、デカルト閉圏については、過去の記事で色々と書いています。 なぜ「光が影を作ること」と「主張の一部を再主張すること」が関係するのか；あるいは、デカルト圏入門 (2007年) 圏論的指数の周辺：ラムダ計算、デカルト閉圏、ノイマン型コンピュータ (2007年) 圏論的指数の定義 (2007年) デカルト閉圏におけるお絵描き計算の基礎 (2007年) モノイド閉圏、オダンゴ、留め金、池袋 (2008年) 演繹系とお絵描き圏論…

… 1/2： カリー／ハワード対応のために」の続きです。前回 1/2 の内容： 予備知識と参考資料 大きなラムダ計算とは何か 概要と目標 集合と写像に関する基礎的事項 型システム 今回 2/2 の内容： 疑似ラムダ項の構文 ラムダ項の構成と型付け 大きなラムダ式のアルファ変換 大きなラムダ式の構造規則 マルチ代入 型証明系TPS1 TPS1における代入消去と型付けの一意性 ラムダ計算のポリ化： 型証明系TPS2 もうひとつの型証明系TPS3 圏LLEの定義 圏LLEのモノイド構…

「カリー／ハワード対応への障壁」において、カリー／ハワード対応（Curry-Howard correspondence/isomorphism）をうまく説明するのは難しい、という話をしました。その記事の最後の一言は： いまだベストと思える説明に届かず。 その後も、ベスト（に近い）説明とはどんなものかと考えています。以前から僕は「大きなラムダ計算」という方法を使っているのですが、これをベースにするのがやはり良いように思えます。大きなラムダ計算は型付きラムダ計算の定式化のひとつで…

…いる」というカリー／ハワード／ランベック対応（Curry-Howard-Lambek correspondence）の確率版があるような気がします。オマケ：マルコフ・テンソルと関数の一覧矢印が'→!'と書いてあるのは関数です。 test: 感染? → 陽性? effect: 感染?×投与? → 発病? infection: 1 → 感染? develop: 感染? → 発病? infection2: 1 → AB感染? develop2: AB感染? → 発病? loss: …

「カリー／ハワード対応を小一時間で説明してみようか」と思ったのですが、すぐさま、この企ては諦めました。無理だよな。もちろん、ある程度の準備が必要という事情がありますが、分かりやすい対応を作る際に障害物・障壁があるんですよね、… ったくもう。愚痴を書きます。内容： 何と何を対応させるのか シーケント計算を考慮する 邪魔だが無視できない存在としての自然演繹 悩む！ 何と何を対応させるのかカリー／ハワード“対応”なんで、何かと何かを対応させるのでしょうが、何を対応させるの？ オーソ…

…、あるいは“カリー／ハワード対応”においては、型付きラムダ項の計算（書き換え、変換）だけではなくて、シーケント計算が必要になります。型理論では、シーケントを型判断（type judgement）と呼ぶことが多いですが、内実はシーケントです。シーケントは、その形からいくつかの種類に分類できます。そして、シーケントの種類ごとに対応する圏も別な種類になります。これらの圏は、よく似ているので同一視することもありますが、区別したほうがいいと思います。内容： モノイド閉圏 シーケントの分…

…＝CADG カリー／ハワード／ランベック対応 CADGのこれから リソース計算が微分計算だってぇぇ?!ラムダ計算をご存知でしょうか？ ラムダ計算はコンピュータ科学において重要な位置を占めます。関数型プログラミング言語は、すべからくラムダ計算の影響を受けています。関数型とは言いがたいプログラミング言語（例えばJavaやC++）でさえ、最近はラムダ式（ラムダ計算の表現法）をサポートしています。1993年、ボードル（Gérard Boudol）は、多重度付きラムダ計算という“ラムダ…

…せば、それがカリー／ハワード対応になります。「証明」という言葉が、証明オブジェクトというデータを表すこともありますが、証明オブジェクトを作り出す行為を「証明」と呼ぶこともあります。この2種の「証明」はシッカリ区別すべきです。「証明オブジェクト」と「証明行為」とすれば区別できますが、もっと明確に区別するために、証明行為をリーズニング（reasoning）と呼ぶことにします。すると、次のことが言えます。 自然演繹では、証明オブジェクトを証明図として図示する。リーズニングを図示する…

…ゴール」という言葉の困った使い方。証明支援系はカリー／ハワード対応を使うことが多いので、型理論の用語も使います。型理論の用語法はいいかげん混乱してますが、この混乱も持ち込まれます。その結果、証明支援系のマニュアルや解説の記述は悲惨なことになります。冒頭の一覧表（の枠組み）を作った動機は、Isabelleのマニュアルの激しく曖昧・多義的な用語法を整理するためでした。論理や論理的ソフトウェアが自分自身を語るときの論理性や整合性がグダグダなのは、「なんとかならんのかよ」と思います。

…ケント計算、カリー／ハワード対応 2011年11月 大きなラムダ式／小さなラムダ式 2011年11月 Alloy、コンパクト論理、関係圏 2012年1月 圏論の筆算としてのシーケント計算 2012年1月 シーケント計算と圏論（続きみたいな） 2015年 中学レベル代入計算からカリー／ハワード流証明の圏へ 多圏はメンドクセー 多圏を定義するには 多圏を何に使いたいのか 何とかなりそう [追記]4年以上のブランクの後で続きを書きました。 対称モノイド多圏（簡約版） [/追記]多圏…

…し現在では、カリー／ハワード対応により、同じものだと認識されています。「同じもの」とは、同じ意味論的な対象物を指していて、表現としての構文が違うだけ、ということです。同じ意味論的な対象物とは、デカルト閉圏やその変形・拡張のことです。そうであるなら、同じ対象物に対する異なる構文を異なるままにしておく意義ってあるんでしょうか？現状では、ラムダ計算とシーケント計算では、それぞれ別な記号法や用語法が使われていて、一緒に使おうとするとメチャクチャ使い勝手が悪いことになります。型理論は型…

…ア: 単行本カリー／ハワード対応について説明している論理の本は少ないので、非常に助かります。かつてラムダセミナー／モニャドセミナーでカリー／ハワード対応を題材にしたときのネタ本はこれです。この本『数理論理学』は、コンピューターサイエンス向けに論理をリフォームすることを目指して書かれたもので、自然演繹やシーケント計算のようなポピュラーな話題でも、伝統や標準的な解説法に拘らず、林さん独自の工夫が随所にあります。それと、共立出版『プログラム検証論』と遊星社『構成的プログラミングの基…

…述べるのは、カリー／ハワード対応を目いっぱい意識した構文です。つまり、論理の計算のなかに型理論の構成要素を可能な限り取り込みます。この構文は、これから使ってみて変える可能性が高いです。なにか叩き台がないと試すことが出来ないので定義をしてみよう、ということです。型シーケント「型付きラムダ計算のモデルの作り方」において、大きなラムダ式について述べました。大きなラムダ式と型判断と型シーケントは同じものです。書き方が多少異なるだけです。（以下に出てくる指数の記号「^」については、「圏…

…代入計算からカリー／ハワード流証明の圏へ 小さなラムダ式（単なるラムダ項）ではなくて大きなラムダ式（＝型判断＝シーケント）を射とみなすべきなんですが、大きなラムダ式にどうやって射を対応付けるかをもう少し詳しく書いておくことにします。内容： 大きなラムダ式・再論 大きなラムダ式のセマンティクス ラムダ抽象 圏的ラムダ計算の一般化とか 大きなラムダ式・再論常識的な型付きラムダ計算の構文を考えて、その構文による式（ラムダ項）をM、Nなどとします。このラムダ計算で使う変数の集合をVa…

…っていると、カリー／ハワード対応の威力を実感します。一方で、証明といえども所詮は計算なんだな、とも思います。中学校くらいでやる代入計算の直接的な延長線上に証明の合成操作があるんですよね。中学レベルの計算と形式的証明では、用語や記号がまったく違うのですが、そこにうまく通路を作ってやると、やってることは大差ないことが分かります。「寄り道Coq： exactタクティクと型理論と圏論」の最後の節「大きなラムダ式／小さなラムダ式」で述べたことの敷衍です。内容： 1次式の代入計算 代入の…

…体は項です。カリー／ハワード対応では、Propositions-as-Types, Proofs-as-Terms と解釈するので、型がAである項tを実際に作れるなら、「命題としての型A」は「証明としての項t」により“証明された”とみなします。この事情をもう少しハッキリさせます。型理論を少しだけ「名前 : 型」という形を型宣言と呼びましょう。型理論では、型宣言という用語をあまり使いませんが、「型宣言」は多くの人に馴染みがある言葉だと思います。型宣言のコロンの左にある名前の用途…

…の背景であるカリー／ハワード対応は必須じゃないでしょうが、論理記号や推論図くらいは知ってないとゲームのルールを説明できません。そして、説明に使う言葉がまた問題です。Coqの説明には、関数型言語、論理、型理論などの言葉が入り混じって登場します。型理論の用語や記号が無茶苦茶のグチャグチャであることは「用語法／記号法／図示法は、ほんっとうーに方言が多い」からリンクされている一連のエントリーを参照してください。Coqでは型理論の用語に加え、論理やラムダ計算の用語、Coq独自の用語も混…

…oqの証明はカリー／ハワード対応に基づいていて云々」とはよく言われてますが、その本質は真偽値をどう解釈するか？ というあたりじゃないか、と思います。スローガンは「真偽値は、なんだっていいのだ」です。Coqにおいて、真偽や論理演算（AND、ORなど）をどう考えるかについて書いてみます。「Coqにおいて」と言いましたが、Coqの操作やスクリプトは全然出てきません。背景となる考え方の話です。内容： C言語の真偽値 集合全体を真偽値に使う 空集合ではない証拠 論理システムと型システム…

…らしいので、カリー／ハワード・スタイルの対応がありますね。表にします。 連言・含意の論理 型付きラムダ計算 右カン拡張 命題 P, Q 集合 A, B 関手 F, G 帰結関係 P |- Q 写像 f:A→B 自然変換 α::F⇒G 連言 P∧Q 直積 A×B 結合 F;G 含意 P⊃Q 写像集合 BA 右カン拡張 FG 演繹定理 カリー双射対応 カン双射対応 含意導入 ラムダ抽象 自然変換のシフト モーダスポネンス 適用／評価 自然変換のアンシフト 推論／証明 写像の計算 …

カリー／ハワード対応を通して（標準的な）型付きラムダ計算と対応する論理は、連言（∧）と含意（⊃）を持つ論理です。これら2つの体系に共通することは、デカルト閉圏をモデルに持つことです。デカルト閉圏が繋ぎになって、2つの形式体系が結ばれていると言ってもよいでしょう。デカルト閉圏の代わりにコンパクト閉圏を取ると、対応する論理体系は連言と否定（¬）を持つ論理です。ただし、連言（∧）と選言（∨）は一致してしまい、そのせいで否定も古典論理の否定とは違った振る舞いをします。含意は選言（＝連…

…]] です。カリー／ハワード対応があるので、指数法則は次の推論が妥当であることを意味しています。 A∧B ⊃ C -------------- B ⊃ (A⊃C) B ⊃ (A⊃C) -------------- A∧B ⊃ Cあるいは、シーケントで書いて、A∧B ⊃ C ⇒ B ⊃ (A⊃C) と B ⊃ (A⊃C) ⇒ A∧B ⊃ C を示せばいいことになります。論理の証明図を書いて、それをデカルト閉圏Cで再解釈すれば、指数法則を与える具体的な同型が構成できるはずです。で…

…付けする規則カリー／ハワード対応の一番簡単な例は、「タプルを持つ型付きラムダ計算」と「含意と連言を持つ命題論理」の対応です。この対応を復習しながら、ラムダ式（ラムダ項）の型付けを説明します。まず、A、Bなどは命題として、以下の（論理の意味の）推論規則（推論図）を考えましょう。 A A⊃B ---------- B A B -------- A∧BA、Bなどは集合だと解釈してみます。集合は、Sets-as-Typesの立場なら型だと言えます。論理の含意記号「⊃」を関数集合を作る…