Czym jest rachunek λ?

Mam coś, co nazwałbym filozoficznym pytaniem o rachunek λ.

Podczas eksploracji rachunku λ będziesz zaskoczony, widząc wszystkie rzeczy, które możesz tam zrobić. Możesz zdefiniować liczby całkowite, operacje arytmetyczne, booleany, instrukcje if-then-else, pętle, funkcje rekurencyjne itp. Uważam, że zostało ono obliczone jako kompletne.

Ale z drugiej strony, jeśli weźmiesz pod uwagę, co możesz zrobić z funkcjami w rachunku λ, zdajesz sobie sprawę, że jedyne, co możesz zrobić, to nakarmić ją funkcją i zwraca ona inną funkcję. I ten proces nigdy się nie kończy.

Jak więc wyodrębnić wynik z obliczeń?

Załóżmy, że wynikiem wyrażenia jest funkcja f. Chcesz sprawdzić, czy ftego się spodziewałeś. Możesz to przetestować, skorzystać z funkcji, którą znasz, zastosować się fdo niej i otrzymać g. Ale aby gto sprawdzić , musisz teraz sprawdzić, co grobi. I zaczynasz wszystko od nowa. Więc jak możesz coś powiedzieć f?

Wydaje mi się, że można zastąpić wszystkie funkcje w rachunku λ pojedynczą funkcją, funkcją tożsamości I = λx.xi wszystko nadal działa tak, jak opisano w rachunku λ. Liczebnik Kościoła, 3gdy jest dany fi xwraca f(f(f(x))). Ale ponieważ fi xmoże być tylko I, powraca I. Istosowane Ii Irównież zwraca I. ISpełnia więc definicję 3. W „wartości logiczne” (λxy.x)i (λxy.y)potrzebuje 2 argumenty, które będą Ii Itak obie wartości logiczne powróci I. Każda z nich jest równoważna z tożsamością, mimo że zachowują się dokładnie zgodnie z ich definicjami.

Jak więc różnicę? Jak wykazujesz, że rachunek λ dotyczy więcej niż jednej funkcji?

Czy istnieje koncepcja tożsamości? Czy potrafisz natychmiast zidentyfikować funkcję bez jej oceny? Wierzę, że udowodniono, że nie ma możliwości przetestowania 2 funkcji pod kątem równości.

A może rachunek λ nie dotyczy funkcji, ale formalnego opisu ich działania? Oznaczałoby to, że wyrażenia λ nie tylko definiują działanie funkcji, ale także dane, którymi manipulują te funkcje. Więc kiedy piszesz A B, nie stosuje Asię B, ale trzeba zastosować funkcja opisana przez struny Ado formalnej definicji funkcji zawartych w Bpowrocie inną formalną definicję.

Co tak naprawdę dzieje się w rachunku λ? Z jakimi przedmiotami matematycznymi ma do czynienia?

Kontynuacja:

OK, z poniższej odpowiedzi wynika, że ​​rachunek λ nie tyle dotyczy funkcji w sensie matematycznym, ale podzbioru funkcji, które można wyrazić jako wyrażenia λ. Lub nawet więcej o manipulowaniu wyrażeniami λ.

Rzeczywiście niemożliwe jest określenie semantycznej równoważności warunków rachunku lambda. Jest to jedno zastosowanie twierdzenia Rice'a. Łatwo jest jednak porównywać składniowo terminy , to znaczy sprawdzać, czy mają dokładnie taką samą strukturę (równoważnie, jeśli ich „ciąg znaków” jest taki sam). To naprawdę wszystko, czego potrzebujesz, aby uzyskać wyniki.

Na przykład, aby obliczyć funkcje n = f(i)od naturali do naturali, podajesz kodowanie kościoła ijako parametr do funkcji rachunku lambda, stosujesz reguły redukcji aż do zatrzymania i sprawdzasz wynikowy termin. Jeśli pasuje do struktury cyfr kościoła, wyodrębnij liczbę, nktórą koduje. To twój wynik. Jeśli wynikowy termin nie wygląda jak cyfra kościelna lub redukcja się nie zatrzymuje, funkcja jest niezdefiniowana i.

Terminy skutecznie ściągają podwójną stawkę jako „kod” i „dane”. To nic specjalnego: taśma maszyny Turinga (ciąg znaków nad jakimś alfabetem) może być --- i często jest --- interpretowana jako kodowanie maszyny Turinga lub jakiegoś jej aspektu. Podobnie, bity w głównej pamięci maszyny von Neumanna mogą być kodowaniem programu lub kodowaniem czegoś innego. Lub nawet oba naraz. Różni się tylko „domyślna perspektywa”.