ここでのタルスキーの定理は、不動点に関するタルスキーの定理です。不動点関連でも次のような「タルスキーの定理」があります。 最小プレ不動点と最小不動点の関係を述べた定理 最小不動点の存在定理 不動点集合の性質に関する定理 「最小プレ不動点ならば…
「タルスキーの最小プレ不動点定理（訂正）」において： 証明の流れを完全に追えるように、中間の命題にいちいち名前（ブラケットで囲った文言）を付けて参照することにします。 と、やってはみたのですが、“証明の流れ”がテキストで直列に（シリアライズさ…
「不動点方程式／不動点不等式と不動点オペレーター」において、タルスキーの最小プレ不動点定理を出しましたが、記述が間違っていたので訂正し、省いていた証明を記します。$`\newcommand{\mrm}[1]{\mathrm{#1}} \newcommand{\cat}[1]{\mathcal{#1}} \newco…
「フリーモナド 1： 自由で無料な木」において、次のように予告しました。 圏論的な不動点方程式と、不動点方程式によるフリーモナドの構成については「2」で述べます。 しかし、不動点の話はフリーモナドとは独立に語れるので、「フリーモナド」の続きでは…
ひとつ前の記事「フリーモナド 1： 自由で無料な木」において次のように書きました（ブラケット内は要約です）。 [圏論的に考えた場合と、型クラスで考えた場合とでは] メンタルモデルがだいぶ違います。この食い違いがコミュニケーションの障害になることが…
フリーモナドの「フリー」は、「自由」の意味と共に「ただ〈for free〉」の意味もあります。「ただで手に入るモナド」ということです。しかし、この「ただで」は、「課金したらガチャをただで引けるよ」の「ただで」と同じで、事前のコストはかかっています…
2017年に書いた「ほぼ絶滅 アンミラ」という記事にて： 現在のアンナミラーズ ウィング高輪店は、現存する唯一のアンナミラーズです。最盛期には20店舗あったということですが …。 最後のアンナミラーズだった高輪店も2022年8月31日で閉店したんですね。 さ…
指標に対する不完全インスタンス〈不完全モデル〉という概念を導入します。不完全インスタンスは、記号の乱用、オーバーロードなどの分析に使うつもりです。内容： 指標の例 指標のモデル〈インスタンス〉 無名のモデル ラベルの省略 不完全モデル 指標の例…
とある論文で、説明のためにHaskell風疑似コードが使われていました。そのひとつが次： data 0 a instance Functor 0 where fmap = ⊥ ウーム、わかる人にはわかるのかも知れないけど、ほぼ意味不明。いったい何を言いたいのでしょう？ 僕が説明します。$`\ne…
「自然演繹の再構築への道」という記事を書いたのは6年前です。それから折に触れて“自然演繹の再構築”について考えてはいますが、細部まで詰めているわけじゃないです。んで、また最近ちょっと考えている次第。上記過去記事では、「モノイド圏から多圏を作っ…
推論規則〈inference rule〉と型つけ規則〈typing rule〉の両方を含むシステムで使いやすいものがないかな、と探していました。僕が思う“使いやすい”とは： 意味論〈セマンティクス〉はハイパードクトリン。 カリー／ハワード／ランベック対応と相性がよい。…
年に2,3回、誰かに向かって同じ話をしている気がするので、ブログ記事にしておきます。$` \newcommand{\Imp}{\Rightarrow } \newcommand{\Iff}{\Leftrightarrow } \newcommand{\mrm}[1]{\mathrm{#1}} \require{color} \newcommand{\Keyword}[1]{ \textcolor{…
記事タイトルの「述語論理」は、昨日の記事「圏論的述語論理とお絵描き」で紹介した、ハイパードクトリンによる圏論的述語論理のことです。このスタイルの述語論理に関係する話題には、記事タイトル冒頭に「述語論理：」を付けるつもり。ハイパードクトリン…
圏論的述語論理の話は過去に何度かしたことがありますが、現時点での観点から大雑把に復習してみます。そして、「全称記号の導入」と「存在記号の消去」と呼ばれる“推論規則”の絵の描き方を紹介します。$` \newcommand{\Imp}{\Rightarrow } \newcommand{PPB}…
加藤五郎さんによると、米田の補題は「圏論の大黒柱」だそうです（「圏論番外：米田の補題に向けてのオシャベリ」参照）。どのくらい重要で強力かというと（「米田、米田、米田」より）： the category theorist's joke that "all theorems are Yoneda." ...…
