let式、上江州計算、カリー／ハワード対応

• Nick Benton他 A Term calculus for Intuitionistic Linear Logic →http://research.microsoft.com/~nick/tlca93.ps
• Masahito Hasegawa, Logical Predicates for Intuitionistic Linear Type Theories (1999) → http://citeseer.ist.psu.edu/hasegawa99logical.html

この2つで、let式の構文が違う（つうか逆）。ベントン達は let 式 be タプル変数、長谷川さんは let タプル変数 be 式。

let タプル変数:= 式として、タプル変数:= 式の部分を上江州方式で解釈すると、変数（変域の積）への射となる。これなら、let (x, y):= E in Fは、F・[(x, y):= E]という結合なので、(let g in f) ＝ f・g というやたらに単純な解釈となる。「タプル変数:= 式」と「式 =:タプル変数」を同じ意味だとすれば（f:=g ≡ g=:f ≡ g;f）、と、構文の違いを吸収できる。素晴らしい！ 上江州計算イケてるぜ。

ラムダ項の構文図（λは箱でなくノードとして束縛線を明示的に描く）と自然演繹の証明グラフをよく比べると、これも面白いこと（カリー／ハワード対応とか）が分かる。（カウフマンの言う）抽象テンソル計算、多圏の計算とかも関係しそうだし。

シーケント計算、書き換え／正規化構造

証明は自然演繹とする。

1. 仮定と結論を持つ証明図（ペトリネット風グラフ）
2. グラフ書き換え規則としての推論規則、書き換え過程としての証明行為
3. 仮定を除く（含意導入）規則
4. 公理は仮定と考えない
5. 特殊ケースとしての仮定のない証明図
6. 非形式的なシーケント＝証明図の仕様
7. 正しい証明図とは
8. シーケントに対する証明図、命題に対する証明図
9. シーケント、命題の証明可能性
10. 推論規則がシーケント表現ではどのように書けるか？
11. シーケントを最も簡単な証明図で意味付ける
12. 証明図の書き換え規則とシーケントの（ワンステップ）推論図

正規化構造（あるいは簡約構造、書き換え構造）を持つ集合でenrichされたグラフ（圏の素材）があるとき、グラフからの自由圏／自由複圏／自由多圏にも正規化構造を入れることができて、「自由結合＋正規化」がうまくできるなら、正規な射だけからなる目的の圏を作れる、って筋書きだな。

結局は図形の組み合わせ論では？

高次圏まで含めた圏とは、“なんらかの意味で「きれい」な”多面体分割を与えられた図形（CW複体とか）じゃなかろうか。その図形に代数演算がたくさん含まれている。代数的な法則は up-to-homotopy、または up-to-isotopy でしか成立しない。

up-to-homo/iso-topyなので、次元が異なる圏が同型（ホモトピー同値）だったりするわけだろう、たぶん。