Z artykułu na temat strategii oceny w Wikipedii:
Pojęcie strategii redukcji w rachunku lambda jest podobne, ale wyraźne.
Z artykułu na temat strategii redukcji na Wikipedii:
Jest podobny, ale nieznacznie różni się od pojęcia strategii oceny w informatyce.
Jakie jest subtelne rozróżnienie między strategiami oceny a strategiami redukcji, na które wskazują te dwa artykuły? Czy to tylko dwie podobne koncepcje z różnych domen?
Odpowiedzi:
Strategia redukcji jest funkcją Lambdy, która wybiera jeden redeks (wyrażenie redukowalne) ze wszystkich możliwych redexów - w zależności od tego, co zdefiniujesz jako redex.
Nieformalnie strategia oceny to kolejność, w jakiej język ocenia swoje argumenty. Strategia przekazywania parametrów jest tym, co język przekazuje funkcji.
Aby zrozumieć związek między nimi, przestudiuj artykuł Plotkina o nazwie Call-by-name, call-by-value i rachunku lambda. Wyraźnie wyjaśnia, że chcesz wybrać odrębne AXIOMY w zależności od tego, jakiej kolejności oceny chcesz. Dla nazwy Cb chcesz stary aksjomat beta, a dla wartości cb chcesz aksjomat wartości beta. Jeśli to zrobisz, wszystkie meta-twierdzenia działają tak samo dla obu smaków. Później pokazałem (wraz z wieloma współpracownikami), że ten pomysł uogólnia wszystko, co studiował świat PL.
To wszystko techniczne, a nie jakiś wiersz, który można interpretować. Po prostu poczytaj o tym.
- Matthias Felleisen
ps Powiem, że myślę, że ludziom łatwiej będzie zrozumieć artykuł Plotkina z Części I w naszej książce Redex. Ale tak, to 3 razy dłużej.
źródło
Artykuł w Wikipedii „Strategia redukcji” jest całkowicie wyodrębniony z konkretnej edycji dokonanej przez anonimowy adres IP w artykule „Strategia oceny”.
Pogląd, który reprezentuje, nie jest zgodny, w tym sensie, że podejrzewam, że stosunkowo niewiele osób w tej dziedzinie spontanicznie udzieli tej odpowiedzi, jeśli zapytasz ich „czy rozróżniłbyś nazwy„ strategia redukcji ”i„ strategia oceny ”?”. Słyszałem to tylko od Matthiasa Felleisena, który jest nieugięty w kwestii znaczenia tego rozróżnienia - i zakładam, że ten punkt widzenia podzielają inni, którzy mieli okazję poświęcić czas na szczegółowe omówienie z nim tych kwestii.
Moje obecne rozumienie tego punktu (ale nie zbadałem jeszcze szczegółów technicznych w pełni) dotyczy następujących kwestii: chodzi o to, czy używasz semantyki „duży krok” w porównaniu z „małym krokiem” - to rozróżnienie jest standardowe i zrozumiałe przez wszystkich w terenie. Semantyka małych kroków definiuje jeden atomowy stopień redukcji, a wynik jest ogólnie nadal redukowalny. Semantyka w dużym kroku definiuje jeden „duży” krok redukcji, który przechodzi od programu startowego do jego wartości (lub bogatszego typu „odpowiedź”, jeśli twój język ma inne obserwowalne efekty niż zwracanie wartości, np. Wejście / wyjście lub stan zmienny).
Jeśli zdefiniujesz relację zarówno dużego, jak i małego kroku, możesz sprawdzić, czy semantyka dużego kroku jest zawarta w przechodzącym zamknięciu relacji małego kroku i czy relacja małego kroku nie ogranicza się do innych zablokowanych terminów niż te osiągnięte przez relację dużego kroku lub rozbieżne, jeśli zdefiniowano redukcję dużego kroku. Jest to oczekiwana relacja spójności między nimi.
Myślę, że sformułowanie artykułu można mniej więcej opisać współczesnymi terminami, ponieważ „strategia oceny jest relacją dużego kroku”, „strategia redukcji jest relacją małego kroku”. Zwróć uwagę, że dyskusja przeprowadzona w artykule „Strategia redukcji” dotyczy głównie artykułów i badań (oraz, co ważniejsze, elokwentnych poglądów powstałych podczas ich czytania i pisania) w latach 1973–1991, w czasie, gdy te pojęcia dopiero się rodziły, oraz prawdopodobnie nie tak dobrze rozumiane jak dzisiaj. (semantyka dużego kroku została podkreślona przez Kahna w 1987 r., a jednym z najważniejszych dzieł dotyczących semantyki małych kroków jest Wright i Felleisen, 1992)
Jeśli chodzi o bardziej upartą stronę tego, dlaczego Felleisen nalega na znaczenie tej różnicy (to znaczy, dlaczego może być w tym coś więcej niż tylko „mały krok kontra duży krok, meh”), moje obecne rozumienie jest następujące: chodzi o to, że semantykę małych kroków należy postrzegać jako szczegół implementacji. Thesemantyka, zgodnie z tym argumentem, jest funkcją abstrakcyjną, która odwzorowuje każdy program na jego wartość / odpowiedź, a pozostałe są urządzeniami implementacyjnymi zaprojektowanymi w celu przybliżenia go (lub uzasadnienia równoważności wywołanej przez tę semantykę). Kiedy mówimy dziś „duży krok”, mamy na myśli system wnioskowania o charakterze składniowym, ale „strategia redukcji”, o której mowa powyżej, jest w rzeczywistości jej abstrakcją jako mapowaniem. (Nie sądzę, by to w praktyce dodawało wyrazu lub siły temu pojęciu, ale czyni je bardziej abstrakcyjnym).
Myślę więc, że to, co mówią ta strona Wikipedii i Matthias Felleisen, to coś w stylu: „Zdefiniuj swoją ocenę w dowolny sposób, ale pod koniec dnia ważne jest, w jaki sposób twoje programy są mapowane na ich wartości / odpowiedzi / zachowania, i to właśnie należy nazwać „semantyką operacyjną” i uzasadniać. ”.
Zauważ, że to stanowisko jest nieco sprzeczne z obecnym rozróżnieniem (które moim zdaniem jest raczej zgodne, ale może być z mojej strony stronniczością kulturową) między „semantyką operacyjną” a „semantyką denotacyjną”, gdzie ta pierwsza jest postrzegana jako bardziej syntaktyczna z natury (zdefiniowany jako relacja redukcji), a ten drugi typowo charakteryzuje się tym, że równoważne obliczeniowo programy mają dokładnie to samo oznaczenie (więc oznaczenie jest nieświadome faktycznego mechanizmu obliczeniowego). Zgodnie z tym ostatnim poglądem to, co zaproponowano w artykułach jako „strategię oceny” lub „semantykę operacyjną”, a moje wyjaśnienie powyżej byłoby raczej postrzegane jako semantyka denotacyjna - ale, co prawda, ma bardziej konkretny charakter niż większość: wartości / odpowiedzi / zachowania są bliższe obiektom składniowym niż wielu domenom semantycznym.
Odniesienia: aby zrozumieć ten punkt widzenia, prawdopodobnie warto wrócić do jego proklamowanego źródła, którym jest artykuł Gordona Plotkina z 1973 roku. Możesz również mieć szczęście, wypróbowując jeden z ostatnich artykułów cytowanych na wikipedii; Odkryłem na przykład, że „Parameter-passing and the Lambda Calculus”, autorstwa Cranka i Felleisena, 1991, podali bardzo jasny przegląd ich stanowiska w tej sprawie na kilku pierwszych stronach.
źródło