Расширение моделей лямбда-исчисления

Я перевожу книгу на LISP и, естественно, она затрагивает некоторые элементы калькуляции. Таким образом, понятие экстенсиональности упоминается там наряду с некоторыми моделями λ- вычисления, а именно: P ω и D ∞ (да, с бесконечностью вверху). И говорят, что P ω экстенсиональна, а D ∞ нет.$\lambda$$\lambda$$\mathcal{P}_\omega$$D^\infty$$\mathcal{P}_\omega$$D^\infty$

Но ... Я просматривал лямбда-исчисление Барендрегта , его синтаксис и семантику и (надеюсь, правильно) прочитал с точностью до наоборот: не экстенсиональный, D ∞ есть.$\mathcal{P}_\omega$$D_\infty$

Кто-нибудь знает об этой странной модели ? Может ли это быть той же моделью, что и D ∞ , но ошибочно написана? Прав ли я по поводу расширенности моделей?$D^\infty$$D_\infty$

Спасибо.

Я предполагаю, что под экстенсиональностью вы подразумеваете закон Если это то, что вы имеете в виду, то модель графа P ω неявляетсяэкстенсиональной, в то время как D ∞ Даны Скоттаесть (я предполагаю, что D ∞ является моделью Даны Скотта β- ξ η λ- исчисления).

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

Чтобы увидеть это, напомним, что является алгебраической решеткой со свойством того, что ее пространство непрерывных отображений [ P ω → P ω ] является собственным ретрактом P ω , т. Е. Существуют непрерывные отображения Λ : P ω → [ P ω → P ω ] и Γ : [ P ω → P ω ] → P ω такое, что Λ ∘ Γ = i d, но $\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}$ . Для u , v ∈ P ω приложение u v интерпретируется как Λ ( u ) ( v ) . Теперь возьмем u и u ′ так , что u ≠ u ′, но Λ ( u ) = Λ ( v ) (они существуют, потому что Γ ∘ Λ ≠ i d ). Тогда для всех v мы имеем$\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$ все же u ≠ u ′ . Экстенсиональность нарушена.$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$