…という概念をカリー／ハワード／ランベック対応で論理に移すと、証明で使ってよい背景的前提（明示的な仮定とは別）になるからです。以上は昔〈過去〉の話でしたが、次節以降であらためて環境付き計算を説明します。環境付き計算のインデックス付き圏環境 $`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]…

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

…コタプルは、カリー／ハワード／ランベック対応を通じて、論理の全称限量子／存在限量子に対応します。製品情報の出力だの、割引した価格の計算だのが、圏論的双対性／極限・余極限、全称限量子／存在限量子に繋がっているのは楽しいですね。その楽しい話は将来書かれるかも知れない（書かれないかも知れない*4）。[追記]本題の記事を書きました。→「タプル・コタプルとVΣ計算」[/追記] *1:特に、パイの束縛変数が走る集合が有限集合の場合です。 *2:パターンマッチ分岐が使えるプログラミング言語…

カリー／ハワード／ランベック対応の辞書 続・カリー／ハワード／ランベック対応の辞書 まだあるの？ まだあります！カリー／ハワード／ランベック対応〈Curry-Howard-Lambek correspondence〉は、「型理論（ラムダ計算を含む）」「論理」「圏論」の三分野のあいだの対応ですが、今回は、抽象的・一般的な圏ではなくて、集合圏と位相空間の圏を取り上げます。主に、依存型理論の概念を、論理、集合圏、位相空間の圏で何に対応するかをまとめます。先に、幾つかの言葉の説明をし…

「続・カリー／ハワード／ランベック対応の辞書」にて： 圏論では、射のあいだの等式的関係、例えば $`\langle f , g \rangle; \pi_1 = f`$ などが重要ですが、論理ではあまり言及しません。分野ごとに、興味のあり方や価値観が違うからでしょう。 論理における導入規則と除去規則のあいだの関係を、圏論的な記法で等式的法則として述べておきます。実際に論理で使うには、組み合わせや調整が必要です。$`\newcommand{\In}{\text{ in }} \…

「カリー／ハワード／ランベック対応の辞書」の続きです。カリー／ハワード／ランベック対応〈Curry-Howard-Lambek correspondence〉は、細部まで対応が行き届いているので、論理の推論規則の対応物を見てみます。論理では、「導入規則と除去規則が“きれいに”ペアになっている」と言ったりしますが、他分野に移って考えると、けっこうゴチャゴチャで、たいして“きれい”でもないことが分かります。導入と除去のペアは憶えやすいのがメリットですが、整合的対称性があるわけでは…

カリー／ハワード／ランベック対応〈Curry-Howard-Lambek correspondence〉は、「型理論（ラムダ計算を含む）」「論理」「圏論」の三分野の概念のあいだの精密・詳細な対応を与えてくれます。しかし、言葉はうまく対応してくれません。異なる分野の言語・文化・習慣にはギャップがあるからです。言葉の対応表（つまり翻訳の辞書）が作れないのは僕の長年の悩みです。ことあるごとに辞書を試作してはうまくいかずヘコんでいます。以下は、現時点でのだいたいの辞書〈対応表〉です。…

…証と要求： カリー／ハワード対応も添えて この過去記事で、$`\vdash!`$（アスキー文字なら |-!）と $`\vdash?`$（アスキー文字なら |-?）という記号で平叙文と疑問文を区別しています。今回のこの記事では、疑問文に対して、可読性・視認性が良い記法を紹介します。上記過去記事にちょっと追加事項があるだけです。不明なことがあったら過去記事も参照してください。$`\newcommand{\mrm}[1]{\mathrm{#1}} \newcommand{\Imp}…

…）、論理は、カリー／ハワード／ランベック対応により、同種の構造（例えばデカルト閉圏）を扱っていると理解することが出来ます。しかし、用語法・記法はバラバラです。このバラバラさゆえに、対応関係を捉えられなかったり、混乱したりする人もいそうです。整理しておきましょう。$`\newcommand{\cat}[1]{ \mathcal{#1}} \newcommand{\mrm}[1]{ \mathrm{#1}} \newcommand{\In}{ \text{ in }} \newc…

…クトリン。 カリー／ハワード／ランベック対応と相性がよい。 自然演繹としてもシーケント計算としても使える。 これらの条件をまーまー満たすシステムを見つけたので紹介します。これから紹介する推論規則／型つけ規則は、次のバーケダル*1／ビージャック*2の論文にあるものを僅かに変更したものです。 Title: A Taste of Categorical Logic — Tutorial Notes Authors: Lars Birkedal (birkedal@cs.au.dk)…

…述語論理： カリー／ハワード／ランベック対応と推論・型つけ規則 述語論理： 様々な多圏達の分類整理 述語論理： 二重圏的ハイパードクトリン 述語論理： シード付き二重圏 -- 訂正と再論 関連記事： 自然言語混じり形式証明の意味論と最近の型理論 ハイパードクトリン述語論理とは、限量子も扱う論理です。命題論理でも述語は扱うので、“述語を扱う論理”という意味ではありません（言葉に騙されないように）。述語論理の圏論的定式化といえば、ローヴェア〈William Lawvere〉のハイ…

…。ついでに、カリー／ハワード対応で型の世界に移ったときの形式的疑問文の話もします。この記事で述べた“疑問文”の具体的・現実的な使い方は次の記事にあります。 証明の“お膳立て”のやり方 内容： 疑問符と感嘆符 保証と要求 保証と要求の形式化 保証と要求を細かく分類する カリー／ハワード対応と型推論 疑問符と感嘆符AさんとBさんがいて、目の前のお皿によくわからない黒い塊がのっているとします。 Aさん「これ食べられる」 Bさん「これ食べられる」 字面の上では、二人はまったく同じこと…

…あります（「カリー／ハワード対応のための記法・図法」参照）。これは再利用が可能ですが、一枚描くのが大変。絵でなくて、テキストを2次元的に配置する方法をやってみたことがあります。 絵算のテキスト表現（結論：疲れる） 絵算のテキスト化を完全にやってみた（超・疲れた） 絵算からテキスト、そして可換図式化もやってみた（当然疲れた） さかんに「疲れる」と言ってますが、実際疲れます。それでも、現状では2次元レイアウトのテキストくらいで妥協するしかない気がするので、この方法を再度試してみま…

…いるので（「カリー／ハワード対応のための記法・図法」参照）だいぶ不格好です。幾つか注意をしておくと： 矢印があるので明らかですが、描画方向は上から下です。 ノード（射の図示） は、三角形で表すのが多数派です。三角で囲むことが出来なかったので丸で囲んでます。 は、マルコフ圏の対角射〈コピー射〉です。枝分かれしたワイヤーだけで描くことが多いと思います。 左側の I は恒等射です。通常、恒等射はノードとしては描かずワイヤーだけです。 図に出現している射のプロファイルを列挙します。 …

…（「確率論のカリー／ハワード／ランベック対応」参照）のトピックのひとつに「確率的論理」という言葉を入れておいたのですが、「確率的論理」ではひどく漠然としていて、何のことか分からないですね。より具体的に言えば、ファジー論理とエフェクト論理とPS論理の3つを想定していて、総称的に確率的論理と呼んでいます。このなかで、PS論理は名称がないので僕が今さっき命名したものです。印象（あくまで僕の印象）で言うと、ファジー論理が工学的な論理、エフェクト論理が物理（特に量子力学）的論理、PS論…

…ング図は、「カリー／ハワード対応のための記法・図法」で述べた方法で描いています。カクカクが気になるかたは、手描きか頭のなかでなめらかに補正してください。説明不十分な記事ですが、とりあえず投稿した理由はこのリンクが参照している過去記事の冒頭と同じ意図です。内容： 述語論理のモデル ベック／シュバレー条件 述語論理のモデル述語論理の（構文ではなくて）モデルについて説明します。古典的真偽値の集合を B = {0, 1} とします。0は偽で、1は真を表します。0 ＜ 1 という順序を…

…は「確率論のカリー／ハワード／ランベック対応」です。このテーマの背景については次の記事に書きました。 「確率論のカリー／ハワード／ランベック対応」 上記の記事はビッグピクチャー／大局観を述べたもので、実際のセミナーでは具体的な計算を重視します。「いったいどんな感じなのだろう？」という方のために1月16日(土曜)18時から無料ガイダンス回（第0回）をZoomで行います。ガイダンス回＝第0回は、単に内容紹介ではなくて、「第1回の前の回」という位置付けです。本編全10回ですが、サー…

カリー／ハワード対応〈Curry-Howard correspondence〉は、複数（2つ以上）の分野、あるいは複数の理論体系のあいだの同型対応です。2つの分野のあいだにカリー／ハワード対応がある場合、これら2つの分野は事実上同じものとみなせます。有名なカリー／ハワード対応の事例は「連言含意論理 ←→ 単純型付きラムダ計算」の対応です（後述）。2つの分野のうち片方について知っているなら、カリー／ハワード対応に伴う翻訳を施せば、もう一方の分野についても知ることができます。異な…

カリー／ハワード対応には、ある種の主張が伴います。その主張とは次のようなタイプのものです。 歴史的に別々に発展してきた異なる分野が扱っている概念的対象物が、実は同じものだ。 複数の分野のあいだの同型性を主張してるんですね。そんな同型を与える対応を、カリー／ハワード対応、あるいはカリー／ハワード同型と呼びます。典型的なカリー／ハワード対応には、単純型付きラムダ計算と連言含意論理の同型対応があります。さらにデカルト閉圏を含めた三分野のあいだの同型性もあります*1。他にも、カリー／…