圏論的な観点からいうと、シーケント計算て、圏のスジのような部分だけを議論している -- 圏をプレ順序集合に潰してしまうからな。シーケント計算では、圏の性質をキチンと捉えることはできない。が、単純化するもんだから計算も簡単になるメリットはある。…

次のものは、なんか入り口は同じようだ。 古典テンソル計算 複線形代数 結び目理論 ラムダ計算 シーケント計算 プログラムの制御構造 どれも結局、コンパクト閉圏、コンパクト論理、0次元または1次元のTQFTになる。

テンソル計算は線形コンパクト閉圏でやればいい。コンパクト閉圏の計算は、コンパクト論理と同じはず。コンパクト論理のシーケント計算はテンソル計算と同じはず。だから、テンソル計算のためのシーケント計算があるはず。で、それを書き下したいのだがなー。