イータ変換までやるかな、それと、大きなラムダの基本概念とか

土曜日の目標を、ベータ変換だけでなくイータ変換までにしようかと、もし可能ならだが。ガンマオペレーション＝脱抽象が、ラムダオベレーション＝抽象の逆であることを理解する。

背景となる意味的な法則は：

• Exec(λt.(φ・t), a) = Exec(φ, a)

である。ここで； Execは解釈実行系（評価系＝関数ランタイムエンジン）、ラムダ式は関数コードとして解釈し、記号「・」はExec自身の実行を表す（指示する）演算子。

これを「Execの中の人」の立場で解釈すると、

• λt.(φ・t) ⇒ φ

という事前処理を行うことになる。この関数コードの事前（実行に先立つ）処理をイータ変換と呼ぶ。次が、イータ法則、あるいはイータ仮説と呼んでいいだろう。

• なかの人がイータ変換を行っても実行結果に影響を与えない。

ところでガンマオペレーションは、g = <x| g(x)> に対して <x, t|Exec(g(x), t)> として与えられる。次のイータ・コード化ルールを設ける。

• Λt<x, t| Exec(g(x), t)> = <x| λt.(g(x)・t) >

この段階で既に、記号「・」の導入とイータ・コード化ルール、イータ仮説（イータ変換が意味的に妥当とする仮説）、イータ変換を行う解釈実行系などを導入している。イータ変換合理化のために、けっこう色々やっているのだ。

これらの下準備のもとで：

   Γ(g)

  = Γt<x| g(x)>

  = <x, t| Exec(g(x), t) >
以上Γオペレーションの定義
   Λ(Γ(g))

 = Λt<x, t| Exec(g(x), t) >

 // イータ・コード化ルール（ドットの使用）

 = <x| λt.(g(x)・t) >

 // イータ仮説、イータ変換の実施

 = <x| g(x) >

 // 大きいラムダのイータ法則

 = g

大きいラムダ計算は、対象となる（オブジェクトレベル）の言語／計算ではなくて、記述用の外の言語だから妥当性は天下りに信じるか、直観に訴えるしかない。大きいラムダ計算でも、アルファ、ベータ、イータの法則（等式）がある。

1. アルファ： <x | f(x)> = <y | f(y)>
2. ベータ： <x | f(x)>(a) = f(a)
3. エータ： <x | f(x)> = f