Hちょびよみ勉強ノート(10回目)
引き続き圏論で足し算
圏論縛りプレイルール
使っていい言葉とかが制限されてる
名詞
- 射
- 対象
- 図式
述語
- 射の合成 <- 関数合成
- 射が恒等 <- def id(a: A): A = a
- 射が存在する <- 関数が定義できる
- 射が一意 <- 具体例一つだけ確かめればよい。射と射が等しいと言える
- 図式が可換 <- ある射とある射が等しい*1
圏論では具体的な値に言及できないので、気軽に「何かと何かが等しい」とは言えない縛りプレイ。何かと何かが等しいことを言いたければ、可換図式を書いて射と射が可換であるということを言う戦略をとることが多いらしい。
「0は 0 + a = a と言う性質がある」を言いたければ「"0 + a"を表す射と"0"を表す射が等しい」と言う必要があって、前述のとおり「等しい」を言うためには「射が一意」か「図式が可換」であることを使うので、"0 + a"の射と"0"の射の可換図式が書ければ上記のことが言えた、となるらしい。
0 + a の射
足し算の話なのでまず
add: Z × Z → Z
を用意する。
圏論ではドメイン*2とコドメイン*3は一回書いたら変えられない。
ここで書きたいのは 0 + a = a なので、上記のaddの定義では範囲が広すぎてダメ。ドメインをもうちょっと制限してやる必要がある。
ので
add Z × Z → Z ↑ zero × id 0Z × Z
を書いて制限する。
- 整数と整数からある整数が求まる計算addがある
- 特殊な整数集合0ZからZへの射が存在する*4
間をすっ飛ばすと(射を合成すると)、0Z × Z → Z という風になって、0 + a が何らかの整数になることを表す射が存在することを書けた
a の射
0 + a これは書けた
→
0Z × Z Z
→
a 別の経路でZへ行くこの射を可換図で書ければ 0 + a と a が可換(等しい)と言える0Z × Z → Z は左をガン無視して右だけとればZになるのでright*5関数を設定すれば
add
Z × Z → Z
zero × id ↑ ／ right
0Z × Zとなって、0 + a(zero × idとaddの合成)とa(right)は可換(等しい)となる。
