Dlaczego ważne jest, aby funkcje były anonimowe w rachunku lambda?

Oglądałem wykład Jima Weiricha zatytułowany „ Przygody w programowaniu funkcjonalnym ”. W tym wykładzie wprowadza pojęcie kombinatorów Y, które zasadniczo znajduje punkt stały dla funkcji wyższego rzędu.

Jedną z motywów, jak wspomina, jest możliwość wyrażenia funkcji rekurencyjnych za pomocą rachunku lambda, tak aby teoria Kościoła (wszystko, co można skutecznie obliczyć, można było obliczyć za pomocą rachunku lambda) pozostaje.

Problem polega na tym, że funkcja nie może się tak po prostu wywołać, ponieważ rachunek lambda nie pozwala na nazwane funkcje, tj.

nie może nosić nazwy „ ”, należy ją zdefiniować anonimowo:$n$

Dlaczego dla rachunku lambda ważne jest, aby funkcje nie były nazwane? Jaką zasadę narusza się, jeśli istnieją funkcje nazwane? A może po prostu źle zrozumiałem wideo Jim?

Główne twierdzenie dotyczące tej kwestii wynika z brytyjskiego matematyka z końca XVI wieku, zwanego William Shakespeare . Jego najbardziej znany artykuł na ten temat zatytułowany „ Romeo i Julia ” został opublikowany w 1597 r., Choć prace badawcze przeprowadzono kilka lat wcześniej, zainspirowane takimi prekursorami, jak Arthur Brooke i William Painter.

Jego główny wynik, określony w akcie II. Scena II to słynne twierdzenie :

Co jest w imieniu? to, co nazywamy różą
Pod jakimkolwiek innym imieniem pachniałoby tak słodko;

Twierdzenie to można intuicyjnie rozumieć jako „nazwy nie przyczyniają się do znaczenia”.

Większa część pracy poświęcona jest przykładowi uzupełniającemu twierdzenie i pokazując, że chociaż nazwy nie wnoszą żadnego znaczenia, są źródłem niekończących się problemów.

Jak podkreślił Szekspira, nazwy mogą być zmieniane bez zmiany znaczenia, że operacja została nazwana później -conversion$\alpha$ przez Alonzo Church i jego zwolenników. W rezultacie ustalenie, co oznacza nazwa, niekoniecznie jest proste. Rodzi to szereg problemów, takich jak opracowanie koncepcji środowiska, w którym określono powiązanie nazwa-nazwa, oraz reguły określające, jakie jest obecne środowisko, gdy próbujesz określić znaczenie związane z nazwą. Zaskoczyło to przez pewien czas informatyków, co spowodowało problemy techniczne, takie jak niesławny problem Funarga. Środowiska pozostają problemem w niektórych popularnych językach programowania, ale generalnie uważa się je za niebezpieczne fizycznie bardziej szczegółowe, niemal tak samo zabójcze, jak przykład opracowany przez Szekspira w jego pracy.

Kwestia ta jest również zbliżona do problemów podniesionych w formalnej teorii języka , gdy alfabety i systemy formalne muszą być zdefiniowane aż do izomorfizmu , aby podkreślić, że symbole alfabetów są abstrakcyjnymi bytami , niezależnie od tego, jak „materializują się” jako elementy z jakiegoś zestawu.

Ten ważny wynik Szekspira pokazuje również, że nauka odbiegała wówczas od magii i religii, gdzie istota lub znaczenie może mieć prawdziwe imię .

Wniosek z tego wszystkiego jest taki, że w pracy teoretycznej często wygodniej jest nie obciążać się nazwiskami, chociaż może to wydawać się prostsze w praktycznej pracy i życiu codziennym. Pamiętaj jednak, że nie wszyscy nazywani mamami są twoimi matkami.

Uwaga :
zagadnienie to zostało ostatnio poruszone przez amerykańskiego logistę XX wieku Gertrude Stein . Jednak jej koledzy z matematyki wciąż zastanawiają się nad dokładnymi technicznymi implikacjami jej głównego twierdzenia :

Róża jest różą Róża jest różą.

opublikowany w 1913 r. w krótkim komunikacie zatytułowanym „Sacred Emily”.

$\lambda$$\lambda$$\pi$$\nu x.P$$\pi$

$\lambda$$\lambda$$\lambda$

$\mathsf{let} f = M \mathsf{in} N$$(\lambda f.N)M$$\lambda$

Uważam, że chodzi o to, że nazwy nie są konieczne. Wszystko, co wydaje się wymagać nazw, można zapisać jako funkcje anonimowe.

Możesz myśleć o rachunku lambda jak o języku asemblera. Ktoś z wykładu o asemblerze może powiedzieć: „W języku asemblera nie ma drzew zorientowanych obiektowo”. Możesz wtedy wymyślić sprytny sposób na wdrożenie drzew spadkowych, ale nie o to chodzi. Chodzi o to, że drzewa dziedziczenia nie są wymagane na najbardziej podstawowym poziomie programowania komputera fizycznego.

W rachunku lambda chodzi o to, że nazwy nie są wymagane do opisania algorytmu na najbardziej podstawowym poziomie.

Podobają mi się do tej pory 3 odpowiedzi - szczególnie analiza Shakespearena @ babou - ale nie rzucają one światła na to, co uważam za istotę pytania.

Rachunek λ wiąże nazwy funkcji za każdym razem, gdy zastosujesz funkcję do funkcji. Problemem nie jest brak nazwisk.

„Problem polega na tym, że funkcja nie może się wywołać po prostu” przez odwołanie się do jej nazwy.

(W czystym Lispie wiązanie nazwa -> funkcja nie jest objęte zakresem funkcji. Aby funkcja mogła się wywoływać po nazwie, funkcja musiałaby odnosić się do środowiska, które odwołuje się do funkcji. Czysta Lisp nie ma cykliczne struktury danych. Impure Lisp robi to poprzez mutowanie środowiska, do którego odnosi się funkcja.)

Jak zauważył @MartinBerger, historycznym powodem, dla którego rachunek λ nie pozwala na wywołanie funkcji przez nazwę, była próba wykluczenia paradoksu Curry'ego przy próbie użycia rachunku λ jako podstawy matematyki, w tym logiki dedukcyjnej. To nie działało, ponieważ techniki takie jak kombinator Y pozwalają na rekurencję nawet bez odniesienia do siebie.

Z Wikipedii:

Jeśli możemy zdefiniować funkcję, r = (λ.x x x ⇒ y)to r r = (r r ⇒ y).

Jeśli r rjest prawdą, to yjest prawdą. Jeśli r rjest fałszywe, to r r ⇒ yjest prawdziwe, co jest sprzecznością. Tak yjest i jak ykażde stwierdzenie, każde stwierdzenie może być prawdziwe.

r rjest obliczeniem nie kończącym się. Uważane za logikę r rjest wyrażeniem wartości, która nie istnieje.