Teoria wykonalności: różnica mocy między rachunkiem lambda a maszynami Turinga

Mam trzy powiązane pytania, które są zaznaczone punktorami poniżej (nie, nie można ich podzielić, jeśli się zastanawiasz). Andrej Bauer napisał tutaj , że niektóre funkcje można realizować za pomocą maszyny Turinga, ale nie za pomocą rachunku lambda. Kluczowym krokiem jego rozumowania jest:

Jeśli jednak użyjemy rachunku lambda, wówczas [program] c ma obliczyć liczbę reprezentującą maszynę Turinga na podstawie terminu lambda reprezentującego funkcję f. Tego nie da się zrobić (wyjaśnię dlaczego, jeśli zadacie to jako osobne pytanie).

• Chciałbym zobaczyć wyjaśnienie / nieformalny dowód.

Nie widzę tu zastosowania twierdzenia Rice'a; miałoby to zastosowanie do problemu „czy ta maszyna Turinga i ten równoważnik L lambda?”, ponieważ zastosowanie tego predykatu do równoważnych terminów daje ten sam rezultat. Wymagana funkcja może jednak obliczać różne, ale równoważne, bazy TM dla różnych, ale równoważnych terminów lambda.

• Co więcej, jeśli problem dotyczy introspekcji terminu lambda, myślę, że przekazanie kodowania Gödela terminu lambda byłoby również dopuszczalne, prawda?

Z jednej strony, biorąc pod uwagę, że jego przykład dotyczy obliczania, w rachunku lambda, liczby kroków wymaganych przez maszynę Turinga do wykonania danego zadania, nie jestem bardzo zaskoczony.

• Ale ponieważ tutaj rachunek lambda nie może rozwiązać problemu związanego z maszyną Turinga, zastanawiam się, czy można zdefiniować podobny problem dla rachunku lambda i udowodnić, że jest on nierozwiązywalny dla maszyn Turinga, czy faktycznie istnieje różnica w mocy na korzyść Maszyny Turinga (co by mnie zaskoczyło).

John Longley ma bardzo obszerny artykuł ankietowy omawiający związane z tym kwestie, „Pojęcia obliczalności w wyższym typie” .

Podstawową ideą jest to, że teza Churcha-Turinga dotyczy tylko funkcji z - i jest więcej do obliczeń! W szczególności, kiedy piszemy programy, korzystamy z funkcji wyższego typu (takich jak ( N → N ) → N ).$\mathbb{N} \to \mathbb{N}$$(\mathbb{N} \to \mathbb{N}) \to \mathbb{N}$

Aby w pełni zdefiniować model obliczeń wyższego typu, musimy określić konwencję wywoływania funkcji, aby jedna funkcja mogła wywoływać inną funkcję otrzymaną jako argument. W rachunku lambda standardowa konwencja wywoływania polega na tym, że reprezentujemy funkcje według terminów lambda, a jedyne, co można zrobić z lambda w rachunku lambda, to zastosować go. W typowych kodowaniach z maszynami Turinga przekazujemy funkcje jako argumenty, ustalając konkretne kodowanie Godela, a następnie łańcuchy reprezentujące indeks maszyny, którą chcesz przekazać jako argument.

Różnica w kodowaniu oznacza, że ​​możesz analizować składnię argumentu za pomocą kodowania w stylu TM, a nie możesz ze standardową reprezentacją rachunku lambda. Jeśli więc otrzymujesz termin lambda dla funkcji typu , możesz przetestować jego zachowanie, przekazując mu określone n - nie możesz w żaden sposób analizować struktury tego terminu. To po prostu za mało informacji, aby zrozumieć kod terminu lambda.$\mathbb{N} \to \mathbb{N}$$n$

Warto zauważyć, że przy wyższych typach, jeśli język jest mniej ekspresyjny przy jednym rzędzie, jest bardziej ekspresyjny o jeden rząd w górę, ponieważ funkcje są sprzeczne. Podobnie są funkcje, które można pisać w LC, których nie można kodować w stylu TM (ponieważ polegają one na tym, że można przekazywać argumenty funkcjonalne i wiedzieć, że odbiornik nie może zajrzeć do funkcji, którą dajesz) .

EDYCJA: Oto przykład funkcji definiowanej w PCF, ale nie w kodowaniu TM + Goedel. Zadeklaruję isAlwaysTruefunkcję

 isAlwaysTrue : ((unit → bool) → bool) → bool

który powinien zwracać wartość true, jeśli jego argument ignoruje argument i zawsze zwraca wartość true, powinien zwracać wartość false, jeśli argument zwraca wartość false na dowolnym wejściu, i przechodzi do pętli, jeśli jego argument przechodzi do pętli na dowolnym wejściu. Możemy dość łatwo zdefiniować tę funkcję w następujący sposób:

isAlwaysTrue p = p (λ(). true) ∧ p (λ(). false) ∧ p (λ(). ⊥)

gdzie ⊥jest obliczeniem zapętlenia i ∧jest operatorem i na booleanach. Działa to, ponieważ unit → boolw PCF są tylko trzej mieszkańcy , dlatego możemy je wyczerpująco wyliczyć. Jednak w modelu stylu + kodowania Goedela TM pmoże sprawdzać, ile czasu zajmuje jego argument, aby zwrócić odpowiedź, i na tej podstawie zwracać różne odpowiedzi. W związku z tym wdrożenie za isAlwaysTruepomocą baz TM nie spełniłoby specyfikacji.

Co powiedziała Neel, a także następujące.

$\mathbb{N} \to \mathbb{N}$$\lambda$$\lambda$$\lambda$

$\lambda$$\mathbb{N} \to \mathbb{N}$

$\lambda$$\mathbb{N} \to \mathbb{N}$$\lambda$

$\mathbb{N} \to \mathbb{N}$$\lambda$$\mathtt{app}$$\overline{n}$$f : \mathbb{N} \to \mathbb{N}$$f(k)$$\mathtt{app} \; \overline{n} \; \overline{k}$$\overline{n}$$n$$\mathtt{app}$$\lambda$

$X$$f : X \times \mathbb{N} \to \mathbb{N}$$\lambda$$t$$\tilde{f} : X \to (\mathbb{N} \to \mathbb{N})$$\lambda$$s$$X$$\mathbb{N} \to \mathbb{N}$$\lambda$$f$$\tilde{f}$$\mathbb{N} \to \mathbb{N}$$\lambda$$\lambda$$\mathbb{N} \to \mathbb{N}$$\lambda$

$X$$\mathbb{N} \to \mathbb{N}$$\lambda$$X$$X$