ウエス計算2006 #2
上江州さんは、彼の計算（それを僕が「ウエス計算」と名付けた）を、トポスを扱うときのチョッとした道具くらいにしか考えてなかったのだろう。ていねいに作ってないし、まじめに説明もしてない。でも僕は、ウエス計算はそれなりに使えると思うから、再構成する。
Cは直積×でモノイド圏になっている。C⊆C'で、C'のほうは実際はデカルト閉圏としていいだろう。ラムダ風計算をするために、CをC'にまで拡張する必要がある。が、変数の変域割り当て#:V→|C|はCの範囲で考え、変数列への変域割り当てやベキの構成にはC'も使う。
変数列Xは集合ではないが、[X]を成分の集合とする。変数列に重複はないから、length(X) = card([X])。変数列に集合と同じような演算を同じ記号で定義する。
- X＼Y -- Xから、Yに出現する変数をすべて取り除く。
- X・Y -- 単なる連接、重複が生じる可能性あり。
- X∩Y -- Xを見ていって、Yにも出現する成分だけを取り出して列にする。
- X∪Y -- X・(Y＼X)
順序は3種類定義できる。
- X<≦Y -- XがYの接頭辞になっている。
- X≦Y -- XはYの部分列になっている。
- X⊆Y -- Xの成分はすべてYに出現する。
X∩Y≦Xだが、X∩Y≦Yではない（限らない）。X<≦X∪Yだが、Y<≦X∪Yではない。
X=(x1, ..., xn)として#(X)から#(x1)×...×#(xn) in CへのC'での同型射をιXと書いたが、これを
射影 #( (x1, ..., xn))-(ι)→#(x1)×...×#(xn)-(πi)→#(xi) をxi/Xと略記する。例えば、x1/X:#( (x1, ..., xn))→#(x1)。Xが文脈から明らかなときはxi/-と書く。Xごとにx1/Xの意味は変わるが、xi/- は一般的に「変数に対する射影」と解釈してよい。
C'の射fがf:#(X)→A（A∈C）の形をしているとき、fを変数列Xからの射または、X上のv→射と呼ぶ（v→射が上江州さんの呼称）。変数xが列Xに出現して、fが変数列Xからの射のとき、記号を乱用して x∈f と書く。
とりあえず、今回はここまで。ウエス抽象（圏的抽象）とチャーチ抽象（ラムダ抽象）が定義できたらウエス計算の定義だけは終わる。上江州さんは、ウエス計算をバキバキ使って、高階ハイティング・セオリーとトポスの間の関係とか、論理関手の随伴とかを具体的に構成しているのだが、知られてない、つうか忘れ去られているのだろう。MOTTAINAI.
