γアノテーションは、束縛子や限量子と似た構文で、γ記号の後に変数を伴いスコープを持つ。γにくっついている変数をγ変数と呼ぶことにする。γアノテーションに変数の束縛作用はなくて、γアノテートされた項（スコープ内部）でγ変数は自由のままである。したが…

CCC計算 - 檜山正幸のキマイラ飼育記 メモ編 で出したγ導入の件。γアノテーションという記法をラムダ計算に追加して、γアノテーションの導入規則も加える。γアノテーションの「γ」には何の意味もない。ギリシャ文字を適当に選んだだけ。ガンマ計算とかガンマ…

本編： 感動か効率性か - 檜山正幸のキマイラ飼育記 オカシイと文句を垂れるなら、修正案を提示しないとね。シーケントの左辺が型宣言の集まり、右辺が型付き代入文の集まりとなる形を仮にCCCシーケントと呼ぶ。CCCシーケントの意味はデカルト閉圏の射だが、…