„Słynni logicy popełniali tutaj zawstydzające błędy”, wiersz z SICP. Do czego to się odnosi?

Oto kontekst ( Struktura i interpretacja programów komputerowych , sekcja 1.1.8, pod nagłówkiem „Nazwy lokalne”):

Formalny parametr procedury ma bardzo szczególną rolę w definicji procedury, ponieważ nie ma znaczenia, jaką nazwę ma parametr formalny. Taka nazwa nazywa się zmienną powiązaną i mówimy, że definicja procedury wiąże jej parametry formalne. Znaczenie definicji procedury pozostaje niezmienione, jeśli zmienna związana jest konsekwentnie zmieniana w całej definicji.

Na końcu tego ostatniego wiersza znajduje się przypis (26), który mówi:

Pojęcie konsekwentnej zmiany nazwy jest w rzeczywistości subtelne i trudne do formalnego zdefiniowania. Znani logicy popełniali tutaj zawstydzające błędy.

Do czego lub do kogo odnosi się ten tekst? Dlaczego zdefiniowanie „spójnej zmiany nazwy” byłoby trudne, którzy logicy popełniali błędy, próbując to zdefiniować, i jakie były te błędy?

logic

— ubadub
źródło

Mówię moim uczniom, że jedynym sposobem na zrozumienie „konsekwentnej zmiany nazw zmiennych” jest prawidłowe zaimplementowanie tego cholerstwa. Wiele książek logicznych unika tego problemu, podaje niekompletne procedury zmiany nazwy lub przynajmniej pomija dowody, że podane procedury zmiany nazwy są prawidłowe. Ale nie wiem, do jakich konkretnych plotek odnosi się książka.

— Andrej Bauer,

Precyzyjne radzenie sobie ze zmiennymi nazwami, świeżymi nazwami, podstawianiem unikania przechwytywania itp. Jest jedną z najbardziej trywialnych rzeczy, które szybko stają się naprawdę kłopotliwe w definicjach i dowodach. W przypadku tak trywialnego problemu nie chce się wydawać więcej niż trywialną ilość cykli mentalnych, ale o wiele więcej byłoby to potrzebne, aby uniknąć wielu trudnych ujęć / kolizji / itp. Często ludzie PL dbają o swoje definicje, ale następnie przywołaj „konwencję Barendregta” i zignoruj problem, nieco nadużywając „świeżego” tu i tam, gdy jest to potrzebne.

— chi

Byłbym wdzięczny za bardziej konkretne odpowiedzi, poniżej w polu odpowiedzi, jeśli to w ogóle możliwe. Te komentarze wciąż sprawiają, że problem brzmi tajemniczo, ponieważ napisałeś je do przeczytania przez kogoś, kto już zna dany problem, podczas gdy ja nie jestem

— ubadub

W szczególności @chi byłbym wdzięczny za przeczytanie zaleceń dotyczących tego tematu, jeśli takie masz. Z góry

— dziękuję

To jest częściowa odpowiedź: nie mam pojęcia, do jakich błędów lub osób odnosi się SICP. Mogę jedynie podać kilka wskazówek na temat tego, dlaczego zmiana nazwy zmiennej może być bolesna w precyzyjnej obsłudze.

Po pierwsze, wydaje się to banalne. Na przykład możemy zmienić nazwę powiązanych zmiennych w indeksowanych sumach

\sum_{x} e = \sum_{y} (e {y / x})

$\sum_x e = \sum_y (e\{y/x\})$

gdzie jest dowolnym wyrażeniem, a oznacza składniowe zastąpienie każdego przez . Trywialne, prawda? $e$ $e\{y/x\}$ $x$ $y$

Cóż, jeśli ślepo zastosujemy powyższą zasadę, otrzymamy

\sum_{x} (x + y) = \sum_{y} (y + y)

$\sum_x (x+y) = \sum_y (y+y)$

To nie jest dobrze. Musimy dodać wymaganie „ nie występuje we ”, inaczej otrzymamy konflikt nazw. $y$ $e$

Teraz rozważ tę poprawną nazwę

\sum_{x} \sum_{y} (x + y) = \sum_{x} \sum_{z} (x + z)

$\sum_x \sum_y (x+y) = \sum_x \sum_z (x+z)$

jeśli chcemy zmienić nazwę na , zgodnie z powyższą regułą możemy to zrobić po prawej stronie, ale nie po lewej stronie. Jest to niewygodne, ponieważ oba różnią się jedynie zmianą nazwy, dlatego należy postępować w ten sam sposób. $x$ $y$

Typowym podejściem tutaj jest uciekanie się do przedefiniowania jako „podstawienie unikające przechwytywania” i złagodzenie wymogu „ nie występuje we ” i zamiast tego należy użyć „ nie występuje za darmo we ”. $e\{y/x\}$ $y$ $e$ $y$ $e$

Następnie definiujemy wystąpienia bezpłatne:

f r e e (x) = {x} f r e e (e + t) = f r e e (e) \cup f r e e (t) f r e e (\sum_{x} e) = f r e e (e) ∖ {x}

$free(x)=\{x\} \qquad free(e+t) = free(e)\cup free(t) \qquad free(\sum_x e) = free(e)\setminus\{x\}$

Wreszcie, przechwyć unikając zamiany:

$x\{t/y\}$ to jeśli , a przeciwnym razie. $t$ $x=y$ $x$
$(e+e')\{t/y\} = e\{t/y\} + e'\{t/y\}$ (łatwy przypadek)
$(\sum_x e)\{t/y\} = ??$

Ostatni przypadek jest bolesny. Jeśli , podstawienie nie jest op, ponieważ chcemy, aby wpłynęło tylko na wolne zmienne, a jest powiązane. Zatem wynikiem jest po prostu . $x=y$ $x$ $\sum_x e$

Jeśli , chcielibyśmy powiedzieć, że . Zasadniczo jest to jednak błędne, ponieważ jeśli występuje za darmo , otrzymujemy przechwytywanie. $y\neq x$ $(\sum_x e)\{t/y\} = \sum_x (e\{t/y\})$ $x$ $t$

Westchnienie. Zatem pozwalamy, by była „pierwszą” zmienną, która wynosi 1) nie , 2) nie jest wolna w , i 3) nie jest wolna w . Tutaj „pierwszy” oznacza, że musimy uporządkować zestaw nazw zmiennych (np. Wybierając bijection między nazwami a naturali). Następnie w końcu pozwalamy . $z$ $y$ $t$ $\sum_x e$ $(\sum_x e)\{t/y\} = \sum_z (e\{z/x\}\{t/y\})$

Mam nadzieję, że dobrze to zrozumiałem. (Nawiasem mówiąc, moja pierwsza próba była błędna)

Niektórzy autorzy rozważają więcej przypadków, ale wynik jest taki sam „do zmiany nazwy”. Wybór „pierwszego” nie ma tak naprawdę znaczenia powyżej: każde takie działałoby dobrze i prowadziło do tego samego rezultatu (ponownie, aż do zmiany nazwy). $z$ $z$

Wreszcie mamy dźwiękową definicję zmiany nazwy ( -conversion) i unikania przechwytywania podstawienia wolnej zmiennej. Powyżej rozważałem sumy, ale odnoszą się one do wszystkich segregatorów (np. w rachunku lambda, definicje funkcji w wielu PL itp.). $\alpha$ $\lambda x$

Teraz wyobraź sobie, że musisz sobie radzić z tą skomplikowaną definicją za każdym razem, gdy chcemy udowodnić coś w teorii PL. Moglibyśmy, ale nie chcemy. Jest nudny, żmudny, podatny na błędy, zaśmieca dowód i nie zapewnia czytelnikowi wglądu. Z tego powodu wielu autorów PL po prostu pomija szczegóły, mówiąc (lub nawet przyjmując za pewnik!), Że terminy należy przyjmować „aż do zmiany nazwy”, że wszystkie powiązane zmienne są przyjmowane odrębnie od wszystkiego, od czego muszą się różnić, że zakładamy „konwencję Barendregta” lub coś w tym samym kierunku.

Szczerze mówiąc, jest to oszustwo w dowodach. Możemy również dodać „mrugnięcie, mrugnięcie, szturchnięcie, nie mów nic więcej!” w tym samym duchu. Zasadniczo prosimy o litość i mówimy czytelnikowi: „słuchaj, to jest nudne, nie chcę tego robić, nie chcesz go czytać - oboje wiemy, że przy ogromnym wysiłku możemy przepisać ten dowód na uwzględnij wszystkie szczegóły ”.

Technicznie rzecz biorąc, to jest możliwe, aby wykorzystać ten skrót, aby udowodnić fałszywe oświadczenie. Doświadczony recenzent dowodu wie jednak, co jest „moralnie w porządku” i może udoskonalić (z wielkim wysiłkiem), a co podejrzane. Ta ostatnia może zawierać coś, co zależy od faktycznego wyboru powiązanych nazw (więc tak naprawdę nie pracujemy zgodnie z obietnicą!). W takich przypadkach recenzent poprosi o więcej szczegółów, aby przekonać go.

— chi
źródło