このブログの更新は Twitterアカウント @m_hiyama で通知されます。
Follow @m_hiyama

メールでのご連絡は hiyama{at}chimaira{dot}org まで。

はじめてのメールはスパムと判定されることがあります。最初は、信頼されているドメインから差し障りのない文面を送っていただけると、スパムと判定されにくいと思います。

参照用 記事

タルスキーの定理の実例と応用

ここでのタルスキーの定理は、不動点に関するタルスキーの定理です。不動点関連でも次のような「タルスキーの定理」があります。 最小プレ不動点と最小不動点の関係を述べた定理 最小不動点の存在定理 不動点集合の性質に関する定理 「最小プレ不動点ならば…

証明のツリー構造も描いてみる

「タルスキーの最小プレ不動点定理(訂正)」において: 証明の流れを完全に追えるように、中間の命題にいちいち名前(ブラケットで囲った文言)を付けて参照することにします。 と、やってはみたのですが、“証明の流れ”がテキストで直列に(シリアライズさ…

タルスキーの最小プレ不動点定理(訂正)

「不動点方程式/不動点不等式と不動点オペレーター」において、タルスキーの最小プレ不動点定理を出しましたが、記述が間違っていたので訂正し、省いていた証明を記します。$`\newcommand{\mrm}[1]{\mathrm{#1}} \newcommand{\cat}[1]{\mathcal{#1}} \newco…

不動点方程式/不動点不等式と不動点オペレーター

「フリーモナド 1: 自由で無料な木」において、次のように予告しました。 圏論的な不動点方程式と、不動点方程式によるフリーモナドの構成については「2」で述べます。 しかし、不動点の話はフリーモナドとは独立に語れるので、「フリーモナド」の続きでは…

Functor型クラスの型インスタンスは関手なのか?

ひとつ前の記事「フリーモナド 1: 自由で無料な木」において次のように書きました(ブラケット内は要約です)。 [圏論的に考えた場合と、型クラスで考えた場合とでは] メンタルモデルがだいぶ違います。この食い違いがコミュニケーションの障害になることが…

フリーモナド 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." ...…