# 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.

• Would you mind giving context for the LISP book? Does it have references for the results or the models it refers to? – cody Jul 19 '12 at 21:16
• Yeah, it's Christian Queinnec's LISP in Small Pieces, p. 153. The excerpt with the mention: [...]Since then, the properties have been extended in several different ways, producing several different models: $D^\infty$ or $P_\omega$ in [Sco76, Sto77]. [...] Strangely enough, $P_\omega$ is extensional because two functions that compute the same thing at every point are equal, whereas $D^\infty$ is not extensional.[...] Sco76 stands for Dana Scotts' Data Types as Lattices. Sto77 stands for Joseph Stoys' Denotational Semantics: The Scott-Stachey Approach to Programming Language Theory. – Chris Jul 20 '12 at 7:24
• Thanks! In that case it is likely that there was a typo, that $D^\infty$ stands for $D_\infty$ and that it is $P_\omega$ that is not extensional. – cody Jul 20 '12 at 8:37

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.
• By the way, LIPS is not an extension of the $\lambda$-calculus, it is just inspired by it. Scheme could be considered an extension, although of course in Scheme extensionality fails badly due to presence of computational effects. – Andrej Bauer Jul 20 '12 at 9:05