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

19

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.

n(x,y)=x+y

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

(x,y)x+y

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?

Rohan Prabhu
źródło
4
To wcale nie wydaje się ważne. Możesz przypisać do zmiennej n, a następnie nadałeś nazwę funkcji. (x,t)x+yn
Yuval Filmus
@YuvalFilmus tak, możesz powiązać nazwę z funkcją. Myślę, że prawdziwym pytaniem, zdziwieniem, jest to, dlaczego (w rachunku lambda) nie można wywołać funkcji o takiej nazwie? Dlaczego potrzebujemy techniki takiej jak operator Y, aby wykonywać funkcje rekurencyjne? Mam nadzieję, że moja odpowiedź poniżej pomoże.
Jerry101
1
@ Jerry101 Historycznym powodem braku samodzielnego stosowania jest to, że rachunek miał być podstawą matematyki, a zdolność do samodzielnego stosowania sprawia, że ​​taka podstawa jest natychmiast niespójna. Zatem ta pozorna niezdolność (którą wiemy, że można teraz obejść) jest cechą projektową λ- rachunku. λλ
Martin Berger,
@MartinBerger proszę powiedzieć więcej. Niespójny z powodu mojej odpowiedzi? A może z innego powodu?
Jerry101
1
@ Jerry101 Niespójny w tym sensie, że możesz udowodnić 0 = 1 w takim fundamencie matematyki. Po Kleene i Rosser wykazał niespójność czystego, bez typu -calculus, Prosto wpisany λ -calculus został opracowany jako alternatywa, która nie pozwala nam określić combintors fix-punktowych, takich jak Y . Ale jeśli dodasz rekurencję do prostego λ- kalkulatora, znowu stanie się ona niespójna, ponieważ każdy typ jest zamieszkiwany przez program nie kończący się. λλYλ
Martin Berger,

Odpowiedzi:

24

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α 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”.

Babou
źródło
3
Uwaga dodatkowa: w ostatnich dziesięcioleciach „róża” (w informatyce) została w większości zastąpiona przez „foobar” (i jego części) jako kanoniczny przykład nazwy, która jest równie dobra jak każda inna. Ta preferencja została najwyraźniej wprowadzona przez amerykańskich inżynierów kolejowych.
FrankW
To powiedziawszy, kanoniczne nazwy często używanych pojęć są ważne dla sprawnej komunikacji.
Raphael
1
@Raphael zgodził się, ale umieściłbym to w kategorii życia codziennego. I skąd znamy granice tego, co naprawdę jest kanoniczne? Mimo to często odczuwam zaniepokojenie, gdy widzę, że studenci przyjmują całą terminologię, zapis i definicje (a nawet sposób, w jaki twierdzą niektóre twierdzenia) za niezmienną prawdę podaną przez Boga. Nawet tutaj, na SE, uczniowie zadają pytania, nie zdając sobie sprawy, że możemy nie znać ich notacji lub definicji, których używają na zajęciach. Magia prawdziwych imion nie umiera łatwo.
babou
10

λλπνx.Pπ

λλλ

letf=MinN(λf.N)Mλ

Martin Berger
źródło
1
Myślę, że OP chciał mieć możliwość nazywania funkcji, a nie zabraniać anonimowych. To powiedziawszy, sądzę, że wszelkie wymagania rachunku λ dotyczące potrzeby anonimowych funkcji będą również widoczne w językach takich jak Lisp / Scheme lub ML. W przypadku Lisp / Schemat meta-okólność ewaluatorów powinna umożliwiać tworzenie nowych nazw w razie potrzeby, chociaż nie jestem pewien, czy chciałbym tego w formalny sposób. Korzystanie z nieograniczonej liczby funkcji niekoniecznie stanowi problem, gdy rekurencja umożliwia lokalne ponowne wykorzystanie już używanych nazw.
babou
λλ
Czy ostatni wiersz powinien brzmieć (lambda f. N) M?
Joe the Person,
@JoethePerson Tak, dobrze zauważony. Naprawiony. Dzięki.
Martin Berger,
4

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.

Prawdziwy John Connor
źródło
4

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.

Jerry101
źródło
λ.x xxxxx
@RohanPrabhu λ.x x xtłumaczy na Lisp as (lambda (x) (x x))i JavaScript as function (x) {return x(x);}. x⇒yoznacza x implies ymniej więcej tyle samo, co (NOT x) OR y. Zobacz en.wikipedia.org/wiki/Lambda_calculus
Jerry101
Dziękujemy za odpowiedź na to żenujące pytanie debiutanta!
Rohan Prabhu