Extensionalidad de los modelos de cálculo lambda

Estoy traduciendo un libro sobre LISP y, naturalmente, toca algunos elementos del cálculo . Entonces, una noción de extensionalidad se menciona allí junto con algunos modelos de cálculo λ , a saber: P ω y D ∞ (sí, con el infinito en la parte superior). Y se dice que P ω es extensional mientras que D ∞ no lo es.$\lambda$$\lambda$$\mathcal{P}_\omega$$D^\infty$$\mathcal{P}_\omega$$D^\infty$

Pero ... Estaba mirando el cálculo Lambda de Barendregt , su sintaxis y semántica , y (con suerte, correctamente) leí exactamente lo contrario: no es extensional, D ∞ sí .$\mathcal{P}_\omega$$D_\infty$

¿Alguien sabe acerca de ese extraño modelo ? ¿Podría ser el mismo modelo que D ∞ , pero escrito erróneamente? ¿Estoy en lo cierto acerca de la extensionalidad de los modelos?$D^\infty$$D_\infty$

Gracias.

Supongo que por extensionalidad te refieres a la ley Si esto es lo que quiere decir entonces el modelo gráfico P ω esnoextensional, mientras que de Dana Scott D ∞ es (supongo D ∞ es el modelo de Dana Scott, del ß xi eta lambda -calculus).

$$(\forall x . f x = g x) \implies f = g.$$ $\mathcal{P}\omega$$D_\infty$$D^\infty$$\beta\xi\eta\lambda$

Para ver esto, recuerde que es una red algebraica con la propiedad de que su espacio de mapas continuos [ P ω → P ω ] es una retracción adecuada de P ω , es decir, hay mapas continuos Λ : P ω → [ P ω → P ω ] y Γ : [ P ω → P ω ] → P ω tal que Λ ∘ Γ = i d pero $\mathcal{P}\omega$$[\mathcal{P}\omega \to \mathcal{P}\omega]$$\mathcal{P}\omega$

$$\Lambda : \mathcal{P}\omega \to [\mathcal{P}\omega \to \mathcal{P}\omega]$$ $$\Gamma : [\mathcal{P}\omega \to \mathcal{P}\omega] \to \mathcal{P}\omega$$ $\Lambda \circ \Gamma = \mathrm{id}$ . Dado u , v ∈ P ω , la aplicación u v se interpreta como Λ ( u ) ( v ) . Ahora tome u y u ′ de modo que u ≠ u ′ pero Λ ( u ) = Λ ( v ) (estos existen porque Γ ∘ Λ ≠ i d ). Entonces para todos v tenemos$\Gamma \circ \Lambda \neq \mathrm{id}$$u, v \in \mathcal{P}\omega$$u v$$\Lambda(u)(v)$$u$$u'$$u \neq u'$$\Lambda(u) = \Lambda(v)$$\Gamma \circ \Lambda \neq \mathrm{id}$$v$ todavía u ≠ u ′ . La extensión se viola.$u v = u v'$$u \neq u'$

$[D_\infty \to D_\infty]$$D_\infty$

$$\Lambda : D_\infty \to [D_\infty \to D_\infty]$$ $$\Gamma : [D_\infty \to D_\infty] \to D_\infty$$ $u, u' \in D_\infty$$u v = u' v$$v \in D_\infty$$\Lambda(u)(v) = \Lambda(u')(v)$$v \in D_\infty$$\Lambda(u) = \Lambda(u')$$u = \Gamma(\Lambda(u)) = \Gamma(\Lambda(u')) = u'$

$\Gamma \circ \Lambda = \mathrm{id}$$\Lambda \circ \Gamma = \mathrm{id}$$\lambda$

$$\lambda X. u(X) = \Gamma (v \mapsto u(v))$$ $u(X)$$X$$v$$u(v)$$\lambda$$\lambda X . u(X)$$\Gamma$$\Lambda \circ \Gamma = \mathrm{id}$ $$(\lambda X . u(X)) w = \Lambda (\Gamma (v \mapsto u(v))) (w) = (v \mapsto u(v))(w) = u(w)$$ $\beta$