デカルト閉圏(CCC) - pogi-log

デカルト閉圏(CCC)

デカルト閉圏(デカルトへいけん、Cartesian Close Category; CCC)

プログラミング言語はデカルト閉圏と対応があると言えるらしい。

正確には単純型付きラムダ計算と対応がある

単純型付きラムダ計算はデカルト閉圏という圏と対応がある

[Lambek1986]で確認されている

圏$ C がデカルト閉である条件は

$ C が終対象を持つ

対象$ 1 が存在し、任意の対象$ A に対して唯一の射$ !_a : A \to 1 を持つ

$ C の任意の二対象$ A, B に対し、$ C はそれらの直積$ A × B を対象に持つ

$ C の任意の二対象$ A, B に対し、$ C はそれらの冪対象$ B^A を対象に持つ。

プログラムを圏との対応を考えると

型が対象

関数が射

関数合成が射の合成

id関数が恒等射

確認用

Q. デカルト閉圏とは

関連

モノイダル圏

極限と余極限

始対象と終対象

参考

『計算機科学のための圏論の基礎の基礎』

プログラマであるあなたが圏論を学んで得られる事、得られない事 - Creatable a => a -> IO b

relation between type theory and category theory in nLab

デカルト閉圏とその応用（1/3）... 概要 - YouTube

https://www.youtube.com/watch?v=en7Y0aYvza4

デカルト閉圏とその応用（2A/3）... デカルト閉圏の基礎その１積，極限，和，余極限の復習 - YouTube

https://www.youtube.com/watch?v=zkZIWTDkXwE

カルテジアン閉圏とは，ひとことで言うと，有限直積(finite products)と冪(exponentials)を持つ圏です．

ref: 『圏論の歩き方』P64

メモ

デカルト閉圏とその応用（2B/3）... デカルト閉圏の基礎その２冪（べき）とデカルト閉圏 - YouTube

https://www.youtube.com/watch?v=3CvHDVvOWi0

https://m-hiyama.hatenablog.com/entry/20110131/1296434095

[Lambek1986] Joachim Lambek, Philip J. Scott, Introduction to higher order categorical logic, Cambridge Studies in Advanced Mathematics 7 (1986) (ISBN: 0-521-24665-2, pdf)