「続・カリー／ハワード／ランベック対応の辞書」にて： 圏論では、射のあいだの等式的関係、例えば $`\langle f , g \rangle; \pi_1 = f`$ などが重要ですが、論理ではあまり言及しません。分野ごとに、興味のあり方や価値観が違うからでしょう。 論理にお…
現状の証明支援系〈proof assistant〉について、僕はしょっちゅう愚痴と文句を言っています（twitterでぼやいたりしてる）。大きな不満点は、フォワード・リーズニングの対話的サポートがまったくない点です。不便だし面白くない。内容： 証明ソフトウェアの…
「カリー／ハワード／ランベック対応の辞書」の続きです。カリー／ハワード／ランベック対応〈Curry-Howard-Lambek correspondence〉は、細部まで対応が行き届いているので、論理の推論規則の対応物を見てみます。論理では、「導入規則と除去規則が“きれいに…
カリー／ハワード／ランベック対応〈Curry-Howard-Lambek correspondence〉は、「型理論（ラムダ計算を含む）」「論理」「圏論」の三分野の概念のあいだの精密・詳細な対応を与えてくれます。しかし、言葉はうまく対応してくれません。異なる分野の言語・文…
論理では、命題だけではなくてメタ命題も扱います。メタ命題で使う記号〈メタ記号〉に ’$`\vdash`$’ や ’$`\models`$’ があります。どちらも「命題はほんとうだ」という意味で使います（が、ほんとうである根拠は違います）。「‥‥という命題はほんとうだ」と…
昔、「具体的に具体的に具体的に具体的に」（4回繰り返し）というフレーズを使ったことがあります（「「具体的に具体的に具体的に具体的に」（4回繰り返し）とはどういうことか」参照）。これは、抽象的な議論を具体的に書く・語ることはできるが、曖昧な思…
応用圏論〈Applied Category Theory〉においても、コエンド〈coend〉の利用は増えています。例えば、“オプティックの圏”のホムセットの構成にはコエンドを使います。ところが、コエンドの説明が（僕自身の説明も含めて）だいたいは不親切で、「細かい事まで…
表題のような主張を、いつかどこかで見たことがあるんですが、いつ・どこで？かは思い出せません。なぜ「非可換環上の加群は豊穣関手」とみなせるか？は説明できそうなので、この記事に書いてみます。$`\newcommand{\mrm}[1]{\mathrm{#1} } \newcommand{\In}…
ラムダ項〈ラムダ式〉を、ド・ブラウン・インデックス〈de Bruijn index〉を使って書く方法。内容： de Bruijn のカタカナ書き ラムダ項の構文 意図してない束縛 ラムダ項の2次元記法 ド・ブラウン・インデックス 他の例 de Bruijn のカタカナ書き12年前〈20…
証明支援系Lean〈リーン〉は、かなり前（2017年くらい）から注目しているソフトウェアです。注目はしているんですが、ちゃんと調べる機会がなかったので、このブログで触れたことはありませんでした。2022年のうちに紹介したい（今は大晦日の夜）。Leanは現…
jq（https://stedolan.github.io/jq/）の紹介では、「JSON処理のワンライナー〈一行野郎〉としてめちゃくちゃ便利！」とアピールするのが定番です。もちろんそれは本当で、「めちゃくちゃ便利！」です。が、実は jq は、ワンライナー記述にとどまらない、か…
ECMAScript Modules（ESM）方式のモジュールシステムを前提に、ブラウザ向けJavaScriptプログラムを書いていたら奇妙な現象に遭遇しました。同一のJavaScriptモジュールが、ブラウザ内に二回ロードされていたのが原因でした。内容： クラスの定義とクラスの…
「二重圏を語るために」にて： 広く合意された約束はないので、二重圏を語るときは、ローカルルールをしっかり決めましょう。そうでないと、話がワヤクチャになります。 ローカルルールの事例を述べておきます。$`\newcommand{\twoto}{\Rightarrow} \newcomm…
二重圏を話題としたコミュニケーションは、なかなかに大変です。前もって約束を決めておかないと、話がワヤクチャになります。この記事でガイドラインを示します。$`\newcommand{\cat}[1]{ \mathcal{#1}} \newcommand{\mrm}[1]{ \mathrm{#1}} \newcommand{\I…
圏論、型理論（型付きラムダ計算含む）、論理は、カリー／ハワード／ランベック対応により、同種の構造（例えばデカルト閉圏）を扱っていると理解することが出来ます。しかし、用語法・記法はバラバラです。このバラバラさゆえに、対応関係を捉えられなかっ…
