数理論理学（数学基礎論）　その14

7 ：１３２人目の素数さん：2019/03/24(日) 21:34:57.51 ID:FOTRZJL+.net

>>5
> Yコンビネータ
・・・
> Y = (λf . (λx . f (x x)) (λx . f (x x)))
> 評価戦略が名前渡しの場合はこのまま使える。 ・・・

これは間違い。評価戦略が名前渡しであっても Y は使えない。それを示すために
君が書き下してくれたY gの式変形をどちら向きにも進める変換 “＝” による等式でなく
簡約 “→” による評価として→で向き付けられた形に書き直してみよう。

（“≡” は構文的に同一の項であることを示す。なお、「α変換」は
束縛変数に対する名前の付け替えというメタ言語的な操作なので
ここではα変換の前後は構文的に同一の項として扱い“≡”で示した）

　 Y g
≡ (λf . (λx . f (x x)) (λx . f (x x))) g (Yの定義より)
→ (λx . g (x x)) (λx . g (x x)) (λfのβ簡約、主関数をgに適用)
≡ (λy . g (y y)) (λx . g (x x)) (α変換、束縛変数の名前を変える)
→ g ((λx . g (x x)) (λx . g (x x))) (λyのβ簡約、左の関数を右の関数に適用)
← g (Y g) (第2式より)

最後のステップが逆向きの簡約 “←” であることに注意。
このステップは絶対に本来の簡約 “→” の向きには書き直せないので
Y コンビネータは名前呼びでも使えないことが分かる。

名前呼びの簡約戦略の場合に正しく動く不動点コンビネータで最も有名な例は
Turing のΘコンビネータで、λ項として書き下すと以下のようになる：

Θ ≡ (λx y, y(x x y))(λx y, y(x x y))

最後に、これを用いた Θg という項が簡約によって確かに g(Θg) になることを確かめておく：

　 Θ g
≡ ((λx y, y(x x y))(λx y, y(x x y))) g
≡ ((λz w, w(z z w))(λx y, y(x x y))) g　・・・・・・・・・・・・　α変換
→ (λw. w((λx y, y(x x y))(λx y, y(x x y)) w)) g　・・・　 β簡約
≡ (λw. w(Θ w)) g　・・・・・・・・・・・・・・・・・・・・・・・・・・・・・　Θの定義で置き換え
→ g(Θ g)

なお、値呼びの簡約戦略で正しく動く不動点コンビネータも勿論ある。
具体的な定義は、例えば次にある：
Daniel P. Friedman & Matthias Felleisen “The Little Schemer” 4th ed., p. 172 (The MIT Press, 1996).