型付きλ計算で不動点演算子が使えない話の続き

Erlangでパーサ・コンビネータ - kgbu?では、自分で証明できなかったので、プログラム意味論 (情報数学講座)で参考文献に挙げられていたプログラミング言語の基礎理論 (情報数学講座)のp.130あたりを読んでみた。
だいたい納得できた。やはり、有限の型では型付けができない、という話になるようだ。この場合、型のほうを拡張して、再帰的な型の定義ができればなんとかなるらしい。なるほど。