γアノテーションとγ置換
CCC計算 - 檜山正幸のキマイラ飼育記 メモ編 で出したγ導入の件。γアノテーションという記法をラムダ計算に追加して、γアノテーションの導入規則も加える。γアノテーションの「γ」には何の意味もない。ギリシャ文字を適当に選んだだけ。ガンマ計算とかガンマ項と呼ぼう。
構文的には、Eが項のとき、γu.E も項となる。uは変数で、通常はEにuが自由に出現する。γアノテーションの動機は、項Eが型コンテキストと共に射 f:X→Y を表現するとき、f*:XA→Y* を表現する項が欲しいから。
γアノテーションは型コンテキストと共に使う。というか、型コンテキストがないと使えない。変数uは型コンテキスト内で u:X<-A のような指数型として宣言されている。宣言されてないとダメ。そのときに限り γu.E を項として使える。
γはバインダー（束縛子）ではない。変数uは自由なままに残る。しかし、γはスコープを持つ。スコープ内の項は、通常と扱いが変わる。置換方法が変わる。γで指定された変数をγ変数と呼ぶと、γ変数は自由だが、置換は変形される。
λa:A.G :X<-A のとき、次のような置換計算ができる。γ置換と呼ぶことにする。
(γu.E)[(λa:A.G)/u] --------------------- λa:A.(E[G/u]) :Y<-A
λ抽象でuを置換するとき、そのまま置き換えるのではなくて、λをはずした本体で置換してから、外側にλを付ける。γuは、変数uに対する置換がそのようにすることを指示する。
項Hが型 X<-A を持つがλ抽象でないときは、λa:A.(H a) としてλ抽象にする。η変換による同値を仮定している。H ≡ λa:A.(H a)
η同値性（η変換が同値であること）を仮定すれば、γ置換は常に出来る。
