圏を直接扱うプログラミング言語
ヤノフスキ―がSammyという言語を定義している。
- Kolmogorov Complexity of Categories (2013)
- Noson S. Yanofsky
- 16p
- https://pdfs.semanticscholar.org/bbf1/5662508b3efe27999ad9506e6ba17b1be397.pdf
- Kolmogorov Complexity of Categories (2013) スライド
- Noson S. Yanofsky
- 42p
- http://www.cs.ox.ac.uk/sa60/slides/yanofsky-samsonfest-2013.pdf
- Computability and Complexity of Categorical Structures (2015)
- Noson S. Yanofsky
- 33p
- https://arxiv.org/abs/1507.05305
2013論文の5pから8pにかけてSammyの記述がある。スライドでは、7pから13pにかけて。2015論文の最後のページ（33p）にSammyの基本演算の表がある。
Operations in the Sammy Programming Language
| Operation | Input | Output | Note |
|---|---|---|---|
| Source1 | Functor | Category | Source of the functor |
| Source2 | N.T. | Functor | Source of the N.T. |
| Target1 | Functor | Category | Target of the functor |
| Target2 | N.T. | Functor | Target of the N.T. |
| Ident0 | Category | Functor | Identity functor of a category |
| Ident1 | Functor | N.T. | Identity N.T. of a functor |
| Op0 | Category | Category | Opposite category |
| Op1 | Functor | Functor | Opposite functor |
| Comp | 2 composable funcs | Functor | Composition of functors |
| Hcomp | 2 composable N.T. | N.T. | Horizontal composition of N.T.s |
| Vcomp | 2 composable N.T. | N.T. | Vertical composition of N.T.s |
| Pow0 | 2 categories | Category | Power category |
| Pow1 | 2 functors | Functor | Power functor |
| KanEx | 2 functors | Functor & N.T. | Right Kan extension |
| KanExInd | 3 functors and a N.T. | N.T. | Induced by right Kan extension |
| KanLif | 2 functors | Functor & N.T. | Right Kan lifting |
| KanLifInd | 3 functors and a N.T. | N.T. | Induced by right Kan lifting |
| ◦ | Category | Functor | The functor C2 ×C1 C2 → C2 |
| If | 2 N.T.s and label | Conditional break operation | |
| Return | Cat, func and/ or NT | Final statement of a program |
powerは指数のことだろう。Pow0(C, D) := DC かな？ 指数構成とカン拡張が基本演算。
エンドの計算 - 檜山正幸のキマイラ飼育記 メモ編で引用した次の論文、
- A Higher-Order Calculus for Categories (2001)
- Mario Jose Caccamo, Glynn Winskel
- 27p
- http://www.brics.dk/RS/01/27/BRICS-RS-01-27.pdf
これも形式的な言語を導入している。こっちはBNFで、
- C ::= Set | 0 | 1 | C^op | C1 × C2 | C1 + C2 | [C, C]
という圏構成子を使っている。この上にある種のラムダ計算を構成するが、基本絵算にエンドとコエンドを入れている。
極限・余極限、エンド・コエンド、カン拡張などは相互に定義しあうので、どれを基本にとってもいいが、このような超越的な演算がどっちにしろ必要ということだろう。
