Extensionalidade de modelos de cálculo lambda

Estou traduzindo um livro sobre LISP e, naturalmente, ele toca alguns elementos do -calculus. Portanto, uma noção de extensionalidade é mencionada ao lado de alguns modelos de -calculus, a saber: e (sim, com o infinito no topo). E é dito que é extensional, enquanto não é.$\lambda$P ω D ∞ P ω D $\lambda$$\mathcal{P}_\omega$$D^\infty$$\mathcal{P}_\omega$$D^\infty$

Mas ... eu estava olhando o Cálculo Lambda de Barendregt , It's Syntax and Semantics e (esperançosamente, corretamente), li exatamente o oposto: não é extensional, é.D $\mathcal{P}_\omega$$D_\infty$

Alguém sabe sobre esse modelo estranho ? Poderia ser exatamente o mesmo modelo que , mas erroneamente escrito? Estou certo sobre a extensionalidade dos modelos?D $D^\infty$$D_\infty$

Obrigado.

Presumo que por extensionalidade você queira dizer a lei Se é isso que você quer dizer, o modelo gráfico não é extensional, enquanto o Dana Scott é (presumo que é o modelo de Dana Scott do - cálculo).P ω D ∞ D ∞ β ξ η

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

Para ver isso, lembre-se de que é uma estrutura algébrica com a propriedade de que seu espaço de mapas contínuos é uma retração adequada de , ou seja, existem mapas contínuos e modo que mas . Dado , o aplicativo é interpretado como . Agora pegue[ P ω → P ω ] P ω Ganhe muitos : P ω → [ P ω → P ω ] Γ : [ P ω → P ω ] → P ω Ganhe muitos ∘ Γ = i d Γ ∘ Ganhe muitos ≠ i d u , v ∈ P ω u v Λ ( u ) ( $\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}$$\Gamma \circ \Lambda \neq \mathrm{id}$$u, v \in \mathcal{P}\omega$$u v$$\Lambda(u)(v)$$u$e tal que mas (elas existem porque ). Então, para todos os , temos ainda . Extensionalidade é violada.$u'$$u \neq u'$$\Lambda(u) = \Lambda(v)$$\Gamma \circ \Lambda \neq \mathrm{id}$$v$$u v = u v'$$u \neq u'$

Por outro lado, é isomórfico para , ou seja, existem mapas contínuos e que são inversos um do outro. Portanto, considere qualquer e suponha que para todos . Isso significa que para todos os , portanto e, portanto, . Extensionalidade é estabelecida.$[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'$

Vemos que a extensionalidade é uma consequência de . Para que serve a outra equação ? Para isso, devemos lembrar como -abstraction é interpretada: Em palavras, uma expressão com uma variável pode ser interpretada como um mapa que leva para . Em seguida, a -abstraction é interpretado como a imagem dessa função. Agora em obtemos $\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)$$ que é apenas redução.$\beta$