プログラミング言語をひとつ与えることは、結局は指標を与えることと同じで、問題は指標から自由圏を作る一種の閉包演算<->のほうだな。どのような種類の自由圏（エルブラン圏、項集合）を与えるかがプログラミング言語構文の特徴付けになる。閉包演算<->は…

指標圏に境界概念とグルーイングを導入して、コボルディズム的な二重圏だと考える。インスティチューションをこの二重圏の上で定義する。すると、Mod、Sen、Spec、Theo（Sen上に作る順序集合）なども拡張されるだろう。さらに、証明系ProofやプログラムProg…

有向グラフとしての指標Σと部分有向グラフΦ、Ψを一緒にした(Σ, Φ, Ψ)を射とするコボルディズム圏を考えることができる。このコボルディズムでは次元概念は役割を演じない。圏Cに対してΣ代数圏 C-AlgΣは、関手圏C<Σ>として定義する。コボルディズム指標(Σ, Φ,…

もう少し考えよう。有向グラフとしての指標Σ（有限に限らない！）、部分有向グラフΦ、Ψを一緒に考える。|Φ| = B を基本(basic)ソート、|Ψ| = D を公開定義（public defined）ソートと呼ぶ。別な部分グラフΔ⊆Σがあるとして、Δの辺はコンストラクタ演算記号と…

指標は単なる有向グラフと考えてよい（そう考えるべき！）。境界付きグラフがあるんだから境界付き指標があってもいい。BHKのconstructor-based指標Σを考える。ソートにはlooseとconstrainedがあるが、これをbasicとdefinedと呼び替える。basicソートとbasic…

Bidoit/Hennicker/Kurzはさすがに書くのに長すぎるからBHKと略記する。