…圏と圏の圏 カリー／ハワード／ランベック対応のための“呼び名”と“書き方” // 導出系 また、演繹系と帰納構造との関係は最近の記事で扱っています。 帰納構造と帰納原理 // 演繹系から作る帰納構造 上記記事の最後「「考え直したほうがいい点」」に次のように書きました。 帰納構造の台集合は大きな集合も許すべきだろう。なんなら台集合を宇宙にとってもいい。 帰納構造を、集合論または型理論の宇宙ともっと密接に関係付けるべきだろう。 帰納構造のベース集合 $`X_0`$ を、構文的コン…

…圏と圏の圏 カリー／ハワード／ランベック対応のための“呼び名”と“書き方” // 導出系 さて、演繹系から帰納構造を組み立てましょう。演繹系のすべての項達の集合を $`X`$ （台集合）とします。演繹系のステップ達は分類されているとして、その種別の集合 $`I`$ をインデキシング集合とします。同じ種別のステップでは、上段に並ぶ項の個数が決まっているとして、その個数からアリティ関数 $`n:I \to \mbf{N}`$ を決めます。$`i\in I`$ に対する構文的コンス…

…というと； カリー／ハワード／ランベック対応によれば、型と命題は事実上同じものなので、区別する必要はないです -- と言われても、「型と命題はなんか違うような気がする」と思うでしょ。その気持ちへの対処を考えました。それは、型を命題へと“キャストする”オペレーターを導入する、という方法です。このオペレーターは、拡がり・大きさを持つ集合を一点（単元集合）に潰してしまうオペレーターなのでクラッシュ・オペレーターと呼びましょう。そして、クラッシュ・オペレーターを $`\nabla`$…

…ありません！カリー／ハワード／ランベック対応によれば、論理と型理論に本質的な違いはありません。よって、述語論理の圏論的な定式化とは、型理論の圏論的な定式化と同じことです。型理論で限量子に相当するものはシグマ型とパイ型です。シグマ型が存在限量子に相当し、パイ型が全称限量子に相当します。そういう事情でハイパードクトリンは、シグマ型とパイ型を持つような型理論の圏論的な定式化でもあります。論理の用語とメンタルモデルで語るときは“ハイパードクトリン”と呼ぶ、ということです。呼び名だけの…

…ン拡張と充填三角形 補遺 カン拡張／カン持ち上げと上ホム対象／下ホム対象、充填三角形 左随伴関手は左カン拡張を保存する カリー vs. カン、双対 vs. 随伴 カン拡張の左右： 混乱する原因がわかった！ 右カン拡張の eval は run それでもカン拡張の左右を忘れてしまう ラムダ計算の自然性とお絵描き なにゆえにカン拡張なのか カン拡張における上下左右： 入門の前に整理すべきこと カリー／ハワード対応の新しい仲間 右カン拡張が、自然変換のラムダ計算における指数型らしい件

…ついては、「カリー／ハワード／ランベック対応のための“呼び名”と“書き方”」をみてください。導出システムを形式的体系〈formal system〉としてキチンと定義すれば、導出システムのあいだの準同型射〈homomorphism〉も定義できます。とある種類の導出システム達は圏を形成します。導出システム達の圏を、プレースホルダー $`x`$ を使って次のように書きます。$`\quad x\mbf{DS}`$ 'DS' は 'derivation systems' または 'de…

…述語論理： カリー／ハワード／ランベック対応と推論・型つけ規則」では、フェンス記号に '$`|`$' を使っていますが、'$`|`$' は OR の意味を持った区切り記号にしたいので、コンテキストの区切り（OR の意味は持たない、むしろ AND）には '$`\|`$' を使うことにします。さて、型理論の演繹定理ですが、$`T`$ を型理論の導出システムとして、次の2つのメタ命題が、メタに同値であることを主張します。 $`\Sigma \Vvdash_T \Gamma \vda…

…のテーマは「カリー／ハワード／ランベック対応」です。最近の記事がすべてカリー／ハワード／ランベック対応に関係するわけではありませんが、9月の記事「関数の構成法 (カリー／ハワード／ランベック対応も少し)」あたりから、カリー／ハワード／ランベック対応についてまた考える機会が増えました。以前からの悩みのタネなんですが、「カリー／ハワード／ランベック対応とハイティング／ド・モルガン圏」で書いたこと： この綺麗な対応がなかなか伝わらないようです。対応が見えにくくなっている大きな原因は…

…思えますが、カリー／ハワード／ランベック対応によれば「型と命題は同じもの」です。曖昧語「型」は型項と解釈できるし、曖昧語「命題」は文〈論理式〉と解釈できる（「命題」と「型」の曖昧性を図示」参照）ので、型項と文が同じものであることは、さほど驚くことではありません。$`\F{S}`$ はコンテキストの圏 $`\cat{C}`$ 上の反変関手〈前層〉ですが、指標の圏 $`\cat{S}`$ 上では共変関手〈余前層〉です。コンテキスト／指標の圏 $`\cat{C}\& \cat{S}…

…-- これはカリー／ハワード／ランベック対応の主張です。Propositions-as-Types, Types-as-Propositions と表現されることもあります。ところが、「命題」という言葉は非常に曖昧です。同様に「型」という言葉も非常に曖昧です。不幸中の幸いというか、「命題」と「型」の曖昧性のパターンは同じです。言葉の曖昧性も含めて Propositions-as-Types, Types-as-Propositions というわけです。「命題」「型」に共通な曖…

昨日の記事「カリー／ハワード／ランベック対応とハイティング／ド・モルガン圏」で話題にしたハイティング圏について、もう少しダラッと述べます。$` \newcommand{\mrm}[1]{ \mathrm{#1} } \newcommand{\mbf}[1]{\mathbf{#1}} \newcommand{\cat}[1]{\mathcal{#1}} %\newcommand{\msf}[1]{\mathsf{#1}} %\newcommand{\mbb}[1]{\mathb…

カリー／ハワード／ランベック対応については、このブログ内で何度も言及しています。 このブログ内 ハワード の検索結果 論理／型理論／圏論の三者のあいだに、精密で綺麗な対応があります -- それがカリー／ハワード／ランベック対応です。カリー／ハワード／ランベック対応はとても重要な概念だし、実用的な意義もあります。しかしながら、この綺麗な対応がなかなか伝わらないようです。対応が見えにくくなっている大きな原因は、構造が綺麗に対応していても、言葉や記号は対応してないことです。論理／型…

…の後結合： カリー／ハワード／ランベック対応 言葉と記号を整理しよう関数の構成法〈作り方〉は基本的なことです。内容的には基本的でも、言葉や記号で混乱している可能性はあります。「シーケントに関する不満と対策」より： 「オーバーロードやコンフリクトは日常茶飯事なのだから、そんなに気にすることないよ」と思う人もいるでしょう。僕もかつてはさほど気にしてませんでした。が、ここ10年くらいの経験で、「オーバーロード／コンフリクトを適切に処理する」ことは、とてもとてもとても難しいことだ、と…

…あります。 カリー／ハワード／ランベック対応の辞書 続・カリー／ハワード／ランベック対応の辞書 まだある、カリー／ハワード／ランベック対応の辞書 カリー／ハワード／ランベック対応の辞書： 推論規則再論 カリー／ハワード／ランベック対応： チートシート 誤認・思い込みも語彙エントリーにする動物事典に、架空の動物である龍や一角獣を載せることはないかも知れません。が、龍や一角獣は実在しないんだよ、という情報を含めることには意義があるでしょう。語彙目録には、誤認・思い込みから生じる言…

…と型 補遺 カリー／ハワード対応に親しむ （誰も書かないCoq入門以前 3） 述語は論理型を値とする型ファミリーなので、「述語は型だ」は不正確です。次ならいいでしょう。 述語はパラメータを持つ型だ。 パラメータを持つ型は型ファミリーなので、次でも同じです。 述語は型ファミリーだ。 さて、論理式〈formula〉ですが、これは構文的概念です。なにかを表す構文的対象物〈syntactic object〉を項〈term〉と呼びます。論理式は、論理で使う項です。「論理式は型だ」をより…

…ています。 カリー／ハワード対応に親しむ （誰も書かないCoq入門以前 3） スローガンは「真偽値は、なんだっていいのだ」です。...[snip]...宇宙全体を真偽値だと考えましょう。C言語の「数値が真偽値」の場合と同じように、真偽の解釈規則を与えます。 $`{\bf Prop} = |{\bf Set}|`$ のときは、任意のファミリー〈indexed family of sets〉が述語になります。$`\newcommand{\In}{\text{ in }} \new…

…述語論理： カリー／ハワード／ランベック対応と推論・型つけ規則」があります。$`\Glob`$ の推論規則は以下のようです。 $`\Rule{dummy-bdry}`$ ダミーな境界項 $`*`$ は無条件に正当 $`\Rule{new-bdry}`$ 新しい境界項の構成法と正当性 $`\Rule{trivial}`$ 自明な推論は正当な推論 $`\Rule{ctx-thin}`$ コンテキストを水増し（thinning）しても推論の正当性は維持される $`\Rule{emp…

…という概念をカリー／ハワード／ランベック対応で論理に移すと、証明で使ってよい背景的前提（明示的な仮定とは別）になるからです。以上は昔〈過去〉の話でしたが、次節以降であらためて環境付き計算を説明します。環境付き計算のインデックス付き圏環境 $`S`$ ごとに、$`S`$-環境付き計算の圏が構成できて、$`S`$ を動かすとインデックス付き圏になります。そのことをこの節で説明します。$`\cat{C} = (\cat{C}, \times, \mrm{I})`$ は、モノイド圏と…

…もあります。カリー／ハワード／ランベック対応により、“単純型理論←→命題論理”、“依存型理論←→述語論理”と対応するので、依存型理論と述語論理が共通のフレームワークに包摂されるのは当然とも言えます。適当なセッティングのもとで、依存型理論を目指してシステムを構成すれば、そのシステムは述語論理にも使える／使えてしまう、というわけです。この“依存型理論・兼・述語論理”のシステムの公理的特徴付けがハイパードクトリンです。ハイパードクトリンの具体的構成には、“ファミリー＝述語”の圏にお…

…相当します。カリー／ハワード／ランベック対応〈Curry-Howard-Lambek correspondence〉により、論理とラムダ計算は対応しますが、ラムダ計算が棲んでいる生息地〈habitat〉が色々とあり得ます。様々な評価射とそのコンビネータを区別したいなら、プロファイルをシッカリ書いて、識別のための添字を付けるとかします。 $`{\mrm{ev}^\cat{C}}_{A, B}: [A,B]\times A \to B \In \cat{C}`$ $`{\mrm{…

…`$内容： カリー／ハワード／ランベック対応と複圏・多圏 形式証明のストリング図 変数名・ラベルの利用 ラベル利用の事例 ノードとコネクター 追記・補足の記事： 自然言語混じり形式証明の意味論 シリーズ・ハブ記事： チャットAIで形式証明も自然言語混じりで書ける（はず） カリー／ハワード／ランベック対応と複圏・多圏我々がバックボーンとする考え方はカリー／ハワード／ランベック対応〈Curry-Howard-Lambek correspondence〉です。つまり、型付きラムダ計…

…いからです。カリー／ハワード／ランベック対応により、命題は型のことであり、証明は計算で、定理は関数です。「背理法を使う」推論規則（Lean 4では推論規則と定理の区別もない）by_contradictionは、モジュールMathlib.Logic.Basicに入っているので、ソースファイル冒頭で当該モジュールをインポートする必要があります。Lean 4では前方参照が出来ないので、サブ証明の定理のほうを主定理より先に書かなくてはなりません。 import Mathlib.Log…

カリー／ハワード／ランベック対応の話を何度かしました。「カリー／ハワード／ランベック対応の辞書」の最後に、最近のカリー／ハワード／ランベック対応関連の記事をまとめてあります。最近に限らないなら： ブログ内検索： 「ハワード」の検索結果 さて、カリー／ハワード／ランベック対応によれば、“関数型プログラミング言語でプログラミングをすること”と、“形式化された証明記述言語で証明を書くこと”は同じことです。しかし実際には： 「俺はプログラムなら書けるが、証明を書ける気がしない」 「証…

…ダ式」です。「大きなラムダ式／小さなラムダ式」という言葉は、14年前に書いた記事「セミナー補足：関数コードの実行エンジン」以来使い続けているのですが、（当然ながら）普及はしませんね。でも、「大きなラムダ式＝大きなタプル」と「小さなラムダ式＝小さなタプル」を区別しないとラムダ計算／型理論は理解できないと思いますよ。 *4:型理論のなかでもたくさんの方言があります。 *5:省略の程度や省略の方法が分野ごとに違うことが、カリー／ハワード／ランベック対応を理解する障害になっています。

…ワーリング「カリー／ハワード／ランベック対応の辞書： 推論規則再論」にて： $`A, B, X, Y`$ などは圏 $`\mathcal{C}`$ の対象を表します。$`I, J`$ なども $`\mathcal{C}`$ の対象ですが、これらを“集合とみなす方法”〈dereification〉があるとします*1。[脚注 *1] この仮定は、パワーリング／テンソリングを使って取り除くことができるかも知れません。現状、よくわからない。 パワーリングとテンソリング（コパワーリング…

「カリー／ハワード／ランベック対応の辞書： 推論規則再論」で次のように書いています。 $`A, B, X, Y`$ などは圏 $`\mathcal{C}`$ の対象を表します。$`I, J`$ なども $`\mathcal{C}`$ の対象ですが、これらを“集合とみなす方法”〈dereification〉があるとします*1。[脚注 *1] この仮定は、パワーリング／テンソリングを使って取り除くことができるかも知れません。現状、よくわからない。 「よくわからない」のは、圏の外部…

「カリー／ハワード／ランベック対応の辞書」を皮切りにカリー／ハワード／ランベック対応に関して幾つかの記事を書きました。 カリー／ハワード／ランベック対応の辞書（最初の記事） 続・カリー／ハワード／ランベック対応の辞書 論理と圏論： 導入規則と除去規則のあいだの等式的法則 まだある、カリー／ハワード／ランベック対応の辞書 タプル・コタプルとVΣ計算 矢印の混乱に対処する： デカルト閉圏のための記法 矢印のオーバーロードがひどい件： 所感 カリー／ハワード／ランベック対応の辞書：…

続・カリー／ハワード／ランベック対応の辞書 矢印の混乱に対処する： デカルト閉圏のための記法 上記2つの記事で述べた内容を組み合わせて、記述を追加します。論理でいう「推論規則」は種類が違うものをゴッチャにしています。導入規則〈introduction rule〉と除去規則〈elimination rule〉のあいだに対称性はありません。対称といえる部分でも、その対称性が「双対性か可逆性か随伴性か」の区別を付けてなくて曖昧です。このへんのこと（自然演繹への悪口）は次の過去記事に…

…十数年前からカリー／ハワード対応のセミナーとかやっているわけです。複数の分野に関係する事柄を説明するのはなかなか難しい、計算過程を理解する／してもらうのも大変。だがしかし、僕やあなたが悪いとは限らない： 説明がうまくいかないときは用語法が悪いのかも知れない。 計算がうまくいかないときは記法が悪いのかも知れない。 デカルト閉圏周辺の記法、特に矢印の使い方を整理して、概念がもっとスッキリするように／計算がもっと楽になるようにしましょう。$`\newcommand{\cat}[1]…

…るでしょう。カリー／ハワード／ランベック対応（「カリー／ハワード／ランベック対応の辞書」参照）によれば、圏論的な双対性の対応物は、型理論（ラムダ計算含む）にも論理にも存在するはずです。また、関数型プログラミング言語は型付きラムダ計算に基づいているので、プログラミングのなかでも双対性が存在するはずです。実際、圏論の双対性の対応物は存在しています。圏論以外の分野では、圏論のように双対性が単純明快に表現されているわけではなくて、見えにくく分かりにくい状況になっています。その理由はお…