Erlangでパーサ・コンビネータ

lambda

なんて大それたことをするつもりは無かったんだけどなー。Javascriptでやってる人もいるくらいだから、、、とかいう考えで大ハマリ中。
（以下追記修正あり）
で、Erlangだと、anonymousな再帰関数はどうやって書くんだ？という問題にぶち当たった。
以下、とりあえず読んだもの

ErlangでのYコンビネータの定義（2)より

y(M) ->
  G = fun (F) -> M (fun(A) -> (F(F))(A) end) end,
  G(G).

Yコンビネータを使えば、F(f)=fとなる不動点として再帰関数を定義することになる。

erl> Fac = fun (F) ->
	      fun (0) -> 1;
		  (N) -> N * F(N-1)
	      end
      end.

erl> (y(Fac))(5).
120

ところで、λ計算できる関数だと、なぜ、常にこの不動点が存在することが保証されるのだろう？このあたりのことは、自分の持っている本としてはプログラム意味論 (情報数学講座)しか資料が無くて困った。(↑の話はp.21）
（6/20に追記：型なしのλ計算ならば、常に不動点が存在することは簡単に証明できる。上記の本の同じページに証明が書いてある。しかし、型つきのλ計算では、不動点のλ式は存在しない→練習問題2.8の5がその証明なのだが、結局自分では証明できなかった orz..　型つきλ計算だと、正しく型付けされている式は、必ず有限ステップで正規形に変換できるので、証明するならば、Ａ）M(FM) とFM の正規形を導いて、それが一致しないことを示す。Ｂ）有限のステップでは正規形に変換できない。できるとすると矛盾がある..のいずれかの方法だと思うのだが）
（6/21にBarendregtの論文を読んだメモを書き始めたが、中身はまだぐちゃぐちゃ）
(2008/Jun/28に追記：型付きλ計算で不動点演算子が使えない話の続き - kgbu?で、プログラミング言語の基礎理論 (情報数学講座)のp.130あたりを読むと納得できそう)

(3)で例として出てきたもの。Erlangのコマンドラインで、無名の再帰関数を使っている。

erl> Fact = fun(N) ->
        F1 = fun
                (0,_F) -> 1;
                (M,F) -> M * F(M-1,F)
        end,
        F1(N,F1)
end.

erl> Fact(5).
120

順番は逆だが、(1)でも、コマンドラインで無名の再帰関数を定義してみている。

erl> F = fun(Lambda, Line, N) ->
   case Line of
     [] -> N;
     [10 | Rest] -> Lambda(Lambda, Rest, N+1);
     [_ | Rest] -> Lambda(Lambda, Rest, N)
   end
 end.
#Fun
 F(F, "Hello\nWorld\n", 0).