11
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ Would you mind giving context for the LISP book? Does it have references for the results or the models it refers to? $\endgroup$ – cody Jul 19 '12 at 21:16
  • 1
    $\begingroup$ 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. $\endgroup$ – Chris Jul 20 '12 at 7:24
  • 1
    $\begingroup$ 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. $\endgroup$ – cody Jul 20 '12 at 8:37
14
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ 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. $\endgroup$ – Chris Jul 20 '12 at 7:45
  • $\begingroup$ French is irrelevant, you have the proof in front of your eyes. $\endgroup$ – Andrej Bauer Jul 20 '12 at 9:04
  • $\begingroup$ 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. $\endgroup$ – Andrej Bauer Jul 20 '12 at 9:05

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.