ゲンツェンが構造規則と論理規則を分けた理由がサッパリわからなかったが、ハロ多圏とコア圏で考えてはじめて納得がいった。しかし、エライ人は、50年も100年も先を見られるんだな。なんでシーケントを考えついたのだろう？ 奇跡に思えるよ。ハーフツイスト…

結局、ハロ多圏の多射が項であって、コア圏の射が値だな。多射は図形だが、それは構文的な存在でもあり、項書き換えの対象となる。つまり、書き換え操作が計算であり2-多射でもある。計算の結果を対応さると、式と計算の意味論ができて、多圏のほうには、2-…

ゲルハルト・マック http://d.hatena.ne.jp/m-hiyama-memo/20080207/1202355931 を見よ。

Oが基本対象の集合として、Pは、O*にdom/codを持つ多射からなる多圏とする。多射の合成は2種類あり、f: Γ ⇒ Δ,Δ' と g:Δ',Ψ ⇒ Φ に対する f[;Δ']g と、 f:Γ ⇒ Δ',Δ と g:Ψ,Δ' ⇒ Φ に対する f[Δ';]g の2種。適当な公理は満たす。それとは別に、並置によるモノ…

ひたすら計算とは違った感じで合成（結合）を扱ってみる。(f;g)(x) = g^・(f^・x) が成立することを示す。まず、を考える。正確には、<f, g, x| Exec(g^, Exec(f^, x))> だが略記した。これをフルカリー化すると <|λf.λg.λx.(g^・(f^・x) >、この引数なし関数（値はコンビネータ）をcとする。</f,>…