Extensionality of lambda calculus models I'm translating a book on LISP and naturally it touches some elements of $\lambda$-calculus. So, a notion of extensionality is mentioned there alongside some models of $\lambda$-calculus, namely: $\mathcal{P}_\omega$ and $D^\infty$ (yes, with the infinity at the top). And it is said that $\mathcal{P}_\omega$ is extensional while $D^\infty$ is not.

But... I was looking through the Barendregt's Lambda Calculus, It's Syntax and Semantics, and (hopefully, correctly) read there exactly the opposite: $\mathcal{P}_\omega$ is not extensional, $D_\infty$ is.

Does anybody know about that strange model $D^\infty$? Could it be just the same model as $D_\infty$, but erroneously written? Am I right about the extensionality of the models?

Thanks.
I presume that by extensionality you mean the law
$$(\forall x . f x = g x) \implies f = g.$$
If this is what you mean then the graph model $\mathcal{P}\omega$ is not extensional, while Dana Scott's $D_\infty$ is (I presume $D^\infty$ is Dana Scott's model of the $\beta\xi\eta\lambda$-calculus).

To see this, recall that $\mathcal{P}\omega$ is an algebraic lattice with the property that its space of continuous maps $[\mathcal{P}\omega \to \mathcal{P}\omega]$ is a proper retract of $\mathcal{P}\omega$, i.e., there are continuous maps
$$\Lambda : \mathcal{P}\omega \to [\mathcal{P}\omega \to \mathcal{P}\omega]$$
and
$$\Gamma : [\mathcal{P}\omega \to \mathcal{P}\omega] \to \mathcal{P}\omega$$
such that $\Lambda \circ \Gamma = \mathrm{id}$ but $\Gamma \circ \Lambda \neq \mathrm{id}$. Given $u, v \in \mathcal{P}\omega$, the application $u v$ is interpreted as $\Lambda(u)(v)$. Now take $u$ and $u'$ such that $u \neq u'$ but $\Lambda(u) = \Lambda(v)$ (these exist because $\Gamma \circ \Lambda \neq \mathrm{id}$). Then for all $v$ we have $u v = u v'$ yet $u \neq u'$. Extensionality is violated.

In contrast, $[D_\infty \to D_\infty]$ is isomorphic to $D_\infty$, i.e., there are continuous maps
$$\Lambda : D_\infty \to [D_\infty \to D_\infty]$$
and
$$\Gamma : [D_\infty \to D_\infty] \to D_\infty$$ which are inverses of each other. So consider any $u, u' \in D_\infty$ and suppose that $u v = u' v$ for all $v \in D_\infty$. This means that $\Lambda(u)(v) = \Lambda(u')(v)$ for all $v \in D_\infty$, hence $\Lambda(u) = \Lambda(u')$ and so $u = \Gamma(\Lambda(u)) = \Gamma(\Lambda(u')) = u'$. Extensionality is established.

We see that extensionality is a consequence of $\Gamma \circ \Lambda = \mathrm{id}$. What is the other equation $\Lambda \circ \Gamma = \mathrm{id}$ good for? For this we have to remember how $\lambda$-abstraction is interpreted:
$$\lambda X. u(X) = \Gamma (v \mapsto u(v))$$
In words, an expression $u(X)$ with a variable $X$ may be interpreted as a map which takes $v$ to $u(v)$. Then the $\lambda$-abstraction $\lambda X . u(X)$ is interpreted as the $\Gamma$-image of that function. Now from $\Lambda \circ \Gamma = \mathrm{id}$ we get
$$(\lambda X . u(X)) w = \Lambda (\Gamma (v \mapsto u(v))) (w) = (v \mapsto u(v))(w) = u(w)$$
which is just $\beta$-reduction.