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

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

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

参照用 記事

雑記/備忘

ワイヤリング図とケリー/マックレーン・グラフ

応用圏論〈ACT -- Applied Category Theory〉で頻繁に使用されるワイヤリング図は、ケリー/マックレーン・グラフとして表現できます。ケリー/マックレーン・グラフを経由すれば、ワイヤリングの関数による表現も自然に感じるでしょう。この記事は、以下の2…

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

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

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

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

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

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

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

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

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

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

フリーモナド 1: 自由で無料な木

フリーモナドの「フリー」は、「自由」の意味と共に「ただ〈for free〉」の意味もあります。「ただで手に入るモナド」ということです。しかし、この「ただで」は、「課金したらガチャをただで引けるよ」の「ただで」と同じで、事前のコストはかかっています…

指標と不完全インスタンス

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

ほぼワケワカラン疑似コード

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

自然変換のためのラムダ計算 (2)

「自然変換のためのラムダ計算」の続きです。$`% \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…

群の作用の左と右

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

ストリング図のテキスト化: ボックス&ポート方式

「ストリング図のテキスト化は何が大変か?」にて: [ストリング図のテキスト化は]大変なんです。大変でやる気になれないのですが、でもやらざるを得ないでしょう -- 低コストの情報伝達手段がテキスト化する以外にないので。 という事情で、テキスト化の方…

ストリング図のテキスト化は何が大変か?

昨日の記事「ストリング図のテキスト化」で、「テキスト表示を使って、オペラッド結合の記述や計算をするのは、やる前に気力が萎える」と言いました。つまり、大変なんです。大変でやる気になれないのですが、でもやらざるを得ないでしょう -- 低コストの情…

ストリング図のテキスト化

僕はストリング図が大好きです。ストリング図の利用・応用の範囲は広がっているようです。しかしながら現状においては、ストリング図の作成・公開・交換は容易ではないので、テキストに翻訳してコミュニケーションに使用することになります。テキスト化が好…

スパイダー付き圏における仮想スパイダー

スパイダー付き圏を定義したので、以前から使っていた描画技法の話ができますね(ニコ)。現実には存在しない射だけど、ストリング図では“射であるかのごとく”に描くと便利なもの -- 仮想スパイダーの話をします。$`% \newcommand{\cat}[1]{ \mathcal{#1} } \n…

スパイダー付き圏

CD圏〈準マルコフ圏 | GSモノイド圏〉やハイパーグラフ圏〈ダンジョン圏〉のように、モノイド圏の各対象ごとに与えられる特別な射達とその法則により定義されるタイプの圏を総称してスパイダー付き圏と呼びたいと思います。$`% \newcommand{\cat}[1]{ \mathc…

マルコフ圏にモナドが欲しい事情

マルコフ圏を普及させた当事者であるフリッツ〈Tobias Fritz〉達は、モナドを備えたマルコフ圏の定義も試みています。 Title: Representable Markov Categories and Comparison of Statistical Experiments in Categorical Probability Authors: Tobias Frit…

サーフェイス図のテキスト表現 その2

昨日書いた記事「サーフェイス図のテキスト表現」に、少し続きがあります。$`\newcommand{\twoto}{\Rightarrow} \newcommand{\cat}[1]{\mathcal{#1}} \newcommand{\In}{\text{ in } } \newcommand{\Id}{\mathrm{Id}} \newcommand{\C}{\mathop{;}} \newcomman…

サーフェイス図のテキスト表現

最近、ラックス・モノイド関手の記述と計算のためにサーフェイス図を描いているのですが、サーフェイス図をきれいに描いて公開するのは手間がかかり過ぎて無理です。致し方ないのでテキストで表示しますが、3次元的情報をシリアライズしたテキストは、書くの…