Kombinacyjna interpretacja rachunku lambda

10

Według Petera Selinger , Lambda Rachunek jest algebraiczna (PDF). Na początku tego artykułu mówi:

Kombinacyjna interpretacja rachunku lambda jest znana jako niedoskonała, ponieważ nie spełnia reguły $ξ$ : zgodnie z interpretacją $M = N$ nie oznacza $\lambda x.M = \lambda x.N$ (Barendregt, 1984).

Pytania:

Jaki rodzaj równoważności ma tu na myśli?
Biorąc pod uwagę tę definicję równoważności, jaki jest kontrprzykład tego wniosku?

terminology lambda-calculus combinatory-logic

— Simon Shine
źródło

7

Równoważność jest po prostu równoważnością omawianej teorii równań . W tym przypadku jest to teoria przedstawiona w tabeli 1. Zauważ, że teoria ta nie obejmuje : uczyni to teorię ekstensywną, a ostatecznie chodzi o to, że szanuje intensywność , podczas gdy spowoduje CL częściowo ekstensywny. Nie jestem pewien, dlaczego druga odpowiedź wspomina . $\lambda$ $\eta$ $\xi$ $\lambda$ $\eta$

Zauważ, że w : $\lambda$

\begin{matrix} (1) & (M =_{β} N) ⟹ (λ x . M =_{β} λ x . N) \end{matrix}

$(M =_\beta N) \Longrightarrow (\lambda x.M =_\beta \lambda x.N) \tag{1}$

Powinno to być intuicyjnie oczywiste: jeśli jest -wymienialne na gdy stoi samo, to jest też -wymienialne na gdy jest podtermem . $M$ $\beta$ $N$ $\beta$ $N$ $\lambda x.M$

Regułę zdefiniowany jako umożliwia bezpośrednie wnioskowanie, gdy jest częścią teorii . Jego analogiem CL będzie: $\xi$

\begin{aligned} M & = N \\ (ξ_{λ}) & (λ x . M) & = (λ x . N) \end{aligned}

$\begin{align} M &\;= N \\ \hline (\lambda x.M) &\;= (\lambda x.N) \tag{$\xi_\lambda$} \end{align}$

λ

$\lambda$

\begin{aligned} M & = N \\ (ξ_{C L}) & (λ^{*} x . M) & = (λ^{*} x . N) \end{aligned}

$\begin{align} M &\;= N \\ \hline (\lambda^* x.M) &\;= (\lambda^* x.N) \tag{$\xi_{CL}$} \end{align}$

Chodzi o to, że w CL nie ma zastosowania :

\begin{matrix} (2) & (M =_{w} N) ⟹ (λ^{*} x . M =_{w} λ^{*} x . N) \end{matrix}

$(M =_w N) \Longrightarrow (\lambda^* x.M =_w \lambda^*x.N) \tag{2}$

Innymi słowy, jeśli dwa terminy są słabo równe, to niekoniecznie jest tak w przypadku ich pseudoabstrakcyjnych wersji.

W związku z tym, jeśli dodamy do teorii CL, wówczas zaczniemy równanie terminów, które mają różne formy normalne. $\xi_{CL}$

Uwaga. Tutaj oznacza słabą równość. Oznacza to, że można przekonwertować na (i odwrotnie) poprzez serię i (prawdopodobnie również , jeśli jest to część teorii). Jak zapewne wiesz, jest analogiem CL dla . $M =_w N$ $M$ $N$ $\mathsf{S}$ $\mathsf{K}$ $\mathsf{I}$ $=_w$ $=_\beta$

$\lambda^*$ to pseudoabstrakcja zdefiniowana na stronie 5 dokumentu. Ma następującą właściwość:

\begin{matrix} (3) & (λ^{*} x . M.) N. ⊳_{w} [N. / x] M. \end{matrix}

$(\lambda^*x.M)N \rhd_w [N/x]M \tag{3}$

Ta właściwość ułatwia znalezienie analogu CL dla dowolnego -termu: wystarczy zmienić na i zastosować tłumaczenia zgodnie z definicją . $\lambda$ $\lambda$ $\lambda^*$ $\lambda^*$

Dla jasności, „kontrprzykład” w tej odpowiedzi nie jest kontrprzykładem na (2). Ponieważ jeśli mamy:

\begin{matrix} (4) & M. = x \end{matrix}

$M = x \tag{4}$

\begin{matrix} (5) & N. = (λ^{*} z . z) x \end{matrix}

$N = (\lambda^*z.z)x \tag{5}$

Wtedy naprawdę oznacza (stosując tłumaczenia strony 5 oraz fakt, że jest zdefiniowany jako na końcu strony 4): $N$ $\mathsf{I}$ $\mathsf{SKK}$

\begin{matrix} (6) & N. = (λ^{*} z . z) x = ja x = S. K. K. x \end{matrix}

$N = (\lambda^*z.z)x = \mathsf{I}x = \mathsf{SKK}x \tag{6}$

Ponieważ , to w rzeczywistości ma to . Jeśli jednak jest to przeciwny przykład, powinniśmy mieć to . Ale jeśli tłumaczymy, w rzeczywistości otrzymujemy: $\mathsf{SKK}x \rhd_w \mathsf{K}x(\mathsf{K}x) \rhd_w x$ $M =_w N$ $(\lambda^* y. M) \not=_w (\lambda^* y. N)$

\begin{matrix} (7) & (λ^{*} y . M.) = (λ^{*} y . x) = K. x \end{matrix}

$(\lambda^* y. M) = (\lambda^* y. x) = \mathsf{K}x \tag{7}$

\begin{matrix} (8) & (λ^{*} y . N.) = (λ^{*} y . S. K. K. x) = K. (S. K. K. x) \end{matrix}

$(\lambda^* y. N) = (\lambda^* y. \mathsf{SKK}x) = \mathsf{K}(\mathsf{SKK}x)\tag{8}$

Łatwo jest zweryfikować, że (7) i (8) są wciąż słabo równe, ponieważ:

\begin{matrix} (9) & K. (S. K. K. x) ⊳_{w} K. (K. x (K. x)) ⊳_{w} K. x \end{matrix}

$\mathsf{K}(\mathsf{SKK}x) \rhd_w \mathsf{K}(\mathsf{K}x(\mathsf{K}x)) \rhd_w \mathsf{K}x \tag{9}$

Teraz właściwym przeciw-przykładem dla (2) byłoby:

M. = K. x y

$M = \mathsf{K}xy$

N. = x

$N = x$

Ponieważ , zdecydowanie ma to . Jeśli jednak przetłumaczysz ostrożnie wersje abstrakcji, zobaczysz, że obie są odrębnymi formami normalnymi - i nie mogą być przekształcalne zgodnie z twierdzeniem Church-Rosser. $\mathsf{K}xy \rhd_w x$ $M =_w N$

Najpierw sprawdzamy : $M'$

\begin{aligned} M^{'} & = λ^{*} x . K x y \\ = S (λ^{*} x . K x) (λ^{*} x . y) \\ = S (λ^{*} x . K x) (K y) \\ = S (S (λ^{*} x . K) (λ^{*} x . x)) (K y) \\ = S (S (λ^{*} x . K) (I)) (K y) \\ = S (S (λ^{*} x . K) (S K K)) (K y) \\ = S (S (K K) (S K K)) (K y) \end{aligned}

$\begin{align} M' &= \lambda^* x.\mathsf{K}xy \\ &= \mathsf{S}(\lambda^* x.\mathsf{K}x)(\lambda^* x.y)\\ &= \mathsf{S}(\lambda^* x.\mathsf{K}x)(\mathsf{K}y) \\ &= \mathsf{S}(\mathsf{S}(\lambda^* x.\mathsf{K})(\lambda^* x.x))(\mathsf{K}y) \\ &= \mathsf{S}(\mathsf{S}(\lambda^* x.\mathsf{K})(\mathsf{I}))(\mathsf{K}y) \\ &= \mathsf{S}(\mathsf{S}(\lambda^* x.\mathsf{K})(\mathsf{SKK}))(\mathsf{K}y) \\ &= \mathsf{S}(\mathsf{S}(\mathsf{KK})(\mathsf{SKK}))(\mathsf{K}y) \end{align}$ Tutaj możesz sprawdzić, czy jest normalną formą. Tutaj możesz sprawdzić, czy , jak można się spodziewać, jeśli ma zachowywać się jak abstrakcja dla CL.

M^{'}

$M'$

(λ^{*} x . K x y) P ⊳_{w} P

$(\lambda^* x.Kxy)P \rhd_w P$

λ^{*}

$\lambda^*$

Teraz sprawdzamy : $N'$

\begin{aligned} {N.}^{'} & = λ^{*} x . x \\ = ja \\ = S. K. K. \end{aligned}

$\begin{align} N' &= \lambda^*x.x \\ &= \mathsf{I} \\ &= \mathsf{SKK} \end{align}$

Która jest oczywiście normalną formą inną niż , więc według twierdzenia Church-Rosser. Należy również zauważyć, że , to znaczy i «wytwarzają taką samą moc» dla dowolnych wejść . $M'$ $M' \not=_w N'$ $N'P \rhd_w P$ $M'$ $N'$ $P$

Udowodniliśmy teraz, że (2) nie zachowuje się w CL i że teoria CL zawierająca zrównuje zatem warunki, które nie są słabo równe. Ale dlaczego nas to obchodzi? $\xi$

Przede wszystkim sprawia, że kombinacyjna interpretacja niedoskonała: najwyraźniej nie wszystkie właściwości metateoretyczne zostają przeniesione. $\lambda$

Ponadto, a może co ważniejsze, chociaż istnieją ekstensywne teorie i CL, są one pierwotnie i powszechnie utrzymywane w intensywności. Intiętność jest przyjemną właściwością, ponieważ obliczenia modelu i CL jako procesu, i z tej perspektywy dwa różne programy (konkretnie terminy o innej normalnej formie), które zawsze dają takie same wyniki (przy równych danych wejściowych), nie mogą być zrównane. szanuje tę zasadę w , a jeśli chcemy, aby rozszerzana, moglibyśmy po prostu dodać np. . Ale wprowadzenie $\lambda$ $\lambda$ $\xi$ $\lambda$ $\lambda$ $\eta$ $\xi$ w CL nie czyni już tego całkowicie intensywnym (w rzeczywistości tylko częściowo). I to jest powód, dla „s«rozgłos», jak ujmuje to artykuł. $\xi$

— Roy O.
źródło

1

Nie mogę komentować jakości, ponieważ niewiele wiem na ten temat, ale wygląda to na trochę pracy. Doceniam, dziękuję!

— Raphael

Rzeczywiście post skończył się dłużej, niż się spodziewałem. Dzięki za komentarz. :)

— Roy O.

2

O to. Dzieje . Regularnie .

— Raphael

3

EDYCJA Ta odpowiedź jest niepoprawna, jak słusznie zauważył drugi odpowiadający. Użyłem tłumaczenia na logikę kombinacyjną z Asperti i Longo, która subtelnie różni się od tej w Selinger.

W rzeczywistości ilustruje to kluczowy punkt: „kombinacyjna interpretacja” rachunku lambda nie jest jedną rzeczą! Różni autorzy robią to nieco inaczej.

Zostawiam tutaj swoją odpowiedź dla potomnych, ale druga odpowiedź jest lepsza.

Równoważność w tym kontekście jest zdefiniowana w tabelach 1 i 2 w pracy Selingera. Jednak nieco inna aksjatyzacja może nieco wyjaśnić.

To tak naprawdę oznacza, że dwa pojęcia są konwertowalne w teorii . Możemy zdefiniować „wymienialność” za pomocą następujących dwóch aksjomatów: $\lambda$

$\beta$ . , jeśli wolny dla w $(\lambda x. M) N = [N/x]M$ $x$ $N$ $M$
$\eta$ . , jeśli nie jest wolny w $\lambda y. M y = M$ $y$ $M$

Plus, oczywiście, zwykłe aksjomaty i reguły wnioskowania potrzebne do przeprowadzenia kongruencją. Z tego powinno być oczywiste, że każdy kontrprzykład będzie polegał na warunku swobodnej zmiennej przy reguły . $=$ $\eta$

Myślę, że jest to prawdopodobnie najprostsze:

M. = x

$M = x$

N. = (λ z . z) x

$N = (\lambda z. z) x$

Możesz sam sprawdzić, czy , ale ich odpowiednie interpretacje kombinatoryczne nie są równe zgodnie z regułami w Tabeli 2. $\lambda y. M = \lambda y. N$

— Pseudonim
źródło

Czego nie rozumiem na temat twojej odpowiedzi: 1) dlaczego wspominasz , podczas gdy teoria w Tabeli 1 nie zawiera jej i jest wyraźnie intensywna? 2) Jak kombinacyjne interpretacje i nie jest równy? Pochodne w mojej odpowiedzi pokazują, że są. 3) Reguła nie jest adresowana, podczas gdy jest to winowajcą problemu.

η

$\eta$

λ y . M

$\lambda y.M$

λ y . N

$\lambda y. N$

ξ

$\xi$

— Roy O.