Rozległość modeli rachunku lambda

Tłumaczę książkę na temat LISP i oczywiście dotyka ona niektórych elementów rachunku. Zatem wzmiankowane jest pojęcie ekstensywności wraz z niektórymi modelami rachunku, a mianowicie: i (tak, z nieskończonością u góry). I mówi się, że jest ekstensjonalny podczas nie jest. $\lambda$ $\lambda$ $\mathcal{P}_\omega$ $D^\infty$ $\mathcal{P}_\omega$ $D^\infty$

Ale ... Patrzyłem na rachunek Lambda Barendregta , jego składnię i semantykę , i (mam nadzieję, poprawnie) przeczytałem dokładnie odwrotnie: nie jest ekstensywne, jest. $\mathcal{P}_\omega$ $D_\infty$

Czy ktoś wie o tym dziwnym modelu ? Czy może to być ten sam model co , ale błędnie napisany? Czy mam rację co do ekstensywności modeli? $D^\infty$ $D_\infty$

Dzięki.

— Chris
źródło

Czy mógłbyś podać kontekst dla książki LISP? Czy zawiera odniesienia do wyników lub modeli, do których się odnosi?

— cody

Tak, to LISP Christian Queinnec in Small Pieces , str. 153. Fragment ze wzmianką: [...] Od tego czasu właściwości zostały rozszerzone na kilka różnych sposobów, tworząc kilka różnych modeli:

lub

w [Sco76, Sto77]. [...] o dziwo,

jest ekstensjonalny ponieważ dwie funkcje, które obliczają to samo w każdym punkcie są równe, natomiast

nie jest ekstensjonalny. [...] stoi Sco76 dla Dana Scotts' typów danych, jak Gratki . Sto77 oznacza Denotational Semantics Josepha Stoysa : The Scott-Stachey Approach to Programming Language Theory .

D^{\infty}

$D^\infty$

P_{ω}

$P_\omega$

P_{ω}

$P_\omega$

D^{\infty}

$D^\infty$

— Chris

Dzięki! W takim przypadku prawdopodobne jest, że wystąpiła literówka, że

oznacza

i że to

nie jest ekstensywne.

D^{\infty}

$D^\infty$

D_{\infty}

$D_\infty$

P_{ω}

$P_\omega$

— cody

Zakładam, że przez ekstensywność rozumiesz prawo Jeśli to jest to, co masz na myśli następnie model wykres jestnieekstensjonalny, natomiast Dana Scotta jest (jak mniemam jest modelem Dana Scotta z -calculus).

(\forall x . f x = g x) ⟹ f = g .

$(\forall x . f x = g x) \implies f = g.$

P ω

$\mathcal{P}\omega$

D_{\infty}

$D_\infty$

D^{\infty}

$D^\infty$

β ξ η λ

$\beta\xi\eta\lambda$

Aby to zobaczyć, przypomnij sobie, że jest siecią algebraiczną z tą właściwością, że jej przestrzeń ciągłych map jest właściwym wycofaniem , tzn. Istnieją ciągłe mapy i tak, że ale $\mathcal{P}\omega$ $[\mathcal{P}\omega \to \mathcal{P}\omega]$ $\mathcal{P}\omega$

Λ : P ω \to [P ω \to P ω]

$\Lambda : \mathcal{P}\omega \to [\mathcal{P}\omega \to \mathcal{P}\omega]$

Γ : [P ω \to P ω] \to P ω

$\Gamma : [\mathcal{P}\omega \to \mathcal{P}\omega] \to \mathcal{P}\omega$

Λ \circ Γ = i d

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

. Biorąc pod uwagę

, aplikacja

jest interpretowana jako

. Teraz weź

tak, że

ale

(istnieją, ponieważ

). Zatem dla wszystkich

mamy

Γ \circ Λ \neq i d

$\Gamma \circ \Lambda \neq \mathrm{id}$

u, v \in P ω

$u, v \in \mathcal{P}\omega$

u v

$u v$

Λ (u) (v)

$\Lambda(u)(v)$

u

$u$

u^{'}

$u'$

u \neq u^{'}

$u \neq u'$

Λ (u) = Λ (v)

$\Lambda(u) = \Lambda(v)$

Γ \circ Λ \neq i d

$\Gamma \circ \Lambda \neq \mathrm{id}$

v

$v$

jeszcze

. Przestępczość jest naruszona.

u v = u v^{'}

$u v = u v'$

u \neq u^{'}

$u \neq u'$

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

Λ : D_{\infty} \to [D_{\infty} \to D_{\infty}]

$\Lambda : D_\infty \to [D_\infty \to D_\infty]$

Γ : [D_{\infty} \to D_{\infty}] \to D_{\infty}

$\Gamma : [D_\infty \to D_\infty] \to D_\infty$

u, u^{'} \in D_{\infty}

$u, u' \in D_\infty$

u v = u^{'} v

$u v = u' v$

v \in D_{\infty}

$v \in D_\infty$

Λ (u) (v) = Λ (u^{'}) (v)

$\Lambda(u)(v) = \Lambda(u')(v)$

v \in D_{\infty}

$v \in D_\infty$

Λ (u) = Λ (u^{'})

$\Lambda(u) = \Lambda(u')$

u = Γ (Λ (u)) = Γ (Λ (u^{'})) = u^{'}

$u = \Gamma(\Lambda(u)) = \Gamma(\Lambda(u')) = u'$

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

λ X . u (X) = Γ (v \mapsto u (v))

$\lambda X. u(X) = \Gamma (v \mapsto u(v))$

u (X)

$u(X)$

X

$X$

v

$v$

u (v)

$u(v)$

λ

$\lambda$

λ X . u (X)

$\lambda X . u(X)$

Γ

$\Gamma$

Λ \circ Γ = i d

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

(λ X . u (X)) w = Λ (Γ (v \mapsto u (v))) (w) = (v \mapsto u (v)) (w) = u (w)

$(\lambda X . u(X)) w = \Lambda (\Gamma (v \mapsto u(v))) (w) = (v \mapsto u(v))(w) = u(w)$

β

$\beta$

— Andrej Bauer
źródło

Wielkie dzięki. Zakładam więc, że w książce jest błąd faktyczny. Może to być możliwe, ponieważ sama książka jest tłumaczeniem z języka francuskiego, aw tym akapicie oryginalnej książki może być kilka podwójnych negacji. Niestety nie mam francuskiego, żeby przynajmniej spróbować sprawdzić.

— Chris

Francuski nie ma znaczenia, masz dowód przed oczami.

— Andrej Bauer,

λ

$\lambda$