指標に対する不完全インスタンス〈不完全モデル〉という概念を導入します。不完全インスタンスは、記号の乱用、オーバーロードなどの分析に使うつもりです。内容： 指標の例 指標のモデル〈インスタンス〉 無名のモデル ラベルの省略 不完全モデル 指標の例…

とある論文で、説明のために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." ...…

「自然変換のためのラムダ計算」の続きです。$`% \newcommand{\cat}[1]{\mathcal{#1}} %\newcommand{\id}{\mathrm{id} } \newcommand{\mrm}[1]{\mathrm{#1} } \newcommand{\In}{\text{ in } } %\newcommand{\Iff}{\Leftrightarrow } \newcommand{\twoto}{\Ri…

米田の補題をストリング図で描いておくと、米田同型〈the Yoneda isomorphism〉の作り方を忘れないんじゃないかと思います。$`% \newcommand{\cat}[1]{\mathcal{#1}} \newcommand{\id}{\mathrm{id} } \newcommand{\mrm}[1]{\mathrm{#1} } \newcommand{\In}{\…

とある自然変換の計算をしていて、通常のラムダ計算の構文はどうも具合が悪い気がしました。視力がいい人なら問題ないでしょうが、老眼近視の僕には視認性が良い構文が必要です。また、ラムダ計算に図式順記法を取り入れます。$` \newcommand{\Iff}{\Leftrig…

「多相関数」って言葉が意味不明ですが、それは一旦棚に上げて、リストの長さは多相関数の事例だとしましょう。リストの長さの宣言を次のように書くことがあります。$`\quad \text{length} : \forall \alpha.\text{List}\, \alpha \to {\bf N}`$ここで論理の…

「落第」の意味は、例えば、なんかの資格を取ろうと試験を受けたが落ちて資格を取れなかった、とそんな感じです。落第厳密モノイド圏は、厳密モノイド圏になりたかったけど、公理を満たし切れずになれなかった圏です。実は、パッと見厳密モノイド圏っぽい落…

集合と写像の話をします。集合圏のごく基本的な用語・記法は使います（最初の節に説明あり）。写像のセクションと集合族のタプルを定義して、その関係を述べます。$`\newcommand{\In}{\text{ in }} \newcommand{\id}{\mathrm{id}} \newcommand{\Iff}{\Leftri…

群が「左から作用する」「右から作用する」という言い方があります。このときの「左」「右」はどんな意味なんでしょう？ また、「左」か「右」かはどうやって判断するのでしょう？ なにかを左（あるいは右）と呼ぶべき必然的根拠があるとは思えないので「約…