ラムダ計算の話でD \simeq D \to Dが出てくる理由が分かりかけたけどやっぱりよく分からない

ラムダ計算の数学的体系を考えようとすると
$D \simeq D \to D$
となってしまうので, 普通の方法ではうまくいきませんよね, みたいな話をdomain theoryの導入ではしばしば見かける.
大体の文献でほとんど自明みたいに書かれるから, ずっとよく分からなかったのだけど, やっと意味が分かりかけた.

一番シンプルなuntyped lambda calculusは,

term := variable
      | lambda variable . term
      | term term

みたいに定義できる.
上記以外はtermではない.

この, 3つ目が厄介の原因なのだ.
すべてのtermについて, それはtermからtermへの関数と見ることができる.
ラムダ項 $\lambda x . x$ は明らかにtermからtermへの関数だ.
それだけでなく, variableである $x$ も, $x(\lambda y. y)$ みたいにして関数になることができる. (untyped lambda calculusでは)
$x y$ だって, $(x y) z$ みたいにできるので, termからtermへの関数だ.

すべてのtermの集合を $D$ とする.
そのすべての元 $x\in D$ について, それは $D\to D$ の元である.
逆に, 何らかのtermからtermへの写像があるとき, それはtermであると考えることができる(←？)
すなわち
$D \simeq D \to D$
なのだけど, cardinaryを考えるとこの一対一対応はありえない.

まぁこういうことなのだ.
... わけだけど, 「逆に」の部分は明らかに間違っていて, 例えば

x -> y
a -> a (otherwise)

みたいな写像は, 確かにtermからtermへの写像なのだけど, termでは書けない.
んー, なんか掴みかけたのだけど証明が崩壊していて気持ち悪い気分.
$D \subseteq D \to D$ だったらなんの矛盾も起きない...
困ったものだなぁ...

$\lambda x. x x$ みたいなラムダ項に型を与えることを考える.
$x: D$ とすると, $x : D \to E$ みたいになって,
$D \simeq D \to E$
だから $\left|E\right| \ge 2$ だとcardinaryがおかしいね.
みたいなことを, 書いてる人もよく見かける.
いわゆるdomain equationってやつ.
まぁこれは型付け不能としてrejectすればいいのかな, それともcardinaryを考えることがnonsenceなのかもしれない.
(なんでこの話で $D \simeq D\to D$ になるのかはよくわかんない)

最近はuntyped lambda calculusに興味がある.
categoricalなsemanticsと, domain theoryには1年以上も前から関心があるのだけど, いまいちきちんと掴めてない.
ここら辺の文献を調べまくって, untyped lambda calculusをベースにした言語を作りたい(パーサーを簡単なevaluatorはすでにある)
どの文献を読めばいいのかっていうのはすでに把握しているのだけど, 本業(プログラミングとは全く関係ない)があまりに忙しい.
就職したら片手間に勉強し始められるんじゃないかなー... みたいな淡い期待がある.
というか, categoryとdomainをちゃんと理解してる人, 日本人のブログでほとんど見たことないなー.