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）、と、構文の違いを吸収できる。素晴らしい！ 上江州計算イケてるぜ。

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