Związek między maszyną Turinga a rachunkiem lambda?

49

Czy istnieje związek między Maszyną Turinga a rachunkiem lambda - czy zdarzyło się, że powstały mniej więcej w tym samym czasie?

computability lambda-calculus turing-machines

— Sokole Oko
źródło

7

Czy potrafisz rozwinąć swoje pytanie? Oba modele mają tę samą moc obliczeniową (oba są w stanie wyrazić rodzinę funkcji rekurencyjnych), to znaczy, że Turing jest kompletny. Zobacz: en.wikipedia.org/wiki/Turing_completeness

— Joel Rybicki

powiązane: Teoria wykonalności: różnica mocy między rachunkiem Lambda a maszynami Turinga

— Kaveh

To miłe pytanie!

— Tayfun Zapłać

31

Rachunek lambda jest starszy niż model maszyny Turinga, najwyraźniej pochodzący z okresu 1928–1929 (Seldin 2006), i został wymyślony, aby zawrzeć pojęcie funkcji schematycznej, której Kościół potrzebował dla fundamentalnej logiki, którą opracował. Nie został wymyślony, aby uchwycić ogólne pojęcie funkcji obliczeniowej, a w rzeczywistości wersja o słabszym typie lepiej spełniłaby jego cele.

Wydaje się, że jest to cel uboczny w tym, że rachunek, który wynalazł Kościół, okazał się być kompletnym Turinga, chociaż później Kościół wykorzystał rachunek lambda jako podstawę do tego, co nazwał funkcjami obliczalnymi (1936), do których odwoływał się Turing w swoim artykule .

Prosta teoria typów Kościoła (1940) przedstawia bardziej umiarkowaną, typowaną teorię funkcji, która wystarcza do wyrażenia składni logiki wyższego rzędu, ale nie wyraża wszystkich funkcji rekurencyjnych. Teorię tę można postrzegać jako bardziej zgodną z pierwotną motywacją Kościoła.

Bibliografia

Church (1936). Nierozwiązywalny problem w elementarnej teorii liczb. American Journal of Mathematics 58: 345–363.
Kościół (1940). Sformułowanie prostej teorii typów . Journal of Symbolic Logic 5 (2): 56–68.
Seldin (2006). Logika Curry i Kościoła . W Handbook of the History of Logic, vol.5: Logic from Russell to Church , str. 819–874. Holandia Północna: Amsterdam.

Uwaga Ta odpowiedź została znacznie zmieniona z powodu zastrzeżeń Kaveha i Sasho. Polecam oś czasu Wikipedii, którą zasugerował Kaveh, Historię Kościoła - tezę Turinga , która zawiera niektóre cytaty z najważniejszych artykułów.

— Charles Stewart
źródło

2

Church twierdził, że rachunek lambda przechwytuje intuicyjny zapis funkcji obliczeniowej przed tekstem Turinga, dlatego nazywa się to tezą Kościoła. Idea uchwycenia ogólnego pojęcia funkcji obliczeniowych sięga wstecz (np. Ogólne funkcje rekurencyjne Godela), a Church próbował je uchwycić.

— Kaveh

5

Myślę, że mylące jest twierdzenie, że równoważność modeli jest całkowitym wypadkiem. Wydaje mi się, że Church i Turing postanowili uchwycić powiązane pojęcia, nawet jeśli nie było od razu oczywiste, że te pojęcia są ze sobą powiązane. Czy powiedziałbyś, że to „całkowity wypadek”, że integracja Riemanna i przeciwdziałanie różnicowaniu są ze sobą ściśle powiązane?

— Sasho Nikolov,

@Kaveh: Według Seldina (2006) Logika Kościoła i Curry'ego , cele i składnia rachunku lambda zostały opracowane w latach 1928–1929, na długo zanim Church zdał sobie sprawę z ogólnego pojęcia funkcji rekurencyjnej. Moja odpowiedź przydałaby się na osi czasu, ale nie mam teraz czasu, aby ją zebrać.

— Charles Stewart

1

@Charles: Kościół był w Getyndze 1927–1928. Z pewnością był świadomy tego, co się działo na temat teorii funkcji rekurencyjnych i programu Hilberta. Wynik Ackermanna dotyczący nieprymitywnej funkcji rekurencyjnej pochodzi z tego samego roku. Kościół próbował zbudować podstawy matematyki. Wszystko to wydarzyło się przed pracą Turinga. Zobacz to . Kleene udowodnił równoważność ogólnych funkcji rekurencyjnych i funkcji definiowalnej przed pracą Turinga. Twój ostatni akapit jest mylący, ponieważ daje wrażenie, że byli

λ

$\lambda$

— Kaveh

1

@Charles, tak jak napisałem, zgadzam się, że pierwotną motywacją Kościoła było zbudowanie fundamentu (coś w rodzaju systemu Frege'a) (AFAIK), ale on również uważał go za model obliczeniowy przed pracą Turinga. Nie sądzę, aby odpowiedź musiała zostać usunięta, poprawienie drugiego akapitu powinno być w porządku. (powodem, dla którego skomentowałem to, że w ostatnich czasach ludzie nie doceniają pracy Kościoła w obliczeniach.)

— Kaveh

26

Chciałbym tylko zauważyć, że podczas gdy rachunek lambda i maszyny Turinga obliczają tę samą klasę funkcji liczbowych, nie są one dokładnie równoważne pod każdym względem, jaki można sobie wyobrazić. Na przykład w teorii wykonalności istnieją stwierdzenia, które można zrealizować za pomocą maszyny Turinga, ale nie za pomocą rachunku lambda. Jednym z takich stwierdzeń jest formalna teza Kościoła, która stwierdza:

\forall f : n a t \to n a t \exists e \forall n \exists k (T (e, n, k) \land U (k, f (n)))

$\forall f : \mathbf{nat} \to \mathbf{nat} \ \exists e \ \forall n \ \exists k \ \big( \mathbf{T}(e, n, k) \land \mathbf{U}(k,f(n)) \big)$

Tutaj jest T orzecznik KLEENE użytkownika . Realizatorem tego oświadczenia byłby program który akceptuje (reprezentację) mapy i wyprowadza (reprezentację) z pożądaną właściwością. W modelu maszyny Turinga mapa jest reprezentowana przez kod maszyny Turinga obliczającej , więc program jest po prostu (kod maszyny Turinga) funkcją tożsamości. Jeśli jednak użyjemy rachunku lambda, to ma obliczyć liczbę reprezentującą maszynę Turinga na podstawie terminu lambda reprezentującego funkcję $\mathbf{T}$ $c$ $f$ $e$ $f$ $f$ $c$ $c$ $f$ . Tego nie da się zrobić (wyjaśnię dlaczego, jeśli zadacie to jako osobne pytanie).

— Andrej Bauer
źródło

4

Mamy teraz znaczniki .

T_{E} X

$T_EX$

— András Salamon

Andrej, artykuł z Wikipedii używa innej kolejności parametrów, których używasz, drugi argument to dane wejściowe, a trzeci to kod zatrzymania obliczeń, pierwszy argument to kod maszyny. Wydaje mi się, że podajesz CT, edytowałem go na podstawie vDT88.

— Kaveh,

Jeszcze jedno, wydaje się, że dla wykonalności podajesz jako kod TM i oczekujesz -term, ale czy nie byłoby bardziej naturalne podawanie również jako -term, a wtedy funkcja tożsamości działałaby ? (Jeśli wolisz, mogę zadać to osobne pytanie).

f

$f$

λ

$\lambda$

f

$f$

λ

$\lambda$

— Kaveh

@Kaveh: Myślę, że było na odwrót, ale zastanawiam się także, dlaczego nie jest naturalne, aby mieć również dane wyjściowe tego samego typu co dane wejściowe w przypadku rachunku lambda.

— Abel Molina,

1

Czy coś w rodzaju realizatora stwierdzenia „każdy jest ciągły”? A może realizator dla „przestrzeni Cantora i przestrzeni Baire są homeomorficzne”?

f : R \to R

$f : \mathbb{R} \to \mathbb{R}$

2^{N}

$2^\mathbb{N}$

N^{N}

$\mathbb{N}^\mathbb{N}$

— Andrej Bauer,

11

Są one powiązane zarówno matematycznie, jak i historycznie.

Rachunek lambda został opracowany w latach 1928–1929 przez Alonzo Church (opublikowany w 1932 r.).

Maszyna Turinga została opracowana w latach 1935–1937 przez Alana Turinga (opublikowana w 1937 r.).

Alan Turing był doktorem Alonzo Church. student w Princeton w latach 1936–1938.

Maszyny Turinga i rachunek lambda są równoważne pod względem mocy obliczeniowej: każda z nich może skutecznie symulować drugą.

— Matt Might
źródło

6

Entscheidungsproblem jest jednym ze słynnych 23 problemów zaproponowanych przez matematyka Davida Hilberta.

Odpowiednio w 1936 i 1937 Alonzo Church i Alan Turing opublikowali niezależne artykuły pokazujące, że nie można algorytmicznie decydować, czy twierdzenia arytmetyczne są prawdziwe, czy fałszywe, a zatem niemożliwe jest ogólne rozwiązanie Entscheidungsproblem.

Dokonał tego Alonzo Church w 1936 r. Z koncepcją „efektywnej obliczalności” na podstawie rachunku λ oraz Alan Turing w tym samym roku ze swoją koncepcją maszyn Turinga. Później uznano, że są to równoważne modele obliczeń. - Wikipedia

Więc rachunek lambda i maszyny Turinga nie tylko ściśle związane, ale są one równoważne modele obliczeniowe .

Być może spodoba ci się również przeczytanie Annotowanego Turinga: Zwiedzanie z przewodnikiem przez historyczny artykuł Alana Turinga na temat obliczalności i maszyny Turinga autorstwa Charlesa Petzolda . Ta książka zawiera kilka interesujących informacji na ten temat.

— Pratik Deoghare
źródło

4

Maszyny Turinga i rachunek Lambda to dwa modele, które wychwytują pojęcie algorytmu (obliczenia mechaniczne). Rachunek lambda został wymyślony przez Kościół do wykonywania obliczeń z funkcjami. Jest to podstawa funkcjonalnych języków programowania. Zasadniczo każdy problem, który można obliczać (rozstrzygać) przez maszyny Turinga, można również obliczać za pomocą rachunku Lambda. Są to dwa równoważne modele obliczeń (do czynników wielomianowych) i oba próbują uchwycić moc dowolnego obliczenia mechanicznego.

— Mohammad Al-Turkistany
źródło