Czy Lambda Calculus jest czysto składniowy?

Czytałem od kilku tygodni o rachunku Lambda, ale jeszcze nie widziałem niczego, co różni się materialnie od istniejących funkcji matematycznych i chcę wiedzieć, czy to tylko kwestia notacji, czy też są jakieś nowe właściwości lub reguły utworzone przez aksjomaty rachunku lambda, które nie mają zastosowania do każdej funkcji matematycznej. Na przykład przeczytałem, że:

„Mogą istnieć funkcje anonimowe” : funkcje Lambda nie są anonimowe, wszystkie nazywane są po prostu lambda. W notacji matematycznej dopuszczalne jest używanie tej samej zmiennej dla różnych funkcji, jeśli nazwa nie jest ważna. Na przykład dwie funkcje w połączeniu Galois są często nazywane *.

„Funkcje mogą przyjmować funkcje jako dane wejściowe” : Nie jest nowością, można to zrobić za pomocą zwykłych funkcji.

„Funkcje to czarne skrzynki” : Tylko dane wejściowe i wyjściowe są również poprawnymi opisami funkcji matematycznych ...

To może wydawać się dyskusją lub opiniotwórczym pytaniem, ale uważam, że powinna istnieć „poprawna” odpowiedź na to pytanie. Chcę wiedzieć, czy rachunek lambda jest tylko konwencją notacyjną, czy syntaktyczną do pracy z funkcjami matematycznymi, czy też istnieją jakieś istotne lub semantyczne różnice między lambdami a funkcjami zwykłymi.

Jak na ironię, tytuł ma rację, ale nie w sposób, w jaki wydaje się, że miałeś na myśli, że „rachunek lambda jest tylko konwencją notacyjną”, co nie jest dokładne.

Terminy lambda nie są funkcjami ¹ . Są to fragmenty składni, tj. Zbiory symboli na stronie. Mamy zasady manipulowania tymi zbiorami symboli, przede wszystkim redukcją beta. Możesz mieć wiele różnych terminów lambda, które odpowiadają tej samej funkcji. ²⁾

Zajmę się twoimi punktami bezpośrednio.

Po pierwsze, lambda nie jest nazwą, która jest ponownie używana. Byłoby to nie tylko bardzo mylące, ale nie piszemy (lub ), co byśmy zrobili, gdyby była nazwą funkcji, tak jak piszemy . W moglibyśmy zastąpić (gdyby był zdefiniowany terminem lambda) terminem lambda dającym coś w rodzaju znaczenie jest wyrażeniem, które może reprezentować funkcję, a nie deklaracja deklarująca funkcję (o nazwie$\lambda(x)$$(\lambda\ x)$$\lambda$$f(x)$$f(x)$$f$$(\lambda y.y)(x)$$(\lambda y.y)$$\lambda$albo coś innego). W każdym razie, kiedy przeciążamy terminologię / notację, jest to (można mieć nadzieję) zrobione w sposób, w którym można je jednoznacznie określić kontekstowo, z pewnością nie może tak być w przypadku terminów lambda.

Twój następny punkt jest w porządku, ale trochę nieistotny. To nie są zawody, w których obowiązują Warunki Team Lambda i Funkcje Drużynowe i tylko jeden może wygrać. Głównym zastosowaniem terminów lambda jest studiowanie i rozumienie określonych rodzajów funkcji. Wielomian nie jest funkcją, chociaż często niedbale je identyfikujemy. Badanie wielomianów nie oznacza, że ​​uważa się, że wszystkie funkcje powinny być wielomianami, ani też nie jest tak, że wielomiany muszą „robić” coś „nowego”, aby być wartym przestudiowania.

Ustawione funkcje teoretyczne nie są czarnymi skrzynkami, chociaż są one całkowicie zdefiniowane przez ich relację wejścia-wyjścia. (Dosłownie są ich stosunek wejścia-wyjścia). Wyrażenia lambda nie są również czarne skrzynki i są nie zdefiniowane przez ich relacji nadawczo-odbiorczego. Jak już wspomniałem wcześniej, możesz mieć różne wyrażenia lambda, które wytwarzają tę samą relację przepływów międzygałęziowych. Podkreśla to również fakt, że terminy lambda nie mogą być funkcjami, ale mogą indukować funkcje. ²⁾

W rzeczywistości analogia między wielomianami a terminami lambda jest bardzo bliska i podejrzewam, że możesz nie docenić różnicy między wielomianem a funkcją, którą reprezentuje, więc rozwinę trochę. ³ Zazwyczaj po wprowadzeniu wielomianów, zwykle o rzeczywistych współczynnikach, są one traktowane jako rzeczywiste funkcje określonego typu. Rozważmy teraz teorię rejestrów przesuwnych z liniowym sprzężeniem zwrotnym (LFSR). Jest to w dużej mierze teoria wielomianów ) w stosunku do , ale jeśli uważamy to za funkcję od , to są najwyżej takie funkcje. Istnieje jednak nieskończona liczba wielomianów w . ⁴$\mathbb F_2$F 2 → F 2 4 F 2 F 2 → F 2 F 2 2 N → 2 N. $\mathbb F_2\to\mathbb F_2$$4$$\mathbb F_2$Jednym ze sposobów na to jest to, że możemy interpretować te wielomiany jako coś innego niż , w rzeczywistości każda zrobi to. W przypadku LFSR zwykle interpretujemy wielomiany jako operacje na strumieniach bitów, które, jeśli chcemy, mogą być reprezentowane jako funkcje , chociaż zdecydowana większość takich funkcji nie byłaby obrazem interpretacji LFSR.$\mathbb F_2\to\mathbb F_2$$\mathbb F_2$$\mathbf{2}^{\mathbb N}\to\mathbf{2}^{\mathbb N}$

Dotyczy to również terminów lambda, możemy interpretować oba z nich jako rzeczy inne niż funkcje. Są to zarówno znacznie łatwiejsze w obsłudze obiekty do pracy niż typowo nieskończenie nieskończone zestawy funkcji. Oba są znacznie bardziej obliczeniowe niż funkcje arbitralne. Potrafię napisać program do manipulowania wielomianami (o współczynnikach, które co najmniej są obliczalne) i wyrażeniami lambda. Rzeczywiście, niepoprawione terminy lambda są jednym z oryginalnych modeli funkcji obliczalnych. Ta bardziej symboliczna / syntaktyczna, obliczeniowa / obliczeniowa perspektywa jest zwykle bardziej podkreślana, szczególnie w przypadku niepisanego rachunku lambda, niż bardziej semantyczne interpretacje rachunku lambda. WpisanyTerminy lambda są znacznie łatwiejsze w zarządzaniu i zwykle (choć nie zawsze) można je łatwo interpretować jako ustawione funkcje teoretyczne, ale zwykle można je interpretować jako jeszcze szerszą klasę rzeczy oprócz funkcji niż niepoprawny rachunek lambda. Mają też bogatą własną teorię syntaktyczną i bardzo głębokie powiązanie z logiką .

¹ Możliwe, że problem może pójść w drugą stronę. Być może masz nieporozumienie na temat funkcji.

² W rzeczywistości nie jest to takie proste. W przypadku niepisanego rachunku lambda tak naprawdę nie ma sensu naiwnie interpretować arbitralnych terminów lambda jako funkcji teoretycznych . Możesz zacząć to dostrzegać, próbując wyrazić, jaka powinna być dziedzina interpretacji. Jeśli interpretuję termin lambda jako element zestawu , chcę również móc interpretować go jako funkcję na i na ponieważ chcę interpretować aplikację jako aplikację funkcji. Skończysz na (lub jego osłabienie), co jest prawdziwe tylko dla zestawu singletonów. Tym, czego potrzebujemy do nietypowego rachunku lambda, jest obiekt refleksyjny$D$$D$$D$$D^D\subseteq D$, a dla kategorii zestawów nie ma nietrywialnych obiektów refleksyjnych. Historia jest nieco inna w przypadku typowanych wyrażeń lambda, ale wciąż może być nietrywialna.

³ Jeśli jasno rozumiesz to rozróżnienie, wówczas analogia powinna być bardzo pouczająca.

⁴ Ten problem nie występuje w przypadku pól o charakterystyce 0, takich jak liczby zespolone, liczby rzeczywiste, liczby wymierne lub liczby całkowite, więc rozróżnienie nie jest tak wyraźne, choć nadal istnieje.

Pomyśl o koncepcji zmiennych. W starych językach, takich jak podstawowy, nie miałeś alokacji dynamicznej i potrzebujesz jednej nazwy dla każdej zmiennej. (Nie jest to do końca dokładne, ponieważ masz tablice, ale chodzi o to, że ...) w wielu problemach musisz być w stanie przydzielić tyle zmiennych, ile chcesz, bez ograniczenia liczby nazw definiowanych przez twój program.

Funkcje Lambda pozwalają pozbyć się tego samego ograniczenia dotyczącego nazw funkcji, umożliwiając Twojemu programowi zdefiniowanie tylu funkcji, ile potrzebuje i „przechowywanie” ich w tych samych złożonych strukturach danych, co innych zmiennych. Nie jest to coś, co można zrobić z konwencjonalnymi nazwanymi funkcjami.