<p>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 <em>not</em> extensional, while Dana Scott's $D_\infty$ is (I presume $D^\infty$ is Dana Scott's model of the $\beta\xi\eta\lambda$-calculus).</p>

<p>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.</p>

<p>In contrast, $[D_\infty \to D_\infty]$ is <em>isomorphic</em> 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.</p>

<p>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.</p>

CC BY-SA 3.0
2012-07-20T07:45:44.507Z
Great, thanks. So then I will assume that there is a factual error in the book. That may be possible, because the book itself is a translation from French, and there might be some double negation shenanigans in that paragraph of the original book, or something like that. Unfortunately, I don't have a French one to at least try to check.
Chris
CC BY-SA 3.0
2012-07-20T09:04:43.717Z
French is irrelevant, you have the proof in front of your eyes.
Andrej Bauer
CC BY-SA 3.0
2012-07-20T09:05:51.970Z
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
CC BY-SA 3.0
2012-07-19T20:59:50.637Z
2012-07-19T20:59:50.637Z
Andrej Bauer
<p>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.</p>

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

<p>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?</p>

<p>Thanks.</p>

CC BY-SA 3.0
2012-07-19T21:16:09.993Z
Would you mind giving context for the LISP book? Does it have references for the results or the models it refers to?
cody
CC BY-SA 3.0
2012-07-20T07:24:18.450Z
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
CC BY-SA 3.0
2012-07-20T08:37:23.787Z
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
<lo.logic><lambda-calculus><formal-modeling><extensionality>
Extensionality of lambda calculus models
Chris
# Extensionality of lambda calculus models

(Asked by: username_0 on 2012-07-19)

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.

**Tags:** lo.logic, lambda-calculus, formal-modeling, extensionality

> **Comments:**
> **username_1**: Would you mind giving context for the LISP book? Does it have references for the results or the models it refers to?  
> **username_0**: Yeah, it's username_0tian 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_.  
> **username_1**: 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.  

---

## 1 answers

### Answer by username_2 on 2012-07-19. Score: 14 | Accepted answer

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.

> **Comments:**
> **username_0**: Great, thanks. So then I will assume that there is a factual error in the book. That may be possible, because the book itself is a translation from French, and there might be some double negation shenanigans in that paragraph of the original book, or something like that. Unfortunately, I don't have a French one to at least try to check.  
> **username_2**: French is irrelevant, you have the proof in front of your eyes.  
> **username_2**: 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.  

---

